1 files changed, 66 insertions, 0 deletions
diff --git a/contrib/subtac/test/euclid.v b/contrib/subtac/test/euclid.v
new file mode 100644
index 00000000..481b6708
--- /dev/null
+++ b/contrib/subtac/test/euclid.v
@@ -0,0 +1,66 @@
+
+Notation "( x & y )" := (@existS _ _ x y) : core_scope.
+Unset Printing All.
+
+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).
+reflexivity.
+Defined.
+
+Extraction testsig.
+Extraction sigS.
+Extract Inductive sigS => "" [ "" ].
+Extraction testsig.
+
+Require Import Coq.Arith.Compare_dec.
+
+Require Import Omega.
+
+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.
+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.
+
+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).
+
+exact (Acc_a).
+auto.
+auto.
+Focus 1.
+
+