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
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
Require Import BinPos.
Require Import BinNat.
Require Import ZArith_base.
Definition Ngeb a b :=
match a with
N0 => false
| Npos na => match Pcompare na b Eq with Lt => false | _ => true end end.
Fixpoint pdiv_eucl (a b:positive) {struct a} : N * N :=
match a with
| xH =>
match b with xH => (1, 0)%N | _ => (0, 1)%N end
| xO a' =>
let (q, r) := pdiv_eucl a' b in
let r' := (2 * r)%N in
if (Ngeb r' b) then(2 * q + 1, (Nminus r' (Npos b)))%N
else (2 * q, r')%N
| xI a' =>
let (q, r) := pdiv_eucl a' b in
let r' := (2 * r + 1)%N in
if (Ngeb r' b) then(2 * q + 1, (Nminus r' (Npos b)))%N
else (2 * q, r')%N
end.
Theorem Ngeb_correct: forall a b,
if Ngeb a b then a = ((Nminus a (Npos b)) + Npos b)%N else True.
destruct a; intros; simpl; auto.
case_eq (Pcompare p b Eq); intros; auto.
rewrite (Pcompare_Eq_eq _ _ H).
assert (HH: forall p, Pminus p p = xH).
intro p0; unfold Pminus; rewrite Pminus_mask_diag; auto.
simpl; auto.
generalize (Pplus_minus _ _ H).
case (p - b)%positive; intros; subst;
unfold Nplus; rewrite Pplus_comm; trivial.
Qed.
Theorem Z_of_N_plus:
forall a b, Z_of_N (a + b) = (Z_of_N a + Z_of_N b)%Z.
destruct a; destruct b; simpl; auto.
Qed.
Theorem Z_of_N_mult:
forall a b, Z_of_N (a * b) = (Z_of_N a * Z_of_N b)%Z.
destruct a; destruct b; simpl; auto.
Qed.
Ltac z_of_n_tac := repeat (rewrite Z_of_N_plus || rewrite Z_of_N_mult).
Ltac ztac := repeat (rewrite Zmult_plus_distr_l ||
rewrite Zmult_plus_distr_r ||
rewrite <- Zplus_assoc ||
rewrite Zmult_assoc || rewrite Zmult_1_l ).
Theorem pdiv_eucl_correct: forall a b,
let (q,r) := pdiv_eucl a b in Zpos a = (Z_of_N q * Zpos b + Z_of_N r)%Z.
induction a; unfold pdiv_eucl; fold pdiv_eucl.
intros b; generalize (IHa b); case pdiv_eucl.
intros q1 r1 Hq1.
generalize (Ngeb_correct (2 * r1 + 1) b); case Ngeb; intros H.
set (u := Nminus (2 * r1 + 1) (Npos b)) in * |- *.
assert (HH: Z_of_N u = (Z_of_N (2 * r1 + 1) - Zpos b)%Z).
rewrite H; z_of_n_tac; simpl.
rewrite Zplus_comm; rewrite Zminus_plus; trivial.
rewrite HH; z_of_n_tac; simpl Z_of_N.
rewrite Zpos_xI; rewrite Hq1.
ztac; apply f_equal2 with (f := Zplus); auto.
rewrite Zplus_minus; trivial.
rewrite Zpos_xI; rewrite Hq1; z_of_n_tac; ztac; auto.
intros b; generalize (IHa b); case pdiv_eucl.
intros q1 r1 Hq1.
generalize (Ngeb_correct (2 * r1) b); case Ngeb; intros H.
set (u := Nminus (2 * r1) (Npos b)) in * |- *.
assert (HH: Z_of_N u = (Z_of_N (2 * r1) - Zpos b)%Z).
rewrite H; z_of_n_tac; simpl.
rewrite Zplus_comm; rewrite Zminus_plus; trivial.
rewrite HH; z_of_n_tac; simpl Z_of_N.
rewrite Zpos_xO; rewrite Hq1.
ztac; apply f_equal2 with (f := Zplus); auto.
rewrite Zplus_minus; trivial.
rewrite Zpos_xO; rewrite Hq1; z_of_n_tac; ztac; auto.
destruct b; auto.
Qed.
Definition zdiv_eucl (a b:Z) :=
match a, b with
Z0, _ => (Z0, Z0)
| _, Z0 => (Z0, a)
| Zpos na, Zpos nb =>
let (nq, nr) := pdiv_eucl na nb in (Z_of_N nq, Z_of_N nr)
| Zneg na, Zpos nb =>
let (nq, nr) := pdiv_eucl na nb in (Zopp (Z_of_N nq), Zopp (Z_of_N nr))
| Zpos na, Zneg nb =>
let (nq, nr) := pdiv_eucl na nb in (Zopp(Z_of_N nq), Z_of_N nr)
| Zneg na, Zneg nb =>
let (nq, nr) := pdiv_eucl na nb in (Z_of_N nq, Zopp (Z_of_N nr))
end.
Theorem zdiv_eucl_correct: forall a b,
let (q,r) := zdiv_eucl a b in a = (q * b + r)%Z.
destruct a; destruct b; simpl; auto;
generalize (pdiv_eucl_correct p p0); case pdiv_eucl; auto; intros;
try change (Zneg p) with (Zopp (Zpos p)); rewrite H.
destruct n; auto.
repeat (rewrite Zopp_plus_distr || rewrite Zopp_mult_distr_l); trivial.
repeat (rewrite Zopp_plus_distr || rewrite Zopp_mult_distr_r); trivial.
Qed.
Definition ndiv_eucl (a b:N) :=
match a, b with
N0, _ => (N0, N0)
| _, N0 => (N0, a)
| Npos na, Npos nb =>
let (nq, nr) := pdiv_eucl na nb in (nq, nr)
end.
Theorem ndiv_eucl_correct: forall a b,
let (q,r) := ndiv_eucl a b in a = (q * b + r)%N.
destruct a; destruct b; simpl; auto;
generalize (pdiv_eucl_correct p p0); case pdiv_eucl; auto; intros;
destruct n; destruct n0; simpl; simpl in H; try
discriminate;
injection H; intros; subst; trivial.
Qed.
|
