diff options
| author |  Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2010-07-21 09:46:51 +0200 |
| commit | 5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 (patch) | |
| tree | 631ad791a7685edafeb1fb2e8faeedc8379318ae /test-suite/success | |
| parent | da178a880e3ace820b41d38b191d3785b82991f5 (diff) | |
Imported Upstream snapshot 8.3~beta0+13298
Diffstat (limited to 'test-suite/success')
76 files changed, 1985 insertions, 911 deletions
diff --git a/test-suite/success/Abstract.v b/test-suite/success/Abstract.v index fc8800a5..ffd50f6e 100644 --- a/test-suite/success/Abstract.v +++ b/test-suite/success/Abstract.v @@ -18,7 +18,7 @@ Proof. induction n. simpl ; apply Dummy0. replace (2 * S n0) with (2*n0 + 2) ; auto with arith. - apply DummyApp. + apply DummyApp. 2:exact Dummy2. apply IHn0 ; abstract omega. Defined. diff --git a/test-suite/success/AdvancedCanonicalStructure.v b/test-suite/success/AdvancedCanonicalStructure.v index 8e613dca..b533db6e 100644 --- a/test-suite/success/AdvancedCanonicalStructure.v +++ b/test-suite/success/AdvancedCanonicalStructure.v @@ -21,7 +21,6 @@ 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. @@ -54,7 +53,7 @@ Open Scope type_scope. Section type_reification. -Inductive term :Type := +Inductive term :Type := Fun : term -> term -> term | Prod : term -> term -> term | Bool : term @@ -63,18 +62,18 @@ Inductive term :Type := | TYPE :term | Var : Type -> term. -Fixpoint interp (t:term) := - match t with +Fixpoint interp (t:term) := + match t with Bool => bool | SET => Set | PROP => Prop - | TYPE => Type + | TYPE => Type | Fun a b => interp a -> interp b | Prod a b => interp a * interp b | Var x => x end. -Record interp_pair :Type := +Record interp_pair :Type := { repr:>term; abs:>Type; link: abs = interp repr }. @@ -95,25 +94,25 @@ thus thesis using rewrite (link a);rewrite (link b);reflexivity. end proof. Qed. -Canonical Structure ProdCan (a b:interp_pair) := +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) := +Canonical Structure FunCan (a b:interp_pair) := Build_interp_pair (Fun a b) (a -> b) (fun_interp a b). -Canonical Structure BoolCan := +Canonical Structure BoolCan := Build_interp_pair Bool bool (refl_equal _). -Canonical Structure VarCan (x:Type) := +Canonical Structure VarCan (x:Type) := Build_interp_pair (Var x) x (refl_equal _). -Canonical Structure SetCan := +Canonical Structure SetCan := Build_interp_pair SET Set (refl_equal _). -Canonical Structure PropCan := +Canonical Structure PropCan := Build_interp_pair PROP Prop (refl_equal _). -Canonical Structure TypeCan := +Canonical Structure TypeCan := Build_interp_pair TYPE Type (refl_equal _). (* Print Canonical Projections. *) @@ -140,5 +139,5 @@ End type_reification. - + diff --git a/test-suite/success/AdvancedTypeClasses.v b/test-suite/success/AdvancedTypeClasses.v new file mode 100644 index 00000000..b4efa7ed --- /dev/null +++ b/test-suite/success/AdvancedTypeClasses.v @@ -0,0 +1,78 @@ +Generalizable All Variables. + +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. + +Class interp_pair (abs : Type) := + { repr : term; + link: abs = interp repr }. + +Implicit Arguments repr [[interp_pair]]. +Implicit Arguments link [[interp_pair]]. + +Lemma prod_interp `{interp_pair a, interp_pair b} : a * b = interp (Prod (repr a) (repr b)). + simpl. intros. rewrite <- link. rewrite <- (link b). reflexivity. +Qed. + +Lemma fun_interp :forall `{interp_pair a, interp_pair b}, (a -> b) = interp (Fun (repr a) (repr b)). + simpl. intros. rewrite <- link. rewrite <- (link b). reflexivity. +Qed. + +Coercion repr : interp_pair >-> term. + +Definition abs `{interp_pair a} : Type := a. +Coercion abs : interp_pair >-> Sortclass. + +Lemma fun_interp' :forall `{ia : interp_pair, ib : interp_pair}, (ia -> ib) = interp (Fun ia ib). + simpl. intros a ia b ib. rewrite <- link. rewrite <- (link b). reflexivity. +Qed. + +Instance ProdCan `(interp_pair a, interp_pair b) : interp_pair (a * b) := + { repr := Prod (repr a) (repr b) ; link := prod_interp }. + +Instance FunCan `(interp_pair a, interp_pair b) : interp_pair (a -> b) := + { link := fun_interp }. + +Instance BoolCan : interp_pair bool := + { repr := Bool ; link := refl_equal _ }. + +Instance VarCan x : interp_pair x | 10 := { repr := Var x ; link := refl_equal _ }. +Instance SetCan : interp_pair Set := { repr := SET ; link := refl_equal _ }. +Instance PropCan : interp_pair Prop := { repr := PROP ; link := refl_equal _ }. +Instance TypeCan : interp_pair Type := { repr := TYPE ; link := refl_equal _ }. + +(* Print Canonical Projections. *) + +Variable A:Type. + +Variable Inhabited: term -> Prop. + +Variable Inhabited_correct: forall `{interp_pair p}, Inhabited (repr p) -> p. + +Lemma L : Prop * A -> bool * (Type -> Set) . +apply (Inhabited_correct _ _). +change (Inhabited (Fun (Prod PROP (Var A)) (Prod Bool (Fun TYPE SET)))). +Admitted. + +End type_reification. diff --git a/test-suite/success/Case12.v b/test-suite/success/Case12.v index f6a0d578..729ab824 100644 --- a/test-suite/success/Case12.v +++ b/test-suite/success/Case12.v @@ -62,10 +62,10 @@ Check Inductive list''' (A:Set) (B:=(A*A)%type) (a:A) : B -> Set := | nil''' : list''' A a (a,a) - | cons''' : + | cons''' : forall a' : A, let m := (a',a) in list''' A a m -> list''' A a (a,a). -Fixpoint length''' (A:Set) (B:=(A*A)%type) (a:A) (m:B) (l:list''' A a m) +Fixpoint length''' (A:Set) (B:=(A*A)%type) (a:A) (m:B) (l:list''' A a m) {struct l} : nat := match l with | nil''' => 0 diff --git a/test-suite/success/Case15.v b/test-suite/success/Case15.v index 8431880d..69fca48e 100644 --- a/test-suite/success/Case15.v +++ b/test-suite/success/Case15.v @@ -12,7 +12,7 @@ Check (* Suggested by Pierre Letouzey (PR#207) *) Inductive Boite : Set := - boite : forall b : bool, (if b then nat else (nat * nat)%type) -> Boite. + boite : forall b : bool, (if b then nat else (nat * nat)%type) -> Boite. Definition test (B : Boite) := match B return nat with @@ -30,7 +30,7 @@ Check [x] end. Check [x] - Cases x of + Cases x of (c true true) => true | (c false O) => true | _ => false @@ -40,7 +40,7 @@ Check [x] Check [x:I] Cases x of - (c b y) => + (c b y) => (<[b:bool](if b then bool else nat)->bool>if b then [y](if y then true else false) else [y]Cases y of diff --git a/test-suite/success/Case17.v b/test-suite/success/Case17.v index 061e136e..66af9e0d 100644 --- a/test-suite/success/Case17.v +++ b/test-suite/success/Case17.v @@ -11,7 +11,7 @@ Variables (l0 : list bool) (rec : forall l' : list bool, length l' <= S (length l0) -> - {l'' : list bool & + {l'' : list bool & {t : nat | parse_rel l' l'' t /\ length l'' <= length l'}} + {(forall (l'' : list bool) (t : nat), ~ parse_rel l' l'' t)}). @@ -25,17 +25,17 @@ Check | inleft (existS _ _) => inright _ (HHH _) | inright Hnp => inright _ (HHH _) end - :{l'' : list bool & + :{l'' : list bool & {t : nat | parse_rel (true :: l0) l'' t /\ length l'' <= S (length l0)}} + {(forall (l'' : list bool) (t : nat), ~ parse_rel (true :: l0) l'' t)}). - + (* The same but with relative links to l0 and rec *) - + Check (fun (l0 : list bool) (rec : forall l' : list bool, length l' <= S (length l0) -> - {l'' : list bool & + {l'' : list bool & {t : nat | parse_rel l' l'' t /\ length l'' <= length l'}} + {(forall (l'' : list bool) (t : nat), ~ parse_rel l' l'' t)}) => match rec l0 (HHH _) with @@ -45,6 +45,6 @@ Check | inleft (existS _ _) => inright _ (HHH _) | inright Hnp => inright _ (HHH _) end - :{l'' : list bool & + :{l'' : list bool & {t : nat | parse_rel (true :: l0) l'' t /\ length l'' <= S (length l0)}} + {(forall (l'' : list bool) (t : nat), ~ parse_rel (true :: l0) l'' t)}). diff --git a/test-suite/success/Case3.v b/test-suite/success/Case3.v new file mode 100644 index 00000000..de7784ae --- /dev/null +++ b/test-suite/success/Case3.v @@ -0,0 +1,29 @@ +Inductive Le : nat -> nat -> Set := + | LeO : forall n : nat, Le 0 n + | LeS : forall n m : nat, Le n m -> Le (S n) (S m). + +Parameter discr_l : forall n : nat, S n <> 0. + +Type + (fun n : nat => + match n return (n = 0 \/ n <> 0) with + | O => or_introl (0 <> 0) (refl_equal 0) + | S O => or_intror (1 = 0) (discr_l 0) + | S (S x) => or_intror (S (S x) = 0) (discr_l (S x)) + end). + +Parameter iguales : forall (n m : nat) (h : Le n m), Prop. + +Type + match LeO 0 as h in (Le n m) return Prop with + | LeO O => True + | LeS (S x) (S y) H => iguales (S x) (S y) H + | _ => False + end. + +Type + match LeO 0 as h in (Le n m) return Prop with + | LeO O => True + | LeS (S x) O H => iguales (S x) 0 H + | _ => False + end. diff --git a/test-suite/success/Cases.v b/test-suite/success/Cases.v index 499c0660..e63972ce 100644 --- a/test-suite/success/Cases.v +++ b/test-suite/success/Cases.v @@ -31,10 +31,11 @@ Type (* Interaction with coercions *) Parameter bool2nat : bool -> nat. Coercion bool2nat : bool >-> nat. -Check (fun x => match x with - | O => true - | S _ => 0 - end:nat). +Definition foo : nat -> nat := + fun x => match x with + | O => true + | S _ => 0 + end. (****************************************************************************) (* All remaining examples come from Cristina Cornes' V6 TESTS/MultCases.v *) @@ -255,7 +256,7 @@ Type match 0, 1 return nat with Type match 0, 1 with | x, y => x + y end. - + Type match 0, 1 return nat with | O, y => y | S x, y => x + y @@ -522,7 +523,7 @@ Type | O, _ => 0 | S _, _ => c end). - + (* Rows of pattern variables: some tricky cases *) Axioms (P : nat -> Prop) (f : forall n : nat, P n). @@ -612,14 +613,14 @@ Type (* Type [A:Set][n:nat][l:(Listn A n)] - <[_:nat](Listn A O)>Cases l of + <[_:nat](Listn A O)>Cases l of (Niln as b) => b | (Consn n a (Niln as b))=> (Niln A) | (Consn n a (Consn m b l)) => (Niln A) end. Type [A:Set][n:nat][l:(Listn A n)] - Cases l of + Cases l of (Niln as b) => b | (Consn n a (Niln as b))=> (Niln A) | (Consn n a (Consn m b l)) => (Niln A) @@ -627,9 +628,9 @@ Type [A:Set][n:nat][l:(Listn A n)] *) (******** This example rises an error unconstrained_variables! Type [A:Set][n:nat][l:(Listn A n)] - Cases l of + Cases l of (Niln as b) => (Consn A O O b) - | ((Consn n a Niln) as L) => L + | ((Consn n a Niln) as L) => L | (Consn n a _) => (Consn A O O (Niln A)) end. **********) @@ -956,7 +957,7 @@ Definition length3 (n : nat) (l : listn n) := | _ => 0 end. - + Type match LeO 0 return nat with | LeS n m h => n + m | x => 0 @@ -1071,10 +1072,10 @@ Type | Consn _ _ _ as b => b end). -(** Horrible error message! +(** Horrible error message! Type [A:Set][n:nat][l:(Listn A n)] - Cases l of + Cases l of (Niln as b) => b | ((Consn _ _ _ ) as b)=> b end. @@ -1179,7 +1180,7 @@ Type (fun n : nat => match test n with Parameter compare : forall n m : nat, {n < m} + {n = m} + {n > m}. Type match compare 0 0 return nat with - + (* k<i *) | inleft (left _) => 0 (* k=i *) | inleft _ => 0 (* k>i *) | inright _ => 0 @@ -1187,7 +1188,7 @@ Type Type match compare 0 0 with - + (* k<i *) | inleft (left _) => 0 (* k=i *) | inleft _ => 0 (* k>i *) | inright _ => 0 @@ -1374,7 +1375,7 @@ Type | var, var => True | oper op1 l1, oper op2 l2 => False | _, _ => False - end. + end. Reset LTERM. @@ -1660,7 +1661,7 @@ Type | Cons a x, Cons b y => V4 a x b y end). - + (* ===================================== *) Inductive Eqlong : @@ -1724,7 +1725,7 @@ Parameter -Fixpoint Eqlongdec (n : nat) (x : listn n) (m : nat) +Fixpoint Eqlongdec (n : nat) (x : listn n) (m : nat) (y : listn m) {struct x} : Eqlong n x m y \/ ~ Eqlong n x m y := match x in (listn n), y in (listn m) diff --git a/test-suite/success/CasesDep.v b/test-suite/success/CasesDep.v index 49bd77fc..29721843 100644 --- a/test-suite/success/CasesDep.v +++ b/test-suite/success/CasesDep.v @@ -38,29 +38,29 @@ Require Import Logic_Type. Section Orderings. Variable U : Type. - + Definition Relation := U -> U -> Prop. Variable R : Relation. - + Definition Reflexive : Prop := forall x : U, R x x. - + Definition Transitive : Prop := forall x y z : U, R x y -> R y z -> R x z. - + Definition Symmetric : Prop := forall x y : U, R x y -> R y x. - + Definition Antisymmetric : Prop := forall x y : U, R x y -> R y x -> x = y. - + Definition contains (R R' : Relation) : Prop := forall x y : U, R' x y -> R x y. Definition same_relation (R R' : Relation) : Prop := contains R R' /\ contains R' R. Inductive Equivalence : Prop := Build_Equivalence : Reflexive -> Transitive -> Symmetric -> Equivalence. - + Inductive PER : Prop := Build_PER : Symmetric -> Transitive -> PER. - + End Orderings. (***** Setoid *******) @@ -105,7 +105,7 @@ Definition Map_setoid := Build_Setoid Map ext Equiv_map_eq. End Maps. -Notation ap := (explicit_ap _ _). +Notation ap := (explicit_ap _ _). (* <Warning> : Grammar is replaced by Notation *) @@ -128,8 +128,8 @@ Axiom eq_Suc : forall n m : posint, n = m -> Suc n = Suc m. Definition pred (n : posint) : posint := match n return posint with - | Z => (* Z *) Z - (* Suc u *) + | Z => (* Z *) Z + (* Suc u *) | Suc u => u end. @@ -141,7 +141,7 @@ Axiom not_eq_Suc : forall n m : posint, n <> m -> Suc n <> Suc m. Definition IsSuc (n : posint) : Prop := match n return Prop with | Z => (* Z *) False - (* Suc p *) + (* Suc p *) | Suc p => True end. Definition IsZero (n : posint) : Prop := @@ -163,7 +163,7 @@ Definition Decidable (A : Type) (R : Relation A) := forall x y : A, R x y \/ ~ R x y. -Record DSetoid : Type := +Record DSetoid : Type := {Set_of : Setoid; prf_decid : Decidable (elem Set_of) (equal Set_of)}. (* example de Dsetoide d'entiers *) @@ -190,7 +190,7 @@ Definition Dposint := Build_DSetoid Set_of_posint Eq_posint_deci. Section Sig. -Record Signature : Type := +Record Signature : Type := {Sigma : DSetoid; Arity : Map (Set_of Sigma) (Set_of Dposint)}. Variable S : Signature. @@ -268,8 +268,8 @@ Reset equalT. Fixpoint equalT (t1 : TERM) : TERM -> Prop := match t1 return (TERM -> Prop) with - | var v1 => - (*var*) + | var v1 => + (*var*) fun t2 : TERM => match t2 return Prop with | var v2 => @@ -289,12 +289,12 @@ Fixpoint equalT (t1 : TERM) : TERM -> Prop := EqListT (ap (Arity S) op1) l1 (ap (Arity S) op2) l2 end end - + with EqListT (n1 : posint) (l1 : LTERM n1) {struct l1} : forall n2 : posint, LTERM n2 -> Prop := match l1 in (LTERM _) return (forall n2 : posint, LTERM n2 -> Prop) with | nil => - (*nil*) + (*nil*) fun (n2 : posint) (l2 : LTERM n2) => match l2 in (LTERM _) return Prop with | nil => @@ -336,7 +336,7 @@ Fixpoint equalT (t1 : TERM) : TERM -> Prop := EqListT (ap (Arity S) op1) l1 (ap (Arity S) op2) l2 end end - + with EqListT (n1 : posint) (l1 : LTERM n1) {struct l1} : forall n2 : posint, LTERM n2 -> Prop := match l1 return (forall n2 : posint, LTERM n2 -> Prop) with @@ -374,8 +374,8 @@ Fixpoint equalT (t1 : TERM) : TERM -> Prop := EqListT (ap (Arity S) op1) l1 (ap (Arity S) op2) l2 end end - - with EqListT (n1 : posint) (l1 : LTERM n1) (n2 : posint) + + with EqListT (n1 : posint) (l1 : LTERM n1) (n2 : posint) (l2 : LTERM n2) {struct l1} : Prop := match l1 with | nil => match l2 with @@ -401,8 +401,8 @@ Fixpoint equalT (t1 t2 : TERM) {struct t1} : Prop := equal _ op1 op2 /\ EqListT (ap (Arity S) op1) l1 (ap (Arity S) op2) l2 | _, _ => False end - - with EqListT (n1 : posint) (l1 : LTERM n1) (n2 : posint) + + with EqListT (n1 : posint) (l1 : LTERM n1) (n2 : posint) (l2 : LTERM n2) {struct l1} : Prop := match l1, l2 with | nil, nil => True @@ -433,16 +433,16 @@ Inductive I : unit -> Type := | C : forall a, I a -> I tt. (* -Definition F (l:I tt) : l = l := +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: +some kind of pattern-unification) would produce: *) -Definition F (l:I tt) : l = l := +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. @@ -451,7 +451,7 @@ Inductive J : nat -> Type := | D : forall a, J (S a) -> J a. (* -Definition G (l:J O) : l = l := +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 _ @@ -461,7 +461,7 @@ one would expect that the compilation of G (this involves inversion) would produce: *) -Definition G (l:J O) : l = l := +Definition G (l:J O) : l = l := match l return l = l with | D 0 l'' => match l'' as _l'' in J n return @@ -480,3 +480,29 @@ Fixpoint app {A} {n m} (v : listn A n) (w : listn A m) : listn A (n + m) := | niln => w | consn a n' v' => consn _ a _ (app v' w) end. + +(* Testing regression of bug 2106 *) + +Set Implicit Arguments. +Require Import List. + +Inductive nt := E. +Definition root := E. +Inductive ctor : list nt -> nt -> Type := + Plus : ctor (cons E (cons E nil)) E. + +Inductive term : nt -> Type := +| Term : forall s n, ctor s n -> spine s -> term n +with spine : list nt -> Type := +| EmptySpine : spine nil +| ConsSpine : forall n s, term n -> spine s -> spine (n :: s). + +Inductive step : nt -> nt -> Type := + | Step : forall l n r n' (c:ctor (l++n::r) n'), spine l -> spine r -> step n +n'. + +Definition test (s:step E E) := + match s with + | Step nil _ (cons E nil) _ Plus l l' => true + | _ => false + end. diff --git a/test-suite/success/Discriminate.v b/test-suite/success/Discriminate.v index b57c5478..dffad323 100644 --- a/test-suite/success/Discriminate.v +++ b/test-suite/success/Discriminate.v @@ -2,11 +2,11 @@ (* Check that Discriminate tries Intro until *) -Lemma l1 : 0 = 1 -> False. +Lemma l1 : 0 = 1 -> False. discriminate 1. Qed. -Lemma l2 : forall H : 0 = 1, H = H. +Lemma l2 : forall H : 0 = 1, H = H. discriminate H. Qed. diff --git a/test-suite/success/Equations.v b/test-suite/success/Equations.v deleted file mode 100644 index e31135c2..00000000 --- a/test-suite/success/Equations.v +++ /dev/null @@ -1,321 +0,0 @@ -Require Import Program. - -Equations neg (b : bool) : bool := -neg true := false ; -neg false := true. - -Eval compute in neg. - -Require Import Coq.Lists.List. - -Equations head A (default : A) (l : list A) : A := -head A default nil := default ; -head A default (cons a v) := a. - -Eval compute in head. - -Equations tail {A} (l : list A) : (list A) := -tail A nil := nil ; -tail A (cons a v) := v. - -Eval compute in @tail. - -Eval compute in (tail (cons 1 nil)). - -Reserved Notation " x ++ y " (at level 60, right associativity). - -Equations app' {A} (l l' : list A) : (list A) := -app' A nil l := l ; -app' A (cons a v) l := cons a (app' v l). - -Equations app (l l' : list nat) : list nat := - [] ++ l := l ; - (a :: v) ++ l := a :: (v ++ l) - -where " x ++ y " := (app x y). - -Eval compute in @app'. - -Equations zip' {A} (f : A -> A -> A) (l l' : list A) : (list A) := -zip' A f nil nil := nil ; -zip' A f (cons a v) (cons b w) := cons (f a b) (zip' f v w) ; -zip' A f nil (cons b w) := nil ; -zip' A f (cons a v) nil := nil. - - -Eval compute in @zip'. - -Equations zip'' {A} (f : A -> A -> A) (l l' : list A) (def : list A) : (list A) := -zip'' A f nil nil def := nil ; -zip'' A f (cons a v) (cons b w) def := cons (f a b) (zip'' f v w def) ; -zip'' A f nil (cons b w) def := def ; -zip'' A f (cons a v) nil def := def. - -Eval compute in @zip''. - -Inductive fin : nat -> Set := -| fz : Π{n}, fin (S n) -| fs : Π{n}, fin n -> fin (S n). - -Inductive finle : Π(n : nat) (x : fin n) (y : fin n), Prop := -| leqz : Π{n j}, finle (S n) fz j -| leqs : Π{n i j}, finle n i j -> finle (S n) (fs i) (fs j). - -Scheme finle_ind_dep := Induction for finle Sort Prop. - -Instance finle_ind_pack n x y : DependentEliminationPackage (finle n x y) := - { elim_type := _ ; elim := finle_ind_dep }. - -Implicit Arguments finle [[n]]. - -Require Import Bvector. - -Implicit Arguments Vnil [[A]]. -Implicit Arguments Vcons [[A] [n]]. - -Equations vhead {A n} (v : vector A (S n)) : A := -vhead A n (Vcons a v) := a. - -Equations vmap {A B} (f : A -> B) {n} (v : vector A n) : (vector B n) := -vmap A B f 0 Vnil := Vnil ; -vmap A B f (S n) (Vcons a v) := Vcons (f a) (vmap f v). - -Eval compute in (vmap id (@Vnil nat)). -Eval compute in (vmap id (@Vcons nat 2 _ Vnil)). -Eval compute in @vmap. - -Equations Below_nat (P : nat -> Type) (n : nat) : Type := -Below_nat P 0 := unit ; -Below_nat P (S n) := prod (P n) (Below_nat P n). - -Equations below_nat (P : nat -> Type) n (step : Π(n : nat), Below_nat P n -> P n) : Below_nat P n := -below_nat P 0 step := tt ; -below_nat P (S n) step := let rest := below_nat P n step in - (step n rest, rest). - -Class BelowPack (A : Type) := - { Below : Type ; below : Below }. - -Instance nat_BelowPack : BelowPack nat := - { Below := ΠP n step, Below_nat P n ; - below := λ P n step, below_nat P n (step P) }. - -Definition rec_nat (P : nat -> Type) n (step : Πn, Below_nat P n -> P n) : P n := - step n (below_nat P n step). - -Fixpoint Below_vector (P : ΠA n, vector A n -> Type) A n (v : vector A n) : Type := - match v with Vnil => unit | Vcons a n' v' => prod (P A n' v') (Below_vector P A n' v') end. - -Equations below_vector (P : ΠA n, vector A n -> Type) A n (v : vector A n) - (step : ΠA n (v : vector A n), Below_vector P A n v -> P A n v) : Below_vector P A n v := -below_vector P A ?(0) Vnil step := tt ; -below_vector P A ?(S n) (Vcons a v) step := - let rest := below_vector P A n v step in - (step A n v rest, rest). - -Instance vector_BelowPack : BelowPack (ΠA n, vector A n) := - { Below := ΠP A n v step, Below_vector P A n v ; - below := λ P A n v step, below_vector P A n v (step P) }. - -Instance vector_noargs_BelowPack A n : BelowPack (vector A n) := - { Below := ΠP v step, Below_vector P A n v ; - below := λ P v step, below_vector P A n v (step P) }. - -Definition rec_vector (P : ΠA n, vector A n -> Type) A n v - (step : ΠA n (v : vector A n), Below_vector P A n v -> P A n v) : P A n v := - step A n v (below_vector P A n v step). - -Class Recursor (A : Type) (BP : BelowPack A) := - { rec_type : Πx : A, Type ; rec : Πx : A, rec_type x }. - -Instance nat_Recursor : Recursor nat nat_BelowPack := - { rec_type := λ n, ΠP step, P n ; - rec := λ n P step, rec_nat P n (step P) }. - -(* Instance vect_Recursor : Recursor (ΠA n, vector A n) vector_BelowPack := *) -(* rec_type := Π(P : ΠA n, vector A n -> Type) step A n v, P A n v; *) -(* rec := λ P step A n v, rec_vector P A n v step. *) - -Instance vect_Recursor_noargs A n : Recursor (vector A n) (vector_noargs_BelowPack A n) := - { rec_type := λ v, Π(P : ΠA n, vector A n -> Type) step, P A n v; - rec := λ v P step, rec_vector P A n v step }. - -Implicit Arguments Below_vector [P A n]. - -Notation " x ~= y " := (@JMeq _ x _ y) (at level 70, no associativity). - -(** Won't pass the guardness check which diverges anyway. *) - -(* Equations trans {n} {i j k : fin n} (p : finle i j) (q : finle j k) : finle i k := *) -(* trans ?(S n) ?(fz) ?(j) ?(k) leqz q := leqz ; *) -(* trans ?(S n) ?(fs i) ?(fs j) ?(fs k) (leqs p) (leqs q) := leqs (trans p q). *) - -(* Lemma trans_eq1 n (j k : fin (S n)) (q : finle j k) : trans leqz q = leqz. *) -(* Proof. intros. simplify_equations ; reflexivity. Qed. *) - -(* Lemma trans_eq2 n i j k p q : @trans (S n) (fs i) (fs j) (fs k) (leqs p) (leqs q) = leqs (trans p q). *) -(* Proof. intros. simplify_equations ; reflexivity. Qed. *) - -Section Image. - Context {S T : Type}. - Variable f : S -> T. - - Inductive Imf : T -> Type := imf (s : S) : Imf (f s). - - Equations inv (t : T) (im : Imf t) : S := - inv (f s) (imf s) := s. - -End Image. - -Section Univ. - - Inductive univ : Set := - | ubool | unat | uarrow (from:univ) (to:univ). - - Equations interp (u : univ) : Type := - interp ubool := bool ; interp unat := nat ; - interp (uarrow from to) := interp from -> interp to. - - Equations foo (u : univ) (el : interp u) : interp u := - foo ubool true := false ; - foo ubool false := true ; - foo unat t := t ; - foo (uarrow from to) f := id ∘ f. - - Eval lazy beta delta [ foo foo_obligation_1 foo_obligation_2 ] iota zeta in foo. - -End Univ. - -Eval compute in (foo ubool false). -Eval compute in (foo (uarrow ubool ubool) negb). -Eval compute in (foo (uarrow ubool ubool) id). - -Inductive foobar : Set := bar | baz. - -Equations bla (f : foobar) : bool := -bla bar := true ; -bla baz := false. - -Eval simpl in bla. -Print refl_equal. - -Notation "'refl'" := (@refl_equal _ _). - -Equations K {A} (x : A) (P : x = x -> Type) (p : P (refl_equal x)) (p : x = x) : P p := -K A x P p refl := p. - -Equations eq_sym {A} (x y : A) (H : x = y) : y = x := -eq_sym A x x refl := refl. - -Equations eq_trans {A} (x y z : A) (p : x = y) (q : y = z) : x = z := -eq_trans A x x x refl refl := refl. - -Lemma eq_trans_eq A x : @eq_trans A x x x refl refl = refl. -Proof. reflexivity. Qed. - -Equations nth {A} {n} (v : vector A n) (f : fin n) : A := -nth A (S n) (Vcons a v) fz := a ; -nth A (S n) (Vcons a v) (fs f) := nth v f. - -Equations tabulate {A} {n} (f : fin n -> A) : vector A n := -tabulate A 0 f := Vnil ; -tabulate A (S n) f := Vcons (f fz) (tabulate (f ∘ fs)). - -Equations vlast {A} {n} (v : vector A (S n)) : A := -vlast A 0 (Vcons a Vnil) := a ; -vlast A (S n) (Vcons a (n:=S n) v) := vlast v. - -Print Assumptions vlast. - -Equations vlast' {A} {n} (v : vector A (S n)) : A := -vlast' A ?(0) (Vcons a Vnil) := a ; -vlast' A ?(S n) (Vcons a (n:=S n) v) := vlast' v. - -Lemma vlast_equation1 A (a : A) : vlast' (Vcons a Vnil) = a. -Proof. intros. simplify_equations. reflexivity. Qed. - -Lemma vlast_equation2 A n a v : @vlast' A (S n) (Vcons a v) = vlast' v. -Proof. intros. simplify_equations ; reflexivity. Qed. - -Print Assumptions vlast'. -Print Assumptions nth. -Print Assumptions tabulate. - -Extraction vlast. -Extraction vlast'. - -Equations vliat {A} {n} (v : vector A (S n)) : vector A n := -vliat A 0 (Vcons a Vnil) := Vnil ; -vliat A (S n) (Vcons a v) := Vcons a (vliat v). - -Eval compute in (vliat (Vcons 2 (Vcons 5 (Vcons 4 Vnil)))). - -Equations vapp' {A} {n m} (v : vector A n) (w : vector A m) : vector A (n + m) := -vapp' A ?(0) m Vnil w := w ; -vapp' A ?(S n) m (Vcons a v) w := Vcons a (vapp' v w). - -Eval compute in @vapp'. - -Fixpoint vapp {A n m} (v : vector A n) (w : vector A m) : vector A (n + m) := - match v with - | Vnil => w - | Vcons a n' v' => Vcons a (vapp v' w) - end. - -Lemma JMeq_Vcons_inj A n m a (x : vector A n) (y : vector A m) : n = m -> JMeq x y -> JMeq (Vcons a x) (Vcons a y). -Proof. intros until y. simplify_dep_elim. reflexivity. Qed. - -Equations NoConfusion_fin (P : Prop) {n : nat} (x y : fin n) : Prop := -NoConfusion_fin P (S n) fz fz := P -> P ; -NoConfusion_fin P (S n) fz (fs y) := P ; -NoConfusion_fin P (S n) (fs x) fz := P ; -NoConfusion_fin P (S n) (fs x) (fs y) := (x = y -> P) -> P. - -Eval compute in NoConfusion_fin. -Eval compute in NoConfusion_fin_comp. - -Print Assumptions NoConfusion_fin. - -Eval compute in (fun P n => NoConfusion_fin P (n:=S n) fz fz). - -(* Equations noConfusion_fin P (n : nat) (x y : fin n) (H : x = y) : NoConfusion_fin P x y := *) -(* noConfusion_fin P (S n) fz fz refl := λ p _, p ; *) -(* noConfusion_fin P (S n) (fs x) (fs x) refl := λ p : x = x -> P, p refl. *) - -Equations_nocomp NoConfusion_vect (P : Prop) {A n} (x y : vector A n) : Prop := -NoConfusion_vect P A 0 Vnil Vnil := P -> P ; -NoConfusion_vect P A (S n) (Vcons a x) (Vcons b y) := (a = b -> x = y -> P) -> P. - -Equations noConfusion_vect (P : Prop) A n (x y : vector A n) (H : x = y) : NoConfusion_vect P x y := -noConfusion_vect P A 0 Vnil Vnil refl := λ p, p ; -noConfusion_vect P A (S n) (Vcons a v) (Vcons a v) refl := λ p : a = a -> v = v -> P, p refl refl. - -(* Instance fin_noconf n : NoConfusionPackage (fin n) := *) -(* NoConfusion := λ P, Πx y, x = y -> NoConfusion_fin P x y ; *) -(* noConfusion := λ P x y, noConfusion_fin P n x y. *) - -Instance vect_noconf A n : NoConfusionPackage (vector A n) := - { NoConfusion := λ P, Πx y, x = y -> NoConfusion_vect P x y ; - noConfusion := λ P x y, noConfusion_vect P A n x y }. - -Equations fog {n} (f : fin n) : nat := -fog (S n) fz := 0 ; fog (S n) (fs f) := S (fog f). - -Inductive Split {X : Set}{m n : nat} : vector X (m + n) -> Set := - append : Π(xs : vector X m)(ys : vector X n), Split (vapp xs ys). - -Implicit Arguments Split [[X]]. - -Equations_nocomp split {X : Set}(m n : nat) (xs : vector X (m + n)) : Split m n xs := -split X 0 n xs := append Vnil xs ; -split X (S m) n (Vcons x xs) := - let 'append xs' ys' in Split _ _ vec := split m n xs return Split (S m) n (Vcons x vec) in - append (Vcons x xs') ys'. - -Eval compute in (split 0 1 (vapp Vnil (Vcons 2 Vnil))). -Eval compute in (split _ _ (vapp (Vcons 3 Vnil) (Vcons 2 Vnil))). - -Extraction Inline split_obligation_1 split_obligation_2. -Recursive Extraction split. - -Eval compute in @split. diff --git a/test-suite/success/Field.v b/test-suite/success/Field.v index b4c06c7b..dd82036e 100644 --- a/test-suite/success/Field.v +++ b/test-suite/success/Field.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: Field.v 9197 2006-10-02 15:55:52Z barras $ *) +(* $Id$ *) (**** Tests of Field with real numbers ****) @@ -31,7 +31,7 @@ Proof. intros. field. Abort. - + (* Example 3 *) Goal forall a b : R, 1 / (a * b) * (1 / (1 / b)) = 1 / a. Proof. @@ -44,7 +44,7 @@ Proof. intros. field_simplify_eq. Abort. - + Goal forall a b : R, 1 / (a * b) * (1 / 1 / b) = 1 / a. Proof. intros. @@ -58,21 +58,21 @@ Proof. intros. field; auto. Qed. - + (* Example 5 *) Goal forall a : R, 1 = 1 * (1 / a) * a. Proof. intros. field. Abort. - + (* Example 6 *) Goal forall a b : R, b = b * / a * a. Proof. intros. field. Abort. - + (* Example 7 *) Goal forall a b : R, b = b * (1 / a) * a. Proof. @@ -81,11 +81,17 @@ Proof. Abort. (* Example 8 *) -Goal -forall x y : R, -x * (1 / x + x / (x + y)) = -- (1 / y) * y * (- (x * (x / (x + y))) - 1). +Goal forall x y : R, + x * (1 / x + x / (x + y)) = + - (1 / y) * y * (- (x * (x / (x + y))) - 1). Proof. intros. field. Abort. + +(* Example 9 *) +Goal forall a b : R, 1 / (a * b) * (1 / 1 / b) = 1 / a -> False. +Proof. +intros. +field_simplify_eq in H. +Abort. diff --git a/test-suite/success/Fixpoint.v b/test-suite/success/Fixpoint.v index cf821073..3a4f8899 100644 --- a/test-suite/success/Fixpoint.v +++ b/test-suite/success/Fixpoint.v @@ -5,7 +5,7 @@ Inductive listn : nat -> Set := | consn : forall n:nat, nat -> listn n -> listn (S n). Fixpoint f (n:nat) (m:=pred n) (l:listn m) (p:=S n) {struct l} : nat := - match n with O => p | _ => + match n with O => p | _ => match l with niln => p | consn q _ l => f (S q) l end end. @@ -48,3 +48,46 @@ Fixpoint foldrn n bs := End folding. +(* Check definition by tactics *) + +Set Automatic Introduction. + +Inductive even : nat -> Type := + | even_O : even 0 + | even_S : forall n, odd n -> even (S n) +with odd : nat -> Type := + odd_S : forall n, even n -> odd (S n). + +Fixpoint even_div2 n (H:even n) : nat := + match H with + | even_O => 0 + | even_S n H => S (odd_div2 n H) + end +with odd_div2 n H : nat. +destruct H. +apply even_div2 with n. +assumption. +Qed. + +Fixpoint even_div2' n (H:even n) : nat with odd_div2' n (H:odd n) : nat. +destruct H. +exact 0. +apply odd_div2' with n. +assumption. +destruct H. +apply even_div2' with n. +assumption. +Qed. + +CoInductive Stream1 (A B:Type) := Cons1 : A -> Stream2 A B -> Stream1 A B +with Stream2 (A B:Type) := Cons2 : B -> Stream1 A B -> Stream2 A B. + +CoFixpoint ex1 (n:nat) (b:bool) : Stream1 nat bool +with ex2 (n:nat) (b:bool) : Stream2 nat bool. +apply Cons1. +exact n. +apply (ex2 n b). +apply Cons2. +exact b. +apply (ex1 (S n) (negb b)). +Defined. diff --git a/test-suite/success/Fourier.v b/test-suite/success/Fourier.v index 2d184fef..b63bead4 100644 --- a/test-suite/success/Fourier.v +++ b/test-suite/success/Fourier.v @@ -1,10 +1,10 @@ Require Import Rfunctions. Require Import Fourier. - + Lemma l1 : forall x y z : R, Rabs (x - z) <= Rabs (x - y) + Rabs (y - z). intros; split_Rabs; fourier. Qed. - + Lemma l2 : forall x y : R, x < Rabs y -> y < 1 -> x >= 0 -> - y <= 1 -> Rabs x <= 1. intros. diff --git a/test-suite/success/Funind.v b/test-suite/success/Funind.v index 1c3e56f2..b17adef6 100644 --- a/test-suite/success/Funind.v +++ b/test-suite/success/Funind.v @@ -6,7 +6,7 @@ Definition iszero (n : nat) : bool := end. Functional Scheme iszero_ind := Induction for iszero Sort Prop. - + Lemma toto : forall n : nat, n = 0 -> iszero n = true. intros x eg. functional induction iszero x; simpl in |- *. @@ -14,7 +14,7 @@ trivial. inversion eg. Qed. - + Function ftest (n m : nat) : nat := match n with | O => match m with @@ -30,7 +30,7 @@ intros n m. Qed. Lemma test2 : forall m n, ~ 2 = ftest n m. -Proof. +Proof. intros n m;intro H. functional inversion H ftest. Qed. @@ -45,9 +45,9 @@ Require Import Arith. Lemma test11 : forall m : nat, ftest 0 m <= 2. intros m. functional induction ftest 0 m. -auto. auto. -auto with *. +auto. +auto with *. Qed. Function lamfix (m n : nat) {struct n } : nat := @@ -92,7 +92,7 @@ Function trivfun (n : nat) : nat := end. -(* essaie de parametre variables non locaux:*) +(* essaie de parametre variables non locaux:*) Parameter varessai : nat. @@ -101,7 +101,7 @@ Lemma first_try : trivfun varessai = 0. trivial. assumption. Defined. - + Functional Scheme triv_ind := Induction for trivfun Sort Prop. @@ -134,7 +134,7 @@ Function funex (n : nat) : nat := | S r => funex r end end. - + Function nat_equal_bool (n m : nat) {struct n} : bool := match n with @@ -150,7 +150,7 @@ Function nat_equal_bool (n m : nat) {struct n} : bool := Require Export Div2. - + Functional Scheme div2_ind := Induction for div2 Sort Prop. Lemma div2_inf : forall n : nat, div2 n <= n. intros n. @@ -177,7 +177,7 @@ intros n m. functional induction nested_lam n m; simpl;auto. Qed. - + Function essai (x : nat) (p : nat * nat) {struct x} : nat := let (n, m) := (p: nat*nat) in match n with @@ -187,7 +187,7 @@ Function essai (x : nat) (p : nat * nat) {struct x} : nat := | S r => S (essai r (q, m)) end end. - + Lemma essai_essai : forall (x : nat) (p : nat * nat), let (n, m) := p in 0 < n -> 0 < essai x p. intros x p. @@ -209,30 +209,30 @@ Function plus_x_not_five'' (n m : nat) {struct n} : nat := | false => S recapp end end. - + Lemma notplusfive'' : forall x y : nat, y = 5 -> plus_x_not_five'' x y = x. intros a b. functional induction plus_x_not_five'' a b; intros hyp; simpl in |- *; auto. Qed. - + Lemma iseq_eq : forall n m : nat, n = m -> nat_equal_bool n m = true. intros n m. functional induction nat_equal_bool n m; simpl in |- *; intros hyp; auto. -rewrite <- hyp in y; simpl in y;tauto. +rewrite <- hyp in y; simpl in y;tauto. inversion hyp. Qed. - + Lemma iseq_eq' : forall n m : nat, nat_equal_bool n m = true -> n = m. intros n m. functional induction nat_equal_bool n m; simpl in |- *; intros eg; auto. inversion eg. inversion eg. Qed. - - + + Inductive istrue : bool -> Prop := istrue0 : istrue true. - + Functional Scheme plus_ind := Induction for plus Sort Prop. Lemma inf_x_plusxy' : forall x y : nat, x <= x + y. @@ -242,7 +242,7 @@ auto with arith. auto with arith. Qed. - + Lemma inf_x_plusxy'' : forall x : nat, x <= x + 0. intros n. unfold plus in |- *. @@ -251,7 +251,7 @@ auto with arith. apply le_n_S. assumption. Qed. - + Lemma inf_x_plusxy''' : forall x : nat, x <= 0 + x. intros n. functional induction plus 0 n; intros; auto with arith. @@ -263,25 +263,25 @@ Function mod2 (n : nat) : nat := | S (S m) => S (mod2 m) | _ => 0 end. - + Lemma princ_mod2 : forall n : nat, mod2 n <= n. intros n. functional induction mod2 n; simpl in |- *; auto with arith. Qed. - + Function isfour (n : nat) : bool := match n with | S (S (S (S O))) => true | _ => false end. - + Function isononeorfour (n : nat) : bool := match n with | S O => true | S (S (S (S O))) => true | _ => false end. - + Lemma toto'' : forall n : nat, istrue (isfour n) -> istrue (isononeorfour n). intros n. functional induction isononeorfour n; intros istr; simpl in |- *; @@ -294,14 +294,14 @@ destruct n. inversion istr. destruct n. tauto. simpl in *. inversion H0. Qed. - + Lemma toto' : forall n m : nat, n = 4 -> istrue (isononeorfour n). intros n. functional induction isononeorfour n; intros m istr; inversion istr. apply istrue0. rewrite H in y; simpl in y;tauto. Qed. - + Function ftest4 (n m : nat) : nat := match n with | O => match m with @@ -313,12 +313,12 @@ Function ftest4 (n m : nat) : nat := | S r => 1 end end. - + Lemma test4 : forall n m : nat, ftest n m <= 2. intros n m. functional induction ftest n m; auto with arith. Qed. - + Lemma test4' : forall n m : nat, ftest4 (S n) m <= 2. intros n m. assert ({n0 | n0 = S n}). @@ -332,7 +332,7 @@ inversion 1. auto with arith. auto with arith. Qed. - + Function ftest44 (x : nat * nat) (n m : nat) : nat := let (p, q) := (x: nat*nat) in match n with @@ -345,7 +345,7 @@ Function ftest44 (x : nat * nat) (n m : nat) : nat := | S r => 1 end end. - + Lemma test44 : forall (pq : nat * nat) (n m o r s : nat), ftest44 pq n (S m) <= 2. intros pq n m o r s. @@ -355,7 +355,7 @@ auto with arith. auto with arith. auto with arith. Qed. - + Function ftest2 (n m : nat) {struct n} : nat := match n with | O => match m with @@ -364,12 +364,12 @@ Function ftest2 (n m : nat) {struct n} : nat := end | S p => ftest2 p m end. - + Lemma test2' : forall n m : nat, ftest2 n m <= 2. intros n m. functional induction ftest2 n m; simpl in |- *; intros; auto. Qed. - + Function ftest3 (n m : nat) {struct n} : nat := match n with | O => 0 @@ -378,7 +378,7 @@ Function ftest3 (n m : nat) {struct n} : nat := | S r => 0 end end. - + Lemma test3' : forall n m : nat, ftest3 n m <= 2. intros n m. functional induction ftest3 n m. @@ -390,7 +390,7 @@ intros. simpl in |- *. auto. Qed. - + Function ftest5 (n m : nat) {struct n} : nat := match n with | O => 0 @@ -399,7 +399,7 @@ Function ftest5 (n m : nat) {struct n} : nat := | S r => ftest5 p r end end. - + Lemma test5 : forall n m : nat, ftest5 n m <= 2. intros n m. functional induction ftest5 n m. @@ -411,21 +411,21 @@ intros. simpl in |- *. auto. Qed. - + Function ftest7 (n : nat) : nat := match ftest5 n 0 with | O => 0 | S r => 0 end. - + Lemma essai7 : forall (Hrec : forall n : nat, ftest5 n 0 = 0 -> ftest7 n <= 2) - (Hrec0 : forall n r : nat, ftest5 n 0 = S r -> ftest7 n <= 2) + (Hrec0 : forall n r : nat, ftest5 n 0 = S r -> ftest7 n <= 2) (n : nat), ftest7 n <= 2. intros hyp1 hyp2 n. functional induction ftest7 n; auto. Qed. - + Function ftest6 (n m : nat) {struct n} : nat := match n with | O => 0 @@ -435,7 +435,7 @@ Function ftest6 (n m : nat) {struct n} : nat := end end. - + Lemma princ6 : (forall n m : nat, n = 0 -> ftest6 0 m <= 2) -> (forall n m p : nat, @@ -448,16 +448,16 @@ generalize hyp1 hyp2 hyp3. clear hyp1 hyp2 hyp3. functional induction ftest6 n m; auto. Qed. - + Lemma essai6 : forall n m : nat, ftest6 n m <= 2. intros n m. functional induction ftest6 n m; simpl in |- *; auto. Qed. -(* Some tests with modules *) +(* Some tests with modules *) Module M. -Function test_m (n:nat) : nat := - match n with +Function test_m (n:nat) : nat := + match n with | 0 => 0 | S n => S (S (test_m n)) end. @@ -470,14 +470,14 @@ reflexivity. simpl;rewrite IHn0;reflexivity. Qed. End M. -(* We redefine a new Function with the same name *) -Function test_m (n:nat) : nat := +(* We redefine a new Function with the same name *) +Function test_m (n:nat) : nat := pred n. Lemma test_m_is_pred : forall n, test_m n = pred n. -Proof. +Proof. intro n. -functional induction (test_m n). (* the test_m_ind to use is the last defined saying that test_m = pred*) +functional induction (test_m n). (* the test_m_ind to use is the last defined saying that test_m = pred*) reflexivity. Qed. diff --git a/test-suite/success/Generalization.v b/test-suite/success/Generalization.v index 6b503e95..de34e007 100644 --- a/test-suite/success/Generalization.v +++ b/test-suite/success/Generalization.v @@ -1,3 +1,4 @@ +Generalizable All Variables. Check `(a = 0). Check `(a = 0)%type. diff --git a/test-suite/success/Hints.v b/test-suite/success/Hints.v index e1c74048..4aa00e68 100644 --- a/test-suite/success/Hints.v +++ b/test-suite/success/Hints.v @@ -23,11 +23,11 @@ Hint Destruct h8 := 4 Hypothesis (_ <= _) => fun H => apply H. (* Checks that local names are accepted *) Section A. - Remark Refl : forall (A : Set) (x : A), x = x. - Proof refl_equal. + Remark Refl : forall (A : Set) (x : A), x = x. + Proof. exact refl_equal. Defined. Definition Sym := sym_equal. Let Trans := trans_equal. - + Hint Resolve Refl: foo. Hint Resolve Sym: bar. Hint Resolve Trans: foo2. @@ -46,3 +46,24 @@ Section A. End A. +Axiom a : forall n, n=0 <-> n<=0. + +Hint Resolve -> a. +Goal forall n, n=0 -> n<=0. +auto. +Qed. + + +(* This example comes from Chlipala's ltamer *) +(* It used to fail from r12902 to r13112 since type_of started to call *) +(* e_cumul (instead of conv_leq) which was not able to unify "?id" and *) +(* "(fun x => x) ?id" *) + +Notation "e :? pf" := (eq_rect _ (fun X : Set => X) e _ pf) + (no associativity, at level 90). + +Axiom cast_coalesce : + forall (T1 T2 T3 : Set) (e : T1) (pf1 : T1 = T2) (pf2 : T2 = T3), + ((e :? pf1) :? pf2) = (e :? trans_eq pf1 pf2). + +Hint Rewrite cast_coalesce : ltamer. diff --git a/test-suite/success/Import.v b/test-suite/success/Import.v new file mode 100644 index 00000000..ff5c1ed7 --- /dev/null +++ b/test-suite/success/Import.v @@ -0,0 +1,11 @@ +(* Test visibility of imported objects *) + +Require Import make_local. + +(* Check local implicit arguments are not imported *) + +Check (f nat 0). + +(* Check local arguments scopes are not imported *) + +Check (f nat (0*0)). diff --git a/test-suite/success/Inductive.v b/test-suite/success/Inductive.v index 1adcbd39..203fbbb7 100644 --- a/test-suite/success/Inductive.v +++ b/test-suite/success/Inductive.v @@ -1,4 +1,32 @@ -(* Check local definitions in context of inductive types *) +(* Test des definitions inductives imbriquees *) + +Require Import List. + +Inductive X : Set := + cons1 : list X -> X. + +Inductive Y : Set := + cons2 : list (Y * Y) -> Y. + +(* Test inductive types with local definitions (arity) *) + +Inductive eq1 : forall A:Type, let B:=A in A -> Prop := + refl1 : eq1 True I. + +Check + fun (P : forall A : Type, let B := A in A -> Type) (f : P True I) (A : Type) => + let B := A in + fun (a : A) (e : eq1 A a) => + match e in (eq1 A0 B0 a0) return (P A0 a0) with + | refl1 => f + end. + +Inductive eq2 (A:Type) (a:A) + : forall B C:Type, let D:=(A*B*C)%type in D -> Prop := + refl2 : eq2 A a unit bool (a,tt,true). + +(* Check inductive types with local definitions (parameters) *) + Inductive A (C D : Prop) (E:=C) (F:=D) (x y : E -> F) : E -> Set := I : forall z : E, A C D x y z. @@ -7,9 +35,9 @@ Check let E := C in let F := D in fun (x y : E -> F) (P : forall c : C, A C D x y c -> Type) - (f : forall z : C, P z (I C D x y z)) (y0 : C) + (f : forall z : C, P z (I C D x y z)) (y0 : C) (a : A C D x y y0) => - match a as a0 in (A _ _ _ _ y1) return (P y1 a0) with + match a as a0 in (A _ _ _ _ _ _ y1) return (P y1 a0) with | I x0 => f x0 end). @@ -20,7 +48,7 @@ Check let E := C in let F := D in fun (x y : E -> F) (P : B C D x y -> Type) - (f : forall p0 q0 : C, P (Build_B C D x y p0 q0)) + (f : forall p0 q0 : C, P (Build_B C D x y p0 q0)) (b : B C D x y) => match b as b0 return (P b0) with | Build_B x0 x1 => f x0 x1 diff --git a/test-suite/success/Injection.v b/test-suite/success/Injection.v index 867d7374..c5cd7380 100644 --- a/test-suite/success/Injection.v +++ b/test-suite/success/Injection.v @@ -17,7 +17,7 @@ Qed. Lemma l3 : forall x y : nat, existS (fun n : nat => {n = n} + {n = n}) x (left _ (refl_equal x)) = - existS (fun n : nat => {n = n} + {n = n}) y (left _ (refl_equal y)) -> + existS (fun n : nat => {n = n} + {n = n}) y (left _ (refl_equal y)) -> x = y. intros x y H. injection H. diff --git a/test-suite/success/Inversion.v b/test-suite/success/Inversion.v index b08ffcc3..5091b44c 100644 --- a/test-suite/success/Inversion.v +++ b/test-suite/success/Inversion.v @@ -5,13 +5,13 @@ Fixpoint T (n : nat) : Type := match n with | O => nat -> Prop | S n' => T n' - end. + end. Inductive R : forall n : nat, T n -> nat -> Prop := | RO : forall (Psi : T 0) (l : nat), Psi l -> R 0 Psi l | RS : - forall (n : nat) (Psi : T (S n)) (l : nat), R n Psi l -> R (S n) Psi l. -Definition Psi00 (n : nat) : Prop := False. -Definition Psi0 : T 0 := Psi00. + forall (n : nat) (Psi : T (S n)) (l : nat), R n Psi l -> R (S n) Psi l. +Definition Psi00 (n : nat) : Prop := False. +Definition Psi0 : T 0 := Psi00. Lemma Inversion_RO : forall l : nat, R 0 Psi0 l -> Psi00 l. inversion 1. Abort. @@ -39,14 +39,14 @@ extension I -> Type := | super_add : forall r (e' : extension I), in_extension r e -> - super_extension e e' -> super_extension e (add_rule r e'). + super_extension e e' -> super_extension e (add_rule r e'). Lemma super_def : forall (I : Set) (e1 e2 : extension I), super_extension e2 e1 -> forall ru, in_extension ru e1 -> in_extension ru e2. -Proof. +Proof. simple induction 1. inversion 1; auto. elim magic. @@ -105,5 +105,27 @@ Abort. Inductive foo2 : option nat -> Prop := Foo : forall t, foo2 (Some t). Goal forall o, foo2 o -> 0 = 1. intros. -eapply trans_eq. +eapply trans_eq. inversion H. + +(* Check that the part of "injection" that is called by "inversion" + does the same number of intros as the number of equations + introduced, even in presence of dependent equalities that + "injection" renounces to split *) + +Fixpoint prodn (n : nat) := + match n with + | O => unit + | (S m) => prod (prodn m) nat + end. + +Inductive U : forall n : nat, prodn n -> bool -> Prop := +| U_intro : U 0 tt true. + +Lemma foo3 : forall n (t : prodn n), U n t true -> False. +Proof. +(* used to fail because dEqThen thought there were 2 new equations but + inject_at_positions actually introduced only one; leading then to + an inconsistent state that disturbed "inversion" *) +intros. inversion H. +Abort. diff --git a/test-suite/success/LegacyField.v b/test-suite/success/LegacyField.v index d53e4010..fada3bd5 100644 --- a/test-suite/success/LegacyField.v +++ b/test-suite/success/LegacyField.v @@ -30,14 +30,14 @@ Proof. intros. legacy field. Abort. - + (* Example 3 *) Goal forall a b : R, (1 / (a * b) * (1 / 1 / b))%R = (1 / a)%R. Proof. intros. legacy field. Abort. - + (* Example 4 *) Goal forall a b : R, a <> 0%R -> b <> 0%R -> (1 / (a * b) / 1 / b)%R = (1 / a)%R. @@ -45,21 +45,21 @@ Proof. intros. legacy field. Abort. - + (* Example 5 *) Goal forall a : R, 1%R = (1 * (1 / a) * a)%R. Proof. intros. legacy field. Abort. - + (* Example 6 *) Goal forall a b : R, b = (b * / a * a)%R. Proof. intros. legacy field. Abort. - + (* Example 7 *) Goal forall a b : R, b = (b * (1 / a) * a)%R. Proof. diff --git a/test-suite/success/LetPat.v b/test-suite/success/LetPat.v index 545b8aeb..4c790680 100644 --- a/test-suite/success/LetPat.v +++ b/test-suite/success/LetPat.v @@ -13,16 +13,16 @@ 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) := +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) := +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) := +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) := +Definition l8 A (B : A -> Type) (t : sigT B) : B (projT1 t) := match t with existT x y => y end. @@ -47,9 +47,9 @@ 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 := +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 f g => fun x => g (f x). diff --git a/test-suite/success/Notations.v b/test-suite/success/Notations.v index 4bdd579a..661a8757 100644 --- a/test-suite/success/Notations.v +++ b/test-suite/success/Notations.v @@ -14,7 +14,7 @@ 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 +(* Check that first non empty definition at an empty level can be of any associativity *) Definition marker := O. @@ -30,4 +30,32 @@ Notation "' 'C_' G ( A )" := (A,G) (at level 8, G at level 2). (* Check import of notations from within a section *) Notation "+1 x" := (S x) (at level 25, x at level 9). -Section A. Global Notation "'Z'" := O (at level 9). End A. +Section A. Require Import make_notation. End A. + +(* Check use of "$" (see bug #1961) *) + +Notation "$ x" := (id x) (at level 30). +Check ($ 5). + +(* Check regression of bug #2087 *) + +Notation "'exists' x , P" := (x, P) + (at level 200, x ident, right associativity, only parsing). + +Definition foo P := let '(exists x, Q) := P in x = Q :> nat. + +(* Check empty levels when extending binder_constr *) + +Notation "'exists' x >= y , P" := (exists x, x >= y /\ P)%nat + (at level 200, x ident, right associativity, y at level 69). + +(* This used to loop at some time before r12491 *) + +Notation R x := (@pair _ _ x). +Check (fun x:nat*nat => match x with R x y => (x,y) end). + +(* Check multi-tokens recursive notations *) + +Local Notation "[ a # ; .. # ; b ]" := (a + .. (b + 0) ..). +Check [ 0 ]. +Check [ 0 # ; 1 ]. diff --git a/test-suite/success/Nsatz.v b/test-suite/success/Nsatz.v new file mode 100644 index 00000000..fde9f470 --- /dev/null +++ b/test-suite/success/Nsatz.v @@ -0,0 +1,216 @@ +Require Import NsatzR ZArith Reals List Ring_polynom. + +Section Examples. + +Delimit Scope PE_scope with PE. +Infix "+" := PEadd : PE_scope. +Infix "*" := PEmul : PE_scope. +Infix "-" := PEsub : PE_scope. +Infix "^" := PEpow : PE_scope. +Notation "[ n ]" := (@PEc Z n) (at level 0). + +Open Scope R_scope. + +Lemma example1 : forall x y, + x+y=0 -> + x*y=0 -> + x^2=0. +Proof. + nsatzR. +Qed. + +Lemma example2 : forall x, x^2=0 -> x=0. +Proof. + nsatzR. +Qed. + +(* +Notation X := (PEX Z 3). +Notation Y := (PEX Z 2). +Notation Z_ := (PEX Z 1). +*) +Lemma example3 : forall x y z, + x+y+z=0 -> + x*y+x*z+y*z=0-> + x*y*z=0 -> x^3=0. +Proof. +Time nsatzR. +Qed. + +(* +Notation X := (PEX Z 4). +Notation Y := (PEX Z 3). +Notation Z_ := (PEX Z 2). +Notation U := (PEX Z 1). +*) +Lemma example4 : forall x y z u, + x+y+z+u=0 -> + x*y+x*z+x*u+y*z+y*u+z*u=0-> + x*y*z+x*y*u+x*z*u+y*z*u=0-> + x*y*z*u=0 -> x^4=0. +Proof. +Time nsatzR. +Qed. + +(* +Notation x_ := (PEX Z 5). +Notation y_ := (PEX Z 4). +Notation z_ := (PEX Z 3). +Notation u_ := (PEX Z 2). +Notation v_ := (PEX Z 1). +Notation "x :: y" := (List.cons x y) +(at level 60, right associativity, format "'[hv' x :: '/' y ']'"). +Notation "x :: y" := (List.app x y) +(at level 60, right associativity, format "x :: y"). +*) + +Lemma example5 : forall x y z u v, + x+y+z+u+v=0 -> + x*y+x*z+x*u+x*v+y*z+y*u+y*v+z*u+z*v+u*v=0-> + x*y*z+x*y*u+x*y*v+x*z*u+x*z*v+x*u*v+y*z*u+y*z*v+y*u*v+z*u*v=0-> + x*y*z*u+y*z*u*v+z*u*v*x+u*v*x*y+v*x*y*z=0 -> + x*y*z*u*v=0 -> x^5=0. +Proof. +Time nsatzR. +Qed. + +End Examples. + +Section Geometry. +Require Export Reals NsatzR. +Open Scope R_scope. + +Record point:Type:={ + X:R; + Y:R}. + +Definition collinear(A B C:point):= + (X A - X B)*(Y C - Y B)-(Y A - Y B)*(X C - X B)=0. + +Definition parallel (A B C D:point):= + ((X A)-(X B))*((Y C)-(Y D))=((Y A)-(Y B))*((X C)-(X D)). + +Definition notparallel (A B C D:point)(x:R):= + x*(((X A)-(X B))*((Y C)-(Y D))-((Y A)-(Y B))*((X C)-(X D)))=1. + +Definition orthogonal (A B C D:point):= + ((X A)-(X B))*((X C)-(X D))+((Y A)-(Y B))*((Y C)-(Y D))=0. + +Definition equal2(A B:point):= + (X A)=(X B) /\ (Y A)=(Y B). + +Definition equal3(A B:point):= + ((X A)-(X B))^2+((Y A)-(Y B))^2 = 0. + +Definition nequal2(A B:point):= + (X A)<>(X B) \/ (Y A)<>(Y B). + +Definition nequal3(A B:point):= + not (((X A)-(X B))^2+((Y A)-(Y B))^2 = 0). + +Definition middle(A B I:point):= + 2*(X I)=(X A)+(X B) /\ 2*(Y I)=(Y A)+(Y B). + +Definition distance2(A B:point):= + (X B - X A)^2 + (Y B - Y A)^2. + +(* AB = CD *) +Definition samedistance2(A B C D:point):= + (X B - X A)^2 + (Y B - Y A)^2 = (X D - X C)^2 + (Y D - Y C)^2. +Definition determinant(A O B:point):= + (X A - X O)*(Y B - Y O) - (Y A - Y O)*(X B - X O). +Definition scalarproduct(A O B:point):= + (X A - X O)*(X B - X O) + (Y A - Y O)*(Y B - Y O). +Definition norm2(A O B:point):= + ((X A - X O)^2+(Y A - Y O)^2)*((X B - X O)^2+(Y B - Y O)^2). + + +Lemma a1:forall A B C:Prop, ((A\/B)/\(A\/C)) -> (A\/(B/\C)). +intuition. +Qed. + +Lemma a2:forall A B C:Prop, ((A\/C)/\(B\/C)) -> ((A/\B)\/C). +intuition. +Qed. + +Lemma a3:forall a b c d:R, (a-b)*(c-d)=0 -> (a=b \/ c=d). +intros. +assert ( (a-b = 0) \/ (c-d = 0)). +apply Rmult_integral. +trivial. +destruct H0. +left; nsatz. +right; nsatz. +Qed. + +Ltac geo_unfold := + unfold collinear; unfold parallel; unfold notparallel; unfold orthogonal; + unfold equal2; unfold equal3; unfold nequal2; unfold nequal3; + unfold middle; unfold samedistance2; + unfold determinant; unfold scalarproduct; unfold norm2; unfold distance2. + +Ltac geo_end := + repeat ( + repeat (match goal with h:_/\_ |- _ => decompose [and] h; clear h end); + repeat (apply a1 || apply a2 || apply a3); + repeat split). + +Ltac geo_rewrite_hyps:= + repeat (match goal with + | h:X _ = _ |- _ => rewrite h in *; clear h + | h:Y _ = _ |- _ => rewrite h in *; clear h + end). + +Ltac geo_begin:= + geo_unfold; + intros; + geo_rewrite_hyps; + geo_end. + +(* Examples *) + +Lemma Thales: forall O A B C D:point, + collinear O A C -> collinear O B D -> + parallel A B C D -> + (distance2 O B * distance2 O C = distance2 O D * distance2 O A + /\ distance2 O B * distance2 C D = distance2 O D * distance2 A B) + \/ collinear O A B. +repeat geo_begin. +(* +Time nsatz. +*) +Time nsatz without sugar. +(* +Time nsatz with lexico sugar. +Time nsatz with lexico. +*) +(* +Time nsatzRpv 1%N 1%Z (@nil R) (@nil R). (* revlex, sugar, no div *) +(*Finished transaction in 1. secs (0.479927u,0.s)*) +Time nsatzRpv 1%N 0%Z (@nil R) (@nil R). (* revlex, no sugar, no div *) +(*Finished transaction in 0. secs (0.543917u,0.s)*) +Time nsatzRpv 1%N 2%Z (@nil R) (@nil R). (* lex, no sugar, no div *) +(*Finished transaction in 0. secs (0.586911u,0.s)*) +Time nsatzRpv 1%N 3%Z (@nil R) (@nil R). (* lex, sugar, no div *) +(*Finished transaction in 0. secs (0.481927u,0.s)*) +Time nsatzRpv 1%N 5%Z (@nil R) (@nil R). (* revlex, sugar, div *) +(*Finished transaction in 1. secs (0.601909u,0.s)*) +*) +Time nsatz. +Qed. + +Lemma hauteurs:forall A B C A1 B1 C1 H:point, + collinear B C A1 -> orthogonal A A1 B C -> + collinear A C B1 -> orthogonal B B1 A C -> + collinear A B C1 -> orthogonal C C1 A B -> + collinear A A1 H -> collinear B B1 H -> + + collinear C C1 H + \/ collinear A B C. + +geo_begin. +Time nsatz. +(*Finished transaction in 3. secs (2.43263u,0.010998s)*) +Qed. + +End Geometry. diff --git a/test-suite/success/Nsatz_domain.v b/test-suite/success/Nsatz_domain.v new file mode 100644 index 00000000..8a30b47f --- /dev/null +++ b/test-suite/success/Nsatz_domain.v @@ -0,0 +1,274 @@ +Require Import Nsatz_domain ZArith Reals List Ring_polynom. + +Variable A: Type. +Variable Ad: Domain A. + +Add Ring Ar1: (@ring_ring A (@domain_ring _ Ad)). + +Instance Ari : Ring A := { + ring0 := @ring0 A (@domain_ring _ Ad); + ring1 := @ring1 A (@domain_ring _ Ad); + ring_plus := @ring_plus A (@domain_ring _ Ad); + ring_mult := @ring_mult A (@domain_ring _ Ad); + ring_sub := @ring_sub A (@domain_ring _ Ad); + ring_opp := @ring_opp A (@domain_ring _ Ad); + ring_ring := @ring_ring A (@domain_ring _ Ad)}. + +Instance Adi : Domain A := { + domain_ring := Ari; + domain_axiom_product := @domain_axiom_product A Ad; + domain_axiom_one_zero := @domain_axiom_one_zero A Ad}. + +Instance zero_ring2 : Zero A := {zero := ring0}. +Instance one_ring2 : One A := {one := ring1}. +Instance addition_ring2 : Addition A := {addition x y := ring_plus x y}. +Instance multiplication_ring2 : Multiplication A := {multiplication x y := ring_mult x y}. +Instance subtraction_ring2 : Subtraction A := {subtraction x y := ring_sub x y}. +Instance opposite_ring2 : Opposite A := {opposite x := ring_opp x}. + +Goal forall x y:A, x = y -> x+0 = y*1+0. +nsatz_domain. +Qed. + +Goal forall a b c:A, a = b -> b = c -> c = a. +nsatz_domain. +Qed. + +Goal forall a b c:A, a = b -> b = c -> a = c. +nsatz_domain. +Qed. + +Goal forall a b c x:A, a = b -> b = c -> a*a = c*c. +nsatz_domain. +Qed. + +Goal forall x y:Z, x = y -> (x+0)%Z = (y*1+0)%Z. +nsatz_domainZ. +Qed. + +Goal forall x y:R, x = y -> (x+0)%R = (y*1+0)%R. +nsatz_domainR. +Qed. + +Goal forall a b c x:R, a = b -> b = c -> (a*a)%R = (c*c)%R. +nsatz_domainR. +Qed. + +Section Examples. + +Delimit Scope PE_scope with PE. +Infix "+" := PEadd : PE_scope. +Infix "*" := PEmul : PE_scope. +Infix "-" := PEsub : PE_scope. +Infix "^" := PEpow : PE_scope. +Notation "[ n ]" := (@PEc Z n) (at level 0). + +Open Scope R_scope. + +Lemma example1 : forall x y, + x+y=0 -> + x*y=0 -> + x^2=0. +Proof. + nsatz_domainR. +Qed. + +Lemma example2 : forall x, x^2=0 -> x=0. +Proof. + nsatz_domainR. +Qed. + +(* +Notation X := (PEX Z 3). +Notation Y := (PEX Z 2). +Notation Z_ := (PEX Z 1). +*) +Lemma example3 : forall x y z, + x+y+z=0 -> + x*y+x*z+y*z=0-> + x*y*z=0 -> x^3=0. +Proof. +Time nsatz_domainR. +simpl. +discrR. +Qed. + +(* +Notation X := (PEX Z 4). +Notation Y := (PEX Z 3). +Notation Z_ := (PEX Z 2). +Notation U := (PEX Z 1). +*) +Lemma example4 : forall x y z u, + x+y+z+u=0 -> + x*y+x*z+x*u+y*z+y*u+z*u=0-> + x*y*z+x*y*u+x*z*u+y*z*u=0-> + x*y*z*u=0 -> x^4=0. +Proof. +Time nsatz_domainR. +Qed. + +(* +Notation x_ := (PEX Z 5). +Notation y_ := (PEX Z 4). +Notation z_ := (PEX Z 3). +Notation u_ := (PEX Z 2). +Notation v_ := (PEX Z 1). +Notation "x :: y" := (List.cons x y) +(at level 60, right associativity, format "'[hv' x :: '/' y ']'"). +Notation "x :: y" := (List.app x y) +(at level 60, right associativity, format "x :: y"). +*) + +Lemma example5 : forall x y z u v, + x+y+z+u+v=0 -> + x*y+x*z+x*u+x*v+y*z+y*u+y*v+z*u+z*v+u*v=0-> + x*y*z+x*y*u+x*y*v+x*z*u+x*z*v+x*u*v+y*z*u+y*z*v+y*u*v+z*u*v=0-> + x*y*z*u+y*z*u*v+z*u*v*x+u*v*x*y+v*x*y*z=0 -> + x*y*z*u*v=0 -> x^5=0. +Proof. +Time nsatz_domainR. +Qed. + +End Examples. + +Section Geometry. + +Open Scope R_scope. + +Record point:Type:={ + X:R; + Y:R}. + +Definition collinear(A B C:point):= + (X A - X B)*(Y C - Y B)-(Y A - Y B)*(X C - X B)=0. + +Definition parallel (A B C D:point):= + ((X A)-(X B))*((Y C)-(Y D))=((Y A)-(Y B))*((X C)-(X D)). + +Definition notparallel (A B C D:point)(x:R):= + x*(((X A)-(X B))*((Y C)-(Y D))-((Y A)-(Y B))*((X C)-(X D)))=1. + +Definition orthogonal (A B C D:point):= + ((X A)-(X B))*((X C)-(X D))+((Y A)-(Y B))*((Y C)-(Y D))=0. + +Definition equal2(A B:point):= + (X A)=(X B) /\ (Y A)=(Y B). + +Definition equal3(A B:point):= + ((X A)-(X B))^2+((Y A)-(Y B))^2 = 0. + +Definition nequal2(A B:point):= + (X A)<>(X B) \/ (Y A)<>(Y B). + +Definition nequal3(A B:point):= + not (((X A)-(X B))^2+((Y A)-(Y B))^2 = 0). + +Definition middle(A B I:point):= + 2*(X I)=(X A)+(X B) /\ 2*(Y I)=(Y A)+(Y B). + +Definition distance2(A B:point):= + (X B - X A)^2 + (Y B - Y A)^2. + +(* AB = CD *) +Definition samedistance2(A B C D:point):= + (X B - X A)^2 + (Y B - Y A)^2 = (X D - X C)^2 + (Y D - Y C)^2. +Definition determinant(A O B:point):= + (X A - X O)*(Y B - Y O) - (Y A - Y O)*(X B - X O). +Definition scalarproduct(A O B:point):= + (X A - X O)*(X B - X O) + (Y A - Y O)*(Y B - Y O). +Definition norm2(A O B:point):= + ((X A - X O)^2+(Y A - Y O)^2)*((X B - X O)^2+(Y B - Y O)^2). + + +Lemma a1:forall A B C:Prop, ((A\/B)/\(A\/C)) -> (A\/(B/\C)). +intuition. +Qed. + +Lemma a2:forall A B C:Prop, ((A\/C)/\(B\/C)) -> ((A/\B)\/C). +intuition. +Qed. + +Lemma a3:forall a b c d:R, (a-b)*(c-d)=0 -> (a=b \/ c=d). +intros. +assert ( (a-b = 0) \/ (c-d = 0)). +apply Rmult_integral. +trivial. +destruct H0. +left; nsatz_domainR. +right; nsatz_domainR. +Qed. + +Ltac geo_unfold := + unfold collinear; unfold parallel; unfold notparallel; unfold orthogonal; + unfold equal2; unfold equal3; unfold nequal2; unfold nequal3; + unfold middle; unfold samedistance2; + unfold determinant; unfold scalarproduct; unfold norm2; unfold distance2. + +Ltac geo_end := + repeat ( + repeat (match goal with h:_/\_ |- _ => decompose [and] h; clear h end); + repeat (apply a1 || apply a2 || apply a3); + repeat split). + +Ltac geo_rewrite_hyps:= + repeat (match goal with + | h:X _ = _ |- _ => rewrite h in *; clear h + | h:Y _ = _ |- _ => rewrite h in *; clear h + end). + +Ltac geo_begin:= + geo_unfold; + intros; + geo_rewrite_hyps; + geo_end. + +(* Examples *) + +Lemma Thales: forall O A B C D:point, + collinear O A C -> collinear O B D -> + parallel A B C D -> + (distance2 O B * distance2 O C = distance2 O D * distance2 O A + /\ distance2 O B * distance2 C D = distance2 O D * distance2 A B) + \/ collinear O A B. +repeat geo_begin. + +Time nsatz_domainR. +simpl;discrR. +Time nsatz_domainR. +simpl;discrR. +Qed. + +Require Import NsatzR. + +Lemma hauteurs:forall A B C A1 B1 C1 H:point, + collinear B C A1 -> orthogonal A A1 B C -> + collinear A C B1 -> orthogonal B B1 A C -> + collinear A B C1 -> orthogonal C C1 A B -> + collinear A A1 H -> collinear B B1 H -> + + collinear C C1 H + \/ collinear A B C. + +geo_begin. +(* Time nsatzRpv 2%N 1%Z (@nil R) (@nil R).*) +(*Finished transaction in 3. secs (2.363641u,0.s)*) +(*Time nsatz_domainR. trop long! *) +(* en fait nsatz_domain ne tient pas encore compte de la liste des variables! ;-) *) +Time + let lv := constr:(Y A1 + :: X A1 + :: Y B1 + :: X B1 + :: Y A0 + :: Y B + :: X B + :: X A0 + :: X H + :: Y C + :: Y C1 :: Y H :: X C1 :: X C ::nil) in + nsatz_domainpv 2%N 1%Z (@List.nil R) lv ltac:simplR Rdi. +(* Finished transaction in 6. secs (5.579152u,0.001s) *) +Qed. + +End Geometry. diff --git a/test-suite/success/Omega0.v b/test-suite/success/Omega0.v index accaec41..b8f8660e 100644 --- a/test-suite/success/Omega0.v +++ b/test-suite/success/Omega0.v @@ -3,24 +3,24 @@ Open Scope Z_scope. (* Pierre L: examples gathered while debugging romega. *) -Lemma test_romega_0 : - forall m m', +Lemma test_romega_0 : + forall m m', 0<= m <= 1 -> 0<= m' <= 1 -> (0 < m <-> 0 < m') -> m = m'. Proof. intros. omega. Qed. -Lemma test_romega_0b : - forall m m', +Lemma test_romega_0b : + forall m m', 0<= m <= 1 -> 0<= m' <= 1 -> (0 < m <-> 0 < m') -> m = m'. Proof. intros m m'. omega. Qed. -Lemma test_romega_1 : - forall (z z1 z2 : Z), +Lemma test_romega_1 : + forall (z z1 z2 : Z), z2 <= z1 -> z1 <= z2 -> z1 >= 0 -> @@ -32,8 +32,8 @@ intros. omega. Qed. -Lemma test_romega_1b : - forall (z z1 z2 : Z), +Lemma test_romega_1b : + forall (z z1 z2 : Z), z2 <= z1 -> z1 <= z2 -> z1 >= 0 -> @@ -45,42 +45,42 @@ intros z z1 z2. omega. Qed. -Lemma test_romega_2 : forall a b c:Z, +Lemma test_romega_2 : forall a b c:Z, 0<=a-b<=1 -> b-c<=2 -> a-c<=3. Proof. intros. omega. Qed. -Lemma test_romega_2b : forall a b c:Z, +Lemma test_romega_2b : forall a b c:Z, 0<=a-b<=1 -> b-c<=2 -> a-c<=3. Proof. intros a b c. omega. Qed. -Lemma test_romega_3 : forall a b h hl hr ha hb, - 0 <= ha - hl <= 1 -> +Lemma test_romega_3 : forall a b h hl hr ha hb, + 0 <= ha - hl <= 1 -> -2 <= hl - hr <= 2 -> h =b+1 -> (ha >= hr /\ a = ha \/ ha <= hr /\ a = hr) -> (hl >= hr /\ b = hl \/ hl <= hr /\ b = hr) -> (-3 <= ha -hr <=3 -> 0 <= hb - a <= 1) -> - (-2 <= ha-hr <=2 -> hb = a + 1) -> + (-2 <= ha-hr <=2 -> hb = a + 1) -> 0 <= hb - h <= 1. Proof. intros. omega. Qed. -Lemma test_romega_3b : forall a b h hl hr ha hb, - 0 <= ha - hl <= 1 -> +Lemma test_romega_3b : forall a b h hl hr ha hb, + 0 <= ha - hl <= 1 -> -2 <= hl - hr <= 2 -> h =b+1 -> (ha >= hr /\ a = ha \/ ha <= hr /\ a = hr) -> (hl >= hr /\ b = hl \/ hl <= hr /\ b = hr) -> (-3 <= ha -hr <=3 -> 0 <= hb - a <= 1) -> - (-2 <= ha-hr <=2 -> hb = a + 1) -> + (-2 <= ha-hr <=2 -> hb = a + 1) -> 0 <= hb - h <= 1. Proof. intros a b h hl hr ha hb. @@ -88,18 +88,18 @@ omega. Qed. -Lemma test_romega_4 : forall hr ha, +Lemma test_romega_4 : forall hr ha, ha = 0 -> - (ha = 0 -> hr =0) -> + (ha = 0 -> hr =0) -> hr = 0. Proof. intros hr ha. omega. Qed. -Lemma test_romega_5 : forall hr ha, +Lemma test_romega_5 : forall hr ha, ha = 0 -> - (~ha = 0 \/ hr =0) -> + (~ha = 0 \/ hr =0) -> hr = 0. Proof. intros hr ha. @@ -118,14 +118,14 @@ intros z. omega. Qed. -Lemma test_romega_7 : forall z, +Lemma test_romega_7 : forall z, 0>=0 /\ z=0 \/ 0<=0 /\ z =0 -> 1 = z+1. Proof. intros. omega. Qed. -Lemma test_romega_7b : forall z, +Lemma test_romega_7b : forall z, 0>=0 /\ z=0 \/ 0<=0 /\ z =0 -> 1 = z+1. Proof. intros. diff --git a/test-suite/success/Omega2.v b/test-suite/success/Omega2.v index 54b13702..c4d086a3 100644 --- a/test-suite/success/Omega2.v +++ b/test-suite/success/Omega2.v @@ -4,7 +4,7 @@ Require Import ZArith Omega. Open Scope Z_scope. -Lemma Test46 : +Lemma Test46 : forall v1 v2 v3 v4 v5 : Z, ((2 * v4) + (5)) + (8 * v2) <= ((4 * v4) + (3 * v4)) + (5 * v4) -> 9 * v4 > (1 * v4) + ((2 * v1) + (0 * v2)) -> diff --git a/test-suite/success/OmegaPre.v b/test-suite/success/OmegaPre.v index bb800b7a..f4996734 100644 --- a/test-suite/success/OmegaPre.v +++ b/test-suite/success/OmegaPre.v @@ -4,7 +4,7 @@ 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 diff --git a/test-suite/success/ProgramWf.v b/test-suite/success/ProgramWf.v new file mode 100644 index 00000000..81bdbc29 --- /dev/null +++ b/test-suite/success/ProgramWf.v @@ -0,0 +1,99 @@ +Require Import Arith Program. +Require Import ZArith Zwf. + +Set Implicit Arguments. +(* Set Printing All. *) +Print sigT_rect. +Obligation Tactic := program_simplify ; auto with *. +About MR. + +Program Fixpoint merge (n m : nat) {measure (n + m) (lt)} : nat := + match n with + | 0 => 0 + | S n' => merge n' m + end. + +Print merge. + + +Print Zlt. +Print Zwf. + +Open Local Scope Z_scope. + +Program Fixpoint Zwfrec (n m : Z) {measure (n + m) (Zwf 0)} : Z := + match n ?= m with + | Lt => Zwfrec n (Zpred m) + | _ => 0 + end. + +Next Obligation. + red. Admitted. + +Close Scope Z_scope. + +Program Fixpoint merge_wf (n m : nat) {wf lt m} : nat := + match n with + | 0 => 0 + | S n' => merge n' m + end. + +Print merge_wf. + +Program Fixpoint merge_one (n : nat) {measure n} : nat := + match n with + | 0 => 0 + | S n' => merge_one n' + end. + +Print Hint well_founded. +Print merge_one. Eval cbv delta [merge_one] beta zeta in merge_one. + +Import WfExtensionality. + +Lemma merge_unfold n m : merge n m = + match n with + | 0 => 0 + | S n' => merge n' m + end. +Proof. intros. unfold merge at 1. unfold merge_func. + unfold_sub merge (merge n m). + simpl. destruct n ; reflexivity. +Qed. + +Print merge. + +Require Import Arith. +Unset Implicit Arguments. + +Time 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 Setoid. + +Next Obligation. + intros ; simpl in *. apply H. + simpl in * ; omega. +Qed. + +Next Obligation. simpl in *; intros. + revert H0 ; clear_subset_proofs. intros. + case (le_gt_dec p i) ; intro. simpl in *. assert(p = i) by omega. subst. + revert H0 ; clear_subset_proofs ; tauto. + + apply H. simpl. omega. +Qed. + +Program Fixpoint check_n' (n : nat) (m : nat | m = n) (p : nat) (q : nat | q = p) + {measure (p - n) p} : nat := + _. diff --git a/test-suite/success/Projection.v b/test-suite/success/Projection.v index 88da6013..d8faa88a 100644 --- a/test-suite/success/Projection.v +++ b/test-suite/success/Projection.v @@ -12,7 +12,7 @@ Check fun (s:S) (a b:s.(Dom)) => s.(Op) a b. Set Implicit Arguments. Unset Strict Implicit. -Unset Strict Implicit. +Unset Strict Implicit. Structure S' (A : Set) : Type := {Dom' : Type; Op' : A -> Dom' -> Dom'}. @@ -29,9 +29,9 @@ Check fun (s:S') (a b:s.(Dom')) => _.(Op') a b. Check fun (s:S') (a b:s.(Dom')) => s.(Op') a b. Set Implicit Arguments. -Unset Strict Implicits. +Unset Strict Implicits. -Structure S' (A:Set) : Type := +Structure S' (A:Set) : Type := {Dom' : Type; Op' : A -> Dom' -> Dom'}. diff --git a/test-suite/success/ROmega.v b/test-suite/success/ROmega.v index 0c37c59a..801ece9e 100644 --- a/test-suite/success/ROmega.v +++ b/test-suite/success/ROmega.v @@ -22,7 +22,7 @@ Qed. Lemma lem3 : forall x y : Z, x = y -> (x + x)%Z = (y + y)%Z. Proof. intros. -romega. +romega. Qed. (* Proposed by Jean-Christophe Filliâtre: confusion between an Omega *) diff --git a/test-suite/success/ROmega0.v b/test-suite/success/ROmega0.v index 86cf49cb..1348bb62 100644 --- a/test-suite/success/ROmega0.v +++ b/test-suite/success/ROmega0.v @@ -3,24 +3,24 @@ Open Scope Z_scope. (* Pierre L: examples gathered while debugging romega. *) -Lemma test_romega_0 : - forall m m', +Lemma test_romega_0 : + forall m m', 0<= m <= 1 -> 0<= m' <= 1 -> (0 < m <-> 0 < m') -> m = m'. Proof. intros. romega. Qed. -Lemma test_romega_0b : - forall m m', +Lemma test_romega_0b : + forall m m', 0<= m <= 1 -> 0<= m' <= 1 -> (0 < m <-> 0 < m') -> m = m'. Proof. intros m m'. romega. Qed. -Lemma test_romega_1 : - forall (z z1 z2 : Z), +Lemma test_romega_1 : + forall (z z1 z2 : Z), z2 <= z1 -> z1 <= z2 -> z1 >= 0 -> @@ -32,8 +32,8 @@ intros. romega. Qed. -Lemma test_romega_1b : - forall (z z1 z2 : Z), +Lemma test_romega_1b : + forall (z z1 z2 : Z), z2 <= z1 -> z1 <= z2 -> z1 >= 0 -> @@ -45,42 +45,42 @@ intros z z1 z2. romega. Qed. -Lemma test_romega_2 : forall a b c:Z, +Lemma test_romega_2 : forall a b c:Z, 0<=a-b<=1 -> b-c<=2 -> a-c<=3. Proof. intros. romega. Qed. -Lemma test_romega_2b : forall a b c:Z, +Lemma test_romega_2b : forall a b c:Z, 0<=a-b<=1 -> b-c<=2 -> a-c<=3. Proof. intros a b c. romega. Qed. -Lemma test_romega_3 : forall a b h hl hr ha hb, - 0 <= ha - hl <= 1 -> +Lemma test_romega_3 : forall a b h hl hr ha hb, + 0 <= ha - hl <= 1 -> -2 <= hl - hr <= 2 -> h =b+1 -> (ha >= hr /\ a = ha \/ ha <= hr /\ a = hr) -> (hl >= hr /\ b = hl \/ hl <= hr /\ b = hr) -> (-3 <= ha -hr <=3 -> 0 <= hb - a <= 1) -> - (-2 <= ha-hr <=2 -> hb = a + 1) -> + (-2 <= ha-hr <=2 -> hb = a + 1) -> 0 <= hb - h <= 1. Proof. intros. romega. Qed. -Lemma test_romega_3b : forall a b h hl hr ha hb, - 0 <= ha - hl <= 1 -> +Lemma test_romega_3b : forall a b h hl hr ha hb, + 0 <= ha - hl <= 1 -> -2 <= hl - hr <= 2 -> h =b+1 -> (ha >= hr /\ a = ha \/ ha <= hr /\ a = hr) -> (hl >= hr /\ b = hl \/ hl <= hr /\ b = hr) -> (-3 <= ha -hr <=3 -> 0 <= hb - a <= 1) -> - (-2 <= ha-hr <=2 -> hb = a + 1) -> + (-2 <= ha-hr <=2 -> hb = a + 1) -> 0 <= hb - h <= 1. Proof. intros a b h hl hr ha hb. @@ -88,18 +88,18 @@ romega. Qed. -Lemma test_romega_4 : forall hr ha, +Lemma test_romega_4 : forall hr ha, ha = 0 -> - (ha = 0 -> hr =0) -> + (ha = 0 -> hr =0) -> hr = 0. Proof. intros hr ha. romega. Qed. -Lemma test_romega_5 : forall hr ha, +Lemma test_romega_5 : forall hr ha, ha = 0 -> - (~ha = 0 \/ hr =0) -> + (~ha = 0 \/ hr =0) -> hr = 0. Proof. intros hr ha. @@ -118,14 +118,14 @@ intros z. romega. Qed. -Lemma test_romega_7 : forall z, +Lemma test_romega_7 : forall z, 0>=0 /\ z=0 \/ 0<=0 /\ z =0 -> 1 = z+1. Proof. intros. romega. Qed. -Lemma test_romega_7b : forall z, +Lemma test_romega_7b : forall z, 0>=0 /\ z=0 \/ 0<=0 /\ z =0 -> 1 = z+1. Proof. intros. diff --git a/test-suite/success/ROmega2.v b/test-suite/success/ROmega2.v index a3be2898..87e8c8e3 100644 --- a/test-suite/success/ROmega2.v +++ b/test-suite/success/ROmega2.v @@ -6,7 +6,7 @@ Open Scope Z_scope. (* First a simplified version used during debug of romega on Test46 *) -Lemma Test46_simplified : +Lemma Test46_simplified : forall v1 v2 v5 : Z, 0 = v2 + v5 -> 0 < v5 -> @@ -18,7 +18,7 @@ Qed. (* The complete problem *) -Lemma Test46 : +Lemma Test46 : forall v1 v2 v3 v4 v5 : Z, ((2 * v4) + (5)) + (8 * v2) <= ((4 * v4) + (3 * v4)) + (5 * v4) -> 9 * v4 > (1 * v4) + ((2 * v1) + (0 * v2)) -> diff --git a/test-suite/success/ROmegaPre.v b/test-suite/success/ROmegaPre.v index 550edca5..bd473fa6 100644 --- a/test-suite/success/ROmegaPre.v +++ b/test-suite/success/ROmegaPre.v @@ -4,7 +4,7 @@ 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 diff --git a/test-suite/success/RecTutorial.v b/test-suite/success/RecTutorial.v index 60e170e4..d4e6a82e 100644 --- a/test-suite/success/RecTutorial.v +++ b/test-suite/success/RecTutorial.v @@ -1,5 +1,5 @@ -Inductive nat : Set := - | O : nat +Inductive nat : Set := + | O : nat | S : nat->nat. Check nat. Check O. @@ -14,8 +14,8 @@ Print le. Theorem zero_leq_three: 0 <= 3. Proof. - constructor 2. - constructor 2. + constructor 2. + constructor 2. constructor 2. constructor 1. @@ -32,7 +32,7 @@ Qed. Lemma zero_lt_three : 0 < 3. Proof. unfold lt. - repeat constructor. + repeat constructor. Qed. @@ -132,7 +132,7 @@ Require Import Compare_dec. Check le_lt_dec. -Definition max (n p :nat) := match le_lt_dec n p with +Definition max (n p :nat) := match le_lt_dec n p with | left _ => p | right _ => n end. @@ -152,9 +152,9 @@ Extraction max. Inductive tree(A:Set) : Set := - node : A -> forest A -> tree A + node : A -> forest A -> tree A with - forest (A: Set) : Set := + forest (A: Set) : Set := nochild : forest A | addchild : tree A -> forest A -> forest A. @@ -162,7 +162,7 @@ with -Inductive +Inductive even : nat->Prop := evenO : even O | evenS : forall n, odd n -> even (S n) @@ -176,11 +176,11 @@ Qed. -Definition nat_case := +Definition nat_case := fun (Q : Type)(g0 : Q)(g1 : nat -> Q)(n:nat) => match n return Q with - | 0 => g0 - | S p => g1 p + | 0 => g0 + | S p => g1 p end. Eval simpl in (nat_case nat 0 (fun p => p) 34). @@ -200,7 +200,7 @@ Eval simpl in fun p => pred (S p). Definition xorb (b1 b2:bool) := -match b1, b2 with +match b1, b2 with | false, true => true | true, false => true | _ , _ => false @@ -208,7 +208,7 @@ end. Definition pred_spec (n:nat) := {m:nat | n=0 /\ m=0 \/ n = S m}. - + Definition predecessor : forall n:nat, pred_spec n. intro n;case n. @@ -220,7 +220,7 @@ Print predecessor. Extraction predecessor. -Theorem nat_expand : +Theorem nat_expand : forall n:nat, n = match n with 0 => 0 | S p => S p end. intro n;case n;simpl;auto. Qed. @@ -228,7 +228,7 @@ Qed. Check (fun p:False => match p return 2=3 with end). Theorem fromFalse : False -> 0=1. - intro absurd. + intro absurd. contradiction. Qed. @@ -244,12 +244,12 @@ Section equality_elimination. End equality_elimination. - + Theorem trans : forall n m p:nat, n=m -> m=p -> n=p. Proof. - intros n m p eqnm. + intros n m p eqnm. case eqnm. - trivial. + trivial. Qed. Lemma Rw : forall x y: nat, y = y * x -> y * x * x = y. @@ -282,7 +282,7 @@ Lemma four_n : forall n:nat, n+n+n+n = 4*n. Undo. intro n; pattern n at 1. - + rewrite <- mult_1_l. repeat rewrite mult_distr_S. @@ -314,7 +314,7 @@ Proof. intros m Hm; exists m;trivial. Qed. -Definition Vtail_total +Definition Vtail_total (A : Set) (n : nat) (v : vector A n) : vector A (pred n):= match v in (vector _ n0) return (vector A (pred n0)) with | Vnil => Vnil A @@ -322,7 +322,7 @@ match v in (vector _ n0) return (vector A (pred n0)) with end. Definition Vtail' (A:Set)(n:nat)(v:vector A n) : vector A (pred n). - intros A n v; case v. + case v. simpl. exact (Vnil A). simpl. @@ -331,7 +331,7 @@ Defined. (* Inductive Lambda : Set := - lambda : (Lambda -> False) -> Lambda. + lambda : (Lambda -> False) -> Lambda. Error: Non strictly positive occurrence of "Lambda" in @@ -347,7 +347,7 @@ Section Paradox. (* understand matchL Q l (fun h : Lambda -> False => t) - as match l return Q with lambda h => t end + as match l return Q with lambda h => t end *) Definition application (f x: Lambda) :False := @@ -377,26 +377,26 @@ Definition isingle l := inode l (fun i => ileaf). Definition t1 := inode 0 (fun n => isingle (Z_of_nat (2*n))). -Definition t2 := inode 0 - (fun n : nat => +Definition t2 := inode 0 + (fun n : nat => inode (Z_of_nat n) (fun p => isingle (Z_of_nat (n*p)))). Inductive itree_le : itree-> itree -> Prop := | le_leaf : forall t, itree_le ileaf t - | le_node : forall l l' s s', - Zle l l' -> - (forall i, exists j:nat, itree_le (s i) (s' j)) -> + | le_node : forall l l' s s', + Zle l l' -> + (forall i, exists j:nat, itree_le (s i) (s' j)) -> itree_le (inode l s) (inode l' s'). -Theorem itree_le_trans : +Theorem itree_le_trans : forall t t', itree_le t t' -> forall t'', itree_le t' t'' -> itree_le t t''. induction t. constructor 1. - + intros t'; case t'. inversion 1. intros z0 i0 H0. @@ -409,20 +409,20 @@ Theorem itree_le_trans : inversion_clear H0. intro i2; case (H4 i2). intros. - generalize (H i2 _ H0). + generalize (H i2 _ H0). intros. case (H3 x);intros. generalize (H5 _ H6). exists x0;auto. Qed. - + Inductive itree_le' : itree-> itree -> Prop := | le_leaf' : forall t, itree_le' ileaf t - | le_node' : forall l l' s s' g, - Zle l l' -> - (forall i, itree_le' (s i) (s' (g i))) -> + | le_node' : forall l l' s s' g, + Zle l l' -> + (forall i, itree_le' (s i) (s' (g i))) -> itree_le' (inode l s) (inode l' s'). @@ -434,7 +434,7 @@ Lemma t1_le_t2 : itree_le t1 t2. constructor. auto with zarith. intro i; exists (2 * i). - unfold isingle. + unfold isingle. constructor. auto with zarith. exists i;constructor. @@ -455,7 +455,7 @@ Qed. Require Import List. -Inductive ltree (A:Set) : Set := +Inductive ltree (A:Set) : Set := lnode : A -> list (ltree A) -> ltree A. Inductive prop : Prop := @@ -482,8 +482,8 @@ Qed. Check (fun (P:Prop->Prop)(p: ex_Prop P) => match p with exP_intro X HX => X end). Error: -Incorrect elimination of "p" in the inductive type -"ex_Prop", the return type has sort "Type" while it should be +Incorrect elimination of "p" in the inductive type +"ex_Prop", the return type has sort "Type" while it should be "Prop" Elimination of an inductive object of sort "Prop" @@ -496,8 +496,8 @@ because proofs can be eliminated only to build proofs Check (match prop_inject with (prop_intro P p) => P end). Error: -Incorrect elimination of "prop_inject" in the inductive type -"prop", the return type has sort "Type" while it should be +Incorrect elimination of "prop_inject" in the inductive type +"prop", the return type has sort "Type" while it should be "Prop" Elimination of an inductive object of sort "Prop" @@ -508,17 +508,17 @@ because proofs can be eliminated only to build proofs Print prop_inject. (* -prop_inject = +prop_inject = prop_inject = prop_intro prop (fun H : prop => H) : prop *) -Inductive typ : Type := - typ_intro : Type -> typ. +Inductive typ : Type := + typ_intro : Type -> typ. Definition typ_inject: typ. -split. +split. exact typ. (* Defined. @@ -564,13 +564,13 @@ Reset comes_from_the_left. Definition comes_from_the_left (P Q:Prop)(H:P \/ Q): Prop := match H with - | or_introl p => True + | or_introl p => True | or_intror q => False end. Error: -Incorrect elimination of "H" in the inductive type -"or", the return type has sort "Type" while it should be +Incorrect elimination of "H" in the inductive type +"or", the return type has sort "Type" while it should be "Prop" Elimination of an inductive object of sort "Prop" @@ -582,41 +582,41 @@ because proofs can be eliminated only to build proofs Definition comes_from_the_left_sumbool (P Q:Prop)(x:{P}+{Q}): Prop := match x with - | left p => True + | left p => True | right q => False end. - + Close Scope Z_scope. -Theorem S_is_not_O : forall n, S n <> 0. +Theorem S_is_not_O : forall n, S n <> 0. -Definition Is_zero (x:nat):= match x with - | 0 => True +Definition Is_zero (x:nat):= match x with + | 0 => True | _ => False end. Lemma O_is_zero : forall m, m = 0 -> Is_zero m. Proof. intros m H; subst m. - (* + (* ============================ Is_zero 0 *) simpl;trivial. Qed. - + red; intros n Hn. apply O_is_zero with (m := S n). assumption. Qed. -Theorem disc2 : forall n, S (S n) <> 1. +Theorem disc2 : forall n, S (S n) <> 1. Proof. intros n Hn; discriminate. Qed. @@ -632,7 +632,7 @@ Qed. Theorem inj_succ : forall n m, S n = S m -> n = m. Proof. - + Lemma inj_pred : forall n m, n = m -> pred n = pred m. Proof. @@ -666,9 +666,9 @@ Proof. intros n p H; case H ; intros; discriminate. Qed. - + eapply not_le_Sn_0_with_constraints; eauto. -Qed. +Qed. Theorem not_le_Sn_0' : forall n:nat, ~ (S n <= 0). @@ -681,7 +681,7 @@ Check le_Sn_0_inv. Theorem le_Sn_0'' : forall n p : nat, ~ S n <= 0 . Proof. - intros n p H; + intros n p H; inversion H using le_Sn_0_inv. Qed. @@ -689,9 +689,9 @@ Derive Inversion_clear le_Sn_0_inv' with (forall n :nat, S n <= 0). Check le_Sn_0_inv'. -Theorem le_reverse_rules : - forall n m:nat, n <= m -> - n = m \/ +Theorem le_reverse_rules : + forall n m:nat, n <= m -> + n = m \/ exists p, n <= p /\ m = S p. Proof. intros n m H; inversion H. @@ -704,21 +704,21 @@ Restart. Qed. Inductive ArithExp : Set := - Zero : ArithExp + Zero : ArithExp | Succ : ArithExp -> ArithExp | Plus : ArithExp -> ArithExp -> ArithExp. Inductive RewriteRel : ArithExp -> ArithExp -> Prop := RewSucc : forall e1 e2 :ArithExp, - RewriteRel e1 e2 -> RewriteRel (Succ e1) (Succ e2) + RewriteRel e1 e2 -> RewriteRel (Succ e1) (Succ e2) | RewPlus0 : forall e:ArithExp, - RewriteRel (Plus Zero e) e + RewriteRel (Plus Zero e) e | RewPlusS : forall e1 e2:ArithExp, RewriteRel e1 e2 -> RewriteRel (Plus (Succ e1) e2) (Succ (Plus e1 e2)). - + Fixpoint plus (n p:nat) {struct n} : nat := match n with | 0 => p @@ -739,7 +739,7 @@ Fixpoint plus'' (n p:nat) {struct n} : nat := Fixpoint even_test (n:nat) : bool := - match n + match n with 0 => true | 1 => false | S (S p) => even_test p @@ -749,20 +749,20 @@ Fixpoint even_test (n:nat) : bool := Reset even_test. Fixpoint even_test (n:nat) : bool := - match n - with + match n + with | 0 => true | S p => odd_test p end with odd_test (n:nat) : bool := match n - with + with | 0 => false | S p => even_test p end. - + Eval simpl in even_test. @@ -779,11 +779,11 @@ Section Principle_of_Induction. Variable P : nat -> Prop. Hypothesis base_case : P 0. Hypothesis inductive_step : forall n:nat, P n -> P (S n). -Fixpoint nat_ind (n:nat) : (P n) := +Fixpoint nat_ind (n:nat) : (P n) := match n return P n with | 0 => base_case | S m => inductive_step m (nat_ind m) - end. + end. End Principle_of_Induction. @@ -803,9 +803,9 @@ Variable P : nat -> nat ->Prop. Hypothesis base_case1 : forall x:nat, P 0 x. Hypothesis base_case2 : forall x:nat, P (S x) 0. Hypothesis inductive_step : forall n m:nat, P n m -> P (S n) (S m). -Fixpoint nat_double_ind (n m:nat){struct n} : P n m := - match n, m return P n m with - | 0 , x => base_case1 x +Fixpoint nat_double_ind (n m:nat){struct n} : P n m := + match n, m return P n m with + | 0 , x => base_case1 x | (S x), 0 => base_case2 x | (S x), (S y) => inductive_step x y (nat_double_ind x y) end. @@ -816,15 +816,15 @@ Variable P : nat -> nat -> Set. Hypothesis base_case1 : forall x:nat, P 0 x. Hypothesis base_case2 : forall x:nat, P (S x) 0. Hypothesis inductive_step : forall n m:nat, P n m -> P (S n) (S m). -Fixpoint nat_double_rec (n m:nat){struct n} : P n m := - match n, m return P n m with - | 0 , x => base_case1 x +Fixpoint nat_double_rec (n m:nat){struct n} : P n m := + match n, m return P n m with + | 0 , x => base_case1 x | (S x), 0 => base_case2 x | (S x), (S y) => inductive_step x y (nat_double_rec x y) end. End Principle_of_Double_Recursion. -Definition min : nat -> nat -> nat := +Definition min : nat -> nat -> nat := nat_double_rec (fun (x y:nat) => nat) (fun (x:nat) => 0) (fun (y:nat) => 0) @@ -868,7 +868,7 @@ Require Import Minus. (* Fixpoint div (x y:nat){struct x}: nat := - if eq_nat_dec x 0 + if eq_nat_dec x 0 then 0 else if eq_nat_dec y 0 then x @@ -901,18 +901,18 @@ Qed. Lemma minus_smaller_positive : forall x y:nat, x <>0 -> y <> 0 -> x - y < x. Proof. - destruct x; destruct y; - ( simpl;intros; apply minus_smaller_S || + destruct x; destruct y; + ( simpl;intros; apply minus_smaller_S || intros; absurd (0=0); auto). Qed. -Definition minus_decrease : forall x y:nat, Acc lt x -> - x <> 0 -> +Definition minus_decrease : forall x y:nat, Acc lt x -> + x <> 0 -> y <> 0 -> Acc lt (x-y). Proof. intros x y H; case H. - intros Hz posz posy. + intros Hz posz posy. apply Hz; apply minus_smaller_positive; assumption. Defined. @@ -920,21 +920,19 @@ Print minus_decrease. -Definition div_aux (x y:nat)(H: Acc lt x):nat. - fix 3. - intros. - refine (if eq_nat_dec x 0 - then 0 - else if eq_nat_dec y 0 +Fixpoint div_aux (x y:nat)(H: Acc lt x):nat. + refine (if eq_nat_dec x 0 + then 0 + else if eq_nat_dec y 0 then y else div_aux (x-y) y _). - apply (minus_decrease x y H);assumption. + apply (minus_decrease x y H);assumption. Defined. Print div_aux. (* -div_aux = +div_aux = (fix div_aux (x y : nat) (H : Acc lt x) {struct H} : nat := match eq_nat_dec x 0 with | left _ => 0 @@ -948,7 +946,7 @@ div_aux = *) Require Import Wf_nat. -Definition div x y := div_aux x y (lt_wf x). +Definition div x y := div_aux x y (lt_wf x). Extraction div. (* @@ -974,7 +972,7 @@ Proof. Abort. (* - Lemma vector0_is_vnil_aux : forall (A:Set)(n:nat)(v:vector A n), + Lemma vector0_is_vnil_aux : forall (A:Set)(n:nat)(v:vector A n), n= 0 -> v = Vnil A. Toplevel input, characters 40281-40287 @@ -990,7 +988,7 @@ The term "Vnil A" has type "vector A 0" while it is expected to have type *) Require Import JMeq. -Lemma vector0_is_vnil_aux : forall (A:Set)(n:nat)(v:vector A n), +Lemma vector0_is_vnil_aux : forall (A:Set)(n:nat)(v:vector A n), n= 0 -> JMeq v (Vnil A). Proof. destruct v. @@ -1026,7 +1024,7 @@ Eval simpl in (fun (A:Set)(v:vector A 0) => v). Lemma Vid_eq : forall (n:nat) (A:Type)(v:vector A n), v=(Vid _ n v). Proof. - destruct v. + destruct v. reflexivity. reflexivity. Defined. @@ -1034,7 +1032,7 @@ Defined. Theorem zero_nil : forall A (v:vector A 0), v = Vnil. Proof. intros. - change (Vnil (A:=A)) with (Vid _ 0 v). + change (Vnil (A:=A)) with (Vid _ 0 v). apply Vid_eq. Defined. @@ -1050,7 +1048,7 @@ Defined. -Definition vector_double_rect : +Definition vector_double_rect : forall (A:Set) (P: forall (n:nat),(vector A n)->(vector A n) -> Type), P 0 Vnil Vnil -> (forall n (v1 v2 : vector A n) a b, P n v1 v2 -> @@ -1105,7 +1103,7 @@ Qed. | LCons : A -> LList A -> LList A. - + Definition head (A:Set)(s : Stream A) := match s with Cons a s' => a end. @@ -1144,7 +1142,7 @@ Hypothesis bisim2 : forall s1 s2:Stream A, R s1 s2 -> CoFixpoint park_ppl : forall s1 s2:Stream A, R s1 s2 -> EqSt s1 s2 := fun s1 s2 (p : R s1 s2) => - eqst s1 s2 (bisim1 p) + eqst s1 s2 (bisim1 p) (park_ppl (bisim2 p)). End Parks_Principle. @@ -1154,7 +1152,7 @@ Theorem map_iterate : forall (A:Set)(f:A->A)(x:A), Proof. intros A f x. apply park_ppl with - (R:= fun s1 s2 => exists x: A, + (R:= fun s1 s2 => exists x: A, s1 = iterate f (f x) /\ s2 = map f (iterate f x)). intros s1 s2 (x0,(eqs1,eqs2));rewrite eqs1;rewrite eqs2;reflexivity. diff --git a/test-suite/success/Record.v b/test-suite/success/Record.v index 885fff48..8334322c 100644 --- a/test-suite/success/Record.v +++ b/test-suite/success/Record.v @@ -17,34 +17,34 @@ Obligation Tactic := crush. Program Definition vnil {A} : vector A 0 := {| vec_list := [] |}. -Program Definition vcons {A n} (a : A) (v : vector A n) : vector A (S n) := +Program Definition vcons {A n} (a : A) (v : vector A n) : vector A (S n) := {| vec_list := cons a (vec_list v) |}. Hint Rewrite map_length rev_length : datatypes. -Program Definition vmap {A B n} (f : A -> B) (v : vector A n) : vector B n := +Program Definition vmap {A B n} (f : A -> B) (v : vector A n) : vector B n := {| vec_list := map f v |}. -Program Definition vreverse {A n} (v : vector A n) : vector A n := +Program Definition vreverse {A n} (v : vector A n) : vector A n := {| vec_list := rev v |}. -Fixpoint va_list {A B} (v : list (A -> B)) (w : list A) : list B := +Fixpoint va_list {A B} (v : list (A -> B)) (w : list A) : list B := match v, w with | nil, nil => nil | cons f fs, cons x xs => cons (f x) (va_list fs xs) | _, _ => nil end. -Program Definition va {A B n} (v : vector (A -> B) n) (w : vector A n) : vector B n := +Program Definition va {A B n} (v : vector (A -> B) n) (w : vector A n) : vector B n := {| vec_list := va_list v w |}. -Next Obligation. +Next Obligation. destruct v as [v Hv]; destruct w as [w Hw] ; simpl. - subst n. revert w Hw. induction v ; destruct w ; crush. + subst n. revert w Hw. induction v ; destruct w ; crush. rewrite IHv ; auto. Qed. -(* Correct type inference of record notation. Initial example by Spiwack. *) +(* Correct type inference of record notation. Initial example by Spiwack. *) Inductive Machin := { Bazar : option Machin @@ -80,3 +80,10 @@ Record DecidableOrder : Type := ; le_trans : transitive _ le ; le_total : forall x y, {x <= y}+{y <= x} }. + +(* Test syntactic sugar suggested by wish report #2138 *) + +Record R : Type := { + P (A : Type) : Prop := exists x : A -> A, x = x; + Q A : P A -> P A +}. diff --git a/test-suite/success/Section.v b/test-suite/success/Section.v new file mode 100644 index 00000000..8e9e79b3 --- /dev/null +++ b/test-suite/success/Section.v @@ -0,0 +1,6 @@ +(* Test bug 2168: ending section of some name was removing objects of the + same name *) + +Require Import make_notation. + +Check add2 3. diff --git a/test-suite/success/Simplify_eq.v b/test-suite/success/Simplify_eq.v index 5b856e3d..d9abdbf5 100644 --- a/test-suite/success/Simplify_eq.v +++ b/test-suite/success/Simplify_eq.v @@ -2,11 +2,11 @@ (* Check that Simplify_eq tries Intro until *) -Lemma l1 : 0 = 1 -> False. +Lemma l1 : 0 = 1 -> False. simplify_eq 1. Qed. -Lemma l2 : forall (x : nat) (H : S x = S (S x)), H = H -> False. +Lemma l2 : forall (x : nat) (H : S x = S (S x)), H = H -> False. simplify_eq H. intros. apply (n_Sn x H0). diff --git a/test-suite/success/Tauto.v b/test-suite/success/Tauto.v index f0809839..42898b8d 100644 --- a/test-suite/success/Tauto.v +++ b/test-suite/success/Tauto.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: Tauto.v 7693 2005-12-21 23:50:17Z herbelin $ *) +(* $Id$ *) (**** Tactics Tauto and Intuition ****) diff --git a/test-suite/success/TestRefine.v b/test-suite/success/TestRefine.v index 82c5cf2e..5f44c752 100644 --- a/test-suite/success/TestRefine.v +++ b/test-suite/success/TestRefine.v @@ -9,13 +9,11 @@ (************************************************************************) Lemma essai : forall x : nat, x = x. - refine ((fun x0 : nat => match x0 with | O => _ | S p => _ - end) - :forall x : nat, x = x). (* x0=x0 et x0=x0 *) + end)). Restart. @@ -44,7 +42,7 @@ Abort. (************************************************************************) -Lemma T : nat. +Lemma T : nat. refine (S _). @@ -97,7 +95,7 @@ Abort. (************************************************************************) -Parameter f : nat * nat -> nat -> nat. +Parameter f : nat * nat -> nat -> nat. Lemma essai : nat. @@ -145,11 +143,10 @@ Lemma essai : forall n : nat, {x : nat | x = S n}. Restart. refine - ((fun n : nat => match n with + (fun n : nat => match n with | O => _ | S p => _ - end) - :forall n : nat, {x : nat | x = S n}). + end). Restart. @@ -178,10 +175,10 @@ Restart. | S p => _ end). -exists 1. trivial. +exists 1. trivial. elim (f0 p). refine - (fun (x : nat) (h : x = S p) => exist (fun x : nat => x = S (S p)) (S x) _). + (fun (x : nat) (h : x = S p) => exist (fun x : nat => x = S (S p)) (S x) _). rewrite h. auto. Qed. diff --git a/test-suite/success/Typeclasses.v b/test-suite/success/Typeclasses.v new file mode 100644 index 00000000..55351a47 --- /dev/null +++ b/test-suite/success/Typeclasses.v @@ -0,0 +1,60 @@ +Generalizable All Variables. + +Module mon. + +Reserved Notation "'return' t" (at level 0). +Reserved Notation "x >>= y" (at level 65, left associativity). + + + +Record Monad {m : Type -> Type} := { + unit : Π{α}, α -> m α where "'return' t" := (unit t) ; + bind : Π{α β}, m α -> (α -> m β) -> m β where "x >>= y" := (bind x y) ; + bind_unit_left : Π{α β} (a : α) (f : α -> m β), return a >>= f = f a }. + +Print Visibility. +Print unit. +Implicit Arguments unit [[m] [m0] [α]]. +Implicit Arguments Monad []. +Notation "'return' t" := (unit t). + +(* Test correct handling of existentials and defined fields. *) + +Class A `(e: T) := { a := True }. +Class B `(e_: T) := { e := e_; sg_ass :> A e }. + +Goal forall `{B T}, a. + intros. exact I. +Defined. + +Class B' `(e_: T) := { e' := e_; sg_ass' :> A e_ }. + +Goal forall `{B' T}, a. + intros. exact I. +Defined. + +End mon. + +(* Correct treatment of dependent goals *) + +(* First some preliminaries: *) + +Section sec. + Context {N: Type}. + Class C (f: N->N) := {}. + Class E := { e: N -> N }. + Context + (g: N -> N) `(E) `(C e) + `(forall (f: N -> N), C f -> C (fun x => f x)) + (U: forall f: N -> N, C f -> False). + +(* Now consider the following: *) + + Let foo := U (fun x => e x). + Check foo _. + +(* This type checks fine, so far so good. But now + let's try to get rid of the intermediate constant foo. + Surely we can just expand it inline, right? Wrong!: *) + Check U (fun x => e x) _. +End sec.
\ No newline at end of file diff --git a/test-suite/success/apply.v b/test-suite/success/apply.v index 952890ee..a6f9fa23 100644 --- a/test-suite/success/apply.v +++ b/test-suite/success/apply.v @@ -135,7 +135,7 @@ Qed. Definition apply (f:nat->Prop) := forall x, f x. Goal apply (fun n => n=0) -> 1=0. intro H. -auto. +auto. Qed. (* The following fails if the coercion Zpos is not introduced around p @@ -157,10 +157,10 @@ Qed. 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 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). +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 @@ -171,14 +171,14 @@ Qed. (* A similar example with a arbitrary long conversion between the two possible instances *) -Fixpoint compute_succ x := +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 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 H with (y:=y). apply H0. Qed. @@ -187,10 +187,10 @@ Qed. 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) -> +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. @@ -239,6 +239,28 @@ 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 *) +reflexivity. +Qed. + +(* Check that unification does not commit too early to a representative + of an eta-equivalence class that would be incompatible with other + unification constraints *) + +Lemma eta : forall f : (forall P, P 1), + (forall P, f P = f P) -> + forall Q, f (fun x => Q x) = f (fun x => Q x). +intros. +apply H. +Qed. + +(* Test propagation of evars from subgoal to brother subgoals *) + + (* This works because unfold calls clos_norm_flags which calls nf_evar *) + +Lemma eapply_evar_unfold : let x:=O in O=x -> 0=O. +intros x H; eapply trans_equal; +[apply H | unfold x;match goal with |- ?x = ?x => reflexivity end]. +Qed. (* Test non-regression of (temporary) bug 1981 *) @@ -248,9 +270,124 @@ exact O. trivial. Qed. -(* Test non-regression of (temporary) bug 1980 *) +(* Check pattern-unification on evars in apply unification *) + +Lemma evar : exists f : nat -> nat, forall x, f x = 0 -> x = 0. +Proof. +eexists; intros x H. +apply H. +Qed. + +(* Check that "as" clause applies to main premise only and leave the + side conditions away *) + +Lemma side_condition : + forall (A:Type) (B:Prop) x, (True -> B -> x=0) -> B -> x=x. +Proof. +intros. +apply H in H0 as ->. +reflexivity. +exact I. +Qed. + +(* Check that "apply" is chained on the last subgoal of each lemma and + that side conditions come first (as it is the case since 8.2) *) + +Lemma chaining : + forall A B C : Prop, + (1=1 -> (2=2 -> A -> B) /\ True) -> + (3=3 -> (True /\ (4=4 -> C -> A))) -> C -> B. +Proof. +intros. +apply H, H0. +exact (refl_equal 1). +exact (refl_equal 2). +exact (refl_equal 3). +exact (refl_equal 4). +assumption. +Qed. + +(* Check that the side conditions of "apply in", even when chained and + used through conjunctions, come last (as it is the case for single + calls to "apply in" w/o destruction of conjunction since 8.2) *) + +Lemma chaining_in : + forall A B C : Prop, + (1=1 -> True /\ (B -> 2=2 -> 5=0)) -> + (3=3 -> (A -> 4=4 -> B) /\ True) -> A -> 0=5. +Proof. +intros. +apply H0, H in H1 as ->. +exact (refl_equal 0). +exact (refl_equal 1). +exact (refl_equal 2). +exact (refl_equal 3). +exact (refl_equal 4). +Qed. + +(* From 12612, descent in conjunctions is more powerful *) +(* The following, which was failing badly in bug 1980, is now accepted + (even if somehow surprising) *) Goal True. -try eapply ex_intro. -trivial. +eapply ex_intro. +instantiate (2:=fun _ :True => True). +instantiate (1:=I). +exact I. Qed. + +(* The following, which were not accepted, are now accepted as + expected by descent in conjunctions *) + +Goal True. +eapply (ex_intro (fun _ => True) I). +exact I. +Qed. + +Goal True. +eapply (fun (A:Prop) (x:A) => conj I x). +exact I. +Qed. + +(* The following was not accepted from r12612 to r12657 *) + +Record sig0 := { p1 : nat; p2 : p1 = 0 }. + +Goal forall x : sig0, p1 x = 0. +intro x; +apply x. +Qed. + +(* The following worked in 8.2 but was not accepted from r12229 to + r12926 because "simple apply" started to use pattern unification of + evars. Evars pattern unification for simple (e)apply was disabled + in 12927 but "simple eapply" below worked from 12898 to 12926 + because pattern-unification also started supporting abstraction + over Metas. However it did not find the "simple" solution and hence + the subsequent "assumption" failed. *) + +Goal exists f:nat->nat, forall x y, x = y -> f x = f y. +intros; eexists; intros. +simple eapply (@f_equal nat). +assumption. +Existential 1 := fun x => x. +Qed. + +(* The following worked in 8.2 but was not accepted from r12229 to + r12897 for the same reason because eauto uses "simple apply". It + worked from 12898 to 12926 because eauto uses eassumption and not + assumption. *) + +Goal exists f:nat->nat, forall x y, x = y -> f x = f y. +intros; eexists; intros. +eauto. +Existential 1 := fun x => x. +Qed. + +(* The following was accepted before r12612 but is still not accepted in r12658 + +Goal forall x : { x:nat | x = 0}, proj1_sig x = 0. +intro x; +apply x. + +*) diff --git a/test-suite/success/autointros.v b/test-suite/success/autointros.v new file mode 100644 index 00000000..0a081271 --- /dev/null +++ b/test-suite/success/autointros.v @@ -0,0 +1,15 @@ +Set Automatic Introduction. + +Inductive even : nat -> Prop := +| even_0 : even 0 +| even_odd : forall n, odd n -> even (S n) +with odd : nat -> Prop := +| odd_1 : odd 1 +| odd_even : forall n, even n -> odd (S n). + +Lemma foo {n : nat} (E : even n) : even (S (S n)) +with bar {n : nat} (O : odd n) : odd (S (S n)). +Proof. destruct E. constructor. constructor. apply even_odd. apply (bar _ H). + destruct O. repeat constructor. apply odd_even. apply (foo _ H). +Defined. + diff --git a/test-suite/success/cc.v b/test-suite/success/cc.v index 94d827fd..b565183b 100644 --- a/test-suite/success/cc.v +++ b/test-suite/success/cc.v @@ -22,12 +22,12 @@ intros. congruence. Qed. -(* Examples that fail due to dependencies *) +(* Examples that fail due to dependencies *) (* yields transitivity problem *) Theorem dep : - forall (A : Set) (P : A -> Set) (f g : forall x : A, P x) + forall (A : Set) (P : A -> Set) (f g : forall x : A, P x) (x y : A) (e : x = y) (e0 : f y = g y), f x = g x. intros; dependent rewrite e; exact e0. Qed. @@ -42,12 +42,12 @@ intros; rewrite e; reflexivity. Qed. -(* example that Congruence. can solve - (dependent function applied to the same argument)*) +(* example that Congruence. can solve + (dependent function applied to the same argument)*) Theorem dep3 : forall (A : Set) (P : A -> Set) (f g : forall x : A, P x), - f = g -> forall x : A, f x = g x. intros. + f = g -> forall x : A, f x = g x. intros. congruence. Qed. @@ -61,7 +61,7 @@ Qed. Theorem inj2 : forall (A : Set) (a c d : A) (f : A -> A * A), - f = pair (B:=A) a -> Some (f c) = Some (f d) -> c = d. + f = pair (B:=A) a -> Some (f c) = Some (f d) -> c = d. intros. congruence. Qed. @@ -80,7 +80,7 @@ Qed. (* example with implications *) -Theorem arrow : forall (A B: Prop) (C D:Set) , A=B -> C=D -> +Theorem arrow : forall (A B: Prop) (C D:Set) , A=B -> C=D -> (A -> C) = (B -> D). congruence. Qed. @@ -101,7 +101,6 @@ Proof. congruence. auto. Qed. - - -
\ No newline at end of file + + diff --git a/test-suite/success/change.v b/test-suite/success/change.v index cea01712..5ac6ce82 100644 --- a/test-suite/success/change.v +++ b/test-suite/success/change.v @@ -4,3 +4,29 @@ 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). +Abort. + +Goal forall x, 2 + S x = 1 + S x. +intro. +change (?u + S x) with (S (u + x)). +Abort. + +(* Check the combination of at, with and in (see bug #2146) *) + +Goal 3=3 -> 3=3. intro H. +change 3 at 2 with (1+2) in |- *. +change 3 at 2 with (1+2) in H |-. +change 3 with (1+2) in H at 1 |- * at 1. +(* Now check that there are no more 3's *) +change 3 with (1+2) in * || reflexivity. +Qed. + +(* Note: the following is invalid and must fail +change 3 at 1 with (1+2) at 3. +change 3 at 1 with (1+2) in *. +change 3 at 1 with (1+2) in H at 2 |-. +change 3 at 1 with (1+2) in |- * at 3. +change 3 at 1 with (1+2) in H |- *. +change 3 at 1 with (1+2) in H, H|-. +change 3 in |- * at 1. + *) diff --git a/test-suite/success/clear.v b/test-suite/success/clear.v index 8169361c..976bec73 100644 --- a/test-suite/success/clear.v +++ b/test-suite/success/clear.v @@ -1,7 +1,7 @@ Goal forall x:nat, (forall x, x=0 -> True)->True. intros; eapply H. instantiate (1:=(fun y => _) (S x)). - simpl. + simpl. clear x. trivial. Qed. diff --git a/test-suite/success/coercions.v b/test-suite/success/coercions.v index 525348de..908b5f77 100644 --- a/test-suite/success/coercions.v +++ b/test-suite/success/coercions.v @@ -24,7 +24,7 @@ Coercion C : nat >-> Funclass. (* Remark: in the following example, it cannot be decided whether C is from nat to Funclass or from A to nat. An explicit Coercion command is - expected + expected Parameter A : nat -> Prop. Parameter C:> forall n:nat, A n -> nat. @@ -71,7 +71,6 @@ Record Morphism (X Y:Setoid) : Type := {evalMorphism :> X -> Y}. Definition extSetoid (X Y:Setoid) : Setoid. -intros X Y. constructor. exact (Morphism X Y). Defined. diff --git a/test-suite/success/conv_pbs.v b/test-suite/success/conv_pbs.v index 062c3ee5..f6ebacae 100644 --- a/test-suite/success/conv_pbs.v +++ b/test-suite/success/conv_pbs.v @@ -30,7 +30,7 @@ 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 + | (y,t) :: rho => if var_eq_dec x y then remove_assoc A x rho else (y,t) :: remove_assoc A x rho end. @@ -38,7 +38,7 @@ 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 + | (y,t) :: rho => if var_eq_dec x y then Some t else assoc A x rho end. @@ -126,34 +126,34 @@ Inductive in_context (A:formula) : list formula -> Prop := | 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 + | 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) + | 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' + | 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) + | 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) + | 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 : +Axiom context_prefix_trans : forall Gamma Gamma' Gamma'', - context_prefix Gamma Gamma' + context_prefix Gamma Gamma' -> context_prefix Gamma' Gamma'' -> context_prefix Gamma Gamma''. -Axiom Weakening : +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. @@ -170,20 +170,20 @@ Canonical Structure Universal := Build_Kripke universal_weakening. Axiom subst_commute : - forall A rho x t, + 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, + 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, + : 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 + 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 => @@ -192,21 +192,21 @@ Fixpoint universal_completeness (Gamma:context)(A:formula){struct A} (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 _ + | 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' + := + match A return forall rho, + (forall C Gamma', context_prefix Gamma Gamma' -> Gamma' ; subst_formula rho A |- C -> Gamma' |- C) - -> force _ rho Gamma A + -> force _ rho Gamma A with | Atom (p,t) as C => fun rho H => H _ Gamma (CtxPrefixRefl Gamma)(ProofAxiom _ _) diff --git a/test-suite/success/decl_mode.v b/test-suite/success/decl_mode.v index fede31a8..bc1757fd 100644 --- a/test-suite/success/decl_mode.v +++ b/test-suite/success/decl_mode.v @@ -8,10 +8,10 @@ proof. assume n:nat. per induction on n. suppose it is 0. - suffices (0=0) to show thesis. + 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)))). + have (div2 (double (S m))= div2 (S (S (double m)))). ~= (S (div2 (double m))). thus ~= (S m) by Hrec. end induction. @@ -56,12 +56,12 @@ proof. end proof. Qed. -Lemma main_thm_aux: forall n,even n -> +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)) + *** 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. @@ -75,14 +75,14 @@ proof. per induction on m. suppose it is 0. thus thesis. - suppose it is (S mm) and thesis for mm. + 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. @@ -95,7 +95,7 @@ proof. 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')) + ~= (S ( p' + p' * S p' + S p'* S p')) by plus_n_Sm. hence thesis . suppose it is 0. @@ -106,19 +106,19 @@ proof. 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) + 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. + 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) + 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)))) + ~= (double(double (double (div2 p * div2 p)))) by H3,main_thm_aux. - then H'':(div2 n * div2 n = double (div2 p * div2 p)) + 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''. @@ -137,8 +137,8 @@ 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). +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. @@ -147,7 +147,7 @@ proof. suppose it is (Zpos z). thus thesis. suppose it is (Zneg z). - have ((INR (Zabs_nat (Zneg z)) * INR (Zabs_nat (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)). @@ -160,19 +160,19 @@ Definition irrational (x:R):Prop := Theorem irrationnal_sqrt_2: irrational (sqrt (INR 2%nat)). proof. - let p:Z,q:nat be such that H:(q<>0%nat) + 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))) + 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. + ~= (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)). diff --git a/test-suite/success/dependentind.v b/test-suite/success/dependentind.v index 46dd0cb6..fe0165d0 100644 --- a/test-suite/success/dependentind.v +++ b/test-suite/success/dependentind.v @@ -1,5 +1,4 @@ -Require Import Coq.Program.Program. - +Require Import Coq.Program.Program Coq.Program.Equality. Variable A : Set. @@ -39,7 +38,7 @@ Delimit Scope context_scope with ctx. Arguments Scope snoc [context_scope]. -Notation " Γ ,, Ï„ " := (snoc Γ Ï„) (at level 25, t at next level, left associativity). +Notation " Γ , Ï„ " := (snoc Γ Ï„) (at level 25, Ï„ at next level, left associativity) : context_scope. Fixpoint conc (Δ Γ : ctx) : ctx := match Δ with @@ -47,60 +46,64 @@ Fixpoint conc (Δ Γ : ctx) : ctx := | snoc Δ' x => snoc (conc Δ' Γ) x end. -Notation " Γ ;; Δ " := (conc Δ Γ) (at level 25, left associativity) : context_scope. +Notation " Γ ; Δ " := (conc Δ Γ) (at level 25, left associativity) : context_scope. + +Reserved Notation " Γ ⊢ Ï„ " (at level 30, no associativity). + +Generalizable All Variables. Inductive term : ctx -> type -> Type := -| ax : forall Γ Ï„, term (snoc Γ Ï„) Ï„ -| weak : forall Γ Ï„, term Γ Ï„ -> forall Ï„', term (Γ ,, Ï„') Ï„ -| abs : forall Γ Ï„ Ï„', term (snoc Γ Ï„) Ï„' -> term Γ (Ï„ --> Ï„') -| app : forall Γ Ï„ Ï„', term Γ (Ï„ --> Ï„') -> term Γ Ï„ -> term Γ Ï„'. +| ax : `(Γ, Ï„ ⊢ Ï„) +| weak : `{Γ ⊢ Ï„ -> Γ, Ï„' ⊢ Ï„} +| abs : `{Γ, Ï„ ⊢ Ï„' -> Γ ⊢ Ï„ --> Ï„'} +| app : `{Γ ⊢ Ï„ --> Ï„' -> Γ ⊢ Ï„ -> Γ ⊢ Ï„'} + +where " Γ ⊢ Ï„ " := (term Γ Ï„) : type_scope. Hint Constructors term : lambda. Open Local Scope context_scope. -Notation " Γ |-- Ï„ " := (term Γ Ï„) (at level 0) : type_scope. +Ltac eqns := subst ; reverse ; simplify_dep_elim ; simplify_IH_hyps. -Lemma weakening : forall Γ Δ Ï„, term (Γ ;; Δ) Ï„ -> - forall Ï„', term (Γ ,, Ï„' ;; Δ) Ï„. -Proof with simpl in * ; reverse ; simplify_dep_elim ; simplify_IH_hyps ; eauto with lambda. +Lemma weakening : forall Γ Δ Ï„, Γ ; Δ ⊢ Ï„ -> + forall Ï„', Γ , Ï„' ; Δ ⊢ Ï„. +Proof with simpl in * ; eqns ; eauto with lambda. intros Γ Δ Ï„ H. dependent induction H. - destruct Δ... + destruct Δ as [|Δ Ï„'']... - destruct Δ... + destruct Δ as [|Δ Ï„'']... - destruct Δ... - apply abs... - - specialize (IHterm (Δ,, t,, Ï„)%ctx Γ0)... + destruct Δ as [|Δ Ï„'']... + apply abs. + specialize (IHterm Γ (Δ, Ï„'', Ï„))... - intro. - apply app with Ï„... -Qed. + intro. eapply app... +Defined. -Lemma exchange : forall Γ Δ α β Ï„, term (Γ,, α,, β ;; Δ) Ï„ -> term (Γ,, β,, α ;; Δ) Ï„. -Proof with simpl in * ; subst ; reverse ; simplify_dep_elim ; simplify_IH_hyps ; auto. +Lemma exchange : forall Γ Δ α β Ï„, term (Γ, α, β ; Δ) Ï„ -> term (Γ, β, α ; Δ) Ï„. +Proof with simpl in * ; eqns ; eauto. intros until 1. dependent induction H. - destruct Δ... + destruct Δ ; eqns. apply weak ; apply ax. apply ax. destruct Δ... - pose (weakening Γ0 (empty,, α))... + pose (weakening Γ (empty, α))... apply weak... - apply abs... - specialize (IHterm (Δ ,, Ï„))... + apply abs... + specialize (IHterm Γ (Δ, Ï„))... - eapply app with Ï„... -Save. + eapply app... +Defined. (** Example by Andrew Kenedy, uses simplification of the first component of dependent pairs. *) @@ -124,5 +127,5 @@ Inductive Ev : forall t, Exp t -> Exp t -> Prop := Ev (Fst e) e1. Lemma EvFst_inversion : forall t1 t2 (e:Exp (Prod t1 t2)) e1, Ev (Fst e) e1 -> exists e2, Ev e (Pair e1 e2). -intros t1 t2 e e1 ev. dependent destruction ev. exists e2 ; assumption. +intros t1 t2 e e1 ev. dependent destruction ev. exists e2 ; assumption. Qed. diff --git a/test-suite/success/destruct.v b/test-suite/success/destruct.v index 5aa78816..8013e1d3 100644 --- a/test-suite/success/destruct.v +++ b/test-suite/success/destruct.v @@ -1,11 +1,11 @@ (* Submitted by Robert Schneck *) -Parameter A B C D : Prop. +Parameters A B C D : Prop. Axiom X : A -> B -> C /\ D. Lemma foo : A -> B -> C. Proof. -intros. +intros. destruct X. (* Should find axiom X and should handle arguments of X *) assumption. assumption. @@ -45,9 +45,9 @@ Require Import List. Definition alist R := list (nat * R)%type. Section Properties. - Variables A : Type. - Variables a : A. - Variables E : alist A. + Variable A : Type. + Variable a : A. + Variable E : alist A. Lemma silly : E = E. Proof. @@ -55,3 +55,22 @@ Section Properties. Abort. End Properties. + +(* This used not to work before revision 11944 *) + +Goal forall P:(forall n, 0=n -> Prop), forall H: 0=0, P 0 H. +destruct H. +Abort. + +(* The calls to "destruct" below did not work before revision 12356 *) + +Variable A0:Type. +Variable P:A0->Type. +Require Import JMeq. +Goal forall a b (p:P a) (q:P b), + forall H:a = b, eq_rect a P p b H = q -> JMeq (existT _ a p) (existT _ b q). +intros. +destruct H. +destruct H0. +reflexivity. +Qed. diff --git a/test-suite/success/eauto.v b/test-suite/success/eauto.v index 26339d51..c7a2a6c9 100644 --- a/test-suite/success/eauto.v +++ b/test-suite/success/eauto.v @@ -56,5 +56,5 @@ Lemma simpl_plus_l_rr1 : (forall m p : Nat, plus' n m = plus' n p -> m = p) -> forall m p : Nat, S' (plus' n m) = S' (plus' n p) -> m = p. intros. - eauto. (* does EApply H *) + eauto. (* does EApply H *) Qed. diff --git a/test-suite/success/evars.v b/test-suite/success/evars.v index 082cbfbe..6423ad14 100644 --- a/test-suite/success/evars.v +++ b/test-suite/success/evars.v @@ -10,7 +10,7 @@ Definition c A (Q : (nat * A -> Prop) -> Prop) P := (* What does this test ? *) Require Import List. -Definition list_forall_bool (A : Set) (p : A -> bool) +Definition list_forall_bool (A : Set) (p : A -> bool) (l : list A) : bool := fold_right (fun a r => if p a then r else false) true l. @@ -109,21 +109,21 @@ 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 := +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' := +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 +(* 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) +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). @@ -133,14 +133,14 @@ 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 +(* 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, +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). @@ -198,10 +198,26 @@ 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 +(* An example from y-not that was failing in 8.2rc1 *) + +Fixpoint filter (A:nat->Set) (l:list (sigT A)) : list (sigT A) := + match l with + | nil => nil + | (existT k v)::l' => (existT _ k v):: (filter A l') + end. + +(* Bug #2000: used to raise Out of memory in 8.2 while it should fail by + lack of information on the conclusion of the type of j *) + +Goal True. +set (p:=fun j => j (or_intror _ (fun a:True => j (or_introl _ a)))) || idtac. +Abort. + +(* Remark: the following example stopped succeeding at some time in + the development of 8.2 but it works again (this was because 8.2 + algorithm was more general and did not exclude a solution that it + should have excluded for typing reason; handling of types and + backtracking is still to be done) *) Section S. Variables A B : nat -> Prop. @@ -209,4 +225,16 @@ Goal forall x : nat, A x -> B x. refine (fun x H => proj2 (_ x H) _). Abort. End S. -*) + +(* Check that constraints are taken into account by tactics that instantiate *) + +Lemma inj : forall n m, S n = S m -> n = m. +intros n m H. +eapply f_equal with (* should fail because ill-typed *) + (f := fun n => + match n return match n with S _ => nat | _ => unit end with + | S n => n + | _ => tt + end) in H +|| injection H. +Abort. diff --git a/test-suite/success/extraction.v b/test-suite/success/extraction.v index 74d87ffa..d3bdb1b6 100644 --- a/test-suite/success/extraction.v +++ b/test-suite/success/extraction.v @@ -9,10 +9,10 @@ Require Import Arith. Require Import List. -(**** A few tests for the extraction mechanism ****) +(**** A few tests for the extraction mechanism ****) -(* Ideally, we should monitor the extracted output - for changes, but this is painful. For the moment, +(* Ideally, we should monitor the extracted output + for changes, but this is painful. For the moment, we just check for failures of this script. *) (*** STANDARD EXAMPLES *) @@ -23,7 +23,7 @@ Definition idnat (x:nat) := x. Extraction idnat. (* let idnat x = x *) -Definition id (X:Type) (x:X) := x. +Definition id (X:Type) (x:X) := x. Extraction id. (* let id x = x *) Definition id' := id Set nat. Extraction id'. (* type id' = nat *) @@ -47,7 +47,7 @@ Extraction test5. Definition cf (x:nat) (_:x <= 0) := S x. Extraction NoInline cf. Definition test6 := cf 0 (le_n 0). -Extraction test6. +Extraction test6. (* let test6 = cf O *) Definition test7 := (fun (X:Set) (x:X) => x) nat. @@ -60,9 +60,9 @@ Definition d2 := d Set. Extraction d2. (* type d2 = __ d *) Definition d3 (x:d Set) := 0. Extraction d3. (* let d3 _ = O *) -Definition d4 := d nat. +Definition d4 := d nat. Extraction d4. (* type d4 = nat d *) -Definition d5 := (fun x:d Type => 0) Type. +Definition d5 := (fun x:d Type => 0) Type. Extraction d5. (* let d5 = O *) Definition d6 (x:d Type) := x. Extraction d6. (* type 'x d6 = 'x *) @@ -80,7 +80,7 @@ Definition test11 := let n := 0 in let p := S n in S p. Extraction test11. (* let test11 = S (S O) *) Definition test12 := forall x:forall X:Type, X -> X, x Type Type. -Extraction test12. +Extraction test12. (* type test12 = (__ -> __ -> __) -> __ *) @@ -115,14 +115,14 @@ Extraction test20. (** Simple inductive type and recursor. *) Extraction nat. -(* -type nat = - | O - | S of nat +(* +type nat = + | O + | S of nat *) Extraction sumbool_rect. -(* +(* let sumbool_rect f f0 = function | Left -> f __ | Right -> f0 __ @@ -134,7 +134,7 @@ Inductive c (x:nat) : nat -> Set := | refl : c x x | trans : forall y z:nat, c x y -> y <= z -> c x z. Extraction c. -(* +(* type c = | Refl | Trans of nat * nat * c @@ -150,7 +150,7 @@ Inductive Finite (U:Type) : Ensemble U -> Type := forall A:Ensemble U, Finite U A -> forall x:U, ~ A x -> Finite U (Add U A x). Extraction Finite. -(* +(* type 'u finite = | Empty_is_finite | Union_is_finite of 'u finite * 'u @@ -166,7 +166,7 @@ with forest : Set := | Cons : tree -> forest -> forest. Extraction tree. -(* +(* type tree = | Node of nat * forest and forest = @@ -178,7 +178,7 @@ Fixpoint tree_size (t:tree) : nat := match t with | Node a f => S (forest_size f) end - + with forest_size (f:forest) : nat := match f with | Leaf b => 1 @@ -186,7 +186,7 @@ Fixpoint tree_size (t:tree) : nat := end. Extraction tree_size. -(* +(* let rec tree_size = function | Node (a, f) -> S (forest_size f) and forest_size = function @@ -203,13 +203,13 @@ Definition test14 := tata 0. Extraction test14. (* let test14 x x0 x1 = Tata (O, x, x0, x1) *) Definition test15 := tata 0 1. -Extraction test15. +Extraction test15. (* let test15 x x0 = Tata (O, (S O), x, x0) *) Inductive eta : Type := eta_c : nat -> Prop -> nat -> Prop -> eta. Extraction eta_c. -(* +(* type eta = | Eta_c of nat * nat *) @@ -220,15 +220,15 @@ Definition test17 := eta_c 0 True. Extraction test17. (* let test17 x = Eta_c (O, x) *) Definition test18 := eta_c 0 True 0. -Extraction test18. +Extraction test18. (* let test18 _ = Eta_c (O, O) *) (** Example of singleton inductive type *) Inductive bidon (A:Prop) (B:Type) : Type := - tb : forall (x:A) (y:B), bidon A B. -Definition fbidon (A B:Type) (f:A -> B -> bidon True nat) + tb : forall (x:A) (y:B), bidon A B. +Definition fbidon (A B:Type) (f:A -> B -> bidon True nat) (x:A) (y:B) := f x y. Extraction bidon. (* type 'b bidon = 'b *) @@ -252,11 +252,11 @@ Extraction fbidon2. Inductive test_0 : Prop := ctest0 : test_0 with test_1 : Set := - ctest1 : test_0 -> test_1. + ctest1 : test_0 -> test_1. Extraction test_0. (* test0 : logical inductive *) -Extraction test_1. -(* +Extraction test_1. +(* type test1 = | Ctest1 *) @@ -277,19 +277,19 @@ Inductive tp1 : Type := with tp2 : Type := T' : tp1 -> tp2. Extraction tp1. -(* +(* type tp1 = | T of __ * tp2 and tp2 = | T' of tp1 -*) +*) Inductive tp1bis : Type := Tbis : tp2bis -> tp1bis with tp2bis : Type := T'bis : forall (C:Set) (c:C), tp1bis -> tp2bis. Extraction tp1bis. -(* +(* type tp1bis = | Tbis of tp2bis and tp2bis = @@ -344,8 +344,8 @@ intros. exact n. Qed. Extraction oups. -(* -let oups h0 = +(* +let oups h0 = match Obj.magic h0 with | Nil -> h0 | Cons0 (n, l) -> n @@ -357,7 +357,7 @@ let oups h0 = Definition horibilis (b:bool) := if b as b return (if b then Type else nat) then Set else 0. Extraction horibilis. -(* +(* let horibilis = function | True -> Obj.magic __ | False -> Obj.magic O @@ -370,8 +370,8 @@ Definition natbool (b:bool) := if b then nat else bool. Extraction natbool. (* type natbool = __ *) Definition zerotrue (b:bool) := if b as x return natbool x then 0 else true. -Extraction zerotrue. -(* +Extraction zerotrue. +(* let zerotrue = function | True -> Obj.magic O | False -> Obj.magic True @@ -383,7 +383,7 @@ Definition natTrue (b:bool) := if b return Type then nat else True. Definition zeroTrue (b:bool) := if b as x return natProp x then 0 else True. Extraction zeroTrue. -(* +(* let zeroTrue = function | True -> Obj.magic O | False -> Obj.magic __ @@ -393,7 +393,7 @@ Definition natTrue2 (b:bool) := if b return Type then nat else True. Definition zeroprop (b:bool) := if b as x return natTrue x then 0 else I. Extraction zeroprop. -(* +(* let zeroprop = function | True -> Obj.magic O | False -> Obj.magic __ @@ -410,8 +410,8 @@ Extraction test21. Definition test22 := (fun f:forall X:Type, X -> X => (f nat 0, f bool true)) (fun (X:Type) (x:X) => x). -Extraction test22. -(* let test22 = +Extraction test22. +(* let test22 = let f = fun x -> x in Pair ((f O), (f True)) *) (* still ok via optim beta -> let *) @@ -461,8 +461,8 @@ Extraction f_normal. (* inductive with magic needed *) Inductive Boite : Set := - boite : forall b:bool, (if b then nat else (nat * nat)%type) -> Boite. -Extraction Boite. + boite : forall b:bool, (if b then nat else (nat * nat)%type) -> Boite. +Extraction Boite. (* type boite = | Boite of bool * __ @@ -482,8 +482,8 @@ Definition test_boite (B:Boite) := | boite true n => n | boite false n => fst n + snd n end. -Extraction test_boite. -(* +Extraction test_boite. +(* let test_boite = function | Boite (b0, n) -> (match b0 with @@ -494,23 +494,23 @@ let test_boite = function (* singleton inductive with magic needed *) Inductive Box : Type := - box : forall A:Set, A -> Box. + box : forall A:Set, A -> Box. Extraction Box. (* type box = __ *) -Definition box1 := box nat 0. +Definition box1 := box nat 0. Extraction box1. (* let box1 = Obj.magic O *) (* applied constant, magic needed *) Definition idzarb (b:bool) (x:if b then nat else bool) := x. Definition zarb := idzarb true 0. -Extraction NoInline idzarb. -Extraction zarb. +Extraction NoInline idzarb. +Extraction zarb. (* let zarb = Obj.magic idzarb True (Obj.magic O) *) (** function of variable arity. *) -(** Fun n = nat -> nat -> ... -> nat *) +(** Fun n = nat -> nat -> ... -> nat *) Fixpoint Fun (n:nat) : Set := match n with @@ -532,20 +532,20 @@ Fixpoint proj (k n:nat) {struct n} : Fun n := | O => fun x => Const x n | S k => fun x => proj k n end - end. + end. Definition test_proj := proj 2 4 0 1 2 3. -Eval compute in test_proj. +Eval compute in test_proj. -Recursive Extraction test_proj. +Recursive Extraction test_proj. -(*** TO SUM UP: ***) +(*** TO SUM UP: ***) (* Was previously producing a "test_extraction.ml" *) -Recursive Extraction +Recursive Extraction idnat id id' test2 test3 test4 test5 test6 test7 d d2 d3 d4 d5 d6 test8 id id' test9 test10 test11 test12 test13 test19 test20 nat sumbool_rect c Finite tree @@ -581,7 +581,7 @@ Recursive Extraction zerotrue zeroTrue zeroprop test21 test22 test23 f f_prop f_arity f_normal Boite boite1 boite2 test_boite Box box1 zarb test_proj. - + (*** Finally, a test more focused on everyday's life situations ***) diff --git a/test-suite/success/fix.v b/test-suite/success/fix.v index 78b01f3e..be4e0684 100644 --- a/test-suite/success/fix.v +++ b/test-suite/success/fix.v @@ -47,10 +47,10 @@ Fixpoint maxVar (e : rExpr) : rNat := Require Import Streams. -Definition decomp (s:Stream nat) : Stream nat := +Definition decomp (s:Stream nat) : Stream nat := match s with Cons _ s => s end. -CoFixpoint bx0 : Stream nat := Cons 0 bx1 +CoFixpoint bx0 : Stream nat := Cons 0 bx1 with bx1 : Stream nat := Cons 1 bx0. Lemma bx0bx : decomp bx0 = bx1. diff --git a/test-suite/success/hyps_inclusion.v b/test-suite/success/hyps_inclusion.v index 21bfc075..af81e53d 100644 --- a/test-suite/success/hyps_inclusion.v +++ b/test-suite/success/hyps_inclusion.v @@ -8,7 +8,7 @@ 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 + end, when the proof is completed, the section variable recovers its original type and all is correct for Typeops) *) Section A. @@ -16,9 +16,9 @@ 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 +(* next tactic was failing wrt bug #1325 because type-checking the goal detected a syntactically different type for the section variable H *) -case 0. +case 0. Reset A. (* Variant with polymorphic inductive types for bug #1325 *) diff --git a/test-suite/success/implicit.v b/test-suite/success/implicit.v index 9034d6a6..59e1a935 100644 --- a/test-suite/success/implicit.v +++ b/test-suite/success/implicit.v @@ -1,3 +1,5 @@ +(* Testing the behavior of implicit arguments *) + (* Implicit on section variables *) Set Implicit Arguments. @@ -12,15 +14,53 @@ Infix "#" := op (at level 70). Check (forall x : A, x # x). (* Example submitted by Christine *) -Record stack : Type := + +Record stack : Type := {type : Set; elt : type; empty : type -> bool; proof : empty elt = true}. Check (forall (type : Set) (elt : type) (empty : type -> bool), empty elt = true -> stack). +(* Nested sections and manual/automatic implicit arguments *) + +Variable op' : forall A : Set, A -> A -> Set. +Variable op'' : forall A : Set, A -> A -> Set. + +Section B. + +Definition eq1 := fun (A:Type) (x y:A) => x=y. +Definition eq2 := fun (A:Type) (x y:A) => x=y. +Definition eq3 := fun (A:Type) (x y:A) => x=y. + +Implicit Arguments op' []. +Global Implicit Arguments op'' []. + +Implicit Arguments eq2 []. +Global Implicit Arguments eq3 []. + +Check (op 0 0). +Check (op' nat 0 0). +Check (op'' nat 0 0). +Check (eq1 0 0). +Check (eq2 nat 0 0). +Check (eq3 nat 0 0). + +End B. + +Check (op 0 0). +Check (op' 0 0). +Check (op'' nat 0 0). +Check (eq1 0 0). +Check (eq2 0 0). +Check (eq3 nat 0 0). + End Spec. +Check (eq1 0 0). +Check (eq2 0 0). +Check (eq3 nat 0 0). + (* Example submitted by Frédéric (interesting in v8 syntax) *) Parameter f : nat -> nat * nat. @@ -42,7 +82,7 @@ Inductive P n : nat -> Prop := c : P n n. Require Import List. Fixpoint plus n m {struct n} := - match n with + match n with | 0 => m | S p => S (plus p m) end. diff --git a/test-suite/success/import_lib.v b/test-suite/success/import_lib.v index c3dc2fc6..fcedb2b1 100644 --- a/test-suite/success/import_lib.v +++ b/test-suite/success/import_lib.v @@ -1,8 +1,8 @@ Definition le_trans := 0. -Module Test_Read. - Module M. +Module Test_Read. + Module M. Require Le. (* Reading without importing *) Check Le.le_trans. @@ -12,7 +12,7 @@ Module Test_Read. Qed. End M. - Check Le.le_trans. + Check Le.le_trans. Lemma th0 : le_trans = 0. reflexivity. @@ -32,84 +32,84 @@ Definition le_decide := 1. (* from Arith/Compare *) Definition min := 0. (* from Arith/Min *) Module Test_Require. - + Module M. Require Import Compare. (* Imports Min as well *) - + Lemma th1 : le_decide = le_decide. reflexivity. Qed. - + Lemma th2 : min = min. reflexivity. Qed. - + End M. - + (* Checks that Compare and List are loaded *) Check Compare.le_decide. Check Min.min. - - + + (* Checks that Compare and List are _not_ imported *) Lemma th1 : le_decide = 1. reflexivity. Qed. - + Lemma th2 : min = 0. reflexivity. Qed. - + (* It should still be the case after Import M *) Import M. - + Lemma th3 : le_decide = 1. reflexivity. Qed. - + Lemma th4 : min = 0. reflexivity. Qed. -End Test_Require. +End Test_Require. (****************************************************************) Module Test_Import. Module M. Import Compare. (* Imports Min as well *) - + Lemma th1 : le_decide = le_decide. reflexivity. Qed. - + Lemma th2 : min = min. reflexivity. Qed. - + End M. - + (* Checks that Compare and List are loaded *) Check Compare.le_decide. Check Min.min. - - + + (* Checks that Compare and List are _not_ imported *) Lemma th1 : le_decide = 1. reflexivity. Qed. - + Lemma th2 : min = 0. reflexivity. Qed. - + (* It should still be the case after Import M *) Import M. - + Lemma th3 : le_decide = 1. reflexivity. Qed. - + Lemma th4 : min = 0. reflexivity. Qed. diff --git a/test-suite/success/induct.v b/test-suite/success/induct.v index 2aec6e9b..8e1a8d18 100644 --- a/test-suite/success/induct.v +++ b/test-suite/success/induct.v @@ -5,7 +5,8 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* Teste des definitions inductives imbriquees *) + +(* Test des definitions inductives imbriquees *) Require Import List. @@ -15,3 +16,28 @@ Inductive X : Set := Inductive Y : Set := cons2 : list (Y * Y) -> Y. +(* Test inductive types with local definitions *) + +Inductive eq1 : forall A:Type, let B:=A in A -> Prop := + refl1 : eq1 True I. + +Check + fun (P : forall A : Type, let B := A in A -> Type) (f : P True I) (A : Type) => + let B := A in + fun (a : A) (e : eq1 A a) => + match e in (eq1 A0 B0 a0) return (P A0 a0) with + | refl1 => f + end. + +Inductive eq2 (A:Type) (a:A) + : forall B C:Type, let D:=(A*B*C)%type in D -> Prop := + refl2 : eq2 A a unit bool (a,tt,true). + +(* Check that induction variables are cleared even with in clause *) + +Lemma foo : forall n m : nat, n + m = n + m. +Proof. + intros; induction m as [|m] in n |- *. + auto. + auto. +Qed. diff --git a/test-suite/success/ltac.v b/test-suite/success/ltac.v index 757cf6a4..dfa41c82 100644 --- a/test-suite/success/ltac.v +++ b/test-suite/success/ltac.v @@ -3,7 +3,7 @@ (* Submitted by Pierre Crégut *) (* Checks substitution of x *) Ltac f x := unfold x in |- *; idtac. - + Lemma lem1 : 0 + 0 = 0. f plus. reflexivity. @@ -25,7 +25,7 @@ U. Qed. (* Check that Match giving non-tactic arguments are evaluated at Let-time *) - + Ltac B := let y := (match goal with | z:_ |- _ => z end) in @@ -152,6 +152,7 @@ Abort. Ltac afi tac := intros; tac. Goal 1 = 2. afi ltac:auto. +Abort. (* Tactic Notation avec listes *) @@ -179,8 +180,8 @@ Abort. (* Check second-order pattern unification *) Ltac to_exist := - match goal with - |- forall x y, @?P x y => + 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. @@ -201,7 +202,7 @@ Abort. (* Utilisation de let rec sans arguments *) -Ltac is := +Ltac is := let rec i := match goal with |- ?A -> ?B => intro; i | _ => idtac end in i. @@ -220,3 +221,25 @@ Z1 O. Z2 ltac:O. exact I. Qed. + +(* Illegal application used to make Ltac loop. *) + +Section LtacLoopTest. + Ltac f x := idtac. + Goal True. + Timeout 1 try f()(). + Abort. +End LtacLoopTest. + +(* Test binding of open terms *) + +Ltac test_open_match z := + match z with + (forall y x, ?h = 0) => assert (forall x y, h = x + y) + end. + +Goal True. +test_open_match (forall z y, y + z = 0). +reflexivity. +apply I. +Qed. diff --git a/test-suite/success/mutual_ind.v b/test-suite/success/mutual_ind.v index 463efed3..f63dfc38 100644 --- a/test-suite/success/mutual_ind.v +++ b/test-suite/success/mutual_ind.v @@ -9,7 +9,7 @@ Require Export List. - Record signature : Type := + Record signature : Type := {sort : Set; sort_beq : sort -> sort -> bool; sort_beq_refl : forall f : sort, true = sort_beq f f; @@ -20,14 +20,14 @@ Require Export List. fsym_beq_refl : forall f : fsym, true = fsym_beq f f; fsym_beq_eq : forall f1 f2 : fsym, true = fsym_beq f1 f2 -> f1 = f2}. - + Variable F : signature. Definition vsym := (sort F * nat)%type. Definition vsym_sort := fst (A:=sort F) (B:=nat). Definition vsym_nat := snd (A:=sort F) (B:=nat). - + Inductive term : sort F -> Set := | term_var : forall v : vsym, term (vsym_sort v) diff --git a/test-suite/success/parsing.v b/test-suite/success/parsing.v index d1b679d5..3d06d1d0 100644 --- a/test-suite/success/parsing.v +++ b/test-suite/success/parsing.v @@ -2,7 +2,7 @@ Section A. Notation "*" := O (at level 8). Notation "**" := O (at level 99). Notation "***" := O (at level 9). -End A. +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 index 28d0bd55..72f84052 100644 --- a/test-suite/success/pattern.v +++ b/test-suite/success/pattern.v @@ -5,3 +5,45 @@ 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. +Abort. + +(* Check use of occurrences in hypotheses for a reduction tactic such + as pattern *) + +(* Did not work in 8.2 *) +Goal 0=0->True. +intro H. +pattern 0 in H at 2. +set (f n := 0 = n) in H. (* check pattern worked correctly *) +Abort. + +(* Syntactic variant which was working in 8.2 *) +Goal 0=0->True. +intro H. +pattern 0 at 2 in H. +set (f n := 0 = n) in H. (* check pattern worked correctly *) +Abort. + +(* Ambiguous occurrence selection *) +Goal 0=0->True. +intro H. +pattern 0 at 1 in H at 2 || exact I. (* check pattern fails *) +Qed. + +(* Ambiguous occurrence selection *) +Goal 0=1->True. +intro H. +pattern 0, 1 in H at 1 2 || exact I. (* check pattern fails *) +Qed. + +(* Occurrence selection shared over hypotheses is difficult to advocate and + hence no longer allowed *) +Goal 0=1->1=0->True. +intros H1 H2. +pattern 0 at 1, 1 in H1, H2 || exact I. (* check pattern fails *) +Qed. + +(* Test catching of reduction tactics errors (was not the case in 8.2) *) +Goal eq_refl 0 = eq_refl 0. +pattern 0 at 1 || reflexivity. +Qed. diff --git a/test-suite/success/refine.v b/test-suite/success/refine.v index b654277c..4d743a6d 100644 --- a/test-suite/success/refine.v +++ b/test-suite/success/refine.v @@ -7,7 +7,7 @@ exists y; auto. Save test1. Goal exists x : nat, x = 0. - refine (let y := 0 + 0 in ex_intro _ (y + y) _). + refine (let y := 0 + 0 in ex_intro _ (y + y) _). auto. Save test2. @@ -79,7 +79,7 @@ Abort. (* Used to failed with error not clean *) Definition div : - forall x:nat, (forall y:nat, forall n:nat, {q:nat | y = q*n}) -> + forall x:nat, (forall y:nat, forall n:nat, {q:nat | y = q*n}) -> forall n:nat, {q:nat | x = q*n}. refine (fun m div_rec n => @@ -94,7 +94,7 @@ Abort. Goal forall f : forall a (H:a=a), Prop, - (forall a (H:a = a :> nat), f a H -> True /\ True) -> + (forall a (H:a = a :> nat), f a H -> True /\ True) -> True. intros. refine (@proj1 _ _ (H 0 _ _)). @@ -105,13 +105,13 @@ Abort. 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/success/replace.v b/test-suite/success/replace.v index 94b75c7f..0b112937 100644 --- a/test-suite/success/replace.v +++ b/test-suite/success/replace.v @@ -5,7 +5,7 @@ Undo. intros x H H0. replace x with 0. Undo. -replace x with 0 in |- *. +replace x with 0 in |- *. Undo. replace x with 1 in *. Undo. @@ -22,3 +22,11 @@ replace x with 0 in H,H0 |- * . Undo. Admitted. +(* This failed at some point when "replace" started to support arguments + with evars but "abstract" did not supported any evars even defined ones *) + +Class U. +Lemma l (u : U) (f : U -> nat) (H : 0 = f u) : f u = 0. +replace (f _) with 0 by abstract apply H. +reflexivity. +Qed. diff --git a/test-suite/success/rewrite.v b/test-suite/success/rewrite.v index 86e55922..3bce52fe 100644 --- a/test-suite/success/rewrite.v +++ b/test-suite/success/rewrite.v @@ -38,3 +38,73 @@ Goal forall n, 0 + n = n -> True. intros n H. rewrite plus_0_l in H. Abort. + +(* Rewrite dependent proofs from left-to-right *) + +Lemma l1 : + forall x y (H:x = y:>nat) (P:forall x y, x=y -> Type), P x y H -> P x y H. +intros x y H P H0. +rewrite H. +rewrite H in H0. +assumption. +Qed. + +(* Rewrite dependent proofs from right-to-left *) + +Lemma l2 : + forall x y (H:x = y:>nat) (P:forall x y, x=y -> Type), P x y H -> P x y H. +intros x y H P H0. +rewrite <- H. +rewrite <- H in H0. +assumption. +Qed. + +(* Check rewriting dependent proofs with non-symmetric equalities *) + +Lemma l3:forall x (H:eq_true x) (P:forall x, eq_true x -> Type), P x H -> P x H. +intros x H P H0. +rewrite H. +rewrite H in H0. +assumption. +Qed. + +(* Dependent rewrite *) + +Require Import JMeq. + +Goal forall A B (a:A) (b:B), JMeq a b -> JMeq b a -> True. +inversion 1; (* Goal is now [JMeq a a -> True] *) dependent rewrite H3. +Undo. +intros; inversion H; dependent rewrite H4 in H0. +Undo. +intros; inversion H; dependent rewrite <- H4 in H0. +Abort. + +(* Test conversion between terms with evars that both occur in K-redexes and + are elsewhere solvable. + + This is quite an artificial example, but it used to work in 8.2. + + Since rewrite supports conversion on terms without metas, it + was successively unifying (id 0 ?y) and 0 where ?y was not a + meta but, because coming from a "_", an evar. + + After commit r12440 which unified the treatment of metas and + evars, it stopped to work. Chung-Kil Hur's Heq package used + this feature. Solved in r13... +*) + +Parameter g : nat -> nat -> nat. +Definition K (x y:nat) := x. + +Goal (forall y, g y (K 0 y) = 0) -> g 0 0 = 0. +intros. +rewrite (H _). +reflexivity. +Qed. + +Goal (forall y, g (K 0 y) y = 0) -> g 0 0 = 0. +intros. +rewrite (H _). +reflexivity. +Qed. diff --git a/test-suite/success/setoid_ring_module.v b/test-suite/success/setoid_ring_module.v index e947c6d9..2d9e85b5 100644 --- a/test-suite/success/setoid_ring_module.v +++ b/test-suite/success/setoid_ring_module.v @@ -11,11 +11,11 @@ Parameters (Coef:Set)(c0 c1 : Coef) (ceq_refl : forall x, ceq x x). -Add Relation Coef ceq +Add Relation Coef ceq reflexivity proved by ceq_refl symmetry proved by ceq_sym transitivity proved by ceq_trans as ceq_relation. - + Add Morphism cadd with signature ceq ==> ceq ==> ceq as cadd_Morphism. Admitted. diff --git a/test-suite/success/setoid_test.v b/test-suite/success/setoid_test.v index be5999df..033b3f48 100644 --- a/test-suite/success/setoid_test.v +++ b/test-suite/success/setoid_test.v @@ -124,7 +124,7 @@ Goal forall (f : Prop -> Prop) (Q : (nat -> Prop) -> Prop) (H : forall (h : nat -> Prop), Q (fun x : nat => f (h x)) <-> True) - (h:nat -> Prop), + (h:nat -> Prop), Q (fun x : nat => f (Q (fun b : nat => f (h x)))) <-> True. intros f0 Q H. setoid_rewrite H. diff --git a/test-suite/success/setoid_test2.v b/test-suite/success/setoid_test2.v index b89787bb..6baf7970 100644 --- a/test-suite/success/setoid_test2.v +++ b/test-suite/success/setoid_test2.v @@ -205,7 +205,7 @@ Theorem test6: rewrite H. assumption. Qed. - + Theorem test7: forall E1 E2 y y', (eqS1 E1 E2) -> (eqS2 y y') -> (f_test6 (g_test6 (h_test6 E2))) -> @@ -228,7 +228,7 @@ Add Morphism f_test8 : f_compat_test8. Admitted. 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'. - + (*CSC: for test8 to be significant I want to choose the setoid (S1_test8, eqS1_test8'). However this does not happen and there is still no syntax for it ;-( *) diff --git a/test-suite/success/setoid_test_function_space.v b/test-suite/success/setoid_test_function_space.v index ead93d91..381cda2c 100644 --- a/test-suite/success/setoid_test_function_space.v +++ b/test-suite/success/setoid_test_function_space.v @@ -9,11 +9,11 @@ Hint Unfold feq. Lemma feq_refl: forall f, f =f f. intuition. Qed. - + Lemma feq_sym: forall f g, f =f g-> g =f f. intuition. Qed. - + Lemma feq_trans: forall f g h, f =f g-> g =f h -> f =f h. unfold feq. intuition. rewrite H. @@ -22,7 +22,7 @@ Qed. End feq. Infix "=f":= feq (at level 80, right associativity). 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). @@ -30,7 +30,7 @@ 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 nat nat) ==> iff as K_ext1. intuition. apply (K_ext H0 H). intuition. assert (y =f x);auto. apply (K_ext H0 H1). diff --git a/test-suite/success/simpl.v b/test-suite/success/simpl.v index b4de4932..271e6ef7 100644 --- a/test-suite/success/simpl.v +++ b/test-suite/success/simpl.v @@ -2,12 +2,12 @@ (* (cf bug #1031) *) Inductive tree : Set := -| node : nat -> forest -> tree +| node : nat -> forest -> tree with forest : Set := -| leaf : forest -| cons : tree -> forest -> forest +| leaf : forest +| cons : tree -> forest -> forest . -Definition copy_of_compute_size_forest := +Definition copy_of_compute_size_forest := fix copy_of_compute_size_forest (f:forest) : nat := match f with | leaf => 1 diff --git a/test-suite/success/specialize.v b/test-suite/success/specialize.v index 4929ae4c..57837321 100644 --- a/test-suite/success/specialize.v +++ b/test-suite/success/specialize.v @@ -2,7 +2,7 @@ Goal forall a b c : nat, a = b -> b = c -> forall d, a+d=c+d. intros. -(* "compatibility" mode: specializing a global name +(* "compatibility" mode: specializing a global name means a kind of generalize *) specialize trans_equal. intros _. diff --git a/test-suite/success/unfold.v b/test-suite/success/unfold.v index 35910011..0a1d4657 100644 --- a/test-suite/success/unfold.v +++ b/test-suite/success/unfold.v @@ -8,7 +8,7 @@ (* Test le Hint Unfold sur des var locales *) Section toto. -Let EQ := eq. +Let EQ := @eq. Goal EQ nat 0 0. Hint Unfold EQ. auto. diff --git a/test-suite/success/unification.v b/test-suite/success/unification.v index 91ee18ea..ddf122e8 100644 --- a/test-suite/success/unification.v +++ b/test-suite/success/unification.v @@ -1,15 +1,15 @@ (* Test patterns unification *) -Lemma l1 : (forall P, (exists x:nat, P x) -> False) +Lemma l1 : (forall P, (exists x:nat, P x) -> False) -> forall P, (exists x:nat, P x /\ P x) -> False. Proof. intros; apply (H _ H0). Qed. Lemma l2 : forall A:Set, forall Q:A->Set, - (forall (P: forall x:A, Q x -> Prop), - (exists x:A, exists y:Q x, P x y) -> False) - -> forall (P: forall x:A, Q x -> Prop), + (forall (P: forall x:A, Q x -> Prop), + (exists x:A, exists y:Q x, P x y) -> False) + -> forall (P: forall x:A, Q x -> Prop), (exists x:A, exists y:Q x, P x y /\ P x y) -> False. Proof. intros; apply (H _ H0). @@ -43,7 +43,7 @@ Check (fun _h1 => (zenon_notall nat _ (fun _T_0 => Note that the example originally came from a non re-typable pretty-printed term (the checked term is actually re-printed the - same form it is checked). + same form it is checked). *) Set Implicit Arguments. @@ -73,10 +73,10 @@ Qed. (* Test unification modulo eta-expansion (if possible) *) -(* In this example, two instances for ?P (argument of hypothesis H) can be +(* 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 + 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 @@ -92,7 +92,7 @@ Qed. (* Test instanciation of evars by unification *) -Goal (forall x, 0 * x = 0 -> True) -> True. +Goal (forall x, 0 + x = 0 -> True) -> True. intros; eapply H. rewrite <- plus_n_Sm. (* should refine ?x with S ?x' *) Abort. @@ -126,3 +126,13 @@ intros. exists (fun n => match n with O => a | S n' => f' n' end). constructor. Qed. + +(* Check use of types in unification (see Andrej Bauer's mail on + coq-club, June 1 2009; it did not work in 8.2, probably started to + work after Sozeau improved support for the use of types in unification) *) + +Goal (forall (A B : Set) (f : A -> B), (fun x => f x) = f) -> + forall (A B C : Set) (g : (A -> B) -> C) (f : A -> B), g (fun x => f x) = g f. +Proof. + intros. + rewrite H. diff --git a/test-suite/success/univers.v b/test-suite/success/univers.v index 3c2c0883..469cbeb7 100644 --- a/test-suite/success/univers.v +++ b/test-suite/success/univers.v @@ -29,9 +29,9 @@ Inductive dep_eq : forall X : Type, X -> X -> Prop := forall (A : Type) (B : A -> Type), let T := forall x : A, B x in forall (f g : T) (x : A), dep_eq (B x) (f x) (g x) -> dep_eq T f g. - + Require Import Relations. - + Theorem dep_eq_trans : forall X : Type, transitive X (dep_eq X). Proof. unfold transitive in |- *. @@ -51,7 +51,7 @@ Abort. Especially, universe refreshing was not done for "set/pose" *) -Lemma ind_unsec : forall Q : nat -> Type, True. +Lemma ind_unsec : forall Q : nat -> Type, True. intro. set (C := forall m, Q m -> Q m). exact I. |