diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-09-19 13:31:08 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-09-19 13:31:08 +0000 |
commit | 1920bd1b98f649ba60ceb271207df93faa46dc2d (patch) | |
tree | cd26fba6d5add6f4092b119cc02f0d2bd480a142 /test-suite/ideal-features/Case4.v | |
parent | d3b7163e7d033774a84ba6adc5ab707e22c28871 (diff) |
Comportements peut-être souhaités mais en tout cas non officiellement pris en compte
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1995 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite/ideal-features/Case4.v')
-rw-r--r-- | test-suite/ideal-features/Case4.v | 39 |
1 files changed, 39 insertions, 0 deletions
diff --git a/test-suite/ideal-features/Case4.v b/test-suite/ideal-features/Case4.v new file mode 100644 index 000000000..d8f14a4e1 --- /dev/null +++ b/test-suite/ideal-features/Case4.v @@ -0,0 +1,39 @@ +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. + |