diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-12-21 23:50:17 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-12-21 23:50:17 +0000 |
commit | 4d4f08acb5e5f56d38289e5629173bc1b8b5fd57 (patch) | |
tree | c160d442d54dbd15cbd0ab3500cdf94d0a6da74e /test-suite/ideal-features/Case4.v | |
parent | 960859c0c10e029f9768d0d70addeca8f6b6d784 (diff) |
Abandon tests syntaxe v7; remplacement des .v par des fichiers en syntaxe v8
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7693 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite/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 d8f14a4e1..cb076a718 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). |