Handle Implicit Type for identonly binders in notations #19003
Closed
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
SkySkimmer
added
the
request: full CI
coqbot-app
bot
removed
the
request: full CI
|
🔴 CI failures at commit e7bb878 without any failure in the test-suite ✔️ Corresponding jobs for the base commit 00ef3a2 succeeded ❔ Ask me to try to extract minimal test cases that can be added to the test-suite 🏃
|
|
@coqbot ci minimize |
|
I have initiated minimization at commit e7bb878 for the suggested targets ci-iris, ci-mathcomp, ci-mathcomp_1, ci-metacoq, ci-perennial, ci-sf as requested. |
|
Minimized File /home/runner/work/run-coq-bug-minimizer/run-coq-bug-minimizer/builds/coq/coq-failing/_build_ci/sf/slf-current/LibSepReference.v (from ci-sf) (full log on GitHub Actions - verbose log) We are collecting data on the user experience of the Coq Bug Minimizer. 🌟 Minimized Coq File (consider adding this file to the test-suite)(* -*- mode: coq; coq-prog-args: ("-emacs" "-q" "-w" "-implicit-core-hint-db,-ambiguous-paths" "-w" "-deprecated-native-compiler-option" "-native-compiler" "ondemand" "-Q" "/github/workspace/cwd" "Top" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/sf/slf-current" "SLF" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq/user-contrib/Ltac2" "Ltac2" "-top" "SLF.LibSepReference") -*- *)
(* File reduced by coq-bug-minimizer from original input, then from 4306 lines to 103 lines, then from 116 lines to 600 lines, then from 604 lines to 106 lines, then from 119 lines to 176 lines, then from 181 lines to 107 lines, then from 120 lines to 489 lines, then from 493 lines to 117 lines, then from 130 lines to 4151 lines, then from 4153 lines to 128 lines, then from 141 lines to 1101 lines, then from 1104 lines to 129 lines, then from 134 lines to 131 lines *)
(* coqc version 8.20+alpha compiled with OCaml 4.09.0
coqtop version runner-t7b1znuaq-project-4504-concurrent-4:/builds/coq/coq/_build/default,(HEAD detached at e220577dc5a4) (e220577dc5a4cfa9bbac925c2e3fb42236b36b54)
Expected coqc runtime on this file: 0.244 sec *)
Require Coq.ZArith.ZArith.
Export Coq.ZArith.ZArith.
Notation "'int'" := Z : Int_scope.
Declare Scope liblist_scope.
Open Scope liblist_scope.
Infix "::" := cons (at level 60, right associativity) : liblist_scope.
Fixpoint nat_seq (start:nat) (nb:nat) :=
match nb with
| O => nil
| S nb' => start :: nat_seq (S start) nb'
end.
Module Export LibListExec.
Set Implicit Arguments.
Module Import RewListExec.
End RewListExec.
Definition length : forall A, list A -> nat.
Admitted.
Definition map : forall A B, (A->B) -> list A -> list B.
Admitted.
Open Scope Int_scope.
Definition var : Type.
Admitted.
Inductive prim : Type :=
| val_ref : prim
| val_get : prim
| val_set : prim
| val_free : prim
| val_neg : prim
| val_opp : prim
| val_eq : prim
| val_add : prim
| val_neq : prim
| val_sub : prim
| val_mul : prim
| val_div : prim
| val_mod : prim
| val_rand : prim
| val_le : prim
| val_lt : prim
| val_ge : prim
| val_gt : prim
| val_ptr_add : prim.
Definition loc : Type.
Admitted.
Inductive val : Type :=
| val_unit : val
| val_bool : bool -> val
| val_int : int -> val
| val_loc : loc -> val
| val_prim : prim -> val
| val_fun : var -> trm -> val
| val_fix : var -> var -> trm -> val
| val_uninit : val
| val_error : val
with trm : Type :=
| trm_val : val -> trm
| trm_var : var -> trm
| trm_fun : var -> trm -> trm
| trm_fix : var -> var -> trm -> trm
| trm_app : trm -> trm -> trm
| trm_seq : trm -> trm -> trm
| trm_let : var -> trm -> trm -> trm
| trm_if : trm -> trm -> trm -> trm.
Definition heap : Type.
Admitted.
Implicit Types p : loc.
Declare Scope hprop_scope.
Open Scope hprop_scope.
Definition hprop := heap -> Prop.
Definition hempty : hprop.
Admitted.
Definition hstar (H1 H2 : hprop) : hprop.
Admitted.
Definition hexists A (J:A->hprop) : hprop.
Admitted.
Notation "\[]" := (hempty)
(at level 0) : hprop_scope.
Notation "H1 '\*' H2" := (hstar H1 H2)
(at level 41, right associativity) : hprop_scope.
Notation "'\exists' x1 .. xn , H" :=
(hexists (fun x1 => .. (hexists (fun xn => H)) ..))
(at level 39, x1 binder, H at level 50, right associativity,
format "'[' '\exists' '/ ' x1 .. xn , '/ ' H ']'") : hprop_scope.
Definition hpure (P:Prop) : hprop.
Admitted.
Notation "\[ P ]" := (hpure P)
(at level 0, format "\[ P ]") : hprop_scope.
Definition triple (t:trm) (H:hprop) (Q:val->hprop) : Prop.
Admitted.
Notation "'funloc' p '=>' H" :=
(fun (r:val) => \exists p, \[r = val_loc p] \* H)
(at level 200, p name, format "'funloc' p '=>' H") : hprop_scope.
Definition field : Type.
exact (nat).
Defined.
Definition hrecord_field : Type := (field * val).
Definition hrecord_fields : Type.
exact (list hrecord_field).
Defined.
Parameter hrecord : forall (kvs:hrecord_fields) (p:loc), hprop.
Parameter val_alloc_hrecord : forall (ks:list field), trm.
Parameter triple_alloc_hrecord : forall ks,
ks = nat_seq 0 (LibListExec.length ks) ->
triple (val_alloc_hrecord ks)
\[]
(funloc p => hrecord (LibListExec.map (fun k => (k,val_uninit)) ks) p).🛠️ Intermediate Coq File (useful for debugging if minimization did not go as far as you wanted)🛠️ 📜 Intermediate Coq File log (useful for debugging if minimization did not go as far as you wanted)📜 Build Log (contains the Coq error message) (truncated to last 8.0KiB; full 3.1MiB file on GitHub Actions Artifacts under
|
|
Minimized File /home/runner/work/run-coq-bug-minimizer/run-coq-bug-minimizer/builds/coq/coq-failing/_build_ci/mathcomp_1/mathcomp/ssreflect/seq.v (from ci-mathcomp_1) (full log on GitHub Actions - verbose log) We are collecting data on the user experience of the Coq Bug Minimizer. 🌟 Minimized Coq File (consider adding this file to the test-suite)(* -*- mode: coq; coq-prog-args: ("-emacs" "-q" "-w" "-projection-no-head-constant" "-w" "-redundant-canonical-projection" "-w" "-notation-overridden" "-w" "+duplicate-clear" "-w" "-ambiguous-paths" "-w" "+non-primitive-record" "-w" "+undeclared-scope" "-w" "+deprecated-hint-without-locality" "-w" "+deprecated-hint-rewrite-without-locality" "-w" "-opaque-let" "-w" "-deprecated-native-compiler-option" "-native-compiler" "ondemand" "-R" "/github/workspace/builds/coq/coq-failing/_build_ci/mathcomp_1/mathcomp" "mathcomp" "-Q" "/github/workspace/cwd" "Top" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq/user-contrib/Ltac2" "Ltac2" "-I" "/github/workspace/builds/coq/coq-failing/_build_ci/mathcomp_1/mathcomp" "-top" "mathcomp.ssreflect.seq") -*- *)
(* File reduced by coq-bug-minimizer from original input, then from 4741 lines to 61 lines, then from 74 lines to 2244 lines, then from 2249 lines to 77 lines, then from 90 lines to 1126 lines, then from 1131 lines to 89 lines, then from 102 lines to 324 lines, then from 329 lines to 90 lines, then from 103 lines to 161 lines, then from 166 lines to 90 lines, then from 95 lines to 92 lines *)
(* coqc version 8.20+alpha compiled with OCaml 4.14.1
coqtop version runner-t7b1znuaq-project-4504-concurrent-1:/builds/coq/coq/_build/default,(HEAD detached at e220577dc5a4c) (e220577dc5a4cfa9bbac925c2e3fb42236b36b54)
Expected coqc runtime on this file: 0.120 sec *)
Require Coq.ssr.ssrbool.
Axiom proof_admitted : False.
Tactic Notation "admit" := abstract case proof_admitted.
Export Coq.ssr.ssreflect.
Export Coq.ssr.ssrbool.
Set Implicit Arguments.
Module Export Equality.
Definition axiom T (e : rel T) := forall x y, reflect (x = y) (e x y).
Structure mixin_of T := Mixin {op : rel T; _ : axiom op}.
Notation class_of := mixin_of (only parsing).
Structure type := Pack {sort; _ : class_of sort}.
Coercion sort : type >-> Sortclass.
Notation eqType := type.
Notation EqMixin := Mixin.
Notation EqType T m := (@Pack T m).
Notation succn := Datatypes.S.
Notation "n .+1" := (succn n) (at level 2, left associativity,
format "n .+1") : nat_scope.
Fixpoint eqn m n {struct m} :=
match m, n with
| 0, 0 => true
| m'.+1, n'.+1 => eqn m' n'
| _, _ => false
end.
Lemma eqnP : Equality.axiom eqn.
Admitted.
Canonical nat_eqMixin := EqMixin eqnP.
Canonical nat_eqType := Eval hnf in EqType nat nat_eqMixin.
Unset Strict Implicit.
Declare Scope seq_scope.
Open Scope seq_scope.
Notation seq := list.
Infix "::" := cons : seq_scope.
Notation "[ :: ]" := nil (at level 0, format "[ :: ]") : seq_scope.
Section EqSeq.
Variables (n0 : nat) (T : eqType) (x0 : T).
Definition seq_eqclass := seq T.
Coercion pred_of_seq (s : seq_eqclass) : {pred T}.
admit.
Defined.
Canonical seq_predType := PredType (pred_of_seq : seq T -> pred T).
Fixpoint uniq s := if s is x :: s' then (x \notin s') && uniq s' else true.
End EqSeq.
Section Map.
Variables (n0 : nat) (T1 : Type) (x1 : T1).
Variables (T2 : Type) (x2 : T2) (f : T1 -> T2).
Fixpoint map s := if s is x :: s' then f x :: map s' else [::].
End Map.
Section Zip.
Variables (S T : Type) (r : S -> T -> bool).
Definition unzip1 := map (@fst S T).
Definition unzip2 := map (@snd S T).
End Zip.
Variable T : eqType.
Implicit Types (x : T) (s t : seq T) (bs : seq (T * nat)) (acc : seq (seq T)).
Definition wf_tally :=
[qualify a bs : seq (T * nat) | uniq (unzip1 bs) && (0 \notin unzip2 bs)].🛠️ Intermediate Coq File (useful for debugging if minimization did not go as far as you wanted)🛠️ 📜 Intermediate Coq File log (useful for debugging if minimization did not go as far as you wanted)📜 Build Log (contains the Coq error message) (truncated to last 8.0KiB; full 3.2MiB file on GitHub Actions Artifacts under
|
|
Partially Minimized File /home/runner/work/run-coq-bug-minimizer/run-coq-bug-minimizer/builds/coq/coq-failing/_build_ci/mathcomp/mathcomp/ssreflect/seq.v (from ci-mathcomp) (full log on GitHub Actions - verbose log) We are collecting data on the user experience of the Coq Bug Minimizer. ⭐ 🏗️ Partially Minimized Coq File (could not inline HB.structures)(* -*- mode: coq; coq-prog-args: ("-emacs" "-q" "-w" "-projection-no-head-constant" "-w" "-redundant-canonical-projection" "-w" "-notation-overridden" "-w" "+duplicate-clear" "-w" "-ambiguous-paths" "-w" "+non-primitive-record" "-w" "+undeclared-scope" "-w" "+deprecated-hint-without-locality" "-w" "+deprecated-hint-rewrite-without-locality" "-w" "-elpi.add-const-for-axiom-or-sectionvar" "-w" "-opaque-let" "-w" "-argument-scope-delimiter" "-w" "-overwriting-delimiting-key" "-w" "-deprecated-native-compiler-option" "-native-compiler" "ondemand" "-R" "/github/workspace/builds/coq/coq-failing/_build_ci/mathcomp/mathcomp" "mathcomp" "-Q" "/github/workspace/cwd" "Top" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq/user-contrib/HB" "HB" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq/user-contrib/Ltac2" "Ltac2" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq/user-contrib/elpi" "elpi" "-I" "/github/workspace/builds/coq/coq-failing/_build_ci/mathcomp/mathcomp" "-top" "mathcomp.ssreflect.seq") -*- *)
(* File reduced by coq-bug-minimizer from original input, then from 4743 lines to 61 lines, then from 74 lines to 2258 lines, then from 2263 lines to 78 lines, then from 91 lines to 1146 lines, then from 1151 lines to 85 lines, then from 98 lines to 225 lines, then from 231 lines to 86 lines, then from 100 lines to 160 lines, then from 166 lines to 86 lines, then from 92 lines to 88 lines *)
(* coqc version 8.20+alpha compiled with OCaml 4.14.1
coqtop version runner-t7b1znuaq-project-4504-concurrent-1:/builds/coq/coq/_build/default,(HEAD detached at e220577dc5a4c) (e220577dc5a4cfa9bbac925c2e3fb42236b36b54)
Modules that could not be inlined: HB.structures
Expected coqc runtime on this file: 0.362 sec *)
Require Coq.ssr.ssrbool.
Require HB.structures.
Axiom proof_admitted : False.
Tactic Notation "admit" := abstract case proof_admitted.
Export Coq.ssr.ssreflect.
Export Coq.ssr.ssrbool.
Import HB.structures.
Set Implicit Arguments.
Definition eq_axiom T (e : rel T) := forall x y, reflect (x = y) (e x y).
HB.mixin Record hasDecEq T := { eq_op : rel T; eqP : eq_axiom eq_op }.
#[mathcomp(axiom="eq_axiom"), short(type="eqType")]
HB.structure Definition Equality := { T of hasDecEq T }.
Notation succn := Datatypes.S.
Notation "n .+1" := (succn n) (at level 2, left associativity,
format "n .+1") : nat_scope.
Fixpoint eqn m n {struct m} :=
match m, n with
| 0, 0 => true
| m'.+1, n'.+1 => eqn m' n'
| _, _ => false
end.
Lemma eqnP : Equality.axiom eqn.
Admitted.
HB.instance Definition _ := hasDecEq.Build nat eqnP.
Unset Strict Implicit.
Declare Scope seq_scope.
Open Scope seq_scope.
Notation seq := list.
Infix "::" := cons : seq_scope.
Notation "[ :: ]" := nil (at level 0, format "[ :: ]") : seq_scope.
Section EqSeq.
Variables (n0 : nat) (T : eqType) (x0 : T).
Definition seq_eqclass := seq T.
Coercion pred_of_seq (s : seq_eqclass) : {pred T}.
admit.
Defined.
Canonical seq_predType := PredType (pred_of_seq : seq T -> pred T).
Fixpoint uniq s := if s is x :: s' then (x \notin s') && uniq s' else true.
End EqSeq.
Section Map.
Variables (n0 : nat) (T1 : Type) (x1 : T1).
Variables (T2 : Type) (x2 : T2) (f : T1 -> T2).
Fixpoint map s := if s is x :: s' then f x :: map s' else [::].
End Map.
Section Zip.
Variables (S T : Type) (r : S -> T -> bool).
Definition unzip1 := map (@fst S T).
Definition unzip2 := map (@snd S T).
End Zip.
Variable T : eqType.
Implicit Types (x : T) (s t : seq T) (bs : seq (T * nat)) (acc : seq (seq T)).
Definition wf_tally :=
[qualify a bs : seq (T * nat) | uniq (unzip1 bs) && (0 \notin unzip2 bs)].🛠️ Intermediate Coq File (useful for debugging if minimization did not go as far as you wanted) (truncated to 6.0KiB; full 50KiB file on GitHub Actions Artifacts under
|
|
Minimized File /home/runner/work/run-coq-bug-minimizer/run-coq-bug-minimizer/builds/coq/coq-failing/_build_ci/perennial/external/iris/iris/algebra/view.v (from ci-perennial) (full log on GitHub Actions - verbose log) We are collecting data on the user experience of the Coq Bug Minimizer. 🌟 Minimized Coq File (consider adding this file to the test-suite)(* -*- mode: coq; coq-prog-args: ("-emacs" "-w" "-ssr-search-moved" "-w" "+deprecated-instance-without-locality" "-w" "-future-coercion-class-field" "-w" "+deprecated-hint-rewrite-without-locality" "-w" "-deprecated-field-instance-without-locality" "-w" "+deprecated-tactic-notation" "-w" "-deprecated-since-8.19" "-w" "-deprecated-since-8.20" "-w" "-notation-overridden,-redundant-canonical-projection,-deprecated-typeclasses-transparency-without-locality" "-w" "-deprecated-native-compiler-option,-native-compiler-disabled" "-native-compiler" "ondemand" "-Q" "/github/workspace/cwd" "Top" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/perennial/src" "Perennial" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/perennial/external/stdpp/stdpp" "stdpp" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/perennial/external/stdpp/stdpp_unstable" "stdpp.unstable" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/perennial/external/stdpp/stdpp_bitvector" "stdpp.bitvector" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/perennial/external/iris/iris" "iris" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/perennial/external/iris/iris_deprecated" "iris.deprecated" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/perennial/external/iris/iris_unstable" "iris.unstable" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/perennial/external/iris/iris_heap_lang" "iris.heap_lang" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/perennial/external/coqutil/src/coqutil" "coqutil" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/perennial/external/Goose" "Goose" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/perennial/external/record-update/src" "RecordUpdate" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/perennial/external/coq-tactical/src" "Tactical" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/perennial/external/iris-named-props/src" "iris_named_props" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq/user-contrib/Ltac2" "Ltac2" "-top" "iris.algebra.view") -*- *)
(* File reduced by coq-bug-minimizer from original input, then from 702 lines to 65 lines, then from 78 lines to 1129 lines, then from 1133 lines to 74 lines, then from 87 lines to 490 lines, then from 495 lines to 77 lines, then from 90 lines to 385 lines, then from 390 lines to 81 lines, then from 94 lines to 2144 lines, then from 2149 lines to 196 lines, then from 209 lines to 323 lines, then from 328 lines to 204 lines, then from 217 lines to 2215 lines, then from 2217 lines to 232 lines, then from 245 lines to 307 lines, then from 312 lines to 232 lines, then from 245 lines to 311 lines, then from 316 lines to 232 lines, then from 245 lines to 310 lines, then from 315 lines to 232 lines, then from 245 lines to 635 lines, then from 640 lines to 232 lines, then from 245 lines to 660 lines, then from 665 lines to 232 lines, then from 245 lines to 5699 lines, then from 5704 lines to 240 lines, then from 253 lines to 1931 lines, then from 1935 lines to 244 lines, then from 257 lines to 796 lines, then from 801 lines to 250 lines, then from 263 lines to 1197 lines, then from 1200 lines to 249 lines, then from 262 lines to 552 lines, then from 557 lines to 266 lines, then from 279 lines to 348 lines, then from 353 lines to 277 lines, then from 290 lines to 1931 lines, then from 1931 lines to 327 lines, then from 332 lines to 328 lines *)
(* coqc version 8.20+alpha compiled with OCaml 4.14.1
coqtop version runner-t7b1znuaq-project-4504-concurrent-1:/builds/coq/coq/_build/default,(HEAD detached at e220577dc5a4c) (e220577dc5a4cfa9bbac925c2e3fb42236b36b54)
Expected coqc runtime on this file: 0.281 sec *)
Require Coq.QArith.Qcanon.
Require Coq.Unicode.Utf8.
Module Export stdpp_DOT_base_WRAPPED.
Module Export base.
Export Coq.Classes.Morphisms.
Export Coq.Lists.List.
Export Coq.Setoids.Setoid.
Export Coq.Init.Peano.
Export Coq.Unicode.Utf8.
Export ListNotations.
Export Coq.Program.Basics.
Global Generalizable All Variables.
Declare Scope stdpp_scope.
Global Open Scope stdpp_scope.
Notation "(=)" := eq (only parsing) : stdpp_scope.
Notation "(=@{ A } )" := (@eq A) (only parsing) : stdpp_scope.
Class Equiv A := equiv: relation A.
Infix "≡" := equiv (at level 70, no associativity) : stdpp_scope.
Infix "≡@{ A }" := (@equiv A _)
(at level 70, only parsing, no associativity) : stdpp_scope.
Notation "(≡)" := equiv (only parsing) : stdpp_scope.
Notation "(≡@{ A } )" := (@equiv A _) (only parsing) : stdpp_scope.
Class Decision (P : Prop) := decide : {P} + {¬P}.
Global Arguments decide _ {_} : simpl never, assert.
Class RelDecision {A B} (R : A → B → Prop) :=
decide_rel x y :: Decision (R x y).
Notation EqDecision A := (RelDecision (=@{A})).
Class Inj {A B} (R : relation A) (S : relation B) (f : A → B) : Prop :=
inj x y : S (f x) (f y) → R x y.
Class Comm {A B} (R : relation A) (f : B → B → A) : Prop :=
comm x y : R (f x y) (f y x).
Class LeftId {A} (R : relation A) (i : A) (f : A → A → A) : Prop :=
left_id x : R (f i x) x.
Class Assoc {A} (R : relation A) (f : A → A → A) : Prop :=
assoc x y z : R (f x (f y z)) (f (f x y) z).
End base.
Module Export stdpp.
Module Export base.
Include stdpp_DOT_base_WRAPPED.base.
End base.
Module Export stdpp_DOT_proof_irrel_WRAPPED.
Module Export proof_irrel.
Export stdpp.base.
End proof_irrel.
Module Export stdpp.
Module Export proof_irrel.
Include stdpp_DOT_proof_irrel_WRAPPED.proof_irrel.
End proof_irrel.
Module Export stdpp_DOT_decidable_WRAPPED.
Module Export decidable.
Export stdpp.proof_irrel.
Notation cast_if S := (if S then left _ else right _).
Program Definition inj_eq_dec `{EqDecision A} {B} (f : B → A)
`{!Inj (=) (=) f} : EqDecision B := λ x y, cast_if (decide (f x = f y)).
Solve Obligations with firstorder congruence.
Definition bool_decide (P : Prop) {dec : Decision P} : bool.
Admitted.
End decidable.
Module Export stdpp.
Module Export decidable.
Include stdpp_DOT_decidable_WRAPPED.decidable.
End decidable.
Global Instance option_equiv `{Equiv A} : Equiv (option A).
Admitted.
Import Coq.QArith.Qcanon.
Export stdpp.decidable.
Record Qp := mk_Qp { Qp_to_Qc : Qc ; Qp_prf : (0 < Qp_to_Qc)%Qc }.
Section general_properties.
Context {A : Type}.
Implicit Types l k : list A.
Global Instance list_eq_nil_dec l : Decision (l = []).
Admitted.
End general_properties.
Class Dist A := dist : nat → relation A.
Notation "x ≡{ n }≡ y" := (dist n x y)
(at level 70, n at next level, format "x ≡{ n }≡ y").
Notation NonExpansive f := (∀ n, Proper (dist n ==> dist n) f).
Notation NonExpansive2 f := (∀ n, Proper (dist n ==> dist n ==> dist n) f).
Record OfeMixin A `{Equiv A, Dist A} := {
mixin_equiv_dist (x y : A) : x ≡ y ↔ ∀ n, x ≡{n}≡ y;
mixin_dist_equivalence n : Equivalence (@dist A _ n);
mixin_dist_lt n m (x y : A) : x ≡{n}≡ y → m < n → x ≡{m}≡ y;
}.
Structure ofe := Ofe {
ofe_car :> Type;
ofe_equiv : Equiv ofe_car;
ofe_dist : Dist ofe_car;
ofe_mixin : OfeMixin ofe_car
}.
Global Arguments Ofe _ {_ _} _.
Global Hint Extern 0 (Equiv _) => refine (ofe_equiv _); shelve : typeclass_instances.
Global Hint Extern 0 (Dist _) => refine (ofe_dist _); shelve : typeclass_instances.
Definition ofe_mixin_of' A {Ac : ofe} (f : Ac → A) : OfeMixin Ac.
exact (ofe_mixin Ac).
Defined.
Notation ofe_mixin_of A :=
ltac:(let H := eval hnf in (ofe_mixin_of' A id) in exact H) (only parsing).
Class Monoid {M : ofe} (o : M → M → M) := {
monoid_unit : M;
monoid_ne : NonExpansive2 o;
monoid_assoc : Assoc (≡) o;
monoid_comm : Comm (≡) o;
monoid_left_id : LeftId (≡) monoid_unit o;
}.
Class PCore (A : Type) := pcore : A → option A.
Class Op (A : Type) := op : A → A → A.
Infix "⋅" := op (at level 50, left associativity) : stdpp_scope.
Notation "(⋅)" := op (only parsing) : stdpp_scope.
Definition included {A} `{!Equiv A, !Op A} (x y : A) := ∃ z, y ≡ x ⋅ z.
Infix "≼" := included (at level 70) : stdpp_scope.
Class ValidN (A : Type) := validN : nat → A → Prop.
Notation "✓{ n } x" := (validN n x)
(at level 20, n at next level, format "✓{ n } x").
Class Valid (A : Type) := valid : A → Prop.
Notation "✓ x" := (valid x) (at level 20) : stdpp_scope.
Definition includedN `{!Dist A, !Op A} (n : nat) (x y : A) := ∃ z, y ≡{n}≡ x ⋅ z.
Notation "x ≼{ n } y" := (includedN n x y)
(at level 70, n at next level, format "x ≼{ n } y") : stdpp_scope.
Section mixin.
Record CmraMixin A `{!Dist A, !Equiv A, !PCore A, !Op A, !Valid A, !ValidN A} := {
mixin_cmra_op_ne (x : A) : NonExpansive (op x);
mixin_cmra_pcore_ne n (x y : A) cx :
x ≡{n}≡ y → pcore x = Some cx → ∃ cy, pcore y = Some cy ∧ cx ≡{n}≡ cy;
mixin_cmra_validN_ne n : Proper (dist (A := A) n ==> impl) (validN n);
mixin_cmra_valid_validN (x : A) : ✓ x ↔ ∀ n, ✓{n} x;
mixin_cmra_validN_S n (x : A) : ✓{S n} x → ✓{n} x;
mixin_cmra_assoc : Assoc (≡@{A}) (⋅);
mixin_cmra_comm : Comm (≡@{A}) (⋅);
mixin_cmra_pcore_l (x : A) cx : pcore x = Some cx → cx ⋅ x ≡ x;
mixin_cmra_pcore_idemp (x : A) cx : pcore x = Some cx → pcore cx ≡ Some cx;
mixin_cmra_pcore_mono (x y : A) cx :
x ≼ y → pcore x = Some cx → ∃ cy, pcore y = Some cy ∧ cx ≼ cy;
mixin_cmra_validN_op_l n (x y : A) : ✓{n} (x ⋅ y) → ✓{n} x;
mixin_cmra_extend n (x y1 y2 : A) :
✓{n} x → x ≡{n}≡ y1 ⋅ y2 →
{ z1 : A & { z2 | x ≡ z1 ⋅ z2 ∧ z1 ≡{n}≡ y1 ∧ z2 ≡{n}≡ y2 } }
}.
End mixin.
#[projections(primitive=no)]
Structure cmra := Cmra' {
cmra_car :> Type;
cmra_equiv : Equiv cmra_car;
cmra_dist : Dist cmra_car;
cmra_pcore : PCore cmra_car;
cmra_op : Op cmra_car;
cmra_valid : Valid cmra_car;
cmra_validN : ValidN cmra_car;
cmra_ofe_mixin : OfeMixin cmra_car;
cmra_mixin : CmraMixin cmra_car;
}.
Global Arguments Cmra' _ {_ _ _ _ _ _} _ _.
Notation Cmra A m := (Cmra' A (ofe_mixin_of A%type) m) (only parsing).
Global Hint Extern 0 (PCore _) => refine (cmra_pcore _); shelve : typeclass_instances.
Global Hint Extern 0 (Op _) => refine (cmra_op _); shelve : typeclass_instances.
Global Hint Extern 0 (Valid _) => refine (cmra_valid _); shelve : typeclass_instances.
Global Hint Extern 0 (ValidN _) => refine (cmra_validN _); shelve : typeclass_instances.
Coercion cmra_ofeO (A : cmra) : ofe.
exact (Ofe A (cmra_ofe_mixin A)).
Defined.
Canonical Structure cmra_ofeO.
Definition cmra_mixin_of' A {Ac : cmra} (f : Ac → A) : CmraMixin Ac.
Admitted.
Notation cmra_mixin_of A :=
ltac:(let H := eval hnf in (cmra_mixin_of' A id) in exact H) (only parsing).
Class Unit (A : Type) := ε : A.
Record UcmraMixin A `{!Dist A, !Equiv A, !PCore A, !Op A, !Valid A, !Unit A} := {
mixin_ucmra_unit_valid : ✓ (ε : A);
mixin_ucmra_unit_left_id : LeftId (≡@{A}) ε (⋅);
mixin_ucmra_pcore_unit : pcore ε ≡@{option A} Some ε
}.
#[projections(primitive=no)]
Structure ucmra := Ucmra' {
ucmra_car :> Type;
ucmra_equiv : Equiv ucmra_car;
ucmra_dist : Dist ucmra_car;
ucmra_pcore : PCore ucmra_car;
ucmra_op : Op ucmra_car;
ucmra_valid : Valid ucmra_car;
ucmra_validN : ValidN ucmra_car;
ucmra_unit : Unit ucmra_car;
ucmra_ofe_mixin : OfeMixin ucmra_car;
ucmra_cmra_mixin : CmraMixin ucmra_car;
ucmra_mixin : UcmraMixin ucmra_car;
}.
Global Arguments Ucmra' _ {_ _ _ _ _ _ _} _ _ _.
Notation Ucmra A m :=
(Ucmra' A (ofe_mixin_of A%type) (cmra_mixin_of A%type) m) (only parsing).
Global Hint Extern 0 (Unit _) => refine (ucmra_unit _); shelve : typeclass_instances.
Coercion ucmra_ofeO (A : ucmra) : ofe.
exact (Ofe A (ucmra_ofe_mixin A)).
Defined.
Canonical Structure ucmra_ofeO.
Coercion ucmra_cmraR (A : ucmra) : cmra.
exact (Cmra' A (ucmra_ofe_mixin A) (ucmra_cmra_mixin A)).
Defined.
Canonical Structure ucmra_cmraR.
Section ucmra.
Context {A : ucmra}.
Global Instance cmra_monoid : Monoid (@op A _).
Admitted.
End ucmra.
Inductive dfrac :=
| DfracOwn : Qp → dfrac
| DfracDiscarded : dfrac
| DfracBoth : Qp → dfrac.
Record agree (A : Type) : Type := {
agree_car : list A;
agree_not_nil : bool_decide (agree_car = []) = false
}.
Fixpoint big_opL {M : ofe} {o : M → M → M} `{!Monoid o} {A} (f : nat → A → M) (xs : list A) : M :=
match xs with
| [] => monoid_unit
| x :: xs => o (f 0 x) (big_opL (λ n, f (S n)) xs)
end.
Global Arguments big_opL {M} o {_ A} _ !_ /.
Notation "'[^' o 'list]' k ↦ x ∈ l , P" := (big_opL o (λ k x, P) l)
(at level 200, o at level 1, l at level 10, k, x at level 1, right associativity,
format "[^ o list] k ↦ x ∈ l , P") : stdpp_scope.
Structure view_rel (A : ofe) (B : ucmra) := ViewRel {
view_rel_holds :> nat → A → B → Prop;
view_rel_mono n1 n2 a1 a2 b1 b2 :
view_rel_holds n1 a1 b1 →
a1 ≡{n2}≡ a2 →
b2 ≼{n2} b1 →
n2 ≤ n1 →
view_rel_holds n2 a2 b2;
view_rel_validN n a b :
view_rel_holds n a b → ✓{n} b;
view_rel_unit n :
∃ a, view_rel_holds n a ε
}.
Record view {A B} (rel : nat → A → B → Prop) :=
View { view_auth_proj : option (dfrac * agree A) ; view_frag_proj : B }.
Definition view_frag {A B} {rel : view_rel A B} (b : B) : view rel.
Admitted.
Notation "◯V a" := (view_frag a) (at level 20).
Section ofe.
Context {A B : ofe} (rel : nat → A → B → Prop).
Local Instance view_equiv : Equiv (view rel).
Admitted.
Local Instance view_dist : Dist (view rel).
Admitted.
Definition view_ofe_mixin : OfeMixin (view rel).
Admitted.
Canonical Structure viewO := Ofe (view rel) view_ofe_mixin.
End ofe.
Section cmra.
Context {A B} (rel : view_rel A B).
Implicit Types x y : view rel.
Local Instance view_valid_instance : Valid (view rel).
Admitted.
Local Instance view_validN_instance : ValidN (view rel).
Admitted.
Local Instance view_pcore_instance : PCore (view rel).
Admitted.
Local Instance view_op_instance : Op (view rel).
Admitted.
Lemma view_cmra_mixin : CmraMixin (view rel).
Admitted.
Canonical Structure viewR := Cmra (view rel) view_cmra_mixin.
Local Instance view_empty_instance : Unit (view rel).
Admitted.
Lemma view_ucmra_mixin : UcmraMixin (view rel).
Admitted.
Canonical Structure viewUR := Ucmra (view rel) view_ucmra_mixin.
Lemma big_opL_view_frag {C} (g : nat → C → B) (l : list C) :
(◯V [^op list] k↦x ∈ l, g k x) ≡ [^op list] k↦x ∈ l, ◯V (g k x).
Admitted.🛠️ Intermediate Coq File (useful for debugging if minimization did not go as far as you wanted)🛠️ 📜 Intermediate Coq File log (useful for debugging if minimization did not go as far as you wanted)📜 Build Log (contains the Coq error message) (truncated to last 8.0KiB; full 3.7MiB file on GitHub Actions Artifacts under
|
|
Minimized File /home/runner/work/run-coq-bug-minimizer/run-coq-bug-minimizer/builds/coq/coq-failing/_build_ci/iris/iris/algebra/view.v (from ci-iris) (full log on GitHub Actions - verbose log) We are collecting data on the user experience of the Coq Bug Minimizer. 🌟 Minimized Coq File (consider adding this file to the test-suite)(* -*- mode: coq; coq-prog-args: ("-emacs" "-q" "-w" "-notation-overridden" "-w" "-redundant-canonical-projection" "-w" "-unknown-warning" "-w" "-argument-scope-delimiter" "-w" "-deprecated-native-compiler-option" "-native-compiler" "ondemand" "-Q" "/github/workspace/cwd" "Top" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/iris/iris/prelude" "iris.prelude" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/iris/iris/algebra" "iris.algebra" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/iris/iris/si_logic" "iris.si_logic" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/iris/iris/bi" "iris.bi" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/iris/iris/proofmode" "iris.proofmode" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/iris/iris/base_logic" "iris.base_logic" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/iris/iris/program_logic" "iris.program_logic" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/iris/iris_heap_lang" "iris.heap_lang" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/iris/iris_unstable" "iris.unstable" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/iris/iris_deprecated" "iris.deprecated" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq/user-contrib/Autosubst" "Autosubst" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq/user-contrib/Ltac2" "Ltac2" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq/user-contrib/stdpp" "stdpp" "-top" "iris.algebra.view") -*- *)
(* File reduced by coq-bug-minimizer from original input, then from 702 lines to 65 lines, then from 78 lines to 1129 lines, then from 1133 lines to 74 lines, then from 87 lines to 490 lines, then from 495 lines to 77 lines, then from 90 lines to 385 lines, then from 390 lines to 81 lines, then from 94 lines to 2144 lines, then from 2149 lines to 196 lines, then from 209 lines to 323 lines, then from 328 lines to 204 lines, then from 217 lines to 2215 lines, then from 2217 lines to 232 lines, then from 245 lines to 307 lines, then from 312 lines to 232 lines, then from 245 lines to 311 lines, then from 316 lines to 232 lines, then from 245 lines to 310 lines, then from 315 lines to 232 lines, then from 245 lines to 635 lines, then from 640 lines to 232 lines, then from 245 lines to 660 lines, then from 665 lines to 232 lines, then from 245 lines to 5699 lines, then from 5704 lines to 240 lines, then from 253 lines to 1931 lines, then from 1935 lines to 244 lines, then from 257 lines to 796 lines, then from 801 lines to 250 lines, then from 263 lines to 1197 lines, then from 1200 lines to 249 lines, then from 262 lines to 552 lines, then from 557 lines to 266 lines, then from 279 lines to 348 lines, then from 353 lines to 277 lines, then from 290 lines to 1931 lines, then from 1931 lines to 327 lines, then from 332 lines to 328 lines *)
(* coqc version 8.20+alpha compiled with OCaml 4.14.1
coqtop version runner-t7b1znuaq-project-4504-concurrent-1:/builds/coq/coq/_build/default,(HEAD detached at e220577dc5a4c) (e220577dc5a4cfa9bbac925c2e3fb42236b36b54)
Expected coqc runtime on this file: 0.313 sec *)
Require Coq.QArith.Qcanon.
Require Coq.Unicode.Utf8.
Module Export stdpp_DOT_base_WRAPPED.
Module Export base.
Export Coq.Classes.Morphisms.
Export Coq.Lists.List.
Export Coq.Setoids.Setoid.
Export Coq.Init.Peano.
Export Coq.Unicode.Utf8.
Export ListNotations.
Export Coq.Program.Basics.
Global Generalizable All Variables.
Declare Scope stdpp_scope.
Global Open Scope stdpp_scope.
Notation "(=)" := eq (only parsing) : stdpp_scope.
Notation "(=@{ A } )" := (@eq A) (only parsing) : stdpp_scope.
Class Equiv A := equiv: relation A.
Infix "≡" := equiv (at level 70, no associativity) : stdpp_scope.
Infix "≡@{ A }" := (@equiv A _)
(at level 70, only parsing, no associativity) : stdpp_scope.
Notation "(≡)" := equiv (only parsing) : stdpp_scope.
Notation "(≡@{ A } )" := (@equiv A _) (only parsing) : stdpp_scope.
Class Decision (P : Prop) := decide : {P} + {¬P}.
Global Arguments decide _ {_} : simpl never, assert.
Class RelDecision {A B} (R : A → B → Prop) :=
decide_rel x y :: Decision (R x y).
Notation EqDecision A := (RelDecision (=@{A})).
Class Inj {A B} (R : relation A) (S : relation B) (f : A → B) : Prop :=
inj x y : S (f x) (f y) → R x y.
Class Comm {A B} (R : relation A) (f : B → B → A) : Prop :=
comm x y : R (f x y) (f y x).
Class LeftId {A} (R : relation A) (i : A) (f : A → A → A) : Prop :=
left_id x : R (f i x) x.
Class Assoc {A} (R : relation A) (f : A → A → A) : Prop :=
assoc x y z : R (f x (f y z)) (f (f x y) z).
End base.
Module Export stdpp.
Module Export base.
Include stdpp_DOT_base_WRAPPED.base.
End base.
Module Export stdpp_DOT_proof_irrel_WRAPPED.
Module Export proof_irrel.
Export stdpp.base.
End proof_irrel.
Module Export stdpp.
Module Export proof_irrel.
Include stdpp_DOT_proof_irrel_WRAPPED.proof_irrel.
End proof_irrel.
Module Export stdpp_DOT_decidable_WRAPPED.
Module Export decidable.
Export stdpp.proof_irrel.
Notation cast_if S := (if S then left _ else right _).
Program Definition inj_eq_dec `{EqDecision A} {B} (f : B → A)
`{!Inj (=) (=) f} : EqDecision B := λ x y, cast_if (decide (f x = f y)).
Solve Obligations with firstorder congruence.
Definition bool_decide (P : Prop) {dec : Decision P} : bool.
Admitted.
End decidable.
Module Export stdpp.
Module Export decidable.
Include stdpp_DOT_decidable_WRAPPED.decidable.
End decidable.
Global Instance option_equiv `{Equiv A} : Equiv (option A).
Admitted.
Import Coq.QArith.Qcanon.
Export stdpp.decidable.
Record Qp := mk_Qp { Qp_to_Qc : Qc ; Qp_prf : (0 < Qp_to_Qc)%Qc }.
Section general_properties.
Context {A : Type}.
Implicit Types l k : list A.
Global Instance list_eq_nil_dec l : Decision (l = []).
Admitted.
End general_properties.
Class Dist A := dist : nat → relation A.
Notation "x ≡{ n }≡ y" := (dist n x y)
(at level 70, n at next level, format "x ≡{ n }≡ y").
Notation NonExpansive f := (∀ n, Proper (dist n ==> dist n) f).
Notation NonExpansive2 f := (∀ n, Proper (dist n ==> dist n ==> dist n) f).
Record OfeMixin A `{Equiv A, Dist A} := {
mixin_equiv_dist (x y : A) : x ≡ y ↔ ∀ n, x ≡{n}≡ y;
mixin_dist_equivalence n : Equivalence (@dist A _ n);
mixin_dist_lt n m (x y : A) : x ≡{n}≡ y → m < n → x ≡{m}≡ y;
}.
Structure ofe := Ofe {
ofe_car :> Type;
ofe_equiv : Equiv ofe_car;
ofe_dist : Dist ofe_car;
ofe_mixin : OfeMixin ofe_car
}.
Global Arguments Ofe _ {_ _} _.
Global Hint Extern 0 (Equiv _) => refine (ofe_equiv _); shelve : typeclass_instances.
Global Hint Extern 0 (Dist _) => refine (ofe_dist _); shelve : typeclass_instances.
Definition ofe_mixin_of' A {Ac : ofe} (f : Ac → A) : OfeMixin Ac.
exact (ofe_mixin Ac).
Defined.
Notation ofe_mixin_of A :=
ltac:(let H := eval hnf in (ofe_mixin_of' A id) in exact H) (only parsing).
Class Monoid {M : ofe} (o : M → M → M) := {
monoid_unit : M;
monoid_ne : NonExpansive2 o;
monoid_assoc : Assoc (≡) o;
monoid_comm : Comm (≡) o;
monoid_left_id : LeftId (≡) monoid_unit o;
}.
Class PCore (A : Type) := pcore : A → option A.
Class Op (A : Type) := op : A → A → A.
Infix "⋅" := op (at level 50, left associativity) : stdpp_scope.
Notation "(⋅)" := op (only parsing) : stdpp_scope.
Definition included {A} `{!Equiv A, !Op A} (x y : A) := ∃ z, y ≡ x ⋅ z.
Infix "≼" := included (at level 70) : stdpp_scope.
Class ValidN (A : Type) := validN : nat → A → Prop.
Notation "✓{ n } x" := (validN n x)
(at level 20, n at next level, format "✓{ n } x").
Class Valid (A : Type) := valid : A → Prop.
Notation "✓ x" := (valid x) (at level 20) : stdpp_scope.
Definition includedN `{!Dist A, !Op A} (n : nat) (x y : A) := ∃ z, y ≡{n}≡ x ⋅ z.
Notation "x ≼{ n } y" := (includedN n x y)
(at level 70, n at next level, format "x ≼{ n } y") : stdpp_scope.
Section mixin.
Record CmraMixin A `{!Dist A, !Equiv A, !PCore A, !Op A, !Valid A, !ValidN A} := {
mixin_cmra_op_ne (x : A) : NonExpansive (op x);
mixin_cmra_pcore_ne n (x y : A) cx :
x ≡{n}≡ y → pcore x = Some cx → ∃ cy, pcore y = Some cy ∧ cx ≡{n}≡ cy;
mixin_cmra_validN_ne n : Proper (dist (A := A) n ==> impl) (validN n);
mixin_cmra_valid_validN (x : A) : ✓ x ↔ ∀ n, ✓{n} x;
mixin_cmra_validN_S n (x : A) : ✓{S n} x → ✓{n} x;
mixin_cmra_assoc : Assoc (≡@{A}) (⋅);
mixin_cmra_comm : Comm (≡@{A}) (⋅);
mixin_cmra_pcore_l (x : A) cx : pcore x = Some cx → cx ⋅ x ≡ x;
mixin_cmra_pcore_idemp (x : A) cx : pcore x = Some cx → pcore cx ≡ Some cx;
mixin_cmra_pcore_mono (x y : A) cx :
x ≼ y → pcore x = Some cx → ∃ cy, pcore y = Some cy ∧ cx ≼ cy;
mixin_cmra_validN_op_l n (x y : A) : ✓{n} (x ⋅ y) → ✓{n} x;
mixin_cmra_extend n (x y1 y2 : A) :
✓{n} x → x ≡{n}≡ y1 ⋅ y2 →
{ z1 : A & { z2 | x ≡ z1 ⋅ z2 ∧ z1 ≡{n}≡ y1 ∧ z2 ≡{n}≡ y2 } }
}.
End mixin.
#[projections(primitive=no)]
Structure cmra := Cmra' {
cmra_car :> Type;
cmra_equiv : Equiv cmra_car;
cmra_dist : Dist cmra_car;
cmra_pcore : PCore cmra_car;
cmra_op : Op cmra_car;
cmra_valid : Valid cmra_car;
cmra_validN : ValidN cmra_car;
cmra_ofe_mixin : OfeMixin cmra_car;
cmra_mixin : CmraMixin cmra_car;
}.
Global Arguments Cmra' _ {_ _ _ _ _ _} _ _.
Notation Cmra A m := (Cmra' A (ofe_mixin_of A%type) m) (only parsing).
Global Hint Extern 0 (PCore _) => refine (cmra_pcore _); shelve : typeclass_instances.
Global Hint Extern 0 (Op _) => refine (cmra_op _); shelve : typeclass_instances.
Global Hint Extern 0 (Valid _) => refine (cmra_valid _); shelve : typeclass_instances.
Global Hint Extern 0 (ValidN _) => refine (cmra_validN _); shelve : typeclass_instances.
Coercion cmra_ofeO (A : cmra) : ofe.
exact (Ofe A (cmra_ofe_mixin A)).
Defined.
Canonical Structure cmra_ofeO.
Definition cmra_mixin_of' A {Ac : cmra} (f : Ac → A) : CmraMixin Ac.
Admitted.
Notation cmra_mixin_of A :=
ltac:(let H := eval hnf in (cmra_mixin_of' A id) in exact H) (only parsing).
Class Unit (A : Type) := ε : A.
Record UcmraMixin A `{!Dist A, !Equiv A, !PCore A, !Op A, !Valid A, !Unit A} := {
mixin_ucmra_unit_valid : ✓ (ε : A);
mixin_ucmra_unit_left_id : LeftId (≡@{A}) ε (⋅);
mixin_ucmra_pcore_unit : pcore ε ≡@{option A} Some ε
}.
#[projections(primitive=no)]
Structure ucmra := Ucmra' {
ucmra_car :> Type;
ucmra_equiv : Equiv ucmra_car;
ucmra_dist : Dist ucmra_car;
ucmra_pcore : PCore ucmra_car;
ucmra_op : Op ucmra_car;
ucmra_valid : Valid ucmra_car;
ucmra_validN : ValidN ucmra_car;
ucmra_unit : Unit ucmra_car;
ucmra_ofe_mixin : OfeMixin ucmra_car;
ucmra_cmra_mixin : CmraMixin ucmra_car;
ucmra_mixin : UcmraMixin ucmra_car;
}.
Global Arguments Ucmra' _ {_ _ _ _ _ _ _} _ _ _.
Notation Ucmra A m :=
(Ucmra' A (ofe_mixin_of A%type) (cmra_mixin_of A%type) m) (only parsing).
Global Hint Extern 0 (Unit _) => refine (ucmra_unit _); shelve : typeclass_instances.
Coercion ucmra_ofeO (A : ucmra) : ofe.
exact (Ofe A (ucmra_ofe_mixin A)).
Defined.
Canonical Structure ucmra_ofeO.
Coercion ucmra_cmraR (A : ucmra) : cmra.
exact (Cmra' A (ucmra_ofe_mixin A) (ucmra_cmra_mixin A)).
Defined.
Canonical Structure ucmra_cmraR.
Section ucmra.
Context {A : ucmra}.
Global Instance cmra_monoid : Monoid (@op A _).
Admitted.
End ucmra.
Inductive dfrac :=
| DfracOwn : Qp → dfrac
| DfracDiscarded : dfrac
| DfracBoth : Qp → dfrac.
Record agree (A : Type) : Type := {
agree_car : list A;
agree_not_nil : bool_decide (agree_car = []) = false
}.
Fixpoint big_opL {M : ofe} {o : M → M → M} `{!Monoid o} {A} (f : nat → A → M) (xs : list A) : M :=
match xs with
| [] => monoid_unit
| x :: xs => o (f 0 x) (big_opL (λ n, f (S n)) xs)
end.
Global Arguments big_opL {M} o {_ A} _ !_ /.
Notation "'[^' o 'list]' k ↦ x ∈ l , P" := (big_opL o (λ k x, P) l)
(at level 200, o at level 1, l at level 10, k, x at level 1, right associativity,
format "[^ o list] k ↦ x ∈ l , P") : stdpp_scope.
Structure view_rel (A : ofe) (B : ucmra) := ViewRel {
view_rel_holds :> nat → A → B → Prop;
view_rel_mono n1 n2 a1 a2 b1 b2 :
view_rel_holds n1 a1 b1 →
a1 ≡{n2}≡ a2 →
b2 ≼{n2} b1 →
n2 ≤ n1 →
view_rel_holds n2 a2 b2;
view_rel_validN n a b :
view_rel_holds n a b → ✓{n} b;
view_rel_unit n :
∃ a, view_rel_holds n a ε
}.
Record view {A B} (rel : nat → A → B → Prop) :=
View { view_auth_proj : option (dfrac * agree A) ; view_frag_proj : B }.
Definition view_frag {A B} {rel : view_rel A B} (b : B) : view rel.
Admitted.
Notation "◯V a" := (view_frag a) (at level 20).
Section ofe.
Context {A B : ofe} (rel : nat → A → B → Prop).
Local Instance view_equiv : Equiv (view rel).
Admitted.
Local Instance view_dist : Dist (view rel).
Admitted.
Definition view_ofe_mixin : OfeMixin (view rel).
Admitted.
Canonical Structure viewO := Ofe (view rel) view_ofe_mixin.
End ofe.
Section cmra.
Context {A B} (rel : view_rel A B).
Implicit Types x y : view rel.
Local Instance view_valid_instance : Valid (view rel).
Admitted.
Local Instance view_validN_instance : ValidN (view rel).
Admitted.
Local Instance view_pcore_instance : PCore (view rel).
Admitted.
Local Instance view_op_instance : Op (view rel).
Admitted.
Lemma view_cmra_mixin : CmraMixin (view rel).
Admitted.
Canonical Structure viewR := Cmra (view rel) view_cmra_mixin.
Local Instance view_empty_instance : Unit (view rel).
Admitted.
Lemma view_ucmra_mixin : UcmraMixin (view rel).
Admitted.
Canonical Structure viewUR := Ucmra (view rel) view_ucmra_mixin.
Lemma big_opL_view_frag {C} (g : nat → C → B) (l : list C) :
(◯V [^op list] k↦x ∈ l, g k x) ≡ [^op list] k↦x ∈ l, ◯V (g k x).
Admitted.🛠️ Intermediate Coq File (useful for debugging if minimization did not go as far as you wanted)🛠️ 📜 Intermediate Coq File log (useful for debugging if minimization did not go as far as you wanted)📜 Build Log (contains the Coq error message) (truncated to last 8.0KiB; full 3.9MiB file on GitHub Actions Artifacts under
|
Minimization interrupted by timeout, being automatically continued. Partially Minimized File /home/runner/work/run-coq-bug-minimizer/run-coq-bug-minimizer/builds/coq/coq-failing/_build_ci/metacoq/safechecker/theories/PCUICSafeChecker.v (from ci-metacoq) (interrupted by timeout, being automatically continued) (full log on GitHub Actions - verbose log)⭐ ⏱️ Partially Minimized Coq File (timeout)(* -*- mode: coq; coq-prog-args: ("-emacs" "-q" "-w" "-deprecated-native-compiler-option" "-native-compiler" "no" "-R" "/github/workspace/builds/coq/coq-failing/_build_ci/metacoq/utils/theories" "MetaCoq.Utils" "-R" "/github/workspace/builds/coq/coq-failing/_build_ci/metacoq/common/theories" "MetaCoq.Common" "-R" "/github/workspace/builds/coq/coq-failing/_build_ci/metacoq/pcuic/theories" "MetaCoq.PCUIC" "-R" "/github/workspace/builds/coq/coq-failing/_build_ci/metacoq/safechecker/theories" "MetaCoq.SafeChecker" "-Q" "/github/workspace/cwd" "Top" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq/user-contrib/Equations" "Equations" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq/user-contrib/Ltac2" "Ltac2" "-top" "MetaCoq.SafeChecker.PCUICSafeChecker") -*- *)
(* File reduced by coq-bug-minimizer from original input, then from 2560 lines to 33 lines, then from 46 lines to 622 lines, then from 625 lines to 113 lines, then from 126 lines to 1493 lines, then from 1494 lines to 115 lines, then from 128 lines to 821 lines, then from 825 lines to 280 lines, then from 293 lines to 710 lines, then from 715 lines to 282 lines, then from 295 lines to 1746 lines, then from 1751 lines to 545 lines, then from 558 lines to 1457 lines, then from 1461 lines to 711 lines, then from 724 lines to 2544 lines, then from 2543 lines to 722 lines *)
(* coqc version 8.20+alpha compiled with OCaml 4.09.0
coqtop version runner-t7b1znuaq-project-4504-concurrent-4:/builds/coq/coq/_build/default,(HEAD detached at e220577dc5a4) (e220577dc5a4cfa9bbac925c2e3fb42236b36b54)
Expected coqc runtime on this file: 2.158 sec *)
Require MetaCoq.PCUIC.PCUICEquality.
Import Coq.ssr.ssrbool.
Import MetaCoq.Utils.utils.
Import MetaCoq.PCUIC.PCUICAst.
Definition shiftnP k p i :=
(i <? k) || p (i - k).
Fixpoint on_free_vars (p : nat -> bool) (t : term) : bool.
Admitted.
Definition on_free_vars_decl P d :=
test_decl (on_free_vars P) d.
Definition on_free_vars_ctx P ctx :=
alli (fun k => (on_free_vars_decl (shiftnP k P))) 0 (List.rev ctx).
Notation is_open_term Γ := (on_free_vars (shiftnP #|Γ| xpred0)).
Notation is_closed_context := (on_free_vars_ctx xpred0).
Module Export PCUICCumulativitySpec.
Import MetaCoq.Common.config.
Import MetaCoq.PCUIC.PCUICEquality.
Import MetaCoq.PCUIC.Syntax.PCUICCases.
Implicit Types (cf : checker_flags).
Definition cumul_predicate (cumul : context -> term -> term -> Type) cumul_universe Γ p p' :=
All2 (cumul Γ) p.(pparams) p'.(pparams) ×
cmp_universe_instance cumul_universe p.(puinst) p'.(puinst) ×
eq_context_upto_names p.(pcontext) p'.(pcontext) ×
cumul (Γ ,,, inst_case_predicate_context p) p.(preturn) p'.(preturn).
Definition cumul_branch (cumul_term : context -> term -> term -> Type) Γ p br br' :=
eq_context_upto_names br.(bcontext) br'.(bcontext) ×
cumul_term (Γ ,,, inst_case_branch_context p br) br.(bbody) br'.(bbody).
Definition cumul_branches cumul_term Γ p brs brs' := All2 (cumul_branch cumul_term Γ p) brs brs'.
Definition cumul_mfixpoint (cumul_term : context -> term -> term -> Type) Γ mfix mfix' :=
All2 (fun d d' =>
cumul_term Γ d.(dtype) d'.(dtype) ×
cumul_term (Γ ,,, fix_context mfix) d.(dbody) d'.(dbody) ×
d.(rarg) = d'.(rarg) ×
eq_binder_annot d.(dname) d'.(dname)
) mfix mfix'.
Reserved Notation " Σ ;;; Γ ⊢ t ≤s[ pb ] u" (at level 50, Γ, t, u at next level,
format "Σ ;;; Γ ⊢ t ≤s[ pb ] u").
Definition cumul_Ind_univ {cf} (Σ : global_env_ext) pb i napp :=
cmp_global_instance Σ (compare_universe Σ) pb (IndRef i) napp.
Definition cumul_Construct_univ {cf} (Σ : global_env_ext) pb i k napp :=
cmp_global_instance Σ (compare_universe Σ) pb (ConstructRef i k) napp.
Inductive cumulSpec0 {cf : checker_flags} (Σ : global_env_ext) Γ (pb : conv_pb) : term -> term -> Type :=
| cumul_Trans : forall t u v,
is_closed_context Γ -> is_open_term Γ u ->
Σ ;;; Γ ⊢ t ≤s[pb] u ->
Σ ;;; Γ ⊢ u ≤s[pb] v ->
Σ ;;; Γ ⊢ t ≤s[pb] v
| cumul_Sym : forall t u,
Σ ;;; Γ ⊢ t ≤s[Conv] u ->
Σ ;;; Γ ⊢ u ≤s[pb] t
| cumul_Refl : forall t,
Σ ;;; Γ ⊢ t ≤s[pb] t
| cumul_Ind : forall i u u' args args',
cumul_Ind_univ Σ pb i #|args| u u' ->
All2 (fun t u => Σ ;;; Γ ⊢ t ≤s[Conv] u) args args' ->
Σ ;;; Γ ⊢ mkApps (tInd i u) args ≤s[pb] mkApps (tInd i u') args'
| cumul_Construct : forall i k u u' args args',
cumul_Construct_univ Σ pb i k #|args| u u' ->
All2 (fun t u => Σ ;;; Γ ⊢ t ≤s[Conv] u) args args' ->
Σ ;;; Γ ⊢ mkApps (tConstruct i k u) args ≤s[pb] mkApps (tConstruct i k u') args'
| cumul_Sort : forall s s',
compare_sort Σ pb s s' ->
Σ ;;; Γ ⊢ tSort s ≤s[pb] tSort s'
| cumul_Const : forall c u u',
cmp_universe_instance (compare_universe Σ Conv) u u' ->
Σ ;;; Γ ⊢ tConst c u ≤s[pb] tConst c u'
| cumul_Evar : forall e args args',
All2 (fun t u => Σ ;;; Γ ⊢ t ≤s[Conv] u) args args' ->
Σ ;;; Γ ⊢ tEvar e args ≤s[pb] tEvar e args'
| cumul_App : forall t t' u u',
Σ ;;; Γ ⊢ t ≤s[pb] t' ->
Σ ;;; Γ ⊢ u ≤s[Conv] u' ->
Σ ;;; Γ ⊢ tApp t u ≤s[pb] tApp t' u'
| cumul_Lambda : forall na na' ty ty' t t',
eq_binder_annot na na' ->
Σ ;;; Γ ⊢ ty ≤s[Conv] ty' ->
Σ ;;; Γ ,, vass na ty ⊢ t ≤s[pb] t' ->
Σ ;;; Γ ⊢ tLambda na ty t ≤s[pb] tLambda na' ty' t'
| cumul_Prod : forall na na' a a' b b',
eq_binder_annot na na' ->
Σ ;;; Γ ⊢ a ≤s[Conv] a' ->
Σ ;;; Γ ,, vass na a ⊢ b ≤s[pb] b' ->
Σ ;;; Γ ⊢ tProd na a b ≤s[pb] tProd na' a' b'
| cumul_LetIn : forall na na' t t' ty ty' u u',
eq_binder_annot na na' ->
Σ ;;; Γ ⊢ t ≤s[Conv] t' ->
Σ ;;; Γ ⊢ ty ≤s[Conv] ty' ->
Σ ;;; Γ ,, vdef na t ty ⊢ u ≤s[pb] u' ->
Σ ;;; Γ ⊢ tLetIn na t ty u ≤s[pb] tLetIn na' t' ty' u'
| cumul_Case indn : forall p p' c c' brs brs',
cumul_predicate (fun Γ t u => Σ ;;; Γ ⊢ t ≤s[Conv] u) (compare_universe Σ Conv) Γ p p' ->
Σ ;;; Γ ⊢ c ≤s[Conv] c' ->
cumul_branches (fun Γ t u => Σ ;;; Γ ⊢ t ≤s[Conv] u) Γ p brs brs' ->
Σ ;;; Γ ⊢ tCase indn p c brs ≤s[pb] tCase indn p' c' brs'
| cumul_Proj : forall p c c',
Σ ;;; Γ ⊢ c ≤s[Conv] c' ->
Σ ;;; Γ ⊢ tProj p c ≤s[pb] tProj p c'
| cumul_Fix : forall mfix mfix' idx,
cumul_mfixpoint (fun Γ t u => Σ ;;; Γ ⊢ t ≤s[Conv] u) Γ mfix mfix' ->
Σ ;;; Γ ⊢ tFix mfix idx ≤s[pb] tFix mfix' idx
| cumul_CoFix : forall mfix mfix' idx,
cumul_mfixpoint (fun Γ t u => Σ ;;; Γ ⊢ t ≤s[Conv] u) Γ mfix mfix' ->
Σ ;;; Γ ⊢ tCoFix mfix idx ≤s[pb] tCoFix mfix' idx
| cumul_Prim p p' :
onPrims (fun x y => Σ ;;; Γ ⊢ x ≤s[Conv] y) (compare_universe Σ Conv) p p' ->
Σ ;;; Γ ⊢ tPrim p ≤s[pb] tPrim p'
| cumul_beta : forall na t b a,
Σ ;;; Γ ⊢ tApp (tLambda na t b) a ≤s[pb] b {0 := a}
| cumul_zeta : forall na b t b',
Σ ;;; Γ ⊢ tLetIn na b t b' ≤s[pb] b' {0 := b}
| cumul_rel i body :
option_map decl_body (nth_error Γ i) = Some (Some body) ->
Σ ;;; Γ ⊢ tRel i ≤s[pb] lift0 (S i) body
| cumul_iota : forall ci c u args p brs br,
nth_error brs c = Some br ->
#|args| = (ci.(ci_npar) + context_assumptions br.(bcontext))%nat ->
Σ ;;; Γ ⊢ tCase ci p (mkApps (tConstruct ci.(ci_ind) c u) args) brs ≤s[pb] iota_red ci.(ci_npar) p args br
| cumul_fix : forall mfix idx args narg fn,
unfold_fix mfix idx = Some (narg, fn) ->
is_constructor narg args = true ->
Σ ;;; Γ ⊢ mkApps (tFix mfix idx) args ≤s[pb] mkApps fn args
| cumul_cofix_case : forall ip p mfix idx args narg fn brs,
unfold_cofix mfix idx = Some (narg, fn) ->
Σ ;;; Γ ⊢ tCase ip p (mkApps (tCoFix mfix idx) args) brs ≤s[pb] tCase ip p (mkApps fn args) brs
| cumul_cofix_proj : forall p mfix idx args narg fn,
unfold_cofix mfix idx = Some (narg, fn) ->
Σ ;;; Γ ⊢ tProj p (mkApps (tCoFix mfix idx) args) ≤s[pb] tProj p (mkApps fn args)
| cumul_delta : forall c decl body (isdecl : declared_constant Σ c decl) u,
decl.(cst_body) = Some body ->
Σ ;;; Γ ⊢ tConst c u ≤s[pb] body@[u]
| cumul_proj : forall p args u arg,
nth_error args (p.(proj_npars) + p.(proj_arg)) = Some arg ->
Σ ;;; Γ ⊢ tProj p (mkApps (tConstruct p.(proj_ind) 0 u) args) ≤s[pb] arg
where " Σ ;;; Γ ⊢ t ≤s[ pb ] u " := (@cumulSpec0 _ Σ Γ pb t u) : type_scope.
Definition cumulSpec `{checker_flags} (Σ : global_env_ext) Γ := cumulSpec0 Σ Γ Cumul.
Notation " Σ ;;; Γ |- t <=s u " := (@cumulSpec _ Σ Γ t u) (at level 50, Γ, t, u at next level).
Module PCUICConversionParSpec <: EnvironmentTyping.ConversionParSig PCUICTerm PCUICEnvironment PCUICTermUtils PCUICEnvTyping.
Definition cumul_gen := @cumulSpec0.
End PCUICConversionParSpec.
End PCUICCumulativitySpec.
Import MetaCoq.Common.config.
Import MetaCoq.PCUIC.utils.PCUICAstUtils.
Import MetaCoq.PCUIC.utils.PCUICPrimitive.
Import MetaCoq.PCUIC.PCUICEquality.
Export MetaCoq.PCUIC.Syntax.PCUICCases.
Implicit Types (cf : checker_flags) (Σ : global_env_ext).
Definition type_of_constructor mdecl (cdecl : constructor_body) (c : inductive * nat) (u : list Level.t) :=
let mind := inductive_mind (fst c) in
subst0 (inds mind u mdecl.(ind_bodies)) (subst_instance u (cstr_type cdecl)).
Include PCUICEnvTyping.
Inductive FixCoFix : Type := Fix | CoFix.
Class GuardChecker :=
{
guard : FixCoFix -> global_env_ext -> context -> mfixpoint term -> Prop ;
}.
Axiom guard_checking : GuardChecker.
#[global]
Existing Instance guard_checking.
Definition fix_guard := guard Fix.
Definition cofix_guard := guard CoFix.
Definition destInd (t : term) :=
match t with
| tInd ind u => Some (ind, u)
| _ => None
end.
Definition isCoFinite (r : recursivity_kind) :=
match r with
| CoFinite => true
| _ => false
end.
Definition check_recursivity_kind
(lookup: kername -> option global_decl) ind r :=
match lookup ind with
| Some (InductiveDecl mib) => ReflectEq.eqb mib.(ind_finite) r
| _ => false
end.
Definition check_one_fix d :=
let '{| dname := na;
dtype := ty;
dbody := b;
rarg := arg |} := d in
let '(ctx, ty) := decompose_prod_assum [] ty in
match nth_error (List.rev (smash_context [] ctx)) arg with
| Some argd =>
let (hd, args) := decompose_app argd.(decl_type) in
match destInd hd with
| Some (mkInd mind _, u) => Some mind
| None => None
end
| None => None
end.
Definition wf_fixpoint_gen
(lookup: kername -> option global_decl) mfix :=
forallb (isLambda ∘ dbody) mfix &&
let checks := map check_one_fix mfix in
match map_option_out checks with
| Some (ind :: inds) =>
forallb (eqb ind) inds &&
check_recursivity_kind lookup ind Finite
| _ => false
end.
Definition wf_fixpoint (Σ : global_env) := wf_fixpoint_gen (lookup_env Σ).
Definition check_one_cofix d :=
let '{| dname := na;
dtype := ty;
dbody := b;
rarg := arg |} := d in
let '(ctx, ty) := decompose_prod_assum [] ty in
let (hd, args) := decompose_app ty in
match destInd hd with
| Some (mkInd ind _, u) => Some ind
| None => None
end.
Definition wf_cofixpoint_gen
(lookup: kername -> option global_decl) mfix :=
let checks := map check_one_cofix mfix in
match map_option_out checks with
| Some (ind :: inds) =>
forallb (eqb ind) inds &&
check_recursivity_kind lookup ind CoFinite
| _ => false
end.
Definition wf_cofixpoint (Σ : global_env) := wf_cofixpoint_gen (lookup_env Σ).
Reserved Notation "'wf_local' Σ Γ " (at level 9, Σ, Γ at next level).
Reserved Notation " Σ ;;; Γ |- t : T " (at level 50, Γ, t, T at next level).
Variant case_side_conditions `{checker_flags} wf_local_fun typing Σ Γ ci p ps mdecl idecl indices predctx :=
| case_side_info
(eq_npars : mdecl.(ind_npars) = ci.(ci_npar))
(wf_pred : wf_predicate mdecl idecl p)
(cons : consistent_instance_ext Σ (ind_universes mdecl) p.(puinst))
(wf_pctx : wf_local_fun Σ (Γ ,,, predctx))
(conv_pctx : eq_context_upto_names p.(pcontext) (ind_predicate_context ci.(ci_ind) mdecl idecl))
(allowed_elim : is_allowed_elimination Σ idecl.(ind_kelim) ps)
(ind_inst : ctx_inst (typing Σ) Γ (p.(pparams) ++ indices)
(List.rev (subst_instance p.(puinst)
(ind_params mdecl ,,, ind_indices idecl : context))))
(not_cofinite : isCoFinite mdecl.(ind_finite) = false).
Variant case_branch_typing `{checker_flags} wf_local_fun typing Σ Γ (ci:case_info) p ps mdecl idecl ptm brs :=
| case_branch_info
(wf_brs : wf_branches idecl brs)
(brs_ty :
All2i (fun i cdecl br =>
eq_context_upto_names br.(bcontext) (cstr_branch_context ci mdecl cdecl) ×
let brctxty := case_branch_type ci.(ci_ind) mdecl idecl p br ptm i cdecl in
(wf_local_fun Σ (Γ ,,, brctxty.1) ×
((typing Σ (Γ ,,, brctxty.1) br.(bbody) (brctxty.2)) ×
(typing Σ (Γ ,,, brctxty.1) brctxty.2 (tSort ps)))))
0 idecl.(ind_ctors) brs).
Variant primitive_typing_hyps `{checker_flags}
(typing : forall (Σ : global_env_ext) (Γ : context), term -> term -> Type)
Σ Γ : prim_val term -> Type :=
| prim_int_hyps i : primitive_typing_hyps typing Σ Γ (primInt; primIntModel i)
| prim_float_hyps f : primitive_typing_hyps typing Σ Γ (primFloat; primFloatModel f)
| prim_array_hyps a
(wfl : wf_universe Σ (Universe.make' a.(array_level)))
(hty : typing Σ Γ a.(array_type) (tSort (sType (Universe.make' a.(array_level)))))
(hdef : typing Σ Γ a.(array_default) a.(array_type))
(hvalue : All (fun x => typing Σ Γ x a.(array_type)) a.(array_value)) :
primitive_typing_hyps typing Σ Γ (primArray; primArrayModel a).
Equations prim_type (p : prim_val term) (cst : kername) : term :=
prim_type (primInt; _) cst := tConst cst [];
prim_type (primFloat; _) cst := tConst cst [];
prim_type (primArray; primArrayModel a) cst := tApp (tConst cst [a.(array_level)]) a.(array_type).
Inductive typing `{checker_flags} (Σ : global_env_ext) (Γ : context) : term -> term -> Type :=
| type_Rel : forall n decl,
wf_local Σ Γ ->
nth_error Γ n = Some decl ->
Σ ;;; Γ |- tRel n : lift0 (S n) decl.(decl_type)
| type_Sort : forall s,
wf_local Σ Γ ->
wf_sort Σ s ->
Σ ;;; Γ |- tSort s : tSort (Sort.super s)
| type_Prod : forall na A B s1 s2,
lift_typing typing Σ Γ (j_vass_s na A s1) ->
Σ ;;; Γ ,, vass na A |- B : tSort s2 ->
Σ ;;; Γ |- tProd na A B : tSort (Sort.sort_of_product s1 s2)
| type_Lambda : forall na A t B,
lift_typing typing Σ Γ (j_vass na A) ->
Σ ;;; Γ ,, vass na A |- t : B ->
Σ ;;; Γ |- tLambda na A t : tProd na A B
| type_LetIn : forall na b B t A,
lift_typing typing Σ Γ (j_vdef na b B) ->
Σ ;;; Γ ,, vdef na b B |- t : A ->
Σ ;;; Γ |- tLetIn na b B t : tLetIn na b B A
| type_App : forall t na A B s u,
Σ ;;; Γ |- tProd na A B : tSort s ->
Σ ;;; Γ |- t : tProd na A B ->
Σ ;;; Γ |- u : A ->
Σ ;;; Γ |- tApp t u : B{0 := u}
| type_Const : forall cst u decl,
wf_local Σ Γ ->
declared_constant Σ cst decl ->
consistent_instance_ext Σ decl.(cst_universes) u ->
Σ ;;; Γ |- tConst cst u : decl.(cst_type)@[u]
| type_Ind : forall ind u mdecl idecl,
wf_local Σ Γ ->
declared_inductive Σ ind mdecl idecl ->
consistent_instance_ext Σ mdecl.(ind_universes) u ->
Σ ;;; Γ |- tInd ind u : idecl.(ind_type)@[u]
| type_Construct : forall ind i u mdecl idecl cdecl,
wf_local Σ Γ ->
declared_constructor Σ (ind, i) mdecl idecl cdecl ->
consistent_instance_ext Σ mdecl.(ind_universes) u ->
Σ ;;; Γ |- tConstruct ind i u : type_of_constructor mdecl cdecl (ind, i) u
| type_Case : forall ci p c brs indices ps mdecl idecl,
let predctx := case_predicate_context ci.(ci_ind) mdecl idecl p in
let ptm := it_mkLambda_or_LetIn predctx p.(preturn) in
declared_inductive Σ ci.(ci_ind) mdecl idecl ->
Σ ;;; Γ ,,, predctx |- p.(preturn) : tSort ps ->
Σ ;;; Γ |- c : mkApps (tInd ci.(ci_ind) p.(puinst)) (p.(pparams) ++ indices) ->
case_side_conditions (fun Σ Γ => wf_local Σ Γ) typing Σ Γ ci p ps
mdecl idecl indices predctx ->
case_branch_typing (fun Σ Γ => wf_local Σ Γ) typing Σ Γ ci p ps
mdecl idecl ptm brs ->
Σ ;;; Γ |- tCase ci p c brs : mkApps ptm (indices ++ [c])
| type_Proj : forall p c u mdecl idecl cdecl pdecl args,
declared_projection Σ p mdecl idecl cdecl pdecl ->
Σ ;;; Γ |- c : mkApps (tInd p.(proj_ind) u) args ->
#|args| = ind_npars mdecl ->
Σ ;;; Γ |- tProj p c : subst0 (c :: List.rev args) pdecl.(proj_type)@[u]
| type_Fix : forall mfix n decl,
wf_local Σ Γ ->
fix_guard Σ Γ mfix ->
nth_error mfix n = Some decl ->
All (on_def_type (lift_typing1 (typing Σ)) Γ) mfix ->
All (on_def_body (lift_typing1 (typing Σ)) (fix_context mfix) Γ) mfix ->
wf_fixpoint Σ mfix ->
Σ ;;; Γ |- tFix mfix n : decl.(dtype)
| type_CoFix : forall mfix n decl,
wf_local Σ Γ ->
cofix_guard Σ Γ mfix ->
nth_error mfix n = Some decl ->
All (on_def_type (lift_typing1 (typing Σ)) Γ) mfix ->
All (on_def_body (lift_typing1 (typing Σ)) (fix_context mfix) Γ) mfix ->
wf_cofixpoint Σ mfix ->
Σ ;;; Γ |- tCoFix mfix n : decl.(dtype)
| type_Prim p prim_ty cdecl :
wf_local Σ Γ ->
primitive_constant Σ (prim_val_tag p) = Some prim_ty ->
declared_constant Σ prim_ty cdecl ->
primitive_invariants (prim_val_tag p) cdecl ->
primitive_typing_hyps typing Σ Γ p ->
Σ ;;; Γ |- tPrim p : prim_type p prim_ty
| type_Cumul : forall t A B s,
Σ ;;; Γ |- t : A ->
Σ ;;; Γ |- B : tSort s ->
Σ ;;; Γ |- A <=s B ->
Σ ;;; Γ |- t : B
where " Σ ;;; Γ |- t : T " := (typing Σ Γ t T)
and "'wf_local' Σ Γ " := (All_local_env (lift_typing1 (typing Σ)) Γ).
Module PCUICTypingDef <: EnvironmentTyping.Typing PCUICTerm PCUICEnvironment PCUICTermUtils PCUICEnvTyping PCUICConversion PCUICConversionParSpec.
Definition typing := @typing.
End PCUICTypingDef.
Definition wf `{checker_flags} := on_global_env cumulSpec0 (lift_typing typing).
Definition wf_ext `{checker_flags} := on_global_env_ext cumulSpec0 (lift_typing typing).
Record normalizing_flags {cf : checker_flags} : Prop :=
{ nor_check_univs :> check_univs }.
Import MetaCoq.PCUIC.PCUICAst.
Inductive ConversionError :=
| NotFoundConstants (c1 c2 : kername)
| NotFoundConstant (c : kername)
| LambdaNotConvertibleTypes
(Γ1 : context) (na : aname) (A1 t1 : term)
(Γ2 : context) (na' : aname) (A2 t2 : term)
(e : ConversionError)
| LambdaNotConvertibleAnn
(Γ1 : context) (na : aname) (A1 t1 : term)
(Γ2 : context) (na' : aname) (A2 t2 : term)
| ProdNotConvertibleDomains
(Γ1 : context) (na : aname) (A1 B1 : term)
(Γ2 : context) (na' : aname) (A2 B2 : term)
(e : ConversionError)
| ProdNotConvertibleAnn
(Γ1 : context) (na : aname) (A1 B1 : term)
(Γ2 : context) (na' : aname) (A2 B2 : term)
| ContextNotConvertibleAnn
(Γ : context) (decl : context_decl)
(Γ' : context) (decl' : context_decl)
| ContextNotConvertibleType
(Γ : context) (decl : context_decl)
(Γ' : context) (decl' : context_decl)
| ContextNotConvertibleBody
(Γ : context) (decl : context_decl)
(Γ' : context) (decl' : context_decl)
| ContextNotConvertibleLength
| CaseOnDifferentInd
(Γ1 : context)
(ci : case_info) (p : predicate term) (c : term) (brs : list (branch term))
(Γ2 : context)
(ci' : case_info) (p' : predicate term) (c' : term) (brs' : list (branch term))
| CasePredParamsUnequalLength
(Γ1 : context)
(ci : case_info) (p : predicate term) (c : term) (brs : list (branch term))
(Γ2 : context)
(ci' : case_info) (p' : predicate term) (c' : term) (brs' : list (branch term))
| CasePredUnequalUniverseInstances
(Γ1 : context)
(ci : case_info) (p : predicate term) (c : term) (brs : list (branch term))
(Γ2 : context)
(ci' : case_info) (p' : predicate term) (c' : term) (brs' : list (branch term))
| DistinctStuckProj
(Γ : context) (p : projection) (c : term)
(Γ' : context) (p' : projection) (c' : term)
| CannotUnfoldFix
(Γ : context) (mfix : mfixpoint term) (idx : nat)
(Γ' : context) (mfix' : mfixpoint term) (idx' : nat)
| FixRargMismatch (idx : nat)
(Γ : context) (u : def term) (mfix1 mfix2 : mfixpoint term)
(Γ' : context) (v : def term) (mfix1' mfix2' : mfixpoint term)
| FixMfixMismatch (idx : nat)
(Γ : context) (mfix : mfixpoint term)
(Γ' : context) (mfix' : mfixpoint term)
| DistinctCoFix
(Γ : context) (mfix : mfixpoint term) (idx : nat)
(Γ' : context) (mfix' : mfixpoint term) (idx' : nat)
| CoFixRargMismatch (idx : nat)
(Γ : context) (u : def term) (mfix1 mfix2 : mfixpoint term)
(Γ' : context) (v : def term) (mfix1' mfix2' : mfixpoint term)
| CoFixMfixMismatch (idx : nat)
(Γ : context) (mfix : mfixpoint term)
(Γ' : context) (mfix' : mfixpoint term)
| DistinctPrimTags
(Γ : context) (p : prim_val)
(Γ' : context) (p' : prim_val)
| DistinctPrimValues
(Γ : context) (p : prim_val)
(Γ' : context) (p' : prim_val)
| ArrayNotConvertibleLevels
(Γ : context) (a : array_model term) (Γ' : context) (a' : array_model term)
| ArrayValuesNotSameLength
(Γ : context) (a : array_model term) (Γ' : context) (a' : array_model term)
| ArrayNotConvertibleValues
(Γ : context) (a : array_model term) (Γ' : context) (a' : array_model term)
(e : ConversionError)
| ArrayNotConvertibleDefault
(Γ : context) (a : array_model term) (Γ' : context) (a' : array_model term)
(e : ConversionError)
| ArrayNotConvertibleTypes
(Γ : context) (a : array_model term) (Γ' : context) (a' : array_model term)
(e : ConversionError)
| StackHeadError
(leq : conv_pb)
(Γ1 : context)
(t1 : term) (args1 : list term) (u1 : term) (l1 : list term)
(Γ2 : context)
(t2 : term) (u2 : term) (l2 : list term)
(e : ConversionError)
| StackTailError (leq : conv_pb)
(Γ1 : context)
(t1 : term) (args1 : list term) (u1 : term) (l1 : list term)
(Γ2 : context)
(t2 : term) (u2 : term) (l2 : list term)
(e : ConversionError)
| StackMismatch
(Γ1 : context) (t1 : term) (args1 l1 : list term)
(Γ2 : context) (t2 : term) (l2 : list term)
| HeadMismatch
(leq : conv_pb)
(Γ1 : context) (t1 : term)
(Γ2 : context) (t2 : term).
Inductive type_error :=
| UnboundRel (n : nat)
| UnboundVar (id : string)
| UnboundEvar (ev : nat)
| UndeclaredConstant (c : kername)
| UndeclaredInductive (c : inductive)
| UndeclaredConstructor (c : inductive) (i : nat)
| NotCumulSmaller {abstract_structure} (le : bool)
(G : abstract_structure) (Γ : context) (t u t' u' : term) (e : ConversionError)
| NotConvertible {abstract_structure}
(G : abstract_structure)
(Γ : context) (t u : term)
| NotASort (t : term)
| NotAProduct (t t' : term)
| NotAnInductive (t : term)
| NotAnArity (t : term)
| IllFormedFix (m : mfixpoint term) (i : nat)
| UnsatisfiedConstraints (c : ConstraintSet.t)
| Msg (s : string).
Inductive env_error :=
| IllFormedDecl (e : string) (e : type_error)
| AlreadyDeclared (id : string).
Section EnvCheck.
Context (abstract_structure : Type).
Inductive EnvCheck (A : Type) :=
| CorrectDecl (a : A)
| EnvError (Σ : abstract_structure) (e : env_error).
Global Instance envcheck_monad : Monad EnvCheck.
Admitted.
End EnvCheck.
Import MetaCoq.Common.uGraph.
Lemma wf_ext_gc_of_uctx {cf:checker_flags} {Σ : global_env_ext} (HΣ : ∥ wf_ext Σ ∥)
: ∑ uctx', gc_of_uctx (global_ext_uctx Σ) = Some uctx'.
Admitted.
Definition on_global_decls {cf:checker_flags} Σ :=
on_global_decls_data cumulSpec0 (lift_typing typing) (cf:=cf) Σ.(universes) Σ.(retroknowledge) Σ.(declarations).
Class abstract_env_struct {cf:checker_flags} (abstract_env_impl abstract_env_ext_impl : Type) := {
abstract_env_rel : abstract_env_impl -> global_env -> Prop;
abstract_env_ext_rel : abstract_env_ext_impl -> global_env_ext -> Prop;
abstract_env_init (cs:ContextSet.t) (retro : Retroknowledge.t) : on_global_univs cs -> abstract_env_impl;
abstract_env_add_decl X (kn:kername) (d:global_decl) :
(forall Σ, abstract_env_rel X Σ -> ∥ on_global_decls Σ kn d ∥)
-> abstract_env_impl;
abstract_env_add_udecl X udecl :
(forall Σ, abstract_env_rel X Σ -> ∥ on_udecl Σ.(universes) udecl ∥) ->
abstract_env_ext_impl ;
abstract_pop_decls : abstract_env_impl -> abstract_env_impl ;
abstract_env_lookup : abstract_env_ext_impl -> kername -> option global_decl;
abstract_primitive_constant : abstract_env_ext_impl -> Primitive.prim_tag -> option kername;
abstract_env_level_mem : abstract_env_ext_impl -> Level.t -> bool;
abstract_env_leqb_level_n : abstract_env_ext_impl -> Z -> Level.t -> Level.t -> bool;
abstract_env_guard : abstract_env_ext_impl -> FixCoFix -> context -> mfixpoint term -> bool;
abstract_env_is_consistent : abstract_env_impl -> LevelSet.t * GoodConstraintSet.t -> bool ;
}.
Class abstract_env_prop {cf:checker_flags} (abstract_env_impl abstract_env_ext_impl: Type)
`{!abstract_env_struct abstract_env_impl abstract_env_ext_impl} : Prop := {
abstract_env_ext_exists X : ∥ ∑ Σ , abstract_env_ext_rel X Σ ∥;
abstract_env_ext_wf X {Σ} : abstract_env_ext_rel X Σ -> ∥ wf_ext Σ ∥ ;
abstract_env_ext_irr X {Σ Σ'} :
abstract_env_ext_rel X Σ -> abstract_env_ext_rel X Σ' -> Σ = Σ';
abstract_env_exists X : ∥ ∑ Σ , abstract_env_rel X Σ ∥;
abstract_env_wf X {Σ} : abstract_env_rel X Σ -> ∥ wf Σ ∥;
abstract_env_irr X {Σ Σ'} :
abstract_env_rel X Σ -> abstract_env_rel X Σ' -> Σ = Σ';
abstract_env_init_correct univs retro cuniv :
abstract_env_rel (abstract_env_init univs retro cuniv)
{| universes := univs; declarations := []; retroknowledge := retro |} ;
abstract_env_add_decl_correct X Σ kn d H : abstract_env_rel X Σ ->
abstract_env_rel (abstract_env_add_decl X kn d H) (add_global_decl Σ (kn,d));
abstract_env_add_udecl_rel X {Σ} udecl H :
(abstract_env_rel X Σ.1 /\ Σ.2 = udecl) <->
abstract_env_ext_rel (abstract_env_add_udecl X udecl H) Σ;
abstract_pop_decls_correct X decls (prf : forall Σ : global_env, abstract_env_rel X Σ ->
exists d, Σ.(declarations) = d :: decls) :
let X' := abstract_pop_decls X in
forall Σ Σ', abstract_env_rel X Σ -> abstract_env_rel X' Σ' ->
Σ'.(declarations) = decls /\ Σ.(universes) = Σ'.(universes) /\
Σ.(retroknowledge) = Σ'.(retroknowledge);
abstract_env_lookup_correct X {Σ} kn decl : abstract_env_ext_rel X Σ ->
In (kn, decl) (declarations Σ) <-> abstract_env_lookup X kn = Some decl ;
abstract_env_leqb_level_n_correct X {Σ} (wfΣ : abstract_env_ext_rel X Σ):
let uctx := (wf_ext_gc_of_uctx (abstract_env_ext_wf X wfΣ)).π1 in
leqb_level_n_spec_gen uctx (abstract_env_leqb_level_n X);
abstract_env_level_mem_correct X {Σ} (wfΣ : abstract_env_ext_rel X Σ) l:
LevelSet.In l (global_ext_levels Σ) <-> abstract_env_level_mem X l;
abstract_env_is_consistent_correct X Σ uctx udecl :
abstract_env_rel X Σ ->
ConstraintSet.For_all (declared_cstr_levels (LevelSet.union udecl.1 (global_levels Σ))) udecl.2 ->
gc_of_uctx udecl = Some uctx ->
consistent_extension_on (global_uctx Σ) udecl.2 <-> abstract_env_is_consistent X uctx ;
abstract_env_guard_correct X {Σ} (wfΣ : abstract_env_ext_rel X Σ) fix_cofix Γ mfix :
guard fix_cofix Σ Γ mfix <-> abstract_env_guard X fix_cofix Γ mfix;
abstract_primitive_constant_correct X tag Σ :
abstract_env_ext_rel X Σ -> abstract_primitive_constant X tag = PCUICEnvironment.primitive_constant Σ tag
}.
Definition abstract_env_impl {cf:checker_flags} := ∑ X Y Z, @abstract_env_prop _ X Y Z.
Import MCMonadNotation.
Section CheckEnv.
Context {cf:checker_flags} {nor : normalizing_flags}.
Context (X_impl : abstract_env_impl).
Definition X_env_type := X_impl.π1.
Implicit Type X : X_env_type.
Context {AA : Type} {BB : AA -> Type} {T : Type -> Type} {M : Monad T} {A} {P : forall (aa:AA), BB aa -> A -> Type} {Q : forall (aa:AA), BB aa -> A -> Type}
(f : forall x, (forall aa bb, ∥ Q aa bb x ∥) -> T (forall aa bb, ∥ P aa bb x ∥)).
Program Fixpoint monad_All_All l :
(forall (aa:AA) (bb: BB aa), ∥ All (Q aa bb) l ∥) ->
T (forall (aa:AA) (bb:BB aa), ∥ All (P aa bb) l ∥) :=
match l return (forall (aa:AA) (bb: BB aa), ∥ All (Q aa bb) l ∥) -> T (forall (aa:AA) (bb:BB aa) , ∥ All (P aa bb) l ∥) with
| [] => fun _ => ret (fun aa bb => sq All_nil)
| a :: l => fun allq =>
X <- f a _ ;;
Y <- monad_All_All l _ ;;
ret (fun aa bb => _)
end.🛠️ Intermediate Coq File (useful for debugging if minimization did not go as far as you wanted)🛠️ 📜 Intermediate Coq File log (useful for debugging if minimization did not go as far as you wanted)📜 Build Log (contains the Coq error message) (truncated to last 8.0KiB; full 4.2MiB file on GitHub Actions Artifacts under
|
Minimization interrupted by timeout, being automatically continued. Partially Minimized File /home/runner/work/run-coq-bug-minimizer/run-coq-bug-minimizer/builds/coq/coq-failing/_build_ci/metacoq/safechecker/theories/PCUICSafeChecker.v (from ci-metacoq) (interrupted by timeout, being automatically continued) (full log on GitHub Actions - verbose log)⭐ ⏱️ Partially Minimized Coq File (timeout) (truncated to first and last 32KiB; full 114KiB file on GitHub Actions Artifacts under
|
Minimization interrupted by timeout, being automatically continued. Partially Minimized File /home/runner/work/run-coq-bug-minimizer/run-coq-bug-minimizer/builds/coq/coq-failing/_build_ci/metacoq/safechecker/theories/PCUICSafeChecker.v (from ci-metacoq) (interrupted by timeout, being automatically continued) (full log on GitHub Actions - verbose log)⭐ ⏱️ Partially Minimized Coq File (timeout) (truncated to first and last 32KiB; full 81KiB file on GitHub Actions Artifacts under
|
SkySkimmer
added
the
request: full CI
SkySkimmer
force-pushed
the
implicit-type-ident-nota
branch
from
e7bb878
to
aa4dcaa
Compare
coqbot-app
bot
removed
the
request: full CI
|
Some of those failures appear to be real bugs but not sure how minimal they are iris appears to rely on implicit types not applying to these notations |
|
Adding |
|
My motivation for this expired. |
pi8027
reviewed
May 13, 2024
Comment on lines
+1
to
+3
| Notation "[ 'fun' x => F ]" := (fun x => F) | ||
| (at level 0, x ident, only parsing). | ||
| (* or `x pattern` *) |
There was a problem hiding this comment.
This example seems a bit obsolete. It seems more appropriate to use name instead of ident now (cf. #11841).
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Fix #9764