Ajout de "Theorem id1 : t1 ... with idn : tn" pour partager la preuve

des théorèmes prouvés par récursion ou corécursion mutuelle.

Correction au passage du parsing et du printing des tactiques
fix/cofix et documentation de ces tactiques.



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

3 files changed, 75 insertions, 0 deletions

diff --git a/test-suite/output/Fixpoint.out b/test-suite/output/Fixpoint.out
index 62c9d3952..cbb387ce9 100644
--- a/test-suite/output/Fixpoint.out
+++ b/test-suite/output/Fixpoint.out
@@ -9,3 +9,17 @@ let fix f (m : nat) : nat := match m with
                              | S m' => f m'
                              end in f 0
      : nat
+fix even_pos_odd_pos 2
+ with (odd_pos_even_pos (n:_) (H:odd n) {struct H} : n >= 1).
+ intros.
+ destruct H.
+   omega.
+  
+   apply odd_pos_even_pos in H.
+   omega.
+  
+ intros.
+ destruct H.
+  apply even_pos_odd_pos in H.
+  omega.
+
diff --git a/test-suite/output/Fixpoint.v b/test-suite/output/Fixpoint.v
index fc27e8d28..2b13c2041 100644
--- a/test-suite/output/Fixpoint.v
+++ b/test-suite/output/Fixpoint.v
@@ -16,3 +16,26 @@ Check
     end
   in f 0.
 
+Require Import ZArith_base Omega.
+Open Scope Z_scope.
+
+Inductive even: Z -> Prop :=
+| even_base: even 0
+| even_succ: forall n, odd (n - 1) -> even n
+with odd: Z -> Prop :=
+| odd_succ: forall n, even (n - 1) -> odd n.
+
+Lemma even_pos_odd_pos: forall n, even n -> n >= 0.
+Proof.
+fix even_pos_odd_pos 2 with (odd_pos_even_pos n (H:odd n) {struct H} : n >= 1).
+ intros.
+ destruct H.
+   omega.
+   apply odd_pos_even_pos in H.
+   omega.
+ intros.
+ destruct H.
+  apply even_pos_odd_pos in H.
+  omega.
+Show Script.
+Qed.
diff --git a/test-suite/success/fix.v b/test-suite/success/fix.v
index 108886cf5..78b01f3e1 100644
--- a/test-suite/success/fix.v
+++ b/test-suite/success/fix.v
@@ -57,3 +57,41 @@ Lemma bx0bx : decomp bx0 = bx1.
 simpl. (* used to return bx0 in V8.1 and before instead of bx1 *)
 reflexivity.
 Qed.
+
+(* Check mutually inductive statements *)
+
+Require Import ZArith_base Omega.
+Open Scope Z_scope.
+
+Inductive even: Z -> Prop :=
+| even_base: even 0
+| even_succ: forall n, odd (n - 1) -> even n
+with odd: Z -> Prop :=
+| odd_succ: forall n, even (n - 1) -> odd n.
+
+Lemma even_pos_odd_pos: forall n, even n -> n >= 0
+with odd_pos_even_pos : forall n, odd n -> n >= 1.
+Proof.
+ intros.
+ destruct H.
+   omega.
+   apply odd_pos_even_pos in H.
+   omega.
+ intros.
+ destruct H.
+  apply even_pos_odd_pos in H.
+  omega.
+Qed.
+
+CoInductive a : Prop := acons : b -> a
+with b : Prop := bcons : a -> b.
+
+Lemma a1 : a
+with b1 : b.
+Proof.
+apply acons.
+assumption.
+
+apply bcons.
+assumption.
+Qed.