rm problematic variables under beta-redexes and evars for evar instantiation #19822
Conversation
This file contains hidden or 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
coqbot-app
bot
added
the
needs: full CI
Contributor
|
@coqbot run full ci |
coqbot-app
bot
removed
the
needs: full CI
SkySkimmer
added
needs: test-suite update
Member
|
@coqbot ci minimize |
Contributor
|
I have initiated minimization at commit f592551 for the suggested targets ci-argosy, ci-elpi_test, ci-fiat_parsers, ci-hott, ci-iris, ci-perennial, ci-rewriter, ci-unimath as requested. |
Contributor
|
Error: Could not minimize file (from ci-elpi_test) (full log on GitHub Actions, cc @JasonGross) build log (truncated to last 26KiB; full 8.0MiB file on GitHub Actions Artifacts under
|
This comment was marked as outdated.
This comment was marked as outdated.
Contributor
|
Minimized File /home/runner/work/run-coq-bug-minimizer/run-coq-bug-minimizer/builds/coq/coq-failing/_build_ci/argosy/src/Examples/ReplicatedDisk/ReplicatedDiskImpl.v (from ci-argosy) (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" "-deprecated-native-compiler-option,-native-compiler-disabled" "-native-compiler" "ondemand" "-R" "/github/workspace/builds/coq/coq-failing/_build_ci/argosy/src" "RecoveryRefinement" "-R" "/github/workspace/builds/coq/coq-failing/_build_ci/argosy/vendor/classes/src" "Classes" "-R" "/github/workspace/builds/coq/coq-failing/_build_ci/argosy/vendor/array/src" "Array" "-R" "/github/workspace/builds/coq/coq-failing/_build_ci/argosy/vendor/tactical/src" "Tactical" "-Q" "/github/workspace/cwd" "Top" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq/user-contrib/Ltac2" "Ltac2" "-top" "RecoveryRefinement.Examples.ReplicatedDisk.ReplicatedDiskImpl") -*- *)
(* File reduced by coq-bug-minimizer from original input, then from 1103 lines to 98 lines, then from 111 lines to 305 lines, then from 310 lines to 129 lines, then from 142 lines to 260 lines, then from 264 lines to 134 lines, then from 147 lines to 207 lines, then from 212 lines to 137 lines, then from 150 lines to 357 lines, then from 362 lines to 156 lines, then from 169 lines to 657 lines, then from 661 lines to 162 lines, then from 175 lines to 665 lines, then from 668 lines to 227 lines, then from 240 lines to 379 lines, then from 384 lines to 271 lines, then from 284 lines to 1243 lines, then from 1247 lines to 302 lines, then from 315 lines to 413 lines, then from 416 lines to 311 lines, then from 324 lines to 862 lines, then from 867 lines to 320 lines, then from 333 lines to 440 lines, then from 445 lines to 322 lines, then from 327 lines to 323 lines *)
(* coqc version 9.0+alpha compiled with OCaml 4.09.0
coqtop version runner-wbcqh1i1-project-4504-concurrent-0:/builds/coq/coq/_build/default,(HEAD detached at c04db99c8cfb) (c04db99c8cfbe3fa002bf604971eb5b0e09656d4)
Expected coqc runtime on this file: 0.122 sec *)
Axiom proof_admitted : False.
Tactic Notation "admit" := abstract case proof_admitted.
Set Implicit Arguments.
Definition maybe_holds T (p:T -> Prop) : option T -> Prop.
Admitted.
Notation "m ?|= F" := (maybe_holds F m) (at level 20, F at level 50).
Section Array.
Context (A:Type).
Notation list := (list A).
Implicit Types (l:list) (n:nat) (x:A).
Fixpoint assign l n x' : list.
Admitted.
Fixpoint index l n : option A.
Admitted.
End Array.
Axiom bytes : nat -> Type.
Definition blockbytes := 1024.
Definition block := bytes blockbytes.
Definition disk := list block.
Definition addr := nat.
Section OutputRelations.
Definition relation A B T := A -> B -> T -> Prop.
Definition and_then {A B C} {T1 T2}
(r1: relation A B T1)
(r2: T1 -> relation B C T2) :
relation A C T2.
Admitted.
Definition pure A T (o0:T) : relation A A T.
Admitted.
Definition rel_or A B T (r1 r2: relation A B T) : relation A B T.
Admitted.
Definition rimpl {A B} {T} (r1 r2: relation A B T) :=
forall x y o, r1 x y o -> r2 x y o.
End OutputRelations.
Delimit Scope relation_scope with rel.
Open Scope relation_scope.
Notation "r1 ---> r2" := (rimpl r1 r2)
(at level 60, no associativity,
format "'[hv' r1 '/' ---> '/' r2 ']'")
: relation_scope.
Infix "+" := rel_or : relation_scope.
Notation "p1 ;; p2" := (and_then p1 (fun _ => p2))
(at level 54, right associativity)
: relation_scope.
Notation "x <- p1 ; p2" := (and_then p1 (fun x => p2))
(at level 54, right associativity,
format "'[' x <- '[v ' p1 ']' ; ']' '/' p2")
: relation_scope.
Global Generalizable Variables T R Op State.
Inductive proc (Op: Type -> Type) (T : Type) : Type :=
| Call (op : Op T)
| Ret (v : T)
| Bind (T1 : Type) (p1 : proc Op T1) (p2 : T1 -> proc Op T).
Arguments Call {Op T}.
Arguments Ret {Op T} v.
Definition OpSemantics Op State := forall T, Op T -> relation State State T.
Definition CrashSemantics State := relation State State unit.
Record Dynamics Op State :=
{ step: OpSemantics Op State;
crash_step: CrashSemantics State; }.
Section Dynamics.
Context `(sem: Dynamics Op State).
Notation proc := (proc Op).
Notation step := sem.(step).
Notation crash_step := sem.(crash_step).
Fixpoint exec {T} (p: proc T) : relation State State T :=
match p with
| Ret v => pure v
| Call op => step op
| Bind p p' => v <- exec p; exec (p' v)
end.
Fixpoint exec_crash {T} (p: proc T) : relation State State unit :=
match p with
| Ret v => crash_step
| Call op => crash_step + (step op;; crash_step)
| Bind p p' =>
exec_crash p +
(v <- exec p;
exec_crash (p' v))
end.
Definition rexec {T R} (p: proc T) (rec: proc R) : relation State State R.
Admitted.
End Dynamics.
Record SpecProps T R State :=
{ pre: Prop;
post: State -> T -> Prop;
alternate: State -> R -> Prop; }.
Definition Specification T R State := State -> SpecProps T R State.
Definition spec_exec T R State (spec: Specification T R State) :
relation State State T.
Admitted.
Definition spec_aexec T R State (spec: Specification T R State) :
relation State State R.
Admitted.
Section Hoare.
Context `(sem: Dynamics Op State).
Notation proc := (proc Op).
Notation exec := (exec sem).
Notation exec_crash := (exec_crash sem).
Notation rexec := (rexec sem).
Definition proc_rspec T R
(p: proc T) (rec: proc R)
(spec: Specification T R State) :=
exec p ---> spec_exec spec /\
rexec p rec ---> spec_aexec spec.
Definition proc_hspec T
(p: proc T)
(spec: Specification T unit State) :=
exec p ---> spec_exec spec /\
exec_crash p ---> spec_aexec spec.
Definition idempotent A T R `(spec: A -> Specification T R State) :=
forall a state,
pre (spec a state) ->
forall v state', alternate (spec a state) state' v ->
exists a', pre (spec a' state') /\
forall rv state'', post (spec a' state') state'' rv ->
post (spec a state) state'' rv.
Theorem proc_hspec_to_rspec A' T R (p_hspec: Specification T unit State)
`(rec_hspec: A' -> Specification R unit State)
`(p_rspec: Specification T R State)
`(p: proc T) `(rec: proc R):
proc_hspec p p_hspec ->
(forall a, proc_hspec rec (rec_hspec a)) ->
idempotent rec_hspec ->
(forall s, (p_rspec s).(pre) -> (p_hspec s).(pre) /\
(forall s' v, (p_hspec s).(post) s' v ->
(p_rspec s).(post) s' v)) ->
(forall state state' v,
pre (p_hspec state) ->
alternate (p_hspec state) state' v ->
exists a, pre (rec_hspec a state')) ->
(forall a s sc, (p_rspec s).(pre) ->
(forall sfin rv, (rec_hspec a sc).(post) sfin rv ->
(p_rspec s).(alternate) sfin rv)) ->
proc_rspec p rec p_rspec.
Admitted.
End Hoare.
Module Export Layer.
Record Layer Op :=
{ State: Type;
sem: Dynamics Op State;
initP: State -> Prop }.
Coercion sem : Layer >-> Dynamics.
Section Abstraction.
Context (AState CState:Type).
Context (absr: relation AState CState unit).
Definition refine_spec T R (spec: Specification T R AState)
: AState -> Specification T R CState.
exact (fun s cs =>
{| pre := absr s cs tt /\
(spec s).(pre);
post := fun cs' r =>
exists s', absr s' cs' tt /\
(spec s).(post) s' r;
alternate := fun cs' r =>
exists s', absr s' cs' tt /\
(spec s).(alternate) s' r; |}).
Defined.
End Abstraction.
Module Export OneDiskAPI.
Module Export D.
Definition State := disk.
End D.
Definition read_spec (a : addr) : Specification block unit D.State.
Admitted.
Inductive diskId :=
| d0
| d1.
Inductive DiskResult T :=
| Working (v:T)
| Failed.
Definition disk0 (state:State) : option disk.
Admitted.
Definition disk1 (state:State) : option disk.
Admitted.
Inductive Op : Type -> Type :=
| op_read (i : diskId) (a : addr) : Op (DiskResult block)
| op_write (i : diskId) (a : addr) (b : block) : Op (DiskResult unit)
| op_size (i : diskId) : Op (DiskResult nat).
Definition TDBaseDynamics : Dynamics Op State.
Admitted.
Definition td_init (s: State) :=
exists d_0' d_1',
disk0 s ?|= eq d_0' /\
disk1 s ?|= eq d_1'.
Definition TDLayer : Layer Op.
exact ({| Layer.State := State; sem := TDBaseDynamics; initP := td_init |}).
Defined.
Definition read (a:addr) : proc Op block.
Admitted.
Theorem read_int_ok : forall a d,
proc_hspec TDLayer
(read a)
(fun state =>
{|
pre := disk0 state ?|= eq d /\
disk1 state ?|= eq d;
post :=
fun state' r =>
index d a ?|= eq r /\
disk0 state' ?|= eq d /\
disk1 state' ?|= eq d;
alternate :=
fun state' _ =>
disk0 state' ?|= eq d /\
disk1 state' ?|= eq d;
|}).
Admitted.
Global Hint Resolve read_int_ok : core.
Definition Recover : proc Op unit.
Admitted.
Inductive DiskStatus :=
| FullySynced
| OutOfSync (a:addr) (b:block).
Definition Recover_spec : _ -> _ -> Specification unit unit State :=
fun d s state =>
{|
pre :=
match s with
| FullySynced => disk0 state ?|= eq d /\
disk1 state ?|= eq d
| OutOfSync a b => disk0 state ?|= eq (assign d a b) /\
disk1 state ?|= eq d
end;
post :=
fun state' (_:unit) =>
match s with
| FullySynced => disk0 state' ?|= eq d /\
disk1 state' ?|= eq d
| OutOfSync a b =>
(disk0 state' ?|= eq d /\
disk1 state' ?|= eq d) \/
(disk0 state' ?|= eq (assign d a b) /\
disk1 state' ?|= eq (assign d a b))
end;
alternate :=
fun state' (_:unit) =>
match s with
| FullySynced => disk0 state' ?|= eq d /\
disk1 state' ?|= eq d
| OutOfSync a b =>
(disk0 state' ?|= eq d /\
disk1 state' ?|= eq d) \/
(disk0 state' ?|= eq (assign d a b) /\
disk1 state' ?|= eq d) \/
(disk0 state' ?|= eq (assign d a b) /\
disk1 state' ?|= eq (assign d a b))
end;
|}.
Theorem Recover_rok1 d s :
proc_hspec TDLayer
(Recover)
(Recover_spec d s).
Admitted.
Theorem Recover_spec_idempotent1 d :
idempotent (fun (t : unit) => Recover_spec d (FullySynced)).
Admitted.
Definition rd_abstraction (d:D.State) (state: State) (u: unit) : Prop.
admit.
Defined.
Theorem read_rec_ok :
forall a d, proc_rspec TDLayer (read a) Recover
(refine_spec rd_abstraction (OneDiskAPI.read_spec a) d).
Proof.
intros a d.
eapply proc_hspec_to_rspec; eauto using Recover_spec_idempotent1;
unfold refine_spec, rd_abstraction in *.
-
intros [].
eapply Recover_rok1.🛠️ 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 2.6MiB file on GitHub Actions Artifacts under
|
Contributor
|
Minimized File /home/runner/work/run-coq-bug-minimizer/run-coq-bug-minimizer/builds/coq/coq-failing/_build_ci/hott/theories/Algebra/Groups/FreeProduct.v (from ci-hott) (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" "-noinit" "-indices-matter" "-w" "-deprecated-native-compiler-option" "-native-compiler" "no" "-R" "/github/workspace/builds/coq/coq-failing/_build_ci/hott/theories" "HoTT" "-Q" "/github/workspace/cwd" "Top" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/hott/contrib" "HoTT.Contrib" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/hott/test" "HoTT.Tests" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq/user-contrib/Ltac2" "Ltac2" "-top" "HoTT.Algebra.Groups.FreeProduct") -*- *)
(* File reduced by coq-bug-minimizer from original input, then from 731 lines to 61 lines, then from 74 lines to 1249 lines, then from 1253 lines to 83 lines, then from 96 lines to 774 lines, then from 776 lines to 103 lines, then from 116 lines to 628 lines, then from 631 lines to 131 lines, then from 144 lines to 587 lines, then from 592 lines to 168 lines, then from 181 lines to 866 lines, then from 866 lines to 250 lines, then from 263 lines to 2527 lines, then from 2530 lines to 293 lines, then from 306 lines to 1165 lines, then from 1166 lines to 315 lines, then from 328 lines to 940 lines, then from 944 lines to 316 lines, then from 329 lines to 886 lines, then from 891 lines to 316 lines, then from 329 lines to 712 lines, then from 717 lines to 317 lines, then from 330 lines to 369 lines, then from 374 lines to 319 lines, then from 332 lines to 900 lines, then from 905 lines to 353 lines, then from 366 lines to 504 lines, then from 506 lines to 428 lines, then from 441 lines to 483 lines, then from 488 lines to 438 lines, then from 451 lines to 715 lines, then from 720 lines to 466 lines, then from 479 lines to 717 lines, then from 722 lines to 525 lines, then from 538 lines to 1221 lines, then from 1223 lines to 576 lines, then from 589 lines to 1371 lines, then from 1375 lines to 657 lines, then from 670 lines to 760 lines, then from 765 lines to 666 lines, then from 679 lines to 989 lines, then from 991 lines to 681 lines, then from 686 lines to 681 lines *)
(* coqc version 9.0+alpha compiled with OCaml 4.09.0
coqtop version runner-wbcqh1i1-project-4504-concurrent-0:/builds/coq/coq/_build/default,(HEAD detached at c04db99c8cfb) (c04db99c8cfbe3fa002bf604971eb5b0e09656d4)
Expected coqc runtime on this file: 0.181 sec *)
Declare Scope type_scope.
Reserved Notation "x -> y" (at level 99, right associativity, y at level 200).
Reserved Notation "x = y :> T"
(at level 70, y at next level, no associativity).
Reserved Notation "x + y" (at level 50, left associativity).
Reserved Notation "x * y" (at level 40, left associativity).
Reserved Notation "f == g" (at level 70, no associativity).
Reserved Notation "g 'o' f" (at level 40, left associativity).
Delimit Scope function_scope with function.
Delimit Scope trunc_scope with trunc.
Global Open Scope trunc_scope.
Global Open Scope type_scope.
Declare ML Module "ltac_plugin:coq-core.plugins.ltac".
Declare ML Module "number_string_notation_plugin:coq-core.plugins.number_string_notation".
Global Set Default Proof Mode "Classic".
Global Set Universe Polymorphism.
Global Unset Strict Universe Declaration.
Create HintDb typeclass_instances discriminated.
Notation "A -> B" := (forall (_ : A), B) : type_scope.
Inductive option (A : Type) : Type :=
| Some : A -> option A
| None : option A.
Register option as core.option.type.
Inductive sum (A B : Type) : Type :=
| inl : A -> sum A B
| inr : B -> sum A B.
Notation "x + y" := (sum x y) : type_scope.
Record prod (A B : Type) := pair { fst : A ; snd : B }.
Notation "x * y" := (prod x y) : type_scope.
Notation Type0 := Set.
Notation idmap := (fun x => x).
Record sig {A} (P : A -> Type) := exist {
proj1 : A ;
proj2 : P proj1 ;
}.
Notation compose := (fun g f x => g (f x)).
Notation "g 'o' f" := (compose g%function f%function) : function_scope.
Inductive paths {A : Type} (a : A) : A -> Type :=
idpath : paths a a.
Notation "x = y :> A" := (@paths A x y) : type_scope.
Notation "x = y" := (x = y :>_) : type_scope.
Definition ap {A B : Type} (f : A -> B) {x y : A} (p : x = y) : f x = f y.
Admitted.
Definition pointwise_paths A (P : A -> Type) (f g : forall x, P x)
:= forall x, f x = g x.
Global Arguments pointwise_paths {A}%_type_scope {P} (f g)%_function_scope.
Notation "f == g" := (pointwise_paths f g) : type_scope.
Class IsEquiv {A B : Type} (f : A -> B) := {
equiv_inv : B -> A ;
eisretr : f o equiv_inv == idmap ;
eissect : equiv_inv o f == idmap ;
eisadj : forall x : A, eisretr (f x) = ap f (eissect x) ;
}.
Monomorphic Axiom Funext : Type0.
Existing Class Funext.
Inductive trunc_index : Type0 :=
| minus_two : trunc_index
| trunc_S : trunc_index -> trunc_index.
Notation "n .+1" := (trunc_S n) : trunc_scope.
Notation "n .+2" := (n.+1.+1)%trunc : trunc_scope.
Inductive IsTrunc_internal (A : Type@{u}) : trunc_index -> Type@{u} :=
| Build_Contr : forall (center : A) (contr : forall y, center = y), IsTrunc_internal A minus_two
| istrunc_S : forall {n:trunc_index}, (forall x y:A, IsTrunc_internal (x = y) n) -> IsTrunc_internal A (trunc_S n).
Existing Class IsTrunc_internal.
Notation IsTrunc n A := (IsTrunc_internal A n).
Notation IsHProp A := (IsTrunc minus_two.+1 A).
Notation IsHSet A := (IsTrunc minus_two.+2 A).
Inductive nat : Type0 :=
| O : nat
| S : nat -> nat.
Inductive Unit : Type0 := tt : Unit.
Tactic Notation "do_with_holes" tactic3(x) uconstr(p) :=
x uconstr:(p) ||
x uconstr:(p _) ||
x uconstr:(p _ _) ||
x uconstr:(p _ _ _) ||
x uconstr:(p _ _ _ _) ||
x uconstr:(p _ _ _ _ _) ||
x uconstr:(p _ _ _ _ _ _) ||
x uconstr:(p _ _ _ _ _ _ _) ||
x uconstr:(p _ _ _ _ _ _ _ _) ||
x uconstr:(p _ _ _ _ _ _ _ _ _) ||
x uconstr:(p _ _ _ _ _ _ _ _ _ _) ||
x uconstr:(p _ _ _ _ _ _ _ _ _ _ _) ||
x uconstr:(p _ _ _ _ _ _ _ _ _ _ _ _) ||
x uconstr:(p _ _ _ _ _ _ _ _ _ _ _ _ _) ||
x uconstr:(p _ _ _ _ _ _ _ _ _ _ _ _ _ _) ||
x uconstr:(p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) ||
x uconstr:(p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) ||
x uconstr:(p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) ||
x uconstr:(p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) ||
x uconstr:(p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) ||
x uconstr:(p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) ||
x uconstr:(p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) ||
x uconstr:(p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) ||
x uconstr:(p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) ||
x uconstr:(p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) ||
x uconstr:(p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) ||
x uconstr:(p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) ||
x uconstr:(p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) ||
x uconstr:(p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) ||
x uconstr:(p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) ||
x uconstr:(p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _).
Class IsGlobalAxiom (A : Type) : Type0 := {}.
Ltac is_global_axiom A := let _ := constr:(_ : IsGlobalAxiom A) in idtac.
Ltac global_axiom := try match goal with
| |- ?G => is_global_axiom G; exact _
end.
Tactic Notation "srefine" uconstr(term) := simple refine term.
Tactic Notation "snrefine" uconstr(term) := simple notypeclasses refine term; global_axiom.
Tactic Notation "rapply" uconstr(term)
:= do_with_holes ltac:(fun x => refine x) term.
Tactic Notation "srapply" uconstr(term)
:= do_with_holes ltac:(fun x => srefine x) term.
Tactic Notation "snrapply" uconstr(term)
:= do_with_holes ltac:(fun x => snrefine x) term.
Module Export Decimal.
Inductive uint : Type0 :=
| Nil
| D0 (_:uint)
| D1 (_:uint)
| D2 (_:uint)
| D3 (_:uint)
| D4 (_:uint)
| D5 (_:uint)
| D6 (_:uint)
| D7 (_:uint)
| D8 (_:uint)
| D9 (_:uint).
Notation zero := (D0 Nil).
Variant int : Type0 := Pos (d:uint) | Neg (d:uint).
Variant decimal : Type0 :=
| Decimal (i:int) (f:uint)
| DecimalExp (i:int) (f:uint) (e:int).
Register uint as num.uint.type.
Register int as num.int.type.
Register decimal as num.decimal.type.
Fixpoint revapp (d d' : uint) :=
match d with
| Nil => d'
| D0 d => revapp d (D0 d')
| D1 d => revapp d (D1 d')
| D2 d => revapp d (D2 d')
| D3 d => revapp d (D3 d')
| D4 d => revapp d (D4 d')
| D5 d => revapp d (D5 d')
| D6 d => revapp d (D6 d')
| D7 d => revapp d (D7 d')
| D8 d => revapp d (D8 d')
| D9 d => revapp d (D9 d')
end.
Definition rev d := revapp d Nil.
Module Export Little.
Fixpoint succ d :=
match d with
| Nil => D1 Nil
| D0 d => D1 d
| D1 d => D2 d
| D2 d => D3 d
| D3 d => D4 d
| D4 d => D5 d
| D5 d => D6 d
| D6 d => D7 d
| D7 d => D8 d
| D8 d => D9 d
| D9 d => D0 (succ d)
end.
Module Export Hexadecimal.
Inductive uint : Type0 :=
| Nil
| D0 (_:uint)
| D1 (_:uint)
| D2 (_:uint)
| D3 (_:uint)
| D4 (_:uint)
| D5 (_:uint)
| D6 (_:uint)
| D7 (_:uint)
| D8 (_:uint)
| D9 (_:uint)
| Da (_:uint)
| Db (_:uint)
| Dc (_:uint)
| Dd (_:uint)
| De (_:uint)
| Df (_:uint).
Variant hexadecimal : Type0 :=
| Hexadecimal (i:int) (f:uint)
| HexadecimalExp (i:int) (f:uint) (e:Decimal.int).
Register uint as num.hexadecimal_uint.type.
Register int as num.hexadecimal_int.type.
Register hexadecimal as num.hexadecimal.type.
Module Export Numeral.
Variant uint : Type0 := UIntDec (u:Decimal.uint) | UIntHex (u:Hexadecimal.uint).
Variant numeral : Type0 := Dec (d:Decimal.decimal) | Hex (h:Hexadecimal.hexadecimal).
Register uint as num.num_uint.type.
Register int as num.num_int.type.
Register numeral as num.number.type.
Fixpoint tail_add n m :=
match n with
| O => m
| S n => tail_add n (S m)
end.
Fixpoint tail_addmul r n m :=
match n with
| O => r
| S n => tail_addmul (tail_add m r) n m
end.
Definition tail_mul n m := tail_addmul O n m.
Local Notation ten := (S (S (S (S (S (S (S (S (S (S O)))))))))).
Fixpoint of_uint_acc (d:Decimal.uint)(acc:nat) :=
match d with
| Decimal.Nil => acc
| Decimal.D0 d => of_uint_acc d (tail_mul ten acc)
| Decimal.D1 d => of_uint_acc d (S (tail_mul ten acc))
| Decimal.D2 d => of_uint_acc d (S (S (tail_mul ten acc)))
| Decimal.D3 d => of_uint_acc d (S (S (S (tail_mul ten acc))))
| Decimal.D4 d => of_uint_acc d (S (S (S (S (tail_mul ten acc)))))
| Decimal.D5 d => of_uint_acc d (S (S (S (S (S (tail_mul ten acc))))))
| Decimal.D6 d => of_uint_acc d (S (S (S (S (S (S (tail_mul ten acc)))))))
| Decimal.D7 d => of_uint_acc d (S (S (S (S (S (S (S (tail_mul ten acc))))))))
| Decimal.D8 d => of_uint_acc d (S (S (S (S (S (S (S (S (tail_mul ten acc)))))))))
| Decimal.D9 d => of_uint_acc d (S (S (S (S (S (S (S (S (S (tail_mul ten acc))))))))))
end.
Definition of_uint (d:Decimal.uint) := of_uint_acc d O.
Local Notation sixteen := (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S O)))))))))))))))).
Fixpoint of_hex_uint_acc (d:Hexadecimal.uint)(acc:nat) :=
match d with
| Hexadecimal.Nil => acc
| Hexadecimal.D0 d => of_hex_uint_acc d (tail_mul sixteen acc)
| Hexadecimal.D1 d => of_hex_uint_acc d (S (tail_mul sixteen acc))
| Hexadecimal.D2 d => of_hex_uint_acc d (S (S (tail_mul sixteen acc)))
| Hexadecimal.D3 d => of_hex_uint_acc d (S (S (S (tail_mul sixteen acc))))
| Hexadecimal.D4 d => of_hex_uint_acc d (S (S (S (S (tail_mul sixteen acc)))))
| Hexadecimal.D5 d => of_hex_uint_acc d (S (S (S (S (S (tail_mul sixteen acc))))))
| Hexadecimal.D6 d => of_hex_uint_acc d (S (S (S (S (S (S (tail_mul sixteen acc)))))))
| Hexadecimal.D7 d => of_hex_uint_acc d (S (S (S (S (S (S (S (tail_mul sixteen acc))))))))
| Hexadecimal.D8 d => of_hex_uint_acc d (S (S (S (S (S (S (S (S (tail_mul sixteen acc)))))))))
| Hexadecimal.D9 d => of_hex_uint_acc d (S (S (S (S (S (S (S (S (S (tail_mul sixteen acc))))))))))
| Hexadecimal.Da d => of_hex_uint_acc d (S (S (S (S (S (S (S (S (S (S (tail_mul sixteen acc)))))))))))
| Hexadecimal.Db d => of_hex_uint_acc d (S (S (S (S (S (S (S (S (S (S (S (tail_mul sixteen acc))))))))))))
| Hexadecimal.Dc d => of_hex_uint_acc d (S (S (S (S (S (S (S (S (S (S (S (S (tail_mul sixteen acc)))))))))))))
| Hexadecimal.Dd d => of_hex_uint_acc d (S (S (S (S (S (S (S (S (S (S (S (S (S (tail_mul sixteen acc))))))))))))))
| Hexadecimal.De d => of_hex_uint_acc d (S (S (S (S (S (S (S (S (S (S (S (S (S (S (tail_mul sixteen acc)))))))))))))))
| Hexadecimal.Df d => of_hex_uint_acc d (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (tail_mul sixteen acc))))))))))))))))
end.
Definition of_hex_uint (d:Hexadecimal.uint) := of_hex_uint_acc d O.
Definition of_num_uint (d:Numeral.uint) :=
match d with
| Numeral.UIntDec d => of_uint d
| Numeral.UIntHex d => of_hex_uint d
end.
Fixpoint to_little_uint n acc :=
match n with
| O => acc
| S n => to_little_uint n (Decimal.Little.succ acc)
end.
Definition to_uint n :=
Decimal.rev (to_little_uint n Decimal.zero).
Definition to_num_uint n := Numeral.UIntDec (to_uint n).
Number Notation nat of_num_uint to_num_uint (abstract after 5001) : nat_scope.
Module Export HoTT_DOT_Basics_DOT_Trunc_WRAPPED.
Module Export Trunc.
Generalizable Variables A B m n f.
Fixpoint trunc_index_inc@{} (k : trunc_index) (n : nat)
: trunc_index.
exact (match n with
| O => k
| S m => (trunc_index_inc k m).+1
end).
Defined.
Definition nat_to_trunc_index@{} (n : nat) : trunc_index.
exact ((trunc_index_inc minus_two n).+2).
Defined.
Coercion nat_to_trunc_index : nat >-> trunc_index.
Global Instance istrunc_paths' {n : trunc_index} {A : Type} `{IsTrunc n A}
: forall x y : A, IsTrunc n (x = y) | 1000.
Admitted.
Definition istrunc_isequiv_istrunc A {B} (f : A -> B)
`{IsTrunc n A} `{IsEquiv A B f}
: IsTrunc n B.
Admitted.
Global Instance ishprop_istrunc `{Funext} (n : trunc_index) (A : Type)
: IsHProp (IsTrunc n A) | 0.
Admitted.
End Trunc.
End HoTT_DOT_Basics_DOT_Trunc_WRAPPED.
Definition Coeq@{i j u} {B : Type@{i}} {A : Type@{j}} (f g : B -> A) : Type@{u}.
Admitted.
Local Open Scope nat_scope.
Definition ExtensionAlong@{a b p m} {A : Type@{a}} {B : Type@{b}} (f : A -> B)
(P : B -> Type@{p}) (d : forall x:A, P (f x))
:=
sig@{m m} (fun (s : forall y:B, P y) => forall x:A, s (f x) = d x).
Fixpoint ExtendableAlong@{i j k l}
(n : nat) {A : Type@{i}} {B : Type@{j}}
(f : A -> B) (C : B -> Type@{k}) : Type@{l}
:= match n with
| 0 => Unit
| S n => (forall (g : forall a, C (f a)),
ExtensionAlong@{i j k l} f C g) *
forall (h k : forall b, C b),
ExtendableAlong n f (fun b => h b = k b)
end.
Definition ooExtendableAlong@{i j k l}
{A : Type@{i}} {B : Type@{j}}
(f : A -> B) (C : B -> Type@{k}) : Type@{l}.
exact (forall n : nat, ExtendableAlong@{i j k l} n f C).
Defined.
Record Subuniverse@{i} :=
{
In_internal : Type@{i} -> Type@{i} ;
hprop_inO_internal : Funext -> forall (T : Type@{i}),
IsHProp (In_internal T) ;
inO_equiv_inO_internal : forall (T U : Type@{i}) (T_inO : In_internal T)
(f : T -> U) {feq : IsEquiv f},
In_internal U ;
}.
Class In (O : Subuniverse) (T : Type) := in_internal : In_internal O T.
Class PreReflects@{i} (O : Subuniverse@{i}) (T : Type@{i}) :=
{
O_reflector : Type@{i} ;
O_inO : In O O_reflector ;
to : T -> O_reflector ;
}.
Arguments O_reflector O T {_}.
Arguments to O T {_}.
Class Reflects@{i} (O : Subuniverse@{i}) (T : Type@{i})
`{PreReflects@{i} O T} :=
{
extendable_to_O : forall {Q : Type@{i}} {Q_inO : In O Q},
ooExtendableAlong (to O T) (fun _ => Q)
}.
Record ReflectiveSubuniverse@{i} :=
{
rsu_subuniv : Subuniverse@{i} ;
rsu_prereflects : forall (T : Type@{i}), PreReflects rsu_subuniv T ;
rsu_reflects : forall (T : Type@{i}), Reflects rsu_subuniv T ;
}.
Coercion rsu_subuniv : ReflectiveSubuniverse >-> Subuniverse.
Global Existing Instance rsu_prereflects.
Definition rsu_reflector (O : ReflectiveSubuniverse) (T : Type) : Type.
exact (O_reflector O T).
Defined.
Coercion rsu_reflector : ReflectiveSubuniverse >-> Funclass.
Class ReflectsD@{i} (O' O : Subuniverse@{i}) (T : Type@{i})
`{PreReflects@{i} O' T} :=
{
extendable_to_OO :
forall (Q : O_reflector O' T -> Type@{i}) {Q_inO : forall x, In O (Q x)},
ooExtendableAlong (to O' T) Q
}.
Definition reflectsD_from_OO_ind@{i} {O' O : Subuniverse@{i}}
{A : Type@{i}} `{PreReflects O' A}
(OO_ind' : forall (B : O_reflector O' A -> Type@{i})
(B_inO : forall oa, In O (B oa))
(f : forall a, B (to O' A a))
oa, B oa)
(OO_ind_beta' : forall (B : O_reflector O' A -> Type@{i})
(B_inO : forall oa, In O (B oa))
(f : forall a, B (to O' A a))
a, OO_ind' B B_inO f (to O' A a) = f a)
(inO_paths' : forall (B : Type@{i}) (B_inO : In O B)
(z z' : B), In O (z = z'))
: ReflectsD O' O A.
Admitted.
Record Modality@{i} := Build_Modality'
{
modality_subuniv : Subuniverse@{i} ;
modality_prereflects : forall (T : Type@{i}),
PreReflects modality_subuniv T ;
modality_reflectsD : forall (T : Type@{i}),
ReflectsD modality_subuniv modality_subuniv T ;
}.
Global Existing Instance modality_reflectsD.
Definition modality_to_reflective_subuniverse (O : Modality@{i})
: ReflectiveSubuniverse@{i}.
Proof.
refine (Build_ReflectiveSubuniverse
(modality_subuniv O) (modality_prereflects O) _).
intros T; constructor.
intros Q Q_inO.
srapply extendable_to_OO.
Defined.
Coercion modality_to_reflective_subuniverse : Modality >-> ReflectiveSubuniverse.
Definition Build_Modality
(In' : Type -> Type)
(hprop_inO' : Funext -> forall T : Type, IsHProp (In' T))
(inO_equiv_inO' : forall T U : Type,
In' T -> forall f : T -> U, IsEquiv f -> In' U)
(O_reflector' : Type -> Type)
(O_inO' : forall T, In' (O_reflector' T))
(to' : forall T, T -> O_reflector' T)
(O_ind' : forall (A : Type) (B : O_reflector' A -> Type)
(B_inO : forall oa, In' (B oa))
(f : forall a, B (to' A a))
(z : O_reflector' A),
B z)
(O_ind_beta' : forall (A : Type) (B : O_reflector' A -> Type)
(B_inO : forall oa, In' (B oa))
(f : forall a, B (to' A a)) (a : A),
O_ind' A B B_inO f (to' A a) = f a)
(inO_paths' : forall (A : Type) (A_inO : In' A) (z z' : A),
In' (z = z'))
: Modality.
Proof.
pose (O := Build_Subuniverse In' hprop_inO' inO_equiv_inO').
simple refine (Build_Modality' O _ _); intros T.
-
exact (Build_PreReflects O T (O_reflector' T) (O_inO' T) (to' T)).
-
srapply reflectsD_from_OO_ind.
+
rapply O_ind'.
+
rapply O_ind_beta'.
+
rapply inO_paths'.
Defined.
Module Export Trunc.
Cumulative Private Inductive Trunc (n : trunc_index) (A :Type) : Type :=
tr : A -> Trunc n A.
Arguments tr {n A} a.
Global Instance istrunc_truncation (n : trunc_index) (A : Type@{i})
: IsTrunc@{j} n (Trunc@{i} n A).
Admitted.
Definition Trunc_ind {n A}
(P : Trunc n A -> Type) {Pt : forall aa, IsTrunc n (P aa)}
: (forall a, P (tr a)) -> (forall aa, P aa).
exact (fun f aa => match aa with tr a => fun _ => f a end Pt).
Defined.
End Trunc.
Definition Tr (n : trunc_index) : Modality.
Proof.
srapply (Build_Modality (fun A => IsTrunc n A)); cbn.
-
intros A B ? f ?; rapply (istrunc_isequiv_istrunc A f).
-
exact (Trunc n).
-
intros; apply istrunc_truncation.
-
intros A; apply tr.
-
intros A B ? f oa; cbn in *.
exact (Trunc_ind B f oa).
-
intros; reflexivity.
-
exact (@istrunc_paths' n).
Defined.
Declare Scope mc_scope.
Global Open Scope mc_scope.
Class SgOp A := sg_op: A -> A -> A.
Class MonUnit A := mon_unit: A.
Class Negate A := negate: A -> A.
Infix "*" := sg_op : mc_mult_scope.
Notation "(.*.)" := sg_op (only parsing) : mc_mult_scope.
Notation "(-)" := negate (only parsing) : mc_scope.
Class LeftIdentity {A B} (op : A -> B -> B) (x : A): Type
:= left_identity: forall y, op x y = y.
Class RightIdentity {A B} (op : A -> B -> A) (y : B): Type
:= right_identity: forall x, op x y = x.
Class LeftInverse {A} {B} {C} (op : A -> B -> C) (inv : B -> A) (unit : C)
:= left_inverse: forall x, op (inv x) x = unit.
Class RightInverse {A} {B} {C} (op : A -> B -> C) (inv : A -> B) (unit : C)
:= right_inverse: forall x, op x (inv x) = unit.
Class HeteroAssociative {A B C AB BC ABC}
(fA_BC: A -> BC -> ABC) (fBC: B -> C -> BC)
(fAB_C: AB -> C -> ABC) (fAB : A -> B -> AB): Type
:= associativity : forall x y z, fA_BC x (fBC y z) = fAB_C (fAB x y) z.
Class Associative {A} (f : A -> A -> A)
:= simple_associativity : HeteroAssociative f f f f.
Section upper_classes.
Context (A : Type@{i}).
Local Open Scope mc_mult_scope.
Class IsSemiGroup {Aop: SgOp A} :=
{ sg_set : IsHSet A
; sg_ass : Associative (.*.) }.
Class IsMonoid {Aop : SgOp A} {Aunit : MonUnit A} :=
{ monoid_semigroup : IsSemiGroup
; monoid_left_id : LeftIdentity (.*.) mon_unit
; monoid_right_id : RightIdentity (.*.) mon_unit }.
Class IsGroup {Aop : SgOp A} {Aunit : MonUnit A} {Anegate : Negate A} :=
{ group_monoid : @IsMonoid (.*.) Aunit
; negate_l : LeftInverse (.*.) (-) mon_unit
; negate_r : RightInverse (.*.) (-) mon_unit }.
End upper_classes.
Section sgmorphism_classes.
Context {A B : Type} {Aop : SgOp A} {Bop : SgOp B}
{Aunit : MonUnit A} {Bunit : MonUnit B}.
Local Open Scope mc_mult_scope.
Class IsSemiGroupPreserving (f : A -> B) :=
preserves_sg_op : forall x y, f (x * y) = f x * f y.
End sgmorphism_classes.
Record Group := {
group_type :> Type;
group_sgop :: SgOp group_type;
group_unit :: MonUnit group_type;
group_inverse :: Negate group_type;
group_isgroup :: IsGroup group_type;
}.
Record GroupHomomorphism (G H : Group) := Build_GroupHomomorphism {
grp_homo_map :> group_type G -> group_type H;
issemigrouppreserving_grp_homo :: IsSemiGroupPreserving grp_homo_map;
}.
Section FreeProduct.
Context (G H K : Group)
(f : GroupHomomorphism G H) (g : GroupHomomorphism G K).
Local Definition Words : Type.
Admitted.
Local Definition pc1 : Type.
Admitted.
Local Definition pc2 : Type.
Admitted.
Local Definition pc3 : Type.
Admitted.
Local Definition pc4 : Type.
Admitted.
Local Definition pc5 : Type.
Admitted.
Local Definition map1 : pc1 + pc2 + pc3 + pc4 + pc5 -> Words.
Admitted.
Local Definition map2 : pc1 + pc2 + pc3 + pc4 + pc5 -> Words.
Admitted.
Definition amal_type : Type.
exact (Tr 0 (Coeq map1 map2)).
Defined.
Global Instance sgop_amal_type : SgOp amal_type.
Admitted.
Global Instance monunit_amal_type : MonUnit amal_type.
Admitted.
Global Instance negate_amal_type : Negate amal_type.
Admitted.
Global Instance associative_sgop_m : Associative sg_op.
Admitted.
Global Instance leftidentity_sgop_amal_type : LeftIdentity sg_op mon_unit.
Admitted.
Global Instance rightidentity_sgop_amal_type : RightIdentity sg_op mon_unit.
Admitted.
Global Instance leftinverse_sgop_amal_type : LeftInverse sg_op negate mon_unit.
Admitted.
Global Instance rightinverse_sgop_amal_type : RightInverse sg_op negate mon_unit.
Admitted.
Definition AmalgamatedFreeProduct : Group.
Proof.
snrapply (Build_Group amal_type); repeat split; exact _.🛠️ 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
|
Contributor
|
Minimized File /home/runner/work/run-coq-bug-minimizer/run-coq-bug-minimizer/builds/coq/coq-failing/_build_ci/fiat_parsers/src/Common/FMapExtensions/LiftRelationInstances.v (from ci-fiat_parsers) (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" "-compat" "8.4" "-w" "unsupported-attributes" "-w" "-deprecated-native-compiler-option" "-native-compiler" "no" "-w" "-deprecated-appcontext -notation-overridden" "-R" "/github/workspace/builds/coq/coq-failing/_build_ci/fiat_parsers/src" "Fiat" "-R" "/github/workspace/builds/coq/coq-failing/_build_ci/fiat_parsers/Bedrock" "Bedrock" "-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/fiat_parsers/src/Common/Tactics" "-I" "/github/workspace/builds/coq/coq-failing/_build_ci/fiat_parsers" "-top" "Fiat.Common.FMapExtensions.LiftRelationInstances") -*- *)
(* File reduced by coq-bug-minimizer from original input, then from 891 lines to 51 lines, then from 64 lines to 185 lines, then from 190 lines to 52 lines, then from 65 lines to 2346 lines, then from 2343 lines to 74 lines, then from 87 lines to 1906 lines, then from 1906 lines to 76 lines, then from 89 lines to 247 lines, then from 252 lines to 170 lines, then from 183 lines to 236 lines, then from 241 lines to 185 lines, then from 190 lines to 186 lines *)
(* coqc version 9.0+alpha compiled with OCaml 4.09.0
coqtop version runner-wbcqh1i1-project-4504-concurrent-0:/builds/coq/coq/_build/default,(HEAD detached at c04db99c8cfb) (c04db99c8cfbe3fa002bf604971eb5b0e09656d4)
Expected coqc runtime on this file: 0.738 sec *)
Require Stdlib.FSets.FMapFacts.
Ltac split_in_context_by ident funl funr tac :=
repeat match goal with
| [ H : context p [ident] |- _ ] =>
let H0 := context p[funl] in let H0' := eval simpl in H0 in assert H0' by (tac H);
let H1 := context p[funr] in let H1' := eval simpl in H1 in assert H1' by (tac H);
clear H
end.
Ltac split_in_context ident funl funr :=
split_in_context_by ident funl funr ltac:(fun H => apply H).
Ltac split_and' :=
repeat match goal with
| [ H : ?a /\ ?b |- _ ] => let H0 := fresh in let H1 := fresh in
assert (H0 := fst H); assert (H1 := snd H); clear H
end.
Ltac split_and := split_and'; split_in_context and (fun a b : Type => a) (fun a b : Type => b).
Ltac set_match_refl v' only_when :=
lazymatch goal with
| [ |- context G[match ?e with _ => _ end eq_refl] ]
=> only_when e;
let T := fresh in
evar (T : Type); evar (v' : T);
subst T;
let vv := (eval cbv delta [v'] in v') in
let G' := context G[vv] in
let G''' := context G[v'] in
lazymatch goal with |- ?G'' => unify G' G'' end;
change G'''
end.
Ltac set_match_refl_hyp v' only_when :=
lazymatch goal with
| [ H : context G[match ?e with _ => _ end eq_refl] |- _ ]
=> only_when e;
let T := fresh in
evar (T : Type); evar (v' : T);
subst T;
let vv := (eval cbv delta [v'] in v') in
let G' := context G[vv] in
let G''' := context G[v'] in
let G'' := type of H in
unify G' G'';
change G''' in H
end.
Ltac destruct_by_existing_equation match_refl_hyp :=
let v := (eval cbv delta [match_refl_hyp] in match_refl_hyp) in
lazymatch v with
| match ?e with _ => _ end (@eq_refl ?T ?e)
=> let H := fresh in
let e' := fresh in
pose e as e';
change e with e' in (value of match_refl_hyp) at 1;
first [ pose (@eq_refl T e : e = e') as H;
change (@eq_refl T e) with H in (value of match_refl_hyp);
clearbody H e'
| pose (@eq_refl T e : e' = e) as H;
change (@eq_refl T e) with H in (value of match_refl_hyp);
clearbody H e' ];
destruct e'; subst match_refl_hyp
end.
Ltac destruct_rewrite_sumbool e :=
let H := fresh in
destruct e as [H|H];
try lazymatch type of H with
| ?LHS = ?RHS
=> lazymatch RHS with
| context[LHS] => fail
| _ => idtac
end;
rewrite ?H; rewrite ?H in *;
repeat match goal with
| [ |- context G[LHS] ]
=> let LHS' := fresh in
pose LHS as LHS';
let G' := context G[LHS'] in
change G';
replace LHS' with RHS by (subst LHS'; symmetry; apply H);
subst LHS'
end
end.
Ltac break_match_step only_when :=
match goal with
| [ |- context[match ?e with _ => _ end] ]
=> only_when e; is_var e; destruct e
| [ |- context[match ?e with _ => _ end] ]
=> only_when e;
match type of e with
| sumbool _ _ => destruct_rewrite_sumbool e
end
| [ |- context[if ?e then _ else _] ]
=> only_when e; destruct e eqn:?
| [ |- context[match ?e with _ => _ end] ]
=> only_when e; destruct e eqn:?
| _ => let v := fresh in set_match_refl v only_when; destruct_by_existing_equation v
end.
Ltac break_match_hyps_step only_when :=
match goal with
| [ H : context[match ?e with _ => _ end] |- _ ]
=> only_when e; is_var e; destruct e
| [ H : context[match ?e with _ => _ end] |- _ ]
=> only_when e;
match type of e with
| sumbool _ _ => destruct_rewrite_sumbool e
end
| [ H : context[if ?e then _ else _] |- _ ]
=> only_when e; destruct e eqn:?
| [ H : context[match ?e with _ => _ end] |- _ ]
=> only_when e; destruct e eqn:?
| _ => let v := fresh in set_match_refl_hyp v only_when; destruct_by_existing_equation v
end.
Ltac break_match := repeat break_match_step ltac:(fun _ => idtac).
Ltac break_match_hyps := repeat break_match_hyps_step ltac:(fun _ => idtac).
Export Coq.FSets.FMapInterface.
Module FMapExtensions_fun (E: DecidableType) (Import M: WSfun E).
Definition lift_relation_gen_hetero {A B P}
(and : P -> P -> P) (True : P)
(R : A -> B -> P) (defaultA : A) (defaultB : B)
: t A -> t B -> P.
Admitted.
Lemma lift_relation_gen_hetero_iff {A B P} and True' (Q : P -> Prop) R defaultA defaultB (m1 : t A) (m2 : t B)
(QTrue_or_key : Q True' \/ exists k, find k m1 = None /\ find k m2 = None)
(Qand : forall x y, Q (and x y) <-> Q x /\ Q y)
: Q (lift_relation_gen_hetero and True' R defaultA defaultB m1 m2)
<-> forall k, Q (match find k m1, find k m2 with
| Some x1, Some x2 => R x1 x2
| Some x, None => R x defaultB
| None, Some x => R defaultA x
| None, None => True'
end).
Admitted.
End FMapExtensions_fun.
Class pull_forall_able (iffR : Prop -> Prop -> Prop)
:= pull_forall_iffR : forall A P Q, (forall x : A, iffR (P x) (Q x)) -> iffR (forall x, P x) (forall x, Q x).
Module FMapExtensionsLiftRelationInstances_fun (E: DecidableType) (Import M: WSfun E).
Module BasicExtensions := FMapExtensions_fun E M.
Include BasicExtensions.
Section rel.
Context {P} {Q : P -> Prop} {and True'}
(HTrue' : Q True')
(Hand : forall x y, Q (and x y) <-> Q x /\ Q y)
(iffP : P -> P -> Prop)
(iffP_iff : forall x y, iffP x y <-> (Q x <-> Q y))
{A} {default : A}.
Local Coercion Q : P >-> Sortclass.
Local Notation lift R := (@lift_relation_gen_hetero A A P and True' R default default).
Local Ltac t :=
repeat ((rewrite lift_relation_gen_hetero_iff by auto) || intro);
repeat match goal with
| [ H : forall k : key, _, k' : key |- _ ] => specialize (H k')
| [ |- ?R (forall _, _) (forall _, _) ] => apply pull_forall_iffR; intro
end;
try solve [ break_match; break_match_hyps; eauto ].
Context {R : A -> A -> P}.
Context {R1 R2 : A -> A -> P}
{R1_Reflexive : Reflexive R1}
{R2_Reflexive : Reflexive R2}
{R1_subrelation : subrelation R1 R}
{R2_subrelation : subrelation R2 R}.
Global Instance lift_relation_gen_hetero_homo_Proper_Proper_subrelation_iffR
{iffR}
{iffR_Proper : Proper (iff ==> iff ==> flip impl) iffR}
{iffR_pull : pull_forall_able iffR}
{R_Proper : Proper (R1 ==> R2 ==> iffR) R}
: Proper (lift R1 ==> lift R2 ==> iffR) (lift R) | 2.
Proof.
pose proof (R1_Reflexive default).
pose proof (R2_Reflexive default).
t; compute in * |- ; split_and; break_match; try split;
try solve [ eauto 3
| eapply iffR_Proper; [ | | eauto ]; [ | eauto ]; eauto ].
Qed.🛠️ 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
|
Contributor
|
Partially Minimized File /home/runner/work/run-coq-bug-minimizer/run-coq-bug-minimizer/builds/coq/coq-failing/_build_ci/unimath/UniMath/AlgebraicTheories/Combinators.v (from ci-unimath) (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 Ltac2.Notations)(* -*- mode: coq; coq-prog-args: ("-emacs" "-q" "-noinit" "-indices-matter" "-type-in-type" "-w" "-notation-overridden" "-w" "-deprecated-native-compiler-option" "-native-compiler" "no" "-Q" "/github/workspace/cwd" "Top" "-Q" "/github/workspace/builds/coq/coq-failing/_build_ci/unimath/UniMath" "UniMath" "-Q" "/github/workspace/builds/coq/coq-failing/_install_ci/lib/coq/user-contrib/Ltac2" "Ltac2" "-top" "UniMath.AlgebraicTheories.Combinators") -*- *)
(* File reduced by coq-bug-minimizer from original input, then from 2076 lines to 53 lines, then from 66 lines to 121 lines, then from 126 lines to 67 lines, then from 80 lines to 544 lines, then from 550 lines to 81 lines, then from 95 lines to 500 lines, then from 506 lines to 96 lines, then from 110 lines to 433 lines, then from 439 lines to 155 lines, then from 169 lines to 544 lines, then from 550 lines to 170 lines, then from 184 lines to 518 lines, then from 524 lines to 204 lines, then from 218 lines to 557 lines, then from 561 lines to 267 lines, then from 281 lines to 538 lines, then from 544 lines to 291 lines, then from 305 lines to 2633 lines, then from 2603 lines to 296 lines, then from 310 lines to 2483 lines, then from 2431 lines to 306 lines, then from 319 lines to 3402 lines, then from 3274 lines to 309 lines, then from 323 lines to 1112 lines, then from 1084 lines to 313 lines, then from 327 lines to 1494 lines, then from 1486 lines to 313 lines, then from 327 lines to 1690 lines, then from 1558 lines to 312 lines, then from 326 lines to 807 lines, then from 813 lines to 326 lines, then from 340 lines to 1732 lines, then from 1637 lines to 330 lines, then from 344 lines to 4387 lines, then from 4298 lines to 368 lines, then from 382 lines to 587 lines, then from 592 lines to 416 lines, then from 430 lines to 639 lines, then from 645 lines to 464 lines, then from 470 lines to 465 lines *)
(* coqc version 9.0+alpha compiled with OCaml 4.14.1
coqtop version runner-t7b1znuaq-project-4504-concurrent-0:/builds/coq/coq/_build/default,(HEAD detached at c04db99c8cfbe3) (c04db99c8cfbe3fa002bf604971eb5b0e09656d4)
Modules that could not be inlined: Ltac2.Notations
Expected coqc runtime on this file: 0.213 sec *)
Require Ltac2.Notations.
Inductive False : Prop := .
Axiom proof_admitted : False.
Tactic Notation "admit" := abstract case proof_admitted.
Export Coq.Init.Notations.
Export Stdlib.Init.Ltac.
Notation "'∏' x .. y , P" := (forall x, .. (forall y, P) ..)
(at level 200, x binder, y binder, right associativity) : type_scope.
Notation "'λ' x .. y , t" := (fun x => .. (fun y => t) ..)
(at level 200, x binder, y binder, right associativity).
Notation "A -> B" := (forall (_ : A), B) : type_scope.
Notation "x → y" := (x -> y)
(at level 99, y at level 200, right associativity): type_scope.
Reserved Notation "X ≃ Y" (at level 80, no associativity).
Reserved Notation "f ~ g" (at level 70, no associativity).
Reserved Notation "p @ q" (at level 60, right associativity).
Reserved Notation "A × B" (at level 75, right associativity).
Reserved Notation "a --> b" (at level 55).
Reserved Notation "! p " (at level 50, left associativity).
Reserved Notation "X ⨿ Y" (at level 50, left associativity).
Reserved Notation "x ,, y" (at level 60, right associativity).
Ltac simple_rapply p :=
simple refine p ||
simple refine (p _) ||
simple refine (p _ _) ||
simple refine (p _ _ _) ||
simple refine (p _ _ _ _) ||
simple refine (p _ _ _ _ _) ||
simple refine (p _ _ _ _ _ _) ||
simple refine (p _ _ _ _ _ _ _) ||
simple refine (p _ _ _ _ _ _ _ _) ||
simple refine (p _ _ _ _ _ _ _ _ _) ||
simple refine (p _ _ _ _ _ _ _ _ _ _) ||
simple refine (p _ _ _ _ _ _ _ _ _ _ _) ||
simple refine (p _ _ _ _ _ _ _ _ _ _ _ _) ||
simple refine (p _ _ _ _ _ _ _ _ _ _ _ _ _) ||
simple refine (p _ _ _ _ _ _ _ _ _ _ _ _ _ _) ||
simple refine (p _ _ _ _ _ _ _ _ _ _ _ _ _ _ _).
Tactic Notation "use" uconstr(p) := simple_rapply p.
Definition UU := Type.
Identity Coercion fromUUtoType : UU >-> Sortclass.
Inductive unit : UU :=
tt : unit.
Inductive coprod (A B:UU) : UU :=
| ii1 : A -> coprod A B
| ii2 : B -> coprod A B.
Arguments ii1 {_ _} _.
Arguments ii2 {_ _} _.
Notation inl := ii1.
Notation inr := ii2.
Notation "X ⨿ Y" := (coprod X Y).
Inductive nat : UU :=
| O : nat
| S : nat -> nat.
Open Scope nat_scope.
Fixpoint add n m :=
match n with
| O => m
| S p => S (p + m)
end
where "n + m" := (add n m) : nat_scope.
Notation "0" := (O) : nat_scope.
Notation "1" := (S 0) : nat_scope.
Inductive paths {A:UU} (a:A) : A -> UU := paths_refl : paths a a.
Notation "a = b" := (paths a b) : type_scope.
Record total2 { T: UU } ( P: T -> UU ) := tpair { pr1 : T; pr2 : P pr1 }.
Arguments tpair {_} _ _ _.
Arguments pr1 {_ _} _.
Arguments pr2 {_ _} _.
Notation "'∑' x .. y , P" := (total2 (λ x, .. (total2 (λ y, P)) ..))
(at level 200, x binder, y binder, right associativity) : type_scope.
Notation "x ,, y" := (tpair _ x y).
Definition idfun (T : UU) := λ t:T, t.
Definition funcomp {X Y : UU} {Z:Y->UU} (f : X -> Y) (g : ∏ y:Y, Z y) := λ x, g (f x).
Definition dirprod (X Y : UU) := ∑ x:X, Y.
Notation "A × B" := (dirprod A B) : type_scope.
Definition make_dirprod {X Y : UU} (x:X) (y:Y) : X × Y.
Admitted.
Definition pathscomp0 {X : UU} {a b c : X} (e1 : a = b) (e2 : b = c) : a = c.
Admitted.
Notation "p @ q" := (pathscomp0 p q).
Definition pathsinv0 {X : UU} {a b : X} (e : a = b) : b = a.
Admitted.
Notation "! p " := (pathsinv0 p).
Definition maponpaths {T1 T2 : UU} (f : T1 -> T2) {t1 t2 : T1}
(e: t1 = t2) : f t1 = f t2.
Admitted.
Definition homot {X : UU} {P : X -> UU} (f g : ∏ x : X, P x) := ∏ x : X , f x = g x.
Notation "f ~ g" := (homot f g).
Definition isweq {X Y : UU} (f : X -> Y) : UU.
Admitted.
Definition weq (X Y : UU) : UU.
exact (∑ f:X->Y, isweq f).
Defined.
Notation "X ≃ Y" := (weq X%type Y%type) : type_scope.
Definition pr1weq {X Y : UU} := pr1 : X ≃ Y -> (X -> Y).
Coercion pr1weq : weq >-> Funclass.
Fixpoint isofhlevel (n : nat) (X : UU) : UU.
Admitted.
Definition isaprop := isofhlevel 1.
Definition funextsecStatement :=
∏ (T:UU) (P:T -> UU) (f g :∏ t:T, P t), f ~ g -> f = g.
Definition funextfunStatement :=
∏ (X Y:UU) (f g : X -> Y), f ~ g -> f = g.
Theorem funextfunImplication : funextsecStatement -> funextfunStatement.
Admitted.
Definition funextsec : funextsecStatement.
Admitted.
Definition funextfun := funextfunImplication (@funextsec).
Definition hProp := total2 (λ X : UU, isaprop X).
Definition hProptoType := @pr1 _ _ : hProp -> UU.
Coercion hProptoType : hProp >-> UU.
Definition hSet : UU.
Admitted.
Definition pr1hSet : hSet -> UU.
Admitted.
Coercion pr1hSet: hSet >-> UU.
Definition natgth (n m : nat) : hProp.
Admitted.
Notation " x > y " := (natgth x y) : nat_scope.
Definition natlth (n m : nat) := m > n.
Notation " x < y " := (natlth x y) : nat_scope.
Definition stn ( n : nat ) := ∑ m, m < n.
Notation "⟦ n ⟧" := (stn n) : stn.
Definition stnweq {n : nat}
: stn n ⨿ unit ≃ stn (1 + n).
Admitted.
Definition extend_tuple
{T : UU}
{n : nat}
(f : stn n → T)
(last : T)
: stn (S n) → T.
Admitted.
Lemma extend_tuple_inl
{T : UU}
{n : nat}
(f : stn n → T)
(last : T)
(i : stn n)
: extend_tuple f last (stnweq (inl i)) = f i.
Admitted.
Lemma extend_tuple_inr
{T : UU}
{n : nat}
(f : stn n → T)
(last : T)
(t : unit)
: extend_tuple f last (stnweq (inr t)) = last.
Admitted.
Definition precategory_ob_mor : UU.
exact (∑ ob : UU, ob -> ob -> UU).
Defined.
Definition make_precategory_ob_mor (ob : UU)(mor : ob -> ob -> UU) :
precategory_ob_mor.
exact (tpair _ ob mor).
Defined.
Definition ob (C : precategory_ob_mor) : UU.
exact (@pr1 _ _ C).
Defined.
Coercion ob : precategory_ob_mor >-> UU.
Definition precategory_morphisms { C : precategory_ob_mor } :
C -> C -> UU.
exact (pr2 C).
Defined.
Declare Scope cat.
Local Open Scope cat.
Notation "a --> b" := (precategory_morphisms a b) : cat.
Definition precategory_id_comp (C : precategory_ob_mor) : UU.
exact ((∏ c : C, c --> c)
×
(∏ a b c : C, a --> b -> b --> c -> a --> c)).
Defined.
Definition precategory_data : UU.
exact (∑ C : precategory_ob_mor, precategory_id_comp C).
Defined.
Definition make_precategory_data (C : precategory_ob_mor)
(id : ∏ c : C, c --> c)
(comp: ∏ a b c : C, a --> b -> b --> c -> a --> c)
: precategory_data.
exact (tpair _ C (make_dirprod id comp)).
Defined.
Definition precategory_ob_mor_from_precategory_data (C : precategory_data) :
precategory_ob_mor.
exact (pr1 C).
Defined.
Coercion precategory_ob_mor_from_precategory_data :
precategory_data >-> precategory_ob_mor.
Definition is_precategory (C : precategory_data) : UU.
Admitted.
Definition precategory := total2 is_precategory.
Definition make_precategory (C : precategory_data) (H : is_precategory C)
: precategory.
exact (tpair _ C H).
Defined.
Definition precategory_data_from_precategory (C : precategory) :
precategory_data.
exact (pr1 C).
Defined.
Coercion precategory_data_from_precategory : precategory >-> precategory_data.
Definition has_homsets (C : precategory_ob_mor) : UU.
Admitted.
Definition category := ∑ C:precategory, has_homsets C.
Definition make_category C h : category := C,,h.
Definition category_to_precategory : category -> precategory.
exact (pr1).
Defined.
Coercion category_to_precategory : category >-> precategory.
Section IndexedSetCategory.
Context (I : UU).
Definition indexed_set_cat
: category.
Proof.
use make_category.
-
use make_precategory.
+
use make_precategory_data.
*
use make_precategory_ob_mor.
--
exact (I → hSet).
--
intros X Y.
exact (∏ i, X i → Y i).
*
intros X i.
apply idfun.
*
intros X Y Z f g i.
exact (funcomp (f i) (g i)).
+
admit.
-
admit.
Defined.
End IndexedSetCategory.
Definition var_ax
(T : indexed_set_cat nat)
(n : nat)
(i : stn n)
: UU.
exact (T n).
Defined.
Definition subst_ax
(T : indexed_set_cat nat)
(m n : nat)
(f : T m)
(g : stn m → T n)
: UU.
exact (T n).
Defined.
Declare Scope algebraic_theories.
Local Open Scope algebraic_theories.
Definition algebraic_theory_data : UU.
Admitted.
Definition algebraic_theory_data_to_function
(T : algebraic_theory_data)
: nat → hSet.
Admitted.
Coercion algebraic_theory_data_to_function : algebraic_theory_data >-> Funclass.
Definition var
{T : algebraic_theory_data}
{n : nat}
(i : stn n)
: var_ax T n i.
Admitted.
Definition subst
{T : algebraic_theory_data}
{m n : nat}
(f : T m)
(g : stn m → T n)
: subst_ax T m n f g.
admit.
Defined.
Notation "f • g" :=
(subst f g)
(at level 35) : algebraic_theories.
Definition algebraic_theory : UU.
Admitted.
Coercion algebraic_theory_to_algebraic_theory_data (T : algebraic_theory)
: algebraic_theory_data.
Admitted.
Definition var_subst_ax
(T : algebraic_theory_data)
(m n : nat)
(i : stn m)
(f : stn m → T n)
: UU.
exact (var i • f = f i).
Defined.
Definition var_subst
(T : algebraic_theory)
{m n : nat}
(i : stn m)
(f : stn m → T n)
: var_subst_ax (T : algebraic_theory_data) m n i f.
Admitted.
Definition inflate {T : algebraic_theory_data} {n : nat} (f : T n) : T (S n).
Admitted.
Definition inflate_subst (T : algebraic_theory) {m n : nat} (f : T m) (g : stn m → T n)
: inflate (subst f g) = subst f (λ i, inflate (g i)).
Admitted.
Lemma subst_inflate (T : algebraic_theory) {m n : nat} (f : T m) (g : stn (S m) → T n)
: subst (inflate f) g = subst f (λ i, g (stnweq (inl i))).
Admitted.
Definition app_ax
(T : algebraic_theory)
(n : nat)
(f : T n)
: UU.
exact (T (S n)).
Defined.
Definition abs_ax
(T : algebraic_theory)
(n : nat)
(f : T (S n))
: UU.
exact (T n).
Defined.
Definition lambda_theory_data : UU.
Admitted.
Coercion lambda_theory_data_to_algebraic_theory (L : lambda_theory_data)
: algebraic_theory.
Admitted.
Definition appx {L : lambda_theory_data} {n : nat} (f : L n) : app_ax L n f.
Admitted.
Definition abs {L : lambda_theory_data} {n : nat} (f : L (S n)) : abs_ax L n f.
Admitted.
Definition lambda_theory : UU.
Admitted.
Coercion lambda_theory_to_lambda_theory_data (L : lambda_theory) : lambda_theory_data.
Admitted.
Definition subst_abs (L : lambda_theory) {m n : nat} (f : L (S m)) (g : stn m → L n)
: subst (abs f) g = abs (subst f (extend_tuple (λ i, inflate (g i)) (var (stnweq (inr tt))))).
Admitted.
Definition app {L : lambda_theory_data} {n : nat} (f g : L n) : L n.
exact (appx f • extend_tuple var g).
Defined.
Lemma subst_app (L : lambda_theory) {m n : nat} (f g : L m) (h : stn m → L n)
: subst (app f g) h = app (subst f h) (subst g h).
Admitted.
Notation "( a b )" := (app a b) (only printing) : lambda_calculus.
Notation "(λ' n , x )" := (@abs _ n x) (only printing) : lambda_calculus.
Export Ltac2.Init.
Export Ltac2.Notations.
Local Open Scope stn.
Local Open Scope lambda_calculus.
Definition compose
{L : lambda_theory}
{n : nat}
(a b : L n)
: L n.
exact (abs
(app
(inflate a)
(app
(inflate b)
(var (stnweq (inr tt)))))).
Defined.
Notation "a ∘ b" :=
(compose a b)
(at level 40, left associativity)
: lambda_calculus.
Lemma subst_compose
(L : lambda_theory)
{m n : nat}
(a b : L m)
(c : stn m → L n)
: subst (a ∘ b) c = compose (subst a c) (subst b c).
Proof.
refine '(subst_abs _ _ _ @ _).
refine '(maponpaths (λ x, (abs x)) (subst_app _ _ _ _) @ _).
refine '(maponpaths (λ x, (abs (app x _))) (subst_inflate _ _ _) @ _).
refine '(maponpaths (λ x, (abs (app _ x))) (subst_app _ _ _ _) @ _).
refine '(maponpaths (λ x, (abs (app _ (app x _)))) (subst_inflate _ _ _) @ _).
refine '(maponpaths (λ x, (abs (app _ (app _ x)))) (var_subst _ _ _) @ _).
refine '(maponpaths (λ x, (abs (app _ (app _ x)))) (extend_tuple_inr _ _ _) @ _).
refine '(_ @ !maponpaths (λ x, (abs (app x _))) (inflate_subst _ _ _)).
refine '(_ @ !maponpaths (λ x, (abs (app _ (app x _)))) (inflate_subst _ _ _)).
refine '(
maponpaths (λ x, abs (app (_ x) _)) _ @
maponpaths (λ x, abs (app _ (app (_ x) _))) _
);
apply funextfun;
intro i;
exact (extend_tuple_inl _ _ _).🛠️ Intermediate Coq File (useful for debugging if minimization did not go as far as you wanted) (truncated to 6.0KiB; full 22KiB file on GitHub Actions Artifacts under
|
Member
|
@Tragicus could you assess whether the minimized examples are legitimate changes in unification after your patch? Thanks. |
This comment was marked as outdated.
This comment was marked as outdated.
This comment was marked as outdated.
This comment was marked as outdated.
This comment was marked as outdated.
This comment was marked as outdated.
This comment was marked as outdated.
This comment was marked as outdated.
This comment was marked as outdated.
This comment was marked as outdated.
This comment was marked as outdated.
This comment was marked as outdated.
Member
|
bug minimizer should work on ci-iris now with rocq-community/run-coq-bug-minimizer@5b6d818: @coqbot ci minimize ci-iris |
This comment was marked as outdated.
This comment was marked as outdated.
This comment was marked as outdated.
This comment was marked as outdated.
This comment was marked as outdated.
This comment was marked as outdated.
This comment was marked as outdated.
This comment was marked as outdated.
This comment was marked as outdated.
This comment was marked as outdated.
JasonGross
added a commit
to rocq-community/run-coq-bug-minimizer
that referenced
this pull request
Nov 13, 2024
Member
|
hopefully third time's the charm: @coqbot ci minimize ci-iris |
Contributor
|
I am now running minimization at commit f592551 on requested target ci-iris. I'll come back to you with the results once it's done. |
Contributor
Author
|
It does not work either. |
8 tasks
Contributor
|
It seems that the iris issue is caused by |
coqbot-app
bot
added
the
needs: full CI
Contributor
Author
|
I added something in |
Member
This seems wrong (as you say?)? If we have (untested) Goal forall A : Prop, (exists x : A, True) /\ A.
simple refine (fun A => conj _ ?[a]).
epose _ as x.
exists x.
instantiate (1:=?a) in (value of x).the final line should not shelve the second goal. This should probably be true whether we go through instantiate or unification, though I'm not 100% sure about that. |
github-actions
bot
added
the
needs: rebase
…new one in `evarsolve/instantiate_evar`
coqbot-app
bot
removed
the
needs: rebase
Contributor
Author
|
I unconvinced myself that this is wrong, because I only shelve when I instantiate an evar with an (applied) evar. @JasonGross In your example, the final line does not shelve the second goal. |
Contributor
Author
|
Can I see the rest of the CI? |
Member
|
@coqbot run full ci |
coqbot-app
bot
removed
the
needs: full CI
This was referenced Apr 7, 2025
ppedrot
added
the
needs: progress
Contributor
|
You can reopen if you can make progress |
Contributor
Author
|
Things should be better now that #19987 is merged. Can we reopen (I do not seem to have the right to do it myself)? |
Member
|
I can't do that either, it's a github limitation. Seemingly you cannot reopen a PR if the branch has been pushed to another commit in the meantime. You should probably reopen a fresh one. |
Contributor
Author
|
I see, thank you. |
Member
|
If you force-push bbabba0 to the branch, you might then be able to reopen |
Contributor
Author
|
I reopened, we are losing a bit of discussion but this is not that much of a problem. But thank you anyway. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
4 participants
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.
The unification algorithm sometimes fails on problems of the form
?a = tbecause variables that are not in the scope of?aappear int. There are two cases where we can easily solve the problem, namely the one where the variable appears in a beta-redex, as in(fun _ => t) x, and the one where the variable appears in an argument of an evar, e.g.?b x, since we can instantiate the evar to forget the argument.For instance, unifying
forall x : ?T, f (?a x)andforall _ : ?T, ?breduces to unifyingf (?a x)and?b, which fails becausexis not available when instantiating?b.This PR adds these cases in
pretyping/evarsolve.Fixes / closes #????
make doc_gram_rsts.Overlays (to be merged before this)