blob: ba5bdf2327bc1e951727364ab761cc5dc9f2fa60 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
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 sig.
Extract Inductive sig => "" [ "" ].
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.
|
