diff options
Diffstat (limited to 'test-suite/success')
63 files changed, 553 insertions, 554 deletions
diff --git a/test-suite/success/Abstract.v b/test-suite/success/Abstract.v index fc8800a56..ffd50f6ef 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 8e613dcaa..c1405cf91 100644 --- a/test-suite/success/AdvancedCanonicalStructure.v +++ b/test-suite/success/AdvancedCanonicalStructure.v @@ -54,7 +54,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 +63,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 +95,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 +140,5 @@ End type_reification. - + diff --git a/test-suite/success/AdvancedTypeClasses.v b/test-suite/success/AdvancedTypeClasses.v index e6950a2a1..219a8a755 100644 --- a/test-suite/success/AdvancedTypeClasses.v +++ b/test-suite/success/AdvancedTypeClasses.v @@ -2,7 +2,7 @@ Open Scope type_scope. Section type_reification. -Inductive term :Type := +Inductive term :Type := Fun : term -> term -> term | Prod : term -> term -> term | Bool : term @@ -11,19 +11,19 @@ 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. Class interp_pair (abs : Type) := - { repr : term; + { repr : term; link: abs = interp repr }. Implicit Arguments repr [[interp_pair]]. @@ -52,7 +52,7 @@ Instance ProdCan `(interp_pair a, interp_pair b) : interp_pair (a * b) := Instance FunCan `(interp_pair a, interp_pair b) : interp_pair (a -> b) := { link := fun_interp }. -Instance BoolCan : interp_pair bool := +Instance BoolCan : interp_pair bool := { repr := Bool ; link := refl_equal _ }. Instance VarCan : interp_pair x | 10 := { repr := Var x ; link := refl_equal _ }. diff --git a/test-suite/success/Case12.v b/test-suite/success/Case12.v index f6a0d5780..729ab824f 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 8431880d1..69fca48e2 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 061e136e0..66af9e0d3 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/Cases.v b/test-suite/success/Cases.v index ccd92f696..e63972ce1 100644 --- a/test-suite/success/Cases.v +++ b/test-suite/success/Cases.v @@ -256,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 @@ -523,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). @@ -613,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) @@ -628,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. **********) @@ -957,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 @@ -1072,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. @@ -1180,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 @@ -1188,7 +1188,7 @@ Type Type match compare 0 0 with - + (* k<i *) | inleft (left _) => 0 (* k=i *) | inleft _ => 0 (* k>i *) | inright _ => 0 @@ -1375,7 +1375,7 @@ Type | var, var => True | oper op1 l1, oper op2 l2 => False | _, _ => False - end. + end. Reset LTERM. @@ -1661,7 +1661,7 @@ Type | Cons a x, Cons b y => V4 a x b y end). - + (* ===================================== *) Inductive Eqlong : @@ -1725,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 63957885c..297218433 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 @@ -488,7 +488,7 @@ Require Import List. Inductive nt := E. Definition root := E. -Inductive ctor : list nt -> nt -> Type := +Inductive ctor : list nt -> nt -> Type := Plus : ctor (cons E (cons E nil)) E. Inductive term : nt -> Type := diff --git a/test-suite/success/Discriminate.v b/test-suite/success/Discriminate.v index b57c54781..dffad3230 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 index e31135c2f..d6e17f30d 100644 --- a/test-suite/success/Equations.v +++ b/test-suite/success/Equations.v @@ -3,7 +3,7 @@ Require Import Program. Equations neg (b : bool) : bool := neg true := false ; neg false := true. - + Eval compute in neg. Require Import Coq.Lists.List. @@ -30,7 +30,7 @@ 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) + (a :: v) ++ l := a :: (v ++ l) where " x ++ y " := (app x y). @@ -73,7 +73,7 @@ Require Import Bvector. Implicit Arguments Vnil [[A]]. Implicit Arguments Vcons [[A] [n]]. -Equations vhead {A n} (v : vector A (S n)) : A := +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) := @@ -109,7 +109,7 @@ Fixpoint Below_vector (P : ΠA n, vector A n -> Type) A n (v : vector A n) : Ty 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 := +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). @@ -125,7 +125,7 @@ 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) := +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 := @@ -159,7 +159,7 @@ Notation " x ~= y " := (@JMeq _ x _ y) (at level 70, no associativity). 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 := @@ -173,7 +173,7 @@ Section Univ. | ubool | unat | uarrow (from:univ) (to:univ). Equations interp (u : univ) : Type := - interp ubool := bool ; interp unat := nat ; + interp ubool := bool ; interp unat := nat ; interp (uarrow from to) := interp from -> interp to. Equations foo (u : univ) (el : interp u) : interp u := @@ -238,7 +238,7 @@ 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 nth. Print Assumptions tabulate. Extraction vlast. diff --git a/test-suite/success/Field.v b/test-suite/success/Field.v index 6fb922b0f..ab90dc88a 100644 --- a/test-suite/success/Field.v +++ b/test-suite/success/Field.v @@ -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. diff --git a/test-suite/success/Fixpoint.v b/test-suite/success/Fixpoint.v index cf8210733..4130a16ca 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. diff --git a/test-suite/success/Fourier.v b/test-suite/success/Fourier.v index 2d184fef1..b63bead47 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 1c3e56f20..b17adef67 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/Hints.v b/test-suite/success/Hints.v index 98b5992ad..a8cc7f745 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. + 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. diff --git a/test-suite/success/Inductive.v b/test-suite/success/Inductive.v index 724ba502c..203fbbb77 100644 --- a/test-suite/success/Inductive.v +++ b/test-suite/success/Inductive.v @@ -13,7 +13,7 @@ Inductive Y : Set := Inductive eq1 : forall A:Type, let B:=A in A -> Prop := refl1 : eq1 True I. -Check +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) => @@ -35,7 +35,7 @@ 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 | I x0 => f x0 @@ -48,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 867d73746..c5cd7380a 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 b08ffcc32..71e53191b 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,5 @@ 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. diff --git a/test-suite/success/LegacyField.v b/test-suite/success/LegacyField.v index d53e40108..fada3bd54 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 545b8aeb8..4c790680d 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 84ff2608a..1bff74933 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. diff --git a/test-suite/success/Omega0.v b/test-suite/success/Omega0.v index accaec41e..b8f8660e9 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 54b13702a..c4d086a34 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 bb800b7a0..f4996734b 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 index 1898853f6..a6a0da878 100644 --- a/test-suite/success/ProgramWf.v +++ b/test-suite/success/ProgramWf.v @@ -16,7 +16,7 @@ Print merge. Require Import ZArith. -Print Zlt. +Print Zlt. Require Import Zwf. Print Zwf. @@ -28,7 +28,7 @@ Program Fixpoint Zwfrec (n m : Z) {measure (n + m) (Zwf 0)} : Z := | _ => 0 end. -Next Obligation. +Next Obligation. red. Admitted. Close Scope Z_scope. @@ -52,7 +52,7 @@ Print merge_one. Eval cbv delta [merge_one] beta zeta in merge_one. Import WfExtensionality. -Lemma merge_unfold n m : merge n m = +Lemma merge_unfold n m : merge n m = match n with | 0 => 0 | S n' => merge n' m @@ -66,7 +66,7 @@ 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)} : + {measure (n - p)} : Exc (forall (p : { i | i < n}), P p = true) := match le_lt_dec n p with | left _ => value _ @@ -79,14 +79,14 @@ Time Program Fixpoint check_n (n : nat) (P : { i | i < n } -> bool) (p : nat) Require Import Omega Setoid. -Next Obligation. - intros ; simpl in *. apply H. +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. +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. diff --git a/test-suite/success/Projection.v b/test-suite/success/Projection.v index 88da60133..d8faa88a7 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 0c37c59ac..801ece9e3 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 86cf49cb5..1348bb623 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 a3be2898c..87e8c8e33 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 550edca50..bd473fa60 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 60e170e4f..14d27924e 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. + intros A n 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. @@ -923,18 +923,18 @@ 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 + 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 +948,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 +974,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 +990,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 +1026,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 +1034,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 +1050,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 +1105,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 +1144,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 +1154,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 c0065809d..8334322c9 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 diff --git a/test-suite/success/Simplify_eq.v b/test-suite/success/Simplify_eq.v index 5b856e3da..d9abdbf5a 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/TestRefine.v b/test-suite/success/TestRefine.v index dd84402df..5f44c7525 100644 --- a/test-suite/success/TestRefine.v +++ b/test-suite/success/TestRefine.v @@ -42,7 +42,7 @@ Abort. (************************************************************************) -Lemma T : nat. +Lemma T : nat. refine (S _). @@ -95,7 +95,7 @@ Abort. (************************************************************************) -Parameter f : nat * nat -> nat -> nat. +Parameter f : nat * nat -> nat -> nat. Lemma essai : nat. @@ -175,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/apply.v b/test-suite/success/apply.v index f95352b65..8014f73fc 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. @@ -250,7 +250,7 @@ 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. +apply H. Qed. (* Test propagation of evars from subgoal to brother subgoals *) @@ -258,7 +258,7 @@ Qed. (* 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; +intros x H; eapply trans_equal; [apply H | unfold x;match goal with |- ?x = ?x => reflexivity end]. Qed. diff --git a/test-suite/success/cc.v b/test-suite/success/cc.v index 94d827fd5..b565183b9 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/clear.v b/test-suite/success/clear.v index 8169361c4..976bec737 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 525348dec..3d1c91bbe 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. diff --git a/test-suite/success/conv_pbs.v b/test-suite/success/conv_pbs.v index 062c3ee5c..f6ebacaea 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 fede31a8a..bc1757fd5 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 6de7c2197..54bfaa35c 100644 --- a/test-suite/success/dependentind.v +++ b/test-suite/success/dependentind.v @@ -48,7 +48,7 @@ Fixpoint conc (Δ Γ : ctx) : ctx := Notation " Γ ; Δ " := (conc Δ Γ) (at level 25, left associativity) : context_scope. -Reserved Notation " Γ ⊢ Ï„ " (at level 30, no associativity). +Reserved Notation " Γ ⊢ Ï„ " (at level 30, no associativity). Inductive term : ctx -> type -> Type := | ax : `(Γ, Ï„ ⊢ Ï„) @@ -64,7 +64,7 @@ Open Local Scope context_scope. Ltac eqns := subst ; reverse ; simplify_dep_elim ; simplify_IH_hyps. -Lemma weakening : forall Γ Δ Ï„, Γ ; Δ ⊢ Ï„ -> +Lemma weakening : forall Γ Δ Ï„, Γ ; Δ ⊢ Ï„ -> forall Ï„', Γ , Ï„' ; Δ ⊢ Ï„. Proof with simpl in * ; eqns ; eauto with lambda. intros Γ Δ Ï„ H. @@ -97,7 +97,7 @@ Proof with simpl in * ; eqns ; eauto. apply weak... - apply abs... + apply abs... specialize (IHterm (Δ, Ï„0))... eapply app... diff --git a/test-suite/success/destruct.v b/test-suite/success/destruct.v index 59d583fee..e5f1c6187 100644 --- a/test-suite/success/destruct.v +++ b/test-suite/success/destruct.v @@ -5,7 +5,7 @@ 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. diff --git a/test-suite/success/eauto.v b/test-suite/success/eauto.v index 26339d513..c7a2a6c9d 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 6764cfa35..3d3b3b9ef 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). @@ -200,7 +200,7 @@ Abort. (* An example from y-not that was failing in 8.2rc1 *) -Fixpoint filter (A:nat->Set) (l:list (sigT A)) : list (sigT A) := +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') diff --git a/test-suite/success/extraction.v b/test-suite/success/extraction.v index 74d87ffa7..d3bdb1b6d 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 78b01f3e1..be4e06845 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 21bfc0758..af81e53d6 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 9034d6a6f..aabb057a4 100644 --- a/test-suite/success/implicit.v +++ b/test-suite/success/implicit.v @@ -12,7 +12,7 @@ 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 @@ -42,7 +42,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 c3dc2fc62..fcedb2b1a 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 1cf707583..b78651c91 100644 --- a/test-suite/success/induct.v +++ b/test-suite/success/induct.v @@ -21,7 +21,7 @@ Inductive Y : Set := Inductive eq1 : forall A:Type, let B:=A in A -> Prop := refl1 : eq1 True I. -Check +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) => diff --git a/test-suite/success/ltac.v b/test-suite/success/ltac.v index 211ca28b0..09d21628b 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 @@ -180,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. @@ -202,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. diff --git a/test-suite/success/mutual_ind.v b/test-suite/success/mutual_ind.v index 463efed3f..f63dfc385 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 d1b679d55..3d06d1d0f 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/refine.v b/test-suite/success/refine.v index b654277c8..4d743a6d7 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 94b75c7f0..6acdd5161 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. diff --git a/test-suite/success/setoid_ring_module.v b/test-suite/success/setoid_ring_module.v index e947c6d9c..2d9e85b54 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 be5999df5..033b3f485 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 b89787bb0..6baf79701 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 ead93d913..381cda2cd 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 b4de4932e..271e6ef76 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 4929ae4c0..578373217 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/unification.v b/test-suite/success/unification.v index a7e129a38..52c27587a 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. @@ -131,7 +131,7 @@ Qed. 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) -> +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. diff --git a/test-suite/success/univers.v b/test-suite/success/univers.v index 3c2c08831..469cbeb74 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. |