diff options
author | 2000-07-20 16:35:38 +0000 | |
---|---|---|
committer | 2000-07-20 16:35:38 +0000 | |
commit | f8a0d5e7f5efcd588627a2eadeb6e8f9f7d597c6 (patch) | |
tree | 229d4650831bd3a4e910cf8802f7b6418768c114 | |
parent | 19b494e50ce36127782c4147c64e330a06387279 (diff) |
tests Refine
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@558 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r-- | test-suite/tactics/TestRefine.v | 196 |
1 files changed, 196 insertions, 0 deletions
diff --git a/test-suite/tactics/TestRefine.v b/test-suite/tactics/TestRefine.v new file mode 100644 index 000000000..1643c44ca --- /dev/null +++ b/test-suite/tactics/TestRefine.v @@ -0,0 +1,196 @@ + +(* Petit bench vite fait, mal fait *) + +Require Refine. + + +(***********************************************************************) + +Lemma essai : (x:nat)x=x. + +Refine (([x0:nat]Cases x0 of + O => ? + | (S p) => ? + end) :: (x:nat)x=x). (* x0=x0 et x0=x0 *) + +Restart. + +Refine [x0:nat]<[n:nat]n=n>Case x0 of ? [p:nat]? end. (* OK *) + +Restart. + +Refine [x0:nat]<[n:nat]n=n>Cases x0 of O => ? | (S p) => ? end. (* OK *) + +Restart. + +(** +Refine [x0:nat]Cases x0 of O => ? | (S p) => ? end. (* cannot be executed *) +**) + +Abort. + + +(***********************************************************************) + +Lemma T : nat. + +Refine (S ?). + +Abort. + + +(***********************************************************************) + +Lemma essai2 : (x:nat)x=x. + +Refine Fix f{f/1 : (x:nat)x=x := [x:nat]? }. + +Restart. + +Refine Fix f{f/1 : (x:nat)x=x := + [x:nat]<[n:nat](eq nat n n)>Case x of ? [p:nat]? end}. + +Restart. + +Refine Fix f{f/1 : (x:nat)x=x := + [x:nat]<[n:nat]n=n>Cases x of O => ? | (S p) => ? end}. + +Restart. + +Refine Fix f{f/1 : (x:nat)x=x := + [x:nat]<[n:nat](eq nat n n)>Case x of + ? + [p:nat](f_equal nat nat S p p ?) end}. + +Restart. + +Refine Fix f{f/1 : (x:nat)x=x := + [x:nat]<[n:nat](eq nat n n)>Cases x of + O => ? + | (S p) =>(f_equal nat nat S p p ?) end}. + +Abort. + + +(***********************************************************************) + +Lemma essai : nat. + +Parameter f : nat*nat -> nat -> nat. + +Refine (f ? ([x:nat](? :: nat) O)). + +Restart. + +Refine (f ? O). + +Abort. + + +(***********************************************************************) + +Parameter P : nat -> Prop. + +Lemma essai : { x:nat | x=(S O) }. + +Refine (exist nat ? (S O) ?). (* ECHEC *) + +Restart. + +(* mais si on contraint par le but alors ca marche : *) +(* Remarque : on peut toujours faire ça *) +Refine ((exist nat ? (S O) ?) :: { x:nat | x=(S O) }). + +Restart. + +Refine (exist nat [x:nat](x=(S O)) (S O) ?). + +Abort. + + +(***********************************************************************) + +Lemma essai : (n:nat){ x:nat | x=(S n) }. + +Refine [n:nat]<[n:nat]{x:nat|x=(S n)}>Case n of ? [p:nat]? end. + +Restart. + +Refine (([n:nat]Case n of ? [p:nat]? end) :: (n:nat){ x:nat | x=(S n) }). + +Restart. + +Refine [n:nat]<[n:nat]{x:nat|x=(S n)}>Cases n of O => ? | (S p) => ? end. + +Restart. + +Refine Fix f{f/1 :(n:nat){x:nat|x=(S n)} := + [n:nat]<[n:nat]{x:nat|x=(S n)}>Case n of ? [p:nat]? end}. + +Restart. + +Refine Fix f{f/1 :(n:nat){x:nat|x=(S n)} := + [n:nat]<[n:nat]{x:nat|x=(S n)}>Cases n of O => ? | (S p) => ? end}. + +Exists (S O). Trivial. +Elim (f0 p). +Refine [x:nat][h:x=(S p)](exist nat [x:nat]x=(S (S p)) (S x) ?). +Rewrite h. Auto. +Save. + + + +(* Quelques essais de recurrence bien fondée *) + +Require Wf. +Require Wf_nat. + +Lemma essai_wf : nat->nat. + +Refine [x:nat](well_founded_induction + nat + lt ? + [_:nat]nat->nat + [phi0:nat][w:(phi:nat)(lt phi phi0)->nat->nat](w x ?) + x x). +Exact lt_wf. + +Abort. + + +Require Compare_dec. +Require Lt. + +Lemma fibo : nat -> nat. +Refine (well_founded_induction + nat + lt ? + [_:nat]nat + [x0:nat][fib:(x:nat)(lt x x0)->nat] + Cases (zerop x0) of + (left _) => (S O) + | (right h1) => Cases (zerop (pred x0)) of + (left _) => (S O) + | (right h2) => (plus (fib (pred x0) ?) + (fib (pred (pred x0)) ?)) + end + end). +(********* +Refine (well_founded_induction + nat + lt ? + [_:nat]nat + [x0:nat][fib:(x:nat)(lt x x0)->nat] + Cases x0 of + O => (S O) + | (S O) => (S O) + | (S (S p)) => (plus (fib (pred x0) ?) + (fib (pred (pred x0)) ?)) + end). +***********) +Exact lt_wf. +Auto. +Apply lt_trans with m:=(pred x0); Auto. +Save. + + |