Work on mutual defs, various bug fixes.

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

2 files changed, 47 insertions, 60 deletions

diff --git a/contrib/subtac/test/Mutind.v b/contrib/subtac/test/Mutind.v
index 0b40ef82a8..8a9bec52f0 100644
--- a/contrib/subtac/test/Mutind.v
+++ b/contrib/subtac/test/Mutind.v
@@ -1,13 +1,28 @@
-Program Fixpoint f (a : nat) : nat := 
+Program Fixpoint f (a : nat) : { x : nat | x > 0 } := 
   match a with
-  | 0 => 0
+  | 0 => 1
   | S a' => g a a'
   end
-with g (a b : nat) { struct b } : nat := 
+with g (a b : nat) { struct b } : { x : nat | x > 0 } := 
   match b with
-  | 0 => 0
+  | 0 => 1
   | S b' => f b'
   end.
 
+Obligations of f.
+
+Obligation 1 of f.
+  simpl ; intros ; auto with arith.
+Defined.
+
+Obligation 1 of g.
+  simpl ; intros ; auto with arith.
+Defined.
+
 Check f.
-Check g.
\ No newline at end of file
+Check g.
+
+
+
+
+
diff --git a/contrib/subtac/test/euclid.v b/contrib/subtac/test/euclid.v
index c14edad556..7fa80fbd0c 100644
--- a/contrib/subtac/test/euclid.v
+++ b/contrib/subtac/test/euclid.v
@@ -11,71 +11,43 @@ Program Fixpoint euclid (a : nat) (b : { b : nat | b <> O }) {wf a lt}  :
 
 Obligations.
 
-Definition t := fun (Evar46 : forall a : nat, (fun y : nat => @eq nat a y) a) (a : nat) =>
-@existS nat (fun x : nat => @sig nat (fun y : nat => @eq nat x y)) a
-  (@exist nat (fun y : nat => @eq nat a y) a (Evar46 a)).
-
-Program Definition testsig (a : nat) : { x : nat & { y : nat | x = y } } :=
-  (a & a).
+Require Import Coq.subtac.Utils.
+Require Import Coq.subtac.FixSub.
+Require Import Omega.
 
 Obligation 1.
-intros ; simpl ; auto.
+  simpl ; intros.
+  destruct_exists ; simpl in * ; auto with arith.
+  omega.
 Qed.
 
-Solve Obligations using auto.
-reflexivity.
-Defined.
-
-Extraction testsig.
-Extraction sig.
-Extract Inductive sig => "" [ "" ].
-Extraction testsig.
-
-Require Import Coq.Arith.Compare_dec.
+Obligation 2 of euclid.
+  simpl ; intros.
+  destruct_exists ; simpl in * ; auto with arith.
+  assert(x0 * S q' = x0 * q' + x0) by auto with arith ; omega.
+Qed.
 
-Require Import Omega.
+Obligation 4 of euclid.
+  exact Wf_nat.lt_wf.
+Qed.
 
-Lemma minus_eq_add : forall x y z w, y <= x -> x - y = y * z + w -> x = y * S z + w.
-intros.
-assert(y * S z = y * z + y).
-auto.
-rewrite H1.
-omega.
+Obligation 3 of euclid.
+  simpl ; intros.
+  destruct_exists ; simpl in *.
+  omega.
 Qed.
 
-Program Fixpoint euclid (a : nat) (b : { b : nat | b <> O }) {wf a lt}  :
-  { q : nat & { r : nat | a = b * q + r /\ r < b } } :=
-  if le_lt_dec b a then let (q', r) := euclid (a - b) b in 
-  (S q' & r)
-  else (O & a).
-intro euclid.
-simpl ; intros.
-Print euclid_evars.
-eapply euclid_evars with euclid.
-refine (euclid_evars _ _ _ euclid a Acc_a b).
-; simpl ; intros.
-Show Existentials.
+Extraction Inline Fix_sub Fix_F_sub.  
+Extract Inductive sigT => "pair" [ "" ].
+Extract Inductive sumbool => "bool" [ "true" "false" ].
+Extraction le_lt_dec.
+Extraction euclid.
 
-induction b0 ; induction r.
-simpl in H.
-simpl.
-simpl in p0.
-destruct p0.
-split.
 
-apply minus_eq_add.
-omega.
-auto with arith.
-auto.
-simpl.
-induction b0 ; simpl.
-split ; auto.
-omega.
-exact (euclid a0 Acc_a0 b0).
+Program Definition testsig (a : nat) : { x : nat & { y : nat | x = y } } :=
+  (a & a).
 
-exact (Acc_a).
-auto.
-auto.
-Focus 1.
 
+Solve Obligations using simpl ; auto.
 
+Extraction testsig.