diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-12-21 23:50:17 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-12-21 23:50:17 +0000 |
| commit | 4d4f08acb5e5f56d38289e5629173bc1b8b5fd57 (patch) | |
| tree | c160d442d54dbd15cbd0ab3500cdf94d0a6da74e /test-suite/success | |
| parent | 960859c0c10e029f9768d0d70addeca8f6b6d784 (diff) | |
Abandon tests syntaxe v7; remplacement des .v par des fichiers en syntaxe v8
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7693 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite/success')
87 files changed, 3463 insertions, 2999 deletions
diff --git a/test-suite/success/Abstract.v8 b/test-suite/success/Abstract.v index 21a985bcd..fc8800a56 100644 --- a/test-suite/success/Abstract.v8 +++ b/test-suite/success/Abstract.v @@ -24,3 +24,4 @@ induction n. Defined. End S. + diff --git a/test-suite/success/Case1.v b/test-suite/success/Case1.v index 2d5a51345..ea9b654de 100644 --- a/test-suite/success/Case1.v +++ b/test-suite/success/Case1.v @@ -2,14 +2,14 @@ Section NATIND2. Variable P : nat -> Type. -Variable H0 : (P O). -Variable H1 : (P (S O)). -Variable H2 : (n:nat)(P n)->(P (S (S n))). -Fixpoint nat_ind2 [n:nat] : (P n) := - <P>Cases n of - O => H0 - | (S O) => H1 - | (S (S n)) => (H2 n (nat_ind2 n)) - end. +Variable H0 : P 0. +Variable H1 : P 1. +Variable H2 : forall n : nat, P n -> P (S (S n)). +Fixpoint nat_ind2 (n : nat) : P n := + match n as x return (P x) with + | O => H0 + | S O => H1 + | S (S n) => H2 n (nat_ind2 n) + end. End NATIND2. diff --git a/test-suite/success/Case10.v b/test-suite/success/Case10.v index 73413c475..378859e98 100644 --- a/test-suite/success/Case10.v +++ b/test-suite/success/Case10.v @@ -2,25 +2,27 @@ (* To test compilation of dependent case *) (* Multiple Patterns *) (* ============================================== *) -Inductive skel: Type := - PROP: skel - | PROD: skel->skel->skel. +Inductive skel : Type := + | PROP : skel + | PROD : skel -> skel -> skel. Parameter Can : skel -> Type. -Parameter default_can : (s:skel) (Can s). +Parameter default_can : forall s : skel, Can s. -Type [s1,s2:skel] - <[s1,_:skel](Can s1)>Cases s1 s2 of - PROP PROP => (default_can PROP) - | s1 _ => (default_can s1) - end. +Type + (fun s1 s2 : skel => + match s1, s2 return (Can s1) with + | PROP, PROP => default_can PROP + | s1, _ => default_can s1 + end). -Type [s1,s2:skel] -<[s1:skel][_:skel](Can s1)>Cases s1 s2 of - PROP PROP => (default_can PROP) -| (PROP as s) _ => (default_can s) -| ((PROD s1 s2) as s) PROP => (default_can s) -| ((PROD s1 s2) as s) _ => (default_can s) -end. +Type + (fun s1 s2 : skel => + match s1, s2 return (Can s1) with + | PROP, PROP => default_can PROP + | PROP as s, _ => default_can s + | PROD s1 s2 as s, PROP => default_can s + | PROD s1 s2 as s, _ => default_can s + end). diff --git a/test-suite/success/Case11.v b/test-suite/success/Case11.v index 580cd87d1..fd5d139c6 100644 --- a/test-suite/success/Case11.v +++ b/test-suite/success/Case11.v @@ -3,9 +3,11 @@ Section A. -Variables Alpha:Set; Beta:Set. +Variables (Alpha : Set) (Beta : Set). -Definition nodep_prod_of_dep: (sigS Alpha [a:Alpha]Beta)-> Alpha*Beta:= -[c] Cases c of (existS a b)=>(a,b) end. +Definition nodep_prod_of_dep (c : sigS (fun a : Alpha => Beta)) : + Alpha * Beta := match c with + | existS a b => (a, b) + end. End A. diff --git a/test-suite/success/Case12.v b/test-suite/success/Case12.v index 284695f41..20073aa73 100644 --- a/test-suite/success/Case12.v +++ b/test-suite/success/Case12.v @@ -1,60 +1,59 @@ (* This example was proposed by Cuihtlauac ALVARADO *) -Require PolyList. +Require Import List. -Fixpoint mult2 [n:nat] : nat := -Cases n of -| O => O -| (S n) => (S (S (mult2 n))) -end. +Fixpoint mult2 (n : nat) : nat := + match n with + | O => 0 + | S n => S (S (mult2 n)) + end. Inductive list : nat -> Set := -| nil : (list O) -| cons : (n:nat)(list (mult2 n))->(list (S (S (mult2 n)))). + | nil : list 0 + | cons : forall n : nat, list (mult2 n) -> list (S (S (mult2 n))). Type -[P:((n:nat)(list n)->Prop); - f:(P O nil); - f0:((n:nat; l:(list (mult2 n))) - (P (mult2 n) l)->(P (S (S (mult2 n))) (cons n l)))] - Fix F - {F [n:nat; l:(list n)] : (P n l) := - <P>Cases l of - nil => f - | (cons n0 l0) => (f0 n0 l0 (F (mult2 n0) l0)) - end}. + (fun (P : forall n : nat, list n -> Prop) (f : P 0 nil) + (f0 : forall (n : nat) (l : list (mult2 n)), + P (mult2 n) l -> P (S (S (mult2 n))) (cons n l)) => + fix F (n : nat) (l : list n) {struct l} : P n l := + match l as x0 in (list x) return (P x x0) with + | nil => f + | cons n0 l0 => f0 n0 l0 (F (mult2 n0) l0) + end). Inductive list' : nat -> Set := -| nil' : (list' O) -| cons' : (n:nat)[m:=(mult2 n)](list' m)->(list' (S (S m))). + | nil' : list' 0 + | cons' : forall n : nat, let m := mult2 n in list' m -> list' (S (S m)). -Fixpoint length [n; l:(list' n)] : nat := - Cases l of - nil' => O - | (cons' _ m l0) => (S (length m l0)) +Fixpoint length n (l : list' n) {struct l} : nat := + match l with + | nil' => 0 + | cons' _ m l0 => S (length m l0) end. Type -[P:((n:nat)(list' n)->Prop); - f:(P O nil'); - f0:((n:nat) - [m:=(mult2 n)](l:(list' m))(P m l)->(P (S (S m)) (cons' n l)))] - Fix F - {F [n:nat; l:(list' n)] : (P n l) := - <P> - Cases l of - nil' => f - | (cons' n0 m l0) => (f0 n0 l0 (F m l0)) - end}. + (fun (P : forall n : nat, list' n -> Prop) (f : P 0 nil') + (f0 : forall n : nat, + let m := mult2 n in + forall l : list' m, P m l -> P (S (S m)) (cons' n l)) => + fix F (n : nat) (l : list' n) {struct l} : P n l := + match l as x0 in (list' x) return (P x x0) with + | nil' => f + | cons' n0 m l0 => f0 n0 l0 (F m l0) + end). (* Check on-the-fly insertion of let-in patterns for compatibility *) Inductive list'' : nat -> Set := -| nil'' : (list'' O) -| cons'' : (n:nat)[m:=(mult2 n)](list'' m)->[p:=(S (S m))](list'' p). - -Check Fix length { length [n; l:(list'' n)] : nat := - Cases l of - nil'' => O - | (cons'' n l0) => (S (length (mult2 n) l0)) - end }. + | nil'' : list'' 0 + | cons'' : + forall n : nat, + let m := mult2 n in list'' m -> let p := S (S m) in list'' p. + +Check + (fix length n (l : list'' n) {struct l} : nat := + match l with + | nil'' => 0 + | cons'' n l0 => S (length (mult2 n) l0) + end). diff --git a/test-suite/success/Case13.v b/test-suite/success/Case13.v index 71c9191d6..670d01f76 100644 --- a/test-suite/success/Case13.v +++ b/test-suite/success/Case13.v @@ -1,33 +1,56 @@ (* Check coercions in patterns *) Inductive I : Set := - C1 : nat -> I -| C2 : I -> I. + | C1 : nat -> I + | C2 : I -> I. Coercion C1 : nat >-> I. (* Coercion at the root of pattern *) -Check [x]Cases x of (C2 n) => O | O => O | (S n) => n end. +Check (fun x => match x with + | C2 n => 0 + | O => 0 + | S n => n + end). (* Coercion not at the root of pattern *) -Check [x]Cases x of (C2 O) => O | _ => O end. +Check (fun x => match x with + | C2 O => 0 + | _ => 0 + end). (* Unification and coercions inside patterns *) -Check [x:(option nat)]Cases x of None => O | (Some O) => O | _ => O end. +Check + (fun x : option nat => match x with + | None => 0 + | Some O => 0 + | _ => 0 + end). (* Coercion up to delta-conversion, and unification *) -Coercion somenat := (Some nat). -Check [x]Cases x of None => O | O => O | (S n) => n end. +Coercion somenat := Some (A:=nat). +Check (fun x => match x with + | None => 0 + | O => 0 + | S n => n + end). (* Coercions with parameters *) -Inductive listn : nat-> Set := - niln : (listn O) -| consn : (n:nat)nat->(listn n) -> (listn (S n)). +Inductive listn : nat -> Set := + | niln : listn 0 + | consn : forall n : nat, nat -> listn n -> listn (S n). Inductive I' : nat -> Set := - C1' : (n:nat) (listn n) -> (I' n) -| C2' : (n:nat) (I' n) -> (I' n). + | C1' : forall n : nat, listn n -> I' n + | C2' : forall n : nat, I' n -> I' n. Coercion C1' : listn >-> I'. -Check [x:(I' O)]Cases x of (C2' _ _) => O | niln => O | _ => O end. -Check [x:(I' O)]Cases x of (C2' _ niln) => O | _ => O end. +Check (fun x : I' 0 => match x with + | C2' _ _ => 0 + | niln => 0 + | _ => 0 + end). +Check (fun x : I' 0 => match x with + | C2' _ niln => 0 + | _ => 0 + end). diff --git a/test-suite/success/Case14.v b/test-suite/success/Case14.v index edecee79e..f106a64cb 100644 --- a/test-suite/success/Case14.v +++ b/test-suite/success/Case14.v @@ -4,13 +4,18 @@ Axiom bad : false = true. Definition try1 : False := - <[b:bool][_:false=b](if b then False else True)> - Cases bad of refl_equal => I end. + match bad in (_ = b) return (if b then False else True) with + | refl_equal => I + end. Definition try2 : False := - <[b:bool][_:false=b]((if b then False else True)::Prop)> - Cases bad of refl_equal => I end. + match bad in (_ = b) return ((if b then False else True):Prop) with + | refl_equal => I + end. Definition try3 : False := - <[b:bool][_:false=b](([b':bool] if b' then False else True) b)> - Cases bad of refl_equal => I end. + match + bad in (_ = b) return ((fun b' : bool => if b' then False else True) b) + with + | refl_equal => I + end. diff --git a/test-suite/success/Case15.v b/test-suite/success/Case15.v index 229445200..8431880d1 100644 --- a/test-suite/success/Case15.v +++ b/test-suite/success/Case15.v @@ -2,20 +2,23 @@ apparently of inductive type *) (* Check that the non dependency in y is OK both in V7 and V8 *) -Check ([x;y:Prop;z]<[x][z]x=x \/ z=z>Cases x y z of - | O y z' => (or_introl ? (z'=z') (refl_equal ? O)) - | _ y O => (or_intror ?? (refl_equal ? O)) - | x y _ => (or_introl ?? (refl_equal ? x)) - end). +Check + (fun x (y : Prop) z => + match x, y, z return (x = x \/ z = z) with + | O, y, z' => or_introl (z' = z') (refl_equal 0) + | _, y, O => or_intror _ (refl_equal 0) + | x, y, _ => or_introl _ (refl_equal x) + end). (* Suggested by Pierre Letouzey (PR#207) *) -Inductive Boite : Set := - boite : (b:bool)(if b then nat else nat*nat)->Boite. +Inductive Boite : Set := + boite : forall b : bool, (if b then nat else (nat * nat)%type) -> Boite. -Definition test := [B:Boite]<nat>Cases B of - (boite true n) => n -| (boite false (n,m)) => (plus n m) -end. +Definition test (B : Boite) := + match B return nat with + | boite true n => n + | boite false (n, m) => n + m + end. (* Check lazyness of compilation ... future work Inductive I : Set := c : (b:bool)(if b then bool else nat)->I. diff --git a/test-suite/success/Case16.v b/test-suite/success/Case16.v index 3f142faed..77016bbfe 100644 --- a/test-suite/success/Case16.v +++ b/test-suite/success/Case16.v @@ -2,8 +2,9 @@ (* Test dependencies in constructors *) (**********************************************************************) -Check [x : {b:bool|if b then True else False}] - <[x]let (b,_) = x in if b then True else False>Cases x of - | (exist true y) => y - | (exist false z) => z - end. +Check + (fun x : {b : bool | if b then True else False} => + match x return (let (b, _) := x in if b then True else False) with + | exist true y => y + | exist false z => z + end). diff --git a/test-suite/success/Case17.v b/test-suite/success/Case17.v index 07d64958b..061e136e0 100644 --- a/test-suite/success/Case17.v +++ b/test-suite/success/Case17.v @@ -3,43 +3,48 @@ (Simplification of an example from file parsing2.v of the Coq'Art exercises) *) -Require Import PolyList. +Require Import List. -Variable parse_rel : (list bool) -> (list bool) -> nat -> Prop. +Variable parse_rel : list bool -> list bool -> nat -> Prop. -Variables l0:(list bool); rec:(l' : (list bool)) - (le (length l') (S (length l0))) -> - {l'' : (list bool) & - {t : nat | (parse_rel l' l'' t) /\ (le (length l'') (length l'))}} + - {(l'' : (list bool))(t : nat)~ (parse_rel l' l'' t)}. +Variables (l0 : list bool) + (rec : + forall l' : list bool, + length l' <= S (length l0) -> + {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)}). -Axiom HHH : (A:Prop)A. +Axiom HHH : forall A : Prop, A. -Check (Cases (rec l0 (HHH ?)) of - | (inleft (existS (cons false l1) _)) => (inright ? ? (HHH ?)) - | (inleft (existS (cons true l1) (exist t1 (conj Hp Hl)))) => - (inright ? ? (HHH ?)) - | (inleft (existS _ _)) => (inright ? ? (HHH ?)) - | (inright Hnp) => (inright ? ? (HHH ?)) - end :: - {l'' : (list bool) & - {t : nat | (parse_rel (cons true l0) l'' t) /\ (le (length l'') (S (length l0)))}} + - {(l'' : (list bool)) (t : nat) ~ (parse_rel (cons true l0) l'' t)}). +Check + (match rec l0 (HHH _) with + | inleft (existS (false :: l1) _) => inright _ (HHH _) + | inleft (existS (true :: l1) (exist t1 (conj Hp Hl))) => + inright _ (HHH _) + | inleft (existS _ _) => inright _ (HHH _) + | inright Hnp => inright _ (HHH _) + end + :{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 [l0:(list bool);rec:(l' : (list bool)) - (le (length l') (S (length l0))) -> - {l'' : (list bool) & - {t : nat | (parse_rel l' l'' t) /\ (le (length l'') (length l'))}} + - {(l'' : (list bool)) (t : nat) ~ (parse_rel l' l'' t)}] - (Cases (rec l0 (HHH ?)) of - | (inleft (existS (cons false l1) _)) => (inright ? ? (HHH ?)) - | (inleft (existS (cons true l1) (exist t1 (conj Hp Hl)))) => - (inright ? ? (HHH ?)) - | (inleft (existS _ _)) => (inright ? ? (HHH ?)) - | (inright Hnp) => (inright ? ? (HHH ?)) - end :: - {l'' : (list bool) & - {t : nat | (parse_rel (cons true l0) l'' t) /\ (le (length l'') (S (length l0)))}} + - {(l'' : (list bool)) (t : nat) ~ (parse_rel (cons true l0) l'' t)}). +Check + (fun (l0 : list bool) + (rec : forall l' : list bool, + length l' <= S (length l0) -> + {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 + | inleft (existS (false :: l1) _) => inright _ (HHH _) + | inleft (existS (true :: l1) (exist t1 (conj Hp Hl))) => + inright _ (HHH _) + | inleft (existS _ _) => inright _ (HHH _) + | inright Hnp => inright _ (HHH _) + end + :{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/Case2.v b/test-suite/success/Case2.v index 0aa7b5bef..db4336950 100644 --- a/test-suite/success/Case2.v +++ b/test-suite/success/Case2.v @@ -3,9 +3,10 @@ (* Nested patterns *) (* ============================================== *) -Type <[n:nat]n=n>Cases O of - O => (refl_equal nat O) - | m => (refl_equal nat m) -end. +Type + match 0 as n return (n = n) with + | O => refl_equal 0 + | m => refl_equal m + end. diff --git a/test-suite/success/Case5.v b/test-suite/success/Case5.v index fe49cdf95..833621d2b 100644 --- a/test-suite/success/Case5.v +++ b/test-suite/success/Case5.v @@ -1,14 +1,13 @@ -Parameter ff: (n,m:nat)~n=m -> ~(S n)=(S m). -Parameter discr_r : (n:nat) ~(O=(S n)). -Parameter discr_l : (n:nat) ~((S n)=O). +Parameter ff : forall n m : nat, n <> m -> S n <> S m. +Parameter discr_r : forall n : nat, 0 <> S n. +Parameter discr_l : forall n : nat, S n <> 0. -Type -[n:nat] - <[n:nat]n=O\/~n=O>Cases n of - O => (or_introl ? ~O=O (refl_equal ? O)) - | (S O) => (or_intror (S O)=O ? (discr_l O)) - | (S (S x)) => (or_intror (S (S x))=O ? (discr_l (S x))) - - end. +Type + (fun n : nat => + match n return (n = 0 \/ n <> 0) with + | O => or_introl (0 <> 0) (refl_equal 0) + | S O => or_intror (1 = 0) (discr_l 0) + | S (S x) => or_intror (S (S x) = 0) (discr_l (S x)) + end). diff --git a/test-suite/success/Case6.v b/test-suite/success/Case6.v index a262251e7..cc1994e7a 100644 --- a/test-suite/success/Case6.v +++ b/test-suite/success/Case6.v @@ -1,19 +1,15 @@ -Parameter ff: (n,m:nat)~n=m -> ~(S n)=(S m). -Parameter discr_r : (n:nat) ~(O=(S n)). -Parameter discr_l : (n:nat) ~((S n)=O). - -Fixpoint eqdec [n:nat] : (m:nat) n=m \/ ~n=m := -[m:nat] - <[n,m:nat] n=m \/ ~n=m>Cases n m of - O O => (or_introl ? ~O=O (refl_equal ? O)) - - | O (S x) => (or_intror O=(S x) ? (discr_r x)) - - | (S x) O => (or_intror ? ~(S x)=O (discr_l x)) - - | ((S x) as N) ((S y) as M) => - <N=M\/~N=M>Cases (eqdec x y) of - (or_introl h) => (or_introl ? ~N=M (f_equal nat nat S x y h)) - | (or_intror h) => (or_intror N=M ? (ff x y h)) +Parameter ff : forall n m : nat, n <> m -> S n <> S m. +Parameter discr_r : forall n : nat, 0 <> S n. +Parameter discr_l : forall n : nat, S n <> 0. + +Fixpoint eqdec (n m : nat) {struct n} : n = m \/ n <> m := + match n, m return (n = m \/ n <> m) with + | O, O => or_introl (0 <> 0) (refl_equal 0) + | O, S x => or_intror (0 = S x) (discr_r x) + | S x, O => or_intror _ (discr_l x) + | S x as N, S y as M => + match eqdec x y return (N = M \/ N <> M) with + | or_introl h => or_introl (N <> M) (f_equal S h) + | or_intror h => or_intror (N = M) (ff x y h) end - end. + end. diff --git a/test-suite/success/Case7.v b/test-suite/success/Case7.v index 6e2aea480..6e4b20031 100644 --- a/test-suite/success/Case7.v +++ b/test-suite/success/Case7.v @@ -1,16 +1,17 @@ -Inductive List [A:Set] :Set := - Nil:(List A) | Cons:A->(List A)->(List A). +Inductive List (A : Set) : Set := + | Nil : List A + | Cons : A -> List A -> List A. -Inductive Empty [A:Set] : (List A)-> Prop := - intro_Empty: (Empty A (Nil A)). +Inductive Empty (A : Set) : List A -> Prop := + intro_Empty : Empty A (Nil A). -Parameter inv_Empty : (A:Set)(a:A)(x:(List A)) ~(Empty A (Cons A a x)). +Parameter + inv_Empty : forall (A : Set) (a : A) (x : List A), ~ Empty A (Cons A a x). Type -[A:Set] -[l:(List A)] - <[l:(List A)](Empty A l) \/ ~(Empty A l)>Cases l of - Nil => (or_introl ? ~(Empty A (Nil A)) (intro_Empty A)) - | ((Cons a y) as b) => (or_intror (Empty A b) ? (inv_Empty A a y)) - end. + (fun (A : Set) (l : List A) => + match l return (Empty A l \/ ~ Empty A l) with + | Nil => or_introl (~ Empty A (Nil A)) (intro_Empty A) + | Cons a y as b => or_intror (Empty A b) (inv_Empty A a y) + end). diff --git a/test-suite/success/Case8.v b/test-suite/success/Case8.v index b512b5f82..a6113ab9a 100644 --- a/test-suite/success/Case8.v +++ b/test-suite/success/Case8.v @@ -1,7 +1,11 @@ (* Check dependencies in the matching predicate (was failing in V8.0pl1) *) -Inductive t : (x:O=O) x=x -> Prop := - c : (x:0=0) (t x (refl_equal ? x)). +Inductive t : forall x : 0 = 0, x = x -> Prop := + c : forall x : 0 = 0, t x (refl_equal x). -Definition a [x:(t ? (refl_equal ? (refl_equal ? O)))] := - <[_;_;x]Cases x of (c y) => Prop end>Cases x of (c y) => y=y end. +Definition a (x : t _ (refl_equal (refl_equal 0))) := + match x return match x with + | c y => Prop + end with + | c y => y = y + end. diff --git a/test-suite/success/Case9.v b/test-suite/success/Case9.v index a5d07405e..a8534a0b9 100644 --- a/test-suite/success/Case9.v +++ b/test-suite/success/Case9.v @@ -1,55 +1,61 @@ -Inductive List [A:Set] :Set := - Nil:(List A) | Cons:A->(List A)->(List A). - -Inductive eqlong : (List nat)-> (List nat)-> Prop := - eql_cons : (n,m:nat)(x,y:(List nat)) - (eqlong x y) -> (eqlong (Cons nat n x) (Cons nat m y)) -| eql_nil : (eqlong (Nil nat) (Nil nat)). - - -Parameter V1 : (eqlong (Nil nat) (Nil nat))\/ ~(eqlong (Nil nat) (Nil nat)). -Parameter V2 : (a:nat)(x:(List nat)) - (eqlong (Nil nat) (Cons nat a x))\/ ~(eqlong (Nil nat)(Cons nat a x)). -Parameter V3 : (a:nat)(x:(List nat)) - (eqlong (Cons nat a x) (Nil nat))\/ ~(eqlong (Cons nat a x) (Nil nat)). -Parameter V4 : (a:nat)(x:(List nat))(b:nat)(y:(List nat)) - (eqlong (Cons nat a x)(Cons nat b y)) - \/ ~(eqlong (Cons nat a x) (Cons nat b y)). - -Parameter nff : (n,m:nat)(x,y:(List nat)) - ~(eqlong x y)-> ~(eqlong (Cons nat n x) (Cons nat m y)). -Parameter inv_r : (n:nat)(x:(List nat)) ~(eqlong (Nil nat) (Cons nat n x)). -Parameter inv_l : (n:nat)(x:(List nat)) ~(eqlong (Cons nat n x) (Nil nat)). - -Fixpoint eqlongdec [x:(List nat)]: (y:(List nat))(eqlong x y)\/~(eqlong x y) := -[y:(List nat)] - <[x,y:(List nat)](eqlong x y)\/~(eqlong x y)>Cases x y of - Nil Nil => (or_introl ? ~(eqlong (Nil nat) (Nil nat)) eql_nil) - - | Nil ((Cons a x) as L) =>(or_intror (eqlong (Nil nat) L) ? (inv_r a x)) - - | ((Cons a x) as L) Nil => (or_intror (eqlong L (Nil nat)) ? (inv_l a x)) - - | ((Cons a x) as L1) ((Cons b y) as L2) => - <(eqlong L1 L2) \/~(eqlong L1 L2)>Cases (eqlongdec x y) of - (or_introl h) => (or_introl ? ~(eqlong L1 L2) (eql_cons a b x y h)) - | (or_intror h) => (or_intror (eqlong L1 L2) ? (nff a b x y h)) +Inductive List (A : Set) : Set := + | Nil : List A + | Cons : A -> List A -> List A. + +Inductive eqlong : List nat -> List nat -> Prop := + | eql_cons : + forall (n m : nat) (x y : List nat), + eqlong x y -> eqlong (Cons nat n x) (Cons nat m y) + | eql_nil : eqlong (Nil nat) (Nil nat). + + +Parameter V1 : eqlong (Nil nat) (Nil nat) \/ ~ eqlong (Nil nat) (Nil nat). +Parameter + V2 : + forall (a : nat) (x : List nat), + eqlong (Nil nat) (Cons nat a x) \/ ~ eqlong (Nil nat) (Cons nat a x). +Parameter + V3 : + forall (a : nat) (x : List nat), + eqlong (Cons nat a x) (Nil nat) \/ ~ eqlong (Cons nat a x) (Nil nat). +Parameter + V4 : + forall (a : nat) (x : List nat) (b : nat) (y : List nat), + eqlong (Cons nat a x) (Cons nat b y) \/ + ~ eqlong (Cons nat a x) (Cons nat b y). + +Parameter + nff : + forall (n m : nat) (x y : List nat), + ~ eqlong x y -> ~ eqlong (Cons nat n x) (Cons nat m y). +Parameter + inv_r : forall (n : nat) (x : List nat), ~ eqlong (Nil nat) (Cons nat n x). +Parameter + inv_l : forall (n : nat) (x : List nat), ~ eqlong (Cons nat n x) (Nil nat). + +Fixpoint eqlongdec (x y : List nat) {struct x} : + eqlong x y \/ ~ eqlong x y := + match x, y return (eqlong x y \/ ~ eqlong x y) with + | Nil, Nil => or_introl (~ eqlong (Nil nat) (Nil nat)) eql_nil + | Nil, Cons a x as L => or_intror (eqlong (Nil nat) L) (inv_r a x) + | Cons a x as L, Nil => or_intror (eqlong L (Nil nat)) (inv_l a x) + | Cons a x as L1, Cons b y as L2 => + match eqlongdec x y return (eqlong L1 L2 \/ ~ eqlong L1 L2) with + | or_introl h => or_introl (~ eqlong L1 L2) (eql_cons a b x y h) + | or_intror h => or_intror (eqlong L1 L2) (nff a b x y h) end - end. + end. Type - <[x,y:(List nat)](eqlong x y)\/~(eqlong x y)>Cases (Nil nat) (Nil nat) of - Nil Nil => (or_introl ? ~(eqlong (Nil nat) (Nil nat)) eql_nil) - - | Nil ((Cons a x) as L) =>(or_intror (eqlong (Nil nat) L) ? (inv_r a x)) - - | ((Cons a x) as L) Nil => (or_intror (eqlong L (Nil nat)) ? (inv_l a x)) - - | ((Cons a x) as L1) ((Cons b y) as L2) => - <(eqlong L1 L2) \/~(eqlong L1 L2)>Cases (eqlongdec x y) of - (or_introl h) => (or_introl ? ~(eqlong L1 L2) (eql_cons a b x y h)) - | (or_intror h) => (or_intror (eqlong L1 L2) ? (nff a b x y h)) + match Nil nat as x, Nil nat as y return (eqlong x y \/ ~ eqlong x y) with + | Nil, Nil => or_introl (~ eqlong (Nil nat) (Nil nat)) eql_nil + | Nil, Cons a x as L => or_intror (eqlong (Nil nat) L) (inv_r a x) + | Cons a x as L, Nil => or_intror (eqlong L (Nil nat)) (inv_l a x) + | Cons a x as L1, Cons b y as L2 => + match eqlongdec x y return (eqlong L1 L2 \/ ~ eqlong L1 L2) with + | or_introl h => or_introl (~ eqlong L1 L2) (eql_cons a b x y h) + | or_intror h => or_intror (eqlong L1 L2) (nff a b x y h) end - end. + end. diff --git a/test-suite/success/CaseAlias.v b/test-suite/success/CaseAlias.v index b5f0e730e..32d85779f 100644 --- a/test-suite/success/CaseAlias.v +++ b/test-suite/success/CaseAlias.v @@ -1,21 +1,21 @@ (* This has been a bug reported by Y. Bertot *) Inductive expr : Set := - b: expr -> expr -> expr - | u: expr -> expr - | a: expr - | var: nat -> expr . + | b : expr -> expr -> expr + | u : expr -> expr + | a : expr + | var : nat -> expr. -Fixpoint f [t : expr] : expr := - Cases t of - | (b t1 t2) => (b (f t1) (f t2)) - | a => a - | x => (b t a) - end. +Fixpoint f (t : expr) : expr := + match t with + | b t1 t2 => b (f t1) (f t2) + | a => a + | x => b t a + end. -Fixpoint f2 [t : expr] : expr := - Cases t of - | (b t1 t2) => (b (f2 t1) (f2 t2)) - | a => a - | x => (b x a) - end. +Fixpoint f2 (t : expr) : expr := + match t with + | b t1 t2 => b (f2 t1) (f2 t2) + | a => a + | x => b x a + end. diff --git a/test-suite/success/Cases.v b/test-suite/success/Cases.v index 6ccd669af..7c2b7c0bb 100644 --- a/test-suite/success/Cases.v +++ b/test-suite/success/Cases.v @@ -2,89 +2,118 @@ (* Pattern-matching when non inductive terms occur *) (* Dependent form of annotation *) -Type <[n:nat]nat>Cases O eq of O x => O | (S x) y => x end. -Type <[_,_:nat]nat>Cases O eq O of O x y => O | (S x) y z => x end. +Type match 0 as n, eq return nat with + | O, x => 0 + | S x, y => x + end. +Type match 0, eq, 0 return nat with + | O, x, y => 0 + | S x, y, z => x + end. (* Non dependent form of annotation *) -Type <nat>Cases O eq of O x => O | (S x) y => x end. +Type match 0, eq return nat with + | O, x => 0 + | S x, y => x + end. (* Combining dependencies and non inductive arguments *) -Type [A:Set][a:A][H:O=O]<[x][H]H==H>Cases H a of _ _ => (refl_eqT ? H) end. +Type + (fun (A : Set) (a : A) (H : 0 = 0) => + match H in (_ = x), a return (H = H) with + | _, _ => refl_equal H + end). (* Interaction with coercions *) Parameter bool2nat : bool -> nat. Coercion bool2nat : bool >-> nat. -Check [x](Cases x of O => true | (S _) => O end :: nat). +Check (fun x => match x with + | O => true + | S _ => 0 + end:nat). (****************************************************************************) (* All remaining examples come from Cristina Cornes' V6 TESTS/MultCases.v *) -Inductive IFExpr : Set := - Var : nat -> IFExpr - | Tr : IFExpr - | Fa : IFExpr - | IfE : IFExpr -> IFExpr -> IFExpr -> IFExpr. +Inductive IFExpr : Set := + | Var : nat -> IFExpr + | Tr : IFExpr + | Fa : IFExpr + | IfE : IFExpr -> IFExpr -> IFExpr -> IFExpr. -Inductive List [A:Set] :Set := - Nil:(List A) | Cons:A->(List A)->(List A). +Inductive List (A : Set) : Set := + | Nil : List A + | Cons : A -> List A -> List A. -Inductive listn : nat-> Set := - niln : (listn O) -| consn : (n:nat)nat->(listn n) -> (listn (S n)). +Inductive listn : nat -> Set := + | niln : listn 0 + | consn : forall n : nat, nat -> listn n -> listn (S n). -Inductive Listn [A:Set] : nat-> Set := - Niln : (Listn A O) -| Consn : (n:nat)nat->(Listn A n) -> (Listn A (S n)). +Inductive Listn (A : Set) : nat -> Set := + | Niln : Listn A 0 + | Consn : forall n : nat, nat -> Listn A n -> Listn A (S n). -Inductive Le : nat->nat->Set := - LeO: (n:nat)(Le O n) -| LeS: (n,m:nat)(Le n m) -> (Le (S n) (S m)). +Inductive Le : nat -> nat -> Set := + | LeO : forall n : nat, Le 0 n + | LeS : forall n m : nat, Le n m -> Le (S n) (S m). -Inductive LE [n:nat] : nat->Set := - LE_n : (LE n n) | LE_S : (m:nat)(LE n m)->(LE n (S m)). +Inductive LE (n : nat) : nat -> Set := + | LE_n : LE n n + | LE_S : forall m : nat, LE n m -> LE n (S m). -Require Bool. +Require Import Bool. -Inductive PropForm : Set := - Fvar : nat -> PropForm - | Or : PropForm -> PropForm -> PropForm . +Inductive PropForm : Set := + | Fvar : nat -> PropForm + | Or : PropForm -> PropForm -> PropForm. Section testIFExpr. -Definition Assign:= nat->bool. +Definition Assign := nat -> bool. Parameter Prop_sem : Assign -> PropForm -> bool. -Type [A:Assign][F:PropForm] - <bool>Cases F of - (Fvar n) => (A n) - | (Or F G) => (orb (Prop_sem A F) (Prop_sem A G)) - end. - -Type [A:Assign][H:PropForm] - <bool>Cases H of - (Fvar n) => (A n) - | (Or F G) => (orb (Prop_sem A F) (Prop_sem A G)) - end. +Type + (fun (A : Assign) (F : PropForm) => + match F return bool with + | Fvar n => A n + | Or F G => Prop_sem A F || Prop_sem A G + end). + +Type + (fun (A : Assign) (H : PropForm) => + match H return bool with + | Fvar n => A n + | Or F G => Prop_sem A F || Prop_sem A G + end). End testIFExpr. -Type [x:nat]<nat>Cases x of O => O | x => x end. +Type (fun x : nat => match x return nat with + | O => 0 + | x => x + end). Section testlist. -Parameter A:Set. -Inductive list : Set := nil : list | cons : A->list->list. -Parameter inf: A->A->Prop. +Parameter A : Set. +Inductive list : Set := + | nil : list + | cons : A -> list -> list. +Parameter inf : A -> A -> Prop. -Definition list_Lowert2 := - [a:A][l:list](<Prop>Cases l of nil => True - | (cons b l) =>(inf a b) end). +Definition list_Lowert2 (a : A) (l : list) := + match l return Prop with + | nil => True + | cons b l => inf a b + end. -Definition titi := - [a:A][l:list](<list>Cases l of nil => l - | (cons b l) => l end). +Definition titi (a : A) (l : list) := + match l return list with + | nil => l + | cons b l => l + end. Reset list. End testlist. @@ -93,444 +122,490 @@ End testlist. (* ------------------- *) -Type <nat>Cases O of O => O | _ => O end. - -Type <nat>Cases O of - (O as b) => b - | (S O) => O - | (S (S x)) => x end. +Type match 0 return nat with + | O => 0 + | _ => 0 + end. -Type Cases O of - (O as b) => b - | (S O) => O - | (S (S x)) => x end. +Type match 0 return nat with + | O as b => b + | S O => 0 + | S (S x) => x + end. +Type match 0 with + | O as b => b + | S O => 0 + | S (S x) => x + end. -Type [x:nat]<nat>Cases x of - (O as b) => b - | (S x) => x end. -Type [x:nat]Cases x of - (O as b) => b - | (S x) => x end. +Type (fun x : nat => match x return nat with + | O as b => b + | S x => x + end). -Type <nat>Cases O of - (O as b) => b - | (S x) => x end. +Type (fun x : nat => match x with + | O as b => b + | S x => x + end). -Type <nat>Cases O of - x => x - end. +Type match 0 return nat with + | O as b => b + | S x => x + end. -Type Cases O of - x => x - end. +Type match 0 return nat with + | x => x + end. -Type <nat>Cases O of - O => O - | ((S x) as b) => b - end. +Type match 0 with + | x => x + end. -Type [x:nat]<nat>Cases x of - O => O - | ((S x) as b) => b - end. +Type match 0 return nat with + | O => 0 + | S x as b => b + end. -Type [x:nat] Cases x of - O => O - | ((S x) as b) => b - end. +Type (fun x : nat => match x return nat with + | O => 0 + | S x as b => b + end). +Type (fun x : nat => match x with + | O => 0 + | S x as b => b + end). -Type <nat>Cases O of - O => O - | (S x) => O - end. +Type match 0 return nat with + | O => 0 + | S x => 0 + end. -Type <nat*nat>Cases O of - O => (O,O) - | (S x) => (x,O) - end. -Type Cases O of - O => (O,O) - | (S x) => (x,O) - end. +Type match 0 return (nat * nat) with + | O => (0, 0) + | S x => (x, 0) + end. -Type <nat->nat>Cases O of - O => [n:nat]O - | (S x) => [n:nat]O - end. +Type match 0 with + | O => (0, 0) + | S x => (x, 0) + end. -Type Cases O of - O => [n:nat]O - | (S x) => [n:nat]O - end. +Type + match 0 return (nat -> nat) with + | O => fun n : nat => 0 + | S x => fun n : nat => 0 + end. +Type match 0 with + | O => fun n : nat => 0 + | S x => fun n : nat => 0 + end. -Type <nat->nat>Cases O of - O => [n:nat]O - | (S x) => [n:nat](plus x n) - end. -Type Cases O of - O => [n:nat]O - | (S x) => [n:nat](plus x n) - end. +Type + match 0 return (nat -> nat) with + | O => fun n : nat => 0 + | S x => fun n : nat => x + n + end. +Type match 0 with + | O => fun n : nat => 0 + | S x => fun n : nat => x + n + end. -Type <nat>Cases O of - O => O - | ((S x) as b) => (plus b x) - end. -Type <nat>Cases O of - O => O - | ((S (x as a)) as b) => (plus b a) - end. -Type Cases O of - O => O - | ((S (x as a)) as b) => (plus b a) - end. +Type match 0 return nat with + | O => 0 + | S x as b => b + x + end. +Type match 0 return nat with + | O => 0 + | S a as b => b + a + end. +Type match 0 with + | O => 0 + | S a as b => b + a + end. -Type Cases O of - O => O - | _ => O - end. -Type <nat>Cases O of - O => O - | x => x - end. +Type match 0 with + | O => 0 + | _ => 0 + end. -Type <nat>Cases O (S O) of - x y => (plus x y) - end. - -Type Cases O (S O) of - x y => (plus x y) - end. - -Type <nat>Cases O (S O) of - O y => y - | (S x) y => (plus x y) - end. +Type match 0 return nat with + | O => 0 + | x => x + end. -Type Cases O (S O) of - O y => y - | (S x) y => (plus x y) - end. +Type match 0, 1 return nat with + | x, y => x + y + end. +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 + end. -Type <nat>Cases O (S O) of - O x => x - | (S y) O => y - | x y => (plus x y) - end. +Type match 0, 1 with + | O, y => y + | S x, y => x + y + end. +Type match 0, 1 return nat with + | O, x => x + | S y, O => y + | x, y => x + y + end. -Type Cases O (S O) of - O x => (plus x O) - | (S y) O => (plus y O) - | x y => (plus x y) - end. -Type - <nat>Cases O (S O) of - O x => (plus x O) - | (S y) O => (plus y O) - | x y => (plus x y) - end. +Type match 0, 1 with + | O, x => x + 0 + | S y, O => y + 0 + | x, y => x + y + end. -Type - <nat>Cases O (S O) of - O x => x - | ((S x) as b) (S y) => (plus (plus b x) y) - | x y => (plus x y) - end. +Type + match 0, 1 return nat with + | O, x => x + 0 + | S y, O => y + 0 + | x, y => x + y + end. -Type Cases O (S O) of - O x => x - | ((S x) as b) (S y) => (plus (plus b x) y) - | x y => (plus x y) - end. +Type + match 0, 1 return nat with + | O, x => x + | S x as b, S y => b + x + y + | x, y => x + y + end. -Type [l:(List nat)]<(List nat)>Cases l of - Nil => (Nil nat) - | (Cons a l) => l - end. +Type + match 0, 1 with + | O, x => x + | S x as b, S y => b + x + y + | x, y => x + y + end. -Type [l:(List nat)] Cases l of - Nil => (Nil nat) - | (Cons a l) => l - end. -Type <nat>Cases (Nil nat) of - Nil =>O - | (Cons a l) => (S a) - end. -Type Cases (Nil nat) of - Nil =>O - | (Cons a l) => (S a) - end. +Type + (fun l : List nat => + match l return (List nat) with + | Nil => Nil nat + | Cons a l => l + end). + +Type (fun l : List nat => match l with + | Nil => Nil nat + | Cons a l => l + end). + +Type match Nil nat return nat with + | Nil => 0 + | Cons a l => S a + end. +Type match Nil nat with + | Nil => 0 + | Cons a l => S a + end. -Type <(List nat)>Cases (Nil nat) of - (Cons a l) => l - | x => x - end. +Type match Nil nat return (List nat) with + | Cons a l => l + | x => x + end. -Type Cases (Nil nat) of - (Cons a l) => l - | x => x - end. +Type match Nil nat with + | Cons a l => l + | x => x + end. -Type <(List nat)>Cases (Nil nat) of - Nil => (Nil nat) - | (Cons a l) => l - end. +Type + match Nil nat return (List nat) with + | Nil => Nil nat + | Cons a l => l + end. -Type Cases (Nil nat) of - Nil => (Nil nat) - | (Cons a l) => l - end. +Type match Nil nat with + | Nil => Nil nat + | Cons a l => l + end. -Type - <nat>Cases O of - O => O - | (S x) => <nat>Cases (Nil nat) of - Nil => x - | (Cons a l) => (plus x a) - end - end. +Type + match 0 return nat with + | O => 0 + | S x => match Nil nat return nat with + | Nil => x + | Cons a l => x + a + end + end. -Type - Cases O of - O => O - | (S x) => Cases (Nil nat) of - Nil => x - | (Cons a l) => (plus x a) - end - end. +Type + match 0 with + | O => 0 + | S x => match Nil nat with + | Nil => x + | Cons a l => x + a + end + end. -Type - [y:nat]Cases y of - O => O - | (S x) => Cases (Nil nat) of - Nil => x - | (Cons a l) => (plus x a) - end - end. +Type + (fun y : nat => + match y with + | O => 0 + | S x => match Nil nat with + | Nil => x + | Cons a l => x + a + end + end). -Type - <nat>Cases O (Nil nat) of - O x => O - | (S x) Nil => x - | (S x) (Cons a l) => (plus x a) - end. +Type + match 0, Nil nat return nat with + | O, x => 0 + | S x, Nil => x + | S x, Cons a l => x + a + end. -Type [n:nat][l:(listn n)]<[_:nat]nat>Cases l of - niln => O - | x => O - end. +Type + (fun (n : nat) (l : listn n) => + match l return nat with + | niln => 0 + | x => 0 + end). -Type [n:nat][l:(listn n)] - Cases l of - niln => O - | x => O - end. +Type (fun (n : nat) (l : listn n) => match l with + | niln => 0 + | x => 0 + end). -Type <[_:nat]nat>Cases niln of - niln => O - | x => O - end. +Type match niln return nat with + | niln => 0 + | x => 0 + end. -Type Cases niln of - niln => O - | x => O - end. +Type match niln with + | niln => 0 + | x => 0 + end. -Type <[_:nat]nat>Cases niln of - niln => O - | (consn n a l) => a - end. -Type Cases niln of niln => O - | (consn n a l) => a +Type match niln return nat with + | niln => 0 + | consn n a l => a + end. +Type match niln with + | niln => 0 + | consn n a l => a end. -Type <[n:nat][_:(listn n)]nat>Cases niln of - (consn m _ niln) => m - | _ => (S O) end. +Type + match niln in (listn n) return nat with + | consn m _ niln => m + | _ => 1 + end. -Type [n:nat][x:nat][l:(listn n)]<[_:nat]nat>Cases x l of - O niln => O - | y x => O - end. +Type + (fun (n x : nat) (l : listn n) => + match x, l return nat with + | O, niln => 0 + | y, x => 0 + end). + +Type match 0, niln return nat with + | O, niln => 0 + | y, x => 0 + end. -Type <[_:nat]nat>Cases O niln of - O niln => O - | y x => O - end. +Type match niln, 0 return nat with + | niln, O => 0 + | y, x => 0 + end. -Type <[_:nat]nat>Cases niln O of - niln O => O - | y x => O - end. +Type match niln, 0 with + | niln, O => 0 + | y, x => 0 + end. -Type Cases niln O of - niln O => O - | y x => O - end. +Type match niln, niln return nat with + | niln, niln => 0 + | x, y => 0 + end. -Type <[_:nat][_:nat]nat>Cases niln niln of - niln niln => O - | x y => O - end. +Type match niln, niln with + | niln, niln => 0 + | x, y => 0 + end. -Type Cases niln niln of - niln niln => O - | x y => O - end. +Type + match niln, niln, niln return nat with + | niln, niln, niln => 0 + | x, y, z => 0 + end. -Type <[_,_,_:nat]nat>Cases niln niln niln of - niln niln niln => O - | x y z => O - end. +Type match niln, niln, niln with + | niln, niln, niln => 0 + | x, y, z => 0 + end. -Type Cases niln niln niln of - niln niln niln => O - | x y z => O - end. +Type match niln return nat with + | niln => 0 + | consn n a l => 0 + end. -Type <[_:nat]nat>Cases (niln) of - niln => O - | (consn n a l) => O - end. +Type match niln with + | niln => 0 + | consn n a l => 0 + end. -Type Cases (niln) of - niln => O - | (consn n a l) => O - end. +Type + match niln, niln return nat with + | niln, niln => 0 + | niln, consn n a l => n + | consn n a l, x => a + end. -Type <[_:nat][_:nat]nat>Cases niln niln of - niln niln => O - | niln (consn n a l) => n - | (consn n a l) x => a - end. +Type + match niln, niln with + | niln, niln => 0 + | niln, consn n a l => n + | consn n a l, x => a + end. -Type Cases niln niln of - niln niln => O - | niln (consn n a l) => n - | (consn n a l) x => a - end. +Type + (fun (n : nat) (l : listn n) => + match l return nat with + | niln => 0 + | x => 0 + end). -Type [n:nat][l:(listn n)]<[_:nat]nat>Cases l of - niln => O - | x => O - end. +Type + (fun (c : nat) (s : bool) => + match c, s return nat with + | O, _ => 0 + | _, _ => c + end). -Type [c:nat;s:bool] - <[_:nat;_:bool]nat>Cases c s of - | O _ => O - | _ _ => c - end. - -Type [c:nat;s:bool] - <[_:nat;_:bool]nat>Cases c s of - | O _ => O - | (S _) _ => c - end. +Type + (fun (c : nat) (s : bool) => + match c, s return nat with + | O, _ => 0 + | S _, _ => c + end). (* Rows of pattern variables: some tricky cases *) -Axiom P:nat->Prop; f:(n:nat)(P n). +Axioms (P : nat -> Prop) (f : forall n : nat, P n). -Type [i:nat] - <[_:bool;n:nat](P n)>Cases true i of - | true k => (f k) - | _ k => (f k) - end. +Type + (fun i : nat => + match true, i as n return (P n) with + | true, k => f k + | _, k => f k + end). -Type [i:nat] - <[n:nat;_:bool](P n)>Cases i true of - | k true => (f k) - | k _ => (f k) - end. +Type + (fun i : nat => + match i as n, true return (P n) with + | k, true => f k + | k, _ => f k + end). (* Nested Cases: the SYNTH of the Cases on n used to make Multcase believe * it has to synthtize the predicate on O (which he can't) *) -Type <[n]Cases n of O => bool | (S _) => nat end>Cases O of - O => true - | (S _) => O +Type + match 0 as n return match n with + | O => bool + | S _ => nat + end with + | O => true + | S _ => 0 end. -Type [n:nat][l:(listn n)]Cases l of - niln => O - | x => O - end. +Type (fun (n : nat) (l : listn n) => match l with + | niln => 0 + | x => 0 + end). -Type [n:nat][l:(listn n)]<[_:nat]nat>Cases l of - niln => O - | (consn n a niln) => O - | (consn n a (consn m b l)) => (plus n m) - end. +Type + (fun (n : nat) (l : listn n) => + match l return nat with + | niln => 0 + | consn n a niln => 0 + | consn n a (consn m b l) => n + m + end). -Type [n:nat][l:(listn n)]Cases l of - niln => O - | (consn n a niln) => O - | (consn n a (consn m b l)) => (plus n m) - end. +Type + (fun (n : nat) (l : listn n) => + match l with + | niln => 0 + | consn n a niln => 0 + | consn n a (consn m b l) => n + m + end). -Type [n:nat][l:(listn n)]<[_:nat]nat>Cases l of - niln => O - | (consn n a niln) => O - | (consn n a (consn m b l)) => (plus n m) - end. +Type + (fun (n : nat) (l : listn n) => + match l return nat with + | niln => 0 + | consn n a niln => 0 + | consn n a (consn m b l) => n + m + end). -Type [n:nat][l:(listn n)]Cases l of - niln => O - | (consn n a niln) => O - | (consn n a (consn m b l)) => (plus n m) - end. +Type + (fun (n : nat) (l : listn n) => + match l with + | niln => 0 + | consn n a niln => 0 + | consn n a (consn m b l) => n + m + end). -Type [A:Set][n:nat][l:(Listn A n)]<[_:nat]nat>Cases l of - Niln => O - | (Consn n a Niln) => O - | (Consn n a (Consn m b l)) => (plus n m) - end. +Type + (fun (A : Set) (n : nat) (l : Listn A n) => + match l return nat with + | Niln => 0 + | Consn n a Niln => 0 + | Consn n a (Consn m b l) => n + m + end). -Type [A:Set][n:nat][l:(Listn A n)]Cases l of - Niln => O - | (Consn n a Niln) => O - | (Consn n a (Consn m b l)) => (plus n m) - end. +Type + (fun (A : Set) (n : nat) (l : Listn A n) => + match l with + | Niln => 0 + | Consn n a Niln => 0 + | Consn n a (Consn m b l) => n + m + end). (* Type [A:Set][n:nat][l:(Listn A n)] @@ -557,401 +632,441 @@ Type [A:Set][n:nat][l:(Listn A n)] **********) (* To test tratement of as-patterns in depth *) -Type [A:Set] [l:(List A)] - Cases l of - (Nil as b) => (Nil A) - | ((Cons a Nil) as L) => L - | ((Cons a (Cons b m)) as L) => L - end. +Type + (fun (A : Set) (l : List A) => + match l with + | Nil as b => Nil A + | Cons a Nil as L => L + | Cons a (Cons b m) as L => L + end). -Type [n:nat][l:(listn n)] - <[_:nat](listn n)>Cases l of - niln => l - | (consn n a c) => l - end. -Type [n:nat][l:(listn n)] - Cases l of - niln => l - | (consn n a c) => l - end. +Type + (fun (n : nat) (l : listn n) => + match l return (listn n) with + | niln => l + | consn n a c => l + end). +Type + (fun (n : nat) (l : listn n) => + match l with + | niln => l + | consn n a c => l + end). -Type [n:nat][l:(listn n)] - <[_:nat](listn n)>Cases l of - (niln as b) => l - | _ => l - end. +Type + (fun (n : nat) (l : listn n) => + match l return (listn n) with + | niln as b => l + | _ => l + end). -Type [n:nat][l:(listn n)] - Cases l of - (niln as b) => l - | _ => l - end. +Type + (fun (n : nat) (l : listn n) => match l with + | niln as b => l + | _ => l + end). -Type [n:nat][l:(listn n)] - <[_:nat](listn n)>Cases l of - (niln as b) => l - | x => l - end. +Type + (fun (n : nat) (l : listn n) => + match l return (listn n) with + | niln as b => l + | x => l + end). -Type [A:Set][n:nat][l:(Listn A n)] - Cases l of - (Niln as b) => l - | _ => l - end. +Type + (fun (A : Set) (n : nat) (l : Listn A n) => + match l with + | Niln as b => l + | _ => l + end). -Type [A:Set][n:nat][l:(Listn A n)] - <[_:nat](Listn A n)>Cases l of - Niln => l - | (Consn n a Niln) => l - | (Consn n a (Consn m b c)) => l - end. +Type + (fun (A : Set) (n : nat) (l : Listn A n) => + match l return (Listn A n) with + | Niln => l + | Consn n a Niln => l + | Consn n a (Consn m b c) => l + end). -Type [A:Set][n:nat][l:(Listn A n)] - Cases l of - Niln => l - | (Consn n a Niln) => l - | (Consn n a (Consn m b c)) => l - end. +Type + (fun (A : Set) (n : nat) (l : Listn A n) => + match l with + | Niln => l + | Consn n a Niln => l + | Consn n a (Consn m b c) => l + end). -Type [A:Set][n:nat][l:(Listn A n)] - <[_:nat](Listn A n)>Cases l of - (Niln as b) => l - | (Consn n a (Niln as b)) => l - | (Consn n a (Consn m b _)) => l - end. +Type + (fun (A : Set) (n : nat) (l : Listn A n) => + match l return (Listn A n) with + | Niln as b => l + | Consn n a (Niln as b) => l + | Consn n a (Consn m b _) => l + end). -Type [A:Set][n:nat][l:(Listn A n)] - Cases l of - (Niln as b) => l - | (Consn n a (Niln as b)) => l - | (Consn n a (Consn m b _)) => l - end. +Type + (fun (A : Set) (n : nat) (l : Listn A n) => + match l with + | Niln as b => l + | Consn n a (Niln as b) => l + | Consn n a (Consn m b _) => l + end). -Type <[_:nat]nat>Cases (niln) of - niln => O - | (consn n a niln) => O - | (consn n a (consn m b l)) => (plus n m) - end. +Type + match niln return nat with + | niln => 0 + | consn n a niln => 0 + | consn n a (consn m b l) => n + m + end. -Type Cases (niln) of - niln => O - | (consn n a niln) => O - | (consn n a (consn m b l)) => (plus n m) - end. +Type + match niln with + | niln => 0 + | consn n a niln => 0 + | consn n a (consn m b l) => n + m + end. -Type <[_,_:nat]nat>Cases (LeO O) of - (LeO x) => x - | (LeS n m h) => (plus n m) - end. +Type match LeO 0 return nat with + | LeO x => x + | LeS n m h => n + m + end. -Type Cases (LeO O) of - (LeO x) => x - | (LeS n m h) => (plus n m) - end. +Type match LeO 0 with + | LeO x => x + | LeS n m h => n + m + end. -Type [n:nat][l:(Listn nat n)] - <[_:nat]nat>Cases l of - Niln => O - | (Consn n a l) => O - end. +Type + (fun (n : nat) (l : Listn nat n) => + match l return nat with + | Niln => 0 + | Consn n a l => 0 + end). -Type [n:nat][l:(Listn nat n)] - Cases l of - Niln => O - | (Consn n a l) => O - end. +Type + (fun (n : nat) (l : Listn nat n) => + match l with + | Niln => 0 + | Consn n a l => 0 + end). -Type Cases (Niln nat) of - Niln => O - | (Consn n a l) => O - end. +Type match Niln nat with + | Niln => 0 + | Consn n a l => 0 + end. -Type <[_:nat]nat>Cases (LE_n O) of - LE_n => O - | (LE_S m h) => O - end. +Type match LE_n 0 return nat with + | LE_n => 0 + | LE_S m h => 0 + end. -Type Cases (LE_n O) of - LE_n => O - | (LE_S m h) => O - end. +Type match LE_n 0 with + | LE_n => 0 + | LE_S m h => 0 + end. -Type Cases (LE_n O) of - LE_n => O - | (LE_S m h) => O - end. +Type match LE_n 0 with + | LE_n => 0 + | LE_S m h => 0 + end. -Type <[_:nat]nat>Cases (niln ) of - niln => O - | (consn n a niln) => n - | (consn n a (consn m b l)) => (plus n m) - end. +Type + match niln return nat with + | niln => 0 + | consn n a niln => n + | consn n a (consn m b l) => n + m + end. -Type Cases (niln ) of - niln => O - | (consn n a niln) => n - | (consn n a (consn m b l)) => (plus n m) - end. +Type + match niln with + | niln => 0 + | consn n a niln => n + | consn n a (consn m b l) => n + m + end. -Type <[_:nat]nat>Cases (Niln nat) of - Niln => O - | (Consn n a Niln) => n - | (Consn n a (Consn m b l)) => (plus n m) - end. +Type + match Niln nat return nat with + | Niln => 0 + | Consn n a Niln => n + | Consn n a (Consn m b l) => n + m + end. -Type Cases (Niln nat) of - Niln => O - | (Consn n a Niln) => n - | (Consn n a (Consn m b l)) => (plus n m) - end. +Type + match Niln nat with + | Niln => 0 + | Consn n a Niln => n + | Consn n a (Consn m b l) => n + m + end. -Type <[_,_:nat]nat>Cases (LeO O) of - (LeO x) => x - | (LeS n m (LeO x)) => (plus x m) - | (LeS n m (LeS x y h)) => (plus n x) - end. +Type + match LeO 0 return nat with + | LeO x => x + | LeS n m (LeO x) => x + m + | LeS n m (LeS x y h) => n + x + end. -Type Cases (LeO O) of - (LeO x) => x - | (LeS n m (LeO x)) => (plus x m) - | (LeS n m (LeS x y h)) => (plus n x) - end. +Type + match LeO 0 with + | LeO x => x + | LeS n m (LeO x) => x + m + | LeS n m (LeS x y h) => n + x + end. -Type <[_,_:nat]nat>Cases (LeO O) of - (LeO x) => x - | (LeS n m (LeO x)) => (plus x m) - | (LeS n m (LeS x y h)) => m - end. +Type + match LeO 0 return nat with + | LeO x => x + | LeS n m (LeO x) => x + m + | LeS n m (LeS x y h) => m + end. -Type Cases (LeO O) of - (LeO x) => x - | (LeS n m (LeO x)) => (plus x m) - | (LeS n m (LeS x y h)) => m - end. +Type + match LeO 0 with + | LeO x => x + | LeS n m (LeO x) => x + m + | LeS n m (LeS x y h) => m + end. -Type [n,m:nat][h:(Le n m)] - <[_,_:nat]nat>Cases h of - (LeO x) => x - | x => O - end. +Type + (fun (n m : nat) (h : Le n m) => + match h return nat with + | LeO x => x + | x => 0 + end). -Type [n,m:nat][h:(Le n m)] - Cases h of - (LeO x) => x - | x => O - end. +Type (fun (n m : nat) (h : Le n m) => match h with + | LeO x => x + | x => 0 + end). -Type [n,m:nat][h:(Le n m)] - <[_,_:nat]nat>Cases h of - (LeS n m h) => n - | x => O - end. +Type + (fun (n m : nat) (h : Le n m) => + match h return nat with + | LeS n m h => n + | x => 0 + end). -Type [n,m:nat][h:(Le n m)] - Cases h of - (LeS n m h) => n - | x => O - end. +Type + (fun (n m : nat) (h : Le n m) => match h with + | LeS n m h => n + | x => 0 + end). -Type [n,m:nat][h:(Le n m)] - <[_,_:nat]nat*nat>Cases h of - (LeO n) => (O,n) - |(LeS n m _) => ((S n),(S m)) - end. +Type + (fun (n m : nat) (h : Le n m) => + match h return (nat * nat) with + | LeO n => (0, n) + | LeS n m _ => (S n, S m) + end). -Type [n,m:nat][h:(Le n m)] - Cases h of - (LeO n) => (O,n) - |(LeS n m _) => ((S n),(S m)) - end. +Type + (fun (n m : nat) (h : Le n m) => + match h with + | LeO n => (0, n) + | LeS n m _ => (S n, S m) + end). -Fixpoint F [n,m:nat; h:(Le n m)] : (Le n (S m)) := - <[n,m:nat](Le n (S m))>Cases h of - (LeO m') => (LeO (S m')) - | (LeS n' m' h') => (LeS n' (S m') (F n' m' h')) - end. +Fixpoint F (n m : nat) (h : Le n m) {struct h} : Le n (S m) := + match h in (Le n m) return (Le n (S m)) with + | LeO m' => LeO (S m') + | LeS n' m' h' => LeS n' (S m') (F n' m' h') + end. Reset F. -Fixpoint F [n,m:nat; h:(Le n m)] :(Le n (S m)) := - <[n,m:nat](Le n (S m))>Cases h of - (LeS n m h) => (LeS n (S m) (F n m h)) - | (LeO m) => (LeO (S m)) - end. +Fixpoint F (n m : nat) (h : Le n m) {struct h} : Le n (S m) := + match h in (Le n m) return (Le n (S m)) with + | LeS n m h => LeS n (S m) (F n m h) + | LeO m => LeO (S m) + end. (* Rend la longueur de la liste *) -Definition length1:= [n:nat] [l:(listn n)] - <[_:nat]nat>Cases l of - (consn n _ (consn m _ _)) => (S (S m)) - |(consn n _ _) => (S O) - | _ => O - end. +Definition length1 (n : nat) (l : listn n) := + match l return nat with + | consn n _ (consn m _ _) => S (S m) + | consn n _ _ => 1 + | _ => 0 + end. Reset length1. -Definition length1:= [n:nat] [l:(listn n)] - Cases l of - (consn n _ (consn m _ _)) => (S (S m)) - |(consn n _ _) => (S O) - | _ => O - end. +Definition length1 (n : nat) (l : listn n) := + match l with + | consn n _ (consn m _ _) => S (S m) + | consn n _ _ => 1 + | _ => 0 + end. -Definition length2:= [n:nat] [l:(listn n)] - <[_:nat]nat>Cases l of - (consn n _ (consn m _ _)) => (S (S m)) - |(consn n _ _) => (S n) - | _ => O - end. +Definition length2 (n : nat) (l : listn n) := + match l return nat with + | consn n _ (consn m _ _) => S (S m) + | consn n _ _ => S n + | _ => 0 + end. Reset length2. -Definition length2:= [n:nat] [l:(listn n)] - Cases l of - (consn n _ (consn m _ _)) => (S (S m)) - |(consn n _ _) => (S n) - | _ => O - end. +Definition length2 (n : nat) (l : listn n) := + match l with + | consn n _ (consn m _ _) => S (S m) + | consn n _ _ => S n + | _ => 0 + end. -Definition length3 := -[n:nat][l:(listn n)] - <[_:nat]nat>Cases l of - (consn n _ (consn m _ l)) => (S n) - |(consn n _ _) => (S O) - | _ => O - end. +Definition length3 (n : nat) (l : listn n) := + match l return nat with + | consn n _ (consn m _ l) => S n + | consn n _ _ => 1 + | _ => 0 + end. Reset length3. -Definition length3 := -[n:nat][l:(listn n)] - Cases l of - (consn n _ (consn m _ l)) => (S n) - |(consn n _ _) => (S O) - | _ => O - end. +Definition length3 (n : nat) (l : listn n) := + match l with + | consn n _ (consn m _ l) => S n + | consn n _ _ => 1 + | _ => 0 + end. -Type <[_,_:nat]nat>Cases (LeO O) of - (LeS n m h) =>(plus n m) - | x => O - end. -Type Cases (LeO O) of - (LeS n m h) =>(plus n m) - | x => O - end. +Type match LeO 0 return nat with + | LeS n m h => n + m + | x => 0 + end. +Type match LeO 0 with + | LeS n m h => n + m + | x => 0 + end. -Type [n,m:nat][h:(Le n m)]<[_,_:nat]nat>Cases h of - (LeO x) => x - | (LeS n m (LeO x)) => (plus x m) - | (LeS n m (LeS x y h)) =>(plus n (plus m (plus x y))) - end. +Type + (fun (n m : nat) (h : Le n m) => + match h return nat with + | LeO x => x + | LeS n m (LeO x) => x + m + | LeS n m (LeS x y h) => n + (m + (x + y)) + end). -Type [n,m:nat][h:(Le n m)]Cases h of - (LeO x) => x - | (LeS n m (LeO x)) => (plus x m) - | (LeS n m (LeS x y h)) =>(plus n (plus m (plus x y))) - end. +Type + (fun (n m : nat) (h : Le n m) => + match h with + | LeO x => x + | LeS n m (LeO x) => x + m + | LeS n m (LeS x y h) => n + (m + (x + y)) + end). -Type <[_,_:nat]nat>Cases (LeO O) of - (LeO x) => x - | (LeS n m (LeO x)) => (plus x m) - | (LeS n m (LeS x y h)) =>(plus n (plus m (plus x y))) - end. +Type + match LeO 0 return nat with + | LeO x => x + | LeS n m (LeO x) => x + m + | LeS n m (LeS x y h) => n + (m + (x + y)) + end. -Type Cases (LeO O) of - (LeO x) => x - | (LeS n m (LeO x)) => (plus x m) - | (LeS n m (LeS x y h)) =>(plus n (plus m (plus x y))) - end. +Type + match LeO 0 with + | LeO x => x + | LeS n m (LeO x) => x + m + | LeS n m (LeS x y h) => n + (m + (x + y)) + end. -Type <[_:nat]nat>Cases (LE_n O) of - LE_n => O - | (LE_S m LE_n) => (plus O m) - | (LE_S m (LE_S y h)) => (plus O m) - end. +Type + match LE_n 0 return nat with + | LE_n => 0 + | LE_S m LE_n => 0 + m + | LE_S m (LE_S y h) => 0 + m + end. -Type Cases (LE_n O) of - LE_n => O - | (LE_S m LE_n) => (plus O m) - | (LE_S m (LE_S y h)) => (plus O m) - end. +Type + match LE_n 0 with + | LE_n => 0 + | LE_S m LE_n => 0 + m + | LE_S m (LE_S y h) => 0 + m + end. -Type [n,m:nat][h:(Le n m)] Cases h of - x => x - end. +Type (fun (n m : nat) (h : Le n m) => match h with + | x => x + end). -Type [n,m:nat][h:(Le n m)]<[_,_:nat]nat>Cases h of - (LeO n) => n - | x => O - end. -Type [n,m:nat][h:(Le n m)] Cases h of - (LeO n) => n - | x => O - end. +Type + (fun (n m : nat) (h : Le n m) => + match h return nat with + | LeO n => n + | x => 0 + end). +Type (fun (n m : nat) (h : Le n m) => match h with + | LeO n => n + | x => 0 + end). -Type [n:nat]<[_:nat]nat->nat>Cases niln of - niln => [_:nat]O - | (consn n a niln) => [_:nat]O - | (consn n a (consn m b l)) => [_:nat](plus n m) - end. +Type + (fun n : nat => + match niln return (nat -> nat) with + | niln => fun _ : nat => 0 + | consn n a niln => fun _ : nat => 0 + | consn n a (consn m b l) => fun _ : nat => n + m + end). -Type [n:nat] Cases niln of - niln => [_:nat]O - | (consn n a niln) => [_:nat]O - | (consn n a (consn m b l)) => [_:nat](plus n m) - end. +Type + (fun n : nat => + match niln with + | niln => fun _ : nat => 0 + | consn n a niln => fun _ : nat => 0 + | consn n a (consn m b l) => fun _ : nat => n + m + end). -Type [A:Set][n:nat][l:(Listn A n)] - <[_:nat]nat->nat>Cases l of - Niln => [_:nat]O - | (Consn n a Niln) => [_:nat] n - | (Consn n a (Consn m b l)) => [_:nat](plus n m) - end. +Type + (fun (A : Set) (n : nat) (l : Listn A n) => + match l return (nat -> nat) with + | Niln => fun _ : nat => 0 + | Consn n a Niln => fun _ : nat => n + | Consn n a (Consn m b l) => fun _ : nat => n + m + end). -Type [A:Set][n:nat][l:(Listn A n)] - Cases l of - Niln => [_:nat]O - | (Consn n a Niln) => [_:nat] n - | (Consn n a (Consn m b l)) => [_:nat](plus n m) - end. +Type + (fun (A : Set) (n : nat) (l : Listn A n) => + match l with + | Niln => fun _ : nat => 0 + | Consn n a Niln => fun _ : nat => n + | Consn n a (Consn m b l) => fun _ : nat => n + m + end). (* Alsos tests for multiple _ patterns *) -Type [A:Set][n:nat][l:(Listn A n)] - <[n:nat](Listn A n)>Cases l of - (Niln as b) => b - | ((Consn _ _ _ ) as b)=> b - end. +Type + (fun (A : Set) (n : nat) (l : Listn A n) => + match l in (Listn _ n) return (Listn A n) with + | Niln as b => b + | Consn _ _ _ as b => b + end). (** Horrible error message! @@ -962,215 +1077,278 @@ Type [A:Set][n:nat][l:(Listn A n)] end. ******) -Type <[n:nat](listn n)>Cases niln of - (niln as b) => b - | ((consn _ _ _ ) as b)=> b - end. - +Type + match niln in (listn n) return (listn n) with + | niln as b => b + | consn _ _ _ as b => b + end. -Type <[n:nat](listn n)>Cases niln of - (niln as b) => b - | x => x - end. -Type [n,m:nat][h:(LE n m)]<[_:nat]nat->nat>Cases h of - LE_n => [_:nat]n - | (LE_S m LE_n) => [_:nat](plus n m) - | (LE_S m (LE_S y h)) => [_:nat](plus m y ) - end. -Type [n,m:nat][h:(LE n m)]Cases h of - LE_n => [_:nat]n - | (LE_S m LE_n) => [_:nat](plus n m) - | (LE_S m (LE_S y h)) => [_:nat](plus m y ) - end. +Type + match niln in (listn n) return (listn n) with + | niln as b => b + | x => x + end. +Type + (fun (n m : nat) (h : LE n m) => + match h return (nat -> nat) with + | LE_n => fun _ : nat => n + | LE_S m LE_n => fun _ : nat => n + m + | LE_S m (LE_S y h) => fun _ : nat => m + y + end). +Type + (fun (n m : nat) (h : LE n m) => + match h with + | LE_n => fun _ : nat => n + | LE_S m LE_n => fun _ : nat => n + m + | LE_S m (LE_S y h) => fun _ : nat => m + y + end). -Type [n,m:nat][h:(LE n m)] - <[_:nat]nat>Cases h of - LE_n => n - | (LE_S m LE_n ) => (plus n m) - | (LE_S m (LE_S y LE_n )) => (plus (plus n m) y) - | (LE_S m (LE_S y (LE_S y' h))) => (plus (plus n m) (plus y y')) - end. +Type + (fun (n m : nat) (h : LE n m) => + match h return nat with + | LE_n => n + | LE_S m LE_n => n + m + | LE_S m (LE_S y LE_n) => n + m + y + | LE_S m (LE_S y (LE_S y' h)) => n + m + (y + y') + end). -Type [n,m:nat][h:(LE n m)] - Cases h of - LE_n => n - | (LE_S m LE_n ) => (plus n m) - | (LE_S m (LE_S y LE_n )) => (plus (plus n m) y) - | (LE_S m (LE_S y (LE_S y' h))) => (plus (plus n m) (plus y y')) - end. +Type + (fun (n m : nat) (h : LE n m) => + match h with + | LE_n => n + | LE_S m LE_n => n + m + | LE_S m (LE_S y LE_n) => n + m + y + | LE_S m (LE_S y (LE_S y' h)) => n + m + (y + y') + end). -Type [n,m:nat][h:(LE n m)]<[_:nat]nat>Cases h of - LE_n => n - | (LE_S m LE_n) => (plus n m) - | (LE_S m (LE_S y h)) => (plus (plus n m) y) - end. +Type + (fun (n m : nat) (h : LE n m) => + match h return nat with + | LE_n => n + | LE_S m LE_n => n + m + | LE_S m (LE_S y h) => n + m + y + end). -Type [n,m:nat][h:(LE n m)]Cases h of - LE_n => n - | (LE_S m LE_n) => (plus n m) - | (LE_S m (LE_S y h)) => (plus (plus n m) y) - end. -Type [n,m:nat] - <[_,_:nat]nat>Cases (LeO O) of - (LeS n m h) =>(plus n m) - | x => O - end. +Type + (fun (n m : nat) (h : LE n m) => + match h with + | LE_n => n + | LE_S m LE_n => n + m + | LE_S m (LE_S y h) => n + m + y + end). -Type [n,m:nat] - Cases (LeO O) of - (LeS n m h) =>(plus n m) - | x => O - end. +Type + (fun n m : nat => + match LeO 0 return nat with + | LeS n m h => n + m + | x => 0 + end). + +Type (fun n m : nat => match LeO 0 with + | LeS n m h => n + m + | x => 0 + end). -Parameter test : (n:nat){(le O n)}+{False}. -Type [n:nat]<nat>Cases (test n) of - (left _) => O - | _ => O end. +Parameter test : forall n : nat, {0 <= n} + {False}. +Type (fun n : nat => match test n return nat with + | left _ => 0 + | _ => 0 + end). -Type [n:nat] <nat> Cases (test n) of - (left _) => O - | _ => O end. +Type (fun n : nat => match test n return nat with + | left _ => 0 + | _ => 0 + end). -Type [n:nat]Cases (test n) of - (left _) => O - | _ => O end. +Type (fun n : nat => match test n with + | left _ => 0 + | _ => 0 + end). -Parameter compare : (n,m:nat)({(lt n m)}+{n=m})+{(gt n m)}. -Type <nat>Cases (compare O O) of - (* k<i *) (inleft (left _)) => O - | (* k=i *) (inleft _) => O - | (* k>i *) (inright _) => O end. +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 + end. -Type Cases (compare O O) of - (* k<i *) (inleft (left _)) => O - | (* k=i *) (inleft _) => O - | (* k>i *) (inright _) => O end. +Type + match compare 0 0 with + + (* k<i *) | inleft (left _) => 0 + (* k=i *) | inleft _ => 0 + (* k>i *) | inright _ => 0 + end. -CoInductive SStream [A:Set] : (nat->A->Prop)->Type := -scons : - (P:nat->A->Prop)(a:A)(P O a)->(SStream A [n:nat](P (S n)))->(SStream A P). +CoInductive SStream (A : Set) : (nat -> A -> Prop) -> Type := + scons : + forall (P : nat -> A -> Prop) (a : A), + P 0 a -> SStream A (fun n : nat => P (S n)) -> SStream A P. Parameter B : Set. -Type - [P:nat->B->Prop][x:(SStream B P)]<[_:nat->B->Prop]B>Cases x of - (scons _ a _ _) => a end. +Type + (fun (P : nat -> B -> Prop) (x : SStream B P) => + match x return B with + | scons _ a _ _ => a + end). -Type - [P:nat->B->Prop][x:(SStream B P)] Cases x of - (scons _ a _ _) => a end. +Type + (fun (P : nat -> B -> Prop) (x : SStream B P) => + match x with + | scons _ a _ _ => a + end). -Type <nat*nat>Cases (O,O) of (x,y) => ((S x),(S y)) end. -Type <nat*nat>Cases (O,O) of ((x as b), y) => ((S x),(S y)) end. -Type <nat*nat>Cases (O,O) of (pair x y) => ((S x),(S y)) end. +Type match (0, 0) return (nat * nat) with + | (x, y) => (S x, S y) + end. +Type match (0, 0) return (nat * nat) with + | (b, y) => (S b, S y) + end. +Type match (0, 0) return (nat * nat) with + | (x, y) => (S x, S y) + end. -Type Cases (O,O) of (x,y) => ((S x),(S y)) end. -Type Cases (O,O) of ((x as b), y) => ((S x),(S y)) end. -Type Cases (O,O) of (pair x y) => ((S x),(S y)) end. +Type match (0, 0) with + | (x, y) => (S x, S y) + end. +Type match (0, 0) with + | (b, y) => (S b, S y) + end. +Type match (0, 0) with + | (x, y) => (S x, S y) + end. -Parameter concat : (A:Set)(List A) ->(List A) ->(List A). +Parameter concat : forall A : Set, List A -> List A -> List A. -Type <(List nat)>Cases (Nil nat) (Nil nat) of - (Nil as b) x => (concat nat b x) - | ((Cons _ _) as d) (Nil as c) => (concat nat d c) - | _ _ => (Nil nat) - end. -Type Cases (Nil nat) (Nil nat) of - (Nil as b) x => (concat nat b x) - | ((Cons _ _) as d) (Nil as c) => (concat nat d c) - | _ _ => (Nil nat) - end. +Type + match Nil nat, Nil nat return (List nat) with + | Nil as b, x => concat nat b x + | Cons _ _ as d, Nil as c => concat nat d c + | _, _ => Nil nat + end. +Type + match Nil nat, Nil nat with + | Nil as b, x => concat nat b x + | Cons _ _ as d, Nil as c => concat nat d c + | _, _ => Nil nat + end. Inductive redexes : Set := - VAR : nat -> redexes + | VAR : nat -> redexes | Fun : redexes -> redexes - | Ap : bool -> redexes -> redexes -> redexes. - -Fixpoint regular [U:redexes] : Prop := <Prop>Cases U of - (VAR n) => True -| (Fun V) => (regular V) -| (Ap true ((Fun _) as V) W) => (regular V) /\ (regular W) -| (Ap true _ W) => False -| (Ap false V W) => (regular V) /\ (regular W) -end. + | Ap : bool -> redexes -> redexes -> redexes. + +Fixpoint regular (U : redexes) : Prop := + match U return Prop with + | VAR n => True + | Fun V => regular V + | Ap true (Fun _ as V) W => regular V /\ regular W + | Ap true _ W => False + | Ap false V W => regular V /\ regular W + end. -Type [n:nat]Cases n of O => O | (S ((S n) as V)) => V | _ => O end. +Type (fun n : nat => match n with + | O => 0 + | S (S n as V) => V + | _ => 0 + end). Reset concat. -Parameter concat :(n:nat) (listn n) -> (m:nat) (listn m)-> (listn (plus n m)). -Type [n:nat][l:(listn n)][m:nat][l':(listn m)] - <[n,_:nat](listn (plus n m))>Cases l l' of - niln x => x - | (consn n a l'') x =>(consn (plus n m) a (concat n l'' m x)) - end. - -Type [x,y,z:nat] - [H:x=y] - [H0:y=z]<[_:nat]x=z>Cases H of refl_equal => - <[n:nat]x=n>Cases H0 of refl_equal => H - end - end. - -Type [h:False]<False>Cases h of end. +Parameter + concat : + forall n : nat, listn n -> forall m : nat, listn m -> listn (n + m). +Type + (fun (n : nat) (l : listn n) (m : nat) (l' : listn m) => + match l in (listn n), l' return (listn (n + m)) with + | niln, x => x + | consn n a l'', x => consn (n + m) a (concat n l'' m x) + end). -Type [h:False]<True>Cases h of end. +Type + (fun (x y z : nat) (H : x = y) (H0 : y = z) => + match H return (x = z) with + | refl_equal => + match H0 in (_ = n) return (x = n) with + | refl_equal => H + end + end). + +Type (fun h : False => match h return False with + end). -Definition is_zero := [n:nat]Cases n of O => True | _ => False end. +Type (fun h : False => match h return True with + end). -Type [n:nat][h:O=(S n)]<[n:nat](is_zero n)>Cases h of refl_equal => I end. +Definition is_zero (n : nat) := match n with + | O => True + | _ => False + end. -Definition disc : (n:nat)O=(S n)->False := - [n:nat][h:O=(S n)] - <[n:nat](is_zero n)>Cases h of refl_equal => I end. +Type + (fun (n : nat) (h : 0 = S n) => + match h in (_ = n) return (is_zero n) with + | refl_equal => I + end). + +Definition disc (n : nat) (h : 0 = S n) : False := + match h in (_ = n) return (is_zero n) with + | refl_equal => I + end. -Definition nlength3 := [n:nat] [l: (listn n)] - Cases l of - niln => O - | (consn O _ _) => (S O) - | (consn (S n) _ _) => (S (S n)) - end. +Definition nlength3 (n : nat) (l : listn n) := + match l with + | niln => 0 + | consn O _ _ => 1 + | consn (S n) _ _ => S (S n) + end. (* == Testing strategy elimintation predicate synthesis == *) Section titi. -Variable h:False. -Type Cases O of - O => O - | _ => (Except h) - end. +Variable h : False. +Type match 0 with + | O => 0 + | _ => except h + end. End titi. -Type Cases niln of - (consn _ a niln) => a - | (consn n _ x) => O - | niln => O - end. +Type match niln with + | consn _ a niln => a + | consn n _ x => 0 + | niln => 0 + end. -Inductive wsort : Set := ws : wsort | wt : wsort. -Inductive TS : wsort->Set := - id :(TS ws) -| lift:(TS ws)->(TS ws). +Inductive wsort : Set := + | ws : wsort + | wt : wsort. +Inductive TS : wsort -> Set := + | id : TS ws + | lift : TS ws -> TS ws. -Type [b:wsort][M:(TS b)][N:(TS b)] - Cases M N of - (lift M1) id => False - | _ _ => True - end. +Type + (fun (b : wsort) (M N : TS b) => + match M, N with + | lift M1, id => False + | _, _ => True + end). @@ -1182,51 +1360,56 @@ Type [b:wsort][M:(TS b)][N:(TS b)] Parameter LTERM : nat -> Set. -Mutual Inductive TERM : Type := - var : TERM - | oper : (op:nat) (LTERM op) -> TERM. - -Parameter t1, t2:TERM. +Inductive TERM : Type := + | var : TERM + | oper : forall op : nat, LTERM op -> TERM. -Type Cases t1 t2 of - var var => True +Parameter t1 t2 : TERM. - | (oper op1 l1) (oper op2 l2) => False - | _ _ => False - end. +Type + match t1, t2 with + | var, var => True + | oper op1 l1, oper op2 l2 => False + | _, _ => False + end. Reset LTERM. -Require Peano_dec. -Parameter n:nat. -Definition eq_prf := (EXT m | n=m). -Parameter p:eq_prf . +Require Import Peano_dec. +Parameter n : nat. +Definition eq_prf := exists m : _, n = m. +Parameter p : eq_prf. -Type Cases p of - (exT_intro c eqc) => - Cases (eq_nat_dec c n) of - (right _) => (refl_equal ? n) - |(left y) (* c=n*) => (refl_equal ? n) - end - end. +Type + match p with + | ex_intro c eqc => + match eq_nat_dec c n with + | right _ => refl_equal n + | left y => (* c=n*) refl_equal n + end + end. -Parameter ordre_total : nat->nat->Prop. +Parameter ordre_total : nat -> nat -> Prop. -Parameter N_cla:(N:nat){N=O}+{N=(S O)}+{(ge N (S (S O)))}. +Parameter N_cla : forall N : nat, {N = 0} + {N = 1} + {N >= 2}. -Parameter exist_U2:(N:nat)(ge N (S (S O)))-> - {n:nat|(m:nat)(lt O m)/\(le m N) - /\(ordre_total n m) - /\(lt O n)/\(lt n N)}. +Parameter + exist_U2 : + forall N : nat, + N >= 2 -> + {n : nat | + forall m : nat, 0 < m /\ m <= N /\ ordre_total n m /\ 0 < n /\ n < N}. -Type [N:nat](Cases (N_cla N) of - (inright H)=>(Cases (exist_U2 N H) of - (exist a b)=>a - end) - | _ => O - end). +Type + (fun N : nat => + match N_cla N with + | inright H => match exist_U2 N H with + | exist a b => a + end + | _ => 0 + end). @@ -1238,148 +1421,159 @@ Type [N:nat](Cases (N_cla N) of (* == To test that terms named with AS are correctly absolutized before substitution in rhs == *) -Type [n:nat]<[n:nat]nat>Cases (n) of - O => O - | (S O) => O - | ((S (S n1)) as N) => N - end. +Type + (fun n : nat => + match n return nat with + | O => 0 + | S O => 0 + | S (S n1) as N => N + end). (* ========= *) -Type <[n:nat][_:(listn n)]Prop>Cases niln of - niln => True - | (consn (S O) _ _) => False - | _ => True end. - -Type <[n:nat][_:(listn n)]Prop>Cases niln of - niln => True - | (consn (S (S O)) _ _) => False - | _ => True end. - - -Type <[n,m:nat][h:(Le n m)]nat>Cases (LeO O) of - (LeO _) => O - | (LeS (S x) _ _) => x - | _ => (S O) end. - -Type <[n,m:nat][h:(Le n m)]nat>Cases (LeO O) of - (LeO _) => O - | (LeS (S x) (S y) _) => x - | _ => (S O) end. - -Type <[n,m:nat][h:(Le n m)]nat>Cases (LeO O) of - (LeO _) => O - | (LeS ((S x) as b) (S y) _) => b - | _ => (S O) end. +Type + match niln in (listn n) return Prop with + | niln => True + | consn (S O) _ _ => False + | _ => True + end. +Type + match niln in (listn n) return Prop with + | niln => True + | consn (S (S O)) _ _ => False + | _ => True + end. -Parameter ff: (n,m:nat)~n=m -> ~(S n)=(S m). -Parameter discr_r : (n:nat) ~(O=(S n)). -Parameter discr_l : (n:nat) ~((S n)=O). +Type + match LeO 0 as h in (Le n m) return nat with + | LeO _ => 0 + | LeS (S x) _ _ => x + | _ => 1 + end. -Type -[n:nat] - <[n:nat]n=O\/~n=O>Cases n of - O => (or_introl ? ~O=O (refl_equal ? O)) - | (S x) => (or_intror (S x)=O ? (discr_l x)) +Type + match LeO 0 as h in (Le n m) return nat with + | LeO _ => 0 + | LeS (S x) (S y) _ => x + | _ => 1 end. +Type + match LeO 0 as h in (Le n m) return nat with + | LeO _ => 0 + | LeS (S x as b) (S y) _ => b + | _ => 1 + end. -Fixpoint eqdec [n:nat] : (m:nat) n=m \/ ~n=m := -[m:nat] - <[n,m:nat] n=m \/ ~n=m>Cases n m of - O O => (or_introl ? ~O=O (refl_equal ? O)) - | O (S x) => (or_intror O=(S x) ? (discr_r x)) - | (S x) O => (or_intror ? ~(S x)=O (discr_l x)) +Parameter ff : forall n m : nat, n <> m -> S n <> S m. +Parameter discr_r : forall n : nat, 0 <> S n. +Parameter discr_l : forall n : nat, S n <> 0. - | (S x) (S y) => - <(S x)=(S y)\/~(S x)=(S y)>Cases (eqdec x y) of - (or_introl h) => (or_introl ? ~(S x)=(S y) (f_equal nat nat S x y h)) - | (or_intror h) => (or_intror (S x)=(S y) ? (ff x y h)) +Type + (fun n : nat => + match n return (n = 0 \/ n <> 0) with + | O => or_introl (0 <> 0) (refl_equal 0) + | S x => or_intror (S x = 0) (discr_l x) + end). + + +Fixpoint eqdec (n m : nat) {struct n} : n = m \/ n <> m := + match n, m return (n = m \/ n <> m) with + | O, O => or_introl (0 <> 0) (refl_equal 0) + | O, S x => or_intror (0 = S x) (discr_r x) + | S x, O => or_intror _ (discr_l x) + | S x, S y => + match eqdec x y return (S x = S y \/ S x <> S y) with + | or_introl h => or_introl (S x <> S y) (f_equal S h) + | or_intror h => or_intror (S x = S y) (ff x y h) end - end. + end. Reset eqdec. -Fixpoint eqdec [n:nat] : (m:nat) n=m \/ ~n=m := -<[n:nat] (m:nat)n=m \/ ~n=m>Cases n of - O => [m:nat] <[m:nat]O=m\/~O=m>Cases m of - O => (or_introl ? ~O=O (refl_equal nat O)) - |(S x) => (or_intror O=(S x) ? (discr_r x)) - end - | (S x) => [m:nat] - <[m:nat](S x)=m\/~(S x)=m>Cases m of - O => (or_intror (S x)=O ? (discr_l x)) - | (S y) => - <(S x)=(S y)\/~(S x)=(S y)>Cases (eqdec x y) of - (or_introl h) => (or_introl ? ~(S x)=(S y) (f_equal ? ? S x y h)) - | (or_intror h) => (or_intror (S x)=(S y) ? (ff x y h)) - end - end - end. - - -Inductive empty : (n:nat)(listn n)-> Prop := - intro_empty: (empty O niln). - -Parameter inv_empty : (n,a:nat)(l:(listn n)) ~(empty (S n) (consn n a l)). - -Type -[n:nat] [l:(listn n)] - <[n:nat] [l:(listn n)](empty n l) \/ ~(empty n l)>Cases l of - niln => (or_introl ? ~(empty O niln) intro_empty) - | ((consn n a y) as b) => (or_intror (empty (S n) b) ? (inv_empty n a y)) +Fixpoint eqdec (n : nat) : forall m : nat, n = m \/ n <> m := + match n return (forall m : nat, n = m \/ n <> m) with + | O => + fun m : nat => + match m return (0 = m \/ 0 <> m) with + | O => or_introl (0 <> 0) (refl_equal 0) + | S x => or_intror (0 = S x) (discr_r x) + end + | S x => + fun m : nat => + match m return (S x = m \/ S x <> m) with + | O => or_intror (S x = 0) (discr_l x) + | S y => + match eqdec x y return (S x = S y \/ S x <> S y) with + | or_introl h => or_introl (S x <> S y) (f_equal S h) + | or_intror h => or_intror (S x = S y) (ff x y h) + end + end end. -Reset ff. -Parameter ff: (n,m:nat)~n=m -> ~(S n)=(S m). -Parameter discr_r : (n:nat) ~(O=(S n)). -Parameter discr_l : (n:nat) ~((S n)=O). - -Type -[n:nat] - <[n:nat]n=O\/~n=O>Cases n of - O => (or_introl ? ~O=O (refl_equal ? O)) - | (S x) => (or_intror (S x)=O ? (discr_l x)) - end. +Inductive empty : forall n : nat, listn n -> Prop := + intro_empty : empty 0 niln. -Fixpoint eqdec [n:nat] : (m:nat) n=m \/ ~n=m := -[m:nat] - <[n,m:nat] n=m \/ ~n=m>Cases n m of - O O => (or_introl ? ~O=O (refl_equal ? O)) +Parameter + inv_empty : forall (n a : nat) (l : listn n), ~ empty (S n) (consn n a l). - | O (S x) => (or_intror O=(S x) ? (discr_r x)) +Type + (fun (n : nat) (l : listn n) => + match l in (listn n) return (empty n l \/ ~ empty n l) with + | niln => or_introl (~ empty 0 niln) intro_empty + | consn n a y as b => or_intror (empty (S n) b) (inv_empty n a y) + end). - | (S x) O => (or_intror ? ~(S x)=O (discr_l x)) +Reset ff. +Parameter ff : forall n m : nat, n <> m -> S n <> S m. +Parameter discr_r : forall n : nat, 0 <> S n. +Parameter discr_l : forall n : nat, S n <> 0. - | (S x) (S y) => - <(S x)=(S y)\/~(S x)=(S y)>Cases (eqdec x y) of - (or_introl h) => (or_introl ? ~(S x)=(S y) (f_equal nat nat S x y h)) - | (or_intror h) => (or_intror (S x)=(S y) ? (ff x y h)) +Type + (fun n : nat => + match n return (n = 0 \/ n <> 0) with + | O => or_introl (0 <> 0) (refl_equal 0) + | S x => or_intror (S x = 0) (discr_l x) + end). + + +Fixpoint eqdec (n m : nat) {struct n} : n = m \/ n <> m := + match n, m return (n = m \/ n <> m) with + | O, O => or_introl (0 <> 0) (refl_equal 0) + | O, S x => or_intror (0 = S x) (discr_r x) + | S x, O => or_intror _ (discr_l x) + | S x, S y => + match eqdec x y return (S x = S y \/ S x <> S y) with + | or_introl h => or_introl (S x <> S y) (f_equal S h) + | or_intror h => or_intror (S x = S y) (ff x y h) end - end. + end. Reset eqdec. -Fixpoint eqdec [n:nat] : (m:nat) n=m \/ ~n=m := -<[n:nat] (m:nat)n=m \/ ~n=m>Cases n of - O => [m:nat] <[m:nat]O=m\/~O=m>Cases m of - O => (or_introl ? ~O=O (refl_equal nat O)) - |(S x) => (or_intror O=(S x) ? (discr_r x)) - end - | (S x) => [m:nat] - <[m:nat](S x)=m\/~(S x)=m>Cases m of - O => (or_intror (S x)=O ? (discr_l x)) - | (S y) => - <(S x)=(S y)\/~(S x)=(S y)>Cases (eqdec x y) of - (or_introl h) => (or_introl ? ~(S x)=(S y) (f_equal ? ? S x y h)) - | (or_intror h) => (or_intror (S x)=(S y) ? (ff x y h)) - end - end - end. +Fixpoint eqdec (n : nat) : forall m : nat, n = m \/ n <> m := + match n return (forall m : nat, n = m \/ n <> m) with + | O => + fun m : nat => + match m return (0 = m \/ 0 <> m) with + | O => or_introl (0 <> 0) (refl_equal 0) + | S x => or_intror (0 = S x) (discr_r x) + end + | S x => + fun m : nat => + match m return (S x = m \/ S x <> m) with + | O => or_intror (S x = 0) (discr_l x) + | S y => + match eqdec x y return (S x = S y \/ S x <> S y) with + | or_introl h => or_introl (S x <> S y) (f_equal S h) + | or_intror h => or_intror (S x = S y) (ff x y h) + end + end + end. (* ================================================== *) @@ -1387,17 +1581,17 @@ Fixpoint eqdec [n:nat] : (m:nat) n=m \/ ~n=m := (* ================================================== *) -Inductive Empty [A:Set] : (List A)-> Prop := - intro_Empty: (Empty A (Nil A)). +Inductive Empty (A : Set) : List A -> Prop := + intro_Empty : Empty A (Nil A). -Parameter inv_Empty : (A:Set)(a:A)(x:(List A)) ~(Empty A (Cons A a x)). +Parameter + inv_Empty : forall (A : Set) (a : A) (x : List A), ~ Empty A (Cons A a x). Type - <[l:(List nat)](Empty nat l) \/ ~(Empty nat l)>Cases (Nil nat) of - Nil => (or_introl ? ~(Empty nat (Nil nat)) (intro_Empty nat)) - | (Cons a y) => (or_intror (Empty nat (Cons nat a y)) ? - (inv_Empty nat a y)) + match Nil nat as l return (Empty nat l \/ ~ Empty nat l) with + | Nil => or_introl (~ Empty nat (Nil nat)) (intro_Empty nat) + | Cons a y => or_intror (Empty nat (Cons nat a y)) (inv_Empty nat a y) end. @@ -1406,192 +1600,222 @@ Type (* ================================================== *) -Inductive empty : (n:nat)(listn n)-> Prop := - intro_empty: (empty O niln). +Inductive empty : forall n : nat, listn n -> Prop := + intro_empty : empty 0 niln. -Parameter inv_empty : (n,a:nat)(l:(listn n)) ~(empty (S n) (consn n a l)). +Parameter + inv_empty : forall (n a : nat) (l : listn n), ~ empty (S n) (consn n a l). -Type -[n:nat] [l:(listn n)] - <[n:nat] [l:(listn n)](empty n l) \/ ~(empty n l)>Cases l of - niln => (or_introl ? ~(empty O niln) intro_empty) - | ((consn n a y) as b) => (or_intror (empty (S n) b) ? (inv_empty n a y)) - end. +Type + (fun (n : nat) (l : listn n) => + match l in (listn n) return (empty n l \/ ~ empty n l) with + | niln => or_introl (~ empty 0 niln) intro_empty + | consn n a y as b => or_intror (empty (S n) b) (inv_empty n a y) + end). (* ===================================== *) (* Test parametros: *) (* ===================================== *) -Inductive eqlong : (List nat)-> (List nat)-> Prop := - eql_cons : (n,m:nat)(x,y:(List nat)) - (eqlong x y) -> (eqlong (Cons nat n x) (Cons nat m y)) -| eql_nil : (eqlong (Nil nat) (Nil nat)). - - -Parameter V1 : (eqlong (Nil nat) (Nil nat))\/ ~(eqlong (Nil nat) (Nil nat)). -Parameter V2 : (a:nat)(x:(List nat)) - (eqlong (Nil nat) (Cons nat a x))\/ ~(eqlong (Nil nat)(Cons nat a x)). -Parameter V3 : (a:nat)(x:(List nat)) - (eqlong (Cons nat a x) (Nil nat))\/ ~(eqlong (Cons nat a x) (Nil nat)). -Parameter V4 : (a:nat)(x:(List nat))(b:nat)(y:(List nat)) - (eqlong (Cons nat a x)(Cons nat b y)) - \/ ~(eqlong (Cons nat a x) (Cons nat b y)). +Inductive eqlong : List nat -> List nat -> Prop := + | eql_cons : + forall (n m : nat) (x y : List nat), + eqlong x y -> eqlong (Cons nat n x) (Cons nat m y) + | eql_nil : eqlong (Nil nat) (Nil nat). + + +Parameter V1 : eqlong (Nil nat) (Nil nat) \/ ~ eqlong (Nil nat) (Nil nat). +Parameter + V2 : + forall (a : nat) (x : List nat), + eqlong (Nil nat) (Cons nat a x) \/ ~ eqlong (Nil nat) (Cons nat a x). +Parameter + V3 : + forall (a : nat) (x : List nat), + eqlong (Cons nat a x) (Nil nat) \/ ~ eqlong (Cons nat a x) (Nil nat). +Parameter + V4 : + forall (a : nat) (x : List nat) (b : nat) (y : List nat), + eqlong (Cons nat a x) (Cons nat b y) \/ + ~ eqlong (Cons nat a x) (Cons nat b y). Type - <[x,y:(List nat)](eqlong x y)\/~(eqlong x y)>Cases (Nil nat) (Nil nat) of - Nil Nil => V1 - | Nil (Cons a x) => (V2 a x) - | (Cons a x) Nil => (V3 a x) - | (Cons a x) (Cons b y) => (V4 a x b y) - end. + match Nil nat as x, Nil nat as y return (eqlong x y \/ ~ eqlong x y) with + | Nil, Nil => V1 + | Nil, Cons a x => V2 a x + | Cons a x, Nil => V3 a x + | Cons a x, Cons b y => V4 a x b y + end. Type -[x,y:(List nat)] - <[x,y:(List nat)](eqlong x y)\/~(eqlong x y)>Cases x y of - Nil Nil => V1 - | Nil (Cons a x) => (V2 a x) - | (Cons a x) Nil => (V3 a x) - | (Cons a x) (Cons b y) => (V4 a x b y) - end. + (fun x y : List nat => + match x, y return (eqlong x y \/ ~ eqlong x y) with + | Nil, Nil => V1 + | Nil, Cons a x => V2 a x + | Cons a x, Nil => V3 a x + | Cons a x, Cons b y => V4 a x b y + end). (* ===================================== *) -Inductive Eqlong : (n:nat) (listn n)-> (m:nat) (listn m)-> Prop := - Eql_cons : (n,m:nat )(x:(listn n))(y:(listn m)) (a,b:nat) - (Eqlong n x m y) - ->(Eqlong (S n) (consn n a x) (S m) (consn m b y)) -| Eql_niln : (Eqlong O niln O niln). - - -Parameter W1 : (Eqlong O niln O niln)\/ ~(Eqlong O niln O niln). -Parameter W2 : (n,a:nat)(x:(listn n)) - (Eqlong O niln (S n)(consn n a x)) \/ ~(Eqlong O niln (S n) (consn n a x)). -Parameter W3 : (n,a:nat)(x:(listn n)) - (Eqlong (S n) (consn n a x) O niln) \/ ~(Eqlong (S n) (consn n a x) O niln). -Parameter W4 : (n,a:nat)(x:(listn n)) (m,b:nat)(y:(listn m)) - (Eqlong (S n)(consn n a x) (S m) (consn m b y)) - \/ ~(Eqlong (S n)(consn n a x) (S m) (consn m b y)). +Inductive Eqlong : +forall n : nat, listn n -> forall m : nat, listn m -> Prop := + | Eql_cons : + forall (n m : nat) (x : listn n) (y : listn m) (a b : nat), + Eqlong n x m y -> Eqlong (S n) (consn n a x) (S m) (consn m b y) + | Eql_niln : Eqlong 0 niln 0 niln. + + +Parameter W1 : Eqlong 0 niln 0 niln \/ ~ Eqlong 0 niln 0 niln. +Parameter + W2 : + forall (n a : nat) (x : listn n), + Eqlong 0 niln (S n) (consn n a x) \/ ~ Eqlong 0 niln (S n) (consn n a x). +Parameter + W3 : + forall (n a : nat) (x : listn n), + Eqlong (S n) (consn n a x) 0 niln \/ ~ Eqlong (S n) (consn n a x) 0 niln. +Parameter + W4 : + forall (n a : nat) (x : listn n) (m b : nat) (y : listn m), + Eqlong (S n) (consn n a x) (S m) (consn m b y) \/ + ~ Eqlong (S n) (consn n a x) (S m) (consn m b y). Type - <[n:nat][x:(listn n)][m:nat][y:(listn m)] - (Eqlong n x m y)\/~(Eqlong n x m y)>Cases niln niln of - niln niln => W1 - | niln (consn n a x) => (W2 n a x) - | (consn n a x) niln => (W3 n a x) - | (consn n a x) (consn m b y) => (W4 n a x m b y) - end. - - -Type -[n,m:nat][x:(listn n)][y:(listn m)] - <[n:nat][x:(listn n)][m:nat][y:(listn m)] - (Eqlong n x m y)\/~(Eqlong n x m y)>Cases x y of - niln niln => W1 - | niln (consn n a x) => (W2 n a x) - | (consn n a x) niln => (W3 n a x) - | (consn n a x) (consn m b y) => (W4 n a x m b y) - end. - - -Parameter Inv_r : (n,a:nat)(x:(listn n)) ~(Eqlong O niln (S n) (consn n a x)). -Parameter Inv_l : (n,a:nat)(x:(listn n)) ~(Eqlong (S n) (consn n a x) O niln). -Parameter Nff : (n,a:nat)(x:(listn n)) (m,b:nat)(y:(listn m)) - ~(Eqlong n x m y) - -> ~(Eqlong (S n) (consn n a x) (S m) (consn m b y)). - - - -Fixpoint Eqlongdec [n:nat; x:(listn n)] : (m:nat)(y:(listn m)) - (Eqlong n x m y)\/~(Eqlong n x m y) -:= [m:nat][y:(listn m)] - <[n:nat][x:(listn n)][m:nat][y:(listn m)] - (Eqlong n x m y)\/~(Eqlong n x m y)>Cases x y of - niln niln => (or_introl ? ~(Eqlong O niln O niln) Eql_niln) - - | niln ((consn n a x) as L) => - (or_intror (Eqlong O niln (S n) L) ? (Inv_r n a x)) - - | ((consn n a x) as L) niln => - (or_intror (Eqlong (S n) L O niln) ? (Inv_l n a x)) + match + niln as x in (listn n), niln as y in (listn m) + return (Eqlong n x m y \/ ~ Eqlong n x m y) + with + | niln, niln => W1 + | niln, consn n a x => W2 n a x + | consn n a x, niln => W3 n a x + | consn n a x, consn m b y => W4 n a x m b y + end. - | ((consn n a x) as L1) ((consn m b y) as L2) => - <(Eqlong (S n) L1 (S m) L2) \/~(Eqlong (S n) L1 (S m) L2)> - Cases (Eqlongdec n x m y) of - (or_introl h) => - (or_introl ? ~(Eqlong (S n) L1 (S m) L2)(Eql_cons n m x y a b h)) - | (or_intror h) => - (or_intror (Eqlong (S n) L1 (S m) L2) ? (Nff n a x m b y h)) +Type + (fun (n m : nat) (x : listn n) (y : listn m) => + match + x in (listn n), y in (listn m) + return (Eqlong n x m y \/ ~ Eqlong n x m y) + with + | niln, niln => W1 + | niln, consn n a x => W2 n a x + | consn n a x, niln => W3 n a x + | consn n a x, consn m b y => W4 n a x m b y + end). + + +Parameter + Inv_r : + forall (n a : nat) (x : listn n), ~ Eqlong 0 niln (S n) (consn n a x). +Parameter + Inv_l : + forall (n a : nat) (x : listn n), ~ Eqlong (S n) (consn n a x) 0 niln. +Parameter + Nff : + forall (n a : nat) (x : listn n) (m b : nat) (y : listn m), + ~ Eqlong n x m y -> ~ Eqlong (S n) (consn n a x) (S m) (consn m b y). + + + +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) + return (Eqlong n x m y \/ ~ Eqlong n x m y) + with + | niln, niln => or_introl (~ Eqlong 0 niln 0 niln) Eql_niln + | niln, consn n a x as L => or_intror (Eqlong 0 niln (S n) L) (Inv_r n a x) + | consn n a x as L, niln => or_intror (Eqlong (S n) L 0 niln) (Inv_l n a x) + | consn n a x as L1, consn m b y as L2 => + match + Eqlongdec n x m y + return (Eqlong (S n) L1 (S m) L2 \/ ~ Eqlong (S n) L1 (S m) L2) + with + | or_introl h => + or_introl (~ Eqlong (S n) L1 (S m) L2) (Eql_cons n m x y a b h) + | or_intror h => + or_intror (Eqlong (S n) L1 (S m) L2) (Nff n a x m b y h) end - end. + end. (* ============================================== *) (* To test compilation of dependent case *) (* Multiple Patterns *) (* ============================================== *) -Inductive skel: Type := - PROP: skel - | PROD: skel->skel->skel. +Inductive skel : Type := + | PROP : skel + | PROD : skel -> skel -> skel. Parameter Can : skel -> Type. -Parameter default_can : (s:skel) (Can s). +Parameter default_can : forall s : skel, Can s. -Type [s1,s2:skel] -[s1,s2:skel]<[s1:skel][_:skel](Can s1)>Cases s1 s2 of - PROP PROP => (default_can PROP) -| (PROD x y) PROP => (default_can (PROD x y)) -| (PROD x y) _ => (default_can (PROD x y)) -| PROP _ => (default_can PROP) -end. +Type + (fun s1 s2 s1 s2 : skel => + match s1, s2 return (Can s1) with + | PROP, PROP => default_can PROP + | PROD x y, PROP => default_can (PROD x y) + | PROD x y, _ => default_can (PROD x y) + | PROP, _ => default_can PROP + end). (* to test bindings in nested Cases *) (* ================================ *) Inductive Pair : Set := - pnil : Pair | - pcons : Pair -> Pair -> Pair. - -Type [p,q:Pair]Cases p of - (pcons _ x) => - Cases q of - (pcons _ (pcons _ x)) => True - | _ => False - end -| _ => False -end. - - -Type [p,q:Pair]Cases p of - (pcons _ x) => - Cases q of - (pcons _ (pcons _ x)) => - Cases q of - (pcons _ (pcons _ (pcons _ x))) => x + | pnil : Pair + | pcons : Pair -> Pair -> Pair. + +Type + (fun p q : Pair => + match p with + | pcons _ x => match q with + | pcons _ (pcons _ x) => True + | _ => False + end + | _ => False + end). + + +Type + (fun p q : Pair => + match p with + | pcons _ x => + match q with + | pcons _ (pcons _ x) => + match q with + | pcons _ (pcons _ (pcons _ x)) => x | _ => pnil end - | _ => pnil - end -| _ => pnil -end. + | _ => pnil + end + | _ => pnil + end). -Type - [n:nat] - [l:(listn (S n))] - <[z:nat](listn (pred z))>Cases l of - niln => niln - | (consn n _ l) => - <[m:nat](listn m)>Cases l of - niln => niln - | b => b - end - end. +Type + (fun (n : nat) (l : listn (S n)) => + match l in (listn z) return (listn (pred z)) with + | niln => niln + | consn n _ l => + match l in (listn m) return (listn m) with + | niln => niln + | b => b + end + end). (* Test de la syntaxe avec nombres *) -Require Arith. -Type [n]Cases n of (2) => true | _ => false end. - -Require ZArith. -Type [n]Cases n of `0` => true | _ => false end. +Require Import Arith. +Type (fun n => match n with + | S (S O) => true + | _ => false + end). + +Require Import ZArith. +Type (fun n => match n with + | Z0 => true + | _ => false + end). diff --git a/test-suite/success/CasesDep.v b/test-suite/success/CasesDep.v index 0256280ce..0477377e4 100644 --- a/test-suite/success/CasesDep.v +++ b/test-suite/success/CasesDep.v @@ -1,25 +1,28 @@ (* Check forward dependencies *) -Check [P:nat->Prop][Q][A:(P O)->Q][B:(n:nat)(P (S n))->Q][x] - <[_]Q>Cases x of - | (exist O H) => (A H) - | (exist (S n) H) => (B n H) - end. +Check + (fun (P : nat -> Prop) Q (A : P 0 -> Q) (B : forall n : nat, P (S n) -> Q) + x => + match x return Q with + | exist O H => A H + | exist (S n) H => B n H + end). (* Check dependencies in anonymous arguments (from FTA/listn.v) *) -Inductive listn [A:Set] : nat->Set := - niln: (listn A O) -| consn: (a:A)(n:nat)(listn A n)->(listn A (S n)). +Inductive listn (A : Set) : nat -> Set := + | niln : listn A 0 + | consn : forall (a : A) (n : nat), listn A n -> listn A (S n). Section Folding. -Variables B, C : Set. +Variable B C : Set. Variable g : B -> C -> C. Variable c : C. -Fixpoint foldrn [n:nat; bs:(listn B n)] : C := - Cases bs of niln => c - | (consn b _ tl) => (g b (foldrn ? tl)) +Fixpoint foldrn (n : nat) (bs : listn B n) {struct bs} : C := + match bs with + | niln => c + | consn b _ tl => g b (foldrn _ tl) end. End Folding. @@ -30,149 +33,154 @@ End Folding. (* -------------------------------------------------------------------- *) -Require Prelude. -Require Logic_Type. +Require Import Prelude. +Require Import Logic_Type. Section Orderings. - Variable U: Type. + Variable U : Type. - Definition Relation := U -> U -> Prop. + Definition Relation := U -> U -> Prop. - Variable R: Relation. + Variable R : Relation. - Definition Reflexive : Prop := (x: U) (R x x). + Definition Reflexive : Prop := forall x : U, R x x. - Definition Transitive : Prop := (x,y,z: U) (R x y) -> (R y z) -> (R x z). + Definition Transitive : Prop := forall x y z : U, R x y -> R y z -> R x z. - Definition Symmetric : Prop := (x,y: U) (R x y) -> (R y x). + Definition Symmetric : Prop := forall x y : U, R x y -> R y x. - Definition Antisymmetric : Prop := - (x,y: U) (R x y) -> (R y x) -> x==y. + Definition Antisymmetric : Prop := forall x y : U, R x y -> R y x -> x = y. - Definition contains : Relation -> Relation -> Prop := - [R,R': Relation] (x,y: U) (R' x y) -> (R x y). - Definition same_relation : Relation -> Relation -> Prop := - [R,R': Relation] (contains R R') /\ (contains R' R). + 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. + Build_Equivalence : Reflexive -> Transitive -> Symmetric -> Equivalence. Inductive PER : Prop := - Build_PER: Symmetric -> Transitive -> PER. + Build_PER : Symmetric -> Transitive -> PER. End Orderings. (***** Setoid *******) -Inductive Setoid : Type - := Build_Setoid : (S:Type)(R:(Relation S))(Equivalence ? R) -> Setoid. +Inductive Setoid : Type := + Build_Setoid : + forall (S : Type) (R : Relation S), Equivalence _ R -> Setoid. -Definition elem := [A:Setoid] let (S,R,e)=A in S. +Definition elem (A : Setoid) := let (S, R, e) := A in S. -Grammar constr constr1 := - elem [ "|" constr0($s) "|"] -> [ (elem $s) ]. +(* <Warning> : Grammar is replaced by Notation *) -Definition equal := [A:Setoid] - <[s:Setoid](Relation |s|)>let (S,R,e)=A in R. +Definition equal (A : Setoid) := + let (S, R, e) as s return (Relation (elem s)) := A in R. -Grammar constr constr1 := - equal [ constr0($c) "=" "%" "S" constr0($c2) ] -> - [ (equal ? $c $c2) ]. +(* <Warning> : Grammar is replaced by Notation *) -Axiom prf_equiv : (A:Setoid)(Equivalence |A| (equal A)). -Axiom prf_refl : (A:Setoid)(Reflexive |A| (equal A)). -Axiom prf_sym : (A:Setoid)(Symmetric |A| (equal A)). -Axiom prf_trans : (A:Setoid)(Transitive |A| (equal A)). +Axiom prf_equiv : forall A : Setoid, Equivalence (elem A) (equal A). +Axiom prf_refl : forall A : Setoid, Reflexive (elem A) (equal A). +Axiom prf_sym : forall A : Setoid, Symmetric (elem A) (equal A). +Axiom prf_trans : forall A : Setoid, Transitive (elem A) (equal A). Section Maps. -Variables A,B: Setoid. +Variable A B : Setoid. -Definition Map_law := [f:|A| -> |B|] - (x,y:|A|) x =%S y -> (f x) =%S (f y). +Definition Map_law (f : elem A -> elem B) := + forall x y : elem A, equal _ x y -> equal _ (f x) (f y). Inductive Map : Type := - Build_Map : (f:|A| -> |B|)(p:(Map_law f))Map. + Build_Map : forall (f : elem A -> elem B) (p : Map_law f), Map. -Definition explicit_ap := [m:Map] <|A| -> |B|>Match m with - [f:?][p:?]f end. +Definition explicit_ap (m : Map) := + match m return (elem A -> elem B) with + | Build_Map f p => f + end. -Axiom pres : (m:Map)(Map_law (explicit_ap m)). +Axiom pres : forall m : Map, Map_law (explicit_ap m). -Definition ext := [f,g:Map] - (x:|A|) (explicit_ap f x) =%S (explicit_ap g x). +Definition ext (f g : Map) := + forall x : elem A, equal _ (explicit_ap f x) (explicit_ap g x). -Axiom Equiv_map_eq : (Equivalence Map ext). +Axiom Equiv_map_eq : Equivalence Map ext. -Definition Map_setoid := (Build_Setoid Map ext Equiv_map_eq). +Definition Map_setoid := Build_Setoid Map ext Equiv_map_eq. End Maps. -Notation ap := (explicit_ap ? ?). +Notation ap := (explicit_ap _ _). -Grammar constr constr8 := - map_setoid [ constr7($c1) "=>" constr8($c2) ] - -> [ (Map_setoid $c1 $c2) ]. +(* <Warning> : Grammar is replaced by Notation *) -Definition ap2 := [A,B,C:Setoid][f:|(A=>(B=>C))|][a:|A|] (ap (ap f a)). +Definition ap2 (A B C : Setoid) (f : elem (Map_setoid A (Map_setoid B C))) + (a : elem A) := ap (ap f a). (***** posint ******) -Inductive posint : Type - := Z : posint | Suc : posint -> posint. +Inductive posint : Type := + | Z : posint + | Suc : posint -> posint. -Axiom f_equal : (A,B:Type)(f:A->B)(x,y:A) x==y -> (f x)==(f y). -Axiom eq_Suc : (n,m:posint) n==m -> (Suc n)==(Suc m). +Axiom + f_equal : forall (A B : Type) (f : A -> B) (x y : A), x = y -> f x = f y. +Axiom eq_Suc : forall n m : posint, n = m -> Suc n = Suc m. (* The predecessor function *) -Definition pred : posint->posint - := [n:posint](<posint>Case n of (* Z *) Z - (* Suc u *) [u:posint]u end). +Definition pred (n : posint) : posint := + match n return posint with + | Z => (* Z *) Z + (* Suc u *) + | Suc u => u + end. -Axiom pred_Sucn : (m:posint) m==(pred (Suc m)). -Axiom eq_add_Suc : (n,m:posint) (Suc n)==(Suc m) -> n==m. -Axiom not_eq_Suc : (n,m:posint) ~(n==m) -> ~((Suc n)==(Suc m)). +Axiom pred_Sucn : forall m : posint, m = pred (Suc m). +Axiom eq_add_Suc : forall n m : posint, Suc n = Suc m -> n = m. +Axiom not_eq_Suc : forall n m : posint, n <> m -> Suc n <> Suc m. -Definition IsSuc : posint->Prop - := [n:posint](<Prop>Case n of (* Z *) False - (* Suc p *) [p:posint]True end). -Definition IsZero :posint->Prop := - [n:posint]<Prop>Match n with - True - [p:posint][H:Prop]False end. +Definition IsSuc (n : posint) : Prop := + match n return Prop with + | Z => (* Z *) False + (* Suc p *) + | Suc p => True + end. +Definition IsZero (n : posint) : Prop := + match n with + | Z => True + | Suc _ => False + end. -Axiom Z_Suc : (n:posint) ~(Z==(Suc n)). -Axiom Suc_Z: (n:posint) ~(Suc n)==Z. -Axiom n_Sucn : (n:posint) ~(n==(Suc n)). -Axiom Sucn_n : (n:posint) ~(Suc n)==n. -Axiom eqT_symt : (a,b:posint) ~(a==b)->~(b==a). +Axiom Z_Suc : forall n : posint, Z <> Suc n. +Axiom Suc_Z : forall n : posint, Suc n <> Z. +Axiom n_Sucn : forall n : posint, n <> Suc n. +Axiom Sucn_n : forall n : posint, Suc n <> n. +Axiom eqT_symt : forall a b : posint, a <> b -> b <> a. (******* Dsetoid *****) -Definition Decidable :=[A:Type][R:(Relation A)] - (x,y:A)(R x y) \/ ~(R x y). +Definition Decidable (A : Type) (R : Relation A) := + forall x y : A, R x y \/ ~ R x y. -Record DSetoid : Type := -{Set_of : Setoid; - prf_decid : (Decidable |Set_of| (equal Set_of))}. +Record DSetoid : Type := + {Set_of : Setoid; prf_decid : Decidable (elem Set_of) (equal Set_of)}. (* example de Dsetoide d'entiers *) -Axiom eqT_equiv : (Equivalence posint (eqT posint)). -Axiom Eq_posint_deci : (Decidable posint (eqT posint)). +Axiom eqT_equiv : Equivalence posint (eq (A:=posint)). +Axiom Eq_posint_deci : Decidable posint (eq (A:=posint)). (* Dsetoide des posint*) -Definition Set_of_posint := (Build_Setoid posint (eqT posint) eqT_equiv). +Definition Set_of_posint := Build_Setoid posint (eq (A:=posint)) eqT_equiv. -Definition Dposint := (Build_DSetoid Set_of_posint Eq_posint_deci). +Definition Dposint := Build_DSetoid Set_of_posint Eq_posint_deci. @@ -186,23 +194,22 @@ Definition Dposint := (Build_DSetoid Set_of_posint Eq_posint_deci). Section Sig. -Record Signature :Type := -{Sigma : DSetoid; - Arity : (Map (Set_of Sigma) (Set_of Dposint))}. +Record Signature : Type := + {Sigma : DSetoid; Arity : Map (Set_of Sigma) (Set_of Dposint)}. -Variable S:Signature. +Variable S : Signature. Variable Var : DSetoid. -Mutual Inductive TERM : Type := - var : |(Set_of Var)| -> TERM - | oper : (op: |(Set_of (Sigma S))| ) (LTERM (ap (Arity S) op)) -> TERM -with - LTERM : posint -> Type := - nil : (LTERM Z) - | cons : TERM -> (n:posint)(LTERM n) -> (LTERM (Suc n)). +Inductive TERM : Type := + | var : elem (Set_of Var) -> TERM + | oper : + forall op : elem (Set_of (Sigma S)), LTERM (ap (Arity S) op) -> TERM +with LTERM : posint -> Type := + | nil : LTERM Z + | cons : TERM -> forall n : posint, LTERM n -> LTERM (Suc n). @@ -211,51 +218,51 @@ with (* -------------------------------------------------------------------- *) -Parameter t1,t2: TERM. +Parameter t1 t2 : TERM. -Type - Cases t1 t2 of - | (var v1) (var v2) => True - | (oper op1 l1) (oper op2 l2) => False - | _ _ => False - end. +Type + match t1, t2 with + | var v1, var v2 => True + | oper op1 l1, oper op2 l2 => False + | _, _ => False + end. -Parameter n2:posint. -Parameter l1, l2:(LTERM n2). +Parameter n2 : posint. +Parameter l1 l2 : LTERM n2. -Type - Cases l1 l2 of - nil nil => True - | (cons v m y) nil => False - | _ _ => False -end. +Type + match l1, l2 with + | nil, nil => True + | cons v m y, nil => False + | _, _ => False + end. -Type Cases l1 l2 of - nil nil => True - | (cons u n x) (cons v m y) =>False - | _ _ => False -end. +Type + match l1, l2 with + | nil, nil => True + | cons u n x, cons v m y => False + | _, _ => False + end. -Definition equalT [t1:TERM]:TERM->Prop := -[t2:TERM] - Cases t1 t2 of - (var v1) (var v2) => True - | (oper op1 l1) (oper op2 l2) => False - | _ _ => False - end. +Definition equalT (t1 t2 : TERM) : Prop := + match t1, t2 with + | var v1, var v2 => True + | oper op1 l1, oper op2 l2 => False + | _, _ => False + end. -Definition EqListT [n1:posint;l1:(LTERM n1)]: (n2:posint)(LTERM n2)->Prop := -[n2:posint][l2:(LTERM n2)] - Cases l1 l2 of - nil nil => True - | (cons t1 n1' l1') (cons t2 n2' l2') => False - | _ _ => False -end. +Definition EqListT (n1 : posint) (l1 : LTERM n1) (n2 : posint) + (l2 : LTERM n2) : Prop := + match l1, l2 with + | nil, nil => True + | cons t1 n1' l1', cons t2 n2' l2' => False + | _, _ => False + end. Reset equalT. @@ -263,37 +270,52 @@ Reset equalT. (* Initial exemple (without patterns) *) (*-------------------------------------------------------------------*) -Fixpoint equalT [t1:TERM]:TERM->Prop := -<TERM->Prop>Case t1 of - (*var*) [v1:|(Set_of Var)|][t2:TERM] - <Prop>Case t2 of - (*var*)[v2:|(Set_of Var)|] (v1 =%S v2) - (*oper*)[op2:|(Set_of (Sigma S))|][_:(LTERM (ap (Arity S) op2))]False - end - (*oper*)[op1:|(Set_of (Sigma S))|] - [l1:(LTERM (ap (Arity S) op1))][t2:TERM] - <Prop>Case t2 of - (*var*)[v2:|(Set_of Var)|]False - (*oper*)[op2:|(Set_of (Sigma S))|] - [l2:(LTERM (ap (Arity S) op2))] - ((op1=%S op2)/\ (EqListT (ap (Arity S) op1) l1 (ap (Arity S) op2) l2)) - end -end -with EqListT [n1:posint;l1:(LTERM n1)]: (n2:posint)(LTERM n2)->Prop := -<[_:posint](n2:posint)(LTERM n2)->Prop>Case l1 of - (*nil*) [n2:posint][l2:(LTERM n2)] - <[_:posint]Prop>Case l2 of - (*nil*)True - (*cons*)[t2:TERM][n2':posint][l2':(LTERM n2')]False - end - (*cons*)[t1:TERM][n1':posint][l1':(LTERM n1')] - [n2:posint][l2:(LTERM n2)] - <[_:posint]Prop>Case l2 of - (*nil*) False - (*cons*)[t2:TERM][n2':posint][l2':(LTERM n2')] - ((equalT t1 t2) /\ (EqListT n1' l1' n2' l2')) - end -end. +Fixpoint equalT (t1 : TERM) : TERM -> Prop := + match t1 return (TERM -> Prop) with + | var v1 => + (*var*) + fun t2 : TERM => + match t2 return Prop with + | var v2 => + (*var*) equal _ v1 v2 + (*oper*) + | oper op2 _ => False + end + (*oper*) + | oper op1 l1 => + fun t2 : TERM => + match t2 return Prop with + | var v2 => + (*var*) False + (*oper*) + | oper op2 l2 => + equal _ op1 op2 /\ + 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*) + fun (n2 : posint) (l2 : LTERM n2) => + match l2 in (LTERM _) return Prop with + | nil => + (*nil*) True + (*cons*) + | cons t2 n2' l2' => False + end + (*cons*) + | cons t1 n1' l1' => + fun (n2 : posint) (l2 : LTERM n2) => + match l2 in (LTERM _) return Prop with + | nil => + (*nil*) False + (*cons*) + | cons t2 n2' l2' => equalT t1 t2 /\ EqListT n1' l1' n2' l2' + end + end. (* ---------------------------------------------------------------- *) @@ -301,91 +323,97 @@ end. (* ---------------------------------------------------------------- *) Reset equalT. -Fixpoint equalT [t1:TERM]:TERM->Prop := -Cases t1 of - (var v1) => [t2:TERM] - Cases t2 of - (var v2) => (v1 =%S v2) - | (oper op2 _) =>False - end -| (oper op1 l1) => [t2:TERM] - Cases t2 of - (var _) => False - | (oper op2 l2) => (op1=%S op2) - /\ (EqListT (ap (Arity S) op1) l1 (ap (Arity S) op2) l2) - end -end -with EqListT [n1:posint;l1:(LTERM n1)]: (n2:posint)(LTERM n2)->Prop := -<[_:posint](n2:posint)(LTERM n2)->Prop>Cases l1 of - nil => [n2:posint][l2:(LTERM n2)] - Cases l2 of - nil => True - | _ => False - end -| (cons t1 n1' l1') => [n2:posint][l2:(LTERM n2)] - Cases l2 of - nil =>False - | (cons t2 n2' l2') => (equalT t1 t2) - /\ (EqListT n1' l1' n2' l2') - end -end. +Fixpoint equalT (t1 : TERM) : TERM -> Prop := + match t1 with + | var v1 => + fun t2 : TERM => + match t2 with + | var v2 => equal _ v1 v2 + | oper op2 _ => False + end + | oper op1 l1 => + fun t2 : TERM => + match t2 with + | var _ => False + | oper op2 l2 => + equal _ op1 op2 /\ + 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 + | nil => + fun (n2 : posint) (l2 : LTERM n2) => + match l2 with + | nil => True + | _ => False + end + | cons t1 n1' l1' => + fun (n2 : posint) (l2 : LTERM n2) => + match l2 with + | nil => False + | cons t2 n2' l2' => equalT t1 t2 /\ EqListT n1' l1' n2' l2' + end + end. Reset equalT. -Fixpoint equalT [t1:TERM]:TERM->Prop := -Cases t1 of - (var v1) => [t2:TERM] - Cases t2 of - (var v2) => (v1 =%S v2) - | (oper op2 _) =>False - end -| (oper op1 l1) => [t2:TERM] - Cases t2 of - (var _) => False - | (oper op2 l2) => (op1=%S op2) - /\ (EqListT (ap (Arity S) op1) l1 (ap (Arity S) op2) l2) - end -end -with EqListT [n1:posint;l1:(LTERM n1)]: (n2:posint)(LTERM n2)->Prop := -[n2:posint][l2:(LTERM n2)] -Cases l1 of - nil => - Cases l2 of - nil => True - | _ => False - end -| (cons t1 n1' l1') => Cases l2 of - nil =>False - | (cons t2 n2' l2') => (equalT t1 t2) - /\ (EqListT n1' l1' n2' l2') - end -end. +Fixpoint equalT (t1 : TERM) : TERM -> Prop := + match t1 with + | var v1 => + fun t2 : TERM => + match t2 with + | var v2 => equal _ v1 v2 + | oper op2 _ => False + end + | oper op1 l1 => + fun t2 : TERM => + match t2 with + | var _ => False + | oper op2 l2 => + equal _ op1 op2 /\ + EqListT (ap (Arity S) op1) l1 (ap (Arity S) op2) l2 + end + end + + with EqListT (n1 : posint) (l1 : LTERM n1) (n2 : posint) + (l2 : LTERM n2) {struct l1} : Prop := + match l1 with + | nil => match l2 with + | nil => True + | _ => False + end + | cons t1 n1' l1' => + match l2 with + | nil => False + | cons t2 n2' l2' => equalT t1 t2 /\ EqListT n1' l1' n2' l2' + end + end. (* ---------------------------------------------------------------- *) (* Version with multiple patterns *) (* ---------------------------------------------------------------- *) Reset equalT. -Fixpoint equalT [t1:TERM]:TERM->Prop := -[t2:TERM] - Cases t1 t2 of - (var v1) (var v2) => (v1 =%S v2) - - | (oper op1 l1) (oper op2 l2) => - (op1=%S op2) /\ (EqListT (ap (Arity S) op1) l1 (ap (Arity S) op2) l2) - - | _ _ => False - end - -with EqListT [n1:posint;l1:(LTERM n1)]: (n2:posint)(LTERM n2)->Prop := -[n2:posint][l2:(LTERM n2)] - Cases l1 l2 of - nil nil => True - | (cons t1 n1' l1') (cons t2 n2' l2') => (equalT t1 t2) - /\ (EqListT n1' l1' n2' l2') - | _ _ => False -end. +Fixpoint equalT (t1 t2 : TERM) {struct t1} : Prop := + match t1, t2 with + | var v1, var v2 => equal _ v1 v2 + | oper op1 l1, oper op2 l2 => + 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) + (l2 : LTERM n2) {struct l1} : Prop := + match l1, l2 with + | nil, nil => True + | cons t1 n1' l1', cons t2 n2' l2' => + equalT t1 t2 /\ EqListT n1' l1' n2' l2' + | _, _ => False + end. (* ------------------------------------------------------------------ *) @@ -394,12 +422,11 @@ End Sig. (* Exemple soumis par Bruno *) -Definition bProp [b:bool] : Prop := - if b then True else False. +Definition bProp (b : bool) : Prop := if b then True else False. -Definition f0 [F:False;ty:bool]: (bProp ty) := - <[_:bool][ty:bool](bProp ty)>Cases ty ty of - true true => I - | _ false => F - | _ true => I +Definition f0 (F : False) (ty : bool) : bProp ty := + match ty as _, ty return (bProp ty) with + | true, true => I + | _, false => F + | _, true => I end. diff --git a/test-suite/success/Check.v b/test-suite/success/Check.v index 5d183528b..a20490ccf 100644 --- a/test-suite/success/Check.v +++ b/test-suite/success/Check.v @@ -9,6 +9,6 @@ (* This file tests that pretty-printing does not fail *) (* Test of exact output is not specified *) -Check O. +Check 0. Check S. Check nat. diff --git a/test-suite/success/Conjecture.v b/test-suite/success/Conjecture.v index 6db5859b3..ea4b5ff76 100644 --- a/test-suite/success/Conjecture.v +++ b/test-suite/success/Conjecture.v @@ -1,13 +1,13 @@ (* Check keywords Conjecture and Admitted are recognized *) -Conjecture c : (n:nat)n=O. +Conjecture c : forall n : nat, n = 0. Check c. -Theorem d : (n:nat)n=O. +Theorem d : forall n : nat, n = 0. Proof. - NewInduction n. - Reflexivity. - Assert H:False. - 2:NewDestruct H. + induction n. + reflexivity. + assert (H : False). + 2: destruct H. Admitted. diff --git a/test-suite/success/DHyp.v b/test-suite/success/DHyp.v index 73907bc4a..8b1378917 100644 --- a/test-suite/success/DHyp.v +++ b/test-suite/success/DHyp.v @@ -1,14 +1 @@ -V7only [ -HintDestruct Hypothesis h1 (le ? O) 3 [Fun I -> Inversion I ]. -Lemma lem1 : ~(le (S O) O). -Intro H. -DHyp H. -Qed. - -HintDestruct Conclusion h2 (le O ?) 3 [Constructor]. - -Lemma lem2 : (le O O). -DConcl. -Qed. -]. diff --git a/test-suite/success/Decompose.v b/test-suite/success/Decompose.v index 21a3ab5d1..1316cbf95 100644 --- a/test-suite/success/Decompose.v +++ b/test-suite/success/Decompose.v @@ -1,7 +1,9 @@ (* This was a Decompose bug reported by Randy Pollack (29 Mar 2000) *) -Goal (O=O/\((x:nat)(x=x)->(x=x)/\((y:nat)y=y->y=y)))-> True. -Intro H. -Decompose [and] H. (* Was failing *) +Goal +0 = 0 /\ (forall x : nat, x = x -> x = x /\ (forall y : nat, y = y -> y = y)) -> +True. +intro H. +decompose [and] H. (* Was failing *) Abort. diff --git a/test-suite/success/Destruct.v b/test-suite/success/Destruct.v index fdd929bbc..b909e45e7 100644 --- a/test-suite/success/Destruct.v +++ b/test-suite/success/Destruct.v @@ -1,13 +1,13 @@ (* Submitted by Robert Schneck *) -Parameter A,B,C,D : Prop. -Axiom X : A->B->C/\D. +Parameter A B C D : Prop. +Axiom X : A -> B -> C /\ D. -Lemma foo : A->B->C. +Lemma foo : A -> B -> C. Proof. -Intros. -NewDestruct X. (* Should find axiom X and should handle arguments of X *) -Assumption. -Assumption. -Assumption. +intros. +destruct X. (* Should find axiom X and should handle arguments of X *) +assumption. +assumption. +assumption. Qed. diff --git a/test-suite/success/DiscrR.v b/test-suite/success/DiscrR.v index 5d12098f2..54528fb56 100644 --- a/test-suite/success/DiscrR.v +++ b/test-suite/success/DiscrR.v @@ -1,41 +1,41 @@ -Require Reals. -Require DiscrR. +Require Import Reals. +Require Import DiscrR. -Lemma ex0: ``1<>0``. +Lemma ex0 : 1%R <> 0%R. Proof. - DiscrR. -Save. + discrR. +Qed. -Lemma ex1: ``0<>2``. +Lemma ex1 : 0%R <> 2%R. Proof. - DiscrR. -Save. -Lemma ex2: ``4<>3``. + discrR. +Qed. +Lemma ex2 : 4%R <> 3%R. Proof. - DiscrR. -Save. + discrR. +Qed. -Lemma ex3: ``3<>5``. +Lemma ex3 : 3%R <> 5%R. Proof. - DiscrR. -Save. + discrR. +Qed. -Lemma ex4: ``-1<>0``. +Lemma ex4 : (-1)%R <> 0%R. Proof. - DiscrR. -Save. + discrR. +Qed. -Lemma ex5: ``-2<>-3``. +Lemma ex5 : (-2)%R <> (-3)%R. Proof. - DiscrR. -Save. + discrR. +Qed. -Lemma ex6: ``8<>-3``. +Lemma ex6 : 8%R <> (-3)%R. Proof. - DiscrR. -Save. + discrR. +Qed. -Lemma ex7: ``-8<>3``. +Lemma ex7 : (-8)%R <> 3%R. Proof. - DiscrR. -Save. + discrR. +Qed. diff --git a/test-suite/success/Discriminate.v b/test-suite/success/Discriminate.v index 39d2f4bb2..f28c83deb 100644 --- a/test-suite/success/Discriminate.v +++ b/test-suite/success/Discriminate.v @@ -2,10 +2,10 @@ (* Check that Discriminate tries Intro until *) -Lemma l1 : O=(S O)->False. -Discriminate 1. +Lemma l1 : 0 = 1 -> False. + discriminate 1. Qed. -Lemma l2 : (H:O=(S O))H==H. -Discriminate H. +Lemma l2 : forall H : 0 = 1, H = H. + discriminate H. Qed. diff --git a/test-suite/success/Field.v b/test-suite/success/Field.v index aa51e0577..310dfb620 100644 --- a/test-suite/success/Field.v +++ b/test-suite/success/Field.v @@ -10,62 +10,69 @@ (**** Tests of Field with real numbers ****) -Require Reals. +Require Import Reals. (* Example 1 *) -Goal (eps:R)``eps*1/(2+2)+eps*1/(2+2) == eps*1/2``. +Goal +forall eps : R, +(eps * (1 / (2 + 2)) + eps * (1 / (2 + 2)))%R = (eps * (1 / 2))%R. Proof. - Intros. - Field. + intros. + field. Abort. (* Example 2 *) -Goal (f,g:(R->R); x0,x1:R) - ``((f x1)-(f x0))*1/(x1-x0)+((g x1)-(g x0))*1/(x1-x0) == ((f x1)+ - (g x1)-((f x0)+(g x0)))*1/(x1-x0)``. +Goal +forall (f g : R -> R) (x0 x1 : R), +((f x1 - f x0) * (1 / (x1 - x0)) + (g x1 - g x0) * (1 / (x1 - x0)))%R = +((f x1 + g x1 - (f x0 + g x0)) * (1 / (x1 - x0)))%R. Proof. - Intros. - Field. + intros. + field. Abort. (* Example 3 *) -Goal (a,b:R)``1/(a*b)*1/1/b == 1/a``. +Goal forall a b : R, (1 / (a * b) * (1 / 1 / b))%R = (1 / a)%R. Proof. - Intros. - Field. + intros. + field. Abort. (* Example 4 *) -Goal (a,b:R)``a <> 0``->``b <> 0``->``1/(a*b)/1/b == 1/a``. +Goal +forall a b : R, a <> 0%R -> b <> 0%R -> (1 / (a * b) / 1 / b)%R = (1 / a)%R. Proof. - Intros. - Field. + intros. + field. Abort. (* Example 5 *) -Goal (a:R)``1 == 1*1/a*a``. +Goal forall a : R, 1%R = (1 * (1 / a) * a)%R. Proof. - Intros. - Field. + intros. + field. Abort. (* Example 6 *) -Goal (a,b:R)``b == b*/a*a``. +Goal forall a b : R, b = (b * / a * a)%R. Proof. - Intros. - Field. + intros. + field. Abort. (* Example 7 *) -Goal (a,b:R)``b == b*1/a*a``. +Goal forall a b : R, b = (b * (1 / a) * a)%R. Proof. - Intros. - Field. + intros. + field. Abort. (* Example 8 *) -Goal (x,y:R)``x*((1/x)+x/(x+y)) == -(1/y)*y*(-(x*x/(x+y))-1)``. +Goal +forall x y : R, +(x * (1 / x + x / (x + y)))%R = +(- (1 / y) * y * (- (x * (x / (x + y))) - 1))%R. Proof. - Intros. - Field. + intros. + field. Abort. diff --git a/test-suite/success/Fixpoint.v8 b/test-suite/success/Fixpoint.v index 292366242..680046da4 100644 --- a/test-suite/success/Fixpoint.v8 +++ b/test-suite/success/Fixpoint.v @@ -28,3 +28,4 @@ CoFixpoint g (n:nat) (m:=pred n) (l:Stream m) (p:=S n) : Stream p := end l. Eval compute in (fun l => match g 2 (Consn 0 6 l) with Consn _ a _ => a end). + diff --git a/test-suite/success/Fourier.v b/test-suite/success/Fourier.v index f1f7ae080..2d184fef1 100644 --- a/test-suite/success/Fourier.v +++ b/test-suite/success/Fourier.v @@ -1,16 +1,12 @@ -Require Rfunctions. -Require Fourier. +Require Import Rfunctions. +Require Import Fourier. -Lemma l1: - (x, y, z : R) - ``(Rabsolu x-z) <= (Rabsolu x-y)+(Rabsolu y-z)``. -Intros; SplitAbsolu; Fourier. +Lemma l1 : forall x y z : R, Rabs (x - z) <= Rabs (x - y) + Rabs (y - z). +intros; split_Rabs; fourier. Qed. -Lemma l2: - (x, y : R) - ``x < (Rabsolu y)`` -> - ``y < 1`` -> ``x >= 0`` -> ``-y <= 1`` -> ``(Rabsolu x) <= 1``. -Intros. -SplitAbsolu; Fourier. +Lemma l2 : + forall x y : R, x < Rabs y -> y < 1 -> x >= 0 -> - y <= 1 -> Rabs x <= 1. +intros. +split_Rabs; fourier. Qed. diff --git a/test-suite/success/Funind.v b/test-suite/success/Funind.v index 819da2595..84a58a3ad 100644 --- a/test-suite/success/Funind.v +++ b/test-suite/success/Funind.v @@ -1,80 +1,80 @@ -Definition iszero [n:nat] : bool := Cases n of - | O => true - | _ => false - end. - -Functional Scheme iszer_ind := Induction for iszero. - -Lemma toto : (n:nat) n = 0 -> (iszero n) = true. -Intros x eg. -Functional Induction iszero x; Simpl. -Trivial. -Subst x. -Inversion H_eq_. +Definition iszero (n : nat) : bool := + match n with + | O => true + | _ => false + end. + + Functional Scheme iszer_ind := Induction for iszero. + +Lemma toto : forall n : nat, n = 0 -> iszero n = true. +intros x eg. + functional induction iszero x; simpl in |- *. +trivial. + subst x. +inversion H_eq_. Qed. (* We can even reuse the proof as a scheme: *) -Functional Scheme toto_ind := Induction for iszero. + Functional Scheme toto_ind := Induction for iszero. -Definition ftest [n, m:nat] : nat := - Cases n of - | O => Cases m of +Definition ftest (n m : nat) : nat := + match n with + | O => match m with | O => 0 | _ => 1 end - | (S p) => 0 + | S p => 0 end. -Functional Scheme ftest_ind := Induction for ftest. + Functional Scheme ftest_ind := Induction for ftest. -Lemma test1 : (n,m:nat) (le (ftest n m) 2). -Intros n m. -Functional Induction ftest n m;Auto. -Save. +Lemma test1 : forall n m : nat, ftest n m <= 2. +intros n m. + functional induction ftest n m; auto. +Qed. -Lemma test11 : (m:nat) (le (ftest 0 m) 2). -Intros m. -Functional Induction ftest 0 m. -Auto. -Auto. +Lemma test11 : forall m : nat, ftest 0 m <= 2. +intros m. + functional induction ftest 0 m. +auto. +auto. Qed. -Definition lamfix := -[m:nat ] -(Fix trivfun {trivfun [n:nat] : nat := Cases n of - | O => m - | (S p) => (trivfun p) - end}). +Definition lamfix (m : nat) := + fix trivfun (n : nat) : nat := match n with + | O => m + | S p => trivfun p + end. (* Parameter v1 v2 : nat. *) -Lemma lamfix_lem : (v1,v2:nat) (lamfix v1 v2) = v1. -Intros v1 v2. -Functional Induction lamfix v1 v2. -Trivial. -Assumption. +Lemma lamfix_lem : forall v1 v2 : nat, lamfix v1 v2 = v1. +intros v1 v2. + functional induction lamfix v1 v2. +trivial. +assumption. Defined. (* polymorphic function *) -Require PolyList. +Require Import List. -Functional Scheme app_ind := Induction for app. + Functional Scheme app_ind := Induction for app. -Lemma appnil : (A:Set)(l,l':(list A)) l'=(nil A) -> l = (app l l'). -Intros A l l'. -Functional Induction app A l l';Intuition. -Rewrite <- H1;Trivial. -Save. +Lemma appnil : forall (A : Set) (l l' : list A), l' = nil -> l = l ++ l'. +intros A l l'. + functional induction app A l l'; intuition. + rewrite <- H1; trivial. +Qed. @@ -83,10 +83,10 @@ Save. Require Export Arith. -Fixpoint trivfun [n:nat] : nat := - Cases n of +Fixpoint trivfun (n : nat) : nat := + match n with | O => 0 - | (S m) => (trivfun m) + | S m => trivfun m end. @@ -94,22 +94,22 @@ Fixpoint trivfun [n:nat] : nat := Parameter varessai : nat. -Lemma first_try : (trivfun varessai) = 0. -Functional Induction trivfun varessai. -Trivial. -Simpl. -Assumption. +Lemma first_try : trivfun varessai = 0. + functional induction trivfun varessai. +trivial. +simpl in |- *. +assumption. Defined. -Functional Scheme triv_ind := Induction for trivfun. + Functional Scheme triv_ind := Induction for trivfun. -Lemma bisrepetita : (n':nat) (trivfun n') = 0. -Intros n'. -Functional Induction trivfun n'. -Trivial. -Simpl . -Assumption. +Lemma bisrepetita : forall n' : nat, trivfun n' = 0. +intros n'. + functional induction trivfun n'. +trivial. +simpl in |- *. +assumption. Qed. @@ -118,312 +118,335 @@ Qed. -Fixpoint iseven [n:nat] : bool := - Cases n of +Fixpoint iseven (n : nat) : bool := + match n with | O => true - | (S (S m)) => (iseven m) + | S (S m) => iseven m | _ => false end. -Fixpoint funex [n:nat] : nat := - Cases (iseven n) of +Fixpoint funex (n : nat) : nat := + match iseven n with | true => n - | false => Cases n of + | false => match n with | O => 0 - | (S r) => (funex r) + | S r => funex r end end. -Fixpoint nat_equal_bool [n:nat] : nat -> bool := -[m:nat] - Cases n of - | O => Cases m of +Fixpoint nat_equal_bool (n m : nat) {struct n} : bool := + match n with + | O => match m with | O => true | _ => false end - | (S p) => Cases m of + | S p => match m with | O => false - | (S q) => (nat_equal_bool p q) + | S q => nat_equal_bool p q end end. Require Export Div2. -Lemma div2_inf : (n:nat) (le (div2 n) n). -Intros n. -Functional Induction div2 n. -Auto. -Auto. +Lemma div2_inf : forall n : nat, div2 n <= n. +intros n. + functional induction div2 n. +auto. +auto. -Apply le_S. -Apply le_n_S. -Exact H. +apply le_S. +apply le_n_S. +exact H. Qed. (* reuse this lemma as a scheme:*) -Functional Scheme div2_ind := Induction for div2_inf. + Functional Scheme div2_ind := Induction for div2_inf. -Fixpoint nested_lam [n:nat] : nat -> nat := - Cases n of - | O => [m:nat ] 0 - | (S n') => [m:nat ] (plus m (nested_lam n' m)) +Fixpoint nested_lam (n : nat) : nat -> nat := + match n with + | O => fun m : nat => 0 + | S n' => fun m : nat => m + nested_lam n' m end. -Functional Scheme nested_lam_ind := Induction for nested_lam. + Functional Scheme nested_lam_ind := Induction for nested_lam. -Lemma nest : (n, m:nat) (nested_lam n m) = (mult n m). -Intros n m. -Functional Induction nested_lam n m; Auto. +Lemma nest : forall n m : nat, nested_lam n m = n * m. +intros n m. + functional induction nested_lam n m; auto. Qed. -Lemma nest2 : (n, m:nat) (nested_lam n m) = (mult n m). -Intros n m. Pattern n m . -Apply nested_lam_ind; Simpl ; Intros; Auto. +Lemma nest2 : forall n m : nat, nested_lam n m = n * m. +intros n m. pattern n, m in |- *. +apply nested_lam_ind; simpl in |- *; intros; auto. Qed. -Fixpoint essai [x : nat] : nat * nat -> nat := - [p : nat * nat] ( Case p of [n, m : ?] Cases n of - O => O - | (S q) => - Cases x of - O => (S O) - | (S r) => (S (essai r (q, m))) - end - end end ). - -Lemma essai_essai: - (x : nat) - (p : nat * nat) ( Case p of [n, m : ?] (lt O n) -> (lt O (essai x p)) end ). -Intros x p. -(Functional Induction essai x p); Intros. -Inversion H. -Simpl; Try Abstract ( Auto with arith ). -Simpl; Try Abstract ( Auto with arith ). +Fixpoint essai (x : nat) (p : nat * nat) {struct x} : nat := + let (n, m) := p in + match n with + | O => 0 + | S q => match x with + | O => 1 + | 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. + functional induction essai x p; intros. +inversion H. +simpl in |- *; try abstract auto with arith. +simpl in |- *; try abstract auto with arith. Qed. -Fixpoint plus_x_not_five'' [n : nat] : nat -> nat := - [m : nat] let x = (nat_equal_bool m (S (S (S (S (S O)))))) in - let y = O in - Cases n of - O => y - | (S q) => - let recapp = (plus_x_not_five'' q m) in - Cases x of true => (S recapp) | false => (S recapp) end - end. - -Lemma notplusfive'': - (x, y : nat) y = (S (S (S (S (S O))))) -> (plus_x_not_five'' x y) = x. -Intros a b. -Unfold plus_x_not_five''. -(Functional Induction plus_x_not_five'' a b); Intros hyp; Simpl; Auto. +Fixpoint plus_x_not_five'' (n m : nat) {struct n} : nat := + let x := nat_equal_bool m 5 in + let y := 0 in + match n with + | O => y + | S q => + let recapp := plus_x_not_five'' q m in + match x with + | true => S recapp + | false => S recapp + end + end. + +Lemma notplusfive'' : forall x y : nat, y = 5 -> plus_x_not_five'' x y = x. +intros a b. +unfold plus_x_not_five'' in |- *. + functional induction plus_x_not_five'' a b; intros hyp; simpl in |- *; auto. Qed. -Lemma iseq_eq: (n, m : nat) n = m -> (nat_equal_bool n m) = true. -Intros n m. -Unfold nat_equal_bool. -(Functional Induction nat_equal_bool n m); Simpl; Intros hyp; Auto. -Inversion hyp. -Inversion hyp. +Lemma iseq_eq : forall n m : nat, n = m -> nat_equal_bool n m = true. +intros n m. +unfold nat_equal_bool in |- *. + functional induction nat_equal_bool n m; simpl in |- *; intros hyp; auto. +inversion hyp. +inversion hyp. Qed. -Lemma iseq_eq': (n, m : nat) (nat_equal_bool n m) = true -> n = m. -Intros n m. -Unfold nat_equal_bool. -(Functional Induction nat_equal_bool n m); Simpl; Intros eg; Auto. -Inversion eg. -Inversion eg. +Lemma iseq_eq' : forall n m : nat, nat_equal_bool n m = true -> n = m. +intros n m. +unfold nat_equal_bool in |- *. + functional induction nat_equal_bool n m; simpl in |- *; intros eg; auto. +inversion eg. +inversion eg. Qed. -Inductive istrue : bool -> Prop := - istrue0: (istrue true) . +Inductive istrue : bool -> Prop := + istrue0 : istrue true. -Lemma inf_x_plusxy': (x, y : nat) (le x (plus x y)). -Intros n m. -(Functional Induction plus n m); Intros. -Auto with arith. -Auto with arith. +Lemma inf_x_plusxy' : forall x y : nat, x <= x + y. +intros n m. + functional induction plus n m; intros. +auto with arith. +auto with arith. Qed. -Lemma inf_x_plusxy'': (x : nat) (le x (plus x O)). -Intros n. -Unfold plus. -(Functional Induction plus n O); Intros. -Auto with arith. -Apply le_n_S. -Assumption. +Lemma inf_x_plusxy'' : forall x : nat, x <= x + 0. +intros n. +unfold plus in |- *. + functional induction plus n 0; intros. +auto with arith. +apply le_n_S. +assumption. Qed. -Lemma inf_x_plusxy''': (x : nat) (le x (plus O x)). -Intros n. -(Functional Induction plus O n); Intros;Auto with arith. +Lemma inf_x_plusxy''' : forall x : nat, x <= 0 + x. +intros n. + functional induction plus 0 n; intros; auto with arith. Qed. -Fixpoint mod2 [n : nat] : nat := - Cases n of O => O - | (S (S m)) => (S (mod2 m)) - | _ => O end. +Fixpoint mod2 (n : nat) : nat := + match n with + | O => 0 + | S (S m) => S (mod2 m) + | _ => 0 + end. -Lemma princ_mod2: (n : nat) (le (mod2 n) n). -Intros n. -(Functional Induction mod2 n); Simpl; Auto with arith. +Lemma princ_mod2 : forall n : nat, mod2 n <= n. +intros n. + functional induction mod2 n; simpl in |- *; auto with arith. Qed. -Definition isfour : nat -> bool := - [n : nat] Cases n of (S (S (S (S O)))) => true | _ => false end. +Definition isfour (n : nat) : bool := + match n with + | S (S (S (S O))) => true + | _ => false + end. -Definition isononeorfour : nat -> bool := - [n : nat] Cases n of (S O) => true - | (S (S (S (S O)))) => true - | _ => false end. +Definition isononeorfour (n : nat) : bool := + match n with + | S O => true + | S (S (S (S O))) => true + | _ => false + end. -Lemma toto'': (n : nat) (istrue (isfour n)) -> (istrue (isononeorfour n)). -Intros n. -(Functional Induction isononeorfour n); Intros istr; Simpl; Inversion istr. -Apply istrue0. +Lemma toto'' : forall n : nat, istrue (isfour n) -> istrue (isononeorfour n). +intros n. + functional induction isononeorfour n; intros istr; simpl in |- *; + inversion istr. +apply istrue0. Qed. -Lemma toto': (n, m : nat) n = (S (S (S (S O)))) -> (istrue (isononeorfour n)). -Intros n. -(Functional Induction isononeorfour n); Intros m istr; Inversion istr. -Apply istrue0. +Lemma toto' : forall n m : nat, n = 4 -> istrue (isononeorfour n). +intros n. + functional induction isononeorfour n; intros m istr; inversion istr. +apply istrue0. Qed. -Definition ftest4 : nat -> nat -> nat := - [n, m : nat] Cases n of - O => - Cases m of O => O | (S q) => (S O) end - | (S p) => - Cases m of O => O | (S r) => (S O) end - end. - -Lemma test4: (n, m : nat) (le (ftest n m) (S (S O))). -Intros n m. -(Functional Induction ftest n m); Auto with arith. +Definition ftest4 (n m : nat) : nat := + match n with + | O => match m with + | O => 0 + | S q => 1 + end + | S p => match m with + | O => 0 + | 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': (n, m : nat) (le (ftest4 (S n) m) (S (S O))). -Intros n m. -(Functional Induction ftest4 (S n) m). -Auto with arith. -Auto with arith. +Lemma test4' : forall n m : nat, ftest4 (S n) m <= 2. +intros n m. + functional induction ftest4 (S n) m. +auto with arith. +auto with arith. Qed. -Definition ftest44 : nat * nat -> nat -> nat -> nat := - [x : nat * nat] - [n, m : nat] - ( Case x of [p, q : ?] Cases n of - O => - Cases m of O => O | (S q) => (S O) end - | (S p) => - Cases m of O => O | (S r) => (S O) end - end end ). - -Lemma test44: - (pq : nat * nat) (n, m, o, r, s : nat) (le (ftest44 pq n (S m)) (S (S O))). -Intros pq n m o r s. -(Functional Induction ftest44 pq n (S m)). -Auto with arith. -Auto with arith. -Auto with arith. -Auto with arith. +Definition ftest44 (x : nat * nat) (n m : nat) : nat := + let (p, q) := x in + match n with + | O => match m with + | O => 0 + | S q => 1 + end + | S p => match m with + | O => 0 + | 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. + functional induction ftest44 pq n (S m). +auto with arith. +auto with arith. +auto with arith. +auto with arith. Qed. -Fixpoint ftest2 [n : nat] : nat -> nat := - [m : nat] Cases n of - O => - Cases m of O => O | (S q) => O end - | (S p) => (ftest2 p m) - end. +Fixpoint ftest2 (n m : nat) {struct n} : nat := + match n with + | O => match m with + | O => 0 + | S q => 0 + end + | S p => ftest2 p m + end. -Lemma test2: (n, m : nat) (le (ftest2 n m) (S (S O))). -Intros n m. -(Functional Induction ftest2 n m) ; Simpl; Intros; Auto. +Lemma test2 : forall n m : nat, ftest2 n m <= 2. +intros n m. + functional induction ftest2 n m; simpl in |- *; intros; auto. Qed. -Fixpoint ftest3 [n : nat] : nat -> nat := - [m : nat] Cases n of - O => O - | (S p) => - Cases m of O => (ftest3 p O) | (S r) => O end - end. - -Lemma test3: (n, m : nat) (le (ftest3 n m) (S (S O))). -Intros n m. -(Functional Induction ftest3 n m). -Intros. -Auto. -Intros. -Auto. -Intros. -Simpl. -Auto. +Fixpoint ftest3 (n m : nat) {struct n} : nat := + match n with + | O => 0 + | S p => match m with + | O => ftest3 p 0 + | S r => 0 + end + end. + +Lemma test3 : forall n m : nat, ftest3 n m <= 2. +intros n m. + functional induction ftest3 n m. +intros. +auto. +intros. +auto. +intros. +simpl in |- *. +auto. Qed. -Fixpoint ftest5 [n : nat] : nat -> nat := - [m : nat] Cases n of - O => O - | (S p) => - Cases m of O => (ftest5 p O) | (S r) => (ftest5 p r) end - end. - -Lemma test5: (n, m : nat) (le (ftest5 n m) (S (S O))). -Intros n m. -(Functional Induction ftest5 n m). -Intros. -Auto. -Intros. -Auto. -Intros. -Simpl. -Auto. +Fixpoint ftest5 (n m : nat) {struct n} : nat := + match n with + | O => 0 + | S p => match m with + | O => ftest5 p 0 + | 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. +intros. +auto. +intros. +auto. +intros. +simpl in |- *. +auto. Qed. -Definition ftest7 : (n : nat) nat := - [n : nat] Cases (ftest5 n O) of O => O | (S r) => O end. +Definition ftest7 (n : nat) : nat := + match ftest5 n 0 with + | O => 0 + | S r => 0 + end. -Lemma essai7: - (Hrec : (n : nat) (ftest5 n O) = O -> (le (ftest7 n) (S (S O)))) - (Hrec0 : (n, r : nat) (ftest5 n O) = (S r) -> (le (ftest7 n) (S (S O)))) - (n : nat) (le (ftest7 n) (S (S O))). -Intros hyp1 hyp2 n. -Unfold ftest7. -(Functional Induction ftest7 n); Auto. +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) + (n : nat), ftest7 n <= 2. +intros hyp1 hyp2 n. +unfold ftest7 in |- *. + functional induction ftest7 n; auto. Qed. -Fixpoint ftest6 [n : nat] : nat -> nat := - [m : nat] - Cases n of - O => O - | (S p) => - Cases (ftest5 p O) of O => (ftest6 p O) | (S r) => (ftest6 p r) end +Fixpoint ftest6 (n m : nat) {struct n} : nat := + match n with + | O => 0 + | S p => match ftest5 p 0 with + | O => ftest6 p 0 + | S r => ftest6 p r + end end. -Lemma princ6: - ((n, m : nat) n = O -> (le (ftest6 O m) (S (S O)))) -> - ((n, m, p : nat) - (le (ftest6 p O) (S (S O))) -> - (ftest5 p O) = O -> n = (S p) -> (le (ftest6 (S p) m) (S (S O)))) -> - ((n, m, p, r : nat) - (le (ftest6 p r) (S (S O))) -> - (ftest5 p O) = (S r) -> n = (S p) -> (le (ftest6 (S p) m) (S (S O)))) -> - (x, y : nat) (le (ftest6 x y) (S (S O))). -Intros hyp1 hyp2 hyp3 n m. -Generalize hyp1 hyp2 hyp3. -Clear hyp1 hyp2 hyp3. -(Functional Induction ftest6 n m);Auto. +Lemma princ6 : + (forall n m : nat, n = 0 -> ftest6 0 m <= 2) -> + (forall n m p : nat, + ftest6 p 0 <= 2 -> ftest5 p 0 = 0 -> n = S p -> ftest6 (S p) m <= 2) -> + (forall n m p r : nat, + ftest6 p r <= 2 -> ftest5 p 0 = S r -> n = S p -> ftest6 (S p) m <= 2) -> + forall x y : nat, ftest6 x y <= 2. +intros hyp1 hyp2 hyp3 n m. +generalize hyp1 hyp2 hyp3. +clear hyp1 hyp2 hyp3. + functional induction ftest6 n m; auto. Qed. -Lemma essai6: (n, m : nat) (le (ftest6 n m) (S (S O))). -Intros n m. -Unfold ftest6. -(Functional Induction ftest6 n m); Simpl; Auto. +Lemma essai6 : forall n m : nat, ftest6 n m <= 2. +intros n m. +unfold ftest6 in |- *. + functional induction ftest6 n m; simpl in |- *; auto. Qed. diff --git a/test-suite/success/Generalize.v b/test-suite/success/Generalize.v index 0dc739915..980c89dd9 100644 --- a/test-suite/success/Generalize.v +++ b/test-suite/success/Generalize.v @@ -1,7 +1,8 @@ (* Check Generalize Dependent *) -Lemma l1 : [a:=O;b:=a](c:b=b;d:(True->b=b))d=d. -Intros. -Generalize Dependent a. -Intros a b c d. +Lemma l1 : + let a := 0 in let b := a in forall (c : b = b) (d : True -> b = b), d = d. +intros. +generalize dependent a. +intros a b c d. Abort. diff --git a/test-suite/success/Hints.v b/test-suite/success/Hints.v index f32753e02..e1c74048c 100644 --- a/test-suite/success/Hints.v +++ b/test-suite/success/Hints.v @@ -2,47 +2,47 @@ (* Checks that qualified names are accepted *) (* New-style syntax *) -Hint h1 : core arith := Resolve Logic.refl_equal. -Hint h2 := Immediate Logic.trans_equal. -Hint h3 : core := Unfold Logic.sym_equal. -Hint h4 : foo bar := Constructors Logic.eq. -Hint h5 : foo bar := Extern 3 (eq ? ? ?) Apply Logic.refl_equal. +Hint Resolve refl_equal: core arith. +Hint Immediate trans_equal. +Hint Unfold sym_equal: core. +Hint Constructors eq: foo bar. +Hint Extern 3 (_ = _) => apply refl_equal: foo bar. (* Old-style syntax *) -Hints Resolve Coq.Init.Logic.refl_equal Coq.Init.Logic.sym_equal. -Hints Resolve Coq.Init.Logic.refl_equal Coq.Init.Logic.sym_equal : foo. -Hints Immediate Coq.Init.Logic.refl_equal Coq.Init.Logic.sym_equal. -Hints Immediate Coq.Init.Logic.refl_equal Coq.Init.Logic.sym_equal : foo. -Hints Unfold Coq.Init.Datatypes.fst Coq.Init.Logic.sym_equal. -Hints Unfold Coq.Init.Datatypes.fst Coq.Init.Logic.sym_equal : foo. +Hint Resolve refl_equal sym_equal. +Hint Resolve refl_equal sym_equal: foo. +Hint Immediate refl_equal sym_equal. +Hint Immediate refl_equal sym_equal: foo. +Hint Unfold fst sym_equal. +Hint Unfold fst sym_equal: foo. (* What's this stranged syntax ? *) -HintDestruct Conclusion h6 (le ? ?) 4 [ Fun H -> Apply H ]. -HintDestruct Discardable Hypothesis h7 (le ? ?) 4 [ Fun H -> Apply H ]. -HintDestruct Hypothesis h8 (le ? ?) 4 [ Fun H -> Apply H ]. +Hint Destruct h6 := 4 Conclusion (_ <= _) => fun H => apply H. +Hint Destruct h7 := 4 Discardable Hypothesis (_ <= _) => fun H => apply H. +Hint Destruct h8 := 4 Hypothesis (_ <= _) => fun H => apply H. (* Checks that local names are accepted *) Section A. - Remark Refl : (A:Set)(x:A)x=x. + Remark Refl : forall (A : Set) (x : A), x = x. Proof refl_equal. Definition Sym := sym_equal. - Local Trans := trans_equal. + Let Trans := trans_equal. - Hint h1 : foo := Resolve Refl. - Hint h2 : bar := Resolve Sym. - Hint h3 : foo2 := Resolve Trans. + Hint Resolve Refl: foo. + Hint Resolve Sym: bar. + Hint Resolve Trans: foo2. - Hint h2 := Immediate Refl. - Hint h2 := Immediate Sym. - Hint h2 := Immediate Trans. + Hint Immediate Refl. + Hint Immediate Sym. + Hint Immediate Trans. - Hint h3 := Unfold Refl. - Hint h3 := Unfold Sym. - Hint h3 := Unfold Trans. + Hint Unfold Refl. + Hint Unfold Sym. + Hint Unfold Trans. - Hints Resolve Sym Trans Refl. - Hints Immediate Sym Trans Refl. - Hints Unfold Sym Trans Refl. + Hint Resolve Sym Trans Refl. + Hint Immediate Sym Trans Refl. + Hint Unfold Sym Trans Refl. End A. diff --git a/test-suite/success/If.v8 b/test-suite/success/If.v index d044f4ff0..b7f06dcf6 100644 --- a/test-suite/success/If.v8 +++ b/test-suite/success/If.v @@ -4,3 +4,4 @@ Check fun b : bool => if b as b0 return (if b0 then b0 = true else b0 = false) then refl_equal true else refl_equal false. + diff --git a/test-suite/success/ImplicitTactic.v8 b/test-suite/success/ImplicitTactic.v index ccdc0be34..d8fa3043d 100644 --- a/test-suite/success/ImplicitTactic.v8 +++ b/test-suite/success/ImplicitTactic.v @@ -13,3 +13,4 @@ Goal forall n d, d<>0 -> { q:nat & { r:nat | d * q + r = n }}. intros. (* Here, assumption is used to solve the implicit argument of quo *) exists (n / d). + diff --git a/test-suite/success/Inductive.v b/test-suite/success/Inductive.v index 87431a75c..33da5e4ce 100644 --- a/test-suite/success/Inductive.v +++ b/test-suite/success/Inductive.v @@ -1,34 +1,44 @@ (* Check local definitions in context of inductive types *) -Inductive A [C,D:Prop; E:=C; F:=D; x,y:E->F] : E -> Set := - I : (z:E)(A C D x y z). +Inductive A (C D : Prop) (E:=C) (F:=D) (x y : E -> F) : E -> Set := + I : forall z : E, A C D x y z. Check - [C,D:Prop; E:=C; F:=D; x,y:(E ->F); - P:((c:C)(A C D x y c) ->Type); - f:((z:C)(P z (I C D x y z))); - y0:C; a:(A C D x y y0)] - <[y1:C; a0:(A C D x y y1)](P y1 a0)>Cases a of (I x0) => (f x0) end. - -Record B [C,D:Set; E:=C; F:=D; x,y:E->F] : Set := { p : C; q : E }. + (fun C D : Prop => + 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) + (a : A C D x y y0) => + match a as a0 in (A _ _ _ _ y1) return (P y1 a0) with + | I x0 => f x0 + end). + +Record B (C D : Set) (E:=C) (F:=D) (x y : E -> F) : Set := {p : C; q : E}. Check - [C,D:Set; E:=C; F:=D; x,y:(E ->F); - P:((B C D x y) ->Type); - f:((p0,q0:C)(P (Build_B C D x y p0 q0))); - b:(B C D x y)] - <[b0:(B C D x y)](P b0)>Cases b of (Build_B x0 x1) => (f x0 x1) end. + (fun C D : Set => + 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)) + (b : B C D x y) => + match b as b0 return (P b0) with + | Build_B x0 x1 => f x0 x1 + end). (* Check implicit parameters of inductive types (submitted by Pierre Casteran and also implicit in #338) *) Set Implicit Arguments. +Unset Strict Implicit. -CoInductive LList [A:Set] : Set := - | LNil : (LList A) - | LCons : A -> (LList A) -> (LList A). +CoInductive LList (A : Set) : Set := + | LNil : LList A + | LCons : A -> LList A -> LList A. -Implicits LNil [1]. +Implicit Arguments LNil [A]. -Inductive Finite [A:Set] : (LList A) -> Prop := - | Finite_LNil : (Finite LNil) - | Finite_LCons : (a:A) (l:(LList A)) (Finite l) -> (Finite (LCons a l)). +Inductive Finite (A : Set) : LList A -> Prop := + | Finite_LNil : Finite LNil + | Finite_LCons : + forall (a : A) (l : LList A), Finite l -> Finite (LCons a l). diff --git a/test-suite/success/Injection.v b/test-suite/success/Injection.v index fd80cec6f..f8f7c9960 100644 --- a/test-suite/success/Injection.v +++ b/test-suite/success/Injection.v @@ -2,33 +2,37 @@ (* Check that Injection tries Intro until *) -Lemma l1 : (x:nat)(S x)=(S (S x))->False. -Injection 1. -Apply n_Sn. +Lemma l1 : forall x : nat, S x = S (S x) -> False. + injection 1. +apply n_Sn. Qed. -Lemma l2 : (x:nat)(H:(S x)=(S (S x)))H==H->False. -Injection H. -Intros. -Apply (n_Sn x H0). +Lemma l2 : forall (x : nat) (H : S x = S (S x)), H = H -> False. + injection H. +intros. +apply (n_Sn x H0). Qed. (* Check that no tuple needs to be built *) -Lemma l3 : (x,y:nat) - (existS ? [n:nat]({n=n}+{n=n}) x (left ? ? (refl_equal nat x)))= - (existS ? [n:nat]({n=n}+{n=n}) y (left ? ? (refl_equal nat y))) - -> x=y. -Intros x y H. -Injection H. -Exact [H]H. +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)) -> + x = y. +intros x y H. + injection H. +exact (fun H => H). Qed. (* Check that a tuple is built (actually the same as the initial one) *) -Lemma l4 : (p1,p2:{O=O}+{O=O}) - (existS ? [n:nat]({n=n}+{n=n}) O p1)=(existS ? [n:nat]({n=n}+{n=n}) O p2) - ->(existS ? [n:nat]({n=n}+{n=n}) O p1)=(existS ? [n:nat]({n=n}+{n=n}) O p2). -Intros. -Injection H. -Exact [H]H. +Lemma l4 : + forall p1 p2 : {0 = 0} + {0 = 0}, + existS (fun n : nat => {n = n} + {n = n}) 0 p1 = + existS (fun n : nat => {n = n} + {n = n}) 0 p2 -> + existS (fun n : nat => {n = n} + {n = n}) 0 p1 = + existS (fun n : nat => {n = n} + {n = n}) 0 p2. +intros. + injection H. +exact (fun H => H). Qed. diff --git a/test-suite/success/Inversion.v b/test-suite/success/Inversion.v index 2649617bc..f83328e82 100644 --- a/test-suite/success/Inversion.v +++ b/test-suite/success/Inversion.v @@ -1,96 +1,101 @@ -Axiom magic:False. +Axiom magic : False. (* Submitted by Dachuan Yu (bug #220) *) -Fixpoint T[n:nat] : Type := - Cases n of - | O => (nat -> Prop) - | (S n') => (T n') - end. -Inductive R : (n:nat)(T n) -> nat -> Prop := - | RO : (Psi:(T O); l:nat) - (Psi l) -> (R O Psi l) - | RS : (n:nat; Psi:(T (S n)); l:nat) - (R n Psi l) -> (R (S n) Psi l). -Definition Psi00 : (nat -> Prop) := [n:nat] False. -Definition Psi0 : (T O) := Psi00. -Lemma Inversion_RO : (l:nat)(R O Psi0 l) -> (Psi00 l). -Inversion 1. +Fixpoint T (n : nat) : Type := + match n with + | O => nat -> Prop + | S n' => T n' + 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. +Lemma Inversion_RO : forall l : nat, R 0 Psi0 l -> Psi00 l. +inversion 1. Abort. (* Submitted by Pierre Casteran (bug #540) *) Set Implicit Arguments. -Parameter rule: Set -> Type. +Unset Strict Implicit. +Parameter rule : Set -> Type. -Inductive extension [I:Set]:Type := - NL : (extension I) -|add_rule : (rule I) -> (extension I) -> (extension I). +Inductive extension (I : Set) : Type := + | NL : extension I + | add_rule : rule I -> extension I -> extension I. -Inductive in_extension [I :Set;r: (rule I)] : (extension I) -> Type := - in_first : (e:?)(in_extension r (add_rule r e)) -|in_rest : (e,r':?)(in_extension r e) -> (in_extension r (add_rule r' e)). +Inductive in_extension (I : Set) (r : rule I) : extension I -> Type := + | in_first : forall e, in_extension r (add_rule r e) + | in_rest : forall e r', in_extension r e -> in_extension r (add_rule r' e). -Implicits NL [1]. +Implicit Arguments NL [I]. -Inductive super_extension [I:Set;e :(extension I)] : (extension I) -> Type := - super_NL : (super_extension e NL) -| super_add : (r:?)(e': (extension I)) - (in_extension r e) -> - (super_extension e e') -> - (super_extension e (add_rule r e')). +Inductive super_extension (I : Set) (e : extension I) : +extension I -> Type := + | super_NL : super_extension e NL + | super_add : + forall r (e' : extension I), + in_extension r e -> + super_extension e e' -> super_extension e (add_rule r e'). -Lemma super_def : (I :Set)(e1, e2: (extension I)) - (super_extension e2 e1) -> - (ru:?) - (in_extension ru e1) -> - (in_extension ru e2). +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. - Induction 1. - Inversion 1; Auto. - Elim magic. + simple induction 1. + inversion 1; auto. + elim magic. Qed. (* Example from Norbert Schirmer on Coq-Club, Sep 2000 *) +Set Strict Implicit. Unset Implicit Arguments. -Definition Q[n,m:nat;prf:(le n m)]:=True. -Goal (n,m:nat;H:(le (S n) m))(Q (S n) m H)==True. -Intros. -Dependent Inversion_clear H. -Elim magic. -Elim magic. +Definition Q (n m : nat) (prf : n <= m) := True. +Goal forall (n m : nat) (H : S n <= m), Q (S n) m H = True. +intros. +dependent inversion_clear H. +elim magic. +elim magic. Qed. (* Submitted by Boris Yakobowski (bug #529) *) (* Check that Inversion does not fail due to unnormalized evars *) Set Implicit Arguments. +Unset Strict Implicit. Require Import Bvector. Inductive I : nat -> Set := -| C1 : (I (S O)) -| C2 : (k,i:nat)(vector (I i) k) -> (I i). + | C1 : I 1 + | C2 : forall k i : nat, vector (I i) k -> I i. -Inductive SI : (k:nat)(I k) -> (vector nat k) -> nat -> Prop := -| SC2 : (k,i,vf:nat) (v:(vector (I i) k))(xi:(vector nat i))(SI (C2 v) xi vf). +Inductive SI : forall k : nat, I k -> vector nat k -> nat -> Prop := + SC2 : + forall (k i vf : nat) (v : vector (I i) k) (xi : vector nat i), + SI (C2 v) xi vf. -Theorem SUnique : (k:nat)(f:(I k))(c:(vector nat k)) -(v,v':?) (SI f c v) -> (SI f c v') -> v=v'. +Theorem SUnique : + forall (k : nat) (f : I k) (c : vector nat k) v v', + SI f c v -> SI f c v' -> v = v'. Proof. -NewInduction 1. -Intros H ; Inversion H. +induction 1. +intros H; inversion H. Admitted. (* Used to failed at some time *) +Set Strict Implicit. Unset Implicit Arguments. -Parameter bar : (p,q:nat) p=q -> Prop. -Inductive foo : nat -> nat -> Prop := - C : (a,b:nat)(Heq:a = b) (bar a b Heq) -> (foo a b). -Lemma depinv : (a,b:?) (foo a b) -> True. -Intros a b H. -Inversion H. +Parameter bar : forall p q : nat, p = q -> Prop. +Inductive foo : nat -> nat -> Prop := + C : forall (a b : nat) (Heq : a = b), bar a b Heq -> foo a b. +Lemma depinv : forall a b, foo a b -> True. +intros a b H. +inversion H. Abort. diff --git a/test-suite/success/LetIn.v b/test-suite/success/LetIn.v index 0e0b44358..b61ea784b 100644 --- a/test-suite/success/LetIn.v +++ b/test-suite/success/LetIn.v @@ -1,11 +1,11 @@ (* Simple let-in's *) -Definition l1 := [P := O]P. -Definition l2 := [P := nat]P. -Definition l3 := [P := True]P. -Definition l4 := [P := Prop]P. -Definition l5 := [P := Type]P. +Definition l1 := let P := 0 in P. +Definition l2 := let P := nat in P. +Definition l3 := let P := True in P. +Definition l4 := let P := Prop in P. +Definition l5 := let P := Type in P. (* Check casting of let-in *) -Definition l6 := [P := O : nat]P. -Definition l7 := [P := True : Prop]P. -Definition l8 := [P := True : Type]P. +Definition l6 := let P := 0:nat in P. +Definition l7 := let P := True:Prop in P. +Definition l8 := let P := True:Type in P. diff --git a/test-suite/success/MatchFail.v b/test-suite/success/MatchFail.v index d89ee3bec..660ca3cb0 100644 --- a/test-suite/success/MatchFail.v +++ b/test-suite/success/MatchFail.v @@ -6,23 +6,24 @@ Require Export ZArithRing. 2*(POS e)+1 ou 2*(POS e), pour rendre les expressions plus à même d'être utilisées par Ring, lorsque ces expressions contiennent des variables de type positive. *) -Tactic Definition compute_POS := - (Match Context With - | [|- [(POS (xI ?1))]] -> Let v = ?1 In - (Match v With - | [xH] -> - (Fail 1) - |_-> - Rewrite (POS_xI v)) - | [ |- [(POS (xO ?1))]] -> Let v = ?1 In - Match v With - |[xH]-> - (Fail 1) - |[?]-> - Rewrite (POS_xO v)). +Ltac compute_POS := + match goal with + | |- context [(Zpos (xI ?X1))] => + let v := constr:X1 in + match constr:v with + | 1%positive => fail 1 + | _ => rewrite (BinInt.Zpos_xI v) + end + | |- context [(Zpos (xO ?X1))] => + let v := constr:X1 in + match constr:v with + | 1%positive => fail 1 + | _ => rewrite (BinInt.Zpos_xO v) + end + end. -Goal (x:positive)(POS (xI (xI x)))=`4*(POS x)+3`. -Intros. -Repeat compute_POS. -Ring. +Goal forall x : positive, Zpos (xI (xI x)) = (4 * Zpos x + 3)%Z. +intros. +repeat compute_POS. + ring. Qed. diff --git a/test-suite/success/Mod_ltac.v b/test-suite/success/Mod_ltac.v index 1a9f6fc53..44bb3a55e 100644 --- a/test-suite/success/Mod_ltac.v +++ b/test-suite/success/Mod_ltac.v @@ -1,20 +1,20 @@ (* Submitted by Houda Anoun *) Module toto. -Tactic Definition titi:=Auto. +Ltac titi := auto. End toto. Module ti. Import toto. -Tactic Definition equal:= -Match Context With -[ |- ?1=?1]-> titi -| [ |- ?]-> Idtac. +Ltac equal := match goal with + | |- (?X1 = ?X1) => titi + | |- _ => idtac + end. End ti. Import ti. -Definition simple:(a:nat) a=a. -Intro. +Definition simple : forall a : nat, a = a. +intro. equal. Qed. diff --git a/test-suite/success/Mod_params.v b/test-suite/success/Mod_params.v index 098de3cfb..74228bbbf 100644 --- a/test-suite/success/Mod_params.v +++ b/test-suite/success/Mod_params.v @@ -3,10 +3,10 @@ Module Type SIG. End SIG. -Module Type FSIG[X:SIG]. +Module Type FSIG (X: SIG). End FSIG. -Module F[X:SIG]. +Module F (X: SIG). End F. Module Q. @@ -22,57 +22,57 @@ End Q. Module M. Reset M. -Module M[X:SIG]. +Module M (X: SIG). Reset M. -Module M[X,Y:SIG]. +Module M (X Y: SIG). Reset M. -Module M[X:SIG;Y:SIG]. +Module M (X: SIG) (Y: SIG). Reset M. -Module M[X,Y:SIG;Z1,Z:SIG]. +Module M (X Y: SIG) (Z1 Z: SIG). Reset M. -Module M[X:SIG][Y:SIG]. +Module M (X: SIG) (Y: SIG). Reset M. -Module M[X,Y:SIG][Z1,Z:SIG]. +Module M (X Y: SIG) (Z1 Z: SIG). Reset M. -Module M:SIG. +Module M : SIG. Reset M. -Module M[X:SIG]:SIG. +Module M (X: SIG) : SIG. Reset M. -Module M[X,Y:SIG]:SIG. +Module M (X Y: SIG) : SIG. Reset M. -Module M[X:SIG;Y:SIG]:SIG. +Module M (X: SIG) (Y: SIG) : SIG. Reset M. -Module M[X,Y:SIG;Z1,Z:SIG]:SIG. +Module M (X Y: SIG) (Z1 Z: SIG) : SIG. Reset M. -Module M[X:SIG][Y:SIG]:SIG. +Module M (X: SIG) (Y: SIG) : SIG. Reset M. -Module M[X,Y:SIG][Z1,Z:SIG]:SIG. +Module M (X Y: SIG) (Z1 Z: SIG) : SIG. Reset M. -Module M:=(F Q). +Module M := F Q. Reset M. -Module M[X:FSIG]:=(X Q). +Module M (X: FSIG) := X Q. Reset M. -Module M[X,Y:FSIG]:=(X Q). +Module M (X Y: FSIG) := X Q. Reset M. -Module M[X:FSIG;Y:SIG]:=(X Y). +Module M (X: FSIG) (Y: SIG) := X Y. Reset M. -Module M[X,Y:FSIG;Z1,Z:SIG]:=(X Z). +Module M (X Y: FSIG) (Z1 Z: SIG) := X Z. Reset M. -Module M[X:FSIG][Y:SIG]:=(X Y). +Module M (X: FSIG) (Y: SIG) := X Y. Reset M. -Module M[X,Y:FSIG][Z1,Z:SIG]:=(X Z). +Module M (X Y: FSIG) (Z1 Z: SIG) := X Z. Reset M. -Module M:SIG:=(F Q). +Module M : SIG := F Q. Reset M. -Module M[X:FSIG]:SIG:=(X Q). +Module M (X: FSIG) : SIG := X Q. Reset M. -Module M[X,Y:FSIG]:SIG:=(X Q). +Module M (X Y: FSIG) : SIG := X Q. Reset M. -Module M[X:FSIG;Y:SIG]:SIG:=(X Y). +Module M (X: FSIG) (Y: SIG) : SIG := X Y. Reset M. -Module M[X,Y:FSIG;Z1,Z:SIG]:SIG:=(X Z). +Module M (X Y: FSIG) (Z1 Z: SIG) : SIG := X Z. Reset M. -Module M[X:FSIG][Y:SIG]:SIG:=(X Y). +Module M (X: FSIG) (Y: SIG) : SIG := X Y. Reset M. -Module M[X,Y:FSIG][Z1,Z:SIG]:SIG:=(X Z). +Module M (X Y: FSIG) (Z1 Z: SIG) : SIG := X Z. Reset M. diff --git a/test-suite/success/Mod_strengthen.v8 b/test-suite/success/Mod_strengthen.v index 3d9885e47..449610be6 100644 --- a/test-suite/success/Mod_strengthen.v8 +++ b/test-suite/success/Mod_strengthen.v @@ -64,3 +64,4 @@ Proof. reflexivity. Qed. + diff --git a/test-suite/success/NatRing.v b/test-suite/success/NatRing.v index 6a1eeccc6..8426c7e48 100644 --- a/test-suite/success/NatRing.v +++ b/test-suite/success/NatRing.v @@ -1,10 +1,10 @@ -Require ArithRing. +Require Import ArithRing. -Lemma l1 : (S (S O))=(plus (S O) (S O)). -NatRing. +Lemma l1 : 2 = 1 + 1. +ring_nat. Qed. -Lemma l2 : (x:nat)(S (S x))=(plus (S O) (S x)). -Intro. -NatRing. -Qed.
\ No newline at end of file +Lemma l2 : forall x : nat, S (S x) = 1 + S x. +intro. +ring_nat. +Qed. diff --git a/test-suite/success/Omega.v b/test-suite/success/Omega.v index c324919ff..6df2f83d1 100644 --- a/test-suite/success/Omega.v +++ b/test-suite/success/Omega.v @@ -1,40 +1,38 @@ -Require Omega. +Require Import Omega. (* Submitted by Xavier Urbain 18 Jan 2002 *) -Lemma lem1 : (x,y:Z) - `-5 < x < 5` -> - `-5 < y` -> - `-5 < x+y+5`. +Lemma lem1 : + forall x y : Z, (-5 < x < 5)%Z -> (-5 < y)%Z -> (-5 < x + y + 5)%Z. Proof. -Intros x y. -Omega. +intros x y. + omega. Qed. (* Proposed by Pierre Crégut *) -Lemma lem2 : (x:Z) `x < 4` -> `x > 2` -> `x=3`. -Intro. -Omega. +Lemma lem2 : forall x : Z, (x < 4)%Z -> (x > 2)%Z -> x = 3%Z. +intro. + omega. Qed. (* Proposed by Jean-Christophe Filliâtre *) -Lemma lem3 : (x,y:Z) `x = y` -> `x+x = y+y`. +Lemma lem3 : forall x y : Z, x = y -> (x + x)%Z = (y + y)%Z. Proof. -Intros. -Omega. +intros. + omega. Qed. (* Proposed by Jean-Christophe Filliâtre: confusion between an Omega *) (* internal variable and a section variable (June 2001) *) Section A. -Variable x,y : Z. -Hypothesis H : `x > y`. -Lemma lem4 : `x > y`. -Omega. +Variable x y : Z. +Hypothesis H : (x > y)%Z. +Lemma lem4 : (x > y)%Z. + omega. Qed. End A. @@ -42,48 +40,48 @@ End A. (* May 2002 *) Section B. -Variables R1,R2,S1,S2,H,S:Z. -Hypothesis I:`R1 < 0`->`R2 = R1+(2*S1-1)`. -Hypothesis J:`R1 < 0`->`S2 = S1-1`. -Hypothesis K:`R1 >= 0`->`R2 = R1`. -Hypothesis L:`R1 >= 0`->`S2 = S1`. -Hypothesis M:`H <= 2*S`. -Hypothesis N:`S < H`. -Lemma lem5 : `H > 0`. -Omega. +Variable R1 R2 S1 S2 H S : Z. +Hypothesis I : (R1 < 0)%Z -> R2 = (R1 + (2 * S1 - 1))%Z. +Hypothesis J : (R1 < 0)%Z -> S2 = (S1 - 1)%Z. +Hypothesis K : (R1 >= 0)%Z -> R2 = R1. +Hypothesis L : (R1 >= 0)%Z -> S2 = S1. +Hypothesis M : (H <= 2 * S)%Z. +Hypothesis N : (S < H)%Z. +Lemma lem5 : (H > 0)%Z. + omega. Qed. End B. (* From Nicolas Oury (bug #180): handling -> on Set (fixed Oct 2002) *) -Lemma lem6: (A: Set) (i:Z) `i<= 0` -> (`i<= 0` -> A) -> `i<=0`. -Intros. -Omega. +Lemma lem6 : + forall (A : Set) (i : Z), (i <= 0)%Z -> ((i <= 0)%Z -> A) -> (i <= 0)%Z. +intros. + omega. Qed. (* Adapted from an example in Nijmegen/FTA/ftc/RefSeparating (Oct 2002) *) -Require Omega. +Require Import Omega. Section C. -Parameter g:(m:nat)~m=O->Prop. -Parameter f:(m:nat)(H:~m=O)(g m H). -Variable n:nat. -Variable ap_n:~n=O. -Local delta:=(f n ap_n). -Lemma lem7 : n=n. -Omega. +Parameter g : forall m : nat, m <> 0 -> Prop. +Parameter f : forall (m : nat) (H : m <> 0), g m H. +Variable n : nat. +Variable ap_n : n <> 0. +Let delta := f n ap_n. +Lemma lem7 : n = n. + omega. Qed. End C. (* Problem of dependencies *) -Require Omega. -Lemma lem8 : (H:O=O->O=O) H=H -> O=O. -Intros; Omega. +Require Import Omega. +Lemma lem8 : forall H : 0 = 0 -> 0 = 0, H = H -> 0 = 0. +intros; omega. Qed. (* Bug that what caused by the use of intro_using in Omega *) -Require Omega. -Lemma lem9 : (p,q:nat) - ~((le p q)/\(lt p q)\/(le q p)/\(lt p q)) - -> (lt p p)\/(le p p). -Intros; Omega. +Require Import Omega. +Lemma lem9 : + forall p q : nat, ~ (p <= q /\ p < q \/ q <= p /\ p < q) -> p < p \/ p <= p. +intros; omega. Qed. diff --git a/test-suite/success/Omega2.v8 b/test-suite/success/Omega2.v index c1f4877a6..54b13702a 100644 --- a/test-suite/success/Omega2.v8 +++ b/test-suite/success/Omega2.v @@ -25,3 +25,4 @@ forall v1 v2 v3 v4 v5 : Z, intros. omega. Qed. + diff --git a/test-suite/success/PPFix.v8 b/test-suite/success/PPFix.v index 1ecbae3ab..833eb3ad1 100644 --- a/test-suite/success/PPFix.v8 +++ b/test-suite/success/PPFix.v @@ -6,3 +6,4 @@ Check fix a(n: nat): n<5 -> nat := | 0 => fun _ => 0 | S n => fun h => S (a n (lt_S_n _ _ (lt_S _ _ h))) end. + diff --git a/test-suite/success/Print.v b/test-suite/success/Print.v index 4554a8430..c4726bf3f 100644 --- a/test-suite/success/Print.v +++ b/test-suite/success/Print.v @@ -6,15 +6,14 @@ Print Graph. Print Coercions. Print Classes. Print nat. -Print Proof O. +Print Term O. Print All. -Print Grammar constr constr. +Print Grammar constr. Inspect 10. Section A. -Coercion f := [x]True : nat -> Prop. -Print Coercion Paths nat SORTCLASS. +Coercion f (x : nat) : Prop := True. +Print Coercion Paths nat Sortclass. Print Section A. -Print. diff --git a/test-suite/success/Projection.v b/test-suite/success/Projection.v index 7f5cd8000..88da60133 100644 --- a/test-suite/success/Projection.v +++ b/test-suite/success/Projection.v @@ -1,10 +1,8 @@ -Structure S : Type := - {Dom : Type; - Op : Dom -> Dom -> Dom}. +Structure S : Type := {Dom : Type; Op : Dom -> Dom -> Dom}. -Check [s:S](Dom s). -Check [s:S](Op s). -Check [s:S;a,b:(Dom s)](Op s a b). +Check (fun s : S => Dom s). +Check (fun s : S => Op s). +Check (fun (s : S) (a b : Dom s) => Op s a b). (* v8 Check fun s:S => s.(Dom). @@ -13,17 +11,16 @@ Check fun (s:S) (a b:s.(Dom)) => s.(Op) a b. *) Set Implicit Arguments. -Unset Strict Implicits. +Unset Strict Implicit. +Unset Strict Implicit. -Structure S' [A:Set] : Type := - {Dom' : Type; - Op' : A -> Dom' -> Dom'}. +Structure S' (A : Set) : Type := {Dom' : Type; Op' : A -> Dom' -> Dom'}. -Check [s:(S' nat)](Dom' s). -Check [s:(S' nat)](Op' 2!s). -Check [s:(S' nat)](!Op' nat s). -Check [s:(S' nat);a:nat;b:(Dom' s)](Op' a b). -Check [s:(S' nat);a:nat;b:(Dom' s)](!Op' nat s a b). +Check (fun s : S' nat => Dom' s). +Check (fun s : S' nat => Op' (s:=s)). +Check (fun s : S' nat => Op' (A:=nat) (s:=s)). +Check (fun (s : S' nat) (a : nat) (b : Dom' s) => Op' a b). +Check (fun (s : S' nat) (a : nat) (b : Dom' s) => Op' (A:=nat) (s:=s) a b). (* v8 Check fun s:S' => s.(Dom'). diff --git a/test-suite/success/RecTutorial.v8 b/test-suite/success/RecTutorial.v index 1cef3f2f0..7d3d6730f 100644 --- a/test-suite/success/RecTutorial.v8 +++ b/test-suite/success/RecTutorial.v @@ -1227,3 +1227,4 @@ Qed. + diff --git a/test-suite/success/Record.v b/test-suite/success/Record.v index f3a13634d..7fdbcda7b 100644 --- a/test-suite/success/Record.v +++ b/test-suite/success/Record.v @@ -1,3 +1,3 @@ (* Nijmegen expects redefinition of sorts *) Definition CProp := Prop. -Record test : CProp := { n:nat }. +Record test : CProp := {n : nat}. diff --git a/test-suite/success/Reg.v b/test-suite/success/Reg.v index eaa0690cb..89b3032c0 100644 --- a/test-suite/success/Reg.v +++ b/test-suite/success/Reg.v @@ -1,136 +1,144 @@ -Require Reals. +Require Import Reals. -Axiom y : R->R. -Axiom d_y : (derivable y). -Axiom n_y : (x:R)``(y x)<>0``. -Axiom dy_0 : (derive_pt y R0 (d_y R0)) == R1. +Axiom y : R -> R. +Axiom d_y : derivable y. +Axiom n_y : forall x : R, y x <> 0%R. +Axiom dy_0 : derive_pt y 0 (d_y 0%R) = 1%R. -Lemma essai0 : (continuity_pt [x:R]``(x+2)/(y x)+x/(y x)`` R0). -Assert H := d_y. -Assert H0 := n_y. -Reg. +Lemma essai0 : continuity_pt (fun x : R => ((x + 2) / y x + x / y x)%R) 0. +assert (H := d_y). +assert (H0 := n_y). +reg. Qed. -Lemma essai1 : (derivable_pt [x:R]``/2*(sin x)`` ``1``). -Reg. +Lemma essai1 : derivable_pt (fun x : R => (/ 2 * sin x)%R) 1. +reg. Qed. -Lemma essai2 : (continuity [x:R]``(Rsqr x)*(cos (x*x))+x``). -Reg. +Lemma essai2 : continuity (fun x : R => (Rsqr x * cos (x * x) + x)%R). +reg. Qed. -Lemma essai3 : (derivable_pt [x:R]``x*((Rsqr x)+3)`` R0). -Reg. +Lemma essai3 : derivable_pt (fun x : R => (x * (Rsqr x + 3))%R) 0. +reg. Qed. -Lemma essai4 : (derivable [x:R]``(x+x)*(sin x)``). -Reg. +Lemma essai4 : derivable (fun x : R => ((x + x) * sin x)%R). +reg. Qed. -Lemma essai5 : (derivable [x:R]``1+(sin (2*x+3))*(cos (cos x))``). -Reg. +Lemma essai5 : derivable (fun x : R => (1 + sin (2 * x + 3) * cos (cos x))%R). +reg. Qed. -Lemma essai6 : (derivable [x:R]``(cos (x+3))``). -Reg. +Lemma essai6 : derivable (fun x : R => cos (x + 3)). +reg. Qed. -Lemma essai7 : (derivable_pt [x:R]``(cos (/(sqrt x)))*(Rsqr ((sin x)+1))`` R1). -Reg. -Apply Rlt_R0_R1. -Red; Intro; Rewrite sqrt_1 in H; Assert H0 := R1_neq_R0; Elim H0; Assumption. +Lemma essai7 : + derivable_pt (fun x : R => (cos (/ sqrt x) * Rsqr (sin x + 1))%R) 1. +reg. +apply Rlt_0_1. +red in |- *; intro; rewrite sqrt_1 in H; assert (H0 := R1_neq_R0); elim H0; + assumption. Qed. -Lemma essai8 : (derivable_pt [x:R]``(sqrt ((Rsqr x)+(sin x)+1))`` R0). -Reg. -Rewrite sin_0. -Rewrite Rsqr_O. -Replace ``0+0+1`` with ``1``; [Apply Rlt_R0_R1 | Ring]. +Lemma essai8 : derivable_pt (fun x : R => sqrt (Rsqr x + sin x + 1)) 0. +reg. + rewrite sin_0. + rewrite Rsqr_0. + replace (0 + 0 + 1)%R with 1%R; [ apply Rlt_0_1 | ring ]. Qed. -Lemma essai9 : (derivable_pt (plus_fct id sin) R1). -Reg. +Lemma essai9 : derivable_pt (id + sin) 1. +reg. Qed. -Lemma essai10 : (derivable_pt [x:R]``x+2`` R0). -Reg. +Lemma essai10 : derivable_pt (fun x : R => (x + 2)%R) 0. +reg. Qed. -Lemma essai11 : (derive_pt [x:R]``x+2`` R0 essai10)==R1. -Reg. +Lemma essai11 : derive_pt (fun x : R => (x + 2)%R) 0 essai10 = 1%R. +reg. Qed. -Lemma essai12 : (derivable [x:R]``x+(Rsqr (x+2))``). -Reg. +Lemma essai12 : derivable (fun x : R => (x + Rsqr (x + 2))%R). +reg. Qed. -Lemma essai13 : (derive_pt [x:R]``x+(Rsqr (x+2))`` R0 (essai12 R0)) == ``5``. -Reg. +Lemma essai13 : + derive_pt (fun x : R => (x + Rsqr (x + 2))%R) 0 (essai12 0%R) = 5%R. +reg. Qed. -Lemma essai14 : (derivable_pt [x:R]``2*x+x`` ``2``). -Reg. +Lemma essai14 : derivable_pt (fun x : R => (2 * x + x)%R) 2. +reg. Qed. -Lemma essai15 : (derive_pt [x:R]``2*x+x`` ``2`` essai14) == ``3``. -Reg. +Lemma essai15 : derive_pt (fun x : R => (2 * x + x)%R) 2 essai14 = 3%R. +reg. Qed. -Lemma essai16 : (derivable_pt [x:R]``x+(sin x)`` R0). -Reg. +Lemma essai16 : derivable_pt (fun x : R => (x + sin x)%R) 0. +reg. Qed. -Lemma essai17 : (derive_pt [x:R]``x+(sin x)`` R0 essai16)==``2``. -Reg. -Rewrite cos_0. -Reflexivity. +Lemma essai17 : derive_pt (fun x : R => (x + sin x)%R) 0 essai16 = 2%R. +reg. + rewrite cos_0. +reflexivity. Qed. -Lemma essai18 : (derivable_pt [x:R]``x+(y x)`` ``0``). -Assert H := d_y. -Reg. +Lemma essai18 : derivable_pt (fun x : R => (x + y x)%R) 0. +assert (H := d_y). +reg. Qed. -Lemma essai19 : (derive_pt [x:R]``x+(y x)`` ``0`` essai18) == ``2``. -Assert H := dy_0. -Assert H0 := d_y. -Reg. +Lemma essai19 : derive_pt (fun x : R => (x + y x)%R) 0 essai18 = 2%R. +assert (H := dy_0). +assert (H0 := d_y). +reg. Qed. -Axiom z:R->R. -Axiom d_z: (derivable z). +Axiom z : R -> R. +Axiom d_z : derivable z. -Lemma essai20 : (derivable_pt [x:R]``(z (y x))`` R0). -Reg. -Apply d_y. -Apply d_z. +Lemma essai20 : derivable_pt (fun x : R => z (y x)) 0. +reg. +apply d_y. +apply d_z. Qed. -Lemma essai21 : (derive_pt [x:R]``(z (y x))`` R0 essai20) == R1. -Assert H := dy_0. -Reg. +Lemma essai21 : derive_pt (fun x : R => z (y x)) 0 essai20 = 1%R. +assert (H := dy_0). +reg. Abort. -Lemma essai22 : (derivable [x:R]``(sin (z x))+(Rsqr (z x))/(y x)``). -Assert H := d_y. -Reg. -Apply n_y. -Apply d_z. +Lemma essai22 : derivable (fun x : R => (sin (z x) + Rsqr (z x) / y x)%R). +assert (H := d_y). +reg. +apply n_y. +apply d_z. Qed. (* Pour tester la continuite de sqrt en 0 *) -Lemma essai23 : (continuity_pt [x:R]``(sin (sqrt (x-1)))+(exp (Rsqr ((sqrt x)+3)))`` R1). -Reg. -Left; Apply Rlt_R0_R1. -Right; Unfold Rminus; Rewrite Rplus_Ropp_r; Reflexivity. -Qed. - -Lemma essai24 : (derivable [x:R]``(sqrt (x*x+2*x+2))+(Rabsolu (x*x+1))``). -Reg. -Replace ``x*x+2*x+2`` with ``(Rsqr (x+1))+1``. -Apply ge0_plus_gt0_is_gt0; [Apply pos_Rsqr | Apply Rlt_R0_R1]. -Unfold Rsqr; Ring. -Red; Intro; Cut ``0<x*x+1``. -Intro; Rewrite H in H0; Elim (Rlt_antirefl ? H0). -Apply ge0_plus_gt0_is_gt0; [Replace ``x*x`` with (Rsqr x); [Apply pos_Rsqr | Reflexivity] | Apply Rlt_R0_R1]. +Lemma essai23 : + continuity_pt + (fun x : R => (sin (sqrt (x - 1)) + exp (Rsqr (sqrt x + 3)))%R) 1. +reg. +left; apply Rlt_0_1. +right; unfold Rminus in |- *; rewrite Rplus_opp_r; reflexivity. +Qed. + +Lemma essai24 : + derivable (fun x : R => (sqrt (x * x + 2 * x + 2) + Rabs (x * x + 1))%R). +reg. + replace (x * x + 2 * x + 2)%R with (Rsqr (x + 1) + 1)%R. +apply Rplus_le_lt_0_compat; [ apply Rle_0_sqr | apply Rlt_0_1 ]. +unfold Rsqr in |- *; ring. +red in |- *; intro; cut (0 < x * x + 1)%R. +intro; rewrite H in H0; elim (Rlt_irrefl _ H0). +apply Rplus_le_lt_0_compat; + [ replace (x * x)%R with (Rsqr x); [ apply Rle_0_sqr | reflexivity ] + | apply Rlt_0_1 ]. Qed. diff --git a/test-suite/success/Rename.v b/test-suite/success/Rename.v index edb20a81a..8a5db157c 100644 --- a/test-suite/success/Rename.v +++ b/test-suite/success/Rename.v @@ -1,5 +1,5 @@ -Goal (n:nat)(n=O)->(n=O). -Intros. -Rename n into p. -NewInduction p; Auto. +Goal forall n : nat, n = 0 -> n = 0. +intros. +rename n into p. +induction p; auto. Qed. diff --git a/test-suite/success/Require.v b/test-suite/success/Require.v index 654808fc1..f851d8c7d 100644 --- a/test-suite/success/Require.v +++ b/test-suite/success/Require.v @@ -1,3 +1,3 @@ -Require Coq.Arith.Plus. -Read Module Coq.Arith.Minus. +Require Import Coq.Arith.Plus. +Require Coq.Arith.Minus. Locate Library Coq.Arith.Minus. diff --git a/test-suite/success/Reset.v b/test-suite/success/Reset.v index 27100ed37..b71ea69d7 100644 --- a/test-suite/success/Reset.v +++ b/test-suite/success/Reset.v @@ -1,7 +1,7 @@ (* Check Reset Section *) Section A. -Definition B:=Prop. +Definition B := Prop. End A. Reset A. diff --git a/test-suite/success/Simplify_eq.v b/test-suite/success/Simplify_eq.v index 41aa77efe..5b856e3da 100644 --- a/test-suite/success/Simplify_eq.v +++ b/test-suite/success/Simplify_eq.v @@ -2,12 +2,12 @@ (* Check that Simplify_eq tries Intro until *) -Lemma l1 : O=(S O)->False. -Simplify_eq 1. +Lemma l1 : 0 = 1 -> False. + simplify_eq 1. Qed. -Lemma l2 : (x:nat)(H:(S x)=(S (S x)))H==H->False. -Simplify_eq H. -Intros. -Apply (n_Sn x H0). +Lemma l2 : forall (x : nat) (H : S x = S (S x)), H = H -> False. + simplify_eq H. +intros. +apply (n_Sn x H0). Qed. diff --git a/test-suite/success/Tauto.v b/test-suite/success/Tauto.v index b6d999357..42898b8d1 100644 --- a/test-suite/success/Tauto.v +++ b/test-suite/success/Tauto.v @@ -18,183 +18,186 @@ Simplifications of goals, based on LJT* calcul ****) (**** Examples of intuitionistic tautologies ****) -Parameter A,B,C,D,E,F:Prop. -Parameter even:nat -> Prop. -Parameter P:nat -> Prop. +Parameter A B C D E F : Prop. +Parameter even : nat -> Prop. +Parameter P : nat -> Prop. -Lemma Ex_Wallen:(A->(B/\C)) -> ((A->B)\/(A->C)). +Lemma Ex_Wallen : (A -> B /\ C) -> (A -> B) \/ (A -> C). Proof. - Tauto. -Save. + tauto. +Qed. -Lemma Ex_Klenne:~(~(A \/ ~A)). +Lemma Ex_Klenne : ~ ~ (A \/ ~ A). Proof. - Tauto. -Save. + tauto. +Qed. -Lemma Ex_Klenne':(n:nat)(~(~((even n) \/ ~(even n)))). +Lemma Ex_Klenne' : forall n : nat, ~ ~ (even n \/ ~ even n). Proof. - Tauto. -Save. + tauto. +Qed. -Lemma Ex_Klenne'':~(~(((n:nat)(even n)) \/ ~((m:nat)(even m)))). +Lemma Ex_Klenne'' : + ~ ~ ((forall n : nat, even n) \/ ~ (forall m : nat, even m)). Proof. - Tauto. -Save. + tauto. +Qed. -Lemma tauto:((x:nat)(P x)) -> ((y:nat)(P y)). +Lemma tauto : (forall x : nat, P x) -> forall y : nat, P y. Proof. - Tauto. -Save. + tauto. +Qed. -Lemma tauto1:(A -> A). +Lemma tauto1 : A -> A. Proof. - Tauto. -Save. + tauto. +Qed. -Lemma tauto2:(A -> B -> C) -> (A -> B) -> A -> C. +Lemma tauto2 : (A -> B -> C) -> (A -> B) -> A -> C. Proof. - Tauto. -Save. + tauto. +Qed. -Lemma a:(x0: (A \/ B))(x1:(B /\ C))(A -> B). +Lemma a : forall (x0 : A \/ B) (x1 : B /\ C), A -> B. Proof. - Tauto. -Save. + tauto. +Qed. -Lemma a2:((A -> (B /\ C)) -> ((A -> B) \/ (A -> C))). +Lemma a2 : (A -> B /\ C) -> (A -> B) \/ (A -> C). Proof. - Tauto. -Save. + tauto. +Qed. -Lemma a4:(~A -> ~A). +Lemma a4 : ~ A -> ~ A. Proof. - Tauto. -Save. + tauto. +Qed. -Lemma e2:~(~(A \/ ~A)). +Lemma e2 : ~ ~ (A \/ ~ A). Proof. - Tauto. -Save. + tauto. +Qed. -Lemma e4:~(~((A \/ B) -> (A \/ B))). +Lemma e4 : ~ ~ (A \/ B -> A \/ B). Proof. - Tauto. -Save. + tauto. +Qed. -Lemma y0:(x0:A)(x1: ~A)(x2:(A -> B))(x3:(A \/ B))(x4:(A /\ B))(A -> False). +Lemma y0 : + forall (x0 : A) (x1 : ~ A) (x2 : A -> B) (x3 : A \/ B) (x4 : A /\ B), + A -> False. Proof. - Tauto. -Save. + tauto. +Qed. -Lemma y1:(x0:((A /\ B) /\ C))B. +Lemma y1 : forall x0 : (A /\ B) /\ C, B. Proof. - Tauto. -Save. + tauto. +Qed. -Lemma y2:(x0:A)(x1:B)(C \/ B). +Lemma y2 : forall (x0 : A) (x1 : B), C \/ B. Proof. - Tauto. -Save. + tauto. +Qed. -Lemma y3:(x0:(A /\ B))(B /\ A). +Lemma y3 : forall x0 : A /\ B, B /\ A. Proof. - Tauto. -Save. + tauto. +Qed. -Lemma y5:(x0:(A \/ B))(B \/ A). +Lemma y5 : forall x0 : A \/ B, B \/ A. Proof. - Tauto. -Save. + tauto. +Qed. -Lemma y6:(x0:(A -> B))(x1:A) B. +Lemma y6 : forall (x0 : A -> B) (x1 : A), B. Proof. - Tauto. -Save. + tauto. +Qed. -Lemma y7:(x0 : ((A /\ B) -> C))(x1 : B)(x2 : A) C. +Lemma y7 : forall (x0 : A /\ B -> C) (x1 : B) (x2 : A), C. Proof. - Tauto. -Save. + tauto. +Qed. -Lemma y8:(x0 : ((A \/ B) -> C))(x1 : A) C. +Lemma y8 : forall (x0 : A \/ B -> C) (x1 : A), C. Proof. - Tauto. -Save. + tauto. +Qed. -Lemma y9:(x0 : ((A \/ B) -> C))(x1 : B) C. +Lemma y9 : forall (x0 : A \/ B -> C) (x1 : B), C. Proof. - Tauto. -Save. + tauto. +Qed. -Lemma y10:(x0 : ((A -> B) -> C))(x1 : B) C. +Lemma y10 : forall (x0 : (A -> B) -> C) (x1 : B), C. Proof. - Tauto. -Save. + tauto. +Qed. (* This example took much time with the old version of Tauto *) -Lemma critical_example0:(~~B->B)->(A->B)->~~A->B. +Lemma critical_example0 : (~ ~ B -> B) -> (A -> B) -> ~ ~ A -> B. Proof. - Tauto. -Save. + tauto. +Qed. (* Same remark as previously *) -Lemma critical_example1:(~~B->B)->(~B->~A)->~~A->B. +Lemma critical_example1 : (~ ~ B -> B) -> (~ B -> ~ A) -> ~ ~ A -> B. Proof. - Tauto. -Save. + tauto. +Qed. (* This example took very much time (about 3mn on a PIII 450MHz in bytecode) with the old Tauto. Now, it's immediate (less than 1s). *) -Lemma critical_example2:(~A<->B)->(~B<->A)->(~~A<->A). +Lemma critical_example2 : (~ A <-> B) -> (~ B <-> A) -> (~ ~ A <-> A). Proof. - Tauto. -Save. + tauto. +Qed. (* This example was a bug *) -Lemma old_bug0:(~A<->B)->(~(C\/E)<->D/\F)->~(C\/A\/E)<->D/\B/\F. +Lemma old_bug0 : + (~ A <-> B) -> (~ (C \/ E) <-> D /\ F) -> (~ (C \/ A \/ E) <-> D /\ B /\ F). Proof. - Tauto. -Save. + tauto. +Qed. (* Another bug *) -Lemma old_bug1:((A->B->False)->False) -> (B->False) -> False. +Lemma old_bug1 : ((A -> B -> False) -> False) -> (B -> False) -> False. Proof. - Tauto. -Save. + tauto. +Qed. (* A bug again *) -Lemma old_bug2: - ((((C->False)->A)->((B->False)->A)->False)->False) -> - (((C->B->False)->False)->False) -> - ~A->A. +Lemma old_bug2 : + ((((C -> False) -> A) -> ((B -> False) -> A) -> False) -> False) -> + (((C -> B -> False) -> False) -> False) -> ~ A -> A. Proof. - Tauto. -Save. + tauto. +Qed. (* A bug from CNF form *) -Lemma old_bug3: - ((~A\/B)/\(~B\/B)/\(~A\/~B)/\(~B\/~B)->False)->~((A->B)->B)->False. +Lemma old_bug3 : + ((~ A \/ B) /\ (~ B \/ B) /\ (~ A \/ ~ B) /\ (~ B \/ ~ B) -> False) -> + ~ ((A -> B) -> B) -> False. Proof. - Tauto. -Save. + tauto. +Qed. (* sometimes, the behaviour of Tauto depends on the order of the hyps *) -Lemma old_bug3bis: - ~((A->B)->B)->((~B\/~B)/\(~B\/~A)/\(B\/~B)/\(B\/~A)->False)->False. +Lemma old_bug3bis : + ~ ((A -> B) -> B) -> + ((~ B \/ ~ B) /\ (~ B \/ ~ A) /\ (B \/ ~ B) /\ (B \/ ~ A) -> False) -> False. Proof. - Tauto. -Save. + tauto. +Qed. (* A bug found by Freek Wiedijk <freek@cs.kun.nl> *) -Lemma new_bug: - ((A<->B)->(B<->C)) -> - ((B<->C)->(C<->A)) -> - ((C<->A)->(A<->B)) -> - (A<->B). +Lemma new_bug : + ((A <-> B) -> (B <-> C)) -> + ((B <-> C) -> (C <-> A)) -> ((C <-> A) -> (A <-> B)) -> (A <-> B). Proof. - Tauto. -Save. + tauto. +Qed. (* A private club has the following rules : @@ -211,30 +214,31 @@ Save. Section club. -Variable Scottish, RedSocks, WearKilt, Married, GoOutSunday : Prop. +Variable Scottish RedSocks WearKilt Married GoOutSunday : Prop. -Hypothesis rule1 : ~Scottish -> RedSocks. -Hypothesis rule2 : WearKilt \/ ~RedSocks. -Hypothesis rule3 : Married -> ~GoOutSunday. +Hypothesis rule1 : ~ Scottish -> RedSocks. +Hypothesis rule2 : WearKilt \/ ~ RedSocks. +Hypothesis rule3 : Married -> ~ GoOutSunday. Hypothesis rule4 : GoOutSunday <-> Scottish. -Hypothesis rule5 : WearKilt -> (Scottish /\ Married). +Hypothesis rule5 : WearKilt -> Scottish /\ Married. Hypothesis rule6 : Scottish -> WearKilt. Lemma NoMember : False. -Tauto. -Save. + tauto. +Qed. End club. (**** Use of Intuition ****) -Lemma intu0:(((x:nat)(P x)) /\ B) -> - (((y:nat)(P y)) /\ (P O)) \/ (B /\ (P O)). +Lemma intu0 : + (forall x : nat, P x) /\ B -> (forall y : nat, P y) /\ P 0 \/ B /\ P 0. Proof. - Intuition. -Save. + intuition. +Qed. -Lemma intu1:((A:Prop)A\/~A)->(x,y:nat)(x=y\/~x=y). +Lemma intu1 : + (forall A : Prop, A \/ ~ A) -> forall x y : nat, x = y \/ x <> y. Proof. - Intuition. -Save. + intuition. +Qed. diff --git a/test-suite/success/TestRefine.v b/test-suite/success/TestRefine.v index ee3d7e3f8..8ed0f7ba6 100644 --- a/test-suite/success/TestRefine.v +++ b/test-suite/success/TestRefine.v @@ -6,27 +6,32 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* Petit bench vite fait, mal fait *) - -Require Refine. - - (************************************************************************) -Lemma essai : (x:nat)x=x. +Lemma essai : forall x : nat, x = x. -Refine (([x0:nat]Cases x0 of - O => ? - | (S p) => ? - end) :: (x:nat)x=x). (* x0=x0 et x0=x0 *) + refine + ((fun x0 : nat => match x0 with + | O => _ + | S p => _ + end) + :forall x : nat, x = x). (* x0=x0 et x0=x0 *) Restart. -Refine [x0:nat]<[n:nat]n=n>Case x0 of ? [p:nat]? end. (* OK *) + refine + (fun x0 : nat => match x0 as n return (n = n) with + | O => _ + | S p => _ + end). (* OK *) Restart. -Refine [x0:nat]<[n:nat]n=n>Cases x0 of O => ? | (S p) => ? end. (* OK *) + refine + (fun x0 : nat => match x0 as n return (n = n) with + | O => _ + | S p => _ + end). (* OK *) Restart. @@ -41,40 +46,52 @@ Abort. Lemma T : nat. -Refine (S ?). + refine (S _). Abort. (************************************************************************) -Lemma essai2 : (x:nat)x=x. +Lemma essai2 : forall x : nat, x = x. -Refine Fix f{f/1 : (x:nat)x=x := [x:nat]? }. + refine (fix f (x : nat) : x = x := _). Restart. -Refine Fix f{f/1 : (x:nat)x=x := - [x:nat]<[n:nat](eq nat n n)>Case x of ? [p:nat]? end}. + refine + (fix f (x : nat) : x = x := + match x as n return (n = n :>nat) with + | O => _ + | S p => _ + end). Restart. -Refine Fix f{f/1 : (x:nat)x=x := - [x:nat]<[n:nat]n=n>Cases x of O => ? | (S p) => ? end}. + refine + (fix f (x : nat) : x = x := + match x as n return (n = n) with + | O => _ + | S p => _ + end). Restart. -Refine Fix f{f/1 : (x:nat)x=x := - [x:nat]<[n:nat](eq nat n n)>Case x of - ? - [p:nat](f_equal nat nat S p p ?) end}. + refine + (fix f (x : nat) : x = x := + match x as n return (n = n :>nat) with + | O => _ + | S p => f_equal S _ + end). Restart. -Refine Fix f{f/1 : (x:nat)x=x := - [x:nat]<[n:nat](eq nat n n)>Cases x of - O => ? - | (S p) =>(f_equal nat nat S p p ?) end}. + refine + (fix f (x : nat) : x = x := + match x as n return (n = n :>nat) with + | O => _ + | S p => f_equal S _ + end). Abort. @@ -83,13 +100,13 @@ Abort. Lemma essai : nat. -Parameter f : nat*nat -> nat -> nat. +Parameter f : nat * nat -> nat -> nat. -Refine (f ? ([x:nat](? :: nat) O)). + refine (f _ ((fun x : nat => _:nat) 0)). Restart. -Refine (f ? O). + refine (f _ 0). Abort. @@ -98,93 +115,113 @@ Abort. Parameter P : nat -> Prop. -Lemma essai : { x:nat | x=(S O) }. +Lemma essai : {x : nat | x = 1}. -Refine (exist nat ? (S O) ?). (* ECHEC *) + refine (exist _ 1 _). (* ECHEC *) Restart. (* mais si on contraint par le but alors ca marche : *) (* Remarque : on peut toujours faire ça *) -Refine ((exist nat ? (S O) ?) :: { x:nat | x=(S O) }). + refine (exist _ 1 _:{x : nat | x = 1}). Restart. -Refine (exist nat [x:nat](x=(S O)) (S O) ?). + refine (exist (fun x : nat => x = 1) 1 _). Abort. (************************************************************************) -Lemma essai : (n:nat){ x:nat | x=(S n) }. +Lemma essai : forall n : nat, {x : nat | x = S n}. -Refine [n:nat]<[n:nat]{x:nat|x=(S n)}>Case n of ? [p:nat]? end. + refine + (fun n : nat => + match n return {x : nat | x = S n} with + | O => _ + | S p => _ + end). Restart. -Refine (([n:nat]Case n of ? [p:nat]? end) :: (n:nat){ x:nat | x=(S n) }). + refine + ((fun n : nat => match n with + | O => _ + | S p => _ + end) + :forall n : nat, {x : nat | x = S n}). Restart. -Refine [n:nat]<[n:nat]{x:nat|x=(S n)}>Cases n of O => ? | (S p) => ? end. + refine + (fun n : nat => + match n return {x : nat | x = S n} with + | O => _ + | S p => _ + end). Restart. -Refine Fix f{f/1 :(n:nat){x:nat|x=(S n)} := - [n:nat]<[n:nat]{x:nat|x=(S n)}>Case n of ? [p:nat]? end}. + refine + (fix f (n : nat) : {x : nat | x = S n} := + match n return {x : nat | x = S n} with + | O => _ + | S p => _ + end). Restart. -Refine Fix f{f/1 :(n:nat){x:nat|x=(S n)} := - [n:nat]<[n:nat]{x:nat|x=(S n)}>Cases n of O => ? | (S p) => ? end}. + refine + (fix f (n : nat) : {x : nat | x = S n} := + match n return {x : nat | x = S n} with + | O => _ + | S p => _ + end). -Exists (S O). Trivial. -Elim (f0 p). -Refine [x:nat][h:x=(S p)](exist nat [x:nat]x=(S (S p)) (S x) ?). -Rewrite h. Auto. -Save. +exists 1. trivial. +elim (f0 p). + refine + (fun (x : nat) (h : x = S p) => exist (fun x : nat => x = S (S p)) (S x) _). + rewrite h. auto. +Qed. (* Quelques essais de recurrence bien fondée *) -Require Wf. -Require Wf_nat. +Require Import Wf. +Require Import Wf_nat. -Lemma essai_wf : nat->nat. +Lemma essai_wf : nat -> nat. -Refine [x:nat](well_founded_induction - nat - lt ? - [_:nat]nat->nat - [phi0:nat][w:(phi:nat)(lt phi phi0)->nat->nat](w x ?) - x x). -Exact lt_wf. + refine + (fun x : nat => + well_founded_induction _ (fun _ : nat => nat -> nat) + (fun (phi0 : nat) (w : forall phi : nat, phi < phi0 -> nat -> nat) => + w x _) x x). +exact lt_wf. Abort. -Require Compare_dec. -Require Lt. +Require Import Compare_dec. +Require Import Lt. Lemma fibo : nat -> nat. -Refine (well_founded_induction - nat - lt ? - [_:nat]nat - [x0:nat][fib:(x:nat)(lt x x0)->nat] - Cases (zerop x0) of - (left _) => (S O) - | (right h1) => Cases (zerop (pred x0)) of - (left _) => (S O) - | (right h2) => (plus (fib (pred x0) ?) - (fib (pred (pred x0)) ?)) - end - end). -Exact lt_wf. -Auto with arith. -Apply lt_trans with m:=(pred x0); Auto with arith. -Save. - + refine + (well_founded_induction _ (fun _ : nat => nat) + (fun (x0 : nat) (fib : forall x : nat, x < x0 -> nat) => + match zerop x0 with + | left _ => 1 + | right h1 => + match zerop (pred x0) with + | left _ => 1 + | right h2 => fib (pred x0) _ + fib (pred (pred x0)) _ + end + end)). +exact lt_wf. +auto with arith. +apply lt_trans with (m := pred x0); auto with arith. +Qed. diff --git a/test-suite/success/Try.v b/test-suite/success/Try.v index 05cab1e6f..b356f277c 100644 --- a/test-suite/success/Try.v +++ b/test-suite/success/Try.v @@ -2,7 +2,7 @@ non-existent names in Unfold [cf bug #263] *) Lemma lem1 : True. -Try (Unfold i_dont_exist). -Trivial. +try unfold i_dont_exist in |- *. +trivial. Qed. diff --git a/test-suite/success/autorewritein.v8 b/test-suite/success/autorewritein.v index 3e218099a..8126e9e4b 100644 --- a/test-suite/success/autorewritein.v8 +++ b/test-suite/success/autorewritein.v @@ -17,3 +17,4 @@ Proof. intros. autorewrite with base0 in H using try (apply H1; reflexivity). Qed. + diff --git a/test-suite/success/cc.v b/test-suite/success/cc.v index 940aa7507..42df990fd 100644 --- a/test-suite/success/cc.v +++ b/test-suite/success/cc.v @@ -1,73 +1,79 @@ -Theorem t1: (A:Set)(a:A)(f:A->A) - (f a)=a->(f (f a))=a. -Intros. -Congruence. -Save. - -Theorem t2: (A:Set)(a,b:A)(f:A->A)(g:A->A->A) - a=(f a)->(g b (f a))=(f (f a))->(g a b)=(f (g b a))-> - (g a b)=a. -Intros. -Congruence. -Save. +Theorem t1 : forall (A : Set) (a : A) (f : A -> A), f a = a -> f (f a) = a. +intros. + congruence. +Qed. + +Theorem t2 : + forall (A : Set) (a b : A) (f : A -> A) (g : A -> A -> A), + a = f a -> g b (f a) = f (f a) -> g a b = f (g b a) -> g a b = a. +intros. + congruence. +Qed. (* 15=0 /\ 10=0 /\ 6=0 -> 0=1 *) -Theorem t3: (N:Set)(o:N)(s:N->N)(d:N->N) - (s(s(s(s(s(s(s(s(s(s(s(s(s(s(s o)))))))))))))))=o-> - (s (s (s (s (s (s (s (s (s (s o))))))))))=o-> - (s (s (s (s (s (s o))))))=o-> - o=(s o). -Intros. -Congruence. -Save. +Theorem t3 : + forall (N : Set) (o : N) (s d : N -> N), + s (s (s (s (s (s (s (s (s (s (s (s (s (s (s o)))))))))))))) = o -> + s (s (s (s (s (s (s (s (s (s o))))))))) = o -> + s (s (s (s (s (s o))))) = o -> o = s o. +intros. + congruence. +Qed. (* Examples that fail due to dependencies *) (* yields transitivity problem *) -Theorem dep:(A:Set)(P:A->Set)(f,g:(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. -Save. +Theorem dep : + 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. (* yields congruence problem *) -Theorem dep2:(A,B:Set)(f:(A:Set)(b:bool)if b then unit else A->unit)(e:A==B) - (f A true)=(f B true). -Intros;Rewrite e;Reflexivity. -Save. +Theorem dep2 : + forall (A B : Set) + (f : forall (A : Set) (b : bool), if b then unit else A -> unit) + (e : A = B), f A true = f B true. +intros; rewrite e; reflexivity. +Qed. (* example that Congruence. can solve (dependent function applied to the same argument)*) -Theorem dep3:(A:Set)(P:(A->Set))(f,g:(x:A)(P x))f=g->(x:A)(f x)=(g x). Intros. -Congruence. -Save. +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. + congruence. +Qed. (* Examples with injection rule *) -Theorem inj1 : (A:Set;a,b,c,d:A)(a,c)=(b,d)->a=b/\c=d. -Intros. -Split;Congruence. -Save. +Theorem inj1 : + forall (A : Set) (a b c d : A), (a, c) = (b, d) -> a = b /\ c = d. +intros. +split; congruence. +Qed. -Theorem inj2 : (A:Set;a,c,d:A;f:A->A*A) (f=(pair A A a))-> - (Some ? (f c))=(Some ? (f d))->c=d. -Intros. -Congruence. -Save. +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. +intros. + congruence. +Qed. (* Examples with discrimination rule *) -Theorem discr1 : true=false->False. -Intros. -Congruence. -Save. +Theorem discr1 : true = false -> False. +intros. + congruence. +Qed. -Theorem discr2 : (Some ? true)=(Some ? false)->False. -Intros. -Congruence. -Save. +Theorem discr2 : Some true = Some false -> False. +intros. + congruence. +Qed. diff --git a/test-suite/success/coercions.v b/test-suite/success/coercions.v index 17c4f9078..8dd48752b 100644 --- a/test-suite/success/coercions.v +++ b/test-suite/success/coercions.v @@ -1,26 +1,26 @@ (* Interaction between coercions and casts *) (* Example provided by Eduardo Gimenez *) -Parameter Z,S:Set. +Parameter Z S : Set. -Parameter f: S -> Z. -Coercion f: S >-> Z. +Parameter f : S -> Z. +Coercion f : S >-> Z. Parameter g : Z -> Z. -Check [s](g (s::S)). +Check (fun s => g (s:S)). (* Check uniform inheritance condition *) Parameter h : nat -> nat -> Prop. -Parameter i : (n,m:nat)(h n m) -> nat. +Parameter i : forall n m : nat, h n m -> nat. Coercion i : h >-> nat. (* Check coercion to funclass when the source occurs in the target *) -Parameter C: nat -> nat -> nat. -Coercion C : nat >-> FUNCLASS. +Parameter C : nat -> nat -> nat. +Coercion C : nat >-> Funclass. (* Remark: in the following example, it cannot be decide whether C is from nat to Funclass or from A to nat. An explicit Coercion command is diff --git a/test-suite/success/coqbugs0181.v b/test-suite/success/coqbugs0181.v index 21f906a60..d541dcf7b 100644 --- a/test-suite/success/coqbugs0181.v +++ b/test-suite/success/coqbugs0181.v @@ -1,7 +1,7 @@ (* test the strength of pretyping unification *) -Require PolyList. -Definition listn := [A,n] {l:(list A)|(length l)=n}. -Definition make_ln [A,n;l:(list A); h:([l](length l)=n l)] := - (exist ?? l h). +Require Import List. +Definition listn A n := {l : list A | length l = n}. +Definition make_ln A n (l : list A) (h : (fun l => length l = n) l) := + exist _ l h. diff --git a/test-suite/success/destruct.v b/test-suite/success/destruct.v index f09863d9d..ede573a34 100644 --- a/test-suite/success/destruct.v +++ b/test-suite/success/destruct.v @@ -1,9 +1,9 @@ (* Simplification of bug 711 *) -Parameter f:true=false. -Goal let p=f in True. -Intro p. -LetTac b:=true. +Parameter f : true = false. +Goal let p := f in True. +intro p. +set (b := true) in *. (* Check that it doesn't fail with an anomaly *) (* Ultimately, adapt destruct to make it succeeding *) -Try NewDestruct b. +try destruct b. diff --git a/test-suite/success/eauto.v b/test-suite/success/eauto.v index 97f7ccf0e..26339d513 100644 --- a/test-suite/success/eauto.v +++ b/test-suite/success/eauto.v @@ -5,45 +5,56 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -Require PolyList. +Require Import List. -Parameter in_list : (list nat*nat)->nat->Prop. -Definition not_in_list : (list nat*nat)->nat->Prop - := [l,n]~(in_list l n). +Parameter in_list : list (nat * nat) -> nat -> Prop. +Definition not_in_list (l : list (nat * nat)) (n : nat) : Prop := + ~ in_list l n. (* Hints Unfold not_in_list. *) -Axiom lem1 : (l1,l2:(list nat*nat))(n:nat) - (not_in_list (app l1 l2) n)->(not_in_list l1 n). - -Axiom lem2 : (l1,l2:(list nat*nat))(n:nat) - (not_in_list (app l1 l2) n)->(not_in_list l2 n). - -Axiom lem3 : (l:(list nat*nat))(n,p,q:nat) - (not_in_list (cons (p,q) l) n)->(not_in_list l n). - -Axiom lem4 : (l1,l2:(list nat*nat))(n:nat) - (not_in_list l1 n)->(not_in_list l2 n)->(not_in_list (app l1 l2) n). - -Hints Resolve lem1 lem2 lem3 lem4: essai. - -Goal (l:(list nat*nat))(n,p,q:nat) - (not_in_list (cons (p,q) l) n)->(not_in_list l n). -Intros. -EAuto with essai. -Save. +Axiom + lem1 : + forall (l1 l2 : list (nat * nat)) (n : nat), + not_in_list (l1 ++ l2) n -> not_in_list l1 n. + +Axiom + lem2 : + forall (l1 l2 : list (nat * nat)) (n : nat), + not_in_list (l1 ++ l2) n -> not_in_list l2 n. + +Axiom + lem3 : + forall (l : list (nat * nat)) (n p q : nat), + not_in_list ((p, q) :: l) n -> not_in_list l n. + +Axiom + lem4 : + forall (l1 l2 : list (nat * nat)) (n : nat), + not_in_list l1 n -> not_in_list l2 n -> not_in_list (l1 ++ l2) n. + +Hint Resolve lem1 lem2 lem3 lem4: essai. + +Goal +forall (l : list (nat * nat)) (n p q : nat), +not_in_list ((p, q) :: l) n -> not_in_list l n. +intros. + eauto with essai. +Qed. (* Example from Nicolas Magaud on coq-club - Jul 2000 *) -Definition Nat: Set := nat. -Parameter S':Nat ->Nat. -Parameter plus':Nat -> Nat ->Nat. - -Lemma simpl_plus_l_rr1: - ((n0:Nat) ((m, p:Nat) (plus' n0 m)=(plus' n0 p) ->m=p) -> - (m, p:Nat) (S' (plus' n0 m))=(S' (plus' n0 p)) ->m=p) -> - (n:Nat) ((m, p:Nat) (plus' n m)=(plus' n p) ->m=p) -> - (m, p:Nat) (S' (plus' n m))=(S' (plus' n p)) ->m=p. -Intros. -EAuto. (* does EApply H *) +Definition Nat : Set := nat. +Parameter S' : Nat -> Nat. +Parameter plus' : Nat -> Nat -> Nat. + +Lemma simpl_plus_l_rr1 : + (forall n0 : Nat, + (forall m p : Nat, plus' n0 m = plus' n0 p -> m = p) -> + forall m p : Nat, S' (plus' n0 m) = S' (plus' n0 p) -> m = p) -> + forall n : Nat, + (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 *) Qed. diff --git a/test-suite/success/eqdecide.v b/test-suite/success/eqdecide.v index f826df9a4..e7b8ca237 100644 --- a/test-suite/success/eqdecide.v +++ b/test-suite/success/eqdecide.v @@ -6,24 +6,26 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -Inductive T : Set := A: T | B :T->T. +Inductive T : Set := + | A : T + | B : T -> T. -Lemma lem1 : (x,y:T){x=y}+{~x=y}. -Decide Equality. +Lemma lem1 : forall x y : T, {x = y} + {x <> y}. + decide equality. Qed. -Lemma lem2 : (x,y:T){x=y}+{~x=y}. -Intros x y. -Decide Equality x y. +Lemma lem2 : forall x y : T, {x = y} + {x <> y}. +intros x y. + decide equality x y. Qed. -Lemma lem3 : (x,y:T){x=y}+{~x=y}. -Intros x y. -Decide Equality y x. +Lemma lem3 : forall x y : T, {x = y} + {x <> y}. +intros x y. + decide equality y x. Qed. -Lemma lem4 : (x,y:T){x=y}+{~x=y}. -Intros x y. -Compare x y; Auto. +Lemma lem4 : forall x y : T, {x = y} + {x <> y}. +intros x y. + compare x y; auto. Qed. diff --git a/test-suite/success/evars.v b/test-suite/success/evars.v index 0a12789b9..dbace977e 100644 --- a/test-suite/success/evars.v +++ b/test-suite/success/evars.v @@ -1,38 +1,45 @@ (* The "?" of cons and eq should be inferred *) -Variable list:Set -> Set. -Variable cons:(T:Set) T -> (list T) -> (list T). -Check (n:(list nat)) (EX l| (EX x| (n = (cons ? x l)))). +Variable list : Set -> Set. +Variable cons : forall T : Set, T -> list T -> list T. +Check (forall n : list nat, exists l : _, (exists x : _, n = cons _ x l)). (* Examples provided by Eduardo Gimenez *) -Definition c [A;Q:(nat*A->Prop)->Prop;P] := - (Q [p:nat*A]let (i,v) = p in (P i v)). +Definition c A (Q : (nat * A -> Prop) -> Prop) P := + Q (fun p : nat * A => let (i, v) := p in P i v). (* What does this test ? *) -Require PolyList. -Definition list_forall_bool [A:Set][p:A->bool][l:(list A)] : bool := - (fold_right ([a][r]if (p a) then r else false) true l). +Require Import List. +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. (* Checks that solvable ? in the lambda prefix of the definition are harmless*) -Parameter A1,A2,F,B,C : Set. +Parameter A1 A2 F B C : Set. Parameter f : F -> A1 -> B. -Definition f1 [frm0,a1]: B := (f frm0 a1). +Definition f1 frm0 a1 : B := f frm0 a1. (* Checks that solvable ? in the type part of the definition are harmless *) -Definition f2 : (frm0:?;a1:?)B := [frm0,a1](f frm0 a1). +Definition f2 frm0 a1 : B := f frm0 a1. (* Checks that sorts that are evars are handled correctly (bug 705) *) -Require PolyList. - -Fixpoint build [nl : (list nat)] : - (Cases nl of nil => True | _ => False end) -> unit := - <[nl](Cases nl of nil => True | _ => False end) -> unit>Cases nl of - | nil => [_]tt - | (cons n rest) => - Cases n of - | O => [_]tt - | (S m) => [a](build rest (False_ind ? a)) - end +Require Import List. + +Fixpoint build (nl : list nat) : + match nl with + | nil => True + | _ => False + end -> unit := + match nl return (match nl with + | nil => True + | _ => False + end -> unit) with + | nil => fun _ => tt + | n :: rest => + match n with + | O => fun _ => tt + | S m => fun a => build rest (False_ind _ a) + end end. @@ -40,8 +47,12 @@ Fixpoint build [nl : (list nat)] : (* Bug de 1999 corrigé en déc 2004 *) Check - let p = [m:nat;f;n:nat]Cases (f m n) of - (exist a b) => (exist ? ? a b) - end - in - (p:: (x:nat)((y:nat)(n:nat){q:nat | y = (mult q n)}) -> (n:nat){q:nat | x = (mult q n)}). + (let p := + fun (m : nat) f (n : nat) => + match f m n with + | exist a b => exist _ a b + end in + p + :forall x : nat, + (forall y n : nat, {q : nat | y = q * n}) -> + forall n : nat, {q : nat | x = q * n}). diff --git a/test-suite/success/fix.v b/test-suite/success/fix.v index 374029bba..f4a4d36d9 100644 --- a/test-suite/success/fix.v +++ b/test-suite/success/fix.v @@ -12,40 +12,41 @@ Require Import ZArith. Definition rNat := positive. -Inductive rBoolOp: Set := - rAnd: rBoolOp - | rEq: rBoolOp . - -Definition rlt: rNat -> rNat ->Prop := [a, b:rNat](compare a b EGAL)=INFERIEUR. - -Definition rltDec: (m, n:rNat){(rlt m n)}+{(rlt n m) \/ m=n}. -Intros n m; Generalize (compare_convert_INFERIEUR n m); - Generalize (compare_convert_SUPERIEUR n m); - Generalize (compare_convert_EGAL n m); Case (compare n m EGAL). -Intros H' H'0 H'1; Right; Right; Auto. -Intros H' H'0 H'1; Left; Unfold rlt. -Apply convert_compare_INFERIEUR; Auto. -Intros H' H'0 H'1; Right; Left; Unfold rlt. -Apply convert_compare_INFERIEUR; Auto. -Apply H'0; Auto. +Inductive rBoolOp : Set := + | rAnd : rBoolOp + | rEq : rBoolOp. + +Definition rlt (a b : rNat) : Prop := + (a ?= b)%positive Datatypes.Eq = Datatypes.Lt. + +Definition rltDec : forall m n : rNat, {rlt m n} + {rlt n m \/ m = n}. +intros n m; generalize (nat_of_P_lt_Lt_compare_morphism n m); + generalize (nat_of_P_gt_Gt_compare_morphism n m); + generalize (Pcompare_Eq_eq n m); case ((n ?= m)%positive Datatypes.Eq). +intros H' H'0 H'1; right; right; auto. +intros H' H'0 H'1; left; unfold rlt in |- *. +apply nat_of_P_lt_Lt_compare_complement_morphism; auto. +intros H' H'0 H'1; right; left; unfold rlt in |- *. +apply nat_of_P_lt_Lt_compare_complement_morphism; auto. +apply H'0; auto. Defined. -Definition rmax: rNat -> rNat ->rNat. -Intros n m; Case (rltDec n m); Intros Rlt0. -Exact m. -Exact n. +Definition rmax : rNat -> rNat -> rNat. +intros n m; case (rltDec n m); intros Rlt0. +exact m. +exact n. Defined. -Inductive rExpr: Set := - rV: rNat ->rExpr - | rN: rExpr ->rExpr - | rNode: rBoolOp -> rExpr -> rExpr ->rExpr . - -Fixpoint maxVar[e:rExpr]: rNat := - Cases e of - (rV n) => n - | (rN p) => (maxVar p) - | (rNode n p q) => (rmax (maxVar p) (maxVar q)) - end. +Inductive rExpr : Set := + | rV : rNat -> rExpr + | rN : rExpr -> rExpr + | rNode : rBoolOp -> rExpr -> rExpr -> rExpr. + +Fixpoint maxVar (e : rExpr) : rNat := + match e with + | rV n => n + | rN p => maxVar p + | rNode n p q => rmax (maxVar p) (maxVar q) + end. diff --git a/test-suite/success/if.v b/test-suite/success/if.v index 85cd1f11b..3f7638631 100644 --- a/test-suite/success/if.v +++ b/test-suite/success/if.v @@ -1,5 +1,5 @@ (* The synthesis of the elimination predicate may fail if algebric *) (* universes are not cautiously treated *) -Check [b:bool]if b then Type else nat. +Check (fun b : bool => if b then Type else nat). diff --git a/test-suite/success/implicit.v b/test-suite/success/implicit.v index c597f9bf8..1786424e5 100644 --- a/test-suite/success/implicit.v +++ b/test-suite/success/implicit.v @@ -1,20 +1,23 @@ (* Implicit on section variables *) Set Implicit Arguments. +Unset Strict Implicit. (* Example submitted by David Nowak *) Section Spec. -Variable A:Set. -Variable op : (A:Set)A->A->Set. -Infix 6 "#" op V8only (at level 70). -Check (x:A)(x # x). +Variable A : Set. +Variable op : forall A : Set, A -> A -> Set. +Infix "#" := op (at level 70). +Check (forall x : A, x # x). (* Example submitted by Christine *) -Record stack : Type := {type : Set; elt : type; - empty : type -> bool; proof : (empty elt)=true }. +Record stack : Type := + {type : Set; elt : type; empty : type -> bool; proof : empty elt = true}. -Check (type:Set; elt:type; empty:(type->bool))(empty elt)=true->stack. +Check + (forall (type : Set) (elt : type) (empty : type -> bool), + empty elt = true -> stack). End Spec. @@ -22,10 +25,10 @@ End Spec. Parameter f : nat -> nat * nat. Notation lhs := fst. -Check [x](lhs ? ? (f x)). -Check [x](!lhs ? ? (f x)). -Notation "'rhs'" := snd. -Check [x](rhs ? ? (f x)). +Check (fun x => fst (f x)). +Check (fun x => fst (f x)). +Notation rhs := snd. +Check (fun x => snd (f x)). (* V8 seulement Check (fun x => @ rhs ? ? (f x)). *) diff --git a/test-suite/success/import_lib.v b/test-suite/success/import_lib.v index d031691d8..c3dc2fc62 100644 --- a/test-suite/success/import_lib.v +++ b/test-suite/success/import_lib.v @@ -1,47 +1,47 @@ -Definition le_trans:=O. +Definition le_trans := 0. Module Test_Read. Module M. - Read Module Le. (* Reading without importing *) + Require Le. (* Reading without importing *) Check Le.le_trans. - Lemma th0 : le_trans = O. - Reflexivity. + Lemma th0 : le_trans = 0. + reflexivity. Qed. End M. Check Le.le_trans. - Lemma th0 : le_trans = O. - Reflexivity. + Lemma th0 : le_trans = 0. + reflexivity. Qed. Import M. - Lemma th1 : le_trans = O. - Reflexivity. + Lemma th1 : le_trans = 0. + reflexivity. Qed. End Test_Read. (****************************************************************) -Definition le_decide := (S O). (* from Arith/Compare *) -Definition min := O. (* from Arith/Min *) +Definition le_decide := 1. (* from Arith/Compare *) +Definition min := 0. (* from Arith/Min *) Module Test_Require. Module M. - Require Compare. (* Imports Min as well *) + Require Import Compare. (* Imports Min as well *) - Lemma th1 : le_decide = Compare.le_decide. - Reflexivity. + Lemma th1 : le_decide = le_decide. + reflexivity. Qed. - Lemma th2 : min = Min.min. - Reflexivity. + Lemma th2 : min = min. + reflexivity. Qed. End M. @@ -52,23 +52,23 @@ Module Test_Require. (* Checks that Compare and List are _not_ imported *) - Lemma th1 : le_decide = (S O). - Reflexivity. + Lemma th1 : le_decide = 1. + reflexivity. Qed. - Lemma th2 : min = O. - Reflexivity. + Lemma th2 : min = 0. + reflexivity. Qed. (* It should still be the case after Import M *) Import M. - Lemma th3 : le_decide = (S O). - Reflexivity. + Lemma th3 : le_decide = 1. + reflexivity. Qed. - Lemma th4 : min = O. - Reflexivity. + Lemma th4 : min = 0. + reflexivity. Qed. End Test_Require. @@ -79,12 +79,12 @@ Module Test_Import. Module M. Import Compare. (* Imports Min as well *) - Lemma th1 : le_decide = Compare.le_decide. - Reflexivity. + Lemma th1 : le_decide = le_decide. + reflexivity. Qed. - Lemma th2 : min = Min.min. - Reflexivity. + Lemma th2 : min = min. + reflexivity. Qed. End M. @@ -95,23 +95,23 @@ Module Test_Import. (* Checks that Compare and List are _not_ imported *) - Lemma th1 : le_decide = (S O). - Reflexivity. + Lemma th1 : le_decide = 1. + reflexivity. Qed. - Lemma th2 : min = O. - Reflexivity. + Lemma th2 : min = 0. + reflexivity. Qed. (* It should still be the case after Import M *) Import M. - Lemma th3 : le_decide = (S O). - Reflexivity. + Lemma th3 : le_decide = 1. + reflexivity. Qed. - Lemma th4 : min = O. - Reflexivity. + Lemma th4 : min = 0. + reflexivity. Qed. End Test_Import. @@ -121,24 +121,24 @@ Module Test_Export. Module M. Export Compare. (* Exports Min as well *) - Lemma th1 : le_decide = Compare.le_decide. - Reflexivity. + Lemma th1 : le_decide = le_decide. + reflexivity. Qed. - Lemma th2 : min = Min.min. - Reflexivity. + Lemma th2 : min = min. + reflexivity. Qed. End M. (* Checks that Compare and List are _not_ imported *) - Lemma th1 : le_decide = (S O). - Reflexivity. + Lemma th1 : le_decide = 1. + reflexivity. Qed. - Lemma th2 : min = O. - Reflexivity. + Lemma th2 : min = 0. + reflexivity. Qed. @@ -146,12 +146,12 @@ Module Test_Export. Import M. - Lemma th3 : le_decide = Compare.le_decide. - Reflexivity. + Lemma th3 : le_decide = le_decide. + reflexivity. Qed. - Lemma th4 : min = Min.min. - Reflexivity. + Lemma th4 : min = min. + reflexivity. Qed. End Test_Export. @@ -160,30 +160,30 @@ End Test_Export. Module Test_Require_Export. - Definition mult_sym:=(S O). (* from Arith/Mult *) - Definition plus_sym:=O. (* from Arith/Plus *) + Definition mult_sym := 1. (* from Arith/Mult *) + Definition plus_sym := 0. (* from Arith/Plus *) Module M. Require Export Mult. (* Exports Plus as well *) - Lemma th1 : mult_sym = Mult.mult_sym. - Reflexivity. + Lemma th1 : mult_comm = mult_comm. + reflexivity. Qed. - Lemma th2 : plus_sym = Plus.plus_sym. - Reflexivity. + Lemma th2 : plus_comm = plus_comm. + reflexivity. Qed. End M. (* Checks that Mult and Plus are _not_ imported *) - Lemma th1 : mult_sym = (S O). - Reflexivity. + Lemma th1 : mult_sym = 1. + reflexivity. Qed. - Lemma th2 : plus_sym = O. - Reflexivity. + Lemma th2 : plus_sym = 0. + reflexivity. Qed. @@ -191,12 +191,12 @@ Module Test_Require_Export. Import M. - Lemma th3 : mult_sym = Mult.mult_sym. - Reflexivity. + Lemma th3 : mult_comm = mult_comm. + reflexivity. Qed. - Lemma th4 : plus_sym = Plus.plus_sym. - Reflexivity. + Lemma th4 : plus_comm = plus_comm. + reflexivity. Qed. End Test_Require_Export. diff --git a/test-suite/success/import_mod.v b/test-suite/success/import_mod.v index b4a8af46f..c098c6e89 100644 --- a/test-suite/success/import_mod.v +++ b/test-suite/success/import_mod.v @@ -1,38 +1,38 @@ -Definition p:=O. -Definition m:=O. +Definition p := 0. +Definition m := 0. Module Test_Import. Module P. - Definition p:=(S O). + Definition p := 1. End P. Module M. Import P. - Definition m:=p. + Definition m := p. End M. Module N. Import M. - Lemma th0 : p=O. - Reflexivity. + Lemma th0 : p = 0. + reflexivity. Qed. End N. (* M and P should be closed *) - Lemma th1 : m=O /\ p=O. - Split; Reflexivity. + Lemma th1 : m = 0 /\ p = 0. + split; reflexivity. Qed. Import N. (* M and P should still be closed *) - Lemma th2 : m=O /\ p=O. - Split; Reflexivity. + Lemma th2 : m = 0 /\ p = 0. + split; reflexivity. Qed. End Test_Import. @@ -42,34 +42,34 @@ End Test_Import. Module Test_Export. Module P. - Definition p:=(S O). + Definition p := 1. End P. Module M. Export P. - Definition m:=p. + Definition m := p. End M. Module N. Export M. - Lemma th0 : p=(S O). - Reflexivity. + Lemma th0 : p = 1. + reflexivity. Qed. End N. (* M and P should be closed *) - Lemma th1 : m=O /\ p=O. - Split; Reflexivity. + Lemma th1 : m = 0 /\ p = 0. + split; reflexivity. Qed. Import N. (* M and P should now be opened *) - Lemma th2 : m=(S O) /\ p=(S O). - Split; Reflexivity. + Lemma th2 : m = 1 /\ p = 1. + split; reflexivity. Qed. End Test_Export. diff --git a/test-suite/success/inds_type_sec.v b/test-suite/success/inds_type_sec.v index a391b8046..ed8b23c8d 100644 --- a/test-suite/success/inds_type_sec.v +++ b/test-suite/success/inds_type_sec.v @@ -6,5 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) Section S. -Inductive T [U:Type] : Type := c : U -> (T U). +Inductive T (U : Type) : Type := + c : U -> T U. End S. diff --git a/test-suite/success/induct.v b/test-suite/success/induct.v index 9ae498d2d..2aec6e9b1 100644 --- a/test-suite/success/induct.v +++ b/test-suite/success/induct.v @@ -7,11 +7,11 @@ (************************************************************************) (* Teste des definitions inductives imbriquees *) -Require PolyList. +Require Import List. -Inductive X : Set := - cons1 : (list X)->X. +Inductive X : Set := + cons1 : list X -> X. -Inductive Y : Set := - cons2 : (list Y*Y)->Y. +Inductive Y : Set := + cons2 : list (Y * Y) -> Y. diff --git a/test-suite/success/intros.v8 b/test-suite/success/intros.v index 1da947b50..3599da4dc 100644 --- a/test-suite/success/intros.v8 +++ b/test-suite/success/intros.v @@ -4,3 +4,4 @@ Goal forall A, A -> True. intros _ _. + diff --git a/test-suite/success/ltac.v b/test-suite/success/ltac.v index 5cd397067..b6aa1e705 100644 --- a/test-suite/success/ltac.v +++ b/test-suite/success/ltac.v @@ -2,20 +2,23 @@ (* Submitted by Pierre Crégut *) (* Checks substitution of x *) -Tactic Definition f x := Unfold x; Idtac. +Ltac f x := unfold x in |- *; idtac. -Lemma lem1 : (plus O O) = O. +Lemma lem1 : 0 + 0 = 0. f plus. -Reflexivity. +reflexivity. Qed. (* Submitted by Pierre Crégut *) (* Check syntactic correctness *) -Recursive Tactic Definition F x := Idtac; (G x) -And G y := Idtac; (F y). +Ltac F x := idtac; G x + with G y := idtac; F y. (* Check that Match Context keeps a closure *) -Tactic Definition U := Let a = 'I In Match Context With [ |- ? ] -> Apply a. +Ltac U := let a := constr:I in + match goal with + | |- _ => apply a + end. Lemma lem2 : True. U. @@ -23,81 +26,106 @@ Qed. (* Check that Match giving non-tactic arguments are evaluated at Let-time *) -Tactic Definition B := - Let y = (Match Context With [ z:? |- ? ] -> z) In - Intro H1; Exact y. +Ltac B := let y := (match goal with + | z:_ |- _ => z + end) in + (intro H1; exact y). Lemma lem3 : True -> False -> True -> False. -Intros H H0. +intros H H0. B. (* y is H0 if at let-time, H1 otherwise *) Qed. (* Checks the matching order of hypotheses *) -Tactic Definition Y := Match Context With [ x:?; y:? |- ? ] -> Apply x. -Tactic Definition Z := Match Context With [ y:?; x:? |- ? ] -> Apply x. - -Lemma lem4 : (True->False) -> (False->False) -> False. -Intros H H0. +Ltac Y := match goal with + | x:_,y:_ |- _ => apply x + end. +Ltac Z := match goal with + | y:_,x:_ |- _ => apply x + end. + +Lemma lem4 : (True -> False) -> (False -> False) -> False. +intros H H0. Z. (* Apply H0 *) Y. (* Apply H *) -Exact I. +exact I. Qed. (* Check backtracking *) -Lemma back1 : (0)=(1)->(0)=(0)->(1)=(1)->(0)=(0). -Intros; Match Context With [_:(O)=?1;_:(1)=(1)|-? ] -> Exact (refl_equal ? ?1). +Lemma back1 : 0 = 1 -> 0 = 0 -> 1 = 1 -> 0 = 0. +intros; + match goal with + | _:(0 = ?X1),_:(1 = 1) |- _ => exact (refl_equal X1) + end. Qed. -Lemma back2 : (0)=(0)->(0)=(1)->(1)=(1)->(0)=(0). -Intros; Match Context With [_:(O)=?1;_:(1)=(1)|-? ] -> Exact (refl_equal ? ?1). +Lemma back2 : 0 = 0 -> 0 = 1 -> 1 = 1 -> 0 = 0. +intros; + match goal with + | _:(0 = ?X1),_:(1 = 1) |- _ => exact (refl_equal X1) + end. Qed. -Lemma back3 : (0)=(0)->(1)=(1)->(0)=(1)->(0)=(0). -Intros; Match Context With [_:(O)=?1;_:(1)=(1)|-? ] -> Exact (refl_equal ? ?1). +Lemma back3 : 0 = 0 -> 1 = 1 -> 0 = 1 -> 0 = 0. +intros; + match goal with + | _:(0 = ?X1),_:(1 = 1) |- _ => exact (refl_equal X1) + end. Qed. (* Check context binding *) -Tactic Definition sym t := Match t With [C[?1=?2]] -> Inst C[?1=?2]. - -Lemma sym : ~(0)=(1)->~(1)=(0). -Intro H. -Let t = (sym (Check H)) In Assert t. -Exact H. -Intro H1. -Apply H. -Symmetry. -Assumption. +Ltac sym t := + match constr:t with + | context C[(?X1 = ?X2)] => context C [X1 = X2] + end. + +Lemma sym : 0 <> 1 -> 1 <> 0. +intro H. +let t := sym type of H in +assert t. +exact H. +intro H1. +apply H. +symmetry in |- *. +assumption. Qed. (* Check context binding in match goal *) (* This wasn't working in V8.0pl1, as the list of matched hyps wasn't empty *) -Tactic Definition sym' := - Match Context With [_:True|-C[?1=?2]] -> Let t = Inst C[?2=?1] In Assert t. - -Lemma sym' : True->~(0)=(1)->~(1)=(0). -Intros Ht H. +Ltac sym' := + match goal with + | _:True |- context C[(?X1 = ?X2)] => + let t := context C [X2 = X1] in + assert t + end. + +Lemma sym' : True -> 0 <> 1 -> 1 <> 0. +intros Ht H. sym'. -Exact H. -Intro H1. -Apply H. -Symmetry. -Assumption. +exact H. +intro H1. +apply H. +symmetry in |- *. +assumption. Qed. (* Check that fails abort the current match context *) Lemma decide : True \/ False. -(Match Context With -| _ -> Fail 1 -| _ -> Right) Orelse Left. -Exact I. +match goal with +| _ => fail 1 +| _ => right +end || left. +exact I. Qed. (* Check that "match c with" backtracks on subterms *) -Lemma refl : (1)=(1). -Let t = (Match (1)=(2) With - [[(S ?1)]] -> '((refl_equal nat ?1) :: (1)=(1))) -In Assert H:=t. -Assumption. +Lemma refl : 1 = 1. +let t := + (match constr:(1 = 2) with + | context [(S ?X1)] => constr:(refl_equal X1:1 = 1) + end) in +assert (H := t). +assumption. Qed. (* Note that backtracking in "match c with" is only on type-checking not on @@ -113,7 +141,7 @@ Qed. (* Check the precedences of rel context, ltac context and vars context *) (* (was wrong in V8.0) *) -Tactic Definition check_binding y := Cut (([y]y) = S). +Ltac check_binding y := cut ((fun y => y) = S). Goal True. check_binding true. Abort. diff --git a/test-suite/success/mutual_ind.v b/test-suite/success/mutual_ind.v index e932f50ca..463efed3f 100644 --- a/test-suite/success/mutual_ind.v +++ b/test-suite/success/mutual_ind.v @@ -7,35 +7,36 @@ (************************************************************************) (* Definition mutuellement inductive et dependante *) -Require Export PolyList. +Require Export List. - Record signature : Type := { - sort : Set; - sort_beq : sort->sort->bool; - sort_beq_refl : (f:sort)true=(sort_beq f f); - sort_beq_eq : (f1,f2:sort)true=(sort_beq f1 f2)->f1=f2; + Record signature : Type := + {sort : Set; + sort_beq : sort -> sort -> bool; + sort_beq_refl : forall f : sort, true = sort_beq f f; + sort_beq_eq : forall f1 f2 : sort, true = sort_beq f1 f2 -> f1 = f2; fsym :> Set; - fsym_type : fsym->(list sort)*sort; - fsym_beq : fsym->fsym->bool; - fsym_beq_refl : (f:fsym)true=(fsym_beq f f); - fsym_beq_eq : (f1,f2:fsym)true=(fsym_beq f1 f2)->f1=f2 - }. + fsym_type : fsym -> list sort * sort; + fsym_beq : fsym -> fsym -> bool; + 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. + Definition vsym := (sort F * nat)%type. - Definition vsym_sort := (fst (sort F) nat). - Definition vsym_nat := (snd (sort F) nat). + Definition vsym_sort := fst (A:=sort F) (B:=nat). + Definition vsym_nat := snd (A:=sort F) (B:=nat). - Mutual Inductive term : (sort F)->Set := - | term_var : (v:vsym)(term (vsym_sort v)) - | term_app : (f:F)(list_term (Fst (fsym_type F f))) - ->(term (Snd (fsym_type F f))) - with list_term : (list (sort F)) -> Set := - | term_nil : (list_term (nil (sort F))) - | term_cons : (s:(sort F);l:(list (sort F))) - (term s)->(list_term l)->(list_term (cons s l)). + Inductive term : sort F -> Set := + | term_var : forall v : vsym, term (vsym_sort v) + | term_app : + forall f : F, + list_term (fst (fsym_type F f)) -> term (snd (fsym_type F f)) +with list_term : list (sort F) -> Set := + | term_nil : list_term nil + | term_cons : + forall (s : sort F) (l : list (sort F)), + term s -> list_term l -> list_term (s :: l). diff --git a/test-suite/success/options.v b/test-suite/success/options.v index 9e9af4fa8..bb6781506 100644 --- a/test-suite/success/options.v +++ b/test-suite/success/options.v @@ -1,5 +1,7 @@ (* Check that the syntax for options works *) Set Implicit Arguments. +Unset Strict Implicit. +Set Strict Implicit. Unset Implicit Arguments. Test Implicit Arguments. @@ -12,16 +14,16 @@ Unset Silent. Test Silent. Set Printing Depth 100. -Print Table Printing Depth. +Test Printing Depth. Parameter i : bool -> nat. Coercion i : bool >-> nat. -Set Printing Coercion i. -Unset Printing Coercion i. +Add Printing Coercion i. +Remove Printing Coercion i. Test Printing Coercion i. -Print Table Printing Let. -Print Table Printing If. +Test Printing Let. +Test Printing If. Remove Printing Let sig. Remove Printing If bool. diff --git a/test-suite/success/params_ind.v b/test-suite/success/params_ind.v index 206891286..1bee31c8a 100644 --- a/test-suite/success/params_ind.v +++ b/test-suite/success/params_ind.v @@ -1,4 +1,4 @@ -Inductive list [A:Set] : Set := - nil : (list A) -| cons : A -> (list A->A)-> (list A). +Inductive list (A : Set) : Set := + | nil : list A + | cons : A -> list (A -> A) -> list A. diff --git a/test-suite/success/refine.v b/test-suite/success/refine.v index 96fa79ebd..b61cf275f 100644 --- a/test-suite/success/refine.v +++ b/test-suite/success/refine.v @@ -1,33 +1,34 @@ (* Refine and let-in's *) -Goal (EX x:nat | x=O). -Refine let y = (plus O O) in ?. -Exists y; Auto. +Goal exists x : nat, x = 0. + refine (let y := 0 + 0 in _). +exists y; auto. Save test1. -Goal (EX x:nat | x=O). -Refine let y = (plus O O) in (ex_intro ? ? (plus y y) ?). -Auto. +Goal exists x : nat, x = 0. + refine (let y := 0 + 0 in ex_intro _ (y + y) _). +auto. Save test2. Goal nat. -Refine let y = O in (plus O ?). -Exact (S O). + refine (let y := 0 in 0 + _). +exact 1. Save test3. (* Example submitted by Yves on coqdev *) -Require PolyList. +Require Import List. -Goal (l:(list nat))l=l. +Goal forall l : list nat, l = l. Proof. -Refine [l]<[l]l=l> - Cases l of - | nil => ? - | (cons O l0) => ? - | (cons (S _) l0) => ? - end. + refine + (fun l => + match l return (l = l) with + | nil => _ + | O :: l0 => _ + | S _ :: l0 => _ + end). Abort. (* Submitted by Roland Zumkeller (bug #888) *) @@ -36,10 +37,10 @@ Abort. (co-)fixpoint *) Goal nat -> nat. -Refine( - Fix f {f [n:nat] : nat := (S ?) with - pred [n:nat] : nat := n}). -Exact 0. + refine (fix f (n : nat) : nat := S _ + with pred (n : nat) : nat := n + for f). +exact 0. Qed. (* Submitted by Roland Zumkeller (bug #889) *) @@ -47,17 +48,19 @@ Qed. (* The types of metas were in metamap and they were not updated when passing through a binder *) -Goal (n:nat) nat -> n=0. -Refine [n] - Fix f { f [i:nat] : n=0 := - Cases i of 0 => ? | (S _) => ? end }. +Goal forall n : nat, nat -> n = 0. + refine + (fun n => fix f (i : nat) : n = 0 := match i with + | O => _ + | S _ => _ + end). Abort. (* Submitted by Roland Zumkeller (bug #931) *) (* Don't turn dependent evar into metas *) -Goal ((n:nat)n=O->Prop) -> Prop. -Intro P. -Refine(P ? ?). -Reflexivity. +Goal (forall n : nat, n = 0 -> Prop) -> Prop. +intro P. + refine (P _ _). +reflexivity. Abort. diff --git a/test-suite/success/rewrite.v b/test-suite/success/rewrite.v index 8816d1536..9629b2132 100644 --- a/test-suite/success/rewrite.v +++ b/test-suite/success/rewrite.v @@ -1,17 +1,19 @@ (* Check that dependent rewrite applies on arbitrary terms *) -Inductive listn : nat-> Set := - niln : (listn O) -| consn : (n:nat)nat->(listn n) -> (listn (S n)). +Inductive listn : nat -> Set := + | niln : listn 0 + | consn : forall n : nat, nat -> listn n -> listn (S n). -Axiom ax : (n,n':nat)(l:(listn (plus n n')))(l':(listn (plus n' n))) - (existS ? ? (plus n n') l) =(existS ? ? (plus n' n) l'). +Axiom + ax : + forall (n n' : nat) (l : listn (n + n')) (l' : listn (n' + n)), + existS _ (n + n') l = existS _ (n' + n) l'. -Lemma lem : (n,n':nat)(l:(listn (plus n n')))(l':(listn (plus n' n))) - (plus n n')=(plus n' n) - /\ (existT ? ? (plus n n') l) =(existT ? ? (plus n' n) l'). +Lemma lem : + forall (n n' : nat) (l : listn (n + n')) (l' : listn (n' + n)), + n + n' = n' + n /\ existT _ (n + n') l = existT _ (n' + n) l'. Proof. -Intros n n' l l'. -Dependent Rewrite (ax n n' l l'). -Split; Reflexivity. +intros n n' l l'. + dependent rewrite (ax n n' l l'). +split; reflexivity. Qed. diff --git a/test-suite/success/set.v8 b/test-suite/success/set.v index 5a190d313..230192753 100644 --- a/test-suite/success/set.v8 +++ b/test-suite/success/set.v @@ -5,3 +5,4 @@ intros. set n in * |-. + diff --git a/test-suite/success/setoid_test.v8 b/test-suite/success/setoid_test.v index 574cb525a..dd1022f08 100644 --- a/test-suite/success/setoid_test.v8 +++ b/test-suite/success/setoid_test.v @@ -103,3 +103,4 @@ setoid_rewrite H. setoid_rewrite <- H. trivial. Qed. + diff --git a/test-suite/success/setoid_test2.v8 b/test-suite/success/setoid_test2.v index a4156c680..bac1cf149 100644 --- a/test-suite/success/setoid_test2.v8 +++ b/test-suite/success/setoid_test2.v @@ -239,3 +239,4 @@ Theorem test8: Abort. (*Print Setoids.*) + diff --git a/test-suite/success/setoid_test_function_space.v8 b/test-suite/success/setoid_test_function_space.v index 81ec267e3..1602991df 100644 --- a/test-suite/success/setoid_test_function_space.v8 +++ b/test-suite/success/setoid_test_function_space.v @@ -42,3 +42,4 @@ intuition. setoid_rewrite <- H0. assumption. Qed. + diff --git a/test-suite/success/simpl.v8 b/test-suite/success/simpl.v index 91015ab28..8d32b1d9f 100644 --- a/test-suite/success/simpl.v8 +++ b/test-suite/success/simpl.v @@ -21,3 +21,4 @@ with copy_of_compute_size_tree (t:tree) : nat := Eval simpl in (copy_of_compute_size_forest leaf). + diff --git a/test-suite/success/unfold.v b/test-suite/success/unfold.v index de75dfce8..359100110 100644 --- a/test-suite/success/unfold.v +++ b/test-suite/success/unfold.v @@ -8,8 +8,8 @@ (* Test le Hint Unfold sur des var locales *) Section toto. -Local EQ:=eq. -Goal (EQ nat O O). -Hints Unfold EQ. -Auto. -Save. +Let EQ := eq. +Goal EQ nat 0 0. +Hint Unfold EQ. +auto. +Qed. diff --git a/test-suite/success/univers.v b/test-suite/success/univers.v index a2a1d0dd6..87edc4deb 100644 --- a/test-suite/success/univers.v +++ b/test-suite/success/univers.v @@ -1,41 +1,42 @@ (* This requires cumulativity *) Definition Type2 := Type. -Definition Type1 := Type : Type2. +Definition Type1 : Type2 := Type. -Lemma lem1 : (True->Type1)->Type2. -Intro H. -Apply H. -Exact I. +Lemma lem1 : (True -> Type1) -> Type2. +intro H. +apply H. +exact I. Qed. -Lemma lem2 : (A:Type)(P:A->Type)(x:A)((y:A)(x==y)->(P y))->(P x). -Auto. +Lemma lem2 : + forall (A : Type) (P : A -> Type) (x : A), + (forall y : A, x = y -> P y) -> P x. +auto. Qed. -Lemma lem3 : (P:Prop)P. -Intro P ; Pattern P. -Apply lem2. +Lemma lem3 : forall P : Prop, P. +intro P; pattern P in |- *. +apply lem2. Abort. (* Check managing of universe constraints in inversion *) (* Bug report #855 *) -Inductive dep_eq : (X:Type) X -> X -> Prop := - | intro_eq : (X:Type) (f:X)(dep_eq X f f) - | intro_feq : (A:Type) (B:A->Type) - let T = (x:A)(B x) in - (f, g:T) (x:A) - (dep_eq (B x) (f x) (g x)) -> - (dep_eq T f g). +Inductive dep_eq : forall X : Type, X -> X -> Prop := + | intro_eq : forall (X : Type) (f : X), dep_eq X f f + | intro_feq : + 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 : (X:Type) (transitive X (dep_eq X)). +Theorem dep_eq_trans : forall X : Type, transitive X (dep_eq X). Proof. - Unfold transitive. - Intros X f g h H1 H2. - Inversion H1. + unfold transitive in |- *. + intros X f g h H1 H2. + inversion H1. Abort. @@ -50,8 +51,8 @@ Abort. Especially, universe refreshing was not done for "set/pose" *) -Lemma ind_unsec:(Q:nat->Type)True. -Intro. -Pose C:= (m:?)(Q m)->(Q m). -Exact I. +Lemma ind_unsec : forall Q : nat -> Type, True. +intro. +set (C := forall m, Q m -> Q m). +exact I. Qed. |