diff options
Diffstat (limited to 'test-suite/success')
40 files changed, 1887 insertions, 49 deletions
diff --git a/test-suite/success/AdvancedCanonicalStructure.v b/test-suite/success/AdvancedCanonicalStructure.v new file mode 100644 index 00000000..8e613dca --- /dev/null +++ b/test-suite/success/AdvancedCanonicalStructure.v @@ -0,0 +1,144 @@ +Section group_morphism. + +(* An example with default canonical structures *) + +Variable A B : Type. +Variable plusA : A -> A -> A. +Variable plusB : B -> B -> B. +Variable zeroA : A. +Variable zeroB : B. +Variable eqA : A -> A -> Prop. +Variable eqB : B -> B -> Prop. +Variable phi : A -> B. + +Record img := { + ia : A; + ib :> B; + prf : phi ia = ib +}. + +Parameter eq_img : forall (i1:img) (i2:img), + eqB (ib i1) (ib i2) -> eqA (ia i1) (ia i2). + +Lemma phi_img (a:A) : img. + intro a. + exists a (phi a). + refine ( refl_equal _). +Defined. +Canonical Structure phi_img. + +Lemma zero_img : img. + exists zeroA zeroB. + admit. +Defined. +Canonical Structure zero_img. + +Lemma plus_img : img -> img -> img. +intros i1 i2. +exists (plusA (ia i1) (ia i2)) (plusB (ib i1) (ib i2)). +admit. +Defined. +Canonical Structure plus_img. + +(* Print Canonical Projections. *) + +Goal forall a1 a2, eqA (plusA a1 zeroA) a2. + intros a1 a2. + refine (eq_img _ _ _). +change (eqB (plusB (phi a1) zeroB) (phi a2)). +Admitted. + +End group_morphism. + +Open Scope type_scope. + +Section type_reification. + +Inductive term :Type := + Fun : term -> term -> term + | Prod : term -> term -> term + | Bool : term + | SET :term + | PROP :term + | TYPE :term + | Var : Type -> term. + +Fixpoint interp (t:term) := + match t with + Bool => bool + | SET => Set + | PROP => Prop + | TYPE => Type + | Fun a b => interp a -> interp b + | Prod a b => interp a * interp b + | Var x => x +end. + +Record interp_pair :Type := + { repr:>term; + abs:>Type; + link: abs = interp repr }. + +Lemma prod_interp :forall (a b:interp_pair),a * b = interp (Prod a b) . +proof. +let a:interp_pair,b:interp_pair. +reconsider thesis as (a * b = interp a * interp b). +thus thesis by (link a),(link b). +end proof. +Qed. + +Lemma fun_interp :forall (a b:interp_pair), (a -> b) = interp (Fun a b). +proof. +let a:interp_pair,b:interp_pair. +reconsider thesis as ((a -> b) = (interp a -> interp b)). +thus thesis using rewrite (link a);rewrite (link b);reflexivity. +end proof. +Qed. + +Canonical Structure ProdCan (a b:interp_pair) := + Build_interp_pair (Prod a b) (a * b) (prod_interp a b). + +Canonical Structure FunCan (a b:interp_pair) := + Build_interp_pair (Fun a b) (a -> b) (fun_interp a b). + +Canonical Structure BoolCan := + Build_interp_pair Bool bool (refl_equal _). + +Canonical Structure VarCan (x:Type) := + Build_interp_pair (Var x) x (refl_equal _). + +Canonical Structure SetCan := + Build_interp_pair SET Set (refl_equal _). + +Canonical Structure PropCan := + Build_interp_pair PROP Prop (refl_equal _). + +Canonical Structure TypeCan := + Build_interp_pair TYPE Type (refl_equal _). + +(* Print Canonical Projections. *) + +Variable A:Type. + +Variable Inhabited: term -> Prop. + +Variable Inhabited_correct: forall p, Inhabited (repr p) -> abs p. + +Lemma L : Prop * A -> bool * (Type -> Set) . +refine (Inhabited_correct _ _). +change (Inhabited (Fun (Prod PROP (Var A)) (Prod Bool (Fun TYPE SET)))). +Admitted. + +Check L : abs _ . + +End type_reification. + + + + + + + + + + diff --git a/test-suite/success/Case18.v b/test-suite/success/Case18.v index 91c80e88..be9ca8d4 100644 --- a/test-suite/success/Case18.v +++ b/test-suite/success/Case18.v @@ -12,3 +12,15 @@ Fixpoint max (n m:nat) {struct m} : nat := | S n', S m' => S (max n' m') | 0, p | p, 0 => p end. + +(* Check bug #1477 *) + +Inductive I : Set := + | A : nat -> nat -> I + | B : nat -> nat -> I. + +Definition foo (x:I) : nat := + match x with + | A a b | B b a => S b + end. + diff --git a/test-suite/success/Cases-bug1834.v b/test-suite/success/Cases-bug1834.v new file mode 100644 index 00000000..543ca0c9 --- /dev/null +++ b/test-suite/success/Cases-bug1834.v @@ -0,0 +1,13 @@ +(* Bug in the computation of generalization *) + +(* The following bug, elaborated by Bruno Barras, is solved from r11083 *) + +Parameter P : unit -> Prop. +Definition T := sig P. +Parameter Q : T -> Prop. +Definition U := sig Q. +Parameter a : U. +Check (match a with exist (exist tt e2) e3 => e3=e3 end). + +(* There is still a form submitted by Pierre Corbineau (#1834) which fails *) + diff --git a/test-suite/success/Cases.v b/test-suite/success/Cases.v index 7c2b7c0b..499c0660 100644 --- a/test-suite/success/Cases.v +++ b/test-suite/success/Cases.v @@ -10,6 +10,10 @@ Type match 0, eq, 0 return nat with | O, x, y => 0 | S x, y, z => x end. +Type match 0, eq, 0 return _ with + | O, x, y => 0 + | S x, y, z => x + end. (* Non dependent form of annotation *) Type match 0, eq return nat with @@ -406,7 +410,6 @@ Type match niln with | x => 0 end. - Type match niln return nat with | niln => 0 | consn n a l => a diff --git a/test-suite/success/CasesDep.v b/test-suite/success/CasesDep.v index 0477377e..49bd77fc 100644 --- a/test-suite/success/CasesDep.v +++ b/test-suite/success/CasesDep.v @@ -71,13 +71,9 @@ Inductive Setoid : Type := Definition elem (A : Setoid) := let (S, R, e) := A in S. -(* <Warning> : Grammar is replaced by Notation *) - Definition equal (A : Setoid) := let (S, R, e) as s return (Relation (elem s)) := A in R. -(* <Warning> : Grammar is replaced by Notation *) - Axiom prf_equiv : forall A : Setoid, Equivalence (elem A) (equal A). Axiom prf_refl : forall A : Setoid, Reflexive (elem A) (equal A). @@ -430,3 +426,57 @@ Definition f0 (F : False) (ty : bool) : bProp ty := | _, false => F | _, true => I end. + +(* Simplification of bug/wish #1671 *) + +Inductive I : unit -> Type := +| C : forall a, I a -> I tt. + +(* +Definition F (l:I tt) : l = l := +match l return l = l with +| C tt (C _ l') => refl_equal (C tt (C _ l')) +end. + +one would expect that the compilation of F (this involves +some kind of pattern-unification) would produce: +*) + +Definition F (l:I tt) : l = l := +match l return l = l with +| C tt l' => match l' return C _ l' = C _ l' with C _ l'' => refl_equal (C tt (C _ l'')) end +end. + +Inductive J : nat -> Type := +| D : forall a, J (S a) -> J a. + +(* +Definition G (l:J O) : l = l := +match l return l = l with +| D O (D 1 l') => refl_equal (D O (D 1 l')) +| D _ _ => refl_equal _ +end. + +one would expect that the compilation of G (this involves inversion) +would produce: +*) + +Definition G (l:J O) : l = l := +match l return l = l with +| D 0 l'' => + match l'' as _l'' in J n return + match n return forall l:J n, Prop with + | O => fun _ => l = l + | S p => fun l'' => D p l'' = D p l'' + end _l'' with + | D 1 l' => refl_equal (D O (D 1 l')) + | _ => refl_equal _ + end +| _ => refl_equal _ +end. + +Fixpoint app {A} {n m} (v : listn A n) (w : listn A m) : listn A (n + m) := + match v with + | niln => w + | consn a n' v' => consn _ a _ (app v' w) + end. diff --git a/test-suite/success/Discriminate.v b/test-suite/success/Discriminate.v index f28c83de..b57c5478 100644 --- a/test-suite/success/Discriminate.v +++ b/test-suite/success/Discriminate.v @@ -9,3 +9,26 @@ Qed. Lemma l2 : forall H : 0 = 1, H = H. discriminate H. Qed. + +(* Check the variants of discriminate *) + +Goal O = S O -> True. +discriminate 1. +Undo. +intros. +discriminate H. +Undo. +Ltac g x := discriminate x. +g H. +Abort. + +Goal (forall x y : nat, x = y -> x = S y) -> True. +intros. +try discriminate (H O) || exact I. +Qed. + +Goal (forall x y : nat, x = y -> x = S y) -> True. +intros. +ediscriminate (H O). +instantiate (1:=O). +Abort. diff --git a/test-suite/success/Fixpoint.v b/test-suite/success/Fixpoint.v index 680046da..cf821073 100644 --- a/test-suite/success/Fixpoint.v +++ b/test-suite/success/Fixpoint.v @@ -29,3 +29,22 @@ CoFixpoint g (n:nat) (m:=pred n) (l:Stream m) (p:=S n) : Stream p := Eval compute in (fun l => match g 2 (Consn 0 6 l) with Consn _ a _ => a end). +(* Check inference of simple types in presence of non ambiguous + dependencies (needs revision 10125) *) + +Section folding. + +Inductive vector (A:Type) : nat -> Type := + | Vnil : vector A 0 + | Vcons : forall (a:A) (n:nat), vector A n -> vector A (S n). + +Variables (B C : Set) (g : B -> C -> C) (c : C). + +Fixpoint foldrn n bs := + match bs with + | Vnil => c + | Vcons b _ tl => g b (foldrn _ tl) + end. + +End folding. + diff --git a/test-suite/success/ImplicitArguments.v b/test-suite/success/ImplicitArguments.v new file mode 100644 index 00000000..e7795733 --- /dev/null +++ b/test-suite/success/ImplicitArguments.v @@ -0,0 +1,17 @@ +Inductive vector {A : Type} : nat -> Type := +| vnil : vector 0 +| vcons : A -> forall {n'}, vector n' -> vector (S n'). + +Require Import Coq.Program.Program. + +Program Definition head {A : Type} {n : nat} (v : vector A (S n)) : vector A n := + match v with + | vnil => ! + | vcons a n' v' => v' + end. + +Fixpoint app {A : Type} {n m : nat} (v : vector A n) (w : vector A m) : vector A (n + m) := + match v in vector _ n return vector A (n + m) with + | vnil => w + | vcons a n' v' => vcons a (app v' w) + end. diff --git a/test-suite/success/Injection.v b/test-suite/success/Injection.v index 606e884a..867d7374 100644 --- a/test-suite/success/Injection.v +++ b/test-suite/success/Injection.v @@ -43,6 +43,29 @@ intros; injection H as Hyt Hxz. exact Hxz. Qed. +(* Check the variants of injection *) + +Goal forall x y, S x = S y -> True. +injection 1 as H'. +Undo. +intros. +injection H as H'. +Undo. +Ltac f x := injection x. +f H. +Abort. + +Goal (forall x y : nat, x = y -> S x = S y) -> True. +intros. +try injection (H O) || exact I. +Qed. + +Goal (forall x y : nat, x = y -> S x = S y) -> True. +intros. +einjection (H O). +instantiate (1:=O). +Abort. + (* Injection does not projects at positions in Prop... allow it? Inductive t (A:Prop) : Set := c : A -> t A. @@ -53,7 +76,7 @@ Abort. *) -(* Accept does not project on discriminable positions... allow it? +(* Injection does not project on discriminable positions... allow it? Goal 1=2 -> 1=0. intro H. @@ -61,4 +84,4 @@ injection H. intro; assumption. Qed. - *) +*) diff --git a/test-suite/success/LetPat.v b/test-suite/success/LetPat.v new file mode 100644 index 00000000..545b8aeb --- /dev/null +++ b/test-suite/success/LetPat.v @@ -0,0 +1,55 @@ +(* Simple let-patterns *) +Variable A B : Type. + +Definition l1 (t : A * B * B) : A := let '(x, y, z) := t in x. +Print l1. +Definition l2 (t : (A * B) * B) : A := let '((x, y), z) := t in x. +Definition l3 (t : A * (B * B)) : A := let '(x, (y, z)) := t in x. +Print l3. + +Record someT (A : Type) := mkT { a : nat; b: A }. + +Definition l4 A (t : someT A) : nat := let 'mkT x y := t in x. +Print l4. +Print sigT. + +Definition l5 A (B : A -> Type) (t : sigT B) : B (projT1 t) := + let 'existT x y := t return B (projT1 t) in y. + +Definition l6 A (B : A -> Type) (t : sigT B) : B (projT1 t) := + let 'existT x y as t' := t return B (projT1 t') in y. + +Definition l7 A (B : A -> Type) (t : sigT B) : B (projT1 t) := + let 'existT x y as t' in sigT _ := t return B (projT1 t') in y. + +Definition l8 A (B : A -> Type) (t : sigT B) : B (projT1 t) := + match t with + existT x y => y + end. + +(** An example from algebra, using let' and inference of return clauses + to deconstruct contexts. *) + +Record a_category (A : Type) (hom : A -> A -> Type) := { }. + +Definition category := { A : Type & { hom : A -> A -> Type & a_category A hom } }. + +Record a_functor (A : Type) (hom : A -> A -> Type) (C : a_category A hom) := { }. + +Notation " x :& y " := (@existT _ _ x y) (right associativity, at level 55) : core_scope. + +Definition functor (c d : category) := + let ' A :& homA :& CA := c in + let ' B :& homB :& CB := d in + A -> B. + +Definition identity_functor (c : category) : functor c c := + let 'A :& homA :& CA := c in + fun x => x. + +Definition functor_composition (a b c : category) : functor a b -> functor b c -> functor a c := + let 'A :& homA :& CA := a in + let 'B :& homB :& CB := b in + let 'C :& homB :& CB := c in + fun f g => + fun x => g (f x). diff --git a/test-suite/success/Notations.v b/test-suite/success/Notations.v index a9e2c59a..facd5509 100644 --- a/test-suite/success/Notations.v +++ b/test-suite/success/Notations.v @@ -1,5 +1,5 @@ (* Check that "where" clause behaves as if given independently of the *) -(* definition (variant of bug #113? submitted by Assia Mahboubi) *) +(* definition (variant of bug #1132 submitted by Assia Mahboubi) *) Fixpoint plus1 (n m:nat) {struct n} : nat := match n with @@ -7,3 +7,17 @@ Fixpoint plus1 (n m:nat) {struct n} : nat := | S p => S (p+m) end where "n + m" := (plus1 n m) : nat_scope. + +(* Check behaviour wrt yet empty levels (see Stephane's bug #1850) *) + +Parameter P : Type -> Type -> Type -> Type. +Notation "e |= t --> v" := (P e t v) (at level 100, t at level 54). +Check (nat |= nat --> nat). + +(* Check that first non empty definition at an empty level can be of any + associativity *) + +Definition marker := O. +Notation "x +1" := (S x) (at level 8, left associativity). +Reset marker. +Notation "x +1" := (S x) (at level 8, right associativity). diff --git a/test-suite/success/Omega.v b/test-suite/success/Omega.v index 2d29a835..ecbf04e4 100644 --- a/test-suite/success/Omega.v +++ b/test-suite/success/Omega.v @@ -10,14 +10,14 @@ intros x y. omega. Qed. -(* Proposed by Pierre Crégut *) +(* Proposed by Pierre Crégut *) Lemma lem2 : forall x : Z, (x < 4)%Z -> (x > 2)%Z -> x = 3%Z. intro. omega. Qed. -(* Proposed by Jean-Christophe Filliâtre *) +(* Proposed by Jean-Christophe Filliâtre *) Lemma lem3 : forall x y : Z, x = y -> (x + x)%Z = (y + y)%Z. Proof. @@ -25,7 +25,7 @@ intros. omega. Qed. -(* Proposed by Jean-Christophe Filliâtre: confusion between an Omega *) +(* Proposed by Jean-Christophe Filliâtre: confusion between an Omega *) (* internal variable and a section variable (June 2001) *) Section A. @@ -87,10 +87,8 @@ Qed. (* Check that the interpretation of mult on nat enforces its positivity *) (* Submitted by Hubert Thierry (bug #743) *) -(* Postponed... problem with goals of the form "(n*m=0)%nat -> (n*m=0)%Z" -Require Omega. -Lemma lem10 : (n, m : nat) (le n (plus n (mult n m))). +(* Postponed... problem with goals of the form "(n*m=0)%nat -> (n*m=0)%Z" *) +Lemma lem10 : forall n m:nat, le n (plus n (mult n m)). Proof. -Intros; Omega. +intros; omega with *. Qed. -*) diff --git a/test-suite/success/OmegaPre.v b/test-suite/success/OmegaPre.v new file mode 100644 index 00000000..bb800b7a --- /dev/null +++ b/test-suite/success/OmegaPre.v @@ -0,0 +1,127 @@ +Require Import ZArith Nnat Omega. +Open Scope Z_scope. + +(** Test of the zify preprocessor for (R)Omega *) + +(* More details in file PreOmega.v + + (r)omega with Z : starts with zify_op + (r)omega with nat : starts with zify_nat + (r)omega with positive : starts with zify_positive + (r)omega with N : starts with uses zify_N + (r)omega with * : starts zify (a saturation of the others) +*) + +(* zify_op *) + +Goal forall a:Z, Zmax a a = a. +intros. +omega with *. +Qed. + +Goal forall a b:Z, Zmax a b = Zmax b a. +intros. +omega with *. +Qed. + +Goal forall a b c:Z, Zmax a (Zmax b c) = Zmax (Zmax a b) c. +intros. +omega with *. +Qed. + +Goal forall a b:Z, Zmax a b + Zmin a b = a + b. +intros. +omega with *. +Qed. + +Goal forall a:Z, (Zabs a)*(Zsgn a) = a. +intros. +zify. +intuition; subst; omega. (* pure multiplication: omega alone can't do it *) +Qed. + +Goal forall a:Z, Zabs a = a -> a >= 0. +intros. +omega with *. +Qed. + +Goal forall a:Z, Zsgn a = a -> a = 1 \/ a = 0 \/ a = -1. +intros. +omega with *. +Qed. + +(* zify_nat *) + +Goal forall m: nat, (m<2)%nat -> (0<= m+m <=2)%nat. +intros. +omega with *. +Qed. + +Goal forall m:nat, (m<1)%nat -> (m=0)%nat. +intros. +omega with *. +Qed. + +Goal forall m: nat, (m<=100)%nat -> (0<= m+m <=200)%nat. +intros. +omega with *. +Qed. +(* 2000 instead of 200: works, but quite slow *) + +Goal forall m: nat, (m*m>=0)%nat. +intros. +omega with *. +Qed. + +(* zify_positive *) + +Goal forall m: positive, (m<2)%positive -> (2 <= m+m /\ m+m <= 2)%positive. +intros. +omega with *. +Qed. + +Goal forall m:positive, (m<2)%positive -> (m=1)%positive. +intros. +omega with *. +Qed. + +Goal forall m: positive, (m<=1000)%positive -> (2<=m+m/\m+m <=2000)%positive. +intros. +omega with *. +Qed. + +Goal forall m: positive, (m*m>=1)%positive. +intros. +omega with *. +Qed. + +(* zify_N *) + +Goal forall m:N, (m<2)%N -> (0 <= m+m /\ m+m <= 2)%N. +intros. +omega with *. +Qed. + +Goal forall m:N, (m<1)%N -> (m=0)%N. +intros. +omega with *. +Qed. + +Goal forall m:N, (m<=1000)%N -> (0<=m+m/\m+m <=2000)%N. +intros. +omega with *. +Qed. + +Goal forall m:N, (m*m>=0)%N. +intros. +omega with *. +Qed. + +(* mix of datatypes *) + +Goal forall p, Z_of_N (N_of_nat (nat_of_N (Npos p))) = Zpos p. +intros. +omega with *. +Qed. + + diff --git a/test-suite/success/ROmega.v b/test-suite/success/ROmega.v index ff1f57df..0c37c59a 100644 --- a/test-suite/success/ROmega.v +++ b/test-suite/success/ROmega.v @@ -68,31 +68,29 @@ Variable n : nat. Variable ap_n : n <> 0. Let delta := f n ap_n. Lemma lem7 : n = n. - (*romega. ---> ROMEGA CANT DEAL WITH NAT*) -Admitted. + romega with nat. +Qed. End C. (* Problem of dependencies *) Require Import Omega. Lemma lem8 : forall H : 0 = 0 -> 0 = 0, H = H -> 0 = 0. intros. -(* romega. ---> ROMEGA CANT DEAL WITH NAT*) -Admitted. +romega with nat. +Qed. (* Bug that what caused by the use of intro_using in Omega *) Require Import Omega. Lemma lem9 : forall p q : nat, ~ (p <= q /\ p < q \/ q <= p /\ p < q) -> p < p \/ p <= p. intros. -(* romega. ---> ROMEGA CANT DEAL WITH NAT*) -Admitted. +romega with nat. +Qed. (* Check that the interpretation of mult on nat enforces its positivity *) (* Submitted by Hubert Thierry (bug #743) *) -(* Postponed... problem with goals of the form "(n*m=0)%nat -> (n*m=0)%Z" -Require Omega. -Lemma lem10 : (n, m : nat) (le n (plus n (mult n m))). +(* Postponed... problem with goals of the form "(n*m=0)%nat -> (n*m=0)%Z" *) +Lemma lem10 : forall n m : nat, le n (plus n (mult n m)). Proof. -Intros; Omega. +intros; romega with nat. Qed. -*) diff --git a/test-suite/success/ROmegaPre.v b/test-suite/success/ROmegaPre.v new file mode 100644 index 00000000..550edca5 --- /dev/null +++ b/test-suite/success/ROmegaPre.v @@ -0,0 +1,127 @@ +Require Import ZArith Nnat ROmega. +Open Scope Z_scope. + +(** Test of the zify preprocessor for (R)Omega *) + +(* More details in file PreOmega.v + + (r)omega with Z : starts with zify_op + (r)omega with nat : starts with zify_nat + (r)omega with positive : starts with zify_positive + (r)omega with N : starts with uses zify_N + (r)omega with * : starts zify (a saturation of the others) +*) + +(* zify_op *) + +Goal forall a:Z, Zmax a a = a. +intros. +romega with *. +Qed. + +Goal forall a b:Z, Zmax a b = Zmax b a. +intros. +romega with *. +Qed. + +Goal forall a b c:Z, Zmax a (Zmax b c) = Zmax (Zmax a b) c. +intros. +romega with *. +Qed. + +Goal forall a b:Z, Zmax a b + Zmin a b = a + b. +intros. +romega with *. +Qed. + +Goal forall a:Z, (Zabs a)*(Zsgn a) = a. +intros. +zify. +intuition; subst; romega. (* pure multiplication: omega alone can't do it *) +Qed. + +Goal forall a:Z, Zabs a = a -> a >= 0. +intros. +romega with *. +Qed. + +Goal forall a:Z, Zsgn a = a -> a = 1 \/ a = 0 \/ a = -1. +intros. +romega with *. +Qed. + +(* zify_nat *) + +Goal forall m: nat, (m<2)%nat -> (0<= m+m <=2)%nat. +intros. +romega with *. +Qed. + +Goal forall m:nat, (m<1)%nat -> (m=0)%nat. +intros. +romega with *. +Qed. + +Goal forall m: nat, (m<=100)%nat -> (0<= m+m <=200)%nat. +intros. +romega with *. +Qed. +(* 2000 instead of 200: works, but quite slow *) + +Goal forall m: nat, (m*m>=0)%nat. +intros. +romega with *. +Qed. + +(* zify_positive *) + +Goal forall m: positive, (m<2)%positive -> (2 <= m+m /\ m+m <= 2)%positive. +intros. +romega with *. +Qed. + +Goal forall m:positive, (m<2)%positive -> (m=1)%positive. +intros. +romega with *. +Qed. + +Goal forall m: positive, (m<=1000)%positive -> (2<=m+m/\m+m <=2000)%positive. +intros. +romega with *. +Qed. + +Goal forall m: positive, (m*m>=1)%positive. +intros. +romega with *. +Qed. + +(* zify_N *) + +Goal forall m:N, (m<2)%N -> (0 <= m+m /\ m+m <= 2)%N. +intros. +romega with *. +Qed. + +Goal forall m:N, (m<1)%N -> (m=0)%N. +intros. +romega with *. +Qed. + +Goal forall m:N, (m<=1000)%N -> (0<=m+m/\m+m <=2000)%N. +intros. +romega with *. +Qed. + +Goal forall m:N, (m*m>=0)%N. +intros. +romega with *. +Qed. + +(* mix of datatypes *) + +Goal forall p, Z_of_N (N_of_nat (nat_of_N (Npos p))) = Zpos p. +intros. +romega with *. +Qed. + + diff --git a/test-suite/success/apply.v b/test-suite/success/apply.v index 4f260696..fcce68b9 100644 --- a/test-suite/success/apply.v +++ b/test-suite/success/apply.v @@ -7,8 +7,197 @@ assumption. Qed. Require Import ZArith. -Open Scope Z_scope. -Goal forall x y z, ~ z <= 0 -> x * z < y * z -> x <= y. +Goal (forall x y z, ~ z <= 0 -> x * z < y * z -> x <= y)%Z. intros; apply Znot_le_gt, Zgt_lt in H. apply Zmult_lt_reg_r, Zlt_le_weak in H0; auto. Qed. + +(* Check if it unfolds when there are not enough premises *) + +Goal forall n, n = S n -> False. +intros. +apply n_Sn in H. +assumption. +Qed. + +(* Check naming in with bindings; printing used to be inconsistent before *) +(* revision 9450 *) + +Notation S':=S (only parsing). +Goal (forall S, S = S' S) -> (forall S, S = S' S). +intros. +apply H with (S0 := S). +Qed. + +(* Check inference of implicit arguments in bindings *) + +Goal exists y : nat -> Type, y 0 = y 0. +exists (fun x => True). +trivial. +Qed. + +(* Check universe handling in typed unificationn *) + +Definition E := Type. +Goal exists y : E, y = y. +exists Prop. +trivial. +Qed. + +Variable Eq : Prop = (Prop -> Prop) :> E. +Goal Prop. +rewrite Eq. +Abort. + +(* Check insertion of coercions in bindings *) + +Coercion eq_true : bool >-> Sortclass. +Goal exists A:Prop, A = A. +exists true. +trivial. +Qed. + +(* Check use of unification of bindings types in specialize *) + +Variable P : nat -> Prop. +Variable L : forall (l : nat), P l -> P l. +Goal P 0 -> True. +intros. +specialize L with (1:=H). +Abort. +Reset P. + +(* Two examples that show that hnf_constr is used when unifying types + of bindings (a simplification of a script from Field_Theory) *) + +Require Import List. +Open Scope list_scope. +Fixpoint P (l : list nat) : Prop := + match l with + | nil => True + | e1 :: nil => e1 = e1 + | e1 :: l1 => e1 = e1 /\ P l1 + end. +Variable L : forall n l, P (n::l) -> P l. + +Goal forall (x:nat) l, P (x::l) -> P l. +intros. +apply L with (1:=H). +Qed. + +Goal forall (x:nat) l, match l with nil => x=x | _::_ => x=x /\ P l end -> P l. +intros. +apply L with (1:=H). +Qed. + +(* The following call to auto fails if the type of the clause + associated to the H is not beta-reduced [but apply H works] + (a simplification of a script from FSetAVL) *) + +Definition apply (f:nat->Prop) := forall x, f x. +Goal apply (fun n => n=0) -> 1=0. +intro H. +auto. +Qed. + +(* The following fails if the coercion Zpos is not introduced around p + before trying a subterm that matches the left-hand-side of the equality + (a simplication of an example taken from Nijmegen/QArith) *) + +Require Import ZArith. +Coercion Zpos : positive >-> Z. +Variable f : Z -> Z -> Z. +Variable g : forall q1 q2 p : Z, f (f q1 p) (f q2 p) = Z0. +Goal forall p q1 q2, f (f q1 (Zpos p)) (f q2 (Zpos p)) = Z0. +intros; rewrite g with (p:=p). +reflexivity. +Qed. + +(* A funny example where the behavior differs depending on which of a + multiple solution to a unification problem is chosen (an instance + of this case can be found in the proof of Buchberger.BuchRed.nf_divp) *) + +Definition succ x := S x. +Goal forall (I : nat -> Set) (P : nat -> Prop) (Q : forall n:nat, I n -> Prop), + (forall x y, P x -> Q x y) -> + (forall x, P (S x)) -> forall y: I (S 0), Q (succ 0) y. +intros. +apply H with (y:=y). +(* [x] had two possible instances: [S 0], coming from unifying the + type of [y] with [I ?n] and [succ 0] coming from the unification with + the goal; only the first one allows to make the next apply (which + does not work modulo delta) working *) +apply H0. +Qed. + +(* A similar example with a arbitrary long conversion between the two + possible instances *) + +Fixpoint compute_succ x := + match x with O => S 0 | S n => S (compute_succ n) end. + +Goal forall (I : nat -> Set) (P : nat -> Prop) (Q : forall n:nat, I n -> Prop), + (forall x y, P x -> Q x y) -> + (forall x, P (S x)) -> forall y: I (S 100), Q (compute_succ 100) y. +intros. +apply H with (y:=y). +apply H0. +Qed. + +(* Another example with multiple convertible solutions to the same + metavariable (extracted from Algebra.Hom_module.Hom_module, 10th + subgoal which precisely fails) *) + +Definition ID (A:Type) := A. +Goal forall f:Type -> Type, + forall (P : forall A:Type, A -> Prop), + (forall (B:Type) x, P (f B) x -> P (f B) x) -> + (forall (A:Type) x, P (f (f A)) x) -> + forall (A:Type) (x:f (f A)), P (f (ID (f A))) x. +intros. +apply H. +(* The parameter [B] had two possible instances: [ID (f A)] by direct + unification and [f A] by unification of the type of [x]; only the + first choice makes the next command fail, as it was + (unfortunately?) in Hom_module *) +try apply H. +unfold ID; apply H0. +Qed. + +(* Test coercion below product and on non meta-free terms in with bindings *) +(* Cf wishes #1408 from E. Makarov *) + +Parameter bool_Prop :> bool -> Prop. +Parameter r : bool -> bool -> bool. +Axiom ax : forall (A : Set) (R : A -> A -> Prop) (x y : A), R x y. + +Theorem t : r true false. +apply ax with (R := r). +Qed. + +(* Check verification of type at unification (submitted by Stéphane Lengrand): + without verification, the first "apply" works what leads to the incorrect + instantiation of x by Prop *) + +Theorem u : ~(forall x:Prop, ~x). +unfold not. +intro. +eapply H. +apply (forall B:Prop,B->B) || (instantiate (1:=True); exact I). +Defined. + +(* Fine-tuning coercion insertion in presence of unfolding (bug #1883) *) + +Parameter name : Set. +Definition atom := name. + +Inductive exp : Set := + | var : atom -> exp. + +Coercion var : atom >-> exp. + +Axiom silly_axiom : forall v : exp, v = v -> False. + +Lemma silly_lemma : forall x : atom, False. +intros x. +apply silly_axiom with (v := x). (* fails *) diff --git a/test-suite/success/cc.v b/test-suite/success/cc.v index fecc8977..94d827fd 100644 --- a/test-suite/success/cc.v +++ b/test-suite/success/cc.v @@ -78,6 +78,14 @@ intros. congruence. Qed. +(* example with implications *) + +Theorem arrow : forall (A B: Prop) (C D:Set) , A=B -> C=D -> +(A -> C) = (B -> D). +congruence. +Qed. + + Set Implicit Arguments. Parameter elt: Set. @@ -94,5 +102,6 @@ Proof. auto. Qed. +
\ No newline at end of file diff --git a/test-suite/success/change.v b/test-suite/success/change.v new file mode 100644 index 00000000..cea01712 --- /dev/null +++ b/test-suite/success/change.v @@ -0,0 +1,6 @@ +(* A few tests of the syntax of clauses and of the interpretation of change *) + +Goal let a := 0+0 in a=a. +intro. +change 0 in (value of a). +change ((fun A:Type => A) nat) in (type of a). diff --git a/test-suite/success/clear.v b/test-suite/success/clear.v index 444146f7..8169361c 100644 --- a/test-suite/success/clear.v +++ b/test-suite/success/clear.v @@ -1,6 +1,15 @@ Goal forall x:nat, (forall x, x=0 -> True)->True. intros; eapply H. instantiate (1:=(fun y => _) (S x)). - simpl. - clear x || trivial. + simpl. + clear x. trivial. Qed. + +Goal forall y z, (forall x:nat, x=y -> True) -> y=z -> True. + intros; eapply H. + rename z into z'. + clear H0. + clear z'. + reflexivity. +Qed. + diff --git a/test-suite/success/conv_pbs.v b/test-suite/success/conv_pbs.v new file mode 100644 index 00000000..062c3ee5 --- /dev/null +++ b/test-suite/success/conv_pbs.v @@ -0,0 +1,223 @@ +(* A bit complex but realistic example whose last fixpoint definition + used to fail in 8.1 because of wrong environment in conversion + problems (see revision 9664) *) + +Require Import List. +Require Import Arith. + +Parameter predicate : Set. +Parameter function : Set. +Definition variable := nat. +Definition x0 := 0. +Definition var_eq_dec := eq_nat_dec. + +Inductive term : Set := + | App : function -> term -> term + | Var : variable -> term. + +Definition atom := (predicate * term)%type. + +Inductive formula : Set := + | Atom : atom -> formula + | Imply : formula -> formula -> formula + | Forall : variable -> formula -> formula. + +Notation "A --> B" := (Imply A B) (at level 40). + +Definition substitution range := list (variable * range). + +Fixpoint remove_assoc (A:Set)(x:variable)(rho: substitution A){struct rho} + : substitution A := + match rho with + | nil => rho + | (y,t) :: rho => if var_eq_dec x y then remove_assoc A x rho + else (y,t) :: remove_assoc A x rho + end. + +Fixpoint assoc (A:Set)(x:variable)(rho:substitution A){struct rho} + : option A := + match rho with + | nil => None + | (y,t) :: rho => if var_eq_dec x y then Some t + else assoc A x rho + end. + +Fixpoint subst_term (rho:substitution term)(t:term){struct t} : term := + match t with + | Var x => match assoc _ x rho with + | Some a => a + | None => Var x + end + | App f t' => App f (subst_term rho t') + end. + +Fixpoint subst_formula (rho:substitution term)(A:formula){struct A}:formula := + match A with + | Atom (p,t) => Atom (p, subst_term rho t) + | A --> B => subst_formula rho A --> subst_formula rho B + | Forall y A => Forall y (subst_formula (remove_assoc _ y rho) A) + (* assume t closed *) + end. + +Definition subst A x t := subst_formula ((x,t):: nil) A. + +Record Kripke : Type := { + worlds: Set; + wle : worlds -> worlds -> Type; + wle_refl : forall w, wle w w ; + wle_trans : forall w w' w'', wle w w' -> wle w' w'' -> wle w w''; + domain : Set; + vars : variable -> domain; + funs : function -> domain -> domain; + atoms : worlds -> predicate * domain -> Type; + atoms_mon : forall w w', wle w w' -> forall P, atoms w P -> atoms w' P +}. + +Section Sem. + +Variable K : Kripke. + +Fixpoint sem (rho: substitution (domain K))(t:term){struct t} : domain K := + match t with + | Var x => match assoc _ x rho with + | Some a => a + | None => vars K x + end + | App f t' => funs K f (sem rho t') + end. + +End Sem. + +Notation "w <= w'" := (wle _ w w'). + +Set Implicit Arguments. + +Reserved Notation "w ||- A" (at level 70). + +Definition context := list formula. + +Variable fresh : variable -> context -> Prop. + +Variable fresh_out : context -> variable. + +Axiom fresh_out_spec : forall Gamma, fresh (fresh_out Gamma) Gamma. + +Axiom fresh_peel : forall x A Gamma, fresh x (A::Gamma) -> fresh x Gamma. + +Fixpoint force (K:Kripke)(rho: substitution (domain K))(w:worlds K)(A:formula) + {struct A} : Type := + match A with + | Atom (p,t) => atoms K w (p, sem K rho t) + | A --> B => forall w', w <= w' -> force K rho w' A -> force K rho w' B + | Forall x A => forall w', w <= w' -> forall t, force K ((x,t)::remove_assoc _ x rho) w' A + end. + +Notation "w ||- A" := (force _ nil w A). + +Reserved Notation "Gamma |- A" (at level 70). +Reserved Notation "Gamma ; A |- C" (at level 70, A at next level). + +Inductive context_prefix (Gamma:context) : context -> Type := + | CtxPrefixRefl : context_prefix Gamma Gamma + | CtxPrefixTrans : forall A Gamma', context_prefix Gamma Gamma' -> context_prefix Gamma (cons A Gamma'). + +Inductive in_context (A:formula) : list formula -> Prop := + | InAxiom : forall Gamma, in_context A (cons A Gamma) + | OmWeak : forall Gamma B, in_context A Gamma -> in_context A (cons B Gamma). + +Inductive prove : list formula -> formula -> Type := + | ProofImplyR : forall A B Gamma, prove (cons A Gamma) B + -> prove Gamma (A --> B) + | ProofForallR : forall x A Gamma, (forall y, fresh y (A::Gamma) + -> prove Gamma (subst A x (Var y))) -> prove Gamma (Forall x A) + | ProofCont : forall A Gamma Gamma' C, context_prefix (A::Gamma) Gamma' + -> (prove_stoup Gamma' A C) -> (Gamma' |- C) + +where "Gamma |- A" := (prove Gamma A) + + with prove_stoup : list formula -> formula -> formula -> Type := + | ProofAxiom Gamma C: Gamma ; C |- C + | ProofImplyL Gamma C : forall A B, (Gamma |- A) + -> (prove_stoup Gamma B C) -> (prove_stoup Gamma (A --> B) C) + | ProofForallL Gamma C : forall x t A, (prove_stoup Gamma (subst A x t) C) + -> (prove_stoup Gamma (Forall x A) C) + +where " Gamma ; B |- A " := (prove_stoup Gamma B A). + +Axiom context_prefix_trans : + forall Gamma Gamma' Gamma'', + context_prefix Gamma Gamma' + -> context_prefix Gamma' Gamma'' + -> context_prefix Gamma Gamma''. + +Axiom Weakening : + forall Gamma Gamma' A, + context_prefix Gamma Gamma' -> Gamma |- A -> Gamma' |- A. + +Axiom universal_weakening : + forall Gamma Gamma', context_prefix Gamma Gamma' + -> forall P, Gamma |- Atom P -> Gamma' |- Atom P. + +Canonical Structure Universal := Build_Kripke + context + context_prefix + CtxPrefixRefl + context_prefix_trans + term + Var + App + (fun Gamma P => Gamma |- Atom P) + universal_weakening. + +Axiom subst_commute : + forall A rho x t, + subst_formula ((x,t)::rho) A = subst (subst_formula rho A) x t. + +Axiom subst_formula_atom : + forall rho p t, + Atom (p, sem _ rho t) = subst_formula rho (Atom (p,t)). + +Fixpoint universal_completeness (Gamma:context)(A:formula){struct A} + : forall rho:substitution term, + force _ rho Gamma A -> Gamma |- subst_formula rho A + := + match A + return forall rho, force _ rho Gamma A + -> Gamma |- subst_formula rho A + with + | Atom (p,t) => fun rho H => eq_rect _ (fun A => Gamma |- A) H _ (subst_formula_atom rho p t) + | A --> B => fun rho HImplyAB => + let A' := subst_formula rho A in + ProofImplyR (universal_completeness (A'::Gamma) B rho + (HImplyAB (A'::Gamma)(CtxPrefixTrans A' (CtxPrefixRefl Gamma)) + (universal_completeness_stoup A rho (fun C Gamma' Hle p + => ProofCont Hle p)))) + | Forall x A => fun rho HForallA + => ProofForallR x (fun y Hfresh + => eq_rect _ _ (universal_completeness Gamma A _ + (HForallA Gamma (CtxPrefixRefl Gamma)(Var y))) _ (subst_commute _ _ _ _ )) + end +with universal_completeness_stoup (Gamma:context)(A:formula){struct A} + : forall rho, (forall C Gamma', context_prefix Gamma Gamma' + -> Gamma' ; subst_formula rho A |- C -> Gamma' |- C) + -> force _ rho Gamma A + := + match A return forall rho, + (forall C Gamma', context_prefix Gamma Gamma' + -> Gamma' ; subst_formula rho A |- C + -> Gamma' |- C) + -> force _ rho Gamma A + with + | Atom (p,t) as C => fun rho H + => H _ Gamma (CtxPrefixRefl Gamma)(ProofAxiom _ _) + | A --> B => fun rho H => fun Gamma' Hle HA + => universal_completeness_stoup B rho (fun C Gamma'' Hle' p + => H C Gamma'' (context_prefix_trans Hle Hle') + (ProofImplyL (Weakening Hle' (universal_completeness Gamma' A rho HA)) p)) + | Forall x A => fun rho H => fun Gamma' Hle t + => (universal_completeness_stoup A ((x,t)::remove_assoc _ x rho) + (fun C Gamma'' Hle' p => + H C Gamma'' (context_prefix_trans Hle Hle') + (ProofForallL x t (subst_formula (remove_assoc _ x rho) A) + (eq_rect _ (fun D => Gamma'' ; D |- C) p _ (subst_commute _ _ _ _))))) + end. diff --git a/test-suite/success/decl_mode.v b/test-suite/success/decl_mode.v new file mode 100644 index 00000000..fede31a8 --- /dev/null +++ b/test-suite/success/decl_mode.v @@ -0,0 +1,182 @@ +(* \sqrt 2 is irrationnal, (c) 2006 Pierre Corbineau *) + +Set Firstorder Depth 1. +Require Import ArithRing Wf_nat Peano_dec Div2 Even Lt. + +Lemma double_div2: forall n, div2 (double n) = n. +proof. + assume n:nat. + per induction on n. + suppose it is 0. + suffices (0=0) to show thesis. + thus thesis. + suppose it is (S m) and Hrec:thesis for m. + have (div2 (double (S m))= div2 (S (S (double m)))). + ~= (S (div2 (double m))). + thus ~= (S m) by Hrec. + end induction. +end proof. +Show Script. +Qed. + +Lemma double_inv : forall n m, double n = double m -> n = m . +proof. + let n, m be such that H:(double n = double m). +have (n = div2 (double n)) by double_div2,H. + ~= (div2 (double m)) by H. + thus ~= m by double_div2. +end proof. +Qed. + +Lemma double_mult_l : forall n m, (double (n * m)=n * double m). +proof. + assume n:nat and m:nat. + have (double (n * m) = n*m + n * m). + ~= (n * (m+m)) by * using ring. + thus ~= (n * double m). +end proof. +Qed. + +Lemma double_mult_r : forall n m, (double (n * m)=double n * m). +proof. + assume n:nat and m:nat. + have (double (n * m) = n*m + n * m). + ~= ((n + n) * m) by * using ring. + thus ~= (double n * m). +end proof. +Qed. + +Lemma even_is_even_times_even: forall n, even (n*n) -> even n. +proof. + let n be such that H:(even (n*n)). + per cases of (even n \/ odd n) by even_or_odd. + suppose (odd n). + hence thesis by H,even_mult_inv_r. + end cases. +end proof. +Qed. + +Lemma main_thm_aux: forall n,even n -> +double (double (div2 n *div2 n))=n*n. +proof. + given n such that H:(even n). + *** have (double (double (div2 n * div2 n)) + = double (div2 n) * double (div2 n)) + by double_mult_l,double_mult_r. + thus ~= (n*n) by H,even_double. +end proof. +Qed. + +Require Omega. + +Lemma even_double_n: (forall m, even (double m)). +proof. + assume m:nat. + per induction on m. + suppose it is 0. + thus thesis. + suppose it is (S mm) and thesis for mm. + then H:(even (S (S (mm+mm)))). + have (S (S (mm + mm)) = S mm + S mm) using omega. + hence (even (S mm +S mm)) by H. + end induction. +end proof. +Qed. + +Theorem main_theorem: forall n p, n*n=double (p*p) -> p=0. +proof. + assume n0:nat. + define P n as (forall p, n*n=double (p*p) -> p=0). + claim rec_step: (forall n, (forall m,m<n-> P m) -> P n). + let n be such that H:(forall m : nat, m < n -> P m) and p:nat . + per cases of ({n=0}+{n<>0}) by eq_nat_dec. + suppose H1:(n=0). + per cases on p. + suppose it is (S p'). + assume (n * n = double (S p' * S p')). + =~ 0 by H1,mult_n_O. + ~= (S ( p' + p' * S p' + S p'* S p')) + by plus_n_Sm. + hence thesis . + suppose it is 0. + thus thesis. + end cases. + suppose H1:(n<>0). + assume H0:(n*n=double (p*p)). + have (even (double (p*p))) by even_double_n . + then (even (n*n)) by H0. + then H2:(even n) by even_is_even_times_even. + then (double (double (div2 n *div2 n))=n*n) + by main_thm_aux. + ~= (double (p*p)) by H0. + then H':(double (div2 n *div2 n)= p*p) by double_inv. + have (even (double (div2 n *div2 n))) by even_double_n. + then (even (p*p)) by even_double_n,H'. + then H3:(even p) by even_is_even_times_even. + have (double(double (div2 n * div2 n)) = n*n) + by H2,main_thm_aux. + ~= (double (p*p)) by H0. + ~= (double(double (double (div2 p * div2 p)))) + by H3,main_thm_aux. + then H'':(div2 n * div2 n = double (div2 p * div2 p)) + by double_inv. + then (div2 n < n) by lt_div2,neq_O_lt,H1. + then H4:(div2 p=0) by (H (div2 n)),H''. + then (double (div2 p) = double 0). + =~ p by even_double,H3. + thus ~= 0. + end cases. + end claim. + hence thesis by (lt_wf_ind n0 P). +end proof. +Qed. + +Require Import Reals Field. +(*Coercion INR: nat >->R. +Coercion IZR: Z >->R.*) + +Open Scope R_scope. + +Lemma square_abs_square: + forall p,(INR (Zabs_nat p) * INR (Zabs_nat p)) = (IZR p * IZR p). +proof. + assume p:Z. + per cases on p. + suppose it is (0%Z). + thus thesis. + suppose it is (Zpos z). + thus thesis. + suppose it is (Zneg z). + have ((INR (Zabs_nat (Zneg z)) * INR (Zabs_nat (Zneg z))) = + (IZR (Zpos z) * IZR (Zpos z))). + ~= ((- IZR (Zpos z)) * (- IZR (Zpos z))). + thus ~= (IZR (Zneg z) * IZR (Zneg z)). + end cases. +end proof. +Qed. + +Definition irrational (x:R):Prop := + forall (p:Z) (q:nat),q<>0%nat -> x<> (IZR p/INR q). + +Theorem irrationnal_sqrt_2: irrational (sqrt (INR 2%nat)). +proof. + let p:Z,q:nat be such that H:(q<>0%nat) + and H0:(sqrt (INR 2%nat)=(IZR p/INR q)). + have H_in_R:(INR q<>0:>R) by H. + have triv:((IZR p/INR q* INR q) =IZR p :>R) by * using field. + have sqrt2:((sqrt (INR 2%nat) * sqrt (INR 2%nat))= INR 2%nat:>R) by sqrt_def. + have (INR (Zabs_nat p * Zabs_nat p) + = (INR (Zabs_nat p) * INR (Zabs_nat p))) + by mult_INR. + ~= (IZR p* IZR p) by square_abs_square. + ~= ((IZR p/INR q*INR q)*(IZR p/INR q*INR q)) by triv. (* we have to factor because field is too weak *) + ~= ((IZR p/INR q)*(IZR p/INR q)*(INR q*INR q)) using ring. + ~= (sqrt (INR 2%nat) * sqrt (INR 2%nat)*(INR q*INR q)) by H0. + ~= (INR (2%nat * (q*q))) by sqrt2,mult_INR. + then (Zabs_nat p * Zabs_nat p = 2* (q * q))%nat. + ~= ((q*q)+(q*q))%nat. + ~= (Div2.double (q*q)). + then (q=0%nat) by main_theorem. + hence thesis by H. +end proof. +Qed. diff --git a/test-suite/success/dependentind.v b/test-suite/success/dependentind.v new file mode 100644 index 00000000..48255386 --- /dev/null +++ b/test-suite/success/dependentind.v @@ -0,0 +1,100 @@ +Require Import Coq.Program.Program. +Set Implicit Arguments. +Unset Strict Implicit. + +Variable A : Set. + +Inductive vector : nat -> Type := vnil : vector 0 | vcons : A -> forall n, vector n -> vector (S n). + +Goal forall n, forall v : vector (S n), vector n. +Proof. + intros n H. + dependent destruction H. + assumption. +Save. + +Require Import ProofIrrelevance. + +Goal forall n, forall v : vector (S n), exists v' : vector n, exists a : A, v = vcons a v'. +Proof. + intros n v. + dependent destruction v. + exists v ; exists a. + reflexivity. +Save. + +(* Extraction Unnamed_thm. *) + +Inductive type : Type := +| base : type +| arrow : type -> type -> type. + +Notation " t --> t' " := (arrow t t') (at level 20, t' at next level). + +Inductive ctx : Type := +| empty : ctx +| snoc : ctx -> type -> ctx. + +Notation " Γ , Ï„ " := (snoc Γ Ï„) (at level 25, t at next level, left associativity). + +Fixpoint conc (Γ Δ : ctx) : ctx := + match Δ with + | empty => Γ + | snoc Δ' x => snoc (conc Γ Δ') x + end. + +Notation " Γ ; Δ " := (conc Γ Δ) (at level 25, left associativity). + +Inductive term : ctx -> type -> Type := +| ax : forall Γ Ï„, term (Γ, Ï„) Ï„ +| weak : forall Γ Ï„, term Γ Ï„ -> forall Ï„', term (Γ, Ï„') Ï„ +| abs : forall Γ Ï„ Ï„', term (Γ , Ï„) Ï„' -> term Γ (Ï„ --> Ï„') +| app : forall Γ Ï„ Ï„', term Γ (Ï„ --> Ï„') -> term Γ Ï„ -> term Γ Ï„'. + +Lemma weakening : forall Γ Δ Ï„, term (Γ ; Δ) Ï„ -> + forall Ï„', term (Γ , Ï„' ; Δ) Ï„. +Proof with simpl in * ; auto ; simpl_depind. + intros Γ Δ Ï„ H. + + dependent induction H. + + destruct Δ... + apply weak ; apply ax. + + apply ax. + + destruct Δ... + specialize (IHterm Γ empty)... + apply weak... + + apply weak... + + destruct Δ... + apply weak ; apply abs ; apply H. + + apply abs... + specialize (IHterm Γ0 (Δ, t, Ï„))... + + apply app with Ï„... +Qed. + +Lemma exchange : forall Γ Δ α β Ï„, term (Γ, α, β ; Δ) Ï„ -> term (Γ, β, α ; Δ) Ï„. +Proof with simpl in * ; simpl_depind ; auto. + intros until 1. + dependent induction H. + + destruct Δ... + apply weak ; apply ax. + + apply ax. + + destruct Δ... + pose (weakening (Γ:=Γ0) (Δ:=(empty, α)))... + + apply weak... + + apply abs... + specialize (IHterm Γ0 α β (Δ, Ï„))... + + eapply app with Ï„... +Save. diff --git a/test-suite/success/destruct.v b/test-suite/success/destruct.v index 9f938e10..5aa78816 100644 --- a/test-suite/success/destruct.v +++ b/test-suite/success/destruct.v @@ -23,3 +23,35 @@ set (b := true) in *. try destruct b. Abort. +(* Used to fail with error "n is used in conclusion" before revision 9447 *) + +Goal forall n, n = S n. +induction S. +Abort. + +(* Check that elimination with remaining evars do not raise an bad + error message *) + +Theorem Refl : forall P, P <-> P. tauto. Qed. +Goal True. +case Refl || ecase Refl. +Abort. + + +(* Submitted by B. Baydemir (bug #1882) *) + +Require Import List. + +Definition alist R := list (nat * R)%type. + +Section Properties. + Variables A : Type. + Variables a : A. + Variables E : alist A. + + Lemma silly : E = E. + Proof. + clear. induction E. (* this fails. *) + Abort. + +End Properties. diff --git a/test-suite/success/evars.v b/test-suite/success/evars.v index ad69ced1..082cbfbe 100644 --- a/test-suite/success/evars.v +++ b/test-suite/success/evars.v @@ -68,9 +68,145 @@ Proof. trivial. Qed. Hint Resolve contradiction. Goal False. eauto. +Abort. (* This used to fail in V8.1beta because first-order unification was used before using type information *) Check (exist _ O (refl_equal 0) : {n:nat|n=0}). Check (exist _ O I : {n:nat|True}). + +(* An example (initially from Marseille/Fairisle) that involves an evar with + different solutions (Input, Output or bool) that may or may not be + considered distinct depending on which kind of conversion is used *) + +Section A. +Definition STATE := (nat * bool)%type. +Let Input := bool. +Let Output := bool. +Parameter Out : STATE -> Output. +Check fun (s : STATE) (reg : Input) => reg = Out s. +End A. + +(* The return predicate found should be: "in _=U return U" *) +(* (feature already available in V8.0) *) + +Definition g (T1 T2:Type) (x:T1) (e:T1=T2) : T2 := + match e with + | refl_equal => x + end. + +(* An example extracted from FMapAVL which (may) test restriction on + evars problems of the form ?n[args1]=?n[args2] with distinct args1 + and args2 *) + +Set Implicit Arguments. +Parameter t:Set->Set. +Parameter map:forall elt elt' : Set, (elt -> elt') -> t elt -> t elt'. +Parameter avl: forall elt : Set, t elt -> Prop. +Parameter bst: forall elt : Set, t elt -> Prop. +Parameter map_avl: forall (elt elt' : Set) (f : elt -> elt') (m : t elt), + avl m -> avl (map f m). +Parameter map_bst: forall (elt elt' : Set) (f : elt -> elt') (m : t elt), + bst m -> bst (map f m). +Record bbst (elt:Set) : Set := + Bbst {this :> t elt; is_bst : bst this; is_avl: avl this}. +Definition t' := bbst. +Section B. +Variables elt elt': Set. +Definition map' f (m:t' elt) : t' elt' := + Bbst (map_bst f m.(is_bst)) (map_avl f m.(is_avl)). +End B. +Unset Implicit Arguments. + +(* An example from Lexicographic_Exponentiation that tests the + contraction of reducible fixpoints in type inference *) + +Require Import List. +Check (fun (A:Set) (a b x:A) (l:list A) + (H : l ++ cons x nil = cons b (cons a nil)) => + app_inj_tail l (cons b nil) _ _ H). + +(* An example from NMake (simplified), that uses restriction in solve_refl *) + +Parameter h:(nat->nat)->(nat->nat). +Fixpoint G p cont {struct p} := + h (fun n => match p with O => cont | S p => G p cont end n). + +(* An example from Bordeaux/Cantor that applies evar restriction + below a binder *) + +Require Import Relations. +Parameter lex : forall (A B : Set), (forall (a1 a2:A), {a1=a2}+{a1<>a2}) +-> relation A -> relation B -> A * B -> A * B -> Prop. +Check + forall (A B : Set) eq_A_dec o1 o2, + antisymmetric A o1 -> transitive A o1 -> transitive B o2 -> + transitive _ (lex _ _ eq_A_dec o1 o2). + +(* Another example from Julien Forest that tests unification below binders *) + +Require Import List. +Set Implicit Arguments. +Parameter + merge : forall (A B : Set) (eqA : forall (a1 a2 : A), {a1=a2}+{a1<>a2}) + (eqB : forall (b1 b2 : B), {b1=b2}+{b1<>b2}) + (partial_res l : list (A*B)), option (list (A*B)). +Axiom merge_correct : + forall (A B : Set) eqA eqB (l1 l2 : list (A*B)), + (forall a2 b2 c2, In (a2,b2) l2 -> In (a2,c2) l2 -> b2 = c2) -> + match merge eqA eqB l1 l2 with _ => True end. +Unset Implicit Arguments. + +(* An example from Bordeaux/Additions that tests restriction below binders *) + +Section Additions_while. + +Variable A : Set. +Variables P Q : A -> Prop. +Variable le : A -> A -> Prop. +Hypothesis Q_dec : forall s : A, P s -> {Q s} + {~ Q s}. +Hypothesis le_step : forall s : A, ~ Q s -> P s -> {s' | P s' /\ le s' s}. +Hypothesis le_wf : well_founded le. + +Lemma loopexec : forall s : A, P s -> {s' : A | P s' /\ Q s'}. +refine + (well_founded_induction_type le_wf (fun s => _ -> {s' : A | _ /\ _}) + (fun s hr i => + match Q_dec s i with + | left _ => _ + | right _ => + match le_step s _ _ with + | exist s' h' => + match hr s' _ _ with + | exist s'' _ => exist _ s'' _ + end + end + end)). +Abort. + +End Additions_while. + +(* Two examples from G. Melquiond (bugs #1878 and #1884) *) + +Parameter F1 G1 : nat -> Prop. +Goal forall x : nat, F1 x -> G1 x. +refine (fun x H => proj2 (_ x H)). +Abort. + +Goal forall x : nat, F1 x -> G1 x. +refine (fun x H => proj2 (_ x H) _). +Abort. + +(* Remark: the following example does not succeed any longer in 8.2 because, + the algorithm is more general and does exclude a solution that it should + exclude for typing reason. Handling of types and backtracking is still to + be done + +Section S. +Variables A B : nat -> Prop. +Goal forall x : nat, A x -> B x. +refine (fun x H => proj2 (_ x H) _). +Abort. +End S. +*) diff --git a/test-suite/success/extraction.v b/test-suite/success/extraction.v index 0b3060d5..74d87ffa 100644 --- a/test-suite/success/extraction.v +++ b/test-suite/success/extraction.v @@ -84,7 +84,7 @@ Extraction test12. (* type test12 = (__ -> __ -> __) -> __ *) -Definition test13 := match left True I with +Definition test13 := match @left True True I with | left x => 1 | right x => 0 end. diff --git a/test-suite/success/fix.v b/test-suite/success/fix.v index f4a4d36d..78b01f3e 100644 --- a/test-suite/success/fix.v +++ b/test-suite/success/fix.v @@ -1,10 +1,3 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) (* Ancien bug signale par Laurent Thery sur la condition de garde *) Require Import Bool. @@ -50,3 +43,55 @@ Fixpoint maxVar (e : rExpr) : rNat := | rNode n p q => rmax (maxVar p) (maxVar q) end. +(* Check bug #1491 *) + +Require Import Streams. + +Definition decomp (s:Stream nat) : Stream nat := + match s with Cons _ s => s end. + +CoFixpoint bx0 : Stream nat := Cons 0 bx1 +with bx1 : Stream nat := Cons 1 bx0. + +Lemma bx0bx : decomp bx0 = bx1. +simpl. (* used to return bx0 in V8.1 and before instead of bx1 *) +reflexivity. +Qed. + +(* Check mutually inductive statements *) + +Require Import ZArith_base Omega. +Open Scope Z_scope. + +Inductive even: Z -> Prop := +| even_base: even 0 +| even_succ: forall n, odd (n - 1) -> even n +with odd: Z -> Prop := +| odd_succ: forall n, even (n - 1) -> odd n. + +Lemma even_pos_odd_pos: forall n, even n -> n >= 0 +with odd_pos_even_pos : forall n, odd n -> n >= 1. +Proof. + intros. + destruct H. + omega. + apply odd_pos_even_pos in H. + omega. + intros. + destruct H. + apply even_pos_odd_pos in H. + omega. +Qed. + +CoInductive a : Prop := acons : b -> a +with b : Prop := bcons : a -> b. + +Lemma a1 : a +with b1 : b. +Proof. +apply acons. +assumption. + +apply bcons. +assumption. +Qed. diff --git a/test-suite/success/hyps_inclusion.v b/test-suite/success/hyps_inclusion.v new file mode 100644 index 00000000..21bfc075 --- /dev/null +++ b/test-suite/success/hyps_inclusion.v @@ -0,0 +1,32 @@ +(* Simplified example for bug #1325 *) + +(* Explanation: the proof engine see section variables as goal + variables; especially, it can change their types so that, at + type-checking, the section variables are not recognized + (Typeops.check_hyps_inclusion raises "types do no match"). It + worked before the introduction of polymorphic inductive types because + tactics were using Typing.type_of and not Typeops.typing; the former + was not checking hyps inclusion so that the discrepancy in the types + of section variables seen as goal variables was not a problem (at the + end, when the proof is completed, the section variable recovers its + original type and all is correct for Typeops) *) + +Section A. +Variable H:not True. +Lemma f:nat->nat. destruct H. exact I. Defined. +Goal f 0=f 1. +red in H. +(* next tactic was failing wrt bug #1325 because type-checking the goal + detected a syntactically different type for the section variable H *) +case 0. +Reset A. + +(* Variant with polymorphic inductive types for bug #1325 *) + +Section A. +Variable H:not True. +Inductive I (n:nat) : Type := C : H=H -> I n. +Goal I 0. +red in H. +case 0. +Reset A. diff --git a/test-suite/success/implicit.v b/test-suite/success/implicit.v index 47c58f04..9034d6a6 100644 --- a/test-suite/success/implicit.v +++ b/test-suite/success/implicit.v @@ -36,3 +36,13 @@ Check (fun x => @ rhs _ _ (f x)). Fixpoint g n := match n with O => true | S n => g n end. Inductive P n : nat -> Prop := c : P n n. + +(* Avoid evars in the computation of implicit arguments (cf r9827) *) + +Require Import List. + +Fixpoint plus n m {struct n} := + match n with + | 0 => m + | S p => S (plus p m) + end. diff --git a/test-suite/success/ltac.v b/test-suite/success/ltac.v index 3f25f703..757cf6a4 100644 --- a/test-suite/success/ltac.v +++ b/test-suite/success/ltac.v @@ -173,5 +173,50 @@ Abort. empty args *) Goal True. -match None with @None => exact I end. +match constr:@None with @None => exact I end. Abort. + +(* Check second-order pattern unification *) + +Ltac to_exist := + match goal with + |- forall x y, @?P x y => + let Q := eval lazy beta in (exists x, forall y, P x y) in + assert (Q->Q) + end. + +Goal forall x y : nat, x = y. +to_exist. exact (fun H => H). +Abort. + +(* Used to fail in V8.1 *) + +Tactic Notation "test" constr(t) integer(n) := + set (k := t) in |- * at n. + +Goal forall x : nat, x = 1 -> x + x + x = 3. +intros x H. +test x 2. +Abort. + +(* Utilisation de let rec sans arguments *) + +Ltac is := + let rec i := match goal with |- ?A -> ?B => intro; i | _ => idtac end in + i. + +Goal True -> True -> True. +is. +exact I. +Abort. + +(* Interférence entre espaces des noms *) + +Ltac O := intro. +Ltac Z1 t := set (x:=t). +Ltac Z2 t := t. +Goal True -> True. +Z1 O. +Z2 ltac:O. +exact I. +Qed. diff --git a/test-suite/success/options.v b/test-suite/success/options.v index bb678150..f43a4694 100644 --- a/test-suite/success/options.v +++ b/test-suite/success/options.v @@ -20,7 +20,7 @@ Parameter i : bool -> nat. Coercion i : bool >-> nat. Add Printing Coercion i. Remove Printing Coercion i. -Test Printing Coercion i. +Test Printing Coercion for i. Test Printing Let. Test Printing If. diff --git a/test-suite/success/parsing.v b/test-suite/success/parsing.v new file mode 100644 index 00000000..d1b679d5 --- /dev/null +++ b/test-suite/success/parsing.v @@ -0,0 +1,8 @@ +Section A. +Notation "*" := O (at level 8). +Notation "**" := O (at level 99). +Notation "***" := O (at level 9). +End A. +Notation "*" := O (at level 8). +Notation "**" := O (at level 99). +Notation "***" := O (at level 9). diff --git a/test-suite/success/pattern.v b/test-suite/success/pattern.v new file mode 100644 index 00000000..28d0bd55 --- /dev/null +++ b/test-suite/success/pattern.v @@ -0,0 +1,7 @@ +(* Test pattern with dependent occurrences; Note that it does not + behave as the succession of three generalize because each + quantification introduces new occurrences that are automatically + abstracted with the numbering still based on the original statement *) + +Goal (id true,id false)=(id true,id true). +generalize bool at 2 4 6 8 10 as B, true at 3 as tt, false as ff. diff --git a/test-suite/success/refine.v b/test-suite/success/refine.v index 4346ce9a..4b636618 100644 --- a/test-suite/success/refine.v +++ b/test-suite/success/refine.v @@ -87,3 +87,33 @@ refine | exist _ _ => _ end). Abort. + + +(* Use to fail because sigma was not propagated to get_type_of *) +(* Revealed by r9310, fixed in r9359 *) + +Goal + forall f : forall a (H:a=a), Prop, + (forall a (H:a = a :> nat), f a H -> True /\ True) -> + True. +intros. +refine (@proj1 _ _ (H 0 _ _)). +Abort. + +(* Use to fail because let-in with metas in the body where rejected + because a priori considered as dependent *) + +Require Import Peano_dec. + +Definition fact_F : + forall (n:nat), + (forall m, m<n -> nat) -> + nat. +refine + (fun n fact_rec => + if eq_nat_dec n 0 then + 1 + else + let fn := fact_rec (n-1) _ in + n * fn). +Abort. diff --git a/test-suite/success/rewrite.v b/test-suite/success/rewrite.v index 9629b213..86e55922 100644 --- a/test-suite/success/rewrite.v +++ b/test-suite/success/rewrite.v @@ -17,3 +17,24 @@ intros n n' l l'. dependent rewrite (ax n n' l l'). split; reflexivity. Qed. + +(* Used to raise an anomaly instead of an error in 8.1 *) +(* Submitted by Y. Makarov *) + +Parameter N : Set. +Parameter E : N -> N -> Prop. + +Axiom e : forall (A : Set) (EA : A -> A -> Prop) (a : A), EA a a. + +Theorem th : forall x : N, E x x. +intro x. try rewrite e. +Abort. + +(* Behavior of rewrite wrt conversion *) + +Require Import Arith. + +Goal forall n, 0 + n = n -> True. +intros n H. +rewrite plus_0_l in H. +Abort. diff --git a/test-suite/success/setoid_test.v b/test-suite/success/setoid_test.v index dd1022f0..f49f58e5 100644 --- a/test-suite/success/setoid_test.v +++ b/test-suite/success/setoid_test.v @@ -18,7 +18,7 @@ Definition same (s t : set) : Prop := forall a : A, In a s <-> In a t. Lemma setoid_set : Setoid_Theory set same. -unfold same in |- *; split. +unfold same in |- *; split ; red. red in |- *; auto. red in |- *. @@ -104,3 +104,15 @@ setoid_rewrite <- H. trivial. Qed. +(* Unifying the domain up to delta-conversion (example from emakarov) *) + +Definition id: Set -> Set := fun A => A. +Definition rel : forall A : Set, relation (id A) := @eq. +Definition f: forall A : Set, A -> A := fun A x => x. + +Add Relation (id A) (rel A) as eq_rel. + +Add Morphism (@f A) : f_morph. +Proof. +unfold rel, f. trivial. +Qed. diff --git a/test-suite/success/setoid_test2.v b/test-suite/success/setoid_test2.v index bac1cf14..34fff9d1 100644 --- a/test-suite/success/setoid_test2.v +++ b/test-suite/success/setoid_test2.v @@ -120,6 +120,8 @@ Axiom eqS1: S1 -> S1 -> Prop. Axiom SetoidS1 : Setoid_Theory S1 eqS1. Add Setoid S1 eqS1 SetoidS1 as S1setoid. +Instance eqS1_default : DefaultRelation S1 eqS1. + Axiom eqS1': S1 -> S1 -> Prop. Axiom SetoidS1' : Setoid_Theory S1 eqS1'. Axiom SetoidS1'_bis : Setoid_Theory S1 eqS1'. @@ -218,6 +220,8 @@ Axiom eqS1_test8: S1_test8 -> S1_test8 -> Prop. Axiom SetoidS1_test8 : Setoid_Theory S1_test8 eqS1_test8. Add Setoid S1_test8 eqS1_test8 SetoidS1_test8 as S1_test8setoid. +Instance eqS1_test8_default : DefaultRelation S1_test8 eqS1_test8. + Axiom f_test8 : S2 -> S1_test8. Add Morphism f_test8 : f_compat_test8. Admitted. diff --git a/test-suite/success/setoid_test_function_space.v b/test-suite/success/setoid_test_function_space.v index 1602991d..ead93d91 100644 --- a/test-suite/success/setoid_test_function_space.v +++ b/test-suite/success/setoid_test_function_space.v @@ -26,14 +26,14 @@ Hint Unfold feq. Hint Resolve feq_refl feq_sym feq_trans. Variable K:(nat -> nat)->Prop. Variable K_ext:forall a b, (K a)->(a =f b)->(K b). -Add Relation (fun A B:Type => A -> B) feq - reflexivity proved by feq_refl - symmetry proved by feq_sym - transitivity proved by feq_trans as funsetoid. +Add Parametric Relation (A B : Type) : (A -> B) (@feq A B) + reflexivity proved by (@feq_refl A B) + symmetry proved by (@feq_sym A B) + transitivity proved by (@feq_trans A B) as funsetoid. -Add Morphism K with signature feq ==> iff as K_ext1. +Add Morphism K with signature (@feq nat nat) ==> iff as K_ext1. intuition. apply (K_ext H0 H). -intuition. assert (x2 =f x1);auto. apply (K_ext H0 H1). +intuition. assert (y =f x);auto. apply (K_ext H0 H1). Qed. Lemma three:forall n, forall a, (K a)->(a =f (fun m => (a (n+m))))-> (K (fun m diff --git a/test-suite/success/specialize.v b/test-suite/success/specialize.v new file mode 100644 index 00000000..4929ae4c --- /dev/null +++ b/test-suite/success/specialize.v @@ -0,0 +1,48 @@ + +Goal forall a b c : nat, a = b -> b = c -> forall d, a+d=c+d. +intros. + +(* "compatibility" mode: specializing a global name + means a kind of generalize *) + +specialize trans_equal. intros _. +specialize trans_equal with (1:=H)(2:=H0). intros _. +specialize trans_equal with (x:=a)(y:=b)(z:=c). intros _. +specialize trans_equal with (1:=H)(z:=c). intros _. +specialize trans_equal with nat a b c. intros _. +specialize (@trans_equal nat). intros _. +specialize (@trans_equal _ a b c). intros _. +specialize (trans_equal (x:=a)). intros _. +specialize (trans_equal (x:=a)(y:=b)). intros _. +specialize (trans_equal H H0). intros _. +specialize (trans_equal H0 (z:=b)). intros _. + +(* local "in place" specialization *) +assert (Eq:=trans_equal). + +specialize Eq. +specialize Eq with (1:=H)(2:=H0). Undo. +specialize Eq with (x:=a)(y:=b)(z:=c). Undo. +specialize Eq with (1:=H)(z:=c). Undo. +specialize Eq with nat a b c. Undo. +specialize (Eq nat). Undo. +specialize (Eq _ a b c). Undo. +(* no implicit argument for Eq, hence no (Eq (x:=a)) *) +specialize (Eq _ _ _ _ H H0). Undo. +specialize (Eq _ _ _ b H0). Undo. + +(* +(** strange behavior to inspect more precisely *) + +(* 1) proof aspect : let H:= ... in (fun H => ..) H + presque ok... *) + +(* 2) echoue moins lorsque zero premise de mangé *) +specialize trans_equal with (1:=Eq). (* mal typé !! *) + +(* 3) *) +specialize trans_equal with _ a b c. intros _. +(* Anomaly: Evar ?88 was not declared. Please report. *) +*) + +Abort.
\ No newline at end of file diff --git a/test-suite/success/unification.v b/test-suite/success/unification.v index 68869621..91ee18ea 100644 --- a/test-suite/success/unification.v +++ b/test-suite/success/unification.v @@ -15,6 +15,12 @@ Proof. intros; apply (H _ H0). Qed. +Lemma l3 : (forall P, ~(exists x:nat, P x)) + -> forall P:nat->Prop, ~(exists x:nat, P x -> P x). +Proof. +intros; apply H. +Qed. + (* Example submitted for Zenon *) @@ -56,10 +62,67 @@ Require Import Arith. Parameter x y : nat. Parameter G:x=y->x=y->Prop. Parameter K:x<>y->x<>y->Prop. -Lemma l3 : (forall f:x=y->Prop, forall g:x<>y->Prop, +Lemma l4 : (forall f:x=y->Prop, forall g:x<>y->Prop, match eq_nat_dec x y with left a => f a | right a => g a end) -> match eq_nat_dec x y with left a => G a a | right a => K a a end. Proof. intros. apply H. Qed. + + +(* Test unification modulo eta-expansion (if possible) *) + +(* In this example, two instances for ?P (argument of hypothesis H) can be + inferred (one is by unifying the type [Q true] and [?P true] of the + goal and type of [H]; the other is by unifying the argument of [f]); + we need to unify both instances up to allowed eta-expansions of the + instances (eta is allowed if the meta was applied to arguments) + + This used to fail before revision 9389 in trunk +*) + +Lemma l5 : + forall f : (forall P, P true), (forall P, f P = f P) -> + forall Q, f (fun x => Q x) = f (fun x => Q x). +Proof. +intros. +apply H. +Qed. + +(* Test instanciation of evars by unification *) + +Goal (forall x, 0 * x = 0 -> True) -> True. +intros; eapply H. +rewrite <- plus_n_Sm. (* should refine ?x with S ?x' *) +Abort. + +(* Check handling of identity equation between evars *) +(* The example failed to pass until revision 10623 *) + +Lemma l6 : + (forall y, (forall x, (forall z, y = 0 -> y + z = 0) -> y + x = 0) -> True) + -> True. +intros. +eapply H. +intros. +apply H0. (* Check that equation ?n[H] = ?n[H] is correctly considered true *) +reflexivity. +Qed. + +(* Check treatment of metas erased by K-redexes at the time of turning + them to evas *) + +Inductive nonemptyT (t : Type) : Prop := nonemptyT_intro : t -> nonemptyT t. +Goal True. +try case nonemptyT_intro. (* check that it fails w/o anomaly *) +Abort. + +(* Test handling of return type and when it is decided to make the + predicate dependent or not - see "bug" #1851 *) + +Goal forall X (a:X) (f':nat -> X), (exists f : nat -> X, True). +intros. +exists (fun n => match n with O => a | S n' => f' n' end). +constructor. +Qed. diff --git a/test-suite/success/univers.v b/test-suite/success/univers.v index 87edc4de..3c2c0883 100644 --- a/test-suite/success/univers.v +++ b/test-suite/success/univers.v @@ -56,3 +56,7 @@ intro. set (C := forall m, Q m -> Q m). exact I. Qed. + +(* Submitted by Danko Ilik (bug report #1507); related to LetIn *) + +Record U : Type := { A:=Type; a:A }. |