diff options
Diffstat (limited to 'test-suite')
152 files changed, 816 insertions, 817 deletions
diff --git a/test-suite/bugs/closed/1519.v b/test-suite/bugs/closed/1519.v index 98e3e2144..de60de59e 100644 --- a/test-suite/bugs/closed/1519.v +++ b/test-suite/bugs/closed/1519.v @@ -2,7 +2,7 @@ Section S. Variable A:Prop. Variable W:A. - + Remark T: A -> A. intro Z. rename W into Z_. diff --git a/test-suite/bugs/closed/1780.v b/test-suite/bugs/closed/1780.v index 3929fbae2..ade4462a7 100644 --- a/test-suite/bugs/closed/1780.v +++ b/test-suite/bugs/closed/1780.v @@ -1,12 +1,12 @@ Definition bug := Eval vm_compute in eq_rect. (* bug: -Error: Illegal application (Type Error): +Error: Illegal application (Type Error): The term "eq" of type "forall A : Type, A -> A -> Prop" cannot be applied to the terms "x" : "A" "P" : "A -> Type" "x0" : "A" -The 1st term has type "A" which should be coercible to +The 1st term has type "A" which should be coercible to "Type". *) diff --git a/test-suite/bugs/closed/shouldfail/2006.v b/test-suite/bugs/closed/shouldfail/2006.v index f67e997e8..91a16f955 100644 --- a/test-suite/bugs/closed/shouldfail/2006.v +++ b/test-suite/bugs/closed/shouldfail/2006.v @@ -3,7 +3,7 @@ Definition Type1 := Type. Record R : Type1 := { p:Type1 }. (* was accepted before trunk revision 11619 *) -(* +(* Remarks: - The behaviour was inconsistent with the one of Inductive, e.g. @@ -18,6 +18,6 @@ Remarks: Record R : CProp := { ... }. CoRN may have to change the CProp definition into a notation if the - preservation of the former semantics of Record type constraints + preservation of the former semantics of Record type constraints turns to be required. *) diff --git a/test-suite/bugs/closed/shouldsucceed/1100.v b/test-suite/bugs/closed/shouldsucceed/1100.v index 6d619c748..32c78b4b9 100644 --- a/test-suite/bugs/closed/shouldsucceed/1100.v +++ b/test-suite/bugs/closed/shouldsucceed/1100.v @@ -6,7 +6,7 @@ Parameter PQ : forall n, P n <-> Q n. Lemma PQ2 : forall n, P n -> Q n. intros. - rewrite PQ in H. + rewrite PQ in H. trivial. Qed. diff --git a/test-suite/bugs/closed/shouldsucceed/1322.v b/test-suite/bugs/closed/shouldsucceed/1322.v index 7e21aa7ce..1ec7d452a 100644 --- a/test-suite/bugs/closed/shouldsucceed/1322.v +++ b/test-suite/bugs/closed/shouldsucceed/1322.v @@ -7,7 +7,7 @@ Variable I_eq :I -> I -> Prop. Variable I_eq_equiv : Setoid_Theory I I_eq. (* Add Relation I I_eq - reflexivity proved by I_eq_equiv.(Seq_refl I I_eq) + reflexivity proved by I_eq_equiv.(Seq_refl I I_eq) symmetry proved by I_eq_equiv.(Seq_sym I I_eq) transitivity proved by I_eq_equiv.(Seq_trans I I_eq) as I_eq_relation. *) diff --git a/test-suite/bugs/closed/shouldsucceed/1411.v b/test-suite/bugs/closed/shouldsucceed/1411.v index e330d46fd..a1a7b288a 100644 --- a/test-suite/bugs/closed/shouldsucceed/1411.v +++ b/test-suite/bugs/closed/shouldsucceed/1411.v @@ -23,7 +23,7 @@ Program Fixpoint fetch t p (x:Exact t p) {struct t} := match t, p with | No p' , nil => p' | No p' , _::_ => unreachable nat _ - | Br l r, nil => unreachable nat _ + | Br l r, nil => unreachable nat _ | Br l r, true::t => fetch l t _ | Br l r, false::t => fetch r t _ end. diff --git a/test-suite/bugs/closed/shouldsucceed/1414.v b/test-suite/bugs/closed/shouldsucceed/1414.v index 06922e50a..495a16bca 100644 --- a/test-suite/bugs/closed/shouldsucceed/1414.v +++ b/test-suite/bugs/closed/shouldsucceed/1414.v @@ -7,8 +7,8 @@ Inductive t : Set := | Node : t -> data -> t -> Z -> t. Parameter avl : t -> Prop. -Parameter bst : t -> Prop. -Parameter In : data -> t -> Prop. +Parameter bst : t -> Prop. +Parameter In : data -> t -> Prop. Parameter cardinal : t -> nat. Definition card2 (s:t*t) := let (s1,s2) := s in cardinal s1 + cardinal s2. @@ -16,25 +16,25 @@ Parameter split : data -> t -> t*(bool*t). Parameter join : t -> data -> t -> t. Parameter add : data -> t -> t. -Program Fixpoint union +Program Fixpoint union (s u:t) - (hb1: bst s)(ha1: avl s)(hb2: bst u)(hb2: avl u) - { measure (cardinal s + cardinal u) } : - {s' : t | bst s' /\ avl s' /\ forall x, In x s' <-> In x s \/ In x u} := - match s, u with + (hb1: bst s)(ha1: avl s)(hb2: bst u)(hb2: avl u) + { measure (cardinal s + cardinal u) } : + {s' : t | bst s' /\ avl s' /\ forall x, In x s' <-> In x s \/ In x u} := + match s, u with | Leaf,t2 => t2 | t1,Leaf => t1 - | Node l1 v1 r1 h1, Node l2 v2 r2 h2 => + | Node l1 v1 r1 h1, Node l2 v2 r2 h2 => if (Z_ge_lt_dec h1 h2) then - if (Z_eq_dec h2 1) + if (Z_eq_dec h2 1) then add v2 s else let (l2', r2') := split v1 u in join (union l1 l2' _ _ _ _) v1 (union r1 (snd r2') _ _ _ _) else - if (Z_eq_dec h1 1) + if (Z_eq_dec h1 1) then add v1 s else let (l1', r1') := split v2 u in join (union l1' l2 _ _ _ _) v2 (union (snd r1') r2 _ _ _ _) - end. + end. diff --git a/test-suite/bugs/closed/shouldsucceed/1425.v b/test-suite/bugs/closed/shouldsucceed/1425.v index 8e26209a1..6be30174a 100644 --- a/test-suite/bugs/closed/shouldsucceed/1425.v +++ b/test-suite/bugs/closed/shouldsucceed/1425.v @@ -1,4 +1,4 @@ -Require Import Setoid. +Require Import Setoid. Parameter recursion : forall A : Set, A -> (nat -> A -> A) -> nat -> A. diff --git a/test-suite/bugs/closed/shouldsucceed/1446.v b/test-suite/bugs/closed/shouldsucceed/1446.v index d4e7cea81..8cb2d653b 100644 --- a/test-suite/bugs/closed/shouldsucceed/1446.v +++ b/test-suite/bugs/closed/shouldsucceed/1446.v @@ -1,8 +1,8 @@ Lemma not_true_eq_false : forall (b:bool), b <> true -> b = false. Proof. - destruct b;intros;trivial. - elim H. - exact (refl_equal true). + destruct b;intros;trivial. + elim H. + exact (refl_equal true). Qed. Section BUG. @@ -13,7 +13,7 @@ Section BUG. Hypothesis H1 : b <> true. Goal False. - rewrite (not_true_eq_false _ H) in * |-. + rewrite (not_true_eq_false _ H) in * |-. contradiction. Qed. diff --git a/test-suite/bugs/closed/shouldsucceed/1507.v b/test-suite/bugs/closed/shouldsucceed/1507.v index 32e6489c5..f1872a2bb 100644 --- a/test-suite/bugs/closed/shouldsucceed/1507.v +++ b/test-suite/bugs/closed/shouldsucceed/1507.v @@ -8,10 +8,10 @@ rational intervals. *) -Definition associative (A:Type)(op:A->A->A) := +Definition associative (A:Type)(op:A->A->A) := forall x y z:A, op (op x y) z = op x (op y z). -Definition commutative (A:Type)(op:A->A->A) := +Definition commutative (A:Type)(op:A->A->A) := forall x y:A, op x y = op y x. Definition trichotomous (A:Type)(R:A->A->Prop) := @@ -19,7 +19,7 @@ Definition trichotomous (A:Type)(R:A->A->Prop) := Definition relation (A:Type) := A -> A -> Prop. Definition reflexive (A:Type)(R:relation A) := forall x:A, R x x. -Definition transitive (A:Type)(R:relation A) := +Definition transitive (A:Type)(R:relation A) := forall x y z:A, R x y -> R y z -> R x z. Definition symmetric (A:Type)(R:relation A) := forall x y:A, R x y -> R y x. @@ -52,7 +52,7 @@ Record I (grnd:Set)(le:grnd->grnd->Prop) : Type := Imake { Iplus_opp_r : forall x:Icar, Ic (Iplus x (Iopp x)) (Izero); Imult_inv_r : forall x:Icar, ~(Ic x Izero) -> Ic (Imult x (Iinv x)) Ione; (* distributive laws *) - Imult_plus_distr_l : forall x x' y y' z z' z'', + Imult_plus_distr_l : forall x x' y y' z z' z'', Ic x x' -> Ic y y' -> Ic z z' -> Ic z z'' -> Ic (Imult (Iplus x y) z) (Iplus (Imult x' z') (Imult y' z'')); (* order and lattice structure *) @@ -70,7 +70,7 @@ Record I (grnd:Set)(le:grnd->grnd->Prop) : Type := Imake { Ic_sym : symmetric _ Ic }. -Definition interval_set (X:Set)(le:X->X->Prop) := +Definition interval_set (X:Set)(le:X->X->Prop) := (interval X le) -> Prop. (* can be Set as well *) Check interval_set. Check Ic. @@ -101,7 +101,7 @@ Record N (grnd:Set)(le:grnd->grnd->Prop)(grndI:I grnd le) : Type := Nmake { Nplus_opp_r : forall x:Ncar, Nc (Nplus x (Nopp x)) (Nzero); Nmult_inv_r : forall x:Ncar, ~(Nc x Nzero) -> Nc (Nmult x (Ninv x)) None; (* distributive laws *) - Nmult_plus_distr_l : forall x x' y y' z z' z'', + Nmult_plus_distr_l : forall x x' y y' z z' z'', Nc x x' -> Nc y y' -> Nc z z' -> Nc z z'' -> Nc (Nmult (Nplus x y) z) (Nplus (Nmult x' z') (Nmult y' z'')); (* order and lattice structure *) diff --git a/test-suite/bugs/closed/shouldsucceed/1568.v b/test-suite/bugs/closed/shouldsucceed/1568.v index 9f10f7490..3609e9c83 100644 --- a/test-suite/bugs/closed/shouldsucceed/1568.v +++ b/test-suite/bugs/closed/shouldsucceed/1568.v @@ -3,7 +3,7 @@ CoInductive A: Set := with B: Set := mk_B: A -> B. -CoFixpoint a:A := mk_A b +CoFixpoint a:A := mk_A b with b:B := mk_B a. Goal b = match a with mk_A a1 => a1 end. diff --git a/test-suite/bugs/closed/shouldsucceed/1576.v b/test-suite/bugs/closed/shouldsucceed/1576.v index c9ebbd142..3621f7a1f 100644 --- a/test-suite/bugs/closed/shouldsucceed/1576.v +++ b/test-suite/bugs/closed/shouldsucceed/1576.v @@ -13,8 +13,8 @@ End TC. Module Type TD. Declare Module B: TB . -Declare Module C: TC - with Module B := B . +Declare Module C: TC + with Module B := B . End TD. Module Type TE. @@ -25,7 +25,7 @@ Module Type TF. Declare Module E: TE. End TF. -Module G (D: TD). +Module G (D: TD). Module B' := D.C.B. End G. diff --git a/test-suite/bugs/closed/shouldsucceed/1582.v b/test-suite/bugs/closed/shouldsucceed/1582.v index 47953a66f..be5d3dd21 100644 --- a/test-suite/bugs/closed/shouldsucceed/1582.v +++ b/test-suite/bugs/closed/shouldsucceed/1582.v @@ -1,12 +1,12 @@ Require Import Peano_dec. -Definition fact_F : +Definition fact_F : forall (n:nat), (forall m, m<n -> nat) -> nat. -refine +refine (fun n fact_rec => - if eq_nat_dec n 0 then + if eq_nat_dec n 0 then 1 else let fn := fact_rec (n-1) _ in diff --git a/test-suite/bugs/closed/shouldsucceed/1618.v b/test-suite/bugs/closed/shouldsucceed/1618.v index a90290bfb..a9b067ceb 100644 --- a/test-suite/bugs/closed/shouldsucceed/1618.v +++ b/test-suite/bugs/closed/shouldsucceed/1618.v @@ -6,7 +6,7 @@ Definition A_size (a: A) : nat := | A1 n => 0 end. -Require Import Recdef. +Require Import Recdef. Function n3 (P: A -> Prop) (f: forall n, P (A1 n)) (a: A) {struct a} : P a := match a return (P a) with diff --git a/test-suite/bugs/closed/shouldsucceed/1634.v b/test-suite/bugs/closed/shouldsucceed/1634.v index e0c540f36..0150c2503 100644 --- a/test-suite/bugs/closed/shouldsucceed/1634.v +++ b/test-suite/bugs/closed/shouldsucceed/1634.v @@ -18,7 +18,7 @@ Add Parametric Relation a : (S a) Seq Goal forall (a : A) (x y : S a), Seq x y -> Seq x y. intros a x y H. - setoid_replace x with y. + setoid_replace x with y. reflexivity. trivial. Qed. diff --git a/test-suite/bugs/closed/shouldsucceed/1683.v b/test-suite/bugs/closed/shouldsucceed/1683.v index 1571ee20e..3e99694b3 100644 --- a/test-suite/bugs/closed/shouldsucceed/1683.v +++ b/test-suite/bugs/closed/shouldsucceed/1683.v @@ -30,7 +30,7 @@ Add Parametric Relation A : (ms_type A) (ms_eq A) Hypothesis foobar : forall n, ms_eq CR (IRasCR (foo IR n)) (foo CRasCRing n). Goal forall (b:ms_type CR), - ms_eq CR (IRasCR (foo IR O)) b -> + ms_eq CR (IRasCR (foo IR O)) b -> ms_eq CR (IRasCR (foo IR O)) b. intros b H. rewrite foobar. diff --git a/test-suite/bugs/closed/shouldsucceed/1738.v b/test-suite/bugs/closed/shouldsucceed/1738.v index 0deed3663..c2926a2b2 100644 --- a/test-suite/bugs/closed/shouldsucceed/1738.v +++ b/test-suite/bugs/closed/shouldsucceed/1738.v @@ -5,10 +5,10 @@ Module SomeSetoids (Import M:FSetInterface.S). Lemma Equal_refl : forall s, s[=]s. Proof. red; split; auto. Qed. -Add Relation t Equal - reflexivity proved by Equal_refl +Add Relation t Equal + reflexivity proved by Equal_refl symmetry proved by eq_sym - transitivity proved by eq_trans + transitivity proved by eq_trans as EqualSetoid. Add Morphism Empty with signature Equal ==> iff as Empty_m. diff --git a/test-suite/bugs/closed/shouldsucceed/1740.v b/test-suite/bugs/closed/shouldsucceed/1740.v index d9ce546a2..ec4a7a6bc 100644 --- a/test-suite/bugs/closed/shouldsucceed/1740.v +++ b/test-suite/bugs/closed/shouldsucceed/1740.v @@ -17,7 +17,7 @@ Goal f = | n, O => n | _, _ => O end. - unfold f. + unfold f. reflexivity. Qed. diff --git a/test-suite/bugs/closed/shouldsucceed/1775.v b/test-suite/bugs/closed/shouldsucceed/1775.v index dab4120b9..932949a37 100644 --- a/test-suite/bugs/closed/shouldsucceed/1775.v +++ b/test-suite/bugs/closed/shouldsucceed/1775.v @@ -13,7 +13,7 @@ Goal forall s k k' m, (pl k' (nexists (fun w => (nexists (fun b => pl (pair w w) (pl (pair s b) (nexists (fun w0 => (nexists (fun a => pl (pair b w0) - (nexists (fun w1 => (nexists (fun c => pl + (nexists (fun w1 => (nexists (fun c => pl (pair a w1) (pl (pair a c) k))))))))))))))) m. intros. eapply plImp; [ | eauto | intros ]. diff --git a/test-suite/bugs/closed/shouldsucceed/1776.v b/test-suite/bugs/closed/shouldsucceed/1776.v index abf854553..58491f9de 100644 --- a/test-suite/bugs/closed/shouldsucceed/1776.v +++ b/test-suite/bugs/closed/shouldsucceed/1776.v @@ -10,7 +10,7 @@ Definition nexists (P:nat -> nat -> Prop) : nat -> Prop := Goal forall a A m, True -> - (pl A (nexists (fun x => (nexists + (pl A (nexists (fun x => (nexists (fun y => pl (pair a (S x)) (pair a (S y))))))) m. Proof. intros. diff --git a/test-suite/bugs/closed/shouldsucceed/1784.v b/test-suite/bugs/closed/shouldsucceed/1784.v index 5855b1683..8c2e50e07 100644 --- a/test-suite/bugs/closed/shouldsucceed/1784.v +++ b/test-suite/bugs/closed/shouldsucceed/1784.v @@ -56,16 +56,16 @@ Require Import Program. Program Fixpoint lt_dec (x y:sv) { struct x } : {slt x y}+{~slt x y} := match x with - | I x => + | I x => match y with | I y => if (Z_eq_dec x y) then in_left else in_right | S ys => in_right end - | S xs => + | S xs => match y with | I y => in_right | S ys => - let fix list_in (xs ys:list sv) {struct xs} : + let fix list_in (xs ys:list sv) {struct xs} : {slist_in xs ys} + {~slist_in xs ys} := match xs with | nil => in_left @@ -76,8 +76,8 @@ Program Fixpoint lt_dec (x y:sv) { struct x } : {slt x y}+{~slt x y} := | y::ys => if lt_dec x y then in_left else if elem_in ys then in_left else in_right end - in - if elem_in ys then + in + if elem_in ys then if list_in xs ys then in_left else in_right else in_right end @@ -90,7 +90,7 @@ Next Obligation. intro H; inversion H. Defined. Next Obligation. intro H; inversion H. Defined. Next Obligation. intro H; inversion H; subst. Defined. Next Obligation. - intro H1; contradict H. inversion H1; subst. assumption. + intro H1; contradict H. inversion H1; subst. assumption. contradict H0; assumption. Defined. Next Obligation. intro H1; contradict H0. inversion H1; subst. assumption. Defined. diff --git a/test-suite/bugs/closed/shouldsucceed/1791.v b/test-suite/bugs/closed/shouldsucceed/1791.v index 694f056e8..be0e8ae8b 100644 --- a/test-suite/bugs/closed/shouldsucceed/1791.v +++ b/test-suite/bugs/closed/shouldsucceed/1791.v @@ -9,7 +9,7 @@ Definition k1 := k0 -> k0. (** iterating X n times *) Fixpoint Pow (X:k1)(k:nat){struct k}:k1:= match k with 0 => fun X => X - | S k' => fun A => X (Pow X k' A) + | S k' => fun A => X (Pow X k' A) end. Parameter Bush: k1. diff --git a/test-suite/bugs/closed/shouldsucceed/1844.v b/test-suite/bugs/closed/shouldsucceed/1844.v index 545f26154..5627612f6 100644 --- a/test-suite/bugs/closed/shouldsucceed/1844.v +++ b/test-suite/bugs/closed/shouldsucceed/1844.v @@ -188,7 +188,7 @@ with exec_finish: function -> outcome -> store -> value -> store -> Prop := with exec_function: function -> store -> value -> store -> Prop := | exec_function_intro: forall f st out st1 v st', - exec f.(fn_body) st out st1 -> + exec f.(fn_body) st out st1 -> exec_finish f out st1 v st' -> exec_function f st v st'. diff --git a/test-suite/bugs/closed/shouldsucceed/1901.v b/test-suite/bugs/closed/shouldsucceed/1901.v index 598db3660..7d86adbfb 100644 --- a/test-suite/bugs/closed/shouldsucceed/1901.v +++ b/test-suite/bugs/closed/shouldsucceed/1901.v @@ -2,9 +2,9 @@ Require Import Relations. Record Poset{A:Type}(Le : relation A) : Type := Build_Poset - { - Le_refl : forall x : A, Le x x; - Le_trans : forall x y z : A, Le x y -> Le y z -> Le x z; + { + Le_refl : forall x : A, Le x x; + Le_trans : forall x y z : A, Le x y -> Le y z -> Le x z; Le_antisym : forall x y : A, Le x y -> Le y x -> x = y }. Definition nat_Poset : Poset Peano.le. diff --git a/test-suite/bugs/closed/shouldsucceed/1905.v b/test-suite/bugs/closed/shouldsucceed/1905.v index fb2725c97..8c81d7510 100644 --- a/test-suite/bugs/closed/shouldsucceed/1905.v +++ b/test-suite/bugs/closed/shouldsucceed/1905.v @@ -5,7 +5,7 @@ Axiom t : Set. Axiom In : nat -> t -> Prop. Axiom InE : forall (x : nat) (s:t), impl (In x s) True. -Goal forall a s, +Goal forall a s, In a s -> False. Proof. intros a s Ia. diff --git a/test-suite/bugs/closed/shouldsucceed/1918.v b/test-suite/bugs/closed/shouldsucceed/1918.v index 9d4a3e047..474ec935b 100644 --- a/test-suite/bugs/closed/shouldsucceed/1918.v +++ b/test-suite/bugs/closed/shouldsucceed/1918.v @@ -35,7 +35,7 @@ Definition mon (X:k1) : Type := forall (A B:Set), (A -> B) -> X A -> X B. (** extensionality *) Definition ext (X:k1)(h: mon X): Prop := - forall (A B:Set)(f g:A -> B), + forall (A B:Set)(f g:A -> B), (forall a, f a = g a) -> forall r, h _ _ f r = h _ _ g r. (** first functor law *) @@ -44,7 +44,7 @@ Definition fct1 (X:k1)(m: mon X) : Prop := (** second functor law *) Definition fct2 (X:k1)(m: mon X) : Prop := - forall (A B C:Set)(f:A -> B)(g:B -> C)(x:X A), + forall (A B C:Set)(f:A -> B)(g:B -> C)(x:X A), m _ _ (g o f) x = m _ _ g (m _ _ f x). (** pack up the good properties of the approximation into @@ -60,7 +60,7 @@ Definition pEFct (F:k2) : Type := forall (X:k1), EFct X -> EFct (F X). -(** we show some closure properties of pEFct, depending on such properties +(** we show some closure properties of pEFct, depending on such properties for EFct *) Definition moncomp (X Y:k1)(mX:mon X)(mY:mon Y): mon (fun A => X(Y A)). @@ -92,7 +92,7 @@ Proof. apply (f2 ef2). Defined. -Corollary comppEFct (F G:k2): pEFct F -> pEFct G -> +Corollary comppEFct (F G:k2): pEFct F -> pEFct G -> pEFct (fun X A => F X (G X A)). Proof. red. @@ -104,7 +104,7 @@ Defined. Lemma sumEFct (X Y:k1): EFct X -> EFct Y -> EFct (fun A => X A + Y A)%type. Proof. intros X Y ef1 ef2. - set (m12:=fun (A B:Set)(f:A->B) x => match x with + set (m12:=fun (A B:Set)(f:A->B) x => match x with | inl y => inl _ (m ef1 f y) | inr y => inr _ (m ef2 f y) end). @@ -133,7 +133,7 @@ Proof. rewrite (f2 ef2); reflexivity. Defined. -Corollary sumpEFct (F G:k2): pEFct F -> pEFct G -> +Corollary sumpEFct (F G:k2): pEFct F -> pEFct G -> pEFct (fun X A => F X A + G X A)%type. Proof. red. @@ -145,7 +145,7 @@ Defined. Lemma prodEFct (X Y:k1): EFct X -> EFct Y -> EFct (fun A => X A * Y A)%type. Proof. intros X Y ef1 ef2. - set (m12:=fun (A B:Set)(f:A->B) x => match x with + set (m12:=fun (A B:Set)(f:A->B) x => match x with (x1,x2) => (m ef1 f x1, m ef2 f x2) end). apply (mkEFct(m:=m12)); red; intros. (* prove ext *) @@ -168,7 +168,7 @@ Proof. apply (f2 ef2). Defined. -Corollary prodpEFct (F G:k2): pEFct F -> pEFct G -> +Corollary prodpEFct (F G:k2): pEFct F -> pEFct G -> pEFct (fun X A => F X A * G X A)%type. Proof. red. @@ -248,19 +248,19 @@ Module Type LNMIt_Type. Parameter F:k2. Parameter FpEFct: pEFct F. -Parameter mu20: k1. +Parameter mu20: k1. Definition mu2: k1:= fun A => mu20 A. Parameter mapmu2: mon mu2. Definition MItType: Type := forall G : k1, (forall X : k1, X c_k1 G -> F X c_k1 G) -> mu2 c_k1 G. Parameter MIt0 : MItType. -Definition MIt : MItType:= fun G s A t => MIt0 s t. -Definition InType : Type := - forall (X:k1)(ef:EFct X)(j: X c_k1 mu2), +Definition MIt : MItType:= fun G s A t => MIt0 s t. +Definition InType : Type := + forall (X:k1)(ef:EFct X)(j: X c_k1 mu2), NAT j (m ef) mapmu2 -> F X c_k1 mu2. Parameter In : InType. Axiom mapmu2Red : forall (A:Set)(X:k1)(ef:EFct X)(j: X c_k1 mu2) - (n: NAT j (m ef) mapmu2)(t: F X A)(B:Set)(f:A->B), + (n: NAT j (m ef) mapmu2)(t: F X A)(B:Set)(f:A->B), mapmu2 f (In ef n t) = In ef n (m (FpEFct ef) f t). Axiom MItRed : forall (G : k1) (s : forall X : k1, X c_k1 G -> F X c_k1 G)(X : k1)(ef:EFct X)(j: X c_k1 mu2) @@ -327,8 +327,8 @@ Fixpoint Pow (X:k1)(k:nat){struct k}:k1:= Fixpoint POW (k:nat)(X:k1)(m:mon X){struct k} : mon (Pow X k) := match k return mon (Pow X k) - with 0 => fun _ _ f => f - | S k' => fun _ _ f => m _ _ (POW k' m f) + with 0 => fun _ _ f => f + | S k' => fun _ _ f => m _ _ (POW k' m f) end. Module Type BushkToList_Type. diff --git a/test-suite/bugs/closed/shouldsucceed/1925.v b/test-suite/bugs/closed/shouldsucceed/1925.v index 17eb721ad..4caee1c36 100644 --- a/test-suite/bugs/closed/shouldsucceed/1925.v +++ b/test-suite/bugs/closed/shouldsucceed/1925.v @@ -3,14 +3,14 @@ Require Import List. -Definition compose (A B C : Type) (g : B -> C) (f : A -> B) : A -> C := +Definition compose (A B C : Type) (g : B -> C) (f : A -> B) : A -> C := fun x : A => g(f x). -Definition map_fuse' : - forall (A B C : Type) (g : B -> C) (f : A -> B) (xs : list A), - (map g (map f xs)) = map (compose _ _ _ g f) xs +Definition map_fuse' : + forall (A B C : Type) (g : B -> C) (f : A -> B) (xs : list A), + (map g (map f xs)) = map (compose _ _ _ g f) xs := - fun A B C g f => + fun A B C g f => (fix loop (ys : list A) {struct ys} := match ys as ys return (map g (map f ys)) = map (compose _ _ _ g f) ys with diff --git a/test-suite/bugs/closed/shouldsucceed/1931.v b/test-suite/bugs/closed/shouldsucceed/1931.v index bc8be78fe..930ace1d5 100644 --- a/test-suite/bugs/closed/shouldsucceed/1931.v +++ b/test-suite/bugs/closed/shouldsucceed/1931.v @@ -8,7 +8,7 @@ Inductive T (A:Set) : Set := Fixpoint map (A B:Set)(f:A->B)(t:T A) : T B := match t with app t1 t2 => app (map f t1)(map f t2) - end. + end. Fixpoint subst (A B:Set)(f:A -> T B)(t:T A) :T B := match t with @@ -19,7 +19,7 @@ Fixpoint subst (A B:Set)(f:A -> T B)(t:T A) :T B := Definition k0:=Set. (** interaction of subst with map *) -Lemma substLaw1 (A:k0)(B C:Set)(f: A -> B)(g:B -> T C)(t: T A): +Lemma substLaw1 (A:k0)(B C:Set)(f: A -> B)(g:B -> T C)(t: T A): subst g (map f t) = subst (fun x => g (f x)) t. Proof. intros. diff --git a/test-suite/bugs/closed/shouldsucceed/1935.v b/test-suite/bugs/closed/shouldsucceed/1935.v index 641dcb7af..72396d490 100644 --- a/test-suite/bugs/closed/shouldsucceed/1935.v +++ b/test-suite/bugs/closed/shouldsucceed/1935.v @@ -1,14 +1,14 @@ Definition f (n:nat) := n = n. Lemma f_refl : forall n , f n. -intros. reflexivity. +intros. reflexivity. Qed. Definition f' (x:nat) (n:nat) := n = n. Lemma f_refl' : forall n , f' n n. Proof. - intros. reflexivity. + intros. reflexivity. Qed. Require Import ZArith. diff --git a/test-suite/bugs/closed/shouldsucceed/1939.v b/test-suite/bugs/closed/shouldsucceed/1939.v index 3aa55e834..5e61529b4 100644 --- a/test-suite/bugs/closed/shouldsucceed/1939.v +++ b/test-suite/bugs/closed/shouldsucceed/1939.v @@ -14,6 +14,6 @@ Require Import Setoid Program.Basics. Goal forall x y, R x y -> P y -> P x. Proof. intros x y H1 H2. - rewrite H1. + rewrite H1. auto. Qed.
\ No newline at end of file diff --git a/test-suite/bugs/closed/shouldsucceed/1944.v b/test-suite/bugs/closed/shouldsucceed/1944.v index 7d9f9eb26..ee2918c6e 100644 --- a/test-suite/bugs/closed/shouldsucceed/1944.v +++ b/test-suite/bugs/closed/shouldsucceed/1944.v @@ -1,6 +1,6 @@ (* Test some uses of ? in introduction patterns *) -Inductive J : nat -> Prop := +Inductive J : nat -> Prop := | K : forall p, J p -> (True /\ True) -> J (S p). Lemma bug : forall n, J n -> J (S n). diff --git a/test-suite/bugs/closed/shouldsucceed/1951.v b/test-suite/bugs/closed/shouldsucceed/1951.v index 4fbd6b22d..12c0ef9bf 100644 --- a/test-suite/bugs/closed/shouldsucceed/1951.v +++ b/test-suite/bugs/closed/shouldsucceed/1951.v @@ -28,7 +28,7 @@ Inductive sg : Type := Sg. (* single *) Definition ipl2 (P : a -> Type) := (* in Prop, that means P is true forall *) fold_right (fun x => prod (P x)) sg. (* the elements of a given list *) -Definition ind +Definition ind : forall S : a -> Type, (forall ls : list a, ipl2 S ls -> S (b ls)) -> forall s : a, S s := fun (S : a -> Type) diff --git a/test-suite/bugs/closed/shouldsucceed/1981.v b/test-suite/bugs/closed/shouldsucceed/1981.v index 0c3b96dad..99952682d 100644 --- a/test-suite/bugs/closed/shouldsucceed/1981.v +++ b/test-suite/bugs/closed/shouldsucceed/1981.v @@ -1,5 +1,5 @@ Implicit Arguments ex_intro [A]. Goal exists n : nat, True. - eapply ex_intro. exact 0. exact I. + eapply ex_intro. exact 0. exact I. Qed. diff --git a/test-suite/bugs/closed/shouldsucceed/2001.v b/test-suite/bugs/closed/shouldsucceed/2001.v index 323021dea..c50ad036d 100644 --- a/test-suite/bugs/closed/shouldsucceed/2001.v +++ b/test-suite/bugs/closed/shouldsucceed/2001.v @@ -2,7 +2,7 @@ computed when the user explicitly indicated it *) Inductive T : Set := -| v : T. +| v : T. Definition f (s:nat) (t:T) : nat. fix 2. @@ -12,9 +12,9 @@ refine | v => s end. Defined. - + Lemma test : forall s, f s v = s. -Proof. +Proof. reflexivity. -Qed. +Qed. diff --git a/test-suite/bugs/closed/shouldsucceed/2017.v b/test-suite/bugs/closed/shouldsucceed/2017.v index 948cea3ee..df6661483 100644 --- a/test-suite/bugs/closed/shouldsucceed/2017.v +++ b/test-suite/bugs/closed/shouldsucceed/2017.v @@ -8,8 +8,8 @@ Set Implicit Arguments. Variable choose : forall(P : bool -> Prop)(H : exists x, P x), bool. Variable H : exists x : bool, True. - + Definition coef := match Some true with - Some _ => @choose _ H |_ => true -end . + Some _ => @choose _ H |_ => true +end . diff --git a/test-suite/bugs/closed/shouldsucceed/2083.v b/test-suite/bugs/closed/shouldsucceed/2083.v index 63f91e565..6fc046495 100644 --- a/test-suite/bugs/closed/shouldsucceed/2083.v +++ b/test-suite/bugs/closed/shouldsucceed/2083.v @@ -2,11 +2,11 @@ Require Import Program Arith. Program Fixpoint check_n (n : nat) (P : { i | i < n } -> bool) (p : nat) (H : forall (i : { i | i < n }), i < p -> P i = true) - {measure (n - p)} : + {measure (n - p)} : Exc (forall (p : { i | i < n}), P p = true) := match le_lt_dec n p with | left _ => value _ - | right cmp => + | right cmp => if dec (P p) then check_n n P (S p) _ else diff --git a/test-suite/bugs/closed/shouldsucceed/2117.v b/test-suite/bugs/closed/shouldsucceed/2117.v index 763d85e2c..6377a8b74 100644 --- a/test-suite/bugs/closed/shouldsucceed/2117.v +++ b/test-suite/bugs/closed/shouldsucceed/2117.v @@ -44,7 +44,7 @@ Ltac Subst := apply substcopy;intros;EtaLong. Ltac Rigid_aux := fun A => apply A|| Rigid_aux (copyr_fun _ _ _ _ A). Ltac Rigid := fun A => apply copyr_atom; Rigid_aux A. -Theorem church0: forall i:Type, exists X:(i->i)->i->i, +Theorem church0: forall i:Type, exists X:(i->i)->i->i, copy ((i->i)->i->i) (fun f:i->i => fun x:i=>f (X f x)) (fun f:i->i=>fun x:i=>app i i (X f) (f x)). intros. esplit. diff --git a/test-suite/bugs/closed/shouldsucceed/2139.v b/test-suite/bugs/closed/shouldsucceed/2139.v index 4f71d097f..415a1b27d 100644 --- a/test-suite/bugs/closed/shouldsucceed/2139.v +++ b/test-suite/bugs/closed/shouldsucceed/2139.v @@ -2,19 +2,19 @@ Class Patch (patch : Type) := { commute : patch -> patch -> Prop -}. - +}. + Parameter flip : forall `{patchInstance : Patch patch} - {a b : patch}, + {a b : patch}, commute a b <-> commute b a. - + Lemma Foo : forall `{patchInstance : Patch patch} - {a b : patch}, + {a b : patch}, (commute a b) -> True. -Proof. -intros. -apply flip in H. +Proof. +intros. +apply flip in H. (* failed in well-formed arity check because elimination predicate of iff in (@flip _ _ _ _) had normalized evars while the ones in the diff --git a/test-suite/bugs/closed/shouldsucceed/38.v b/test-suite/bugs/closed/shouldsucceed/38.v index 7bc04b1fe..4fc8d7c97 100644 --- a/test-suite/bugs/closed/shouldsucceed/38.v +++ b/test-suite/bugs/closed/shouldsucceed/38.v @@ -6,7 +6,7 @@ Inductive liste : Set := | vide : liste | c : A -> liste -> liste. -Inductive e : A -> liste -> Prop := +Inductive e : A -> liste -> Prop := | ec : forall (x : A) (l : liste), e x (c x l) | ee : forall (x y : A) (l : liste), e x l -> e x (c y l). diff --git a/test-suite/bugs/closed/shouldsucceed/846.v b/test-suite/bugs/closed/shouldsucceed/846.v index a963b225f..ee5ec1fa6 100644 --- a/test-suite/bugs/closed/shouldsucceed/846.v +++ b/test-suite/bugs/closed/shouldsucceed/846.v @@ -27,7 +27,7 @@ Definition index := list bool. Inductive L (A:Set) : index -> Set := initL: A -> L A nil - | pluslL: forall l:index, One -> L A (false::l) + | pluslL: forall l:index, One -> L A (false::l) | plusrL: forall l:index, L A l -> L A (false::l) | varL: forall l:index, L A l -> L A (true::l) | appL: forall l:index, L A (true::l) -> L A (true::l) -> L A (true::l) @@ -109,7 +109,7 @@ Proof. exact (monL (fun x:One + A => (match (maybe (fun a:A => initL a) x) with | inl u => pluslL _ _ u - | inr t' => plusrL t' end)) r). + | inr t' => plusrL t' end)) r). Defined. Section minimal. @@ -119,11 +119,11 @@ Hypothesis G: Set -> Set. Hypothesis step: sub1 (LamF' G) G. Fixpoint L'(A:Set)(i:index){struct i} : Set := - match i with + match i with nil => A | false::l => One + L' A l | true::l => G (L' A l) - end. + end. Definition LinL': forall (A:Set)(i:index), L A i -> L' A i. Proof. @@ -177,7 +177,7 @@ Proof. assumption. induction a. simpl L' in t. - apply (aczelapp (l1:=true::nil) (l2:=i)). + apply (aczelapp (l1:=true::nil) (l2:=i)). exact (lam' IHi t). simpl L' in t. induction t. diff --git a/test-suite/bugs/opened/shouldnotfail/1416.v b/test-suite/bugs/opened/shouldnotfail/1416.v index c6f4302d8..da67d9b04 100644 --- a/test-suite/bugs/opened/shouldnotfail/1416.v +++ b/test-suite/bugs/opened/shouldnotfail/1416.v @@ -4,12 +4,12 @@ Record Place (Env A: Type) : Type := { read: Env -> A ; write: Env -> A -> Env ; write_read: forall (e:Env), (write e (read e))=e -}. +}. Hint Rewrite -> write_read: placeeq. Record sumPl (Env A B: Type) (vL:(Place Env A)) (vR:(Place Env B)) : Type := - { + { mkEnv: A -> B -> Env ; mkEnv2writeL: forall (e:Env) (x:A), (mkEnv x (read vR e))=(write vL e x) }. diff --git a/test-suite/bugs/opened/shouldnotfail/1501.v b/test-suite/bugs/opened/shouldnotfail/1501.v index 85c09dbd1..1845dd1f6 100644 --- a/test-suite/bugs/opened/shouldnotfail/1501.v +++ b/test-suite/bugs/opened/shouldnotfail/1501.v @@ -8,7 +8,7 @@ Require Export Setoid. Section Essais. (* Parametrized Setoid *) -Parameter K : Type -> Type. +Parameter K : Type -> Type. Parameter equiv : forall A : Type, K A -> K A -> Prop. Parameter equiv_refl : forall (A : Type) (x : K A), equiv x x. Parameter equiv_sym : forall (A : Type) (x y : K A), equiv x y -> equiv y x. @@ -40,7 +40,7 @@ Parameter Hint Resolve equiv_refl equiv_sym equiv_trans: monad. -Add Relation K equiv +Add Relation K equiv reflexivity proved by (@equiv_refl) symmetry proved by (@equiv_sym) transitivity proved by (@equiv_trans) @@ -67,7 +67,7 @@ Proof. unfold fequiv; intros; eapply equiv_trans; auto with monad. Qed. -Add Relation (fun (A B:Type) => A -> K B) fequiv +Add Relation (fun (A B:Type) => A -> K B) fequiv reflexivity proved by (@fequiv_refl) symmetry proved by (@fequiv_sym) transitivity proved by (@fequiv_trans) @@ -82,12 +82,12 @@ Qed. Lemma test: forall (A B: Type) (m1 m2 m3: K A) (f: A -> A -> K B), - (equiv m1 m2) -> (equiv m2 m3) -> + (equiv m1 m2) -> (equiv m2 m3) -> equiv (bind m1 (fun a => bind m2 (fun a' => f a a'))) (bind m2 (fun a => bind m3 (fun a' => f a a'))). Proof. - intros A B m1 m2 m3 f H1 H2. + intros A B m1 m2 m3 f H1 H2. setoid_rewrite H1. (* this works *) setoid_rewrite H2. trivial by equiv_refl. -Qed. +Qed. diff --git a/test-suite/bugs/opened/shouldnotfail/1596.v b/test-suite/bugs/opened/shouldnotfail/1596.v index 766bf524c..de77e35d3 100644 --- a/test-suite/bugs/opened/shouldnotfail/1596.v +++ b/test-suite/bugs/opened/shouldnotfail/1596.v @@ -11,12 +11,12 @@ Module OrderedPair (X:OrderedType) (Y:OrderedType) <: OrderedType with Definition t := (X.t * Y.t)%type. Definition t := (X.t * Y.t)%type. - Definition eq (xy1:t) (xy2:t) := + Definition eq (xy1:t) (xy2:t) := let (x1,y1) := xy1 in let (x2,y2) := xy2 in (X.eq x1 x2) /\ (Y.eq y1 y2). - Definition lt (xy1:t) (xy2:t) := + Definition lt (xy1:t) (xy2:t) := let (x1,y1) := xy1 in let (x2,y2) := xy2 in (X.lt x1 x2) \/ ((X.eq x1 x2) /\ (Y.lt y1 y2)). @@ -101,7 +101,7 @@ Definition t := (X.t * Y.t)%type. Defined. Hint Immediate eq_sym. - Hint Resolve eq_refl eq_trans lt_not_eq lt_trans. + Hint Resolve eq_refl eq_trans lt_not_eq lt_trans. End OrderedPair. Module MessageSpi. @@ -189,8 +189,8 @@ n)->(hedge_synthesis_relation h m n). Fixpoint hedge_in_synthesis (h:hedge) (m:MessageSpi.message) (n:MessageSpi.message) {struct m} : bool := - if H.mem (m,n) h - then true + if H.mem (m,n) h + then true else false. Definition hedge_synthesis_spec (h:hedge) := hedge_synthesis_relation @@ -221,8 +221,8 @@ n). Fixpoint hedge_in_synthesis (h:hedge) (m:MessageSpi.t) (n:MessageSpi.t) {struct m} : bool := - if H.mem (m,n) h - then true + if H.mem (m,n) h + then true else false. Definition hedge_synthesis_spec (h:hedge) := hedge_synthesis_relation @@ -235,7 +235,7 @@ n). induction m;simpl;intro. elim (Bool_elim_bool (H.mem (MessageSpi.MNam n,n0) h));intros. apply SynInc;apply H.mem_2;trivial. - + rewrite H in H0. (* !! impossible here !! *) discriminate H0. Qed. diff --git a/test-suite/bugs/opened/shouldnotfail/1671.v b/test-suite/bugs/opened/shouldnotfail/1671.v index 800c431ec..d95c21084 100644 --- a/test-suite/bugs/opened/shouldnotfail/1671.v +++ b/test-suite/bugs/opened/shouldnotfail/1671.v @@ -6,7 +6,7 @@ CoInductive hdlist : unit -> Type := Variable P : forall bo, hdlist bo -> Prop. Variable all : forall bo l, P bo l. -Definition F (l:hdlist tt) : P tt l := +Definition F (l:hdlist tt) : P tt l := match l in hdlist u return P u l with | cons (cons l') => all tt _ end. diff --git a/test-suite/complexity/injection.v b/test-suite/complexity/injection.v index db2d9c53f..335996c27 100644 --- a/test-suite/complexity/injection.v +++ b/test-suite/complexity/injection.v @@ -43,11 +43,11 @@ Record joinmap (key: Type) (t: Type) (j : joinable t) : Type exists s2, jm_j.(join) s1 s2 s3 }. -Parameter mkJoinmap : forall (key: Type) (t: Type) (j: joinable t), +Parameter mkJoinmap : forall (key: Type) (t: Type) (j: joinable t), joinmap key j. Parameter ADMIT: forall p: Prop, p. -Implicit Arguments ADMIT [p]. +Implicit Arguments ADMIT [p]. Module Share. Parameter jb : joinable bool. @@ -90,7 +90,7 @@ Definition jown : joinable own := Joinable own_is_empty own_join ADMIT ADMIT ADMIT ADMIT ADMIT ADMIT ADMIT ADMIT . End Own. - + Fixpoint sinv (n: nat) : Type := match n with | O => unit diff --git a/test-suite/failure/Case5.v b/test-suite/failure/Case5.v index 29996fd45..494443f1c 100644 --- a/test-suite/failure/Case5.v +++ b/test-suite/failure/Case5.v @@ -1,7 +1,7 @@ Inductive MS : Set := | X : MS -> MS | Y : MS -> MS. - + Type (fun p : MS => match p return nat with | X x => 0 end). diff --git a/test-suite/failure/Case9.v b/test-suite/failure/Case9.v index a3b99f631..d63c49403 100644 --- a/test-suite/failure/Case9.v +++ b/test-suite/failure/Case9.v @@ -1,7 +1,7 @@ Parameter compare : forall n m : nat, {n < m} + {n = m} + {n > m}. Type match compare 0 0 return nat with - + (* k<i *) | left _ _ (left _ _ _) => 0 (* k=i *) | left _ _ _ => 0 (* k>i *) | right _ _ _ => 0 diff --git a/test-suite/failure/guard.v b/test-suite/failure/guard.v index 7e07a9058..75e511386 100644 --- a/test-suite/failure/guard.v +++ b/test-suite/failure/guard.v @@ -18,4 +18,4 @@ Definition f := let h := f in (* h = Rel 4 *) fix F (n:nat) : nat := h F S n. (* here Rel 4 = g *) - + diff --git a/test-suite/failure/inductive3.v b/test-suite/failure/inductive3.v index e5a4e1b66..cf035edf7 100644 --- a/test-suite/failure/inductive3.v +++ b/test-suite/failure/inductive3.v @@ -1,4 +1,4 @@ -(* Check that the nested inductive types positivity check avoids recursively +(* Check that the nested inductive types positivity check avoids recursively non uniform parameters (at least if these parameters break positivity) *) Inductive t (A:Type) : Type := c : t (A -> A) -> t A. diff --git a/test-suite/failure/proofirrelevance.v b/test-suite/failure/proofirrelevance.v index eedf2612b..93e159e8b 100644 --- a/test-suite/failure/proofirrelevance.v +++ b/test-suite/failure/proofirrelevance.v @@ -1,5 +1,5 @@ (* This was working in version 8.1beta (bug in the Sort-polymorphism - of inductive types), but this is inconsistent with classical logic + of inductive types), but this is inconsistent with classical logic in Prop *) Inductive bool_in_prop : Type := hide : bool -> bool_in_prop diff --git a/test-suite/failure/rewrite_in_hyp2.v b/test-suite/failure/rewrite_in_hyp2.v index a32037a21..1533966ef 100644 --- a/test-suite/failure/rewrite_in_hyp2.v +++ b/test-suite/failure/rewrite_in_hyp2.v @@ -1,4 +1,4 @@ -(* Until revision 10221, rewriting in hypotheses of the form +(* Until revision 10221, rewriting in hypotheses of the form "(fun x => phi(x)) t" with "t" not rewritable used to behave as a beta-normalization tactic instead of raising the expected message "nothing to rewrite" *) diff --git a/test-suite/failure/subtyping.v b/test-suite/failure/subtyping.v index 35fd20369..127da8513 100644 --- a/test-suite/failure/subtyping.v +++ b/test-suite/failure/subtyping.v @@ -4,17 +4,17 @@ Module Type T. Parameter A : Type. - Inductive L : Prop := + Inductive L : Prop := | L0 | L1 : (A -> Prop) -> L. End T. -Module TT : T. +Module TT : T. Parameter A : Type. - Inductive L : Type := + Inductive L : Type := | L0 | L1 : (A -> Prop) -> L. diff --git a/test-suite/failure/subtyping2.v b/test-suite/failure/subtyping2.v index 0a75ae456..addd3b459 100644 --- a/test-suite/failure/subtyping2.v +++ b/test-suite/failure/subtyping2.v @@ -61,7 +61,7 @@ End Inverse_Image. Section Burali_Forti_Paradox. - Definition morphism (A : Type) (R : A -> A -> Prop) + Definition morphism (A : Type) (R : A -> A -> Prop) (B : Type) (S : B -> B -> Prop) (f : A -> B) := forall x y : A, R x y -> S (f x) (f y). @@ -69,7 +69,7 @@ Section Burali_Forti_Paradox. assumes there exists an universal system of notations, i.e: - A type A0 - An injection i0 from relations on any type into A0 - - The proof that i0 is injective modulo morphism + - The proof that i0 is injective modulo morphism *) Variable A0 : Type. (* Type_i *) Variable i0 : forall X : Type, (X -> X -> Prop) -> A0. (* X: Type_j *) @@ -82,7 +82,7 @@ Section Burali_Forti_Paradox. (* Embedding of x in y: x and y are images of 2 well founded relations R1 and R2, the ordinal of R2 being strictly greater than that of R1. *) - Record emb (x y : A0) : Prop := + Record emb (x y : A0) : Prop := {X1 : Type; R1 : X1 -> X1 -> Prop; eqx : x = i0 X1 R1; @@ -166,7 +166,7 @@ Defined. End Subsets. - Definition fsub (a b : A0) (H : emb a b) (x : sub a) : + Definition fsub (a b : A0) (H : emb a b) (x : sub a) : sub b := Build_sub _ (witness _ x) (emb_trans _ _ _ (emb_wit _ x) H). (* F is a morphism: a < b => F(a) < F(b) diff --git a/test-suite/failure/univ_include.v b/test-suite/failure/univ_include.v index 4be70d888..56f04f9d6 100644 --- a/test-suite/failure/univ_include.v +++ b/test-suite/failure/univ_include.v @@ -1,9 +1,9 @@ Definition T := Type. Definition U := Type. -Module Type MT. +Module Type MT. Parameter t : T. -End MT. +End MT. Module Type MU. Parameter t : U. diff --git a/test-suite/failure/universes-buraliforti-redef.v b/test-suite/failure/universes-buraliforti-redef.v index 049f97f22..034b7f094 100644 --- a/test-suite/failure/universes-buraliforti-redef.v +++ b/test-suite/failure/universes-buraliforti-redef.v @@ -64,7 +64,7 @@ End Inverse_Image. Section Burali_Forti_Paradox. - Definition morphism (A : Type) (R : A -> A -> Prop) + Definition morphism (A : Type) (R : A -> A -> Prop) (B : Type) (S : B -> B -> Prop) (f : A -> B) := forall x y : A, R x y -> S (f x) (f y). @@ -72,7 +72,7 @@ Section Burali_Forti_Paradox. assumes there exists an universal system of notations, i.e: - A type A0 - An injection i0 from relations on any type into A0 - - The proof that i0 is injective modulo morphism + - The proof that i0 is injective modulo morphism *) Variable A0 : Type. (* Type_i *) Variable i0 : forall X : Type, (X -> X -> Prop) -> A0. (* X: Type_j *) @@ -85,7 +85,7 @@ Section Burali_Forti_Paradox. (* Embedding of x in y: x and y are images of 2 well founded relations R1 and R2, the ordinal of R2 being strictly greater than that of R1. *) - Record emb (x y : A0) : Prop := + Record emb (x y : A0) : Prop := {X1 : Type; R1 : X1 -> X1 -> Prop; eqx : x = i0 X1 R1; @@ -168,7 +168,7 @@ Defined. End Subsets. - Definition fsub (a b : A0) (H : emb a b) (x : sub a) : + Definition fsub (a b : A0) (H : emb a b) (x : sub a) : sub b := Build_sub _ (witness _ x) (emb_trans _ _ _ (emb_wit _ x) H). (* F is a morphism: a < b => F(a) < F(b) diff --git a/test-suite/failure/universes-buraliforti.v b/test-suite/failure/universes-buraliforti.v index d18d21195..1f96ab34a 100644 --- a/test-suite/failure/universes-buraliforti.v +++ b/test-suite/failure/universes-buraliforti.v @@ -47,7 +47,7 @@ End Inverse_Image. Section Burali_Forti_Paradox. - Definition morphism (A : Type) (R : A -> A -> Prop) + Definition morphism (A : Type) (R : A -> A -> Prop) (B : Type) (S : B -> B -> Prop) (f : A -> B) := forall x y : A, R x y -> S (f x) (f y). @@ -55,7 +55,7 @@ Section Burali_Forti_Paradox. assumes there exists an universal system of notations, i.e: - A type A0 - An injection i0 from relations on any type into A0 - - The proof that i0 is injective modulo morphism + - The proof that i0 is injective modulo morphism *) Variable A0 : Type. (* Type_i *) Variable i0 : forall X : Type, (X -> X -> Prop) -> A0. (* X: Type_j *) @@ -68,7 +68,7 @@ Section Burali_Forti_Paradox. (* Embedding of x in y: x and y are images of 2 well founded relations R1 and R2, the ordinal of R2 being strictly greater than that of R1. *) - Record emb (x y : A0) : Prop := + Record emb (x y : A0) : Prop := {X1 : Type; R1 : X1 -> X1 -> Prop; eqx : x = i0 X1 R1; @@ -152,7 +152,7 @@ Defined. End Subsets. - Definition fsub (a b : A0) (H : emb a b) (x : sub a) : + Definition fsub (a b : A0) (H : emb a b) (x : sub a) : sub b := Build_sub _ (witness _ x) (emb_trans _ _ _ (emb_wit _ x) H). (* F is a morphism: a < b => F(a) < F(b) diff --git a/test-suite/failure/universes3.v b/test-suite/failure/universes3.v index 427cec190..8fb414d5a 100644 --- a/test-suite/failure/universes3.v +++ b/test-suite/failure/universes3.v @@ -15,7 +15,7 @@ Inductive I (B:Type (*6*)) := C : B -> impl Prop (I B). where Type(7) is the auxiliary level used to infer the type of I *) -(* We cannot enforce Type1 < Type(6) while we already have +(* We cannot enforce Type1 < Type(6) while we already have Type(6) <= Type(7) < Type3 < Type1 *) Definition J := I Type1. diff --git a/test-suite/ideal-features/Case9.v b/test-suite/ideal-features/Case9.v index 800c431ec..d95c21084 100644 --- a/test-suite/ideal-features/Case9.v +++ b/test-suite/ideal-features/Case9.v @@ -6,7 +6,7 @@ CoInductive hdlist : unit -> Type := Variable P : forall bo, hdlist bo -> Prop. Variable all : forall bo l, P bo l. -Definition F (l:hdlist tt) : P tt l := +Definition F (l:hdlist tt) : P tt l := match l in hdlist u return P u l with | cons (cons l') => all tt _ end. diff --git a/test-suite/ideal-features/complexity/evars_subst.v b/test-suite/ideal-features/complexity/evars_subst.v index 6f9f86a95..b3dfb33cd 100644 --- a/test-suite/ideal-features/complexity/evars_subst.v +++ b/test-suite/ideal-features/complexity/evars_subst.v @@ -3,12 +3,12 @@ (* Let n be the number of let-in. The complexity comes from the fact that each implicit arguments of f was in a larger and larger - context. To compute the type of "let _ := f ?Tn 0 in f ?T 0", + context. To compute the type of "let _ := f ?Tn 0 in f ?T 0", "f ?Tn 0" is substituted in the type of "f ?T 0" which is ?T. This type is an evar instantiated on the n variables denoting the "f ?Ti 0". One obtain "?T[1;...;n-1;f ?Tn[1;...;n-1] 0]". To compute the type of "let _ := f ?Tn-1 0 in let _ := f ?Tn 0 in f ?T 0", another - substitution is done leading to + substitution is done leading to "?T[1;...;n-2;f ?Tn[1;...;n-2] 0;f ?Tn[1;...;n-2;f ?Tn[1;...;n-2] 0] 0]" and so on. At the end, we get a term of exponential size *) @@ -25,7 +25,7 @@ Time Check let _ := f _ 0 in let _ := f _ 0 in let _ := f _ 0 in - + let _ := f _ 0 in let _ := f _ 0 in let _ := f _ 0 in diff --git a/test-suite/ideal-features/eapply_evar.v b/test-suite/ideal-features/eapply_evar.v index b10d5dbf9..8c9a448e7 100644 --- a/test-suite/ideal-features/eapply_evar.v +++ b/test-suite/ideal-features/eapply_evar.v @@ -1,9 +1,9 @@ (* Test propagation of evars from subgoal to brother subgoals *) -(* This does not work (oct 2008) because "match goal" sees "?evar = O" +(* This does not work (oct 2008) because "match goal" sees "?evar = O" and not "O = O" Lemma eapply_evar : O=O -> 0=O. -intro H; eapply trans_equal; +intro H; eapply trans_equal; [apply H | match goal with |- ?x = ?x => reflexivity end]. Qed. diff --git a/test-suite/ideal-features/evars_subst.v b/test-suite/ideal-features/evars_subst.v index 6f9f86a95..b3dfb33cd 100644 --- a/test-suite/ideal-features/evars_subst.v +++ b/test-suite/ideal-features/evars_subst.v @@ -3,12 +3,12 @@ (* Let n be the number of let-in. The complexity comes from the fact that each implicit arguments of f was in a larger and larger - context. To compute the type of "let _ := f ?Tn 0 in f ?T 0", + context. To compute the type of "let _ := f ?Tn 0 in f ?T 0", "f ?Tn 0" is substituted in the type of "f ?T 0" which is ?T. This type is an evar instantiated on the n variables denoting the "f ?Ti 0". One obtain "?T[1;...;n-1;f ?Tn[1;...;n-1] 0]". To compute the type of "let _ := f ?Tn-1 0 in let _ := f ?Tn 0 in f ?T 0", another - substitution is done leading to + substitution is done leading to "?T[1;...;n-2;f ?Tn[1;...;n-2] 0;f ?Tn[1;...;n-2;f ?Tn[1;...;n-2] 0] 0]" and so on. At the end, we get a term of exponential size *) @@ -25,7 +25,7 @@ Time Check let _ := f _ 0 in let _ := f _ 0 in let _ := f _ 0 in - + let _ := f _ 0 in let _ := f _ 0 in let _ := f _ 0 in diff --git a/test-suite/ideal-features/implicit_binders.v b/test-suite/ideal-features/implicit_binders.v index 5b66944b5..2ec727808 100644 --- a/test-suite/ideal-features/implicit_binders.v +++ b/test-suite/ideal-features/implicit_binders.v @@ -1,8 +1,8 @@ (** * Questions de syntaxe autour de la généralisation implicite ** Lieurs de classes - Aujourd'hui, les lieurs de classe [ ] et les - lieurs {{ }} sont équivalents et on a toutes les combinaisons de { et ( pour + Aujourd'hui, les lieurs de classe [ ] et les + lieurs {{ }} sont équivalents et on a toutes les combinaisons de { et ( pour les lieurs de classes (où la variable liée peut être anonyme): *) @@ -22,7 +22,7 @@ Definition bar₄ {( F : Foo A )} (x y : A) := foo x + foo y. (** Les lieurs sont généralisés à tous les termes, pas seulement aux classes: *) -Definition relation A := A -> A -> Prop. +Definition relation A := A -> A -> Prop. Definition inverse {( R : relation A )} := fun x y => R y x. @@ -43,7 +43,7 @@ Definition inverse {( R : relation A )} := fun x y => R y x. [Definition inverse _{R : relation A} := fun x y => R y x] [Definition inverse `(R : relation A) := fun x y => R y x] et - + [Definition inverse `[R : relation A] := fun x y => R y x] ou [Definition inverse `{R : relation A} := fun x y => R y x] @@ -53,7 +53,7 @@ Definition inverse {( R : relation A )} := fun x y => R y x. Definition div (x : nat) ({ y <> 0 }) := 0. -(** Un choix à faire pour les inductifs: accepter ou non de ne pas donner de nom à +(** Un choix à faire pour les inductifs: accepter ou non de ne pas donner de nom à l'argument. Manque de variables anonymes pour l'utilisateur mais pas pour le système... *) Inductive bla [ Foo A ] : Type :=. @@ -73,10 +73,10 @@ Definition instimpl ({ SomeStruct a }) : nat := a + a. (** Donne l'instance explicitement (façon foncteur). *) -Definition foo_prod {( Foo A, Foo B )} : Foo (A * B) := +Definition foo_prod {( Foo A, Foo B )} : Foo (A * B) := fun x => let (l, r) := x in foo l + foo r. -(** *** Questions: +(** *** Questions: - Gardez les crochets [ ] pour {{ }} ? - Quelle syntaxe pour la généralisation ? - Veut-on toutes les combinaisons de statut pour les variables généralisées et la variable liée ? @@ -98,12 +98,12 @@ Definition baz := `{x + y + z = x + (y + z)}. Print baz. (** Proposition d'Arthur C.: déclarer les noms de variables généralisables à la [Implicit Types] - pour plus de robustesse (cela vaudrait aussi pour les lieurs). Les typos du genre de l'exemple suivant + pour plus de robustesse (cela vaudrait aussi pour les lieurs). Les typos du genre de l'exemple suivant ne sont plus silencieuses: *) Check `(foob 0 + x). -(** Utilisé pour généraliser l'implémentation de la généralisation implicite dans +(** Utilisé pour généraliser l'implémentation de la généralisation implicite dans les déclarations d'instances (i.e. les deux defs suivantes sont équivalentes). *) Instance fooa : Foo A. @@ -111,8 +111,8 @@ Admitted. Definition fooa' : `(Foo A). Admitted. -(** Un peu différent de la généralisation des lieurs qui "explosent" les variables - libres en les liant au même niveau que l'objet. Dans la deuxième defs [a] n'est pas lié dans +(** Un peu différent de la généralisation des lieurs qui "explosent" les variables + libres en les liant au même niveau que l'objet. Dans la deuxième defs [a] n'est pas lié dans la définition mais [F : Πa, SomeStruct a]. *) Definition qux {( F : SomeStruct a )} : nat := a. diff --git a/test-suite/ideal-features/universes.v b/test-suite/ideal-features/universes.v index 6db4cfe18..49530ebce 100644 --- a/test-suite/ideal-features/universes.v +++ b/test-suite/ideal-features/universes.v @@ -7,7 +7,7 @@ Definition Ty := Type (* Top.1 *). Inductive Q (A:Type (* Top.2 *)) : Prop := q : A -> Q A. Inductive T (B:Type (* Top.3 *)) := t : B -> Q (T B) -> T B. -(* ajoute Top.4 <= Top.2 inutilement: +(* ajoute Top.4 <= Top.2 inutilement: 4 est l'univers utilisé dans le calcul du type polymorphe de T *) Definition C := T Ty. (* ajoute Top.1 < Top.3 : @@ -23,7 +23,7 @@ Definition C := T Ty. Definition f (A:Type (* Top.1 *)) := True. Inductive R := r : f R -> R. -(* ajoute Top.3 <= Top.1 inutilement: +(* ajoute Top.3 <= Top.1 inutilement: Top.3 est l'univers utilisé dans le calcul du type polymorphe de R *) (* mais il manque la contrainte que l'univers de R est plus petit que Top.1 diff --git a/test-suite/interactive/Evar.v b/test-suite/interactive/Evar.v index 1bc1f71d5..50c5bba0f 100644 --- a/test-suite/interactive/Evar.v +++ b/test-suite/interactive/Evar.v @@ -1,6 +1,6 @@ (* Check that no toplevel "unresolved evar" flees through Declare Implicit Tactic support (bug #1229) *) -Goal True. +Goal True. (* should raise an error, not an anomaly *) set (x := _). diff --git a/test-suite/micromega/example.v b/test-suite/micromega/example.v index 5cb103953..f424f0fcc 100644 --- a/test-suite/micromega/example.v +++ b/test-suite/micromega/example.v @@ -19,7 +19,7 @@ Lemma not_so_easy : forall x n : Z, 2*x + 1 <= 2 *n -> x <= n-1. Proof. intros. - lia. + lia. Qed. @@ -27,19 +27,19 @@ Qed. Lemma some_pol : forall x, 4 * x ^ 2 + 3 * x + 2 >= 0. Proof. - intros. + intros. psatz Z 2. Qed. -Lemma Zdiscr: forall a b c x, +Lemma Zdiscr: forall a b c x, a * x ^ 2 + b * x + c = 0 -> b ^ 2 - 4 * a * c >= 0. Proof. intros ; psatz Z 4. Qed. -Lemma plus_minus : forall x y, +Lemma plus_minus : forall x y, 0 = x + y -> 0 = x -y -> 0 = x /\ 0 = y. Proof. intros. @@ -48,20 +48,20 @@ Qed. -Lemma mplus_minus : forall x y, +Lemma mplus_minus : forall x y, x + y >= 0 -> x -y >= 0 -> x^2 - y^2 >= 0. Proof. intros; psatz Z 2. Qed. -Lemma pol3: forall x y, 0 <= x + y -> +Lemma pol3: forall x y, 0 <= x + y -> x^3 + 3*x^2*y + 3*x* y^2 + y^3 >= 0. Proof. intros; psatz Z 4. Qed. -(* Motivating example from: Expressiveness + Automation + Soundness: +(* Motivating example from: Expressiveness + Automation + Soundness: Towards COmbining SMT Solvers and Interactive Proof Assistants *) Parameter rho : Z. Parameter rho_ge : rho >= 0. @@ -76,7 +76,7 @@ Definition rbound2 (C:Z -> Z -> Z) : Prop := Lemma bounded_drift : forall s t p q C D, s <= t /\ correct p t /\ correct q t /\ - rbound1 C /\ rbound2 C /\ rbound1 D /\ rbound2 D -> + rbound1 C /\ rbound2 C /\ rbound1 D /\ rbound2 D -> Zabs (C p t - D q t) <= Zabs (C p s - D q s) + 2 * rho * (t- s). Proof. intros. @@ -194,8 +194,8 @@ Qed. (* from hol_light/Examples/sos.ml *) Lemma hol_light1 : forall a1 a2 b1 b2, - a1 >= 0 -> a2 >= 0 -> - (a1 * a1 + a2 * a2 = b1 * b1 + b2 * b2 + 2) -> + a1 >= 0 -> a2 >= 0 -> + (a1 * a1 + a2 * a2 = b1 * b1 + b2 * b2 + 2) -> (a1 * b1 + a2 * b2 = 0) -> a1 * a2 - b1 * b2 >= 0. Proof. intros ; psatz Z 4. @@ -323,7 +323,7 @@ Proof. Qed. -Lemma hol_light24 : forall x1 y1 x2 y2, x1 >= 0 -> x2 >= 0 -> y1 >= 0 -> y2 >= 0 -> +Lemma hol_light24 : forall x1 y1 x2 y2, x1 >= 0 -> x2 >= 0 -> y1 >= 0 -> y2 >= 0 -> ((x1 + y1) ^2 + x1 + 1 = (x2 + y2) ^ 2 + x2 + 1) -> (x1 + y1 = x2 + y2). Proof. diff --git a/test-suite/micromega/heap3_vcgen_25.v b/test-suite/micromega/heap3_vcgen_25.v index 0298303f5..efb5c7fd5 100644 --- a/test-suite/micromega/heap3_vcgen_25.v +++ b/test-suite/micromega/heap3_vcgen_25.v @@ -11,7 +11,7 @@ Require Import Psatz. Open Scope Z_scope. -Lemma vcgen_25 : forall +Lemma vcgen_25 : forall (n : Z) (m : Z) (jt : Z) diff --git a/test-suite/micromega/qexample.v b/test-suite/micromega/qexample.v index 1fa250e09..c9c779f90 100644 --- a/test-suite/micromega/qexample.v +++ b/test-suite/micromega/qexample.v @@ -10,7 +10,7 @@ Require Import Psatz. Require Import QArith. Require Import Ring_normalize. -Lemma plus_minus : forall x y, +Lemma plus_minus : forall x y, 0 == x + y -> 0 == x -y -> 0 == x /\ 0 == y. Proof. intros. @@ -37,7 +37,7 @@ Qed. Open Scope Z_scope. Open Scope Q_scope. -Lemma vcgen_25 : forall +Lemma vcgen_25 : forall (n : Q) (m : Q) (jt : Q) diff --git a/test-suite/micromega/rexample.v b/test-suite/micromega/rexample.v index d7386a4ec..c957add69 100644 --- a/test-suite/micromega/rexample.v +++ b/test-suite/micromega/rexample.v @@ -12,7 +12,7 @@ Require Import Ring_normalize. Open Scope R_scope. -Lemma yplus_minus : forall x y, +Lemma yplus_minus : forall x y, 0 = x + y -> 0 = x -y -> 0 = x /\ 0 = y. Proof. intros. @@ -34,7 +34,7 @@ Proof. Qed. -Lemma vcgen_25 : forall +Lemma vcgen_25 : forall (n : R) (m : R) (jt : R) diff --git a/test-suite/micromega/square.v b/test-suite/micromega/square.v index b78bba25c..4c00ffe4a 100644 --- a/test-suite/micromega/square.v +++ b/test-suite/micromega/square.v @@ -20,7 +20,7 @@ Proof. intros [n [p [Heq Hnz]]]; pose (n' := Zabs n); pose (p':=Zabs p). assert (facts : 0 <= Zabs n /\ 0 <= Zabs p /\ Zabs n^2=n^2 /\ Zabs p^2 = p^2) by auto. -assert (H : (0 < n' /\ 0 <= p' /\ n' ^2 = 2* p' ^2)) by +assert (H : (0 < n' /\ 0 <= p' /\ n' ^2 = 2* p' ^2)) by (destruct facts as [Hf1 [Hf2 [Hf3 Hf4]]]; unfold n', p' ; psatz Z 2). generalize p' H; elim n' using (well_founded_ind (Zwf_well_founded 0)); clear. intros n IHn p [Hn [Hp Heq]]. @@ -55,7 +55,7 @@ Theorem sqrt2_not_rational : ~exists x:Q, x^2==2#1. Proof. unfold Qeq; intros [x]; simpl (Qden (2#1)); rewrite Zmult_1_r. intros HQeq. - assert (Heq : (Qnum x ^ 2 = 2 * ' Qden x ^ 2%Q)%Z) by + assert (Heq : (Qnum x ^ 2 = 2 * ' Qden x ^ 2%Q)%Z) by (rewrite QnumZpower in HQeq ; rewrite QdenZpower in HQeq ; auto). assert (Hnx : (Qnum x <> 0)%Z) by (intros Hx; simpl in HQeq; rewrite Hx in HQeq; discriminate HQeq). diff --git a/test-suite/micromega/zomicron.v b/test-suite/micromega/zomicron.v index 60c16a998..3b2460233 100644 --- a/test-suite/micromega/zomicron.v +++ b/test-suite/micromega/zomicron.v @@ -24,7 +24,7 @@ Lemma omega_nightmare : forall x y, 27 <= 11 * x + 13 * y <= 45 -> -10 <= 7 * x Proof. intros ; intuition auto. lia. -Qed. +Qed. Lemma compact_proof : forall z, (z < 0) -> @@ -32,5 +32,5 @@ Lemma compact_proof : forall z, (0 >= z \/ 0 < z) -> False. Proof. intros. - lia. + lia. Qed.
\ No newline at end of file diff --git a/test-suite/modules/PO.v b/test-suite/modules/PO.v index 354c3957f..71d331772 100644 --- a/test-suite/modules/PO.v +++ b/test-suite/modules/PO.v @@ -7,11 +7,11 @@ Implicit Arguments snd. Module Type PO. Parameter T : Set. Parameter le : T -> T -> Prop. - + Axiom le_refl : forall x : T, le x x. Axiom le_trans : forall x y z : T, le x y -> le y z -> le x z. Axiom le_antis : forall x y : T, le x y -> le y x -> x = y. - + Hint Resolve le_refl le_trans le_antis. End PO. @@ -28,10 +28,10 @@ Module Pair (X: PO) (Y: PO) <: PO. Lemma le_trans : forall p1 p2 p3 : T, le p1 p2 -> le p2 p3 -> le p1 p3. unfold le in |- *; intuition; info eauto. - Qed. + Qed. Lemma le_antis : forall p1 p2 : T, le p1 p2 -> le p2 p1 -> p1 = p2. - destruct p1. + destruct p1. destruct p2. unfold le in |- *. intuition. diff --git a/test-suite/modules/Przyklad.v b/test-suite/modules/Przyklad.v index 014f6c604..e3694b818 100644 --- a/test-suite/modules/Przyklad.v +++ b/test-suite/modules/Przyklad.v @@ -1,4 +1,4 @@ -Definition ifte (T : Set) (A B : Prop) (s : {A} + {B}) +Definition ifte (T : Set) (A B : Prop) (s : {A} + {B}) (th el : T) := if s then th else el. Implicit Arguments ifte. @@ -33,7 +33,7 @@ Module Type ELEM. Parameter T : Set. Parameter eq_dec : forall a a' : T, {a = a'} + {a <> a'}. End ELEM. - + Module Type SET (Elt: ELEM). Parameter T : Set. Parameter empty : T. @@ -104,11 +104,11 @@ Module Nat. End Nat. -Module SetNat := F Nat. +Module SetNat := F Nat. -Lemma no_zero_in_empty : SetNat.find 0 SetNat.empty = false. -apply SetNat.find_empty_false. +Lemma no_zero_in_empty : SetNat.find 0 SetNat.empty = false. +apply SetNat.find_empty_false. Qed. (***************************************************************************) @@ -120,8 +120,8 @@ Module Lemmas (G: SET) (E: ELEM). forall (S : ESet.T) (a1 a2 : E.T), let S1 := ESet.add a1 (ESet.add a2 S) in let S2 := ESet.add a2 (ESet.add a1 S) in - forall a : E.T, ESet.find a S1 = ESet.find a S2. - + forall a : E.T, ESet.find a S1 = ESet.find a S2. + intros. unfold S1, S2 in |- *. elim (E.eq_dec a a1); elim (E.eq_dec a a2); intros H1 H2; @@ -137,10 +137,10 @@ Inductive list (A : Set) : Set := | nil : list A | cons : A -> list A -> list A. -Module ListDict (E: ELEM). +Module ListDict (E: ELEM). Definition T := list E.T. Definition elt := E.T. - + Definition empty := nil elt. Definition add (e : elt) (s : T) := cons elt e s. Fixpoint find (e : elt) (s : T) {struct s} : bool := @@ -160,7 +160,7 @@ Module ListDict (E: ELEM). auto. Qed. - + Lemma find_add_false : forall (s : T) (e e' : E.T), e <> e' -> find e (add e' s) = find e s. @@ -171,8 +171,8 @@ Module ListDict (E: ELEM). rewrite H0. simpl in |- *. reflexivity. - Qed. - + Qed. + End ListDict. diff --git a/test-suite/modules/Tescik.v b/test-suite/modules/Tescik.v index 8dadace77..1d1b1e0ab 100644 --- a/test-suite/modules/Tescik.v +++ b/test-suite/modules/Tescik.v @@ -7,20 +7,20 @@ End ELEM. Module Nat. Definition A := nat. Definition x := 0. -End Nat. +End Nat. Module List (X: ELEM). Inductive list : Set := | nil : list | cons : X.A -> list -> list. - + Definition head (l : list) := match l with | nil => X.x | cons x _ => x end. Definition singl (x : X.A) := cons x nil. - + Lemma head_singl : forall x : X.A, head (singl x) = x. auto. Qed. diff --git a/test-suite/modules/fun_objects.v b/test-suite/modules/fun_objects.v index f4dc19b3e..dce2ffd50 100644 --- a/test-suite/modules/fun_objects.v +++ b/test-suite/modules/fun_objects.v @@ -4,7 +4,7 @@ Unset Strict Implicit. Module Type SIG. Parameter id : forall A : Set, A -> A. End SIG. - + Module M (X: SIG). Definition idid := X.id X.id. Definition id := idid X.id. diff --git a/test-suite/modules/injection_discriminate_inversion.v b/test-suite/modules/injection_discriminate_inversion.v index 88c19cb1a..d4ac7b3a2 100644 --- a/test-suite/modules/injection_discriminate_inversion.v +++ b/test-suite/modules/injection_discriminate_inversion.v @@ -7,18 +7,18 @@ Module M1 := M. Goal forall x, M.C x = M1.C 0 -> x = 0 . intros x H. - (* - injection sur deux constructeurs egaux mais appeles - par des modules differents + (* + injection sur deux constructeurs egaux mais appeles + par des modules differents *) - injection H. + injection H. tauto. Qed. Goal M.C 0 <> M1.C 1. - (* - Discriminate sur deux constructeurs egaux mais appeles - par des modules differents + (* + Discriminate sur deux constructeurs egaux mais appeles + par des modules differents *) intro H;discriminate H. Qed. @@ -26,9 +26,9 @@ Qed. Goal forall x, M.C x = M1.C 0 -> x = 0. intros x H. - (* - inversion sur deux constructeurs egaux mais appeles - par des modules differents + (* + inversion sur deux constructeurs egaux mais appeles + par des modules differents *) inversion H. reflexivity. Qed.
\ No newline at end of file diff --git a/test-suite/modules/mod_decl.v b/test-suite/modules/mod_decl.v index b886eb59d..8b40213a4 100644 --- a/test-suite/modules/mod_decl.v +++ b/test-suite/modules/mod_decl.v @@ -31,17 +31,17 @@ Module Type T. Module M0. Axiom A : Set. End M0. - + Declare Module M1: SIG. - + Module M2 <: SIG. Definition A := nat. End M2. - + Module M3 := M0. - + Module M4 : SIG := M0. - + Module M5 <: SIG := M0. Module M6 := F M0. diff --git a/test-suite/modules/modeq.v b/test-suite/modules/modeq.v index 45cf9f124..1238ee9de 100644 --- a/test-suite/modules/modeq.v +++ b/test-suite/modules/modeq.v @@ -19,4 +19,4 @@ Module Z. Module N := M. End Z. -Module A : SIG := Z.
\ No newline at end of file +Module A : SIG := Z.
\ No newline at end of file diff --git a/test-suite/modules/modul.v b/test-suite/modules/modul.v index 9d24d6ce4..36a542ef0 100644 --- a/test-suite/modules/modul.v +++ b/test-suite/modules/modul.v @@ -6,7 +6,7 @@ Module M. Hint Resolve w. (* <Warning> : Grammar is replaced by Notation *) - + Print Hint *. Lemma w1 : rel 0 1. diff --git a/test-suite/modules/obj.v b/test-suite/modules/obj.v index 97337a125..fda1a074a 100644 --- a/test-suite/modules/obj.v +++ b/test-suite/modules/obj.v @@ -1,7 +1,7 @@ Set Implicit Arguments. Unset Strict Implicit. -Module M. +Module M. Definition a (s : Set) := s. Print a. End M. diff --git a/test-suite/modules/objects.v b/test-suite/modules/objects.v index 070f859ea..d3a4c0b05 100644 --- a/test-suite/modules/objects.v +++ b/test-suite/modules/objects.v @@ -2,7 +2,7 @@ Module Type SET. Axiom T : Set. Axiom x : T. End SET. - + Set Implicit Arguments. Unset Strict Implicit. diff --git a/test-suite/modules/objects2.v b/test-suite/modules/objects2.v index e286609e5..220e2b369 100644 --- a/test-suite/modules/objects2.v +++ b/test-suite/modules/objects2.v @@ -4,7 +4,7 @@ (* Bug #1118 (simplified version), submitted by Evelyne Contejean (used to failed in pre-V8.1 trunk because of a call to lookup_mind - for structure objects) + for structure objects) *) Module Type S. Record t : Set := { a : nat; b : nat }. End S. diff --git a/test-suite/modules/sig.v b/test-suite/modules/sig.v index 4cb6291df..da5d25fa2 100644 --- a/test-suite/modules/sig.v +++ b/test-suite/modules/sig.v @@ -18,8 +18,8 @@ Module Type SPRYT. End N. End SPRYT. -Module K : SPRYT := N. -Module K' : SPRYT := M. +Module K : SPRYT := N. +Module K' : SPRYT := M. Module Type SIG. Definition T : Set := M.N.T. diff --git a/test-suite/modules/sub_objects.v b/test-suite/modules/sub_objects.v index 5eec07758..fdfd09f80 100644 --- a/test-suite/modules/sub_objects.v +++ b/test-suite/modules/sub_objects.v @@ -12,7 +12,7 @@ Module M. Module N. Definition idid (A : Set) (x : A) := id x. (* <Warning> : Grammar is replaced by Notation *) - Notation inc := (plus 1). + Notation inc := (plus 1). End N. Definition zero := N.idid 0. diff --git a/test-suite/modules/subtyping.v b/test-suite/modules/subtyping.v index 2df8e84e5..dd7daf429 100644 --- a/test-suite/modules/subtyping.v +++ b/test-suite/modules/subtyping.v @@ -15,7 +15,7 @@ Module Type T. Parameter A : Type (* Top.1 *) . - Inductive L : Type (* max(Top.1,1) *) := + Inductive L : Type (* max(Top.1,1) *) := | L0 | L1 : (A -> Prop) -> L. @@ -23,17 +23,17 @@ End T. Axiom Tp : Type (* Top.5 *) . -Module TT : T. +Module TT : T. Definition A : Type (* Top.6 *) := Tp. (* generates Top.5 <= Top.6 *) - Inductive L : Type (* max(Top.6,1) *) := + Inductive L : Type (* max(Top.6,1) *) := | L0 | L1 : (A -> Prop) -> L. End TT. (* Generates Top.6 <= Top.1 (+ auxiliary constraints for L_rect) *) -(* Note: Top.6 <= Top.1 is generated by subtyping on A; +(* Note: Top.6 <= Top.1 is generated by subtyping on A; subtyping of L follows and has not to be checked *) diff --git a/test-suite/output/Cases.v b/test-suite/output/Cases.v index 37ee71e95..b63375867 100644 --- a/test-suite/output/Cases.v +++ b/test-suite/output/Cases.v @@ -12,7 +12,7 @@ Require Import Arith. Definition proj (x y:nat) (P:nat -> Type) (def:P x) (prf:P y) : P y := match eq_nat_dec x y return P y with - | left eqprf => + | left eqprf => match eqprf in (_ = z) return (P z) with | refl_equal => def end diff --git a/test-suite/output/Fixpoint.v b/test-suite/output/Fixpoint.v index 2b13c2041..af5f05f65 100644 --- a/test-suite/output/Fixpoint.v +++ b/test-suite/output/Fixpoint.v @@ -1,7 +1,7 @@ Require Import List. Check - (fix F (A B : Set) (f : A -> B) (l : list A) {struct l} : + (fix F (A B : Set) (f : A -> B) (l : list A) {struct l} : list B := match l with | nil => nil | a :: l => f a :: F _ _ f l diff --git a/test-suite/output/Notations.v b/test-suite/output/Notations.v index b37c3638a..8d16dff5b 100644 --- a/test-suite/output/Notations.v +++ b/test-suite/output/Notations.v @@ -64,26 +64,26 @@ Open Scope nat_scope. Inductive znat : Set := Zpos (n : nat) | Zneg (m : nat). Coercion Zpos: nat >-> znat. - + Delimit Scope znat_scope with znat. Open Scope znat_scope. - + Variable addz : znat -> znat -> znat. Notation "z1 + z2" := (addz z1 z2) : znat_scope. (* Check that "3+3", where 3 is in nat and the coercion to znat is implicit, - is printed the same way, and not "S 2 + S 2" as if numeral printing was + is printed the same way, and not "S 2 + S 2" as if numeral printing was only tested with coercion still present *) Check (3+3). (**********************************************************************) (* Check recursive notations *) - + Require Import List. Notation "[ x ; .. ; y ]" := (cons x .. (cons y nil) ..). Check [1;2;4]. - + Reserved Notation "( x ; y , .. , z )" (at level 0). Notation "( x ; y , .. , z )" := (pair .. (pair x y) .. z). Check (1;2,4). @@ -102,7 +102,7 @@ Check (pred 3). Check (fun n => match n with 0 => 0 | S n => n end). Check (fun n => match n with S p as x => p | y => 0 end). -Notation "'ifn' x 'is' 'succ' n 'then' t 'else' u" := +Notation "'ifn' x 'is' 'succ' n 'then' t 'else' u" := (match x with O => u | S n => t end) (at level 0, u at level 0). Check fun x => ifn x is succ n then n else 0. diff --git a/test-suite/output/reduction.v b/test-suite/output/reduction.v index 4a460a83f..c4592369f 100644 --- a/test-suite/output/reduction.v +++ b/test-suite/output/reduction.v @@ -9,5 +9,5 @@ Eval simpl in (fix plus (n m : nat) {struct n} : nat := | S p => S (p + m) end) a a. -Eval hnf in match (plus (S n) O) with S n => n | _ => O end. +Eval hnf in match (plus (S n) O) with S n => n | _ => O end. 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. diff --git a/test-suite/typeclasses/clrewrite.v b/test-suite/typeclasses/clrewrite.v index 2978fda26..f21acd4cb 100644 --- a/test-suite/typeclasses/clrewrite.v +++ b/test-suite/typeclasses/clrewrite.v @@ -15,7 +15,7 @@ Section Equiv. Qed. Tactic Notation "simpl" "*" := auto || relation_tac. - + Goal eqA x y -> eqA y x /\ True. intros H ; clrewrite H. split ; simpl*. @@ -27,13 +27,13 @@ Section Equiv. Qed. Goal eqA x y -> eqA y z -> eqA x y. - intros H. + intros H. clrewrite H. intro. refl. Qed. - + Goal eqA x y -> eqA z y -> eqA x y. - intros H. + intros H. clrewrite <- H at 2. clrewrite <- H at 1. intro. refl. @@ -54,7 +54,7 @@ Section Equiv. clrewrite <- H. refl. Qed. - + Goal eqA x y -> True /\ True /\ False /\ eqA x x -> True /\ True /\ False /\ eqA x y. Proof. intros. @@ -70,12 +70,12 @@ Section Trans. Variables x y z w : A. Tactic Notation "simpl" "*" := auto || relation_tac. - + (* Typeclasses eauto := debug. *) Goal R x y -> R y x -> R y y -> R x x. Proof with auto. - intros H H' H''. + intros H H' H''. clrewrite <- H' at 2. clrewrite H at 1... @@ -86,11 +86,11 @@ Section Trans. clrewrite H. refl. Qed. - + Goal R x y -> R z y -> R x y. - intros H. + intros H. clrewrite <- H at 2. - intro. + intro. clrewrite H at 1. Abort. |