Divisibility.v 5.38 KB
Newer Older
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
Guillaume Melquiond's avatar
Guillaume Melquiond committed
4
(*  Copyright 2010-2018   --   Inria - CNRS - Paris-Sud University  *)
5 6 7 8 9 10 11
(*                                                                  *)
(*  This software is distributed under the terms of the GNU Lesser  *)
(*  General Public License version 2.1, with the special exception  *)
(*  on linking described in file LICENSE.                           *)
(*                                                                  *)
(********************************************************************)

12 13 14 15 16 17 18 19 20
(* This file is generated by Why3's Coq-realize driver *)
(* Beware! Only edit allowed sections below    *)
Require Import BuiltIn.
Require BuiltIn.
Require int.Int.
Require int.Abs.
Require int.EuclideanDivision.
Require int.ComputerDivision.
Require number.Parity.
21

22 23 24
(* Hack so that Why3 does not override the notation below.

(* Why3 assumption *)
25 26
Definition divides (d:Z) (n:Z) : Prop :=
  ((d = 0%Z) -> (n = 0%Z)) /\
27
  (~ (d = 0%Z) -> ((ZArith.BinInt.Z.rem n d) = 0%Z)).
28 29 30 31 32 33 34

*)

Require Import Znumtheory.
Notation divides := Zdivide (only parsing).

(* Why3 goal *)
35 36
Lemma divides_spec :
  forall (d:Z) (n:Z), (divides d n) <-> exists q:Z, (n = (q * d)%Z).
37 38 39 40 41 42
Proof.
intros d n.
easy.
Qed.

(* Why3 goal *)
43
Lemma divides_refl : forall (n:Z), divides n n.
44 45 46 47 48
Proof.
exact Zdivide_refl.
Qed.

(* Why3 goal *)
49
Lemma divides_1_n : forall (n:Z), divides 1%Z n.
50 51 52 53 54
Proof.
exact Zone_divide.
Qed.

(* Why3 goal *)
55
Lemma divides_0 : forall (n:Z), divides n 0%Z.
56 57 58 59 60
Proof.
exact Zdivide_0.
Qed.

(* Why3 goal *)
61
Lemma divides_left :
62
  forall (a:Z) (b:Z) (c:Z), (divides a b) -> divides (c * a)%Z (c * b)%Z.
63 64 65 66 67
Proof.
exact Zmult_divide_compat_l.
Qed.

(* Why3 goal *)
68
Lemma divides_right :
69
  forall (a:Z) (b:Z) (c:Z), (divides a b) -> divides (a * c)%Z (b * c)%Z.
70 71 72 73 74
Proof.
exact Zmult_divide_compat_r.
Qed.

(* Why3 goal *)
75
Lemma divides_oppr : forall (a:Z) (b:Z), (divides a b) -> divides a (-b)%Z.
76 77 78 79 80
Proof.
exact Zdivide_opp_r.
Qed.

(* Why3 goal *)
81
Lemma divides_oppl : forall (a:Z) (b:Z), (divides a b) -> divides (-a)%Z b.
82 83 84 85 86
Proof.
exact Zdivide_opp_l.
Qed.

(* Why3 goal *)
87
Lemma divides_oppr_rev :
88
  forall (a:Z) (b:Z), (divides (-a)%Z b) -> divides a b.
89 90 91 92 93
Proof.
exact Zdivide_opp_l_rev.
Qed.

(* Why3 goal *)
94
Lemma divides_oppl_rev :
95
  forall (a:Z) (b:Z), (divides a (-b)%Z) -> divides a b.
96 97 98 99 100
Proof.
exact Zdivide_opp_r_rev.
Qed.

(* Why3 goal *)
101 102
Lemma divides_plusr :
  forall (a:Z) (b:Z) (c:Z),
103
  (divides a b) -> (divides a c) -> divides a (b + c)%Z.
104 105 106 107 108
Proof.
exact Zdivide_plus_r.
Qed.

(* Why3 goal *)
109 110
Lemma divides_minusr :
  forall (a:Z) (b:Z) (c:Z),
111
  (divides a b) -> (divides a c) -> divides a (b - c)%Z.
112 113 114 115 116
Proof.
exact Zdivide_minus_l.
Qed.

(* Why3 goal *)
117
Lemma divides_multl :
118
  forall (a:Z) (b:Z) (c:Z), (divides a b) -> divides a (c * b)%Z.
119 120 121 122 123 124
Proof.
intros a b c.
apply Zdivide_mult_r.
Qed.

(* Why3 goal *)
125
Lemma divides_multr :
126
  forall (a:Z) (b:Z) (c:Z), (divides a b) -> divides a (b * c)%Z.
127 128 129 130 131
Proof.
exact Zdivide_mult_l.
Qed.

(* Why3 goal *)
132
Lemma divides_factorl : forall (a:Z) (b:Z), divides a (b * a)%Z.
133 134 135 136 137
Proof.
exact Zdivide_factor_l.
Qed.

(* Why3 goal *)
138
Lemma divides_factorr : forall (a:Z) (b:Z), divides a (a * b)%Z.
139 140 141 142 143
Proof.
exact Zdivide_factor_r.
Qed.

(* Why3 goal *)
144
Lemma divides_n_1 :
145
  forall (n:Z), (divides n 1%Z) -> (n = 1%Z) \/ (n = (-1%Z)%Z).
146 147 148 149 150
Proof.
exact Zdivide_1.
Qed.

(* Why3 goal *)
151 152
Lemma divides_antisym :
  forall (a:Z) (b:Z),
153
  (divides a b) -> (divides b a) -> (a = b) \/ (a = (-b)%Z).
154 155 156 157 158
Proof.
exact Zdivide_antisym.
Qed.

(* Why3 goal *)
159
Lemma divides_trans :
160
  forall (a:Z) (b:Z) (c:Z), (divides a b) -> (divides b c) -> divides a c.
161 162 163 164 165
Proof.
exact Zdivide_trans.
Qed.

(* Why3 goal *)
166 167
Lemma divides_bounds : forall (a:Z) (b:Z), (divides a b) -> ((~ (b = 0%Z)) ->
  ((ZArith.BinInt.Z.abs a) <= (ZArith.BinInt.Z.abs b))%Z).
168 169 170 171 172 173 174
Proof.
exact Zdivide_bounds.
Qed.

Import EuclideanDivision.

(* Why3 goal *)
175 176
Lemma mod_divides_euclidean :
  forall (a:Z) (b:Z),
177
  ~ (b = 0%Z) -> ((int.EuclideanDivision.mod1 a b) = 0%Z) -> divides b a.
178 179 180 181 182 183 184 185 186
Proof.
intros a b Zb H.
exists (div a b).
rewrite (Div_mod a b Zb) at 1.
rewrite H.
ring.
Qed.

(* Why3 goal *)
187 188 189
Lemma divides_mod_euclidean :
  forall (a:Z) (b:Z),
  ~ (b = 0%Z) -> (divides b a) -> ((int.EuclideanDivision.mod1 a b) = 0%Z).
190 191 192 193 194 195 196 197 198 199 200 201 202
Proof.
intros a b Zb H.
assert (Zmod a b = Z0).
now apply Zdivide_mod.
unfold mod1, div.
rewrite H0.
case Z_le_dec ; intros H1.
rewrite (Z_div_exact_full_2 a b Zb H0) at 1.
apply Zminus_diag.
now elim H1.
Qed.

(* Why3 goal *)
203 204
Lemma mod_divides_computer :
  forall (a:Z) (b:Z),
205
  ~ (b = 0%Z) -> ((ZArith.BinInt.Z.rem a b) = 0%Z) -> divides b a.
206 207
Proof.
intros a b Zb H.
208
exists (Z.quot a b).
209
rewrite Zmult_comm.
210
now apply Zquot.Z_quot_exact_full.
211 212 213
Qed.

(* Why3 goal *)
214 215
Lemma divides_mod_computer :
  forall (a:Z) (b:Z),
216
  ~ (b = 0%Z) -> (divides b a) -> ((ZArith.BinInt.Z.rem a b) = 0%Z).
217 218 219
Proof.
intros a b Zb (q,H).
rewrite H.
220
apply Zquot.Z_rem_mult.
221 222 223
Qed.

(* Why3 goal *)
224 225
Lemma even_divides :
  forall (a:Z), (number.Parity.even a) <-> (divides 2%Z a).
226 227 228 229 230 231
Proof.
split ;
  intros (q,H) ; exists q ; now rewrite Zmult_comm.
Qed.

(* Why3 goal *)
232 233
Lemma odd_divides :
  forall (a:Z), (number.Parity.odd a) <-> ~ (divides 2%Z a).
234 235 236 237 238 239 240 241 242 243 244 245
Proof.
split.
intros H.
contradict H.
apply Parity.even_not_odd.
now apply <- even_divides.
intros H.
destruct (Parity.even_or_odd a).
elim H.
now apply -> even_divides.
exact H0.
Qed.
246