diff options
Diffstat (limited to 'contrib/subtac/test/euclid.v')
-rw-r--r-- | contrib/subtac/test/euclid.v | 66 |
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. + + |