diff options
author | Samuel Mimram <smimram@debian.org> | 2006-04-28 14:59:16 +0000 |
---|---|---|
committer | Samuel Mimram <smimram@debian.org> | 2006-04-28 14:59:16 +0000 |
commit | 3ef7797ef6fc605dfafb32523261fe1b023aeecb (patch) | |
tree | ad89c6bb57ceee608fcba2bb3435b74e0f57919e /test-suite/ideal-features/Case4.v | |
parent | 018ee3b0c2be79eb81b1f65c3f3fa142d24129c8 (diff) |
Imported Upstream version 8.0pl3+8.1alphaupstream/8.0pl3+8.1alpha
Diffstat (limited to 'test-suite/ideal-features/Case4.v')
-rw-r--r-- | test-suite/ideal-features/Case4.v | 73 |
1 files changed, 34 insertions, 39 deletions
diff --git a/test-suite/ideal-features/Case4.v b/test-suite/ideal-features/Case4.v index d8f14a4e..cb076a71 100644 --- a/test-suite/ideal-features/Case4.v +++ b/test-suite/ideal-features/Case4.v @@ -1,39 +1,34 @@ -Inductive listn : nat-> Set := - niln : (listn O) -| consn : (n:nat)nat->(listn n) -> (listn (S n)). - -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. - +Inductive listn : nat -> Set := + | niln : listn 0 + | consn : forall n : nat, nat -> listn n -> listn (S n). + +Inductive empty : forall n : nat, listn n -> Prop := + intro_empty : empty 0 niln. + +Parameter + inv_empty : forall (n a : nat) (l : listn n), ~ empty (S n) (consn n a l). + +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 O y as b => or_intror (empty (S n) b) (inv_empty n 0 y) + | 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 O y => or_intror (empty (S n) (consn n 0 y)) (inv_empty n 0 y) + | consn n a y => or_intror (empty (S n) (consn n a y)) (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 O a y as b => or_intror (empty 1 b) (inv_empty 0 a y) + | consn n a y as b => or_intror (empty (S n) b) (inv_empty n a y) + end). |