Imported Upstream version 8.0pl3upstream/8.0pl3

1 files changed, 0 insertions, 203 deletions

diff --git a/test-suite/tactics/TestRefine.v b/test-suite/tactics/TestRefine.v
deleted file mode 100644
index f752c5bc..00000000
--- a/test-suite/tactics/TestRefine.v
+++ /dev/null
@@ -1,203 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(* 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.
-
-