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

1 files changed, 38 insertions, 0 deletions

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.