diff options
Diffstat (limited to 'test-suite/success/Cases.v')
-rw-r--r-- | test-suite/success/Cases.v | 2494 |
1 files changed, 1359 insertions, 1135 deletions
diff --git a/test-suite/success/Cases.v b/test-suite/success/Cases.v index 6ccd669a..7c2b7c0b 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). |