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
|
(************************************************************************)
(* 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 BinNat Nnat ZArith_base.
Open Scope Z_scope.
Definition NPgeb (a:N)(b:positive) :=
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 (NPgeb 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 (NPgeb r' b) then (2 * q + 1, (Nminus r' (Npos b)))%N
else (2 * q, r')%N
end.
Definition ZOdiv_eucl (a b:Z) : Z * 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.
Definition ZOdiv a b := fst (ZOdiv_eucl a b).
Definition ZOmod a b := snd (ZOdiv_eucl a b).
Definition Ndiv_eucl (a b:N) : N * N :=
match a, b with
| N0, _ => (N0, N0)
| _, N0 => (N0, a)
| Npos na, Npos nb => Pdiv_eucl na nb
end.
Definition Ndiv a b := fst (Ndiv_eucl a b).
Definition Nmod a b := snd (Ndiv_eucl a b).
(* Proofs of specifications for these euclidean divisions. *)
Theorem NPgeb_correct: forall (a:N)(b:positive),
if NPgeb a b then a = (Nminus a (Npos b) + Npos b)%N else True.
Proof.
destruct a; intros; simpl; auto.
generalize (Pcompare_Eq_eq p b).
case_eq (Pcompare p b Eq); intros; auto.
rewrite H0; auto.
now rewrite Pminus_mask_diag.
destruct (Pminus_mask_Gt p b H) as [d [H2 [H3 _]]].
rewrite H2. rewrite <- H3.
simpl; f_equal; apply Pplus_comm.
Qed.
Hint Rewrite Z_of_N_plus Z_of_N_mult Z_of_N_minus Zmult_1_l Zmult_assoc
Zmult_plus_distr_l Zmult_plus_distr_r : zdiv.
Hint Rewrite <- Zplus_assoc : zdiv.
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.
Proof.
induction a; cbv beta iota delta [Pdiv_eucl]; fold Pdiv_eucl; cbv zeta.
intros b; generalize (IHa b); case Pdiv_eucl.
intros q1 r1 Hq1.
generalize (NPgeb_correct (2 * r1 + 1) b); case NPgeb; 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; autorewrite with zdiv; simpl.
rewrite Zplus_comm, Zminus_plus; trivial.
rewrite HH; autorewrite with zdiv; simpl Z_of_N.
rewrite Zpos_xI, Hq1.
autorewrite with zdiv; f_equal; rewrite Zplus_minus; trivial.
rewrite Zpos_xI, Hq1; autorewrite with zdiv; auto.
intros b; generalize (IHa b); case Pdiv_eucl.
intros q1 r1 Hq1.
generalize (NPgeb_correct (2 * r1) b); case NPgeb; 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; autorewrite with zdiv; simpl.
rewrite Zplus_comm, Zminus_plus; trivial.
rewrite HH; autorewrite with zdiv; simpl Z_of_N.
rewrite Zpos_xO, Hq1.
autorewrite with zdiv; f_equal; rewrite Zplus_minus; trivial.
rewrite Zpos_xO, Hq1; autorewrite with zdiv; auto.
destruct b; auto.
Qed.
Theorem ZOdiv_eucl_correct: forall a b,
let (q,r) := ZOdiv_eucl a b in a = q * b + r.
Proof.
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.
Theorem Ndiv_eucl_correct: forall a b,
let (q,r) := Ndiv_eucl a b in a = (q * b + r)%N.
Proof.
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.
|
