diff options
Diffstat (limited to 'test-suite/bugs')
65 files changed, 762 insertions, 130 deletions
diff --git a/test-suite/bugs/closed/1519.v b/test-suite/bugs/closed/1519.v index 98e3e214..de60de59 100644 --- a/test-suite/bugs/closed/1519.v +++ b/test-suite/bugs/closed/1519.v @@ -2,7 +2,7 @@ Section S. Variable A:Prop. Variable W:A. - + Remark T: A -> A. intro Z. rename W into Z_. diff --git a/test-suite/bugs/closed/1780.v b/test-suite/bugs/closed/1780.v index 3929fbae..ade4462a 100644 --- a/test-suite/bugs/closed/1780.v +++ b/test-suite/bugs/closed/1780.v @@ -1,12 +1,12 @@ Definition bug := Eval vm_compute in eq_rect. (* bug: -Error: Illegal application (Type Error): +Error: Illegal application (Type Error): The term "eq" of type "forall A : Type, A -> A -> Prop" cannot be applied to the terms "x" : "A" "P" : "A -> Type" "x0" : "A" -The 1st term has type "A" which should be coercible to +The 1st term has type "A" which should be coercible to "Type". *) diff --git a/test-suite/bugs/closed/shouldfail/2006.v b/test-suite/bugs/closed/shouldfail/2006.v new file mode 100644 index 00000000..91a16f95 --- /dev/null +++ b/test-suite/bugs/closed/shouldfail/2006.v @@ -0,0 +1,23 @@ +(* Take the type constraint on Record into account *) + +Definition Type1 := Type. +Record R : Type1 := { p:Type1 }. (* was accepted before trunk revision 11619 *) + +(* +Remarks: + +- The behaviour was inconsistent with the one of Inductive, e.g. + + Inductive R : Type1 := Build_R : Type1 -> R. + + was correctly refused. + +- CoRN makes some use of the following configuration: + + Definition CProp := Type. + Record R : CProp := { ... }. + + CoRN may have to change the CProp definition into a notation if the + preservation of the former semantics of Record type constraints + turns to be required. +*) diff --git a/test-suite/bugs/closed/shouldfail/2251.v b/test-suite/bugs/closed/shouldfail/2251.v new file mode 100644 index 00000000..642717f4 --- /dev/null +++ b/test-suite/bugs/closed/shouldfail/2251.v @@ -0,0 +1,5 @@ +(* Check that rewrite does not apply to single evars *) + +Lemma evar_rewrite : (forall a : nat, a = 0 -> True) -> True. +intros; eapply H. (* goal is ?30 = nil *) +rewrite plus_n_Sm. diff --git a/test-suite/bugs/closed/shouldsucceed/1100.v b/test-suite/bugs/closed/shouldsucceed/1100.v index 6d619c74..32c78b4b 100644 --- a/test-suite/bugs/closed/shouldsucceed/1100.v +++ b/test-suite/bugs/closed/shouldsucceed/1100.v @@ -6,7 +6,7 @@ Parameter PQ : forall n, P n <-> Q n. Lemma PQ2 : forall n, P n -> Q n. intros. - rewrite PQ in H. + rewrite PQ in H. trivial. Qed. diff --git a/test-suite/bugs/closed/shouldsucceed/1322.v b/test-suite/bugs/closed/shouldsucceed/1322.v index 7e21aa7c..1ec7d452 100644 --- a/test-suite/bugs/closed/shouldsucceed/1322.v +++ b/test-suite/bugs/closed/shouldsucceed/1322.v @@ -7,7 +7,7 @@ Variable I_eq :I -> I -> Prop. Variable I_eq_equiv : Setoid_Theory I I_eq. (* Add Relation I I_eq - reflexivity proved by I_eq_equiv.(Seq_refl I I_eq) + reflexivity proved by I_eq_equiv.(Seq_refl I I_eq) symmetry proved by I_eq_equiv.(Seq_sym I I_eq) transitivity proved by I_eq_equiv.(Seq_trans I I_eq) as I_eq_relation. *) diff --git a/test-suite/bugs/closed/shouldsucceed/1411.v b/test-suite/bugs/closed/shouldsucceed/1411.v index e330d46f..a1a7b288 100644 --- a/test-suite/bugs/closed/shouldsucceed/1411.v +++ b/test-suite/bugs/closed/shouldsucceed/1411.v @@ -23,7 +23,7 @@ Program Fixpoint fetch t p (x:Exact t p) {struct t} := match t, p with | No p' , nil => p' | No p' , _::_ => unreachable nat _ - | Br l r, nil => unreachable nat _ + | Br l r, nil => unreachable nat _ | Br l r, true::t => fetch l t _ | Br l r, false::t => fetch r t _ end. diff --git a/test-suite/bugs/closed/shouldsucceed/1414.v b/test-suite/bugs/closed/shouldsucceed/1414.v index d3c00808..495a16bc 100644 --- a/test-suite/bugs/closed/shouldsucceed/1414.v +++ b/test-suite/bugs/closed/shouldsucceed/1414.v @@ -7,8 +7,8 @@ Inductive t : Set := | Node : t -> data -> t -> Z -> t. Parameter avl : t -> Prop. -Parameter bst : t -> Prop. -Parameter In : data -> t -> Prop. +Parameter bst : t -> Prop. +Parameter In : data -> t -> Prop. Parameter cardinal : t -> nat. Definition card2 (s:t*t) := let (s1,s2) := s in cardinal s1 + cardinal s2. @@ -16,26 +16,25 @@ Parameter split : data -> t -> t*(bool*t). Parameter join : t -> data -> t -> t. Parameter add : data -> t -> t. -Program Fixpoint union - (s:t*t) - (hb1: bst (fst s))(ha1: avl (fst s))(hb2: bst (snd s))(hb2: avl (snd s)) - { measure card2 s } : - {s' : t | bst s' /\ avl s' /\ forall x, In x s' <-> In x (fst s) \/ In x (snd -s)} := - match s with - | (Leaf,t2) => t2 - | (t1,Leaf) => t1 - | (Node l1 v1 r1 h1, Node l2 v2 r2 h2) => +Program Fixpoint union + (s u:t) + (hb1: bst s)(ha1: avl s)(hb2: bst u)(hb2: avl u) + { measure (cardinal s + cardinal u) } : + {s' : t | bst s' /\ avl s' /\ forall x, In x s' <-> In x s \/ In x u} := + match s, u with + | Leaf,t2 => t2 + | t1,Leaf => t1 + | Node l1 v1 r1 h1, Node l2 v2 r2 h2 => if (Z_ge_lt_dec h1 h2) then - if (Z_eq_dec h2 1) - then add v2 (fst s) + if (Z_eq_dec h2 1) + then add v2 s else - let (l2', r2') := split v1 (snd s) in - join (union (l1,l2') _ _ _ _) v1 (union (r1,snd r2') _ _ _ _) + let (l2', r2') := split v1 u in + join (union l1 l2' _ _ _ _) v1 (union r1 (snd r2') _ _ _ _) else - if (Z_eq_dec h1 1) - then add v1 (snd s) + if (Z_eq_dec h1 1) + then add v1 s else - let (l1', r1') := split v2 (fst s) in - join (union (l1',l2) _ _ _ _) v2 (union (snd r1',r2) _ _ _ _) - end. + let (l1', r1') := split v2 u in + join (union l1' l2 _ _ _ _) v2 (union (snd r1') r2 _ _ _ _) + end. diff --git a/test-suite/bugs/opened/shouldnotfail/1416.v b/test-suite/bugs/closed/shouldsucceed/1416.v index c6f4302d..da67d9b0 100644 --- a/test-suite/bugs/opened/shouldnotfail/1416.v +++ b/test-suite/bugs/closed/shouldsucceed/1416.v @@ -4,12 +4,12 @@ Record Place (Env A: Type) : Type := { read: Env -> A ; write: Env -> A -> Env ; write_read: forall (e:Env), (write e (read e))=e -}. +}. Hint Rewrite -> write_read: placeeq. Record sumPl (Env A B: Type) (vL:(Place Env A)) (vR:(Place Env B)) : Type := - { + { mkEnv: A -> B -> Env ; mkEnv2writeL: forall (e:Env) (x:A), (mkEnv x (read vR e))=(write vL e x) }. diff --git a/test-suite/bugs/closed/shouldsucceed/1425.v b/test-suite/bugs/closed/shouldsucceed/1425.v index 8e26209a..6be30174 100644 --- a/test-suite/bugs/closed/shouldsucceed/1425.v +++ b/test-suite/bugs/closed/shouldsucceed/1425.v @@ -1,4 +1,4 @@ -Require Import Setoid. +Require Import Setoid. Parameter recursion : forall A : Set, A -> (nat -> A -> A) -> nat -> A. diff --git a/test-suite/bugs/closed/shouldsucceed/1446.v b/test-suite/bugs/closed/shouldsucceed/1446.v index d4e7cea8..8cb2d653 100644 --- a/test-suite/bugs/closed/shouldsucceed/1446.v +++ b/test-suite/bugs/closed/shouldsucceed/1446.v @@ -1,8 +1,8 @@ Lemma not_true_eq_false : forall (b:bool), b <> true -> b = false. Proof. - destruct b;intros;trivial. - elim H. - exact (refl_equal true). + destruct b;intros;trivial. + elim H. + exact (refl_equal true). Qed. Section BUG. @@ -13,7 +13,7 @@ Section BUG. Hypothesis H1 : b <> true. Goal False. - rewrite (not_true_eq_false _ H) in * |-. + rewrite (not_true_eq_false _ H) in * |-. contradiction. Qed. diff --git a/test-suite/bugs/closed/shouldsucceed/1507.v b/test-suite/bugs/closed/shouldsucceed/1507.v index b484c7dc..f1872a2b 100644 --- a/test-suite/bugs/closed/shouldsucceed/1507.v +++ b/test-suite/bugs/closed/shouldsucceed/1507.v @@ -2,16 +2,16 @@ Implementing reals a la Stolzenberg Danko Ilik, March 2007 - svn revision: $Id: 1507.v 10068 2007-08-10 12:06:59Z notin $ + svn revision: $Id$ XField.v -- (unfinished) axiomatisation of the theories of real and rational intervals. *) -Definition associative (A:Type)(op:A->A->A) := +Definition associative (A:Type)(op:A->A->A) := forall x y z:A, op (op x y) z = op x (op y z). -Definition commutative (A:Type)(op:A->A->A) := +Definition commutative (A:Type)(op:A->A->A) := forall x y:A, op x y = op y x. Definition trichotomous (A:Type)(R:A->A->Prop) := @@ -19,7 +19,7 @@ Definition trichotomous (A:Type)(R:A->A->Prop) := Definition relation (A:Type) := A -> A -> Prop. Definition reflexive (A:Type)(R:relation A) := forall x:A, R x x. -Definition transitive (A:Type)(R:relation A) := +Definition transitive (A:Type)(R:relation A) := forall x y z:A, R x y -> R y z -> R x z. Definition symmetric (A:Type)(R:relation A) := forall x y:A, R x y -> R y x. @@ -52,7 +52,7 @@ Record I (grnd:Set)(le:grnd->grnd->Prop) : Type := Imake { Iplus_opp_r : forall x:Icar, Ic (Iplus x (Iopp x)) (Izero); Imult_inv_r : forall x:Icar, ~(Ic x Izero) -> Ic (Imult x (Iinv x)) Ione; (* distributive laws *) - Imult_plus_distr_l : forall x x' y y' z z' z'', + Imult_plus_distr_l : forall x x' y y' z z' z'', Ic x x' -> Ic y y' -> Ic z z' -> Ic z z'' -> Ic (Imult (Iplus x y) z) (Iplus (Imult x' z') (Imult y' z'')); (* order and lattice structure *) @@ -70,7 +70,7 @@ Record I (grnd:Set)(le:grnd->grnd->Prop) : Type := Imake { Ic_sym : symmetric _ Ic }. -Definition interval_set (X:Set)(le:X->X->Prop) := +Definition interval_set (X:Set)(le:X->X->Prop) := (interval X le) -> Prop. (* can be Set as well *) Check interval_set. Check Ic. @@ -101,7 +101,7 @@ Record N (grnd:Set)(le:grnd->grnd->Prop)(grndI:I grnd le) : Type := Nmake { Nplus_opp_r : forall x:Ncar, Nc (Nplus x (Nopp x)) (Nzero); Nmult_inv_r : forall x:Ncar, ~(Nc x Nzero) -> Nc (Nmult x (Ninv x)) None; (* distributive laws *) - Nmult_plus_distr_l : forall x x' y y' z z' z'', + Nmult_plus_distr_l : forall x x' y y' z z' z'', Nc x x' -> Nc y y' -> Nc z z' -> Nc z z'' -> Nc (Nmult (Nplus x y) z) (Nplus (Nmult x' z') (Nmult y' z'')); (* order and lattice structure *) diff --git a/test-suite/bugs/closed/shouldsucceed/1568.v b/test-suite/bugs/closed/shouldsucceed/1568.v index 9f10f749..3609e9c8 100644 --- a/test-suite/bugs/closed/shouldsucceed/1568.v +++ b/test-suite/bugs/closed/shouldsucceed/1568.v @@ -3,7 +3,7 @@ CoInductive A: Set := with B: Set := mk_B: A -> B. -CoFixpoint a:A := mk_A b +CoFixpoint a:A := mk_A b with b:B := mk_B a. Goal b = match a with mk_A a1 => a1 end. diff --git a/test-suite/bugs/closed/shouldsucceed/1576.v b/test-suite/bugs/closed/shouldsucceed/1576.v index c9ebbd14..3621f7a1 100644 --- a/test-suite/bugs/closed/shouldsucceed/1576.v +++ b/test-suite/bugs/closed/shouldsucceed/1576.v @@ -13,8 +13,8 @@ End TC. Module Type TD. Declare Module B: TB . -Declare Module C: TC - with Module B := B . +Declare Module C: TC + with Module B := B . End TD. Module Type TE. @@ -25,7 +25,7 @@ Module Type TF. Declare Module E: TE. End TF. -Module G (D: TD). +Module G (D: TD). Module B' := D.C.B. End G. diff --git a/test-suite/bugs/closed/shouldsucceed/1582.v b/test-suite/bugs/closed/shouldsucceed/1582.v index 47953a66..be5d3dd2 100644 --- a/test-suite/bugs/closed/shouldsucceed/1582.v +++ b/test-suite/bugs/closed/shouldsucceed/1582.v @@ -1,12 +1,12 @@ Require Import Peano_dec. -Definition fact_F : +Definition fact_F : forall (n:nat), (forall m, m<n -> nat) -> nat. -refine +refine (fun n fact_rec => - if eq_nat_dec n 0 then + if eq_nat_dec n 0 then 1 else let fn := fact_rec (n-1) _ in diff --git a/test-suite/bugs/closed/shouldsucceed/1618.v b/test-suite/bugs/closed/shouldsucceed/1618.v index a90290bf..a9b067ce 100644 --- a/test-suite/bugs/closed/shouldsucceed/1618.v +++ b/test-suite/bugs/closed/shouldsucceed/1618.v @@ -6,7 +6,7 @@ Definition A_size (a: A) : nat := | A1 n => 0 end. -Require Import Recdef. +Require Import Recdef. Function n3 (P: A -> Prop) (f: forall n, P (A1 n)) (a: A) {struct a} : P a := match a return (P a) with diff --git a/test-suite/bugs/closed/shouldsucceed/1634.v b/test-suite/bugs/closed/shouldsucceed/1634.v index e0c540f3..0150c250 100644 --- a/test-suite/bugs/closed/shouldsucceed/1634.v +++ b/test-suite/bugs/closed/shouldsucceed/1634.v @@ -18,7 +18,7 @@ Add Parametric Relation a : (S a) Seq Goal forall (a : A) (x y : S a), Seq x y -> Seq x y. intros a x y H. - setoid_replace x with y. + setoid_replace x with y. reflexivity. trivial. Qed. diff --git a/test-suite/bugs/closed/shouldsucceed/1643.v b/test-suite/bugs/closed/shouldsucceed/1643.v index 4114987d..879a65b1 100644 --- a/test-suite/bugs/closed/shouldsucceed/1643.v +++ b/test-suite/bugs/closed/shouldsucceed/1643.v @@ -10,7 +10,6 @@ Definition decomp_func (s:Str) := Theorem decomp s: s = decomp_func s. Proof. - intros s. case s; simpl; reflexivity. Qed. diff --git a/test-suite/bugs/closed/shouldsucceed/1683.v b/test-suite/bugs/closed/shouldsucceed/1683.v index 1571ee20..3e99694b 100644 --- a/test-suite/bugs/closed/shouldsucceed/1683.v +++ b/test-suite/bugs/closed/shouldsucceed/1683.v @@ -30,7 +30,7 @@ Add Parametric Relation A : (ms_type A) (ms_eq A) Hypothesis foobar : forall n, ms_eq CR (IRasCR (foo IR n)) (foo CRasCRing n). Goal forall (b:ms_type CR), - ms_eq CR (IRasCR (foo IR O)) b -> + ms_eq CR (IRasCR (foo IR O)) b -> ms_eq CR (IRasCR (foo IR O)) b. intros b H. rewrite foobar. diff --git a/test-suite/bugs/closed/shouldsucceed/1711.v b/test-suite/bugs/closed/shouldsucceed/1711.v new file mode 100644 index 00000000..e16612e3 --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/1711.v @@ -0,0 +1,34 @@ +(* Test for evar map consistency - was failing at some point and was *) +(* assumed to be solved from revision 10151 (but using a bad fix) *) + +Require Import List. +Set Implicit Arguments. + +Inductive rose : Set := Rose : nat -> list rose -> rose. + +Section RoseRec. +Variables (P: rose -> Set)(L: list rose -> Set). +Hypothesis + (R: forall n rs, L rs -> P (Rose n rs)) + (Lnil: L nil) + (Lcons: forall r rs, P r -> L rs -> L (cons r rs)). + +Fixpoint rose_rec2 (t:rose) {struct t} : P t := + match t as x return P x with + | Rose n rs => + R n ((fix rs_ind (l' : list rose): L l' := + match l' as x return L x with + | nil => Lnil + | cons t tl => Lcons (rose_rec2 t) (rs_ind tl) + end) + rs) + end. +End RoseRec. + +Lemma rose_map : rose -> rose. +Proof. intro H; elim H using rose_rec2 with + (L:=fun _ => list rose); (* was assumed to fail here *) +(* (L:=fun (_:list rose) => list rose); *) + clear H; simpl; intros. + exact (Rose n rs). exact nil. exact (H::H0). +Defined. diff --git a/test-suite/bugs/closed/shouldsucceed/1738.v b/test-suite/bugs/closed/shouldsucceed/1738.v index 0deed366..c2926a2b 100644 --- a/test-suite/bugs/closed/shouldsucceed/1738.v +++ b/test-suite/bugs/closed/shouldsucceed/1738.v @@ -5,10 +5,10 @@ Module SomeSetoids (Import M:FSetInterface.S). Lemma Equal_refl : forall s, s[=]s. Proof. red; split; auto. Qed. -Add Relation t Equal - reflexivity proved by Equal_refl +Add Relation t Equal + reflexivity proved by Equal_refl symmetry proved by eq_sym - transitivity proved by eq_trans + transitivity proved by eq_trans as EqualSetoid. Add Morphism Empty with signature Equal ==> iff as Empty_m. diff --git a/test-suite/bugs/closed/shouldsucceed/1740.v b/test-suite/bugs/closed/shouldsucceed/1740.v index d9ce546a..ec4a7a6b 100644 --- a/test-suite/bugs/closed/shouldsucceed/1740.v +++ b/test-suite/bugs/closed/shouldsucceed/1740.v @@ -17,7 +17,7 @@ Goal f = | n, O => n | _, _ => O end. - unfold f. + unfold f. reflexivity. Qed. diff --git a/test-suite/bugs/closed/shouldsucceed/1775.v b/test-suite/bugs/closed/shouldsucceed/1775.v index dab4120b..932949a3 100644 --- a/test-suite/bugs/closed/shouldsucceed/1775.v +++ b/test-suite/bugs/closed/shouldsucceed/1775.v @@ -13,7 +13,7 @@ Goal forall s k k' m, (pl k' (nexists (fun w => (nexists (fun b => pl (pair w w) (pl (pair s b) (nexists (fun w0 => (nexists (fun a => pl (pair b w0) - (nexists (fun w1 => (nexists (fun c => pl + (nexists (fun w1 => (nexists (fun c => pl (pair a w1) (pl (pair a c) k))))))))))))))) m. intros. eapply plImp; [ | eauto | intros ]. diff --git a/test-suite/bugs/closed/shouldsucceed/1776.v b/test-suite/bugs/closed/shouldsucceed/1776.v index abf85455..58491f9d 100644 --- a/test-suite/bugs/closed/shouldsucceed/1776.v +++ b/test-suite/bugs/closed/shouldsucceed/1776.v @@ -10,7 +10,7 @@ Definition nexists (P:nat -> nat -> Prop) : nat -> Prop := Goal forall a A m, True -> - (pl A (nexists (fun x => (nexists + (pl A (nexists (fun x => (nexists (fun y => pl (pair a (S x)) (pair a (S y))))))) m. Proof. intros. diff --git a/test-suite/bugs/closed/shouldsucceed/1784.v b/test-suite/bugs/closed/shouldsucceed/1784.v index 5855b168..718b0e86 100644 --- a/test-suite/bugs/closed/shouldsucceed/1784.v +++ b/test-suite/bugs/closed/shouldsucceed/1784.v @@ -56,16 +56,16 @@ Require Import Program. Program Fixpoint lt_dec (x y:sv) { struct x } : {slt x y}+{~slt x y} := match x with - | I x => + | I x => match y with | I y => if (Z_eq_dec x y) then in_left else in_right | S ys => in_right end - | S xs => + | S xs => match y with | I y => in_right | S ys => - let fix list_in (xs ys:list sv) {struct xs} : + let fix list_in (xs ys:list sv) {struct xs} : {slist_in xs ys} + {~slist_in xs ys} := match xs with | nil => in_left @@ -76,8 +76,8 @@ Program Fixpoint lt_dec (x y:sv) { struct x } : {slt x y}+{~slt x y} := | y::ys => if lt_dec x y then in_left else if elem_in ys then in_left else in_right end - in - if elem_in ys then + in + if elem_in ys then if list_in xs ys then in_left else in_right else in_right end @@ -90,12 +90,12 @@ Next Obligation. intro H; inversion H. Defined. Next Obligation. intro H; inversion H. Defined. Next Obligation. intro H; inversion H; subst. Defined. Next Obligation. - intro H1; contradict H. inversion H1; subst. assumption. + intro H1; contradict H. inversion H1; subst. assumption. contradict H0; assumption. Defined. Next Obligation. intro H1; contradict H0. inversion H1; subst. assumption. Defined. Next Obligation. - intro H0; contradict H. inversion H0; subst. assumption. Defined. + intro H1; contradict H. inversion H1; subst. assumption. Defined. Next Obligation. intro H0; contradict H. inversion H0; subst; auto. Defined. diff --git a/test-suite/bugs/closed/shouldsucceed/1791.v b/test-suite/bugs/closed/shouldsucceed/1791.v index 694f056e..be0e8ae8 100644 --- a/test-suite/bugs/closed/shouldsucceed/1791.v +++ b/test-suite/bugs/closed/shouldsucceed/1791.v @@ -9,7 +9,7 @@ Definition k1 := k0 -> k0. (** iterating X n times *) Fixpoint Pow (X:k1)(k:nat){struct k}:k1:= match k with 0 => fun X => X - | S k' => fun A => X (Pow X k' A) + | S k' => fun A => X (Pow X k' A) end. Parameter Bush: k1. diff --git a/test-suite/bugs/closed/shouldsucceed/1844.v b/test-suite/bugs/closed/shouldsucceed/1844.v index 545f2615..5627612f 100644 --- a/test-suite/bugs/closed/shouldsucceed/1844.v +++ b/test-suite/bugs/closed/shouldsucceed/1844.v @@ -188,7 +188,7 @@ with exec_finish: function -> outcome -> store -> value -> store -> Prop := with exec_function: function -> store -> value -> store -> Prop := | exec_function_intro: forall f st out st1 v st', - exec f.(fn_body) st out st1 -> + exec f.(fn_body) st out st1 -> exec_finish f out st1 v st' -> exec_function f st v st'. diff --git a/test-suite/bugs/closed/shouldsucceed/1891.v b/test-suite/bugs/closed/shouldsucceed/1891.v index 11124cdd..2d90a2f1 100644 --- a/test-suite/bugs/closed/shouldsucceed/1891.v +++ b/test-suite/bugs/closed/shouldsucceed/1891.v @@ -7,7 +7,7 @@ Lemma L (x: T unit): (unit -> T unit) -> unit. Proof. - refine (fun x => match x return _ with mkT n => fun g => f (g _) end). + refine (match x return _ with mkT n => fun g => f (g _) end). trivial. Qed. diff --git a/test-suite/bugs/closed/shouldsucceed/1901.v b/test-suite/bugs/closed/shouldsucceed/1901.v index 598db366..7d86adbf 100644 --- a/test-suite/bugs/closed/shouldsucceed/1901.v +++ b/test-suite/bugs/closed/shouldsucceed/1901.v @@ -2,9 +2,9 @@ Require Import Relations. Record Poset{A:Type}(Le : relation A) : Type := Build_Poset - { - Le_refl : forall x : A, Le x x; - Le_trans : forall x y z : A, Le x y -> Le y z -> Le x z; + { + Le_refl : forall x : A, Le x x; + Le_trans : forall x y z : A, Le x y -> Le y z -> Le x z; Le_antisym : forall x y : A, Le x y -> Le y x -> x = y }. Definition nat_Poset : Poset Peano.le. diff --git a/test-suite/bugs/closed/shouldsucceed/1905.v b/test-suite/bugs/closed/shouldsucceed/1905.v index fb2725c9..8c81d751 100644 --- a/test-suite/bugs/closed/shouldsucceed/1905.v +++ b/test-suite/bugs/closed/shouldsucceed/1905.v @@ -5,7 +5,7 @@ Axiom t : Set. Axiom In : nat -> t -> Prop. Axiom InE : forall (x : nat) (s:t), impl (In x s) True. -Goal forall a s, +Goal forall a s, In a s -> False. Proof. intros a s Ia. diff --git a/test-suite/bugs/closed/shouldsucceed/1918.v b/test-suite/bugs/closed/shouldsucceed/1918.v index 9d4a3e04..9d92fe12 100644 --- a/test-suite/bugs/closed/shouldsucceed/1918.v +++ b/test-suite/bugs/closed/shouldsucceed/1918.v @@ -35,7 +35,7 @@ Definition mon (X:k1) : Type := forall (A B:Set), (A -> B) -> X A -> X B. (** extensionality *) Definition ext (X:k1)(h: mon X): Prop := - forall (A B:Set)(f g:A -> B), + forall (A B:Set)(f g:A -> B), (forall a, f a = g a) -> forall r, h _ _ f r = h _ _ g r. (** first functor law *) @@ -44,7 +44,7 @@ Definition fct1 (X:k1)(m: mon X) : Prop := (** second functor law *) Definition fct2 (X:k1)(m: mon X) : Prop := - forall (A B C:Set)(f:A -> B)(g:B -> C)(x:X A), + forall (A B C:Set)(f:A -> B)(g:B -> C)(x:X A), m _ _ (g o f) x = m _ _ g (m _ _ f x). (** pack up the good properties of the approximation into @@ -60,20 +60,20 @@ Definition pEFct (F:k2) : Type := forall (X:k1), EFct X -> EFct (F X). -(** we show some closure properties of pEFct, depending on such properties +(** we show some closure properties of pEFct, depending on such properties for EFct *) Definition moncomp (X Y:k1)(mX:mon X)(mY:mon Y): mon (fun A => X(Y A)). Proof. red. - intros X Y mX mY A B f x. + intros A B f x. exact (mX (Y A)(Y B) (mY A B f) x). Defined. (** closure under composition *) Lemma compEFct (X Y:k1): EFct X -> EFct Y -> EFct (fun A => X(Y A)). Proof. - intros X Y ef1 ef2. + intros ef1 ef2. apply (mkEFct(m:=moncomp (m ef1) (m ef2))); red; intros; unfold moncomp. (* prove ext *) apply (e ef1). @@ -92,7 +92,7 @@ Proof. apply (f2 ef2). Defined. -Corollary comppEFct (F G:k2): pEFct F -> pEFct G -> +Corollary comppEFct (F G:k2): pEFct F -> pEFct G -> pEFct (fun X A => F X (G X A)). Proof. red. @@ -103,8 +103,8 @@ Defined. (** closure under sums *) Lemma sumEFct (X Y:k1): EFct X -> EFct Y -> EFct (fun A => X A + Y A)%type. Proof. - intros X Y ef1 ef2. - set (m12:=fun (A B:Set)(f:A->B) x => match x with + intros ef1 ef2. + set (m12:=fun (A B:Set)(f:A->B) x => match x with | inl y => inl _ (m ef1 f y) | inr y => inr _ (m ef2 f y) end). @@ -133,7 +133,7 @@ Proof. rewrite (f2 ef2); reflexivity. Defined. -Corollary sumpEFct (F G:k2): pEFct F -> pEFct G -> +Corollary sumpEFct (F G:k2): pEFct F -> pEFct G -> pEFct (fun X A => F X A + G X A)%type. Proof. red. @@ -144,8 +144,8 @@ Defined. (** closure under products *) Lemma prodEFct (X Y:k1): EFct X -> EFct Y -> EFct (fun A => X A * Y A)%type. Proof. - intros X Y ef1 ef2. - set (m12:=fun (A B:Set)(f:A->B) x => match x with + intros ef1 ef2. + set (m12:=fun (A B:Set)(f:A->B) x => match x with (x1,x2) => (m ef1 f x1, m ef2 f x2) end). apply (mkEFct(m:=m12)); red; intros. (* prove ext *) @@ -168,7 +168,7 @@ Proof. apply (f2 ef2). Defined. -Corollary prodpEFct (F G:k2): pEFct F -> pEFct G -> +Corollary prodpEFct (F G:k2): pEFct F -> pEFct G -> pEFct (fun X A => F X A * G X A)%type. Proof. red. @@ -220,7 +220,6 @@ Defined. (** constants in k1 *) Lemma constEFct (C:Set): EFct (fun _ => C). Proof. - intro. set (mC:=fun A B (f:A->B)(x:C) => x). apply (mkEFct(m:=mC)); red; intros; unfold mC; reflexivity. Defined. @@ -248,19 +247,19 @@ Module Type LNMIt_Type. Parameter F:k2. Parameter FpEFct: pEFct F. -Parameter mu20: k1. +Parameter mu20: k1. Definition mu2: k1:= fun A => mu20 A. Parameter mapmu2: mon mu2. Definition MItType: Type := forall G : k1, (forall X : k1, X c_k1 G -> F X c_k1 G) -> mu2 c_k1 G. Parameter MIt0 : MItType. -Definition MIt : MItType:= fun G s A t => MIt0 s t. -Definition InType : Type := - forall (X:k1)(ef:EFct X)(j: X c_k1 mu2), +Definition MIt : MItType:= fun G s A t => MIt0 s t. +Definition InType : Type := + forall (X:k1)(ef:EFct X)(j: X c_k1 mu2), NAT j (m ef) mapmu2 -> F X c_k1 mu2. Parameter In : InType. Axiom mapmu2Red : forall (A:Set)(X:k1)(ef:EFct X)(j: X c_k1 mu2) - (n: NAT j (m ef) mapmu2)(t: F X A)(B:Set)(f:A->B), + (n: NAT j (m ef) mapmu2)(t: F X A)(B:Set)(f:A->B), mapmu2 f (In ef n t) = In ef n (m (FpEFct ef) f t). Axiom MItRed : forall (G : k1) (s : forall X : k1, X c_k1 G -> F X c_k1 G)(X : k1)(ef:EFct X)(j: X c_k1 mu2) @@ -327,8 +326,8 @@ Fixpoint Pow (X:k1)(k:nat){struct k}:k1:= Fixpoint POW (k:nat)(X:k1)(m:mon X){struct k} : mon (Pow X k) := match k return mon (Pow X k) - with 0 => fun _ _ f => f - | S k' => fun _ _ f => m _ _ (POW k' m f) + with 0 => fun _ _ f => f + | S k' => fun _ _ f => m _ _ (POW k' m f) end. Module Type BushkToList_Type. diff --git a/test-suite/bugs/closed/shouldsucceed/1925.v b/test-suite/bugs/closed/shouldsucceed/1925.v index 17eb721a..4caee1c3 100644 --- a/test-suite/bugs/closed/shouldsucceed/1925.v +++ b/test-suite/bugs/closed/shouldsucceed/1925.v @@ -3,14 +3,14 @@ Require Import List. -Definition compose (A B C : Type) (g : B -> C) (f : A -> B) : A -> C := +Definition compose (A B C : Type) (g : B -> C) (f : A -> B) : A -> C := fun x : A => g(f x). -Definition map_fuse' : - forall (A B C : Type) (g : B -> C) (f : A -> B) (xs : list A), - (map g (map f xs)) = map (compose _ _ _ g f) xs +Definition map_fuse' : + forall (A B C : Type) (g : B -> C) (f : A -> B) (xs : list A), + (map g (map f xs)) = map (compose _ _ _ g f) xs := - fun A B C g f => + fun A B C g f => (fix loop (ys : list A) {struct ys} := match ys as ys return (map g (map f ys)) = map (compose _ _ _ g f) ys with diff --git a/test-suite/bugs/closed/shouldsucceed/1931.v b/test-suite/bugs/closed/shouldsucceed/1931.v index bc8be78f..930ace1d 100644 --- a/test-suite/bugs/closed/shouldsucceed/1931.v +++ b/test-suite/bugs/closed/shouldsucceed/1931.v @@ -8,7 +8,7 @@ Inductive T (A:Set) : Set := Fixpoint map (A B:Set)(f:A->B)(t:T A) : T B := match t with app t1 t2 => app (map f t1)(map f t2) - end. + end. Fixpoint subst (A B:Set)(f:A -> T B)(t:T A) :T B := match t with @@ -19,7 +19,7 @@ Fixpoint subst (A B:Set)(f:A -> T B)(t:T A) :T B := Definition k0:=Set. (** interaction of subst with map *) -Lemma substLaw1 (A:k0)(B C:Set)(f: A -> B)(g:B -> T C)(t: T A): +Lemma substLaw1 (A:k0)(B C:Set)(f: A -> B)(g:B -> T C)(t: T A): subst g (map f t) = subst (fun x => g (f x)) t. Proof. intros. diff --git a/test-suite/bugs/closed/shouldsucceed/1935.v b/test-suite/bugs/closed/shouldsucceed/1935.v index 641dcb7a..72396d49 100644 --- a/test-suite/bugs/closed/shouldsucceed/1935.v +++ b/test-suite/bugs/closed/shouldsucceed/1935.v @@ -1,14 +1,14 @@ Definition f (n:nat) := n = n. Lemma f_refl : forall n , f n. -intros. reflexivity. +intros. reflexivity. Qed. Definition f' (x:nat) (n:nat) := n = n. Lemma f_refl' : forall n , f' n n. Proof. - intros. reflexivity. + intros. reflexivity. Qed. Require Import ZArith. diff --git a/test-suite/bugs/closed/shouldsucceed/1939.v b/test-suite/bugs/closed/shouldsucceed/1939.v new file mode 100644 index 00000000..5e61529b --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/1939.v @@ -0,0 +1,19 @@ +Require Import Setoid Program.Basics. + + Parameter P : nat -> Prop. + Parameter R : nat -> nat -> Prop. + + Add Parametric Morphism : P + with signature R ++> impl as PM1. + Admitted. + + Add Parametric Morphism : P + with signature R --> impl as PM2. + Admitted. + + Goal forall x y, R x y -> P y -> P x. + Proof. + intros x y H1 H2. + rewrite H1. + auto. + Qed.
\ No newline at end of file diff --git a/test-suite/bugs/closed/shouldsucceed/1944.v b/test-suite/bugs/closed/shouldsucceed/1944.v new file mode 100644 index 00000000..ee2918c6 --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/1944.v @@ -0,0 +1,9 @@ +(* Test some uses of ? in introduction patterns *) + +Inductive J : nat -> Prop := + | K : forall p, J p -> (True /\ True) -> J (S p). + +Lemma bug : forall n, J n -> J (S n). +Proof. + intros ? H. + induction H as [? ? [? ?]]. diff --git a/test-suite/bugs/closed/shouldsucceed/1951.v b/test-suite/bugs/closed/shouldsucceed/1951.v new file mode 100644 index 00000000..12c0ef9b --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/1951.v @@ -0,0 +1,63 @@ + +(* First a simplification of the bug *) + +Set Printing Universes. + +Inductive enc (A:Type (*1*)) (* : Type.1 *) := C : A -> enc A. + +Definition id (X:Type(*5*)) (x:X) := x. + +Lemma test : let S := Type(*6 : 7*) in enc S -> S. +simpl; intros. +apply enc. +apply id. +apply Prop. +Defined. + +(* Then the original bug *) + +Require Import List. + +Inductive a : Set := (* some dummy inductive *) +b : (list a) -> a. (* i don't know if this *) + (* happens for smaller *) + (* ones *) + +Inductive sg : Type := Sg. (* single *) + +Definition ipl2 (P : a -> Type) := (* in Prop, that means P is true forall *) +fold_right (fun x => prod (P x)) sg. (* the elements of a given list *) + +Definition ind + : forall S : a -> Type, + (forall ls : list a, ipl2 S ls -> S (b ls)) -> forall s : a, S s := +fun (S : a -> Type) + (X : forall ls : list a, ipl2 S ls -> S (b ls)) => +fix ind2 (s : a) := +match s as a return (S a) with +| b l => + X l + (list_rect (fun l0 : list a => ipl2 S l0) Sg + (fun (a0 : a) (l0 : list a) (IHl : ipl2 S l0) => + pair (ind2 a0) IHl) l) +end. (* some induction principle *) + +Implicit Arguments ind [S]. + +Lemma k : a -> Type. (* some ininteresting lemma *) +intro;pattern H;apply ind;intros. + assert (K : Type). + induction ls. + exact sg. + exact sg. + exact (prod K sg). +Defined. + +Lemma k' : a -> Type. (* same lemma but with our bug *) +intro;pattern H;apply ind;intros. + apply prod. + induction ls. + exact sg. + exact sg. + exact sg. (* Proof complete *) +Defined. (* bug *) diff --git a/test-suite/bugs/closed/shouldsucceed/1981.v b/test-suite/bugs/closed/shouldsucceed/1981.v index 0c3b96da..99952682 100644 --- a/test-suite/bugs/closed/shouldsucceed/1981.v +++ b/test-suite/bugs/closed/shouldsucceed/1981.v @@ -1,5 +1,5 @@ Implicit Arguments ex_intro [A]. Goal exists n : nat, True. - eapply ex_intro. exact 0. exact I. + eapply ex_intro. exact 0. exact I. Qed. diff --git a/test-suite/bugs/closed/shouldsucceed/2001.v b/test-suite/bugs/closed/shouldsucceed/2001.v index 323021de..d0b3bf17 100644 --- a/test-suite/bugs/closed/shouldsucceed/2001.v +++ b/test-suite/bugs/closed/shouldsucceed/2001.v @@ -1,8 +1,10 @@ (* Automatic computing of guard in "Theorem with"; check that guard is not computed when the user explicitly indicated it *) +Unset Automatic Introduction. + Inductive T : Set := -| v : T. +| v : T. Definition f (s:nat) (t:T) : nat. fix 2. @@ -12,9 +14,9 @@ refine | v => s end. Defined. - + Lemma test : forall s, f s v = s. -Proof. +Proof. reflexivity. -Qed. +Qed. diff --git a/test-suite/bugs/closed/shouldsucceed/2017.v b/test-suite/bugs/closed/shouldsucceed/2017.v index 948cea3e..df666148 100644 --- a/test-suite/bugs/closed/shouldsucceed/2017.v +++ b/test-suite/bugs/closed/shouldsucceed/2017.v @@ -8,8 +8,8 @@ Set Implicit Arguments. Variable choose : forall(P : bool -> Prop)(H : exists x, P x), bool. Variable H : exists x : bool, True. - + Definition coef := match Some true with - Some _ => @choose _ H |_ => true -end . + Some _ => @choose _ H |_ => true +end . diff --git a/test-suite/bugs/closed/shouldsucceed/2083.v b/test-suite/bugs/closed/shouldsucceed/2083.v new file mode 100644 index 00000000..a6ce4de0 --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/2083.v @@ -0,0 +1,27 @@ +Require Import Program Arith. + +Program Fixpoint check_n (n : nat) (P : { i | i < n } -> bool) (p : nat) + (H : forall (i : { i | i < n }), i < p -> P i = true) + {measure (n - p)} : + Exc (forall (p : { i | i < n}), P p = true) := + match le_lt_dec n p with + | left _ => value _ + | right cmp => + if dec (P p) then + check_n n P (S p) _ + else + error + end. + +Require Import Omega. + +Solve Obligations using program_simpl ; auto with *; try omega. + +Next Obligation. + apply H. simpl. omega. +Defined. + +Next Obligation. + case (le_lt_dec p i) ; intros. assert(i = p) by omega. subst. + revert H0. clear_subset_proofs. auto. + apply H. simpl. assumption. Defined. diff --git a/test-suite/bugs/closed/shouldsucceed/2095.v b/test-suite/bugs/closed/shouldsucceed/2095.v new file mode 100644 index 00000000..28ea99df --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/2095.v @@ -0,0 +1,19 @@ +(* Classes and sections *) + +Section OPT. + Variable A: Type. + + Inductive MyOption: Type := + | MyNone: MyOption + | MySome: A -> MyOption. + + Class Opt: Type := { + f_opt: A -> MyOption + }. +End OPT. + +Definition f_nat (n: nat): MyOption nat := MySome _ n. + +Instance Nat_Opt: Opt nat := { + f_opt := f_nat +}. diff --git a/test-suite/bugs/closed/shouldsucceed/2108.v b/test-suite/bugs/closed/shouldsucceed/2108.v new file mode 100644 index 00000000..cad8baa9 --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/2108.v @@ -0,0 +1,22 @@ +(* Declare Module in Module Type *) +Module Type A. +Record t : Set := { something : unit }. +End A. + + +Module Type B. +Declare Module BA : A. +End B. + + +Module Type C. +Declare Module CA : A. +Declare Module CB : B with Module BA := CA. +End C. + + +Module Type D. +Declare Module DA : A. +(* Next line gives: "Anomaly: uncaught exception Not_found. Please report." *) +Declare Module DC : C with Module CA := DA. +End D. diff --git a/test-suite/bugs/closed/shouldsucceed/2117.v b/test-suite/bugs/closed/shouldsucceed/2117.v new file mode 100644 index 00000000..6377a8b7 --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/2117.v @@ -0,0 +1,56 @@ +(* Check pattern-unification on evars in apply unification *) + +Axiom app : forall tau tau':Type, (tau -> tau') -> tau -> tau'. + +Axiom copy : forall tau:Type, tau -> tau -> Prop. +Axiom copyr : forall tau:Type, tau -> tau -> Prop. +Axiom copyf : forall tau:Type, tau -> tau -> Prop. +Axiom eq : forall tau:Type, tau -> tau -> Prop. +Axiom subst : forall tau tau':Type, (tau -> tau') -> tau -> tau' -> Prop. + +Axiom copy_atom : forall tau:Type, forall t t':tau, eq tau t t' -> copy tau t t'. +Axiom copy_fun: forall tau tau':Type, forall t t':(tau->tau'), +(forall x:tau, copyr tau x x->copy tau' (t x) (t' x)) +->copy (tau->tau') t t'. + +Axiom copyr_atom : forall tau:Type, forall t t':tau, copyr tau t t' -> eq tau t t'. +Axiom copyr_fun: forall tau tau':Type, forall t t':(tau->tau'), +copyr (tau->tau') t t' +->(forall x y:tau, copy tau x y->copyr tau' (t x) (t' y)). + +Axiom copyf_atom : forall tau:Type, forall t t':tau, copyf tau t t' -> eq tau t t'. +Axiom copyf_fun: forall tau tau':Type, forall t t':(tau->tau'), +copyr (tau->tau') t t' +->(forall x y:tau, forall z1 z2:tau', +(copy tau x y)-> +(subst tau tau' t x z1)-> +(subst tau tau' t' y z2)-> +copyf tau' z1 z2). + +Axiom eqappg: forall tau tau':Type, forall t:tau->tau', forall q:tau, forall r:tau',forall t':tau', +( ((subst tau tau' t q t') /\ (eq tau' t' r)) +->eq tau' (app tau tau' t q) r). + +Axiom eqappd: forall tau tau':Type, forall t:tau->tau', forall q:tau, forall r:tau', +forall t':tau', ((subst tau tau' t q t') /\ (eq tau' r t')) +->eq tau' r (app tau tau' t q). + +Axiom substcopy: forall tau tau':Type, forall t:tau->tau', forall q:tau, forall r:tau', +(forall x:tau, (copyf tau x q) -> (copy tau' (t x) r)) +->subst tau tau' t q r. + +Ltac EtaLong := (apply copy_fun;intros;EtaLong)|| apply copy_atom.
+Ltac Subst := apply substcopy;intros;EtaLong. +Ltac Rigid_aux := fun A => apply A|| Rigid_aux (copyr_fun _ _ _ _ A). +Ltac Rigid := fun A => apply copyr_atom; Rigid_aux A. + +Theorem church0: forall i:Type, exists X:(i->i)->i->i, +copy ((i->i)->i->i) (fun f:i->i => fun x:i=>f (X f x)) (fun f:i->i=>fun x:i=>app i i (X f) (f x)). +intros. +esplit. +EtaLong. +eapply eqappd;split. +Subst. +apply copyf_atom. +Show Existentials. +apply H1. diff --git a/test-suite/bugs/closed/shouldsucceed/2123.v b/test-suite/bugs/closed/shouldsucceed/2123.v new file mode 100644 index 00000000..422a2c12 --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/2123.v @@ -0,0 +1,11 @@ +(* About the detection of non-dependent metas by the refine tactic *) + +(* The following is a simplification of bug #2123 *) + +Parameter fset : nat -> Set. +Parameter widen : forall (n : nat) (s : fset n), { x : fset (S n) | s=s }. +Goal forall i, fset (S i). +intro. +refine (proj1_sig (widen i _)). + + diff --git a/test-suite/bugs/closed/shouldsucceed/2127.v b/test-suite/bugs/closed/shouldsucceed/2127.v new file mode 100644 index 00000000..20ea4603 --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/2127.v @@ -0,0 +1,11 @@ +(* Check that "apply refl_equal" is not exported as an interactive + tactic but as a statically globalized one *) + +(* (this is a simplification of the original bug report) *) + +Module A. +Hint Rewrite sym_equal using apply refl_equal : foo. +End A. + + + diff --git a/test-suite/bugs/closed/shouldsucceed/2135.v b/test-suite/bugs/closed/shouldsucceed/2135.v new file mode 100644 index 00000000..61882176 --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/2135.v @@ -0,0 +1,9 @@ +(* Check that metas are whd-normalized before trying 2nd-order unification *) +Lemma test : + forall (D:Type) (T : forall C, option C) (Q:forall D, option D -> Prop), + (forall (A : Type) (P : forall B:Type, option B -> Prop), P A (T A)) + -> Q D (T D). +Proof. + intros D T Q H. + pattern (T D). apply H. +Qed. diff --git a/test-suite/bugs/closed/shouldsucceed/2136.v b/test-suite/bugs/closed/shouldsucceed/2136.v new file mode 100644 index 00000000..d2b926f3 --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/2136.v @@ -0,0 +1,61 @@ +(* Bug #2136 + +The fsetdec tactic seems to get confused by hypotheses like + HeqH1 : H1 = MkEquality s0 s1 b +If I clear them then it is able to solve my goal; otherwise it is not. +I would expect it to be able to solve the goal even without this hypothesis +being cleared. A small, self-contained example is below. + +I have coq r12238. + + +Thanks +Ian +*) + + +Require Import FSets. +Require Import Arith. +Require Import FSetWeakList. + +Module DecidableNat. +Definition t := nat. +Definition eq := @eq nat. +Definition eq_refl := @refl_equal nat. +Definition eq_sym := @sym_eq nat. +Definition eq_trans := @trans_eq nat. +Definition eq_dec := eq_nat_dec. +End DecidableNat. + +Module NatSet := Make(DecidableNat). + +Module Export Dec := WDecide (NatSet). +Import FSetDecideAuxiliary. + +Parameter MkEquality : forall ( s0 s1 : NatSet.t ) + ( x : nat ), + NatSet.Equal s1 (NatSet.add x s0). + +Lemma ThisLemmaWorks : forall ( s0 s1 : NatSet.t ) + ( a b : nat ), + NatSet.In a s0 + -> NatSet.In a s1. +Proof. +intros. +remember (MkEquality s0 s1 b) as H1. +clear HeqH1. +fsetdec. +Qed. + +Lemma ThisLemmaWasFailing : forall ( s0 s1 : NatSet.t ) + ( a b : nat ), + NatSet.In a s0 + -> NatSet.In a s1. +Proof. +intros. +remember (MkEquality s0 s1 b) as H1. +fsetdec. +(* +Error: Tactic failure: because the goal is beyond the scope of this tactic. +*) +Qed.
\ No newline at end of file diff --git a/test-suite/bugs/closed/shouldsucceed/2137.v b/test-suite/bugs/closed/shouldsucceed/2137.v new file mode 100644 index 00000000..6c2023ab --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/2137.v @@ -0,0 +1,52 @@ +(* Bug #2137 + +The fsetdec tactic is sensitive to which way round the arguments to <> are. +In the small, self-contained example below, it is able to solve the goal +if it knows that "b <> a", but not if it knows that "a <> b". I would expect +it to be able to solve hte goal in either case. + +I have coq r12238. + + +Thanks +Ian + +*) + +Require Import Arith FSets FSetWeakList. + +Module DecidableNat. +Definition t := nat. +Definition eq := @eq nat. +Definition eq_refl := @refl_equal nat. +Definition eq_sym := @sym_eq nat. +Definition eq_trans := @trans_eq nat. +Definition eq_dec := eq_nat_dec. +End DecidableNat. + +Module NatSet := Make(DecidableNat). + +Module Export NameSetDec := WDecide (NatSet). + +Lemma ThisLemmaWorks : forall ( s0 : NatSet.t ) + ( a b : nat ), + b <> a + -> ~(NatSet.In a s0) + -> ~(NatSet.In a (NatSet.add b s0)). +Proof. +intros. +fsetdec. +Qed. + +Lemma ThisLemmaWasFailing : forall ( s0 : NatSet.t ) + ( a b : nat ), + a <> b + -> ~(NatSet.In a s0) + -> ~(NatSet.In a (NatSet.add b s0)). +Proof. +intros. +fsetdec. +(* +Error: Tactic failure: because the goal is beyond the scope of this tactic. +*) +Qed.
\ No newline at end of file diff --git a/test-suite/bugs/closed/shouldsucceed/2139.v b/test-suite/bugs/closed/shouldsucceed/2139.v new file mode 100644 index 00000000..a7f35508 --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/2139.v @@ -0,0 +1,24 @@ +(* Call of apply on <-> failed because of evars in elimination predicate *) +Generalizable Variables patch. + +Class Patch (patch : Type) := { + commute : patch -> patch -> Prop +}. + +Parameter flip : forall `{patchInstance : Patch patch} + {a b : patch}, + commute a b <-> commute b a. + +Lemma Foo : forall `{patchInstance : Patch patch} + {a b : patch}, + (commute a b) + -> True. +Proof. +intros. +apply flip in H. + +(* failed in well-formed arity check because elimination predicate of + iff in (@flip _ _ _ _) had normalized evars while the ones in the + type of (@flip _ _ _ _) itself had non-normalized evars *) + +(* By the way, is the check necessary ? *) diff --git a/test-suite/bugs/closed/shouldsucceed/2145.v b/test-suite/bugs/closed/shouldsucceed/2145.v new file mode 100644 index 00000000..b6c5da65 --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/2145.v @@ -0,0 +1,20 @@ +(* Test robustness of Groebner tactic in presence of disequalities *) + +Require Export Reals. +Require Export NsatzR. + +Open Scope R_scope. + +Lemma essai : + forall yb xb m1 m2 xa ya, + xa <> xb -> + yb - 2 * m2 * xb = ya - m2 * xa -> + yb - m1 * xb = ya - m1 * xa -> + yb - ya = (2 * xb - xa) * m2 -> + yb - ya = (xb - xa) * m1. +Proof. +intros. +(* clear H. groebner used not to work when H was not cleared *) +nsatzR. +Qed. + diff --git a/test-suite/bugs/closed/shouldsucceed/2193.v b/test-suite/bugs/closed/shouldsucceed/2193.v new file mode 100644 index 00000000..fe258867 --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/2193.v @@ -0,0 +1,31 @@ +(* Computation of dependencies in the "match" return predicate was incomplete *) +(* Submitted by R. O'Connor, Nov 2009 *) + +Inductive Symbol : Set := + | VAR : Symbol. + +Inductive SExpression := + | atomic : Symbol -> SExpression. + +Inductive ProperExpr : SExpression -> SExpression -> Type := + | pe_3 : forall (x : Symbol) (alpha : SExpression), + ProperExpr alpha (atomic VAR) -> + ProperExpr (atomic x) alpha. + +Definition A (P : forall s : SExpression, Type) + (x alpha alpha1 : SExpression) + (t : ProperExpr (x) alpha1) : option (x = atomic VAR) := + match t as pe in ProperExpr a b return option (a = atomic VAR) with + | pe_3 x0 alpha3 tye' => + (fun (x:Symbol) (alpha : SExpression) => @None (atomic x = atomic VAR)) + x0 alpha3 + end. + +Definition B (P : forall s : SExpression, Type) + (x alpha alpha1 : SExpression) + (t : ProperExpr (x) alpha1) : option (x = atomic VAR) := + match t as pe in ProperExpr a b return option (a = atomic VAR) with + | pe_3 x0 alpha3 tye' => + (fun (x:Symbol) (alpha : SExpression) (t:ProperExpr alpha (atomic VAR)) => @None (atomic x = atomic VAR)) + x0 alpha3 tye' + end. diff --git a/test-suite/bugs/closed/shouldsucceed/2231.v b/test-suite/bugs/closed/shouldsucceed/2231.v new file mode 100644 index 00000000..03e2c9bb --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/2231.v @@ -0,0 +1,3 @@ +Inductive unit2 : Type := U : unit -> unit2. +Inductive dummy (u: unit2) : unit -> Type := + V: dummy u (let (tt) := u in tt). diff --git a/test-suite/bugs/closed/shouldsucceed/2244.v b/test-suite/bugs/closed/shouldsucceed/2244.v new file mode 100644 index 00000000..d499e515 --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/2244.v @@ -0,0 +1,19 @@ +(* 1st-order unification did not work when in competition with pattern unif. *) + +Set Implicit Arguments. +Lemma test : forall + (A : Type) + (B : Type) + (f : A -> B) + (S : B -> Prop) + (EV : forall y (f':A->B), (forall x', S (f' x')) -> S (f y)) + (HS : forall x', S (f x')) + (x : A), + S (f x). +Proof. + intros. eapply EV. intros. + (* worked in v8.2 but not in v8.3beta, fixed in r12898 *) + apply HS. + + (* still not compatible with 8.2 because an evar can be solved in + two different ways and is left open *) diff --git a/test-suite/bugs/closed/shouldsucceed/2255.v b/test-suite/bugs/closed/shouldsucceed/2255.v new file mode 100644 index 00000000..bf80ff66 --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/2255.v @@ -0,0 +1,21 @@ +(* Check injection in presence of dependencies hidden in applicative terms *) + +Inductive TupleT : nat -> Type := + nilT : TupleT 0 +| consT {n} A : (A -> TupleT n) -> TupleT (S n). + +Inductive Tuple : forall n, TupleT n -> Type := + nil : Tuple _ nilT +| cons {n} A (x : A) (F : A -> TupleT n) : Tuple _ (F x) -> Tuple _ (consT A F). + +Goal forall n A F x X n0 A0 x0 F0 H0 (H : existT (fun n0 : nat => {H0 : TupleT +n0 & Tuple n0 H0}) + (S n0) + (existT (fun H0 : TupleT (S n0) => Tuple (S n0) H0) + (consT A0 F0) (cons A0 x0 F0 H0)) = + existT (fun n0 : nat => {H0 : TupleT n0 & Tuple n0 H0}) + (S n) + (existT (fun H0 : TupleT (S n) => Tuple (S n) H0) + (consT A F) (cons A x F X))), False. +intros. +injection H. diff --git a/test-suite/bugs/closed/shouldsucceed/2281.v b/test-suite/bugs/closed/shouldsucceed/2281.v new file mode 100644 index 00000000..40948d90 --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/2281.v @@ -0,0 +1,50 @@ +(** Bug #2281 + +In the code below, coq is confused by an equality unless it is first 'subst'ed +away, yet http://coq.inria.fr/stdlib/Coq.FSets.FSetDecide.html says + + fsetdec will first perform any necessary zeta and beta reductions and will +invoke subst to eliminate any Coq equalities between finite sets or their +elements. + +I have coq r12851. + +*) + +Require Import Arith. +Require Import FSets. +Require Import FSetWeakList. + +Module DecidableNat. +Definition t := nat. +Definition eq := @eq nat. +Definition eq_refl := @refl_equal nat. +Definition eq_sym := @sym_eq nat. +Definition eq_trans := @trans_eq nat. +Definition eq_dec := eq_nat_dec. +End DecidableNat. + +Module NatSet := Make(DecidableNat). + +Module Export NameSetDec := WDecide (NatSet). + +Lemma ThisLemmaWorks : forall ( s1 s2 : NatSet.t ) + ( H : s1 = s2 ), + NatSet.Equal s1 s2. +Proof. +intros. +subst. +fsetdec. +Qed. + +Import FSetDecideAuxiliary. + +Lemma ThisLemmaWasFailing : forall ( s1 s2 : NatSet.t ) + ( H : s1 = s2 ), + NatSet.Equal s1 s2. +Proof. +intros. +fsetdec. +(* Error: Tactic failure: because the goal is beyond the scope of this tactic. +*) +Qed.
\ No newline at end of file diff --git a/test-suite/bugs/closed/shouldsucceed/2295.v b/test-suite/bugs/closed/shouldsucceed/2295.v new file mode 100644 index 00000000..f5ca28dc --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/2295.v @@ -0,0 +1,11 @@ +(* Check if omission of "as" in return clause works w/ section variables too *) + +Section sec. + +Variable b: bool. + +Definition d' := + (match b return b = true \/ b = false with + | true => or_introl _ (refl_equal true) + | false => or_intror _ (refl_equal false) + end). diff --git a/test-suite/bugs/closed/shouldsucceed/2299.v b/test-suite/bugs/closed/shouldsucceed/2299.v new file mode 100644 index 00000000..c0552ca7 --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/2299.v @@ -0,0 +1,13 @@ +(* Check that destruct refreshes universes in what it generalizes *) + +Section test. + +Variable A: Type. + +Inductive T: unit -> Type := C: A -> unit -> T tt. + +Let unused := T tt. + +Goal T tt -> False. + intro X. + destruct X. diff --git a/test-suite/bugs/closed/shouldsucceed/2300.v b/test-suite/bugs/closed/shouldsucceed/2300.v new file mode 100644 index 00000000..4e587cbb --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/2300.v @@ -0,0 +1,15 @@ +(* Check some behavior of Ltac pattern-matching wrt universe levels *) + +Section contents. + +Variables (A: Type) (B: (unit -> Type) -> Type). + +Inductive C := c: A -> unit -> C. + +Let unused2 (x: unit) := C. + +Goal True. +intuition. +Qed. + +End contents. diff --git a/test-suite/bugs/closed/shouldsucceed/335.v b/test-suite/bugs/closed/shouldsucceed/335.v new file mode 100644 index 00000000..166fa7a9 --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/335.v @@ -0,0 +1,5 @@ +(* Compatibility of Require with backtracking at interactive module end *) + +Module A. +Require List. +End A. diff --git a/test-suite/bugs/closed/shouldsucceed/38.v b/test-suite/bugs/closed/shouldsucceed/38.v index 7bc04b1f..4fc8d7c9 100644 --- a/test-suite/bugs/closed/shouldsucceed/38.v +++ b/test-suite/bugs/closed/shouldsucceed/38.v @@ -6,7 +6,7 @@ Inductive liste : Set := | vide : liste | c : A -> liste -> liste. -Inductive e : A -> liste -> Prop := +Inductive e : A -> liste -> Prop := | ec : forall (x : A) (l : liste), e x (c x l) | ee : forall (x y : A) (l : liste), e x l -> e x (c y l). diff --git a/test-suite/bugs/closed/shouldsucceed/846.v b/test-suite/bugs/closed/shouldsucceed/846.v index a963b225..ee5ec1fa 100644 --- a/test-suite/bugs/closed/shouldsucceed/846.v +++ b/test-suite/bugs/closed/shouldsucceed/846.v @@ -27,7 +27,7 @@ Definition index := list bool. Inductive L (A:Set) : index -> Set := initL: A -> L A nil - | pluslL: forall l:index, One -> L A (false::l) + | pluslL: forall l:index, One -> L A (false::l) | plusrL: forall l:index, L A l -> L A (false::l) | varL: forall l:index, L A l -> L A (true::l) | appL: forall l:index, L A (true::l) -> L A (true::l) -> L A (true::l) @@ -109,7 +109,7 @@ Proof. exact (monL (fun x:One + A => (match (maybe (fun a:A => initL a) x) with | inl u => pluslL _ _ u - | inr t' => plusrL t' end)) r). + | inr t' => plusrL t' end)) r). Defined. Section minimal. @@ -119,11 +119,11 @@ Hypothesis G: Set -> Set. Hypothesis step: sub1 (LamF' G) G. Fixpoint L'(A:Set)(i:index){struct i} : Set := - match i with + match i with nil => A | false::l => One + L' A l | true::l => G (L' A l) - end. + end. Definition LinL': forall (A:Set)(i:index), L A i -> L' A i. Proof. @@ -177,7 +177,7 @@ Proof. assumption. induction a. simpl L' in t. - apply (aczelapp (l1:=true::nil) (l2:=i)). + apply (aczelapp (l1:=true::nil) (l2:=i)). exact (lam' IHi t). simpl L' in t. induction t. diff --git a/test-suite/bugs/opened/shouldnotfail/1501.v b/test-suite/bugs/opened/shouldnotfail/1501.v index 85c09dbd..1845dd1f 100644 --- a/test-suite/bugs/opened/shouldnotfail/1501.v +++ b/test-suite/bugs/opened/shouldnotfail/1501.v @@ -8,7 +8,7 @@ Require Export Setoid. Section Essais. (* Parametrized Setoid *) -Parameter K : Type -> Type. +Parameter K : Type -> Type. Parameter equiv : forall A : Type, K A -> K A -> Prop. Parameter equiv_refl : forall (A : Type) (x : K A), equiv x x. Parameter equiv_sym : forall (A : Type) (x y : K A), equiv x y -> equiv y x. @@ -40,7 +40,7 @@ Parameter Hint Resolve equiv_refl equiv_sym equiv_trans: monad. -Add Relation K equiv +Add Relation K equiv reflexivity proved by (@equiv_refl) symmetry proved by (@equiv_sym) transitivity proved by (@equiv_trans) @@ -67,7 +67,7 @@ Proof. unfold fequiv; intros; eapply equiv_trans; auto with monad. Qed. -Add Relation (fun (A B:Type) => A -> K B) fequiv +Add Relation (fun (A B:Type) => A -> K B) fequiv reflexivity proved by (@fequiv_refl) symmetry proved by (@fequiv_sym) transitivity proved by (@fequiv_trans) @@ -82,12 +82,12 @@ Qed. Lemma test: forall (A B: Type) (m1 m2 m3: K A) (f: A -> A -> K B), - (equiv m1 m2) -> (equiv m2 m3) -> + (equiv m1 m2) -> (equiv m2 m3) -> equiv (bind m1 (fun a => bind m2 (fun a' => f a a'))) (bind m2 (fun a => bind m3 (fun a' => f a a'))). Proof. - intros A B m1 m2 m3 f H1 H2. + intros A B m1 m2 m3 f H1 H2. setoid_rewrite H1. (* this works *) setoid_rewrite H2. trivial by equiv_refl. -Qed. +Qed. diff --git a/test-suite/bugs/opened/shouldnotfail/1596.v b/test-suite/bugs/opened/shouldnotfail/1596.v index 766bf524..de77e35d 100644 --- a/test-suite/bugs/opened/shouldnotfail/1596.v +++ b/test-suite/bugs/opened/shouldnotfail/1596.v @@ -11,12 +11,12 @@ Module OrderedPair (X:OrderedType) (Y:OrderedType) <: OrderedType with Definition t := (X.t * Y.t)%type. Definition t := (X.t * Y.t)%type. - Definition eq (xy1:t) (xy2:t) := + Definition eq (xy1:t) (xy2:t) := let (x1,y1) := xy1 in let (x2,y2) := xy2 in (X.eq x1 x2) /\ (Y.eq y1 y2). - Definition lt (xy1:t) (xy2:t) := + Definition lt (xy1:t) (xy2:t) := let (x1,y1) := xy1 in let (x2,y2) := xy2 in (X.lt x1 x2) \/ ((X.eq x1 x2) /\ (Y.lt y1 y2)). @@ -101,7 +101,7 @@ Definition t := (X.t * Y.t)%type. Defined. Hint Immediate eq_sym. - Hint Resolve eq_refl eq_trans lt_not_eq lt_trans. + Hint Resolve eq_refl eq_trans lt_not_eq lt_trans. End OrderedPair. Module MessageSpi. @@ -189,8 +189,8 @@ n)->(hedge_synthesis_relation h m n). Fixpoint hedge_in_synthesis (h:hedge) (m:MessageSpi.message) (n:MessageSpi.message) {struct m} : bool := - if H.mem (m,n) h - then true + if H.mem (m,n) h + then true else false. Definition hedge_synthesis_spec (h:hedge) := hedge_synthesis_relation @@ -221,8 +221,8 @@ n). Fixpoint hedge_in_synthesis (h:hedge) (m:MessageSpi.t) (n:MessageSpi.t) {struct m} : bool := - if H.mem (m,n) h - then true + if H.mem (m,n) h + then true else false. Definition hedge_synthesis_spec (h:hedge) := hedge_synthesis_relation @@ -235,7 +235,7 @@ n). induction m;simpl;intro. elim (Bool_elim_bool (H.mem (MessageSpi.MNam n,n0) h));intros. apply SynInc;apply H.mem_2;trivial. - + rewrite H in H0. (* !! impossible here !! *) discriminate H0. Qed. diff --git a/test-suite/bugs/opened/shouldnotfail/1671.v b/test-suite/bugs/opened/shouldnotfail/1671.v index 800c431e..d95c2108 100644 --- a/test-suite/bugs/opened/shouldnotfail/1671.v +++ b/test-suite/bugs/opened/shouldnotfail/1671.v @@ -6,7 +6,7 @@ CoInductive hdlist : unit -> Type := Variable P : forall bo, hdlist bo -> Prop. Variable all : forall bo l, P bo l. -Definition F (l:hdlist tt) : P tt l := +Definition F (l:hdlist tt) : P tt l := match l in hdlist u return P u l with | cons (cons l') => all tt _ end. |