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
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
Require Import BinPos BinNat Pnat Plus Compare_dec.
Local Open Scope N_scope.
Definition NPgeb (a:N)(b:positive) :=
match a with
| 0 => false
| Npos na => match Pcompare na b Eq with Lt => false | _ => true end
end.
Local Notation "a >=? b" := (NPgeb a b) (at level 70).
Fixpoint Pdiv_eucl (a b:positive) : N * N :=
match a with
| xH =>
match b with xH => (1, 0) | _ => (0, 1) end
| xO a' =>
let (q, r) := Pdiv_eucl a' b in
let r' := 2 * r in
if r' >=? b then (2 * q + 1, r' - Npos b)
else (2 * q, r')
| xI a' =>
let (q, r) := Pdiv_eucl a' b in
let r' := 2 * r + 1 in
if r' >=? b then (2 * q + 1, r' - Npos b)
else (2 * q, r')
end.
Definition Ndiv_eucl (a b:N) : N * N :=
match a, b with
| 0, _ => (0, 0)
| _, 0 => (0, 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).
Infix "/" := Ndiv : N_scope.
Infix "mod" := Nmod (at level 40, no associativity) : N_scope.
(** Auxiliary Results about [NPgeb] *)
Lemma NPgeb_ge : forall a b, NPgeb a b = true -> a >= Npos b.
Proof.
destruct a; simpl; intros.
discriminate.
unfold Nge, Ncompare. now destruct Pcompare.
Qed.
Lemma NPgeb_lt : forall a b, NPgeb a b = false -> a < Npos b.
Proof.
destruct a; simpl; intros. red; auto.
unfold Nlt, Ncompare. now destruct Pcompare.
Qed.
Theorem NPgeb_correct: forall (a:N)(b:positive),
if NPgeb a b then a = a - Npos b + Npos b else True.
Proof.
destruct a as [|a]; simpl; intros b; auto.
generalize (Pcompare_Eq_eq a b).
case_eq (Pcompare a b Eq); intros; auto.
rewrite H0; auto.
now rewrite Pminus_mask_diag.
destruct (Pminus_mask_Gt a b H) as [d [H2 [H3 _]]].
rewrite H2. rewrite <- H3.
simpl; f_equal; apply Pplus_comm.
Qed.
Lemma Plt_add_cancel_l : forall n m p, (p+n < p+m -> n<m)%positive.
Proof.
intros n m p H.
unfold Plt in *.
rewrite nat_of_P_compare_morphism in *.
rewrite 2 nat_of_P_plus_morphism in *.
apply nat_compare_lt.
apply nat_compare_lt in H.
eapply plus_lt_reg_l; eauto.
Qed.
Lemma Plt_add_not_lt : forall n m, ~(n+m < n)%positive.
Proof.
intros n m H.
unfold Plt in *.
rewrite nat_of_P_compare_morphism in *.
rewrite nat_of_P_plus_morphism in *.
apply nat_compare_lt in H.
absurd (nat_of_P m < 0)%nat.
red; inversion 1.
apply plus_lt_reg_l with (nat_of_P n). now rewrite plus_0_r.
Qed.
Lemma Nlt_add_cancel_l : forall n m p, p+n < p+m -> n<m.
Proof.
intros. destruct p. simpl; auto.
destruct n; destruct m.
elim (Nlt_irrefl _ H).
red; auto.
rewrite Nplus_0_r in H. simpl in H.
elim (Plt_add_not_lt _ _ H).
apply Plt_add_cancel_l with p; auto.
Qed.
Lemma NPgeb_ineq0 : forall a p, a < Npos p -> NPgeb (2*a) p = true ->
2*a - Npos p < Npos p.
Proof.
intros a p LT GE.
apply Nlt_add_cancel_l with (Npos p).
rewrite Nplus_comm.
generalize (NPgeb_correct (2*a) p). rewrite GE. intros <-.
rewrite <- (Nmult_1_l (Npos p)). rewrite <- Nmult_plus_distr_r.
destruct a; auto.
Qed.
Lemma NPgeb_ineq1 : forall a p, a < Npos p -> NPgeb (2*a+1) p = true ->
(2*a+1) - Npos p < Npos p.
Proof.
intros a p LT GE.
apply Nlt_add_cancel_l with (Npos p).
rewrite Nplus_comm.
generalize (NPgeb_correct (2*a+1) p). rewrite GE. intros <-.
rewrite <- (Nmult_1_l (Npos p)). rewrite <- Nmult_plus_distr_r.
destruct a; auto.
red; simpl. apply Pcompare_eq_Lt; auto.
Qed.
(* Proofs of specifications for these euclidean divisions. *)
Theorem Pdiv_eucl_correct: forall a b,
let (q,r) := Pdiv_eucl a b in Npos a = q * Npos b + 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.
assert (Npos a~1 = 2*q1*Npos b + (2*r1+1))
by now rewrite Nplus_assoc, <- Nmult_assoc, <- Nmult_plus_distr_l, <- Hq1.
generalize (NPgeb_correct (2 * r1 + 1) b); case NPgeb; intros H'; auto.
rewrite Nmult_plus_distr_r, Nmult_1_l.
rewrite <- Nplus_assoc, (Nplus_comm (Npos b)), <- H'; auto.
intros b; generalize (IHa b); case Pdiv_eucl.
intros q1 r1 Hq1.
assert (Npos a~0 = 2*q1*Npos b + 2*r1)
by now rewrite <- Nmult_assoc, <- Nmult_plus_distr_l, <- Hq1.
generalize (NPgeb_correct (2 * r1) b); case NPgeb; intros H'; auto.
rewrite Nmult_plus_distr_r, Nmult_1_l.
rewrite <- Nplus_assoc, (Nplus_comm (Npos b)), <- H'; auto.
destruct b; auto.
Qed.
Theorem Ndiv_eucl_correct: forall a b,
let (q,r) := Ndiv_eucl a b in a = b * q + r.
Proof.
destruct a as [|a]; destruct b as [|b]; simpl; auto.
generalize (Pdiv_eucl_correct a b); case Pdiv_eucl; intros q r.
destruct q. simpl; auto. rewrite Nmult_comm. intro EQ; exact EQ.
Qed.
Theorem Ndiv_mod_eq : forall a b,
a = b * (a/b) + (a mod b).
Proof.
intros; generalize (Ndiv_eucl_correct a b).
unfold Ndiv, Nmod; destruct Ndiv_eucl; simpl; auto.
Qed.
Theorem Pdiv_eucl_remainder : forall a b:positive,
snd (Pdiv_eucl a b) < Npos b.
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 Hr1; simpl in Hr1.
case_eq (NPgeb (2*r1+1) b); intros; unfold snd.
apply NPgeb_ineq1; auto.
apply NPgeb_lt; auto.
intros b; generalize (IHa b); case Pdiv_eucl.
intros q1 r1 Hr1; simpl in Hr1.
case_eq (NPgeb (2*r1) b); intros; unfold snd.
apply NPgeb_ineq0; auto.
apply NPgeb_lt; auto.
destruct b; simpl; reflexivity.
Qed.
Theorem Nmod_lt : forall (a b:N), b<>0 -> a mod b < b.
Proof.
destruct b as [ |b]; intro H; try solve [elim H;auto].
destruct a as [ |a]; try solve [compute;auto]; unfold Nmod, Ndiv_eucl.
generalize (Pdiv_eucl_remainder a b); destruct Pdiv_eucl; simpl; auto.
Qed.
|
