diff options
Diffstat (limited to 'test-suite/bugs')
66 files changed, 1600 insertions, 33 deletions
diff --git a/test-suite/bugs/closed/2310.v b/test-suite/bugs/closed/2310.v index 0be859eddf..7fae328715 100644 --- a/test-suite/bugs/closed/2310.v +++ b/test-suite/bugs/closed/2310.v @@ -14,4 +14,8 @@ Definition replace a (y:Nest (prod a a)) : a = a -> Nest a. (P:=\a.Nest (prod a a) and P:=\_.Nest (prod a a)) and refine should either leave P as subgoal or choose itself one solution *) -intros. refine (Cons (cast H _ y)).
\ No newline at end of file + intros. Fail refine (Cons (cast H _ y)). + Unset Solve Unification Constraints. (* Keep the unification constraint around *) + refine (Cons (cast H _ y)). + intros. + refine (Nest (prod X X)). Qed.
\ No newline at end of file diff --git a/test-suite/bugs/closed/3045.v b/test-suite/bugs/closed/3045.v index ef110ad0d0..5f80013df2 100644 --- a/test-suite/bugs/closed/3045.v +++ b/test-suite/bugs/closed/3045.v @@ -12,7 +12,7 @@ Record SpecializedCategory (obj : Type) := Compose : forall s d d', Morphism d d' -> Morphism s d -> Morphism s d' }. -Arguments Compose {obj} [C s d d'] m1 m2 : rename. +Arguments Compose {obj} [C s d d'] _ _ : rename. Inductive ReifiedMorphism : forall objC (C : SpecializedCategory objC), C -> C -> Type := | ReifiedComposedMorphism : forall objC C s d d', ReifiedMorphism C d d' -> ReifiedMorphism C s d -> @ReifiedMorphism objC C s d'. diff --git a/test-suite/bugs/closed/3209.v b/test-suite/bugs/closed/3209.v new file mode 100644 index 0000000000..855058b011 --- /dev/null +++ b/test-suite/bugs/closed/3209.v @@ -0,0 +1,75 @@ +(* Avoiding some occur-check *) + +(* 1. Original example *) + +Inductive eqT {A} (x : A) : A -> Type := + reflT : eqT x x. +Definition Bi_inv (A B : Type) (f : (A -> B)) := + sigT (fun (g : B -> A) => + sigT (fun (h : B -> A) => + sigT (fun (α : forall b : B, eqT (f (g b)) b) => + forall a : A, eqT (h (f a)) a))). +Definition TEquiv (A B : Type) := sigT (fun (f : A -> B) => Bi_inv _ _ f). + +Axiom UA : forall (A B : Type), TEquiv (TEquiv A B) (eqT A B). +Definition idtoeqv {A B} (e : eqT A B) : TEquiv A B := + sigT_rect (fun _ => TEquiv A B) + (fun (f : TEquiv A B -> eqT A B) H => + sigT_rect _ (* (fun _ => TEquiv A B) *) + (fun g _ => g e) + H) + (UA A B). + +(* 2. Alternative example by Guillaume *) + +Inductive foo (A : Prop) : Prop := Foo : foo A. +Axiom bar : forall (A : Prop) (P : foo A -> Prop), (A -> P (Foo A)) -> Prop. + +(* This used to fail with a Not_found, we fail more graciously but a + heuristic could be implemented, e.g. in some smart occur-check + function, to find a solution of then form ?P := fun _ => ?P' *) + +Fail Check (fun e : ?[T] => bar ?[A] ?[P] (fun g : ?[A'] => g e)). + +(* This works and tells which solution we could have inferred *) + +Check (fun e : ?[T] => bar ?[A] (fun _ => ?[P]) (fun g : ?[A'] => g e)). + +(* For the record, here is the trace in the failing example: + +In (fun e : ?T => bar ?[A] ?[P] (fun g : ?A' => g e)), we have the existential variables + +e:?T |- ?A : Prop +e:?T |- ?P : foo ?A -> Prop +e:?T |- ?A' : Type + +with constraints + +?A' == ?A +?A' == ?T -> ?P (Foo ?A) + +To type (g e), unification first defines + +?A := forall x:?B, ?P'{e:=e,x:=x} +with ?T <= ?B +and ?P'@{e:=e,x:=e} <= ?P@{e:=e} (Foo (forall x:?B, ?P'{e:=e,x:=x})) + +Then, since ?P'@{e:=e,x:=e} may use "e" in two different ways, it is +not a pattern and we define a new + +e:?T x:?B|- ?P'' : foo (?B' -> ?P''') -> Prop + +for some ?B' and ?P''', together with + +?P'@{e,x} := ?P''{e:=e,x:=e} (Foo (?B -> ?P') +?P@{e} := ?P''{e:=e,x:=e} + +Moreover, ?B' and ?P''' have to satisfy + +?B'@{e:=e,x:=e} == ?B@{e:=e} +?P'''@{e:=e,x:=e} == ?P'@{e:=e,x:=x} + +and this leads to define ?P' which was the initial existential +variable to define. +*) + diff --git a/test-suite/bugs/closed/3441.v b/test-suite/bugs/closed/3441.v new file mode 100644 index 0000000000..50d2978077 --- /dev/null +++ b/test-suite/bugs/closed/3441.v @@ -0,0 +1,23 @@ +Axiom f : nat -> nat -> nat. +Fixpoint do_n (n : nat) (k : nat) := + match n with + | 0 => k + | S n' => do_n n' (f k k) + end. + +Notation big := (_ = _). +Axiom k : nat. +Goal True. +Timeout 1 let H := fresh "H" in + let x := constr:(let n := 17 in do_n n = do_n n) in + let y := (eval lazy in x) in + pose proof y as H. (* Finished transaction in 1.102 secs (1.084u,0.016s) (successful) *) +Timeout 1 let H := fresh "H" in + let x := constr:(let n := 17 in do_n n = do_n n) in + let y := (eval lazy in x) in + pose y as H; clearbody H. (* Finished transaction in 0.412 secs (0.412u,0.s) (successful) *) + +Timeout 1 Time let H := fresh "H" in + let x := constr:(let n := 17 in do_n n = do_n n) in + let y := (eval lazy in x) in + assert (H := y). (* Finished transaction in 1.19 secs (1.164u,0.024s) (successful) *)
\ No newline at end of file diff --git a/test-suite/bugs/closed/3495.v b/test-suite/bugs/closed/3495.v new file mode 100644 index 0000000000..102a2aba0d --- /dev/null +++ b/test-suite/bugs/closed/3495.v @@ -0,0 +1,18 @@ +Require Import RelationClasses. + +Axiom R : Prop -> Prop -> Prop. +Declare Instance : Reflexive R. + +Class bar := { x : False }. +Record foo := { a : Prop ; b : bar }. + +Definition default_foo (a0 : Prop) `{b : bar} : foo := {| a := a0 ; b := b |}. + +Goal exists k, R k True. +Proof. +eexists. +evar (b : bar). +let e := match goal with |- R ?e _ => constr:(e) end in +unify e (a (default_foo True)). +subst b. +reflexivity. diff --git a/test-suite/bugs/closed/3513.v b/test-suite/bugs/closed/3513.v index fcdfa0057b..9ed0926a66 100644 --- a/test-suite/bugs/closed/3513.v +++ b/test-suite/bugs/closed/3513.v @@ -1,4 +1,3 @@ -Require Import TestSuite.admit. (* File reduced by coq-bug-finder from original input, then from 5752 lines to 3828 lines, then from 2707 lines to 558 lines, then from 472 lines to 168 lines, then from 110 lines to 101 lines, then from 96 lines to 77 lines, then from 80 lines to 64 lines *) Require Coq.Setoids.Setoid. Import Coq.Setoids.Setoid. @@ -35,7 +34,7 @@ Local Existing Instance ILFun_Ops. Local Existing Instance ILFun_ILogic. Definition catOP (P Q: OPred) : OPred := admit. Add Parametric Morphism : catOP with signature lentails ==> lentails ==> lentails as catOP_entails_m. -admit. +apply admit. Defined. Definition catOPA (P Q R : OPred) : catOP (catOP P Q) R -|- catOP P (catOP Q R) := admit. Class IsPointed (T : Type) := point : T. @@ -69,8 +68,27 @@ Goal forall (T : Type) (O0 : T -> OPred) (O1 : T -> PointedOPred) pose P; refine (P _ _) end; unfold Basics.flip. - 2: solve [ apply reflexivity ]. - Undo. - 2: reflexivity. (* Toplevel input, characters 18-29: -Error: -Tactic failure: The relation lentails is not a declared reflexive relation. Maybe you need to require the Setoid library. *)
\ No newline at end of file + Focus 2. + Set Typeclasses Debug. + Set Typeclasses Legacy Resolution. + apply reflexivity. + (* Debug: 1.1: apply @IsPointed_catOP on +(IsPointed (exists x0 : Actions, (catOP ?Goal O2 : OPred) x0)) +Debug: 1.1.1.1: apply OPred_inhabited on (IsPointed (exists x0 : Actions, ?Goal x0)) +Debug: 1.1.2.1: apply OPred_inhabited on (IsPointed (exists x : Actions, O2 x)) +Debug: 2.1: apply @Equivalence_Reflexive on (Reflexive lentails) +Debug: 2.1.1: no match for (Equivalence lentails) , 5 possibilities +Debug: Backtracking after apply @Equivalence_Reflexive +Debug: 2.2: apply @PreOrder_Reflexive on (Reflexive lentails) +Debug: 2.2.1.1: apply @lentailsPre on (PreOrder lentails) +Debug: 2.2.1.1.1.1: apply ILFun_ILogic on (ILogic OPred) +*) + Undo. Unset Typeclasses Legacy Resolution. + Test Typeclasses Unique Solutions. + Test Typeclasses Unique Instances. + Show Existentials. + Set Typeclasses Debug Verbosity 2. + Set Printing All. + (* As in 8.5, allow a shelved subgoal to remain *) + apply reflexivity. +
\ No newline at end of file diff --git a/test-suite/bugs/closed/3647.v b/test-suite/bugs/closed/3647.v index 495e67e09e..f5a22bd508 100644 --- a/test-suite/bugs/closed/3647.v +++ b/test-suite/bugs/closed/3647.v @@ -650,4 +650,5 @@ Goal forall (ptest : program) (cond : Condition) (value : bool) Grab Existential Variables. subst_body; simpl. - refine (all_behead (projT2 _)). + Fail refine (all_behead (projT2 _)). + Unset Solve Unification Constraints. refine (all_behead (projT2 _)). diff --git a/test-suite/bugs/closed/3699.v b/test-suite/bugs/closed/3699.v index 8dadc2419c..efa4325264 100644 --- a/test-suite/bugs/closed/3699.v +++ b/test-suite/bugs/closed/3699.v @@ -34,8 +34,7 @@ Module NonPrim. : forall b:B, P b. Proof. intros b. - unshelve (refine (pr1 (isconnected_elim _ _))). - exact b. + unshelve (refine (pr1 (isconnected_elim (A:=hfiber f b) _ _))). intro x. exact (transport P x.2 (d x.1)). Defined. @@ -47,8 +46,7 @@ Module NonPrim. : forall b:B, P b. Proof. intros b. - unshelve (refine (pr1 (isconnected_elim _ _))). - exact b. + unshelve (refine (pr1 (isconnected_elim (A:=hfiber f b) _ _))). intros [a p]. exact (transport P p (d a)). Defined. @@ -111,8 +109,7 @@ Module Prim. : forall b:B, P b. Proof. intros b. - unshelve (refine (pr1 (isconnected_elim _ _))). - exact b. + unshelve (refine (pr1 (isconnected_elim (A:=hfiber f b) _ _))). intro x. exact (transport P x.2 (d x.1)). Defined. @@ -124,8 +121,7 @@ Module Prim. : forall b:B, P b. Proof. intros b. - unshelve (refine (pr1 (isconnected_elim _ _))). - exact b. + unshelve (refine (pr1 (isconnected_elim (A:=hfiber f b) _ _))). intros [a p]. exact (transport P p (d a)). Defined. diff --git a/test-suite/bugs/opened/3753.v b/test-suite/bugs/closed/3753.v index 05d77c831b..5bfbee9494 100644 --- a/test-suite/bugs/opened/3753.v +++ b/test-suite/bugs/closed/3753.v @@ -1,4 +1,4 @@ Axiom foo : Type -> Type. Axiom bar : forall (T : Type), T -> foo T. Arguments bar A x : rename. -Fail About bar. +About bar.
\ No newline at end of file diff --git a/test-suite/bugs/closed/4095.v b/test-suite/bugs/closed/4095.v new file mode 100644 index 0000000000..ffd33d3813 --- /dev/null +++ b/test-suite/bugs/closed/4095.v @@ -0,0 +1,87 @@ +(* File reduced by coq-bug-finder from original input, then from 5752 lines to 3828 lines, then from 2707 lines to 558 lines, then from 472 lines to 168 lines, then from 110 lines to 101 lines, then from 96 lines to 77 lines, then from 80 lines to 64 lines, then from 92 lines to 79 lines *) +(* coqc version 8.5beta1 (February 2015) compiled on Feb 23 2015 18:32:3 with OCaml 4.01.0 + coqtop version cagnode15:/afs/csail.mit.edu/u/j/jgross/coq-8.5,v8.5 (ebfc19d792492417b129063fb511aa423e9d9e08) *) +Require Import Coq.Setoids.Setoid. +Generalizable All Variables. +Axiom admit : forall {T}, T. +Ltac admit := apply admit. +Class Equiv (A : Type) := equiv : relation A. +Class type (A : Type) {e : Equiv A} := eq_equiv : Equivalence equiv. +Class ILogicOps Frm := { lentails: relation Frm; + ltrue: Frm; + land: Frm -> Frm -> Frm; + lor: Frm -> Frm -> Frm }. +Infix "|--" := lentails (at level 79, no associativity). +Class ILogic Frm {ILOps: ILogicOps Frm} := { lentailsPre:> PreOrder lentails }. +Definition lequiv `{ILogic Frm} P Q := P |-- Q /\ Q |-- P. +Infix "-|-" := lequiv (at level 85, no associativity). +Instance lequiv_inverse_lentails `{ILogic Frm} : subrelation lequiv (inverse lentails) := admit. +Record ILFunFrm (T : Type) `{e : Equiv T} `{ILOps : ILogicOps Frm} := mkILFunFrm { ILFunFrm_pred :> T -> Frm }. +Section ILogic_Fun. + Context (T: Type) `{TType: type T}. + Context `{IL: ILogic Frm}. + Local Instance ILFun_Ops : ILogicOps (@ILFunFrm T _ Frm _) := admit. + Definition ILFun_ILogic : ILogic (@ILFunFrm T _ Frm _) := admit. +End ILogic_Fun. +Implicit Arguments ILFunFrm [[ILOps] [e]]. +Instance ILogicOps_Prop : ILogicOps Prop | 2 := {| lentails P Q := (P : Prop) -> Q; + ltrue := True; + land P Q := P /\ Q; + lor P Q := P \/ Q |}. +Axiom Action : Set. +Definition Actions := list Action. +Instance ActionsEquiv : Equiv Actions := { equiv a1 a2 := a1 = a2 }. +Definition OPred := ILFunFrm Actions Prop. +Local Existing Instance ILFun_Ops. +Local Existing Instance ILFun_ILogic. +Definition catOP (P Q: OPred) : OPred := admit. +Add Parametric Morphism : catOP with signature lentails ==> lentails ==> lentails as catOP_entails_m. +admit. +Defined. +Definition catOPA (P Q R : OPred) : catOP (catOP P Q) R -|- catOP P (catOP Q R) := admit. +Class IsPointed (T : Type) := point : T. +Notation IsPointed_OPred P := (IsPointed (exists x : Actions, (P : OPred) x)). +Record PointedOPred := mkPointedOPred { + OPred_pred :> OPred; + OPred_inhabited: IsPointed_OPred OPred_pred + }. +Existing Instance OPred_inhabited. +Canonical Structure default_PointedOPred O `{IsPointed_OPred O} : PointedOPred + := {| OPred_pred := O ; OPred_inhabited := _ |}. +Instance IsPointed_catOP `{IsPointed_OPred P, IsPointed_OPred Q} : IsPointed_OPred (catOP P Q) := admit. +Goal forall (T : Type) (O0 : T -> OPred) (O1 : T -> PointedOPred) + (tr : T -> T) (O2 : PointedOPred) (x : T) + (H : forall x0 : T, catOP (O0 x0) (O1 (tr x0)) |-- O1 x0), + exists e1 e2, + catOP (O0 e1) (OPred_pred e2) |-- catOP (O1 x) O2. + intros; do 2 esplit. + rewrite <- catOPA. + lazymatch goal with + | |- ?R (?f ?a ?b) (?f ?a' ?b') => + let P := constr:(fun H H' => @Morphisms.proper_prf (OPred -> OPred -> OPred) + (@Morphisms.respectful OPred (OPred -> OPred) + (@lentails OPred + (@ILFun_Ops Actions ActionsEquiv Prop ILogicOps_Prop)) + (@lentails OPred + (@ILFun_Ops Actions ActionsEquiv Prop ILogicOps_Prop) ==> + @lentails OPred + (@ILFun_Ops Actions ActionsEquiv Prop ILogicOps_Prop))) catOP + catOP_entails_m_Proper a a' H b b' H') in + pose P; + refine (P _ _) + end. + Undo. + Fail lazymatch goal with + | |- ?R (?f ?a ?b) (?f ?a' ?b') => + let P := constr:(fun H H' => Morphisms.proper_prf a a' H b b' H') in + set(p:=P) + end. (* Toplevel input, characters 15-182: +Error: Cannot infer an instance of type +"PointedOPred" for the variable p in environment: +T : Type +O0 : T -> OPred +O1 : T -> PointedOPred +tr : T -> T +O2 : PointedOPred +x0 : T +H : forall x0 : T, catOP (O0 x0) (O1 (tr x0)) |-- O1 x0 *)
\ No newline at end of file diff --git a/test-suite/bugs/closed/4416.v b/test-suite/bugs/closed/4416.v new file mode 100644 index 0000000000..3189685ec0 --- /dev/null +++ b/test-suite/bugs/closed/4416.v @@ -0,0 +1,4 @@ +Goal exists x, x. +Unset Solve Unification Constraints. +unshelve refine (ex_intro _ _ _); match goal with _ => refine (_ _) end. +(* Error: Incorrect number of goals (expected 2 tactics). *)
\ No newline at end of file diff --git a/test-suite/bugs/closed/4464.v b/test-suite/bugs/closed/4464.v new file mode 100644 index 0000000000..f8e9405d93 --- /dev/null +++ b/test-suite/bugs/closed/4464.v @@ -0,0 +1,4 @@ +Goal True -> True. +Proof. + intro H'. + let H := H' in destruct H; try destruct H. diff --git a/test-suite/bugs/closed/4471.v b/test-suite/bugs/closed/4471.v new file mode 100644 index 0000000000..36efc42d47 --- /dev/null +++ b/test-suite/bugs/closed/4471.v @@ -0,0 +1,6 @@ +Goal forall (A B : Type) (P : forall _ : prod A B, Type) (a : A) (b : B) (p p0 : forall (x : A) (x' : B), P (@pair A B x x')), + @eq (P (@pair A B a b)) (p (@fst A B (@pair A B a b)) (@snd A B (@pair A B a b))) + (p0 (@fst A B (@pair A B a b)) (@snd A B (@pair A B a b))). +Proof. + intros. + Fail generalize dependent (a, b). diff --git a/test-suite/bugs/closed/4527.v b/test-suite/bugs/closed/4527.v index 4ca6fe78cd..08628377f0 100644 --- a/test-suite/bugs/closed/4527.v +++ b/test-suite/bugs/closed/4527.v @@ -249,10 +249,10 @@ Section Reflective_Subuniverse. exact H. Defined. - Definition inO_paths@{i j} (S : Type@{i}) {S_inO : In@{Ou Oa i} O S} (x y : + Definition inO_paths@{i} (S : Type@{i}) {S_inO : In@{Ou Oa i} O S} (x y : S) : In@{Ou Oa i} O (x=y). Proof. - simple refine (inO_to_O_retract@{i j} _ _ _); intro u. + simple refine (inO_to_O_retract@{i} _ _ _); intro u. - assert (p : (fun _ : O (x=y) => x) == (fun _=> y)). { @@ -264,4 +264,4 @@ S) : In@{Ou Oa i} O (x=y). hnf. rewrite O_indpaths_beta; reflexivity. Qed. - Check inO_paths@{Type Type}. + Check inO_paths@{Type}. diff --git a/test-suite/bugs/closed/4529.v b/test-suite/bugs/closed/4529.v new file mode 100644 index 0000000000..8b3c24fec6 --- /dev/null +++ b/test-suite/bugs/closed/4529.v @@ -0,0 +1,45 @@ +(* File reduced by coq-bug-finder from original input, then from 1334 lines to 1518 lines, then from 849 lines to 59 lines *) +(* coqc version 8.5 (January 2016) compiled on Jan 22 2016 18:20:47 with OCaml 4.02.3 + coqtop version r-schnelltop:/home/r/src/coq/coq,(HEAD detached at V8.5) (5e23fb90b39dfa014ae5c4fb46eb713cca09dbff) *) +Require Coq.Setoids.Setoid. +Import Coq.Setoids.Setoid. + +Class Equiv A := equiv: relation A. +Infix "≡" := equiv (at level 70, no associativity). +Notation "(≡)" := equiv (only parsing). + +(* If I remove this line, everything compiles. *) +Set Primitive Projections. + +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"). + +Record CofeMixin A `{Equiv A, Dist A} := { + mixin_equiv_dist x y : x ≡ y <-> forall n, x ={n}= y; + mixin_dist_equivalence n : Equivalence (dist n); +}. + +Structure cofeT := CofeT { + cofe_car :> Type; + cofe_equiv : Equiv cofe_car; + cofe_dist : Dist cofe_car; + cofe_mixin : CofeMixin cofe_car +}. +Existing Instances cofe_equiv cofe_dist. +Arguments cofe_car : simpl never. + +Section cofe_mixin. + Context {A : cofeT}. + Implicit Types x y : A. + Lemma equiv_dist x y : x ≡ y <-> forall n, x ={n}= y. +Admitted. +End cofe_mixin. + Context {A : cofeT}. + Global Instance cofe_equivalence : Equivalence ((≡) : relation A). + Proof. + split. + * + intros x. +apply equiv_dist. + diff --git a/test-suite/bugs/closed/4544.v b/test-suite/bugs/closed/4544.v index 048f31ce3d..da140c9318 100644 --- a/test-suite/bugs/closed/4544.v +++ b/test-suite/bugs/closed/4544.v @@ -652,7 +652,7 @@ Defined. Definition ReflectiveSubuniverse := Modality. - Definition O_reflector := O_reflector. + Definition O_reflector@{u a i} := O_reflector@{u a i}. Definition In@{u a i} : forall (O : ReflectiveSubuniverse@{u a}), Type2le@{i a} -> Type2le@{i a} @@ -660,7 +660,7 @@ Defined. Definition O_inO@{u a i} : forall (O : ReflectiveSubuniverse@{u a}) (T : Type@{i}), In@{u a i} O (O_reflector@{u a i} O T) := O_inO@{u a i}. - Definition to := to. + Definition to@{u a i} := to@{u a i}. Definition inO_equiv_inO@{u a i j k} : forall (O : ReflectiveSubuniverse@{u a}) (T : Type@{i}) (U : Type@{j}) (T_inO : In@{u a i} O T) (f : T -> U) (feq : IsEquiv f), diff --git a/test-suite/bugs/closed/4661.v b/test-suite/bugs/closed/4661.v new file mode 100644 index 0000000000..03d2350a69 --- /dev/null +++ b/test-suite/bugs/closed/4661.v @@ -0,0 +1,10 @@ +Module Type Test. + Parameter t : Type. +End Test. + +Module Type Func (T:Test). + Parameter x : Type. +End Func. + +Module Shortest_path (T : Test). +Print Func. diff --git a/test-suite/bugs/closed/4708.v b/test-suite/bugs/closed/4708.v new file mode 100644 index 0000000000..ad2e581004 --- /dev/null +++ b/test-suite/bugs/closed/4708.v @@ -0,0 +1,8 @@ +(*Doc, it hurts when I poke myself.*) + +Notation "'" := 1. (* was: +Setting notation at level 0. +Toplevel input, characters 0-18: +> Notation "'" := 1. +> ^^^^^^^^^^^^^^^^^^ +Anomaly: Uncaught exception Invalid_argument("index out of bounds"). Please report. *) diff --git a/test-suite/bugs/closed/4718.v b/test-suite/bugs/closed/4718.v new file mode 100644 index 0000000000..12a4e8fc1a --- /dev/null +++ b/test-suite/bugs/closed/4718.v @@ -0,0 +1,15 @@ +(*Congruence is weaker than reflexivity when it comes to higher level than necessary equalities:*) + +Goal @eq Set nat nat. +congruence. +Qed. + +Goal @eq Type nat nat. +congruence. (*bug*) +Qed. + +Variable T : Type. + +Goal @eq Type T T. +congruence. +Qed. diff --git a/test-suite/bugs/closed/4722.v b/test-suite/bugs/closed/4722.v new file mode 100644 index 0000000000..f047624c84 --- /dev/null +++ b/test-suite/bugs/closed/4722.v @@ -0,0 +1 @@ +(* -*- coq-prog-args: ("-emacs" "-R" "4722" "Foo") -*- *) diff --git a/test-suite/bugs/closed/4722/tata b/test-suite/bugs/closed/4722/tata new file mode 120000 index 0000000000..b38e66e75f --- /dev/null +++ b/test-suite/bugs/closed/4722/tata @@ -0,0 +1 @@ +toto
\ No newline at end of file diff --git a/test-suite/bugs/closed/4723.v b/test-suite/bugs/closed/4723.v new file mode 100644 index 0000000000..8884812102 --- /dev/null +++ b/test-suite/bugs/closed/4723.v @@ -0,0 +1,28 @@ + +Require Coq.Program.Tactics. + +Record Matrix (m n : nat). + +Definition kp {m n p q: nat} (A: Matrix m n) (B: Matrix p q): + Matrix (m*p) (n*q). Admitted. + +Fail Program Fact kp_assoc + (xr xc yr yc zr zc: nat) + (x: Matrix xr xc) (y: Matrix yr yc) (z: Matrix zr zc): + kp x (kp y z) = kp (kp x y) z. + +Ltac Obligation Tactic := admit. +Fail Program Fact kp_assoc + (xr xc yr yc zr zc: nat) + (x: Matrix xr xc) (y: Matrix yr yc) (z: Matrix zr zc): + kp x (kp y z) = kp (kp x y) z. + +Axiom cheat : forall {A}, A. +Obligation Tactic := apply cheat. + +Program Fact kp_assoc + (xr xc yr yc zr zc: nat) + (x: Matrix xr xc) (y: Matrix yr yc) (z: Matrix zr zc): + kp x (kp y z) = kp (kp x y) z. +admit. +Admitted.
\ No newline at end of file diff --git a/test-suite/bugs/closed/4727.v b/test-suite/bugs/closed/4727.v new file mode 100644 index 0000000000..3854bbffdd --- /dev/null +++ b/test-suite/bugs/closed/4727.v @@ -0,0 +1,10 @@ +(* -*- coq-prog-args: ("-emacs" "-compat" "8.4") -*- *) +Goal forall (P : Set) (l : P) (P0 : Set) (w w0 : P0) (T : Type) (a : P * T) (o : P -> option P0), + (forall (l1 l2 : P) (w1 : P0), o l1 = Some w1 -> o l2 = Some w1 -> l1 = l2) -> + o l = Some w -> o (fst a) = Some w0 -> {w = w0} + {w <> w0} -> False. +Proof. + clear; intros ???????? inj H0 H1 H2. + destruct H2; intuition subst. + eapply inj in H1; [ | eauto ]. + progress subst. (* should succeed, used to not succeed *) +Abort. diff --git a/test-suite/bugs/closed/4733.v b/test-suite/bugs/closed/4733.v index ac0653492a..a6ebda61cf 100644 --- a/test-suite/bugs/closed/4733.v +++ b/test-suite/bugs/closed/4733.v @@ -25,16 +25,16 @@ Check [ _ ]%list : list _. Check [ _ ]%vector : Vector.t _ _. Check [ _ ; _ ]%list : list _. Check [ _ ; _ ]%vector : Vector.t _ _. -Fail Check [ _ ; _ ]%mylist : mylist _. (* ideally, this should work, but that requires removing notations from the parser *) +Check [ _ ; _ ]%mylist : mylist _. Check [ _ ; _ ; _ ]%list : list _. Check [ _ ; _ ; _ ]%vector : Vector.t _ _. -Fail Check [ _ ; _ ; _ ]%mylist : mylist _. (* ideally, this should work, but that requires removing notations from the parser *) +Check [ _ ; _ ; _ ]%mylist : mylist _. Check [ _ ; _ ; _ ; _ ]%list : list _. Check [ _ ; _ ; _ ; _ ]%vector : Vector.t _ _. -Fail Check [ _ ; _ ; _ ; _ ]%mylist : mylist _. (* ideally, this should work, but that requires removing notations from the parser *) +Check [ _ ; _ ; _ ; _ ]%mylist : mylist _. Notation " [ x ; y ; .. ; z ] " := (mycons x (mycons y .. (mycons z mynil) ..)) : mylist_scope. -(* Now these all work, but not so in 8.4. If we get the ability to remove notations, and the above fails can be removed, this section can also just be removed. *) +(* Now these all work, but not so in 8.4. If we get the ability to remove notations, this section can also just be removed. *) Check [ ]%mylist : mylist _. Check [ ]%list : list _. Check []%vector : Vector.t _ _. diff --git a/test-suite/bugs/closed/4745.v b/test-suite/bugs/closed/4745.v new file mode 100644 index 0000000000..c090125e64 --- /dev/null +++ b/test-suite/bugs/closed/4745.v @@ -0,0 +1,35 @@ +(*I get an Anomaly in the following code. + +```*) +Require Vector. + +Module M. + Lemma Vector_map_map : + forall A B C (f : A -> B) (g : B -> C) n (v : Vector.t A n), + Vector.map g (Vector.map f v) = Vector.map (fun a => g (f a)) v. + Proof. + induction v; simpl; auto using f_equal. + Qed. + + Lemma Vector_map_map_transparent : + forall A B C (f : A -> B) (g : B -> C) n (v : Vector.t A n), + Vector.map g (Vector.map f v) = Vector.map (fun a => g (f a)) v. + Proof. + induction v; simpl; auto using f_equal. + Defined. + (* Anomaly: constant not found in kind_of_head: Coq.Vectors.Vector.t_ind. Please report. *) + + (* strangely, explicitly passing the principle to induction works *) + Lemma Vector_map_map_transparent' : + forall A B C (f : A -> B) (g : B -> C) n (v : Vector.t A n), + Vector.map g (Vector.map f v) = Vector.map (fun a => g (f a)) v. + Proof. + induction v using Vector.t_ind; simpl; auto using f_equal. + Defined. +End M. +(*``` + +Changing any of the following things eliminates the Anomaly + * moving the lemma out of the module M to the top level + * proving the lemma as a Fixpoint instead of using induction + * proving the analogous lemma on lists instead of vectors*) diff --git a/test-suite/bugs/closed/4762.v b/test-suite/bugs/closed/4762.v new file mode 100644 index 0000000000..7a87b07a8e --- /dev/null +++ b/test-suite/bugs/closed/4762.v @@ -0,0 +1,24 @@ +Inductive myand (P Q : Prop) := myconj : P -> Q -> myand P Q. + +Lemma foo P Q R : R = myand P Q -> P -> Q -> R. +Proof. intros ->; constructor; auto. Qed. + +Hint Extern 0 (myand _ _) => eapply foo; [reflexivity| |] : test1. + +Goal forall P Q R : Prop, P -> Q -> R -> myand P (myand Q R). +Proof. + intros. + eauto with test1. +Qed. + +Hint Extern 0 => + match goal with + | |- myand _ _ => eapply foo; [reflexivity| |] + end : test2. + +Goal forall P Q R : Prop, P -> Q -> R -> myand P (myand Q R). +Proof. + intros. + eauto with test2. (* works *) +Qed. + diff --git a/test-suite/bugs/closed/4763.v b/test-suite/bugs/closed/4763.v new file mode 100644 index 0000000000..ae8ed0e6e8 --- /dev/null +++ b/test-suite/bugs/closed/4763.v @@ -0,0 +1,13 @@ +Require Import Coq.Arith.Arith Coq.Classes.Morphisms Coq.Classes.RelationClasses. +Coercion is_true : bool >-> Sortclass. +Global Instance: Transitive leb. +Admitted. + +Goal forall x y z, leb x y -> leb y z -> True. + intros ??? H H'. + lazymatch goal with + | [ H : is_true (?R ?x ?y), H' : is_true (?R ?y ?z) |- _ ] + => pose proof (transitivity H H' : is_true (R x z)) + end. + exact I. +Qed.
\ No newline at end of file diff --git a/test-suite/bugs/closed/4772.v b/test-suite/bugs/closed/4772.v new file mode 100644 index 0000000000..c3109fa31c --- /dev/null +++ b/test-suite/bugs/closed/4772.v @@ -0,0 +1,6 @@ + +Record TruncType := BuildTruncType { + trunctype_type : Type +}. + +Fail Arguments BuildTruncType _ _ {_}. (* This should fail *) diff --git a/test-suite/bugs/closed/4785.v b/test-suite/bugs/closed/4785.v index 14af2d91df..c3c97d3f59 100644 --- a/test-suite/bugs/closed/4785.v +++ b/test-suite/bugs/closed/4785.v @@ -21,7 +21,7 @@ Delimit Scope mylist_scope with mylist. Bind Scope mylist_scope with mylist. Arguments mynil {_}, _. Arguments mycons {_} _ _. -Notation " [] " := mynil : mylist_scope. +Notation " [] " := mynil (compat "8.5") : mylist_scope. Notation " [ ] " := mynil (format "[ ]") : mylist_scope. Notation " [ x ] " := (mycons x nil) : mylist_scope. Notation " [ x ; y ; .. ; z ] " := (mycons x (mycons y .. (mycons z nil) ..)) : mylist_scope. diff --git a/test-suite/bugs/closed/4785_compat_85.v b/test-suite/bugs/closed/4785_compat_85.v new file mode 100644 index 0000000000..9d65840acd --- /dev/null +++ b/test-suite/bugs/closed/4785_compat_85.v @@ -0,0 +1,46 @@ +(* -*- coq-prog-args: ("-emacs" "-compat" "8.5") -*- *) +Require Coq.Lists.List Coq.Vectors.Vector. +Require Coq.Compat.Coq85. + +Module A. +Import Coq.Lists.List Coq.Vectors.Vector. +Import ListNotations. +Check [ ]%list : list _. +Import VectorNotations ListNotations. +Delimit Scope vector_scope with vector. +Check [ ]%vector : Vector.t _ _. +Check []%vector : Vector.t _ _. +Check [ ]%list : list _. +Fail Check []%list : list _. + +Goal True. + idtac; [ ]. (* Note that vector notations break the [ | .. | ] syntax of Ltac *) +Abort. + +Inductive mylist A := mynil | mycons (x : A) (xs : mylist A). +Delimit Scope mylist_scope with mylist. +Bind Scope mylist_scope with mylist. +Arguments mynil {_}, _. +Arguments mycons {_} _ _. +Notation " [] " := mynil (compat "8.5") : mylist_scope. +Notation " [ ] " := mynil (format "[ ]") : mylist_scope. +Notation " [ x ] " := (mycons x nil) : mylist_scope. +Notation " [ x ; y ; .. ; z ] " := (mycons x (mycons y .. (mycons z nil) ..)) : mylist_scope. + +Import Coq.Compat.Coq85. +Locate Module VectorNotations. +Import VectorDef.VectorNotations. + +Check []%vector : Vector.t _ _. +Check []%mylist : mylist _. +Check [ ]%mylist : mylist _. +Check [ ]%list : list _. +End A. + +Module B. +Import Coq.Compat.Coq85. + +Goal True. + idtac; []. (* Check that importing the compat file doesn't break the [ | .. | ] syntax of Ltac *) +Abort. +End B. diff --git a/test-suite/bugs/closed/4798.v b/test-suite/bugs/closed/4798.v new file mode 100644 index 0000000000..dbc3d46fce --- /dev/null +++ b/test-suite/bugs/closed/4798.v @@ -0,0 +1,3 @@ +Check match 2 with 0 => 0 | S n => n end. +Notation "|" := 1 (compat "8.4"). +Check match 2 with 0 => 0 | S n => n end. (* fails *) diff --git a/test-suite/bugs/closed/4863.v b/test-suite/bugs/closed/4863.v new file mode 100644 index 0000000000..1e47f2957b --- /dev/null +++ b/test-suite/bugs/closed/4863.v @@ -0,0 +1,33 @@ +Require Import Classes.DecidableClass. + +Inductive Foo : Set := +| foo1 | foo2. + +Lemma Decidable_sumbool : forall P, {P}+{~P} -> Decidable P. +Proof. + intros P H. + refine (Build_Decidable _ (if H then true else false) _). + intuition congruence. +Qed. + +Hint Extern 100 (Decidable (?A = ?B)) => abstract (abstract (abstract (apply Decidable_sumbool; decide equality))) : typeclass_instances. + +Goal forall (a b : Foo), {a=b}+{a<>b}. +intros. +abstract (abstract (decide equality)). (*abstract works here*) +Qed. + +Check ltac:(abstract (exact I)) : True. + +Goal forall (a b : Foo), Decidable (a=b) * Decidable (a=b). +intros. +split. typeclasses eauto. +typeclasses eauto. Qed. + +Goal forall (a b : Foo), Decidable (a=b) * Decidable (a=b). +intros. +split. +refine _. +refine _. +Defined. +(*fails*) diff --git a/test-suite/bugs/closed/4869.v b/test-suite/bugs/closed/4869.v new file mode 100644 index 0000000000..6d21b66fe9 --- /dev/null +++ b/test-suite/bugs/closed/4869.v @@ -0,0 +1,18 @@ +Universes i. + +Fail Constraint i < Set. +Fail Constraint i <= Set. +Fail Constraint i = Set. +Constraint Set <= i. +Constraint Set < i. +Fail Constraint i < j. (* undeclared j *) +Fail Constraint i < Type. (* anonymous *) + +Set Universe Polymorphism. + +Section Foo. + Universe j. + Constraint Set < j. + + Definition foo := Type@{j}. +End Foo.
\ No newline at end of file diff --git a/test-suite/bugs/closed/4955.v b/test-suite/bugs/closed/4955.v new file mode 100644 index 0000000000..dce1f764c3 --- /dev/null +++ b/test-suite/bugs/closed/4955.v @@ -0,0 +1,98 @@ +(* An example involving a first-order unification triggering a cyclic constraint *) + +Module A. +Notation "{ x : A | P }" := (sigT (fun x:A => P)). +Notation "( x ; y )" := (existT _ x y) : fibration_scope. +Open Scope fibration_scope. +Notation "p @ q" := (eq_trans p q) (at level 20). +Notation "p ^" := (eq_sym p) (at level 3). +Definition transport {A : Type} (P : A -> Type) {x y : A} (p : x = y) (u : P x) +: P y := + match p with eq_refl => u end. +Notation "p # x" := (transport _ p x) (right associativity, at level 65, only +parsing). +Definition ap {A B:Type} (f:A -> B) {x y:A} (p:x = y) : f x = f y + := match p with eq_refl => eq_refl end. +Definition apD {A:Type} {B:A->Type} (f:forall a:A, B a) {x y:A} (p:x=y): p # (f +x) = f y + := match p with eq_refl => eq_refl end. +Axiom transport_compose + : forall {A B} {x y : A} (P : B -> Type) (f : A -> B) (p : x = y) (z : P (f +x)), + transport (fun x => P (f x)) p z = transport P (ap f p) z. +Delimit Scope morphism_scope with morphism. +Delimit Scope category_scope with category. +Delimit Scope object_scope with object. +Record PreCategory := { object :> Type ; morphism : object -> object -> Type }. +Delimit Scope functor_scope with functor. +Record Functor (C D : PreCategory) := + { object_of :> C -> D; + morphism_of : forall s d, morphism C s d -> morphism D (object_of s) +(object_of d) }. +Arguments object_of {C%category D%category} f%functor c%object : rename, simpl +nomatch. +Arguments morphism_of [C%category] [D%category] f%functor [s%object d%object] +m%morphism : rename, simpl nomatch. +Section path_functor. + Variable C : PreCategory. + Variable D : PreCategory. + + Local Notation path_functor'_T F G + := { HO : object_of F = object_of G + | transport (fun GO => forall s d, morphism C s d -> morphism D (GO s) +(GO d)) + HO + (morphism_of F) + = morphism_of G } + (only parsing). + Definition path_functor'_sig_inv (F G : Functor C D) : F = G -> +path_functor'_T F G + := fun H' + => (ap object_of H'; + (transport_compose _ object_of _ _) ^ @ apD (@morphism_of _ _) H'). + +End path_functor. +End A. + +(* A variant of it with more axioms *) + +Module B. +Notation "{ x : A | P }" := (sigT (fun x:A => P)). +Notation "( x ; y )" := (existT _ x y). +Notation "p @ q" := (eq_trans p q) (at level 20). +Notation "p ^" := (eq_sym p) (at level 3). +Axiom transport : forall {A : Type} (P : A -> Type) {x y : A} (p : x = y) (u : P x), P y. +Notation "p # x" := (transport _ p x) (right associativity, at level 65, only +parsing). +Definition ap {A B:Type} (f:A -> B) {x y:A} (p:x = y) : f x = f y + := match p with eq_refl => eq_refl end. +Axiom apD : forall {A:Type} {B:A->Type} (f:forall a:A, B a) {x y:A} (p:x=y), p # (f +x) = f y. +Axiom transport_compose + : forall {A B} {x y : A} (P : B -> Type) (f : A -> B) (p : x = y) (z : P (f +x)), + transport (fun x => P (f x)) p z = transport P (ap f p) z. +Record PreCategory := { object :> Type ; morphism : object -> object -> Type }. +Record Functor (C D : PreCategory) := + { object_of :> C -> D; + morphism_of : forall s d, morphism C s d -> morphism D (object_of s) +(object_of d) }. +Arguments object_of {C D} f c : rename, simpl nomatch. +Arguments morphism_of [C] [D] f [s d] m : rename, simpl nomatch. +Section path_functor. + Variable C D : PreCategory. + Local Notation path_functor'_T F G + := { HO : object_of F = object_of G + | transport (fun GO => forall s d, morphism C s d -> morphism D (GO s) +(GO d)) + HO + (morphism_of F) + = morphism_of G }. + Definition path_functor'_sig_inv (F G : Functor C D) : F = G -> +path_functor'_T F G + := fun H' + => (ap object_of H'; + (transport_compose _ object_of _ _) ^ @ apD (@morphism_of _ _) H'). + +End path_functor. +End B. diff --git a/test-suite/bugs/closed/4966.v b/test-suite/bugs/closed/4966.v new file mode 100644 index 0000000000..bd93cdc858 --- /dev/null +++ b/test-suite/bugs/closed/4966.v @@ -0,0 +1,10 @@ +(* Interpretation of auto as an argument of an ltac function (i.e. as an ident) was wrongly "auto with *" *) + +Axiom proof_admitted : False. +Hint Extern 0 => case proof_admitted : unused. +Ltac do_tac tac := tac. + +Goal False. + Set Ltac Profiling. + Fail solve [ do_tac auto ]. +Abort. diff --git a/test-suite/bugs/closed/4970.v b/test-suite/bugs/closed/4970.v new file mode 100644 index 0000000000..7a896582f5 --- /dev/null +++ b/test-suite/bugs/closed/4970.v @@ -0,0 +1,3 @@ +(* Check "{{" is not confused with "{" in notations *) +Reserved Notation "x {{ y }}" (at level 40). +Notation "x {{ y }}" := (x y) (only parsing). diff --git a/test-suite/bugs/closed/5011.v b/test-suite/bugs/closed/5011.v new file mode 100644 index 0000000000..c3043ca5d1 --- /dev/null +++ b/test-suite/bugs/closed/5011.v @@ -0,0 +1,2 @@ +Record decoder (n : nat) W := { decode : W -> nat }. +Existing Class decoder. diff --git a/test-suite/bugs/closed/5036.v b/test-suite/bugs/closed/5036.v new file mode 100644 index 0000000000..12c958be67 --- /dev/null +++ b/test-suite/bugs/closed/5036.v @@ -0,0 +1,10 @@ +Section foo. + Context (F : Type -> Type). + Context (admit : forall {T}, F T = True). + Hint Rewrite (fun T => @admit T). + Lemma bad : F False. + Proof. + autorewrite with core. + constructor. + Qed. +End foo. (* Anomaly: Universe Top.16 undefined. Please report. *)
\ No newline at end of file diff --git a/test-suite/bugs/closed/5045.v b/test-suite/bugs/closed/5045.v new file mode 100644 index 0000000000..dc38738d8f --- /dev/null +++ b/test-suite/bugs/closed/5045.v @@ -0,0 +1,3 @@ +Axiom silly : 1 = 1 -> nat -> nat. +Goal forall pf : 1 = 1, silly pf 0 = 0 -> True. + Fail generalize (@eq nat). diff --git a/test-suite/bugs/closed/5066.v b/test-suite/bugs/closed/5066.v new file mode 100644 index 0000000000..eed7f0f3ff --- /dev/null +++ b/test-suite/bugs/closed/5066.v @@ -0,0 +1,7 @@ +Require Import Vector. + +Fail Program Fixpoint vector_rev {A : Type} {n1 n2 : nat} (v1 : Vector.t A n1) (v2 : Vector.t A n2) : Vector.t A (n1+n2) := + match v1 with + | nil _ => v2 + | cons _ e n' sv => vector_rev sv (cons A e n2 v2) + end. diff --git a/test-suite/bugs/closed/5097.v b/test-suite/bugs/closed/5097.v new file mode 100644 index 0000000000..37b239cf61 --- /dev/null +++ b/test-suite/bugs/closed/5097.v @@ -0,0 +1,7 @@ +(* Tracing existing evars along the weakening rule ("clear") *) +Goal forall y, exists x, x=0->x=y. +intros. +eexists ?[x]. +intros. +let x:=constr:(ltac:(clear y; exact 0)) in idtac x. +Abort. diff --git a/test-suite/bugs/closed/5123.v b/test-suite/bugs/closed/5123.v new file mode 100644 index 0000000000..bcde510ee6 --- /dev/null +++ b/test-suite/bugs/closed/5123.v @@ -0,0 +1,33 @@ +(* IN 8.5pl2 and 8.6 (4da2131), the following shows different typeclass resolution behaviors following an unshelve tactical vs. an Unshelve command: *) + +(*Pose an open constr to prevent immediate typeclass resolution in holes:*) +Tactic Notation "opose" open_constr(x) "as" ident(H) := pose x as H. + +Inductive vect A : nat -> Type := +| vnil : vect A 0 +| vcons : forall (h:A) (n:nat), vect A n -> vect A (S n). + +Class Eqdec A := eqdec : forall a b : A, {a=b}+{a<>b}. + +Require Bool. + +Instance Bool_eqdec : Eqdec bool := Bool.bool_dec. + +Context `{vect_sigT_eqdec : forall A : Type, Eqdec A -> Eqdec {a : nat & vect A a}}. + +Typeclasses eauto := debug. + +Goal True. + unshelve opose (@vect_sigT_eqdec _ _ _ _) as H. + all:cycle 2. + eapply existT. (*BUG: Why does this do typeclass resolution in the evar?*) + Focus 5. +Abort. + +Goal True. + opose (@vect_sigT_eqdec _ _ _ _) as H. + Unshelve. + all:cycle 3. + eapply existT. (*This does no typeclass resultion, which is correct.*) + Focus 5. +Abort.
\ No newline at end of file diff --git a/test-suite/bugs/closed/5127.v b/test-suite/bugs/closed/5127.v new file mode 100644 index 0000000000..831e8fb507 --- /dev/null +++ b/test-suite/bugs/closed/5127.v @@ -0,0 +1,15 @@ +Fixpoint arrow (n: nat) := + match n with + | S n => bool -> arrow n + | O => bool + end. + +Fixpoint apply (n : nat) : arrow n -> bool := + match n return arrow n -> bool with + | S n => fun f => apply _ (f true) + | O => fun x => x + end. + +Axiom f : arrow 10000. +Definition v : bool := Eval compute in apply _ f. +Definition w : bool := Eval vm_compute in v. diff --git a/test-suite/bugs/closed/5145.v b/test-suite/bugs/closed/5145.v new file mode 100644 index 0000000000..0533d21e0c --- /dev/null +++ b/test-suite/bugs/closed/5145.v @@ -0,0 +1,10 @@ +Class instructions := + { + W : Type; + ldi : nat -> W + }. + +Fail Definition foo := + let y2 := ldi 0 in + let '(CF, _) := (true, 0) in + y2. diff --git a/test-suite/bugs/closed/5149.v b/test-suite/bugs/closed/5149.v new file mode 100644 index 0000000000..684dba1961 --- /dev/null +++ b/test-suite/bugs/closed/5149.v @@ -0,0 +1,47 @@ +Goal forall x x' : nat, x = x' -> S x = S x -> exists y, S y = S x. +intros. +eexists. +rewrite <- H. +eassumption. +Qed. + +Goal forall (base_type_code : Type) (t : base_type_code) (flat_type : Type) + (t' : flat_type) (exprf interp_flat_type0 interp_flat_type1 : +flat_type -> Type) + (v v' : interp_flat_type1 t'), + v = v' -> + forall (interpf : forall t0 : flat_type, exprf t0 -> interp_flat_type1 t0) + (SmartVarVar : forall t0 : flat_type, interp_flat_type1 t0 -> +interp_flat_type0 t0) + (Tbase : base_type_code -> flat_type) (x : exprf (Tbase t)) + (x' : interp_flat_type1 (Tbase t)) (T : Type) + (flatten_binding_list : forall t0 : flat_type, + interp_flat_type0 t0 -> interp_flat_type1 t0 -> list T) + (P : T -> list T -> Prop) (prod : Type -> Type -> Type) + (s : forall x0 : base_type_code, prod (exprf (Tbase x0)) +(interp_flat_type1 (Tbase x0)) -> T) + (pair : forall A B : Type, A -> B -> prod A B), + P (s t (pair (exprf (Tbase t)) (interp_flat_type1 (Tbase t)) x x')) + (flatten_binding_list t' (SmartVarVar t' v') v) -> + (forall (t0 : base_type_code) (t'0 : flat_type) (v0 : interp_flat_type1 +t'0) + (x0 : exprf (Tbase t0)) (x'0 : interp_flat_type1 (Tbase t0)), + P (s t0 (pair (exprf (Tbase t0)) (interp_flat_type1 (Tbase t0)) x0 +x'0)) + (flatten_binding_list t'0 (SmartVarVar t'0 v0) v0) -> interpf +(Tbase t0) x0 = x'0) -> + interpf (Tbase t) x = x'. +Proof. + intros ?????????????????????? interpf_SmartVarVar. + solve [ unshelve (subst; eapply interpf_SmartVarVar; eassumption) ] || fail +"too early". + Undo. + (** Implicitely at the dot. The first fails because unshelve adds a goal, and solve hence fails. The second has an ambiant unification problem that is solved after solve *) + Fail solve [ unshelve (eapply interpf_SmartVarVar; subst; eassumption) ]. + solve [eapply interpf_SmartVarVar; subst; eassumption]. + Undo. + Unset Solve Unification Constraints. + (* User control of when constraints are solved *) + solve [ unshelve (eapply interpf_SmartVarVar; subst; eassumption); solve_constraints ]. +Qed. + diff --git a/test-suite/bugs/closed/5161.v b/test-suite/bugs/closed/5161.v new file mode 100644 index 0000000000..d28303b8ab --- /dev/null +++ b/test-suite/bugs/closed/5161.v @@ -0,0 +1,27 @@ +(* Check that the presence of binders with type annotation do not + prevent the recursive binder part to be found *) + +From Coq Require Import Utf8. + +Delimit Scope C_scope with C. +Global Open Scope C_scope. + +Delimit Scope uPred_scope with I. + +Definition FORALL {T : Type} (f : T → Prop) : Prop := ∀ x, f x. + +Notation "∀ x .. y , P" := + (FORALL (λ x, .. (FORALL (λ y, P)) ..)%I) + (at level 200, x binder, y binder, right associativity) : uPred_scope. +Infix "∧" := and : uPred_scope. + +(* The next command fails with + In recursive notation with binders, Φ is expected to come without type. + I would expect this notation to work fine, since the ∀ does support + type annotation. +*) +Notation "'{{{' P } } } e {{{ x .. y ; pat , Q } } }" := + (∀ Φ : _ → _, + (∀ x, .. (∀ y, Q ∧ Φ pat) .. ))%I + (at level 20, x closed binder, y closed binder, + format "{{{ P } } } e {{{ x .. y ; pat , Q } } }") : uPred_scope. diff --git a/test-suite/bugs/closed/5180.v b/test-suite/bugs/closed/5180.v new file mode 100644 index 0000000000..261092ee6d --- /dev/null +++ b/test-suite/bugs/closed/5180.v @@ -0,0 +1,64 @@ +Universes a b c ω ω'. +Definition Typeω := Type@{ω}. +Definition Type2 : Typeω := Type@{c}. +Definition Type1 : Type2 := Type@{b}. +Definition Type0 : Type1 := Type@{a}. + +Set Universe Polymorphism. +Set Printing Universes. + +Definition Typei' (n : nat) + := match n return Type@{ω'} with + | 0 => Type0 + | 1 => Type1 + | 2 => Type2 + | _ => Typeω + end. +Definition TypeOfTypei' {n} (x : Typei' n) : Type@{ω'} + := match n return Typei' n -> Type@{ω'} with + | 0 | 1 | 2 | _ => fun x => x + end x. +Definition Typei (n : nat) : Typei' (S n) + := match n return Typei' (S n) with + | 0 => Type0 + | 1 => Type1 + | _ => Type2 + end. +Definition TypeOfTypei {n} (x : TypeOfTypei' (Typei n)) : Type@{ω'} + := match n return TypeOfTypei' (Typei n) -> Type@{ω'} with + | 0 | 1 | _ => fun x => x + end x. +Check Typei 0 : Typei 1. +Check Typei 1 : Typei 2. + +Definition lift' {n} : TypeOfTypei' (Typei n) -> TypeOfTypei' (Typei (S n)) + := match n return TypeOfTypei' (Typei n) -> TypeOfTypei' (Typei (S n)) with + | 0 | 1 | 2 | _ => fun x => (x : Type) + end. +Definition lift'' {n} : TypeOfTypei' (Typei n) -> TypeOfTypei' (Typei (S n)) + := match n return TypeOfTypei' (Typei n) -> TypeOfTypei' (Typei (S n)) with + | 0 | 1 | 2 | _ => fun x => x + end. (* The command has indeed failed with message: +In environment +n : nat +x : TypeOfTypei' (Typei 0) +The term "x" has type "TypeOfTypei' (Typei 0)" while it is expected to have type + "TypeOfTypei' (Typei 1)" (universe inconsistency: Cannot enforce b = a because a < b). + *) +Check (fun x : TypeOfTypei' (Typei 0) => TypeOfTypei' (Typei 1)). + +Definition lift''' {n} : TypeOfTypei' (Typei n) -> TypeOfTypei' (Typei (S n)). + refine match n return TypeOfTypei' (Typei n) -> TypeOfTypei' (Typei (S n)) with + | 0 | 1 | 2 | _ => fun x => _ + end. + exact x. + Undo. + (* The command has indeed failed with message: +In environment +n : nat +x : TypeOfTypei' (Typei 0) +The term "x" has type "TypeOfTypei' (Typei 0)" while it is expected to have type + "TypeOfTypei' (Typei 1)" (universe inconsistency: Cannot enforce b = a because a < b). + *) + all:compute in *. + all:exact x.
\ No newline at end of file diff --git a/test-suite/bugs/closed/5181.v b/test-suite/bugs/closed/5181.v new file mode 100644 index 0000000000..0e6d471979 --- /dev/null +++ b/test-suite/bugs/closed/5181.v @@ -0,0 +1,3 @@ +Definition foo (x y : nat) := x. +Fail Arguments foo {_} : assert. + diff --git a/test-suite/bugs/closed/5188.v b/test-suite/bugs/closed/5188.v new file mode 100644 index 0000000000..e29ebfb4ec --- /dev/null +++ b/test-suite/bugs/closed/5188.v @@ -0,0 +1,5 @@ +Set Printing All. +Axiom relation : forall (T : Type), Set. +Axiom T : forall A (R : relation A), Set. +Set Printing Universes. +Parameter (A:_) (R:_) (e:@T A R). diff --git a/test-suite/bugs/closed/5198.v b/test-suite/bugs/closed/5198.v new file mode 100644 index 0000000000..7254afb429 --- /dev/null +++ b/test-suite/bugs/closed/5198.v @@ -0,0 +1,39 @@ +(* -*- mode: coq; coq-prog-args: ("-emacs" "-boot" "-nois") -*- *) +(* File reduced by coq-bug-finder from original input, then from 286 lines to +27 lines, then from 224 lines to 53 lines, then from 218 lines to 56 lines, +then from 269 lines to 180 lines, then from 132 lines to 48 lines, then from +253 lines to 65 lines, then from 79 lines to 65 lines *) +(* coqc version 8.6.0 (November 2016) compiled on Nov 12 2016 14:43:52 with +OCaml 4.02.3 + coqtop version jgross-Leopard-WS:/home/jgross/Downloads/coq/coq-v8.6,v8.6 +(7e992fa784ee6fa48af8a2e461385c094985587d) *) +Axiom admit : forall {T}, T. +Set Printing Implicit. +Inductive nat := O | S (_ : nat). +Axiom f : forall (_ _ : nat), nat. +Class ZLikeOps (e : nat) + := { LargeT : Type ; SmallT : Type ; CarryAdd : forall (_ _ : LargeT), LargeT +}. +Class BarrettParameters := + { b : nat ; k : nat ; ops : ZLikeOps (f b k) }. +Axiom barrett_reduce_function_bundled : forall {params : BarrettParameters} + (_ : @LargeT _ (@ops params)), + @SmallT _ (@ops params). + +Global Instance ZZLikeOps e : ZLikeOps (f (S O) e) + := { LargeT := nat ; SmallT := nat ; CarryAdd x y := y }. +Definition SRep := nat. +Local Instance x86_25519_Barrett : BarrettParameters + := { b := S O ; k := O ; ops := ZZLikeOps O }. +Definition SRepAdd : forall (_ _ : SRep), SRep + := let v := (fun x y => barrett_reduce_function_bundled (CarryAdd x y)) in + v. +Definition SRepAdd' : forall (_ _ : SRep), SRep + := (fun x y => barrett_reduce_function_bundled (CarryAdd x y)). +(* Error: +In environment +x : SRep +y : SRep +The term "x" has type "SRep" while it is expected to have type + "@LargeT ?e ?ZLikeOps". + *) diff --git a/test-suite/bugs/closed/5203.v b/test-suite/bugs/closed/5203.v new file mode 100644 index 0000000000..ed137395fc --- /dev/null +++ b/test-suite/bugs/closed/5203.v @@ -0,0 +1,5 @@ +Goal True. + Typeclasses eauto := debug. + Fail solve [ typeclasses eauto ]. + Fail typeclasses eauto. +
\ No newline at end of file diff --git a/test-suite/bugs/closed/5208.v b/test-suite/bugs/closed/5208.v new file mode 100644 index 0000000000..b7a684a27c --- /dev/null +++ b/test-suite/bugs/closed/5208.v @@ -0,0 +1,222 @@ +Require Import Program. + +Require Import Coq.Strings.String. +Require Import Coq.Strings.Ascii. +Require Import Coq.Numbers.BinNums. + +Set Implicit Arguments. +Set Strict Implicit. +Set Universe Polymorphism. +Set Printing Universes. + +Local Open Scope positive. + +Definition field : Type := positive. + +Section poly. + Universe U. + + Inductive fields : Type := + | pm_Leaf : fields + | pm_Branch : fields -> option Type@{U} -> fields -> fields. + + Definition fields_left (f : fields) : fields := + match f with + | pm_Leaf => pm_Leaf + | pm_Branch l _ _ => l + end. + + Definition fields_right (f : fields) : fields := + match f with + | pm_Leaf => pm_Leaf + | pm_Branch _ _ r => r + end. + + Definition fields_here (f : fields) : option Type@{U} := + match f with + | pm_Leaf => None + | pm_Branch _ s _ => s + end. + + Fixpoint fields_get (p : field) (m : fields) {struct p} : option Type@{U} := + match p with + | xH => match m with + | pm_Leaf => None + | pm_Branch _ x _ => x + end + | xO p' => fields_get p' match m with + | pm_Leaf => pm_Leaf + | pm_Branch L _ _ => L + end + | xI p' => fields_get p' match m with + | pm_Leaf => pm_Leaf + | pm_Branch _ _ R => R + end + end. + + Definition fields_leaf : fields := pm_Leaf. + + Inductive member (val : Type@{U}) : fields -> Type := + | pmm_H : forall L R, member val (pm_Branch L (Some val) R) + | pmm_L : forall (V : option Type@{U}) L R, member val L -> member val (pm_Branch L V R) + | pmm_R : forall (V : option Type@{U}) L R, member val R -> member val (pm_Branch L V R). + Arguments pmm_H {_ _ _}. + Arguments pmm_L {_ _ _ _} _. + Arguments pmm_R {_ _ _ _} _. + + Fixpoint get_member (val : Type@{U}) p {struct p} + : forall m, fields_get p m = @Some Type@{U} val -> member val m := + match p as p return forall m, fields_get p m = @Some Type@{U} val -> member@{U} val m with + | xH => fun m => + match m as m return fields_get xH m = @Some Type@{U} val -> member@{U} val m with + | pm_Leaf => fun pf : None = @Some Type@{U} _ => + match pf in _ = Z return match Z with + | Some _ => _ + | None => unit + end + with + | eq_refl => tt + end + | pm_Branch _ None _ => fun pf : None = @Some Type@{U} _ => + match pf in _ = Z return match Z with + | Some _ => _ + | None => unit + end + with + | eq_refl => tt + end + | pm_Branch _ (Some x) _ => fun pf : @Some Type@{U} x = @Some Type@{U} val => + match eq_sym pf in _ = Z return member@{U} val (pm_Branch _ Z _) with + | eq_refl => pmm_H + end + end + | xO p' => fun m => + match m as m return fields_get (xO p') m = @Some Type@{U} val -> member@{U} val m with + | pm_Leaf => fun pf : fields_get p' pm_Leaf = @Some Type@{U} val => + @get_member _ p' pm_Leaf pf + | pm_Branch l _ _ => fun pf : fields_get p' l = @Some Type@{U} val => + @pmm_L _ _ _ _ (@get_member _ p' l pf) + end + | xI p' => fun m => + match m as m return fields_get (xI p') m = @Some Type@{U} val -> member@{U} val m with + | pm_Leaf => fun pf : fields_get p' pm_Leaf = @Some Type@{U} val => + @get_member _ p' pm_Leaf pf + | pm_Branch l _ r => fun pf : fields_get p' r = @Some Type@{U} val => + @pmm_R _ _ _ _ (@get_member _ p' r pf) + end + end. + + Inductive record : fields -> Type := + | pr_Leaf : record pm_Leaf + | pr_Branch : forall L R (V : option Type@{U}), + record L -> + match V return Type@{U} with + | None => unit + | Some t => t + end -> + record R -> + record (pm_Branch L V R). + + + Definition record_left {L} {V : option Type@{U}} {R} + (r : record (pm_Branch L V R)) : record L := + match r in record z + return match z with + | pm_Branch L _ _ => record L + | _ => unit + end + with + | pr_Branch _ l _ _ => l + | pr_Leaf => tt + end. +Set Printing All. + Definition record_at {L} {V : option Type@{U}} {R} (r : record (pm_Branch L V R)) + : match V return Type@{U} with + | None => unit + | Some t => t + end := + match r in record z + return match z (* return ?X *) with + | pm_Branch _ V _ => match V return Type@{U} with + | None => unit + | Some t => t + end + | _ => unit + end + with + | pr_Branch _ _ v _ => v + | pr_Leaf => tt + end. + + Definition record_here {L : fields} (v : Type@{U}) {R : fields} + (r : record (pm_Branch L (@Some Type@{U} v) R)) : v := + match r in record z + return match z return Type@{U} with + | pm_Branch _ (Some v) _ => v + | _ => unit + end + with + | pr_Branch _ _ v _ => v + | pr_Leaf => tt + end. + + Definition record_right {L V R} (r : record (pm_Branch L V R)) : record R := + match r in record z return match z with + | pm_Branch _ _ R => record R + | _ => unit + end + with + | pr_Branch _ _ _ r => r + | pr_Leaf => tt + end. + + Fixpoint record_get {val : Type@{U}} {pm : fields} (m : member val pm) : record pm -> val := + match m in member _ pm return record pm -> val with + | pmm_H => fun r => record_here r + | pmm_L m' => fun r => record_get m' (record_left r) + | pmm_R m' => fun r => record_get m' (record_right r) + end. + + Fixpoint record_set {val : Type@{U}} {pm : fields} (m : member val pm) (x : val) {struct m} + : record pm -> record pm := + match m in member _ pm return record pm -> record pm with + | pmm_H => fun r => + pr_Branch (Some _) + (record_left r) + x + (record_right r) + | pmm_L m' => fun r => + pr_Branch _ + (record_set m' x (record_left r)) + (record_at r) + (record_right r) + | pmm_R m' => fun r => + pr_Branch _ (record_left r) + (record_at r) + (record_set m' x (record_right r)) + end. +End poly. +Axiom cheat : forall {A}, A. +Lemma record_get_record_set_different: + forall (T: Type) (vars: fields) + (pmr pmw: member T vars) + (diff: pmr <> pmw) + (r: record vars) (val: T), + record_get pmr (record_set pmw val r) = record_get pmr r. +Proof. + intros. + revert pmr diff r val. + induction pmw; simpl; intros. + - dependent destruction pmr. + + congruence. + + auto. + + auto. + - dependent destruction pmr. + + auto. + + simpl. apply IHpmw. congruence. + + auto. + - dependent destruction pmr. + + auto. + + auto. + + simpl. apply IHpmw. congruence. +Qed. diff --git a/test-suite/bugs/closed/5322.v b/test-suite/bugs/closed/5322.v new file mode 100644 index 0000000000..01aec8f29b --- /dev/null +++ b/test-suite/bugs/closed/5322.v @@ -0,0 +1,14 @@ +(* Regression in computing types of branches in "match" *) +Inductive flat_type := Unit | Prod (A B : flat_type). +Inductive exprf (op : flat_type -> flat_type -> Type) {var : Type} : flat_type +-> Type := +| Op {t1 tR} (opc : op t1 tR) (args : exprf op t1) : exprf op tR. +Inductive op : flat_type -> flat_type -> Type := a : op Unit Unit. +Arguments Op {_ _ _ _} _ _. +Definition bound_op {var} + {src2 dst2} + (opc2 : op src2 dst2) + : forall (args2 : exprf op (var:=var) src2), Op opc2 args2 = Op opc2 args2. + refine match opc2 return (forall args2, Op opc2 args2 = Op opc2 args2) with + | _ => _ + end. diff --git a/test-suite/bugs/closed/5323.v b/test-suite/bugs/closed/5323.v new file mode 100644 index 0000000000..295b7cd9f5 --- /dev/null +++ b/test-suite/bugs/closed/5323.v @@ -0,0 +1,26 @@ +(* Revealed a missing re-consideration of postponed problems *) + +Module A. +Inductive flat_type := Unit | Prod (A B : flat_type). +Inductive exprf (op : flat_type -> flat_type -> Type) {var : Type} : flat_type +-> Type := +| Op {t1 tR} (opc : op t1 tR) (args : exprf op t1) : exprf op tR. +Inductive op : flat_type -> flat_type -> Type := . +Arguments Op {_ _ _ _} _ _. +Definition bound_op {var} + {src2 dst2} + (opc2 : op src2 dst2) + : forall (args2 : exprf op (var:=var) src2), Op opc2 args2 = Op opc2 args2 + := match opc2 return (forall args2, Op opc2 args2 = Op opc2 args2) with end. +End A. + +(* A shorter variant *) +Module B. +Inductive exprf (op : unit -> Type) : Type := +| A : exprf op +| Op tR (opc : op tR) (args : exprf op) : exprf op. +Inductive op : unit -> Type := . +Definition bound_op (dst2 : unit) (opc2 : op dst2) + : forall (args2 : exprf op), Op op dst2 opc2 args2 = A op + := match opc2 in op h return (forall args2 : exprf ?[U], Op ?[V] ?[I] opc2 args2 = A op) with end. +End B. diff --git a/test-suite/bugs/closed/5331.v b/test-suite/bugs/closed/5331.v new file mode 100644 index 0000000000..28743736d3 --- /dev/null +++ b/test-suite/bugs/closed/5331.v @@ -0,0 +1,11 @@ +(* Checking no anomaly on some unexpected intropattern *) + +Ltac ih H := induction H as H. +Ltac ih' H H' := induction H as H'. + +Goal True -> True. +Fail intro H; ih H. +intro H; ih' H ipattern:([]). +exact I. +Qed. + diff --git a/test-suite/bugs/closed/5346.v b/test-suite/bugs/closed/5346.v new file mode 100644 index 0000000000..0118c18704 --- /dev/null +++ b/test-suite/bugs/closed/5346.v @@ -0,0 +1,29 @@ +Inductive comp : Type -> Type := +| Ret {T} : forall (v:T), comp T +| Bind {T T'} : forall (p: comp T') (p': T' -> comp T), comp T. + +Notation "'do' x .. y <- p1 ; p2" := + (Bind p1 (fun x => .. (fun y => p2) ..)) + (at level 60, right associativity, + x binder, y binder). + +Definition Fst1 A B (p: comp (A*B)) : comp A := + do '(a, b) <- p; + Ret a. + +Definition Fst2 A B (p: comp (A*B)) : comp A := + match tt with + | _ => Bind p (fun '(a, b) => Ret a) + end. + +Definition Fst3 A B (p: comp (A*B)) : comp A := + match tt with + | _ => do a <- p; + Ret (fst a) + end. + +Definition Fst A B (p: comp (A * B)) : comp A := + match tt with + | _ => do '(a, b) <- p; + Ret a + end. diff --git a/test-suite/bugs/closed/HoTT_coq_117.v b/test-suite/bugs/closed/HoTT_coq_117.v index 5fbcfef4e0..de60fd0ae4 100644 --- a/test-suite/bugs/closed/HoTT_coq_117.v +++ b/test-suite/bugs/closed/HoTT_coq_117.v @@ -16,10 +16,29 @@ Definition path_forall `{Funext} {A : Type} {P : A -> Type} (f g : forall x : A, Admitted. Inductive Empty : Set := . -Instance contr_from_Empty {_ : Funext} (A : Type) : +Fail Instance contr_from_Empty {_ : Funext} (A : Type) : + Contr_internal (Empty -> A) := + BuildContr _ + (Empty_rect (fun _ => A)) + (fun f => path_forall _ f (fun x => Empty_rect _ x)). + +Fail Instance contr_from_Empty {F : Funext} (A : Type) : Contr_internal (Empty -> A) := BuildContr _ (Empty_rect (fun _ => A)) (fun f => path_forall _ f (fun x => Empty_rect _ x)). + +(** This could be disallowed, this uses the Funext argument *) +Instance contr_from_Empty {_ : Funext} (A : Type) : + Contr_internal (Empty -> A) := + BuildContr _ + (Empty_rect (fun _ => A)) + (fun f => path_forall _ f (fun x => Empty_rect (fun _ => _ x = f x) x)). + +Instance contr_from_Empty' {_ : Funext} (A : Type) : + Contr_internal (Empty -> A) := + BuildContr _ + (Empty_rect (fun _ => A)) + (fun f => path_forall _ f (fun x => Empty_rect (fun _ => _ x = f x) x)). (* Toplevel input, characters 15-220: Anomaly: unknown meta ?190. Please report. *) diff --git a/test-suite/bugs/opened/4701.v b/test-suite/bugs/opened/4701.v new file mode 100644 index 0000000000..9286f0f1f0 --- /dev/null +++ b/test-suite/bugs/opened/4701.v @@ -0,0 +1,23 @@ +(*Suppose we have*) + + Inductive my_if {A B} : bool -> Type := + | then_case (_ : A) : my_if true + | else_case (_ : B) : my_if false. + Notation "'If' b 'Then' A 'Else' B" := (@my_if A B b) (at level 10). + +(*then here are three inductive type declarations that work:*) + + Inductive I1 := + | i1 (x : I1). + Inductive I2 := + | i2 (x : nat). + Inductive I3 := + | i3 (b : bool) (x : If b Then I3 Else nat). + +(*and here is one that does not, despite being equivalent to [I3]:*) + + Fail Inductive I4 := + | i4 (b : bool) (x : if b then I4 else nat). (* Error: Non strictly positive occurrence of "I4" in + "forall b : bool, (if b then I4 else nat) -> I4". *) + +(*I think this one should work. I believe this is a conservative extension over CIC: Since [match] statements returning types can always be re-encoded as inductive type families, the analysis should be independent of whether the constructor uses an inductive or a [match] statement.*) diff --git a/test-suite/bugs/opened/4717.v b/test-suite/bugs/opened/4717.v new file mode 100644 index 0000000000..9ad4746723 --- /dev/null +++ b/test-suite/bugs/opened/4717.v @@ -0,0 +1,19 @@ +(*See below. They sometimes work, and sometimes do not. Is this a bug?*) + +Require Import Omega Psatz. + +Definition foo := nat. + +Goal forall (n : foo), 0 = n - n. +Proof. intros. omega. (* works *) Qed. + +Goal forall (x n : foo), x = x + n - n. +Proof. + intros. + Fail omega. (* Omega can't solve this system *) + Fail lia. (* Cannot find witness. *) + unfold foo in *. + omega. (* works *) +Qed. + +(* Guillaume Melquiond: What matters is the equality. In the first case, it is @eq nat. In the second case, it is @eq foo. The same issue exists for ring and field. So it is not a bug, but it is worth fixing.*) diff --git a/test-suite/bugs/opened/4721.v b/test-suite/bugs/opened/4721.v new file mode 100644 index 0000000000..1f184b3930 --- /dev/null +++ b/test-suite/bugs/opened/4721.v @@ -0,0 +1,13 @@ +Variables S1 S2 : Set. + +Goal @eq Type S1 S2 -> @eq Type S1 S2. +intro H. +Fail tauto. +assumption. +Qed. + +(*This is in 8.5pl1, and Matthieq Sozeau says: "That's a regression in tauto indeed, which now requires exact equality of the universes, through a non linear goal pattern matching: +match goal with ?X1 |- ?X1 forces both instances of X1 to be convertible, +with no additional universe constraints currently, but the two types are +initially different. This can be fixed easily to allow the same flexibility +as in 8.4 (or assumption) to unify the universes as well."*) diff --git a/test-suite/bugs/opened/4728.v b/test-suite/bugs/opened/4728.v new file mode 100644 index 0000000000..230b4beb6c --- /dev/null +++ b/test-suite/bugs/opened/4728.v @@ -0,0 +1,72 @@ +(*I'd like the final [Check] in the following to work:*) + +Ltac fin_eta_expand := + [ > lazymatch goal with + | [ H : _ |- _ ] => clear H + end.. + | lazymatch goal with + | [ H : ?T |- ?T ] + => exact H + | [ |- ?G ] + => fail 0 "No hypothesis matching" G + end ]; + let n := numgoals in + tryif constr_eq numgoals 0 + then idtac + else fin_eta_expand. + +Ltac pre_eta_expand x := + let T := type of x in + let G := match goal with |- ?G => G end in + unify T G; + unshelve econstructor; + destruct x; + fin_eta_expand. + +Ltac eta_expand x := + let v := constr:(ltac:(pre_eta_expand x)) in + idtac v; + let v := (eval cbv beta iota zeta in v) in + exact v. + +Notation eta_expand x := (ltac:(eta_expand x)) (only parsing). + +Ltac partial_unify eqn := + lazymatch eqn with + | ?x = ?x => idtac + | ?f ?x = ?g ?y + => partial_unify (f = g); + (tryif unify x y then + idtac + else tryif has_evar x then + unify x y + else tryif has_evar y then + unify x y + else + idtac) + | ?x = ?y + => idtac; + (tryif unify x y then + idtac + else tryif has_evar x then + unify x y + else tryif has_evar y then + unify x y + else + idtac) + end. + +Tactic Notation "{" open_constr(old_record) "with" open_constr(new_record) "}" := + let old_record' := eta_expand old_record in + partial_unify (old_record = new_record); + eexact new_record. + +Set Implicit Arguments. +Record prod A B := pair { fst : A ; snd : B }. +Infix "*" := prod : type_scope. +Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) : core_scope. + +Notation "{ old 'with' new }" := (ltac:({ old with new })) (only parsing). + +Check ltac:({ (1, 1) with {| snd := 2 |} }). +Fail Check { (1, 1) with {| snd := 2 |} }. (* Error: Cannot infer this placeholder of type "Type"; should succeed *) diff --git a/test-suite/bugs/opened/4755.v b/test-suite/bugs/opened/4755.v new file mode 100644 index 0000000000..9cc0d361ea --- /dev/null +++ b/test-suite/bugs/opened/4755.v @@ -0,0 +1,34 @@ +(*I'm not sure which behavior is better. But if the change is intentional, it should be documented (I don't think it is), and it'd be nice if there were a flag for this, or if -compat 8.4 restored the old behavior.*) + +Require Import Coq.Setoids.Setoid Coq.Classes.Morphisms. +Definition f (v : option nat) := match v with + | Some k => Some k + | None => None + end. + +Axioms F G : (option nat -> option nat) -> Prop. +Axiom FG : forall f, f None = None -> F f = G f. + +Axiom admit : forall {T}, T. + +Existing Instance eq_Reflexive. + +Global Instance foo (A := nat) + : Proper ((pointwise_relation _ eq) + ==> eq ==> forall_relation (fun _ => Basics.flip Basics.impl)) + (@option_rect A (fun _ => Prop)) | 0. +exact admit. +Qed. + +Global Instance bar (A := nat) + : Proper ((pointwise_relation _ eq) + ==> eq ==> eq ==> Basics.flip Basics.impl) + (@option_rect A (fun _ => Prop)) | 0. +exact admit. +Qed. + +Goal forall k, option_rect (fun _ => Prop) (fun v : nat => v = v /\ F f) True k. +Proof. + intro. + pose proof (_ : (Proper (_ ==> eq ==> _) and)). + Fail setoid_rewrite (FG _ _); []. (* In 8.5: Error: Tactic failure: Incorrect number of goals (expected 2 tactics); works in 8.4 *) diff --git a/test-suite/bugs/opened/4771.v b/test-suite/bugs/opened/4771.v new file mode 100644 index 0000000000..396d74bdbf --- /dev/null +++ b/test-suite/bugs/opened/4771.v @@ -0,0 +1,22 @@ +Module Type Foo. + +Parameter Inline t : nat. + +End Foo. + +Module F(X : Foo). + +Tactic Notation "foo" ref(x) := idtac. + +Ltac g := foo X.t. + +End F. + +Module N. +Definition t := 0 + 0. +End N. + +Module K := F(N). + +(* Was +Anomaly: Uncaught exception Not_found. Please report. *) diff --git a/test-suite/bugs/opened/4778.v b/test-suite/bugs/opened/4778.v new file mode 100644 index 0000000000..633d158e96 --- /dev/null +++ b/test-suite/bugs/opened/4778.v @@ -0,0 +1,35 @@ +Require Import Coq.Setoids.Setoid Coq.Classes.Morphisms. +Definition f (v : option nat) := match v with + | Some k => Some k + | None => None + end. + +Axioms F G : (option nat -> option nat) -> Prop. +Axiom FG : forall f, f None = None -> F f = G f. + +Axiom admit : forall {T}, T. + +Existing Instance eq_Reflexive. + +(* This instance is needed in 8.4, but is useless in 8.5 *) +Global Instance foo (A := nat) + : Proper ((pointwise_relation _ eq) + ==> eq ==> forall_relation (fun _ => Basics.flip Basics.impl)) + (@option_rect A (fun _ => Prop)) | 0. +exact admit. +Qed. + +(* +(* This is required in 8.5, but useless in 8.4 *) +Global Instance bar (A := nat) + : Proper ((pointwise_relation _ eq) + ==> eq ==> eq ==> Basics.flip Basics.impl) + (@option_rect A (fun _ => Prop)) | 0. +exact admit. +Qed. +*) + +Goal forall k, option_rect (fun _ => Prop) (fun v : nat => v = v /\ F f) True k. Proof. + intro. + pose proof (_ : (Proper (_ ==> eq ==> _) and)). + Fail setoid_rewrite (FG _ _); [ | reflexivity.. ]. (* this should succeed without [Fail], as it does in 8.4 *) diff --git a/test-suite/bugs/opened/4781.v b/test-suite/bugs/opened/4781.v new file mode 100644 index 0000000000..8b651ac22e --- /dev/null +++ b/test-suite/bugs/opened/4781.v @@ -0,0 +1,94 @@ +Ltac force_clear := + clear; + repeat match goal with + | [ H : _ |- _ ] => clear H + | [ H := _ |- _ ] => clearbody H + end. + +Class abstract_term {T} (x : T) := by_abstract_term : T. +Hint Extern 0 (@abstract_term ?T ?x) => force_clear; change T; abstract (exact x) : typeclass_instances. + +Goal True. +(* These work: *) + let term := constr:(I) in + let T := type of term in + let x := constr:((_ : abstract_term term) : T) in + pose x. + let term := constr:(I) in + let T := type of term in + let x := constr:((_ : abstract_term term) : T) in + let x := (eval cbv iota in (let v : T := x in v)) in + pose x. + let term := constr:(I) in + let T := type of term in + let x := constr:((_ : abstract_term term) : T) in + let x := match constr:(Set) with ?y => constr:(y) end in + pose x. +(* This fails with an error: *) + Fail let term := constr:(I) in + let T := type of term in + let x := constr:((_ : abstract_term term) : T) in + let x := match constr:(x) with ?y => constr:(y) end in + pose x. (* The command has indeed failed with message: +Error: Variable y should be bound to a term. *) +(* And the rest fail with Anomaly: Uncaught exception Not_found. Please report. *) + Fail let term := constr:(I) in + let T := type of term in + let x := constr:((_ : abstract_term term) : T) in + let x := match constr:(x) with ?y => y end in + pose x. + Fail let term := constr:(I) in + let T := type of term in + let x := constr:((_ : abstract_term term) : T) in + let x := (eval cbv iota in x) in + pose x. + Fail let term := constr:(I) in + let T := type of term in + let x := constr:((_ : abstract_term term) : T) in + let x := type of x in + pose x. (* should succeed *) + Fail let term := constr:(I) in + let T := type of term in + let x := constr:(_ : abstract_term term) in + let x := type of x in + pose x. (* should succeed *) + +(*Apparently what [cbv iota] doesn't see can't hurt it, and [pose] is perfectly happy with abstracted lemmas only some of the time. + +Even stranger, consider:*) + let term := constr:(I) in + let T := type of term in + let x := constr:((_ : abstract_term term) : T) in + let y := (eval cbv iota in (let v : T := x in v)) in + pose y; + let x' := fresh "x'" in + pose x as x'. + let x := (eval cbv delta [x'] in x') in + pose x; + let z := (eval cbv iota in x) in + pose z. + +(*This works fine. But if I change the period to a semicolon, I get:*) + + Fail let term := constr:(I) in + let T := type of term in + let x := constr:((_ : abstract_term term) : T) in + let y := (eval cbv iota in (let v : T := x in v)) in + pose y; + let x' := fresh "x'" in + pose x as x'; + let x := (eval cbv delta [x'] in x') in + pose x. (* Anomaly: Uncaught exception Not_found. Please report. *) + (* should succeed *) +(*and if I use the second one instead of [pose x] (note that using [idtac] works fine), I get:*) + + Fail let term := constr:(I) in + let T := type of term in + let x := constr:((_ : abstract_term term) : T) in + let y := (eval cbv iota in (let v : T := x in v)) in + pose y; + let x' := fresh "x'" in + pose x as x'; + let x := (eval cbv delta [x'] in x') in + let z := (eval cbv iota in x) in (* Error: Variable x should be bound to a term. *) + idtac. (* should succeed *) diff --git a/test-suite/bugs/opened/4803.v b/test-suite/bugs/opened/4803.v index 3ca5c095f5..4530548b8f 100644 --- a/test-suite/bugs/opened/4803.v +++ b/test-suite/bugs/opened/4803.v @@ -25,10 +25,24 @@ Check [ _ ]%list : list _. Check [ _ ]%vector : Vector.t _ _. Check [ _ ; _ ]%list : list _. Check [ _ ; _ ]%vector : Vector.t _ _. -Fail Check [ _ ; _ ]%mylist : mylist _. (* ideally, this should work, but that requires removing notations from the parser; it should be added to Compat/Coq84.v *) +Check [ _ ; _ ]%mylist : mylist _. Check [ _ ; _ ; _ ]%list : list _. Check [ _ ; _ ; _ ]%vector : Vector.t _ _. -Fail Check [ _ ; _ ; _ ]%mylist : mylist _. (* ideally, this should work, but that requires removing notations from the parser *) +Check [ _ ; _ ; _ ]%mylist : mylist _. Check [ _ ; _ ; _ ; _ ]%list : list _. Check [ _ ; _ ; _ ; _ ]%vector : Vector.t _ _. -Fail Check [ _ ; _ ; _ ; _ ]%mylist : mylist _. (* ideally, this should work, but that requires removing notations from the parser *) +Check [ _ ; _ ; _ ; _ ]%mylist : mylist _. + +(** Now check that we can add and then remove notations from the parser *) +(* We should be able to stick some vernacular here to remove [] from the parser *) +Fail Remove Notation "[]". +Goal True. + (* This should not be a syntax error; before moving this file to closed, uncomment this line. *) + (* idtac; []. *) + constructor. +Qed. + +Check { _ : _ & _ }. +Reserved Infix "&" (at level 0). +Fail Remove Infix "&". +(* Check { _ : _ & _ }. *) |