diff options
| author |  mohring <mohring@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-04-20 13:14:27 +0000 |
|---|---|---|
| committer | mohring <mohring@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-04-20 13:14:27 +0000 |
| commit | 07b4a4b98412ab5444132e6407dff9276a070b60 (patch) | |
| tree | 3464a0de3cb58daf82964db4aee3bd5b0215eeb1 /test-suite | |
| parent | 55f59774cb3045374342c5b00f4a999b6ff0911b (diff) | |
Decomposition de Cases
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1651 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/success/Case10.v | 26 | ||||
| -rw-r--r-- | test-suite/success/Case3.v | 25 | ||||
| -rw-r--r-- | test-suite/success/Case4.v | 35 | ||||
| -rw-r--r-- | test-suite/success/Case5.v | 15 | ||||
| -rw-r--r-- | test-suite/success/Case6.v | 15 | ||||
| -rw-r--r-- | test-suite/success/Case7.v | 13 | ||||
| -rw-r--r-- | test-suite/success/Case8.v | 36 | ||||
| -rw-r--r-- | test-suite/success/Case9.v | 53 | ||||
| -rw-r--r-- | test-suite/success/Cases.v | 1098 | ||||
| -rw-r--r-- | test-suite/success/CasesDep.v | 376 |
10 files changed, 796 insertions, 896 deletions
diff --git a/test-suite/success/Case10.v b/test-suite/success/Case10.v new file mode 100644 index 000000000..73413c475 --- /dev/null +++ b/test-suite/success/Case10.v @@ -0,0 +1,26 @@ +(* ============================================== *) +(* To test compilation of dependent case *) +(* Multiple Patterns *) +(* ============================================== *) +Inductive skel: Type := + PROP: skel + | PROD: skel->skel->skel. + +Parameter Can : skel -> Type. +Parameter default_can : (s:skel) (Can s). + + +Type [s1,s2:skel] + <[s1,_:skel](Can s1)>Cases s1 s2 of + PROP PROP => (default_can PROP) + | s1 _ => (default_can s1) + end. + + +Type [s1,s2:skel] +<[s1:skel][_:skel](Can s1)>Cases s1 s2 of + PROP PROP => (default_can PROP) +| (PROP as s) _ => (default_can s) +| ((PROD s1 s2) as s) PROP => (default_can s) +| ((PROD s1 s2) as s) _ => (default_can s) +end. diff --git a/test-suite/success/Case3.v b/test-suite/success/Case3.v new file mode 100644 index 000000000..71429db49 --- /dev/null +++ b/test-suite/success/Case3.v @@ -0,0 +1,25 @@ + +Parameter iguales : (n,m:nat)(h:(Le n m))Prop . + +Type <[n,m:nat][h:(Le n m)]Prop>Cases (LeO O) of + (LeO O) => True + | (LeS (S x) (S y) H) => (iguales (S x) (S y) H) + | _ => False end. + + +Type <[n,m:nat][h:(Le n m)]Prop>Cases (LeO O) of + (LeO O) => True + | (LeS (S x) O H) => (iguales (S x) O H) + | _ => False end. + +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 O) => (or_intror (S O)=O ? (discr_l O)) + | (S (S x)) => (or_intror (S (S x))=O ? (discr_l (S x))) + + end. + diff --git a/test-suite/success/Case4.v b/test-suite/success/Case4.v new file mode 100644 index 000000000..eaec5a52f --- /dev/null +++ b/test-suite/success/Case4.v @@ -0,0 +1,35 @@ +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 O y) as b) => (or_intror (empty (S n) b) ? (inv_empty n O y)) + | ((consn n a y) as b) => (or_intror (empty (S n) b) ? (inv_empty n a y)) + + end. + + +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 O y) => (or_intror (empty (S n) (consn n O y)) ? + (inv_empty n O y)) + | (consn n a y) => (or_intror (empty (S n) (consn n a y)) ? + (inv_empty n a y)) + + end. + +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 O a y) as b) => (or_intror (empty (S O) b) ? (inv_empty O a y)) + | ((consn n a y) as b) => (or_intror (empty (S n) b) ? (inv_empty n a y)) + + end. + diff --git a/test-suite/success/Case5.v b/test-suite/success/Case5.v new file mode 100644 index 000000000..d703286f9 --- /dev/null +++ b/test-suite/success/Case5.v @@ -0,0 +1,15 @@ + +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 O) => (or_intror (S O)=O ? (discr_l O)) + | (S (S x)) => (or_intror (S (S x))=O ? (discr_l (S x))) + + end. diff --git a/test-suite/success/Case6.v b/test-suite/success/Case6.v new file mode 100644 index 000000000..1d5e3fb4e --- /dev/null +++ b/test-suite/success/Case6.v @@ -0,0 +1,15 @@ +Fixpoint eqdec [n:nat] : (m:nat) n=m \/ ~n=m := +[m:nat] + <[n,m:nat] n=m \/ ~n=m>Cases n m of + O O => (or_introl ? ~O=O (refl_equal ? O)) + + | O (S x) => (or_intror O=(S x) ? (discr_r x)) + + | (S x) O => (or_intror ? ~(S x)=O (discr_l x)) + + | ((S x) as N) ((S y) as M) => + <N=M\/~N=M>Cases (eqdec x y) of + (or_introl h) => (or_introl ? ~N=M (f_equal nat nat S x y h)) + | (or_intror h) => (or_intror N=M ? (ff x y h)) + end + end. diff --git a/test-suite/success/Case7.v b/test-suite/success/Case7.v new file mode 100644 index 000000000..d0bb8ee63 --- /dev/null +++ b/test-suite/success/Case7.v @@ -0,0 +1,13 @@ +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)). + + +Type +[A:Set] +[l:(List A)] + <[l:(List A)](Empty A l) \/ ~(Empty A l)>Cases l of + Nil => (or_introl ? ~(Empty A (Nil A)) (intro_Empty A)) + | ((Cons a y) as b) => (or_intror (Empty A b) ? (inv_Empty A a y)) + end. diff --git a/test-suite/success/Case8.v b/test-suite/success/Case8.v new file mode 100644 index 000000000..1775c6a3f --- /dev/null +++ b/test-suite/success/Case8.v @@ -0,0 +1,36 @@ +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 O y) as b) => (or_intror (empty (S n) b) ? (inv_empty n O y)) + | ((consn n a y) as b) => (or_intror (empty (S n) b) ? (inv_empty n a y)) + + end. + + +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 O y) => (or_intror (empty (S n) (consn n O y)) ? + (inv_empty n O y)) + | (consn n a y) => (or_intror (empty (S n) (consn n a y)) ? + (inv_empty n a y)) + + end. + + + +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 O a y) as b) => (or_intror (empty (S O) b) ? (inv_empty O a y)) + | ((consn n a y) as b) => (or_intror (empty (S n) b) ? (inv_empty n a y)) + + end. diff --git a/test-suite/success/Case9.v b/test-suite/success/Case9.v new file mode 100644 index 000000000..39e387d76 --- /dev/null +++ b/test-suite/success/Case9.v @@ -0,0 +1,53 @@ + +Inductive eqlong : (List nat)-> (List nat)-> Prop := + eql_cons : (n,m:nat)(x,y:(List nat)) + (eqlong x y) -> (eqlong (Cons nat n x) (Cons nat m y)) +| eql_nil : (eqlong (Nil nat) (Nil nat)). + + +Parameter V1 : (eqlong (Nil nat) (Nil nat))\/ ~(eqlong (Nil nat) (Nil nat)). +Parameter V2 : (a:nat)(x:(List nat)) + (eqlong (Nil nat) (Cons nat a x))\/ ~(eqlong (Nil nat)(Cons nat a x)). +Parameter V3 : (a:nat)(x:(List nat)) + (eqlong (Cons nat a x) (Nil nat))\/ ~(eqlong (Cons nat a x) (Nil nat)). +Parameter V4 : (a:nat)(x:(List nat))(b:nat)(y:(List nat)) + (eqlong (Cons nat a x)(Cons nat b y)) + \/ ~(eqlong (Cons nat a x) (Cons nat b y)). + +Parameter nff : (n,m:nat)(x,y:(List nat)) + ~(eqlong x y)-> ~(eqlong (Cons nat n x) (Cons nat m y)). +Parameter inv_r : (n:nat)(x:(List nat)) ~(eqlong (Nil nat) (Cons nat n x)). +Parameter inv_l : (n:nat)(x:(List nat)) ~(eqlong (Cons nat n x) (Nil nat)). + +Fixpoint eqlongdec [x:(List nat)]: (y:(List nat))(eqlong x y)\/~(eqlong x y) := +[y:(List nat)] + <[x,y:(List nat)](eqlong x y)\/~(eqlong x y)>Cases x y of + Nil Nil => (or_introl ? ~(eqlong (Nil nat) (Nil nat)) eql_nil) + + | Nil ((Cons a x) as L) =>(or_intror (eqlong (Nil nat) L) ? (inv_r a x)) + + | ((Cons a x) as L) Nil => (or_intror (eqlong L (Nil nat)) ? (inv_l a x)) + + | ((Cons a x) as L1) ((Cons b y) as L2) => + <(eqlong L1 L2) \/~(eqlong L1 L2)>Cases (eqlongdec x y) of + (or_introl h) => (or_introl ? ~(eqlong L1 L2) (eql_cons a b x y h)) + | (or_intror h) => (or_intror (eqlong L1 L2) ? (nff a b x y h)) + end + end. + + +Type + <[x,y:(List nat)](eqlong x y)\/~(eqlong x y)>Cases (Nil nat) (Nil nat) of + Nil Nil => (or_introl ? ~(eqlong (Nil nat) (Nil nat)) eql_nil) + + | Nil ((Cons a x) as L) =>(or_intror (eqlong (Nil nat) L) ? (inv_r a x)) + + | ((Cons a x) as L) Nil => (or_intror (eqlong L (Nil nat)) ? (inv_l a x)) + + | ((Cons a x) as L1) ((Cons b y) as L2) => + <(eqlong L1 L2) \/~(eqlong L1 L2)>Cases (eqlongdec x y) of + (or_introl h) => (or_introl ? ~(eqlong L1 L2) (eql_cons a b x y h)) + | (or_intror h) => (or_intror (eqlong L1 L2) ? (nff a b x y h)) + end + end. + diff --git a/test-suite/success/Cases.v b/test-suite/success/Cases.v index 3dcfbefb3..313f8f74a 100644 --- a/test-suite/success/Cases.v +++ b/test-suite/success/Cases.v @@ -9,11 +9,11 @@ (* Pattern-matching when non inductive terms occur *) (* Dependent form of annotation *) -Check <[n:nat]nat>Cases O eq of O x => O | (S x) y => x end. -Check <[_,_:nat]nat>Cases O eq O of O x y => O | (S x) y z => x end. +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. (* Non dependent form of annotation *) -Check <nat>Cases O eq of O x => O | (S x) y => x end. +Type <nat>Cases O eq of O x => O | (S x) y => x end. (****************************************************************************) (* All remaining examples come from Cristina Cornes' V6 TESTS/MultCases.v *) @@ -54,13 +54,13 @@ Section testIFExpr. Definition Assign:= nat->bool. Parameter Prop_sem : Assign -> PropForm -> bool. -Check [A:Assign][F:PropForm] +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. -Check [A:Assign][H:PropForm] +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)) @@ -69,7 +69,7 @@ End testIFExpr. -Check [x:nat]<nat>Cases x of O => O | x => x end. +Type [x:nat]<nat>Cases x of O => O | x => x end. Section testlist. Parameter A:Set. @@ -92,142 +92,138 @@ End testlist. (* ------------------- *) -Check <nat>Cases O of O => O | _ => O end. +Type <nat>Cases O of O => O | _ => O end. -Check <nat>Cases O of +Type <nat>Cases O of (O as b) => b | (S O) => O | (S (S x)) => x end. -Check Cases O of +Type Cases O of (O as b) => b | (S O) => O | (S (S x)) => x end. -Check [x:nat]<nat>Cases x of +Type [x:nat]<nat>Cases x of (O as b) => b | (S x) => x end. -Check [x:nat]Cases x of +Type [x:nat]Cases x of (O as b) => b | (S x) => x end. -Check <nat>Cases O of +Type <nat>Cases O of (O as b) => b | (S x) => x end. -Check <nat>Cases O of +Type <nat>Cases O of x => x end. -Check Cases O of +Type Cases O of x => x end. -Check <nat>Cases O of +Type <nat>Cases O of O => O | ((S x) as b) => b end. -Check [x:nat]<nat>Cases x of +Type [x:nat]<nat>Cases x of O => O | ((S x) as b) => b end. -Check [x:nat] Cases x of +Type [x:nat] Cases x of O => O | ((S x) as b) => b end. -Check <nat>Cases O of +Type <nat>Cases O of O => O | (S x) => O end. -Check <nat*nat>Cases O of +Type <nat*nat>Cases O of O => (O,O) | (S x) => (x,O) end. -Check Cases O of +Type Cases O of O => (O,O) | (S x) => (x,O) end. -Check <nat->nat>Cases O of +Type <nat->nat>Cases O of O => [n:nat]O | (S x) => [n:nat]O end. -Check Cases O of +Type Cases O of O => [n:nat]O | (S x) => [n:nat]O end. -Check <nat->nat>Cases O of +Type <nat->nat>Cases O of O => [n:nat]O | (S x) => [n:nat](plus x n) end. -Check Cases O of +Type Cases O of O => [n:nat]O | (S x) => [n:nat](plus x n) end. -Check <nat>Cases O of +Type <nat>Cases O of O => O | ((S x) as b) => (plus b x) end. -Check <nat>Cases O of +Type <nat>Cases O of O => O | ((S (x as a)) as b) => (plus b a) end. -Check Cases O of +Type Cases O of O => O | ((S (x as a)) as b) => (plus b a) end. -Check Cases O of +Type Cases O of O => O | _ => O end. -Check <nat>Cases O of +Type <nat>Cases O of O => O | x => x end. -Check Cases O of - x => O - | O => (S O) - end. -Check <nat>Cases O (S O) of +Type <nat>Cases O (S O) of x y => (plus x y) end. -Check Cases O (S O) of +Type Cases O (S O) of x y => (plus x y) end. -Check <nat>Cases O (S O) of +Type <nat>Cases O (S O) of O y => y | (S x) y => (plus x y) end. -Check Cases O (S O) of +Type Cases O (S O) of O y => y | (S x) y => (plus x y) end. -Check <nat>Cases O (S O) of +Type <nat>Cases O (S O) of O x => x | (S y) O => y | x y => (plus x y) @@ -236,13 +232,13 @@ Check <nat>Cases O (S O) of -Check Cases O (S O) of +Type Cases O (S O) of O x => (plus x O) | (S y) O => (plus y O) | x y => (plus x y) end. -Check +Type <nat>Cases O (S O) of O x => (plus x O) | (S y) O => (plus y O) @@ -250,7 +246,7 @@ Check end. -Check +Type <nat>Cases O (S O) of O x => x | ((S x) as b) (S y) => (plus (plus b x) y) @@ -258,54 +254,54 @@ Check end. -Check Cases O (S O) of +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. -Check [l:(List nat)]<(List nat)>Cases l of +Type [l:(List nat)]<(List nat)>Cases l of Nil => (Nil nat) | (Cons a l) => l end. -Check [l:(List nat)] Cases l of +Type [l:(List nat)] Cases l of Nil => (Nil nat) | (Cons a l) => l end. -Check <nat>Cases (Nil nat) of +Type <nat>Cases (Nil nat) of Nil =>O | (Cons a l) => (S a) end. -Check Cases (Nil nat) of +Type Cases (Nil nat) of Nil =>O | (Cons a l) => (S a) end. -Check <(List nat)>Cases (Nil nat) of +Type <(List nat)>Cases (Nil nat) of (Cons a l) => l | x => x end. -Check Cases (Nil nat) of +Type Cases (Nil nat) of (Cons a l) => l | x => x end. -Check <(List nat)>Cases (Nil nat) of +Type <(List nat)>Cases (Nil nat) of Nil => (Nil nat) | (Cons a l) => l end. -Check Cases (Nil nat) of +Type Cases (Nil nat) of Nil => (Nil nat) | (Cons a l) => l end. -Check +Type <nat>Cases O of O => O | (S x) => <nat>Cases (Nil nat) of @@ -314,7 +310,7 @@ Check end end. -Check +Type Cases O of O => O | (S x) => Cases (Nil nat) of @@ -323,7 +319,7 @@ Check end end. -Check +Type [y:nat]Cases y of O => O | (S x) => Cases (Nil nat) of @@ -333,7 +329,7 @@ Check end. -Check +Type <nat>Cases O (Nil nat) of O x => O | (S x) Nil => x @@ -342,120 +338,125 @@ Check -Check [n:nat][l:(listn n)]<[_:nat]nat>Cases l of +Type [n:nat][l:(listn n)]<[_:nat]nat>Cases l of niln => O | x => O end. -Check [n:nat][l:(listn n)] +Type [n:nat][l:(listn n)] Cases l of niln => O | x => O end. -Check <[_:nat]nat>Cases niln of +Type <[_:nat]nat>Cases niln of niln => O | x => O end. -Check Cases niln of +Type Cases niln of niln => O | x => O end. -Check <[_:nat]nat>Cases niln of - niln => O - | (consn n a l) => a - end. -Check Cases niln of +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 + end. + + +Type <[n:nat][_:(listn n)]nat>Cases niln of + (consn m _ niln) => m + | _ => (S O) end. -Check [n:nat][x:nat][l:(listn n)]<[_:nat]nat>Cases x l of + +Type [n:nat][x:nat][l:(listn n)]<[_:nat]nat>Cases x l of O niln => O | y x => O end. -Check <[_:nat]nat>Cases O niln of +Type <[_:nat]nat>Cases O niln of O niln => O | y x => O end. -Check <[_:nat]nat>Cases niln O of +Type <[_:nat]nat>Cases niln O of niln O => O | y x => O end. -Check Cases niln O of +Type Cases niln O of niln O => O | y x => O end. -Check <[_:nat][_:nat]nat>Cases niln niln of +Type <[_:nat][_:nat]nat>Cases niln niln of niln niln => O | x y => O end. -Check Cases niln niln of +Type Cases niln niln of niln niln => O | x y => O end. -Check <[_,_,_:nat]nat>Cases niln niln niln of +Type <[_,_,_:nat]nat>Cases niln niln niln of niln niln niln => O | x y z => O end. -Check Cases niln niln niln of +Type Cases niln niln niln of niln niln niln => O | x y z => O end. -Check <[_:nat]nat>Cases (niln) of +Type <[_:nat]nat>Cases (niln) of niln => O | (consn n a l) => O end. -Check Cases (niln) of +Type Cases (niln) of niln => O | (consn n a l) => O end. -Check <[_:nat][_:nat]nat>Cases niln niln of +Type <[_:nat][_:nat]nat>Cases niln niln of niln niln => O | niln (consn n a l) => n | (consn n a l) x => a end. -Check Cases niln niln of +Type Cases niln niln of niln niln => O | niln (consn n a l) => n | (consn n a l) x => a end. -Check [n:nat][l:(listn n)]<[_:nat]nat>Cases l of +Type [n:nat][l:(listn n)]<[_:nat]nat>Cases l of niln => O | x => O end. -Check [c:nat;s:bool] +Type [c:nat;s:bool] <[_:nat;_:bool]nat>Cases c s of | O _ => O | _ _ => c end. -Check [c:nat;s:bool] +Type [c:nat;s:bool] <[_:nat;_:bool]nat>Cases c s of | O _ => O | (S _) _ => c @@ -465,13 +466,13 @@ Check [c:nat;s:bool] (* Rows of pattern variables: some tricky cases *) Axiom P:nat->Prop; f:(n:nat)(P n). -Check [i:nat] +Type [i:nat] <[_:bool;n:nat](P n)>Cases true i of | true k => (f k) | _ k => (f k) end. -Check [i:nat] +Type [i:nat] <[n:nat;_:bool](P n)>Cases i true of | k true => (f k) | k _ => (f k) @@ -480,24 +481,24 @@ Check [i:nat] (* 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) *) -Check <[n]Cases n of O => bool | (S _) => nat end>Cases O of +Type <[n]Cases n of O => bool | (S _) => nat end>Cases O of O => true | (S _) => O end. -Check [n:nat][l:(listn n)]Cases l of +Type [n:nat][l:(listn n)]Cases l of niln => O | x => O end. -Check [n:nat][l:(listn n)]<[_:nat]nat>Cases l of +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. -Check [n:nat][l:(listn n)]Cases l of +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) @@ -505,40 +506,40 @@ Check [n:nat][l:(listn n)]Cases l of -Check [n:nat][l:(listn n)]<[_:nat]nat>Cases l of +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. -Check [n:nat][l:(listn n)]Cases l of +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. -Check [A:Set][n:nat][l:(Listn A n)]<[_:nat]nat>Cases l of +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. -Check [A:Set][n:nat][l:(Listn A n)]Cases l of +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. (* -Check [A:Set][n:nat][l:(Listn A n)] +Type [A:Set][n:nat][l:(Listn A n)] <[_:nat](Listn A O)>Cases l of (Niln as b) => b | (Consn n a (Niln as b))=> (Niln A) | (Consn n a (Consn m b l)) => (Niln A) end. -Check [A:Set][n:nat][l:(Listn A n)] +Type [A:Set][n:nat][l:(Listn A n)] Cases l of (Niln as b) => b | (Consn n a (Niln as b))=> (Niln A) @@ -546,7 +547,7 @@ Check [A:Set][n:nat][l:(Listn A n)] end. *) (******** This example rises an error unconstrained_variables! -Check [A:Set][n:nat][l:(Listn A n)] +Type [A:Set][n:nat][l:(Listn A n)] Cases l of (Niln as b) => (Consn A O O b) | ((Consn n a Niln) as L) => L @@ -555,7 +556,7 @@ Check [A:Set][n:nat][l:(Listn A n)] **********) (* To test tratement of as-patterns in depth *) -Check [A:Set] [l:(List A)] +Type [A:Set] [l:(List A)] Cases l of (Nil as b) => (Nil A) | ((Cons a Nil) as L) => L @@ -563,66 +564,66 @@ Check [A:Set] [l:(List A)] end. -Check [n:nat][l:(listn n)] +Type [n:nat][l:(listn n)] <[_:nat](listn n)>Cases l of niln => l | (consn n a c) => l end. -Check [n:nat][l:(listn n)] +Type [n:nat][l:(listn n)] Cases l of niln => l | (consn n a c) => l end. -Check [n:nat][l:(listn n)] +Type [n:nat][l:(listn n)] <[_:nat](listn n)>Cases l of (niln as b) => l | _ => l end. -Check [n:nat][l:(listn n)] +Type [n:nat][l:(listn n)] Cases l of (niln as b) => l | _ => l end. -Check [n:nat][l:(listn n)] +Type [n:nat][l:(listn n)] <[_:nat](listn n)>Cases l of (niln as b) => l | x => l end. -Check [A:Set][n:nat][l:(Listn A n)] +Type [A:Set][n:nat][l:(Listn A n)] Cases l of (Niln as b) => l | _ => l end. -Check [A:Set][n:nat][l:(Listn A n)] +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. -Check [A:Set][n:nat][l:(Listn A n)] +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. -Check [A:Set][n:nat][l:(Listn A n)] +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. -Check [A:Set][n:nat][l:(Listn A n)] +Type [A:Set][n:nat][l:(Listn A n)] Cases l of (Niln as b) => l | (Consn n a (Niln as b)) => l @@ -630,157 +631,157 @@ Check [A:Set][n:nat][l:(Listn A n)] end. -Check <[_:nat]nat>Cases (niln) of +Type <[_:nat]nat>Cases (niln) of niln => O | (consn n a niln) => O | (consn n a (consn m b l)) => (plus n m) end. -Check Cases (niln) of +Type Cases (niln) of niln => O | (consn n a niln) => O | (consn n a (consn m b l)) => (plus n m) end. -Check <[_,_:nat]nat>Cases (LeO O) of +Type <[_,_:nat]nat>Cases (LeO O) of (LeO x) => x | (LeS n m h) => (plus n m) end. -Check Cases (LeO O) of +Type Cases (LeO O) of (LeO x) => x | (LeS n m h) => (plus n m) end. -Check [n:nat][l:(Listn nat n)] +Type [n:nat][l:(Listn nat n)] <[_:nat]nat>Cases l of Niln => O | (Consn n a l) => O end. -Check [n:nat][l:(Listn nat n)] +Type [n:nat][l:(Listn nat n)] Cases l of Niln => O | (Consn n a l) => O end. -Check Cases (Niln nat) of +Type Cases (Niln nat) of Niln => O | (Consn n a l) => O end. -Check <[_:nat]nat>Cases (LE_n O) of +Type <[_:nat]nat>Cases (LE_n O) of LE_n => O | (LE_S m h) => O end. -Check Cases (LE_n O) of +Type Cases (LE_n O) of LE_n => O | (LE_S m h) => O end. -Check Cases (LE_n O) of +Type Cases (LE_n O) of LE_n => O | (LE_S m h) => O end. -Check <[_:nat]nat>Cases (niln ) of +Type <[_:nat]nat>Cases (niln ) of niln => O | (consn n a niln) => n | (consn n a (consn m b l)) => (plus n m) end. -Check Cases (niln ) of +Type Cases (niln ) of niln => O | (consn n a niln) => n | (consn n a (consn m b l)) => (plus n m) end. -Check <[_:nat]nat>Cases (Niln nat) of +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. -Check Cases (Niln nat) of +Type Cases (Niln nat) of Niln => O | (Consn n a Niln) => n | (Consn n a (Consn m b l)) => (plus n m) end. -Check <[_,_:nat]nat>Cases (LeO O) of +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. -Check Cases (LeO O) of +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. -Check <[_,_:nat]nat>Cases (LeO O) of +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. -Check Cases (LeO O) of +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. -Check [n,m:nat][h:(Le n m)] +Type [n,m:nat][h:(Le n m)] <[_,_:nat]nat>Cases h of (LeO x) => x | x => O end. -Check [n,m:nat][h:(Le n m)] +Type [n,m:nat][h:(Le n m)] Cases h of (LeO x) => x | x => O end. -Check [n,m:nat][h:(Le n m)] +Type [n,m:nat][h:(Le n m)] <[_,_:nat]nat>Cases h of (LeS n m h) => n | x => O end. -Check [n,m:nat][h:(Le n m)] +Type [n,m:nat][h:(Le n m)] Cases h of (LeS n m h) => n | x => O end. -Check [n,m:nat][h:(Le n m)] +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. -Check [n,m:nat][h:(Le n m)] +Type [n,m:nat][h:(Le n m)] Cases h of (LeO n) => (O,n) |(LeS n m _) => ((S n),(S m)) @@ -854,93 +855,90 @@ Definition length3 := end. -Check <[_,_:nat]nat>Cases (LeO O) of +Type <[_,_:nat]nat>Cases (LeO O) of (LeS n m h) =>(plus n m) | x => O end. -Check Cases (LeO O) of +Type Cases (LeO O) of (LeS n m h) =>(plus n m) | x => O end. -Check [n,m:nat][h:(Le n m)]<[_,_:nat]nat>Cases h of +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. -Check [n,m:nat][h:(Le n m)]Cases h of +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. -Check <[_,_:nat]nat>Cases (LeO O) of +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. -Check Cases (LeO O) of +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. -Check <[_:nat]nat>Cases (LE_n O) of +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. -Check Cases (LE_n O) of +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. -Check [n,m:nat][h:(Le n m)]<[_,_:nat]nat>Cases h of - x => x - end. - Check [n,m:nat][h:(Le n m)] Cases h of +Type [n,m:nat][h:(Le n m)] Cases h of x => x end. -Check [n,m:nat][h:(Le n m)]<[_,_:nat]nat>Cases h of +Type [n,m:nat][h:(Le n m)]<[_,_:nat]nat>Cases h of (LeO n) => n | x => O end. -Check [n,m:nat][h:(Le n m)] Cases h of +Type [n,m:nat][h:(Le n m)] Cases h of (LeO n) => n | x => O end. -Check [n:nat]<[_:nat]nat->nat>Cases niln of +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. -Check [n:nat] Cases niln of +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. -Check [A:Set][n:nat][l:(Listn A n)] +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. -Check [A:Set][n:nat][l:(Listn A n)] +Type [A:Set][n:nat][l:(Listn A n)] Cases l of Niln => [_:nat]O | (Consn n a Niln) => [_:nat] n @@ -948,7 +946,7 @@ Check [A:Set][n:nat][l:(Listn A n)] end. (* Alsos tests for multiple _ patterns *) -Check [A:Set][n:nat][l:(Listn A n)] +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 @@ -956,37 +954,37 @@ Check [A:Set][n:nat][l:(Listn A n)] (** Horrible error message! -Check [A:Set][n:nat][l:(Listn A n)] +Type [A:Set][n:nat][l:(Listn A n)] Cases l of (Niln as b) => b | ((Consn _ _ _ ) as b)=> b end. ******) -Check <[n:nat](listn n)>Cases niln of +Type <[n:nat](listn n)>Cases niln of (niln as b) => b | ((consn _ _ _ ) as b)=> b end. -Check <[n:nat](listn n)>Cases niln of +Type <[n:nat](listn n)>Cases niln of (niln as b) => b | x => x end. -Check [n,m:nat][h:(LE n m)]<[_:nat]nat->nat>Cases h of +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. -Check [n,m:nat][h:(LE n m)]Cases h of +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. -Check [n,m:nat][h:(LE n m)] +Type [n,m:nat][h:(LE n m)] <[_:nat]nat>Cases h of LE_n => n | (LE_S m LE_n ) => (plus n m) @@ -996,7 +994,7 @@ Check [n,m:nat][h:(LE n m)] -Check [n,m:nat][h:(LE n m)] +Type [n,m:nat][h:(LE n m)] Cases h of LE_n => n | (LE_S m LE_n ) => (plus n m) @@ -1005,52 +1003,52 @@ Check [n,m:nat][h:(LE n m)] end. -Check [n,m:nat][h:(LE n m)]<[_:nat]nat>Cases h of +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. -Check [n,m:nat][h:(LE n m)]Cases h of +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. -Check [n,m:nat] +Type [n,m:nat] <[_,_:nat]nat>Cases (LeO O) of (LeS n m h) =>(plus n m) | x => O end. -Check [n,m:nat] +Type [n,m:nat] Cases (LeO O) of (LeS n m h) =>(plus n m) | x => O end. Parameter test : (n:nat){(le O n)}+{False}. -Check [n:nat]<nat>Cases (test n) of +Type [n:nat]<nat>Cases (test n) of (left _) => O | _ => O end. -Check [n:nat] <nat> Cases (test n) of +Type [n:nat] <nat> Cases (test n) of (left _) => O | _ => O end. -Check [n:nat]Cases (test n) of +Type [n:nat]Cases (test n) of (left _) => O | _ => O end. Parameter compare : (n,m:nat)({(lt n m)}+{n=m})+{(gt n m)}. -Check <nat>Cases (compare O O) of +Type <nat>Cases (compare O O) of (* k<i *) (inleft (left _)) => O | (* k=i *) (inleft _) => O | (* k>i *) (inright _) => O end. -Check Cases (compare O O) of +Type Cases (compare O O) of (* k<i *) (inleft (left _)) => O | (* k=i *) (inleft _) => O | (* k>i *) (inright _) => O end. @@ -1062,50 +1060,38 @@ scons : (P:nat->A->Prop)(a:A)(P O a)->(SStream A [n:nat](P (S n)))->(SStream A P). Parameter B : Set. -Check +Type [P:nat->B->Prop][x:(SStream B P)]<[_:nat->B->Prop]B>Cases x of (scons _ a _ _) => a end. -Check +Type [P:nat->B->Prop][x:(SStream B P)] Cases x of (scons _ a _ _) => a end. -Check <nat*nat>Cases (O,O) of (x,y) => ((S x),(S y)) end. -Check <nat*nat>Cases (O,O) of ((x as b), y) => ((S x),(S y)) end. -Check <nat*nat>Cases (O,O) of (pair x y) => ((S x),(S y)) 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. -Check Cases (O,O) of (x,y) => ((S x),(S y)) end. -Check Cases (O,O) of ((x as b), y) => ((S x),(S y)) end. -Check Cases (O,O) of (pair 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. Parameter concat : (A:Set)(List A) ->(List A) ->(List A). -Check <(List nat)>Cases (Nil nat) (Nil nat) of +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. -Check Cases (Nil nat) (Nil nat) of +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. -Definition NIL := (Nil nat). -Definition CONS := (Cons nat). -Check <(List nat)>Cases (Nil nat) of - NIL => NIL - | _ => NIL - end. - -Check Cases (Nil nat) of - NIL => NIL - | _ => NIL - end. - Inductive redexes : Set := VAR : nat -> redexes @@ -1121,30 +1107,30 @@ Fixpoint regular [U:redexes] : Prop := <Prop>Cases U of end. -Check [n:nat]Cases n of O => O | (S ((S n) as V)) => V | _ => O end. +Type [n:nat]Cases n of O => O | (S ((S n) as V)) => V | _ => O end. Reset concat. Parameter concat :(n:nat) (listn n) -> (m:nat) (listn m)-> (listn (plus n m)). -Check [n:nat][l:(listn n)][m:nat][l':(listn 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. -Check [x,y,z:nat] +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. -Check [h:False]<False>Cases h of end. +Type [h:False]<False>Cases h of end. -Check [h:False]<True>Cases h of end. +Type [h:False]<True>Cases h of end. Definition is_zero := [n:nat]Cases n of O => True | _ => False end. -Check [n:nat][h:O=(S n)]<[n:nat](is_zero n)>Cases h of refl_equal => I end. +Type [n:nat][h:O=(S n)]<[n:nat](is_zero n)>Cases h of refl_equal => I end. Definition disc : (n:nat)O=(S n)->False := [n:nat][h:O=(S n)] @@ -1160,13 +1146,13 @@ Definition nlength3 := [n:nat] [l: (listn n)] (* == Testing strategy elimintation predicate synthesis == *) Section titi. Variable h:False. -Check Cases O of +Type Cases O of O => O | _ => (Except h) end. End titi. -Check Cases niln of +Type Cases niln of (consn _ a niln) => a | (consn n _ x) => O | niln => O @@ -1179,7 +1165,7 @@ Inductive TS : wsort->Set := id :(TS ws) | lift:(TS ws)->(TS ws). -Check [b:wsort][M:(TS b)][N:(TS b)] +Type [b:wsort][M:(TS b)][N:(TS b)] Cases M N of (lift M1) id => False | _ _ => True @@ -1187,21 +1173,6 @@ Check [b:wsort][M:(TS b)][N:(TS b)] -(* Testing eta-expansion of elimination predicate *) - -Section NATIND2. -Variable P : nat -> Type. -Variable H0 : (P O). -Variable H1 : (P (S O)). -Variable H2 : (n:nat)(P n)->(P (S (S n))). -Fixpoint nat_ind2 [n:nat] : (P n) := - <P>Cases n of - O => H0 - | (S O) => H1 - | (S (S n)) => (H2 n (nat_ind2 n)) - end. -End NATIND2. - (* ===================================================================== *) (* To test pattern matching over a non-dependent inductive type, but *) (* having constructors with some arguments that depend on others *) @@ -1216,7 +1187,7 @@ Mutual Inductive TERM : Type := Parameter t1, t2:TERM. -Check Cases t1 t2 of +Type Cases t1 t2 of var var => True | (oper op1 l1) (oper op2 l2) => False @@ -1231,7 +1202,7 @@ Parameter n:nat. Definition eq_prf := (EXT m | n=m). Parameter p:eq_prf . -Check Cases p of +Type Cases p of (exT_intro c eqc) => Cases (eq_nat_dec c n) of (right _) => (refl_equal ? n) @@ -1249,7 +1220,7 @@ Parameter exist_U2:(N:nat)(ge N (S (S O)))-> /\(ordre_total n m) /\(lt O n)/\(lt n N)}. -Check [N:nat](Cases (N_cla N) of +Type [N:nat](Cases (N_cla N) of (inright H)=>(Cases (exist_U2 N H) of (exist a b)=>a end) @@ -1263,17 +1234,10 @@ Check [N:nat](Cases (N_cla N) of (* Nested patterns *) (* ============================================== *) - -Check <[n:nat]n=n>Cases O of - O => (refl_equal nat O) - | m => (refl_equal nat m) -end. - - (* == To test that terms named with AS are correctly absolutized before substitution in rhs == *) -Check [n:nat]<[n:nat]nat>Cases (n) of +Type [n:nat]<[n:nat]nat>Cases (n) of O => O | (S O) => O | ((S (S n1)) as N) => N @@ -1281,52 +1245,39 @@ Check [n:nat]<[n:nat]nat>Cases (n) of (* ========= *) -Check <[n:nat][_:(listn n)]Prop>Cases niln of +Type <[n:nat][_:(listn n)]Prop>Cases niln of niln => True | (consn (S O) _ _) => False | _ => True end. -Check <[n:nat][_:(listn n)]Prop>Cases niln of +Type <[n:nat][_:(listn n)]Prop>Cases niln of niln => True | (consn (S (S O)) _ _) => False | _ => True end. -Check <[n,m:nat][h:(Le n m)]nat>Cases (LeO O) of +Type <[n,m:nat][h:(Le n m)]nat>Cases (LeO O) of (LeO _) => O | (LeS (S x) _ _) => x | _ => (S O) end. -Check <[n,m:nat][h:(Le n m)]nat>Cases (LeO O) of +Type <[n,m:nat][h:(Le n m)]nat>Cases (LeO O) of (LeO _) => O | (LeS (S x) (S y) _) => x | _ => (S O) end. -Check <[n,m:nat][h:(Le n m)]nat>Cases (LeO O) of +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. -Parameter iguales : (n,m:nat)(h:(Le n m))Prop . - -Check <[n,m:nat][h:(Le n m)]Prop>Cases (LeO O) of - (LeO O) => True - | (LeS (S x) (S y) H) => (iguales (S x) (S y) H) - | _ => False end. - -Check <[n,m:nat][h:(Le n m)]Prop>Cases (LeO O) of - (LeO O) => True - | (LeS (S x) O H) => (iguales (S x) O H) - | _ => False 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). -Check +Type [n:nat] <[n:nat]n=O\/~n=O>Cases n of O => (or_introl ? ~O=O (refl_equal ? O)) @@ -1334,16 +1285,6 @@ Check end. -Check -[n:nat] - <[n:nat]n=O\/~n=O>Cases n of - O => (or_introl ? ~O=O (refl_equal ? O)) - | (S O) => (or_intror (S O)=O ? (discr_l O)) - | (S (S x)) => (or_intror (S (S x))=O ? (discr_l (S x))) - - end. - - Fixpoint eqdec [n:nat] : (m:nat) n=m \/ ~n=m := [m:nat] <[n,m:nat] n=m \/ ~n=m>Cases n m of @@ -1385,48 +1326,19 @@ Inductive empty : (n:nat)(listn n)-> Prop := Parameter inv_empty : (n,a:nat)(l:(listn n)) ~(empty (S n) (consn n a l)). -Check +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. -Check -[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 O y) as b) => (or_intror (empty (S n) b) ? (inv_empty n O y)) - | ((consn n a y) as b) => (or_intror (empty (S n) b) ? (inv_empty n a y)) - - end. - -Check -[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 O y) => (or_intror (empty (S n) (consn n O y)) ? - (inv_empty n O y)) - | (consn n a y) => (or_intror (empty (S n) (consn n a y)) ? - (inv_empty n a y)) - - end. - -Check -[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 O a y) as b) => (or_intror (empty (S O) b) ? (inv_empty O a y)) - | ((consn n a y) as b) => (or_intror (empty (S n) b) ? (inv_empty n a y)) - - 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). -Check +Type [n:nat] <[n:nat]n=O\/~n=O>Cases n of O => (or_introl ? ~O=O (refl_equal ? O)) @@ -1434,15 +1346,6 @@ Check end. -Check -[n:nat] - <[n:nat]n=O\/~n=O>Cases n of - O => (or_introl ? ~O=O (refl_equal ? O)) - | (S O) => (or_intror (S O)=O ? (discr_l O)) - | (S (S x)) => (or_intror (S (S x))=O ? (discr_l (S x))) - - end. - Fixpoint eqdec [n:nat] : (m:nat) n=m \/ ~n=m := [m:nat] <[n,m:nat] n=m \/ ~n=m>Cases n m of @@ -1461,23 +1364,6 @@ Fixpoint eqdec [n:nat] : (m:nat) n=m \/ ~n=m := Reset eqdec. Fixpoint eqdec [n:nat] : (m:nat) n=m \/ ~n=m := -[m:nat] - <[n,m:nat] n=m \/ ~n=m>Cases n m of - O O => (or_introl ? ~O=O (refl_equal ? O)) - - | O (S x) => (or_intror O=(S x) ? (discr_r x)) - - | (S x) O => (or_intror ? ~(S x)=O (discr_l x)) - - | ((S x) as N) ((S y) as M) => - <N=M\/~N=M>Cases (eqdec x y) of - (or_introl h) => (or_introl ? ~N=M (f_equal nat nat S x y h)) - | (or_intror h) => (or_intror N=M ? (ff x y h)) - 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)) @@ -1506,7 +1392,7 @@ Inductive Empty [A:Set] : (List A)-> Prop := Parameter inv_Empty : (A:Set)(a:A)(x:(List A)) ~(Empty A (Cons A a x)). -Check +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)) ? @@ -1514,16 +1400,6 @@ Check end. -Check -[A:Set] -[l:(List A)] - <[l:(List A)](Empty A l) \/ ~(Empty A l)>Cases l of - Nil => (or_introl ? ~(Empty A (Nil A)) (intro_Empty A)) - | ((Cons a y) as b) => (or_intror (Empty A b) ? (inv_Empty A a y)) - end. - - - (* ================================================== *) (* Sur les listes *) (* ================================================== *) @@ -1534,41 +1410,13 @@ Inductive empty : (n:nat)(listn n)-> Prop := Parameter inv_empty : (n,a:nat)(l:(listn n)) ~(empty (S n) (consn n a l)). -Check +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. -Check -[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 O y) as b) => (or_intror (empty (S n) b) ? (inv_empty n O y)) - | ((consn n a y) as b) => (or_intror (empty (S n) b) ? (inv_empty n a y)) - - end. - -Check -[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 O y) => (or_intror (empty (S n) (consn n O y)) ? - (inv_empty n O y)) - | (consn n a y) => (or_intror (empty (S n) (consn n a y)) ? - (inv_empty n a y)) - - end. - -Check -[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 O a y) as b) => (or_intror (empty (S O) b) ? (inv_empty O a y)) - | ((consn n a y) as b) => (or_intror (empty (S n) b) ? (inv_empty n a y)) - - end. (* ===================================== *) (* Test parametros: *) (* ===================================== *) @@ -1588,7 +1436,7 @@ 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)). -Check +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) @@ -1597,7 +1445,7 @@ Check end. -Check +Type [x,y:(List nat)] <[x,y:(List nat)](eqlong x y)\/~(eqlong x y)>Cases x y of Nil Nil => V1 @@ -1606,45 +1454,6 @@ Check | (Cons a x) (Cons b y) => (V4 a x b y) end. - - -Parameter nff : (n,m:nat)(x,y:(List nat)) - ~(eqlong x y)-> ~(eqlong (Cons nat n x) (Cons nat m y)). -Parameter inv_r : (n:nat)(x:(List nat)) ~(eqlong (Nil nat) (Cons nat n x)). -Parameter inv_l : (n:nat)(x:(List nat)) ~(eqlong (Cons nat n x) (Nil nat)). - - -Fixpoint eqlongdec [x:(List nat)]: (y:(List nat))(eqlong x y)\/~(eqlong x y) := -[y:(List nat)] - <[x,y:(List nat)](eqlong x y)\/~(eqlong x y)>Cases x y of - Nil Nil => (or_introl ? ~(eqlong (Nil nat) (Nil nat)) eql_nil) - - | Nil ((Cons a x) as L) =>(or_intror (eqlong (Nil nat) L) ? (inv_r a x)) - - | ((Cons a x) as L) Nil => (or_intror (eqlong L (Nil nat)) ? (inv_l a x)) - - | ((Cons a x) as L1) ((Cons b y) as L2) => - <(eqlong L1 L2) \/~(eqlong L1 L2)>Cases (eqlongdec x y) of - (or_introl h) => (or_introl ? ~(eqlong L1 L2) (eql_cons a b x y h)) - | (or_intror h) => (or_intror (eqlong L1 L2) ? (nff a b x y h)) - end - end. - -Check - <[x,y:(List nat)](eqlong x y)\/~(eqlong x y)>Cases (Nil nat) (Nil nat) of - Nil Nil => (or_introl ? ~(eqlong (Nil nat) (Nil nat)) eql_nil) - - | Nil ((Cons a x) as L) =>(or_intror (eqlong (Nil nat) L) ? (inv_r a x)) - - | ((Cons a x) as L) Nil => (or_intror (eqlong L (Nil nat)) ? (inv_l a x)) - - | ((Cons a x) as L1) ((Cons b y) as L2) => - <(eqlong L1 L2) \/~(eqlong L1 L2)>Cases (eqlongdec x y) of - (or_introl h) => (or_introl ? ~(eqlong L1 L2) (eql_cons a b x y h)) - | (or_intror h) => (or_intror (eqlong L1 L2) ? (nff a b x y h)) - end - end. - (* ===================================== *) @@ -1664,7 +1473,7 @@ 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)). -Check +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 @@ -1674,7 +1483,7 @@ Check end. -Check +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 @@ -1728,14 +1537,7 @@ Inductive skel: Type := Parameter Can : skel -> Type. Parameter default_can : (s:skel) (Can s). - -Check [s1,s2:skel] - <[s1,_:skel](Can s1)>Cases s1 s2 of - PROP PROP => (default_can PROP) - | s1 _ => (default_can s1) - end. - -Check [s1,s2:skel] +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)) @@ -1743,23 +1545,13 @@ Check [s1,s2:skel] | PROP _ => (default_can PROP) end. -Check [s1,s2:skel] -<[s1:skel][_:skel](Can s1)>Cases s1 s2 of - PROP PROP => (default_can PROP) -| (PROP as s) _ => (default_can s) -| ((PROD s1 s2) as s) PROP => (default_can s) -| ((PROD s1 s2) as s) _ => (default_can s) -end. - - - (* to test bindings in nested Cases *) (* ================================ *) Inductive Pair : Set := pnil : Pair | pcons : Pair -> Pair -> Pair. -Check [p,q:Pair]Cases p of +Type [p,q:Pair]Cases p of (pcons _ x) => Cases q of (pcons _ (pcons _ x)) => True @@ -1769,7 +1561,7 @@ Check [p,q:Pair]Cases p of end. -Check [p,q:Pair]Cases p of +Type [p,q:Pair]Cases p of (pcons _ x) => Cases q of (pcons _ (pcons _ x)) => @@ -1782,75 +1574,7 @@ Check [p,q:Pair]Cases p of | _ => pnil end. - - - -(* ===================== To test ERRORS =============================== - -Check <[n:nat][_:(listn n)]nat>Cases niln of - (consn m _ niln) => m - | _ => (S O) end. - -Check [F:IFExpr] - <Prop>Cases F of - (IfE (Var _) H I) => True - | (IfE _ _ _) => False - | _ => True - end. - -Check [l:(List nat)]<nat>Cases l of - (Nil nat) =>O - | (Cons a l) => (S a) - end. - - -Definition Berry := [x,y,z:bool] - Cases x y z of - true false _ => O - | false _ true => (S O) - | _ true false => (S (S O)) -end. - -Definition Berry := [x,y,z:bool] - <nat>Cases x y z of - true false _ => O - | false _ true => (S O) - | _ true false => (S (S O)) -end. - - -Inductive MS: Set := X:MS->MS | Y:MS->MS. - -Check [p:MS]<nat>Cases p of (X x) => O end. - - - - - -Check <(List nat)>Cases (Nil nat) of - NIL => NIL - | (CONS _ _) => NIL - - end. - -Check [n:nat] - [l:(listn n)] - <nat>Cases n of - O => O - | (S n) => - <([_:nat]nat)>Cases l of - niln => (S O) - | l' => (length1 (S n) l') - end - end. - -Check <nat>Cases (Nil nat) of - ((Nil_) as b) =>b - |((Cons _ _ _) as d) => d - end. - - -Check +Type [n:nat] [l:(listn (S n))] <[z:nat](listn (pred z))>Cases l of @@ -1862,429 +1586,11 @@ Check end end. -Parameter compare : (n,m:nat)({(lt n m)}+{n=m})+{(gt n m)}. -Check <nat>Cases (compare O O) of - (* k<i *) (left _ _ (left _ _ _)) => O - | (* k=i *) (left _ _ _) => O - | (* k>i *) (right _ _ _) => O end. - - - - - - ========================================== - To test binding !! - -Check [x:nat]<nat> Cases x of ((S x) as b) => (S b) end. -let va=dbize_cci sigma env aa;; - -Check [x:nat]<nat> Cases x of ((S x) as b) => (S b x) end. -let va=dbize_cci sigma env aa;; - - -Check [x:nat]<nat> Cases x of - ((S x) as b) => <nat>Cases x of - x => x - end - end. - -Check [x:nat]<nat> Cases x of - ((S x) as b) => <nat>Cases x of - x => (S b x) - end - end. - -Check [x:nat]<nat> Cases x of (S x) => x end . - -Check [x:nat]<nat> Cases x of ((S y x) as b) => (S b x) end. - -Check <nat> Cases (plus O O) of ((S n) as b) => b end - - -======================================= *) - - - -(* -------------------------------------------------------------------- *) -(* Example to test patterns matching on dependent families *) (* This exemple extracted from the developement done by Nacira Chabane *) -(* (equipe Paris 6) *) -(* -------------------------------------------------------------------- *) - - -Require Prelude. -Require Logic_TypeSyntax. -Require Logic_Type. - - -Section Orderings. - Variable U: Type. - - Definition Relation := U -> U -> Prop. - - Variable R: Relation. - - Definition Reflexive : Prop := (x: U) (R x x). - - Definition Transitive : Prop := (x,y,z: U) (R x y) -> (R y z) -> (R x z). - - Definition Symmetric : Prop := (x,y: U) (R x y) -> (R y x). - - Definition Antisymmetric : Prop := - (x,y: U) (R x y) -> (R y x) -> x==y. - - Definition contains : Relation -> Relation -> Prop := - [R,R': Relation] (x,y: U) (R' x y) -> (R x y). - Definition same_relation : Relation -> Relation -> Prop := - [R,R': Relation] (contains R R') /\ (contains R' R). -Inductive Equivalence : Prop := - Build_Equivalence: - Reflexive -> Transitive -> Symmetric -> Equivalence. - - Inductive PER : Prop := - Build_PER: Symmetric -> Transitive -> PER. - -End Orderings. - -(***** Setoid *******) - -Inductive Setoid : Type - := Build_Setoid : (S:Type)(R:(Relation S))(Equivalence ? R) -> Setoid. - -Definition elem := [A:Setoid] - <Type>Match A with [S:?][R:?][e:?]S end. - -Grammar command command1 := - elem [ "|" command0($s) "|"] -> [ <<(elem $s)>>]. - -Definition equal := [A:Setoid] - <[s:Setoid](Relation |s|)>Match A with [S:?][R:?][e:?]R end. - - -Grammar command command1 := - equal [ command0($c) "=" "%" "S" command0($c2) ] -> - [ <<(equal ? $c $c2)>>]. - - -Axiom prf_equiv : (A:Setoid)(Equivalence |A| (equal A)). -Axiom prf_refl : (A:Setoid)(Reflexive |A| (equal A)). -Axiom prf_sym : (A:Setoid)(Symmetric |A| (equal A)). -Axiom prf_trans : (A:Setoid)(Transitive |A| (equal A)). - -Section Maps. -Variables A,B: Setoid. - -Definition Map_law := [f:|A|->|B|] - (x,y:|A|) x =%S y -> (f x) =%S (f y). - -Inductive Map : Type := - Build_Map : (f:|A|->|B|)(p:(Map_law f))Map. - -Definition explicit_ap := [m:Map] <|A|->|B|>Match m with - [f:?][p:?]f end. - -Axiom pres : (m:Map)(Map_law (explicit_ap m)). - -Definition ext := [f,g:Map] - (x:|A|) (explicit_ap f x) =%S (explicit_ap g x). - -Axiom Equiv_map_eq : (Equivalence Map ext). - -Definition Map_setoid := (Build_Setoid Map ext Equiv_map_eq). - -End Maps. - -Syntactic Definition ap := (explicit_ap ? ?). - -Grammar command command8 := - map_setoid [ command7($c1) "=>" command8($c2) ] - -> [ <<(Map_setoid $c1 $c2)>>]. - - -Definition ap2 := [A,B,C:Setoid][f:|(A=>(B=>C))|][a:|A|] (ap (ap f a)). - - - -(***** posint ******) - -Inductive posint : Type - := Z : posint | Suc : posint -> posint. - -Require Logic_Type. - -Axiom f_equal : (A,B:Type)(f:A->B)(x,y:A) x==y -> (f x)==(f y). -Axiom eq_Suc : (n,m:posint) n==m -> (Suc n)==(Suc m). - -(* The predecessor function *) - -Definition pred : posint->posint - := [n:posint](<posint>Case n of (* Z *) Z - (* Suc u *) [u:posint]u end). - -Axiom pred_Sucn : (m:posint) m==(pred (Suc m)). -Axiom eq_add_Suc : (n,m:posint) (Suc n)==(Suc m) -> n==m. -Axiom not_eq_Suc : (n,m:posint) ~(n==m) -> ~((Suc n)==(Suc m)). - - -Definition IsSuc : posint->Prop - := [n:posint](<Prop>Case n of (* Z *) False - (* Suc p *) [p:posint]True end). -Definition IsZero :posint->Prop := - [n:posint]<Prop>Match n with - True - [p:posint][H:Prop]False end. - -Axiom Z_Suc : (n:posint) ~(Z==(Suc n)). -Axiom Suc_Z: (n:posint) ~(Suc n)==Z. -Axiom n_Sucn : (n:posint) ~(n==(Suc n)). -Axiom Sucn_n : (n:posint) ~(Suc n)==n. -Axiom eqT_symt : (a,b:posint) ~(a==b)->~(b==a). - - -(******* Dsetoid *****) - -Definition Decidable :=[A:Type][R:(Relation A)] - (x,y:A)(R x y) \/ ~(R x y). - - -Record DSetoid : Type := -{Set_of : Setoid; - prf_decid : (Decidable |Set_of| (equal Set_of))}. - -(* example de Dsetoide d'entiers *) - - -Axiom eqT_equiv : (Equivalence posint (eqT posint)). -Axiom Eq_posint_deci : (Decidable posint (eqT posint)). - -(* Dsetoide des posint*) - -Definition Set_of_posint := (Build_Setoid posint (eqT posint) eqT_equiv). - -Definition Dposint := (Build_DSetoid Set_of_posint Eq_posint_deci). - - - -(**************************************) - - -(* Definition des signatures *) -(* une signature est un ensemble d'operateurs muni - de l'arite de chaque operateur *) - - -Section Sig. - -Record Signature :Type := -{Sigma : DSetoid; - Arity : (Map (Set_of Sigma) (Set_of Dposint))}. - -Variable S:Signature. - - - -Variable Var : DSetoid. - -Mutual Inductive TERM : Type := - var : |(Set_of Var)|->TERM - | oper : (op: |(Set_of (Sigma S))|) (LTERM (ap (Arity S) op)) -> TERM -with - LTERM : posint -> Type := - nil : (LTERM Z) - | cons : TERM -> (n:posint)(LTERM n) -> (LTERM (Suc n)). - - - -(* -------------------------------------------------------------------- *) -(* Examples *) -(* -------------------------------------------------------------------- *) - - -Parameter t1,t2: TERM. - -Check - Cases t1 t2 of - (var v1) (var v2) => True - - | (oper op1 l1) (oper op2 l2) => False - | _ _ => False - end. - - - -Parameter n2:posint. -Parameter l1, l2:(LTERM n2). - -Check - Cases l1 l2 of - nil nil => True - | (cons v m y) nil => False - | _ _ => False -end. - - -Check Cases l1 l2 of - nil nil => True - | (cons u n x) (cons v m y) =>False - | _ _ => False -end. - - - -Fixpoint equalT [t1:TERM]:TERM->Prop := -[t2:TERM] - Cases t1 t2 of - (var v1) (var v2) => True - | (oper op1 l1) (oper op2 l2) => False - | _ _ => False - end - -with EqListT [n1:posint;l1:(LTERM n1)]: (n2:posint)(LTERM n2)->Prop := -[n2:posint][l2:(LTERM n2)] - Cases l1 l2 of - nil nil => True - | (cons t1 n1' l1') (cons t2 n2' l2') => False - | _ _ => False -end. - - -Reset equalT. -Reset EqListT. -(* ------------------------------------------------------------------*) -(* Initial exemple (without patterns) *) -(*-------------------------------------------------------------------*) - -Fixpoint equalT [t1:TERM]:TERM->Prop := -<TERM->Prop>Case t1 of - (*var*) [v1:|(Set_of Var)|][t2:TERM] - <Prop>Case t2 of - (*var*)[v2:|(Set_of Var)|] (v1 =%S v2) - (*oper*)[op2:|(Set_of (Sigma S))|][_:(LTERM (ap (Arity S) op2))]False - end - (*oper*)[op1:|(Set_of (Sigma S))|] - [l1:(LTERM (ap (Arity S) op1))][t2:TERM] - <Prop>Case t2 of - (*var*)[v2:|(Set_of Var)|]False - (*oper*)[op2:|(Set_of (Sigma S))|] - [l2:(LTERM (ap (Arity S) op2))] - ((op1=%S op2)/\ (EqListT (ap (Arity S) op1) l1 (ap (Arity S) op2) l2)) - end -end -with EqListT [n1:posint;l1:(LTERM n1)]: (n2:posint)(LTERM n2)->Prop := -<[_:posint](n2:posint)(LTERM n2)->Prop>Case l1 of - (*nil*) [n2:posint][l2:(LTERM n2)] - <[_:posint]Prop>Case l2 of - (*nil*)True - (*cons*)[t2:TERM][n2':posint][l2':(LTERM n2')]False - end - (*cons*)[t1:TERM][n1':posint][l1':(LTERM n1')] - [n2:posint][l2:(LTERM n2)] - <[_:posint]Prop>Case l2 of - (*nil*) False - (*cons*)[t2:TERM][n2':posint][l2':(LTERM n2')] - ((equalT t1 t2) /\ (EqListT n1' l1' n2' l2')) - end -end. - - -(* ---------------------------------------------------------------- *) -(* Version with simple patterns *) -(* ---------------------------------------------------------------- *) -Reset equalT. - -Fixpoint equalT [t1:TERM]:TERM->Prop := -Cases t1 of - (var v1) => [t2:TERM] - Cases t2 of - (var v2) => (v1 =%S v2) - | (oper op2 _) =>False - end -| (oper op1 l1) => [t2:TERM] - Cases t2 of - (var _) => False - | (oper op2 l2) => (op1=%S op2) - /\ (EqListT (ap (Arity S) op1) l1 (ap (Arity S) op2) l2) - end -end -with EqListT [n1:posint;l1:(LTERM n1)]: (n2:posint)(LTERM n2)->Prop := -<[_:posint](n2:posint)(LTERM n2)->Prop>Cases l1 of - nil => [n2:posint][l2:(LTERM n2)] - Cases l2 of - nil => True - | _ => False - end -| (cons t1 n1' l1') => [n2:posint][l2:(LTERM n2)] - Cases l2 of - nil =>False - | (cons t2 n2' l2') => (equalT t1 t2) - /\ (EqListT n1' l1' n2' l2') - end -end. - - -Reset equalT. - -Fixpoint equalT [t1:TERM]:TERM->Prop := -Cases t1 of - (var v1) => [t2:TERM] - Cases t2 of - (var v2) => (v1 =%S v2) - | (oper op2 _) =>False - end -| (oper op1 l1) => [t2:TERM] - Cases t2 of - (var _) => False - | (oper op2 l2) => (op1=%S op2) - /\ (EqListT (ap (Arity S) op1) l1 (ap (Arity S) op2) l2) - end -end -with EqListT [n1:posint;l1:(LTERM n1)]: (n2:posint)(LTERM n2)->Prop := -[n2:posint][l2:(LTERM n2)] -Cases l1 of - nil => - Cases l2 of - nil => True - | _ => False - end -| (cons t1 n1' l1') => Cases l2 of - nil =>False - | (cons t2 n2' l2') => (equalT t1 t2) - /\ (EqListT n1' l1' n2' l2') - end -end. - -(* ---------------------------------------------------------------- *) -(* Version with multiple patterns *) -(* ---------------------------------------------------------------- *) -Reset equalT. - -Fixpoint equalT [t1:TERM]:TERM->Prop := -[t2:TERM] - Cases t1 t2 of - (var v1) (var v2) => (v1 =%S v2) - - | (oper op1 l1) (oper op2 l2) => - (op1=%S op2) /\ (EqListT (ap (Arity S) op1) l1 (ap (Arity S) op2) l2) - - | _ _ => False - end - -with EqListT [n1:posint;l1:(LTERM n1)]: (n2:posint)(LTERM n2)->Prop := -[n2:posint][l2:(LTERM n2)] - Cases l1 l2 of - nil nil => True - | (cons t1 n1' l1') (cons t2 n2' l2') => (equalT t1 t2) - /\ (EqListT n1' l1' n2' l2') - | _ _ => False -end. - - -(* ------------------------------------------------------------------ *) -End Sig. (* Test de la syntaxe avec nombres *) Require Arith. -Check [n]Cases n of 2 => true | _ => false end. +Type [n]Cases n of 2 => true | _ => false end. Require ZArith. -Check [n]Cases n of `0` => true | _ => false end. +Type [n]Cases n of `0` => true | _ => false end. diff --git a/test-suite/success/CasesDep.v b/test-suite/success/CasesDep.v new file mode 100644 index 000000000..f882eecd8 --- /dev/null +++ b/test-suite/success/CasesDep.v @@ -0,0 +1,376 @@ + +(* -------------------------------------------------------------------- *) +(* Example to test patterns matching on dependent families *) (* This exemple extracted from the developement done by Nacira Chabane *) +(* (equipe Paris 6) *) +(* -------------------------------------------------------------------- *) + + +Require Prelude. +Require Logic_TypeSyntax. +Require Logic_Type. + + +Section Orderings. + Variable U: Type. + + Definition Relation := U -> U -> Prop. + + Variable R: Relation. + + Definition Reflexive : Prop := (x: U) (R x x). + + Definition Transitive : Prop := (x,y,z: U) (R x y) -> (R y z) -> (R x z). + + Definition Symmetric : Prop := (x,y: U) (R x y) -> (R y x). + + Definition Antisymmetric : Prop := + (x,y: U) (R x y) -> (R y x) -> x==y. + + Definition contains : Relation -> Relation -> Prop := + [R,R': Relation] (x,y: U) (R' x y) -> (R x y). + Definition same_relation : Relation -> Relation -> Prop := + [R,R': Relation] (contains R R') /\ (contains R' R). +Inductive Equivalence : Prop := + Build_Equivalence: + Reflexive -> Transitive -> Symmetric -> Equivalence. + + Inductive PER : Prop := + Build_PER: Symmetric -> Transitive -> PER. + +End Orderings. + +(***** Setoid *******) + +Inductive Setoid : Type + := Build_Setoid : (S:Type)(R:(Relation S))(Equivalence ? R) -> Setoid. + +Definition elem := [A:Setoid] + <Type>Match A with [S:?][R:?][e:?]S end. + +Grammar command command1 := + elem [ "|" command0($s) "|"] -> [ <<(elem $s)>>]. + +Definition equal := [A:Setoid] + <[s:Setoid](Relation |s|)>Match A with [S:?][R:?][e:?]R end. + + +Grammar command command1 := + equal [ command0($c) "=" "%" "S" command0($c2) ] -> + [ <<(equal ? $c $c2)>>]. + + +Axiom prf_equiv : (A:Setoid)(Equivalence |A| (equal A)). +Axiom prf_refl : (A:Setoid)(Reflexive |A| (equal A)). +Axiom prf_sym : (A:Setoid)(Symmetric |A| (equal A)). +Axiom prf_trans : (A:Setoid)(Transitive |A| (equal A)). + +Section Maps. +Variables A,B: Setoid. + +Definition Map_law := [f:|A|->|B|] + (x,y:|A|) x =%S y -> (f x) =%S (f y). + +Inductive Map : Type := + Build_Map : (f:|A|->|B|)(p:(Map_law f))Map. + +Definition explicit_ap := [m:Map] <|A|->|B|>Match m with + [f:?][p:?]f end. + +Axiom pres : (m:Map)(Map_law (explicit_ap m)). + +Definition ext := [f,g:Map] + (x:|A|) (explicit_ap f x) =%S (explicit_ap g x). + +Axiom Equiv_map_eq : (Equivalence Map ext). + +Definition Map_setoid := (Build_Setoid Map ext Equiv_map_eq). + +End Maps. + +Syntactic Definition ap := (explicit_ap ? ?). + +Grammar command command8 := + map_setoid [ command7($c1) "=>" command8($c2) ] + -> [ <<(Map_setoid $c1 $c2)>>]. + + +Definition ap2 := [A,B,C:Setoid][f:|(A=>(B=>C))|][a:|A|] (ap (ap f a)). + + +(***** posint ******) + +Inductive posint : Type + := Z : posint | Suc : posint -> posint. + +Require Logic_Type. + +Axiom f_equal : (A,B:Type)(f:A->B)(x,y:A) x==y -> (f x)==(f y). +Axiom eq_Suc : (n,m:posint) n==m -> (Suc n)==(Suc m). + +(* The predecessor function *) + +Definition pred : posint->posint + := [n:posint](<posint>Case n of (* Z *) Z + (* Suc u *) [u:posint]u end). + +Axiom pred_Sucn : (m:posint) m==(pred (Suc m)). +Axiom eq_add_Suc : (n,m:posint) (Suc n)==(Suc m) -> n==m. +Axiom not_eq_Suc : (n,m:posint) ~(n==m) -> ~((Suc n)==(Suc m)). + + +Definition IsSuc : posint->Prop + := [n:posint](<Prop>Case n of (* Z *) False + (* Suc p *) [p:posint]True end). +Definition IsZero :posint->Prop := + [n:posint]<Prop>Match n with + True + [p:posint][H:Prop]False end. + +Axiom Z_Suc : (n:posint) ~(Z==(Suc n)). +Axiom Suc_Z: (n:posint) ~(Suc n)==Z. +Axiom n_Sucn : (n:posint) ~(n==(Suc n)). +Axiom Sucn_n : (n:posint) ~(Suc n)==n. +Axiom eqT_symt : (a,b:posint) ~(a==b)->~(b==a). + + +(******* Dsetoid *****) + +Definition Decidable :=[A:Type][R:(Relation A)] + (x,y:A)(R x y) \/ ~(R x y). + + +Record DSetoid : Type := +{Set_of : Setoid; + prf_decid : (Decidable |Set_of| (equal Set_of))}. + +(* example de Dsetoide d'entiers *) + + +Axiom eqT_equiv : (Equivalence posint (eqT posint)). +Axiom Eq_posint_deci : (Decidable posint (eqT posint)). + +(* Dsetoide des posint*) + +Definition Set_of_posint := (Build_Setoid posint (eqT posint) eqT_equiv). + +Definition Dposint := (Build_DSetoid Set_of_posint Eq_posint_deci). + + + +(**************************************) + + +(* Definition des signatures *) +(* une signature est un ensemble d'operateurs muni + de l'arite de chaque operateur *) + + +Section Sig. + +Record Signature :Type := +{Sigma : DSetoid; + Arity : (Map (Set_of Sigma) (Set_of Dposint))}. + +Variable S:Signature. + + + +Variable Var : DSetoid. + +Mutual Inductive TERM : Type := + var : |(Set_of Var)|->TERM + | oper : (op: |(Set_of (Sigma S))|) (LTERM (ap (Arity S) op)) -> TERM +with + LTERM : posint -> Type := + nil : (LTERM Z) + | cons : TERM -> (n:posint)(LTERM n) -> (LTERM (Suc n)). + + + +(* -------------------------------------------------------------------- *) +(* Examples *) +(* -------------------------------------------------------------------- *) + + +Parameter t1,t2: TERM. + +Type + Cases t1 t2 of + (var v1) (var v2) => True + + | (oper op1 l1) (oper op2 l2) => False + | _ _ => False + end. + + + +Parameter n2:posint. +Parameter l1, l2:(LTERM n2). + +Type + Cases l1 l2 of + nil nil => True + | (cons v m y) nil => False + | _ _ => False +end. + + +Type Cases l1 l2 of + nil nil => True + | (cons u n x) (cons v m y) =>False + | _ _ => False +end. + + + +Fixpoint equalT [t1:TERM]:TERM->Prop := +[t2:TERM] + Cases t1 t2 of + (var v1) (var v2) => True + | (oper op1 l1) (oper op2 l2) => False + | _ _ => False + end + +with EqListT [n1:posint;l1:(LTERM n1)]: (n2:posint)(LTERM n2)->Prop := +[n2:posint][l2:(LTERM n2)] + Cases l1 l2 of + nil nil => True + | (cons t1 n1' l1') (cons t2 n2' l2') => False + | _ _ => False +end. + + +Reset equalT. +Reset EqListT. +(* ------------------------------------------------------------------*) +(* Initial exemple (without patterns) *) +(*-------------------------------------------------------------------*) + +Fixpoint equalT [t1:TERM]:TERM->Prop := +<TERM->Prop>Case t1 of + (*var*) [v1:|(Set_of Var)|][t2:TERM] + <Prop>Case t2 of + (*var*)[v2:|(Set_of Var)|] (v1 =%S v2) + (*oper*)[op2:|(Set_of (Sigma S))|][_:(LTERM (ap (Arity S) op2))]False + end + (*oper*)[op1:|(Set_of (Sigma S))|] + [l1:(LTERM (ap (Arity S) op1))][t2:TERM] + <Prop>Case t2 of + (*var*)[v2:|(Set_of Var)|]False + (*oper*)[op2:|(Set_of (Sigma S))|] + [l2:(LTERM (ap (Arity S) op2))] + ((op1=%S op2)/\ (EqListT (ap (Arity S) op1) l1 (ap (Arity S) op2) l2)) + end +end +with EqListT [n1:posint;l1:(LTERM n1)]: (n2:posint)(LTERM n2)->Prop := +<[_:posint](n2:posint)(LTERM n2)->Prop>Case l1 of + (*nil*) [n2:posint][l2:(LTERM n2)] + <[_:posint]Prop>Case l2 of + (*nil*)True + (*cons*)[t2:TERM][n2':posint][l2':(LTERM n2')]False + end + (*cons*)[t1:TERM][n1':posint][l1':(LTERM n1')] + [n2:posint][l2:(LTERM n2)] + <[_:posint]Prop>Case l2 of + (*nil*) False + (*cons*)[t2:TERM][n2':posint][l2':(LTERM n2')] + ((equalT t1 t2) /\ (EqListT n1' l1' n2' l2')) + end +end. + + +(* ---------------------------------------------------------------- *) +(* Version with simple patterns *) +(* ---------------------------------------------------------------- *) +Reset equalT. + +Fixpoint equalT [t1:TERM]:TERM->Prop := +Cases t1 of + (var v1) => [t2:TERM] + Cases t2 of + (var v2) => (v1 =%S v2) + | (oper op2 _) =>False + end +| (oper op1 l1) => [t2:TERM] + Cases t2 of + (var _) => False + | (oper op2 l2) => (op1=%S op2) + /\ (EqListT (ap (Arity S) op1) l1 (ap (Arity S) op2) l2) + end +end +with EqListT [n1:posint;l1:(LTERM n1)]: (n2:posint)(LTERM n2)->Prop := +<[_:posint](n2:posint)(LTERM n2)->Prop>Cases l1 of + nil => [n2:posint][l2:(LTERM n2)] + Cases l2 of + nil => True + | _ => False + end +| (cons t1 n1' l1') => [n2:posint][l2:(LTERM n2)] + Cases l2 of + nil =>False + | (cons t2 n2' l2') => (equalT t1 t2) + /\ (EqListT n1' l1' n2' l2') + end +end. + + +Reset equalT. + +Fixpoint equalT [t1:TERM]:TERM->Prop := +Cases t1 of + (var v1) => [t2:TERM] + Cases t2 of + (var v2) => (v1 =%S v2) + | (oper op2 _) =>False + end +| (oper op1 l1) => [t2:TERM] + Cases t2 of + (var _) => False + | (oper op2 l2) => (op1=%S op2) + /\ (EqListT (ap (Arity S) op1) l1 (ap (Arity S) op2) l2) + end +end +with EqListT [n1:posint;l1:(LTERM n1)]: (n2:posint)(LTERM n2)->Prop := +[n2:posint][l2:(LTERM n2)] +Cases l1 of + nil => + Cases l2 of + nil => True + | _ => False + end +| (cons t1 n1' l1') => Cases l2 of + nil =>False + | (cons t2 n2' l2') => (equalT t1 t2) + /\ (EqListT n1' l1' n2' l2') + end +end. + +(* ---------------------------------------------------------------- *) +(* Version with multiple patterns *) +(* ---------------------------------------------------------------- *) +Reset equalT. + +Fixpoint equalT [t1:TERM]:TERM->Prop := +[t2:TERM] + Cases t1 t2 of + (var v1) (var v2) => (v1 =%S v2) + + | (oper op1 l1) (oper op2 l2) => + (op1=%S op2) /\ (EqListT (ap (Arity S) op1) l1 (ap (Arity S) op2) l2) + + | _ _ => False + end + +with EqListT [n1:posint;l1:(LTERM n1)]: (n2:posint)(LTERM n2)->Prop := +[n2:posint][l2:(LTERM n2)] + Cases l1 l2 of + nil nil => True + | (cons t1 n1' l1') (cons t2 n2' l2') => (equalT t1 t2) + /\ (EqListT n1' l1' n2' l2') + | _ _ => False +end. + + +(* ------------------------------------------------------------------ *) + +End Sig. |