- completely new version of "functional inversion" using inversion on

  inductive  

- bug  correction in  "Functional  scheme" and  "functional inversion": the
  function are now parsed as references and not indent

- adding a zeta normalization function in rawtermops to zeta normalize
  graph constructions (not used for now)

- Bug correction  in generation of  functional principle types  (if an
  arguments of the function has a type which is a sort)
  
- adding a new persistent table for functional induction informations
  (graph,...)  

- new  save mechanism  for functional  induction principles  (reuse of
  proofs when possible)

- Minor bug correction in proof of principle.

- Distinguishing building_principles (that is  save them) and making then
  (just construct their proof term)



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

1 files changed, 59 insertions, 5 deletions

diff --git a/test-suite/success/Funind.v b/test-suite/success/Funind.v
index 133764c043..c93a10381a 100644
--- a/test-suite/success/Funind.v
+++ b/test-suite/success/Funind.v
@@ -29,6 +29,18 @@ intros n m.
  functional induction ftest n m; auto.
 Qed.
 
+Lemma test2 : forall m n, ~ 2 = ftest n m.
+Proof. 
+intros n m;intro H.
+functional inversion H ftest.
+Qed.
+
+Lemma test3 : forall n m, ftest n m = 0 -> (n = 0 /\ m = 0)  \/ n <> 0.
+Proof.
+intros n m H;functional inversion H ftest;auto.
+Qed.
+
+
 Require Import Arith.
 Lemma test11 : forall m : nat, ftest 0 m <= 2.
 intros m.
@@ -112,7 +124,8 @@ Function iseven (n : nat) : bool :=
   | S (S m) => iseven m
   | _ => false
   end.
- 
+
+
 Function funex (n : nat) : nat :=
   match iseven n with
   | true => n
@@ -122,6 +135,7 @@ Function funex (n : nat) : nat :=
              end
   end.
  
+
 Function nat_equal_bool (n m : nat) {struct n} : bool :=
   match n with
   | O => match m with
@@ -151,7 +165,6 @@ Qed.
 
 (* reuse this lemma as a scheme:*)
 
-
 Function nested_lam (n : nat) : nat -> nat :=
   match n with
   | O => fun m : nat => 0
@@ -184,7 +197,6 @@ auto with arith.
  auto with arith.
 Qed.
 
- 
 Function plus_x_not_five'' (n m : nat) {struct n} : nat :=
   let x := nat_equal_bool m 5 in
   let y := 0 in
@@ -353,7 +365,7 @@ Function ftest2 (n m : nat) {struct n} : nat :=
   | S p => ftest2 p m
   end.
  
-Lemma test2 : forall n m : nat, ftest2 n m <= 2.
+Lemma test2' : forall n m : nat, ftest2 n m <= 2.
 intros n m.
  functional induction ftest2 n m; simpl in |- *; intros; auto.
 Qed.
@@ -367,7 +379,7 @@ Function ftest3 (n m : nat) {struct n} : nat :=
            end
   end.
  
-Lemma test3 : forall n m : nat, ftest3 n m <= 2.
+Lemma test3' : forall n m : nat, ftest3 n m <= 2.
 intros n m.
  functional induction ftest3 n m.
 intros.
@@ -442,10 +454,52 @@ intros n m.
  functional induction ftest6 n m; simpl in |- *; auto.
 Qed.
 
+(* Some tests with modules *) 
+Module M.
+Function test_m (n:nat) : nat := 
+  match n with 
+    | 0 => 0
+    | S n =>  S (S (test_m n))
+  end.
 
+Lemma test_m_is_double :  forall n, div2 (test_m n) = n.
+Proof.
+intros n.
+functional induction (test_m n).
+reflexivity.
+simpl;rewrite IHn0;reflexivity.
+Qed.
+End M.
+(* We redefine a new Function with the same name *) 
+Function test_m (n:nat) : nat := 
+  pred n.
+
+Lemma test_m_is_pred : forall n, test_m n = pred n.
+Proof. 
+intro n.
+functional induction (test_m n). (* the test_m_ind to use is the last defined  saying that test_m = pred*) 
+reflexivity.
+Qed.
 
+(* Checks if the dot notation are correctly treated in infos *)
+Lemma M_test_m_is_double : forall n, div2 (M.test_m n) = n.
+intro n.
+(* here we should apply M.test_m_ind *)
+functional induction (M.test_m n).
+reflexivity.
+simpl;rewrite IHn0;reflexivity.
+Qed.
 
+Import M.
+(* Now test_m is the one which defines double *)
 
+Lemma test_m_is_double : forall n, div2 (M.test_m n) = n.
+intro n.
+(* here we should apply M.test_m_ind *)
+functional induction (test_m n).
+reflexivity.
+simpl;rewrite IHn0;reflexivity.
+Qed.