summaryrefslogtreecommitdiff
path: root/test-suite/success/Cases.v
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/success/Cases.v')
-rw-r--r--test-suite/success/Cases.v2494
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).
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-10 05:42:22 +0000