1
(************************************************************************)
2
(* v * The Coq Proof Assistant / The Coq Development Team *)
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
4
(* \VV/ **************************************************************)
5
(* // * This file is distributed under the terms of the *)
6
(* * GNU Lesser General Public License Version 2.1 *)
7
(************************************************************************)
10
Require Import BinPos BinNat Nnat ZArith_base.
14
Definition NPgeb (a:N)(b:positive) :=
17
| Npos na => match Pcompare na b Eq with Lt => false | _ => true end
20
Fixpoint Pdiv_eucl (a b:positive) {struct a} : N * N :=
23
match b with xH => (1, 0)%N | _ => (0, 1)%N end
25
let (q, r) := Pdiv_eucl a' b in
26
let r' := (2 * r)%N in
27
if (NPgeb r' b) then (2 * q + 1, (Nminus r' (Npos b)))%N
30
let (q, r) := Pdiv_eucl a' b in
31
let r' := (2 * r + 1)%N in
32
if (NPgeb r' b) then (2 * q + 1, (Nminus r' (Npos b)))%N
36
Definition ZOdiv_eucl (a b:Z) : Z * Z :=
41
let (nq, nr) := Pdiv_eucl na nb in
42
(Z_of_N nq, Z_of_N nr)
44
let (nq, nr) := Pdiv_eucl na nb in
45
(Zopp (Z_of_N nq), Zopp (Z_of_N nr))
47
let (nq, nr) := Pdiv_eucl na nb in
48
(Zopp (Z_of_N nq), Z_of_N nr)
50
let (nq, nr) := Pdiv_eucl na nb in
51
(Z_of_N nq, Zopp (Z_of_N nr))
54
Definition ZOdiv a b := fst (ZOdiv_eucl a b).
55
Definition ZOmod a b := snd (ZOdiv_eucl a b).
58
Definition Ndiv_eucl (a b:N) : N * N :=
62
| Npos na, Npos nb => Pdiv_eucl na nb
65
Definition Ndiv a b := fst (Ndiv_eucl a b).
66
Definition Nmod a b := snd (Ndiv_eucl a b).
69
(* Proofs of specifications for these euclidean divisions. *)
71
Theorem NPgeb_correct: forall (a:N)(b:positive),
72
if NPgeb a b then a = (Nminus a (Npos b) + Npos b)%N else True.
74
destruct a; intros; simpl; auto.
75
generalize (Pcompare_Eq_eq p b).
76
case_eq (Pcompare p b Eq); intros; auto.
78
now rewrite Pminus_mask_diag.
79
destruct (Pminus_mask_Gt p b H) as [d [H2 [H3 _]]].
80
rewrite H2. rewrite <- H3.
81
simpl; f_equal; apply Pplus_comm.
84
Hint Rewrite Z_of_N_plus Z_of_N_mult Z_of_N_minus Zmult_1_l Zmult_assoc
85
Zmult_plus_distr_l Zmult_plus_distr_r : zdiv.
86
Hint Rewrite <- Zplus_assoc : zdiv.
88
Theorem Pdiv_eucl_correct: forall a b,
89
let (q,r) := Pdiv_eucl a b in
90
Zpos a = Z_of_N q * Zpos b + Z_of_N r.
92
induction a; cbv beta iota delta [Pdiv_eucl]; fold Pdiv_eucl; cbv zeta.
93
intros b; generalize (IHa b); case Pdiv_eucl.
95
generalize (NPgeb_correct (2 * r1 + 1) b); case NPgeb; intros H.
96
set (u := Nminus (2 * r1 + 1) (Npos b)) in * |- *.
97
assert (HH: Z_of_N u = (Z_of_N (2 * r1 + 1) - Zpos b)%Z).
98
rewrite H; autorewrite with zdiv; simpl.
99
rewrite Zplus_comm, Zminus_plus; trivial.
100
rewrite HH; autorewrite with zdiv; simpl Z_of_N.
101
rewrite Zpos_xI, Hq1.
102
autorewrite with zdiv; f_equal; rewrite Zplus_minus; trivial.
103
rewrite Zpos_xI, Hq1; autorewrite with zdiv; auto.
104
intros b; generalize (IHa b); case Pdiv_eucl.
106
generalize (NPgeb_correct (2 * r1) b); case NPgeb; intros H.
107
set (u := Nminus (2 * r1) (Npos b)) in * |- *.
108
assert (HH: Z_of_N u = (Z_of_N (2 * r1) - Zpos b)%Z).
109
rewrite H; autorewrite with zdiv; simpl.
110
rewrite Zplus_comm, Zminus_plus; trivial.
111
rewrite HH; autorewrite with zdiv; simpl Z_of_N.
112
rewrite Zpos_xO, Hq1.
113
autorewrite with zdiv; f_equal; rewrite Zplus_minus; trivial.
114
rewrite Zpos_xO, Hq1; autorewrite with zdiv; auto.
118
Theorem ZOdiv_eucl_correct: forall a b,
119
let (q,r) := ZOdiv_eucl a b in a = q * b + r.
121
destruct a; destruct b; simpl; auto;
122
generalize (Pdiv_eucl_correct p p0); case Pdiv_eucl; auto; intros;
123
try change (Zneg p) with (Zopp (Zpos p)); rewrite H.
125
repeat (rewrite Zopp_plus_distr || rewrite Zopp_mult_distr_l); trivial.
126
repeat (rewrite Zopp_plus_distr || rewrite Zopp_mult_distr_r); trivial.
129
Theorem Ndiv_eucl_correct: forall a b,
130
let (q,r) := Ndiv_eucl a b in a = (q * b + r)%N.
132
destruct a; destruct b; simpl; auto;
133
generalize (Pdiv_eucl_correct p p0); case Pdiv_eucl; auto; intros;
134
destruct n; destruct n0; simpl; simpl in H; try discriminate;
135
injection H; intros; subst; trivial.