Adding tests for the "functional induction" facility.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3711 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 7 insertions, 65 deletions

diff --git a/contrib/funind/test.v b/contrib/funind/test.v
index eb794dde6..9e509a21d 100644
--- a/contrib/funind/test.v
+++ b/contrib/funind/test.v
@@ -1,20 +1,14 @@
-(* Declare ML Module "csimpl" "tacinvutils" "tacinv-new". *)
-Require Import Arith.
-(* Require Export Tacinvnew. *)
+Require Export Arith.
  
 Fixpoint trivfun [n : nat] : nat :=
  Cases n of O => O | (S m) => (trivfun m) end.
-(*Parameter P: nat -> Prop.
-  Goal  (n:nat)(P n).
-  Intro n.
-  Invfunproof trivfun params n.
-  Show Proof.
-*)
+
 
 (* essaie de parametre variables non locaux:*) 
 
-Variables varessai:nat.
-Goal(trivfun varessai) = O.
+Parameter varessai:nat.
+
+Lemma first_try (trivfun varessai) = O.
 Functional Induction trivfun varessai.
 Trivial.
 Simpl.
@@ -42,11 +36,6 @@ Fixpoint funex [n : nat] : nat :=
   | false =>
       Cases n of O => O | (S r) => (funex r) end
  end.
-(*Goal (n:nat) (funex n) = O -> (iseven n)=true.
-  Intro n.
-  Invfunproof funex params n.
-  Show Proof.
-   *)
  
 Fixpoint nat_equal_bool [n : nat] : nat ->  bool :=
  [m : nat]  Cases n of
@@ -55,7 +44,6 @@ Fixpoint nat_equal_bool [n : nat] : nat ->  bool :=
              | (S p) =>
                  Cases m of O => false | (S q) => (nat_equal_bool p q) end
             end.
-Require Export Arith.
 Require Export Div2.
  
 Lemma div2_inf: (n : nat)  (le (div2 n) n).
@@ -69,10 +57,6 @@ Apply le_S.
 Apply le_n_S.
 Exact H.
 Qed.
-(* 
-  Functional Scheme plus_ind := Induction plus.
-  Print plus_ind.
-   *)
  
 Fixpoint essai [x : nat] : nat * nat ->  nat :=
  [p : nat * nat]  ( Case p of [n, m : ?]  Cases n of
@@ -93,24 +77,6 @@ Inversion H.
 Simpl; Try Abstract ( Auto with arith ).
 Simpl; Try Abstract ( Auto with arith ).
 Qed.
-(* 
-  Lemma dep_dep:(x:nat)(le x (S x)).
-  Intro x.
-  Invfunproof essai_essai_trans params x.
-   
-   
-  Fixpoint  essaidep[x:nat]: () :=
-  [p:nat*nat]
-  let (n,m)=p in
-  Cases n of
-   | O => O
-   |(S q) =>  
-  Cases x of
-  | O => (S O)
-  | (S r) => (S (essai r (q,m)))
-  end
-  end.
-   *)
  
 Fixpoint plus_x_not_five' [n : nat] : nat ->  nat :=
  [m : nat]  Cases n of
@@ -163,7 +129,6 @@ Fixpoint plus_x_not_five'' [n : nat] : nat ->  nat :=
                      let recapp = (plus_x_not_five'' q m) in
                        Cases x of true => (S recapp) | false => (S recapp) end
                 end.
-(* let in pas encore traites *)
  
 Lemma notplusfive'':
  (x, y : nat) y = (S (S (S (S (S O))))) ->  (plus_x_not_five'' x y) = x.
@@ -200,16 +165,6 @@ Intros x.
 Apply istrue0.
 Inversion eg.
 Qed.
-(* 
-  plus = 
-  Fix plus
-  {plus [n:nat] : nat->nat :=
-     [m:nat]Cases n of
-              O => m
-            | (S p) => (S (plus p m))
-            end}
-     : nat->nat->nat
-   *)
  
 Lemma inf_x_plusxy': (x, y : nat)  (le x (plus x y)).
 Intros n m.
@@ -217,7 +172,7 @@ Intros n m.
 Auto with arith.
 Auto with arith.
 Qed.
-(* *****essais *)
+
  
 Lemma inf_x_plusxy'': (x : nat)  (le x (plus x O)).
 Intros n.
@@ -233,13 +188,6 @@ Intros n.
 (Functional Induction plus O n); Intros;Auto with arith.
 Qed.
 
-(*Lemma inf_x_plusxy''':(x,y:nat)(le x (plus (S x) (S y))).
-  Intros n m.
-  Invfunproof plus params (S n) (S m);Intros.
-  Auto with arith.
-  Assumption.
-  Save.*)
- 
 Fixpoint mod2 [n : nat] : nat :=
  Cases n of   O => O
              | (S (S m)) => (S (mod2 m))
@@ -257,7 +205,6 @@ Definition isononeorfour : nat ->  bool :=
    [n : nat]  Cases n of   (S O) => true
                           | (S (S (S (S O)))) => true
                           | _ => false end.
-(* Inductive istrue : bool -> Prop := istrue0 : (istrue true). *)
  
 Lemma toto'': (n : nat) (istrue (isfour n)) ->  (istrue (isononeorfour n)).
 Intros n.
@@ -421,9 +368,4 @@ Intros n m.
 Unfold ftest6.
 (Functional Induction ftest6 n m); Simpl; Auto.
 Qed.
-  (* 
-   Local Variables: 
-   coq-prog-name: "../mytop.out  -I . -emacs"
-   compile-command: "make -C <chemin du makefile> <chemin du makefile au fichier>.vo"
-   End:
-*)
+