EuclideanDivision.v 5.89 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
(* 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.
18

19 20
(* Why3 goal *)
Definition div: Z -> Z -> Z.
21 22 23 24 25 26
intros x y.
case (Z_le_dec 0 (Zmod x y)) ; intros H.
exact (Zdiv x y).
exact (Zdiv x y + 1)%Z.
Defined.

27 28
(* Why3 goal *)
Definition mod1: Z -> Z -> Z.
29 30 31 32
intros x y.
exact (x - y * div x y)%Z.
Defined.

33
(* Why3 goal *)
34 35 36 37 38 39 40
Lemma Div_mod : forall (x:Z) (y:Z), (~ (y = 0%Z)) -> (x = ((y * (div x
  y))%Z + (mod1 x y))%Z).
intros x y Zy.
unfold mod1, div.
case Z_le_dec ; intros H ; ring.
Qed.

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
(* Why3 goal *)
Lemma Mod_bound : forall (x:Z) (y:Z), (~ (y = 0%Z)) -> ((0%Z <= (mod1 x
  y))%Z /\ ((mod1 x y) < (ZArith.BinInt.Z.abs y))%Z).
intros x y Zy.
zify.
assert (H1 := Z_mod_neg x y).
assert (H2 := Z_mod_lt x y).
unfold mod1, div.
case Z_le_dec ; intros H0.
rewrite Zmult_comm, <- Zmod_eq_full with (1 := Zy).
omega.
replace (x - y * (x / y + 1))%Z with (x - x / y * y - y)%Z by ring.
rewrite <- Zmod_eq_full with (1 := Zy).
omega.
Qed.

(* Why3 goal *)
Lemma Div_unique : forall (x:Z) (y:Z) (q:Z), (0%Z < y)%Z ->
  ((((q * y)%Z <= x)%Z /\ (x < ((q * y)%Z + y)%Z)%Z) -> ((div x y) = q)).
intros x y q h1 (h2,h3).
assert (h:(~(y=0))%Z) by omega.
generalize (Mod_bound x y h); intro h0.
rewrite Z.abs_eq in h0; auto with zarith.
generalize (Div_mod x y h); clear h; intro h.
assert (cases:(div x y = q \/ (div x y <= q - 1 \/ div x y >= q+1))%Z) by omega.
destruct cases as [h4 | [h5 | h6]]; auto.
assert (y * div x y <= y * (q - 1))%Z.
 apply  Zmult_le_compat_l; auto with zarith.
replace (y*(q-1))%Z with (q*y - y)%Z in H by ring.
elimtype False.
omega.
assert (y * div x y >= y * (q + 1))%Z.
 apply  Zmult_ge_compat_l; auto with zarith.
replace (y*(q+1))%Z with (q*y + y)%Z in H by ring.
elimtype False.
omega.
Qed.

79
(* Why3 goal *)
80
Lemma Div_bound : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (0%Z < y)%Z) ->
81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98
  ((0%Z <= (div x y))%Z /\ ((div x y) <= x)%Z).
intros x y (Hx,Hy).
unfold div.
case Z_le_dec ; intros H.
split.
apply Z_div_pos with (2 := Hx).
now apply Zlt_gt.
destruct (Z_eq_dec y 1) as [H'|H'].
rewrite H', Zdiv_1_r.
apply Zle_refl.
rewrite <- (Zdiv_1_r x) at 2.
apply Zdiv_le_compat_l with (1 := Hx).
omega.
elim H.
apply Z_mod_lt.
now apply Zlt_gt.
Qed.

99
(* Why3 goal *)
100 101 102 103 104 105 106
Lemma Mod_1 : forall (x:Z), ((mod1 x 1%Z) = 0%Z).
intros x.
unfold mod1, div.
rewrite Zmod_1_r, Zdiv_1_r, Zmult_1_l.
apply Zminus_diag.
Qed.

107
(* Why3 goal *)
108 109 110 111 112
Lemma Div_1 : forall (x:Z), ((div x 1%Z) = x).
intros x.
unfold div.
now rewrite Zmod_1_r, Zdiv_1_r.
Qed.
113 114

(* Why3 goal *)
115
Lemma Div_inf : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (x < y)%Z) -> ((div x
116 117 118 119 120 121 122 123 124
  y) = 0%Z).
intros x y Hxy.
unfold div.
case Z_le_dec ; intros H.
now apply Zdiv_small.
elim H.
now rewrite Zmod_small.
Qed.

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
(* Why3 goal *)
Lemma Div_inf_neg : forall (x:Z) (y:Z), ((0%Z < x)%Z /\ (x <= y)%Z) ->
  ((div (-x)%Z y) = (-1%Z)%Z).
intros x y Hxy.
assert (h: (x < y \/ x = y)%Z) by omega.
destruct h.
(* case 0 < x < y *)
assert (h1: (x mod y = x)%Z).
  rewrite Zmod_small; auto with zarith.
assert (h2: ((-x) mod y = y - x)%Z).
  rewrite Z_mod_nz_opp_full.
  rewrite h1; auto.
rewrite h1; auto with zarith.
unfold div.
case Z_le_dec; auto with zarith.
intros h3.
rewrite Z_div_nz_opp_full; auto with zarith.
rewrite Zdiv_small; auto with zarith.

(* case x = y *)
subst.
assert (h1: (y mod y = 0)%Z).
  rewrite Z_mod_same_full; auto with zarith.
assert (h2: ((-y) mod y = 0)%Z).
  rewrite Z_mod_zero_opp_full; auto with zarith.
unfold div.
case Z_le_dec; rewrite h2; auto with zarith.
intro.
rewrite Z_div_zero_opp_full; auto with zarith.
rewrite Z_div_same_full; auto with zarith.
Qed.

157 158 159 160 161 162 163 164
(* Why3 goal *)
Lemma Mod_0 : forall (y:Z), (~ (y = 0%Z)) -> ((mod1 0%Z y) = 0%Z).
intros y Hy.
unfold mod1, div.
rewrite Zmod_0_l.
simpl.
now rewrite Zdiv_0_l, Zmult_0_r.
Qed.
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 197 198 199 200 201
(* Why3 goal *)
Lemma Div_1_left : forall (y:Z), (1%Z < y)%Z -> ((div 1%Z y) = 0%Z).
intros y Hy.
rewrite Div_inf; auto with zarith.
Qed.

(* Why3 goal *)
Lemma Div_minus1_left : forall (y:Z), (1%Z < y)%Z -> ((div (-1%Z)%Z
  y) = (-1%Z)%Z).
intros y Hy.
unfold div.
assert (h1: (1 mod y = 1)%Z).
apply Zmod_1_l; auto.
assert (h2: ((-(1)) mod y = y-1)%Z).
  rewrite Z_mod_nz_opp_full; auto with zarith.
case Z_le_dec; auto with zarith.
intro.
rewrite Z_div_nz_opp_full; auto with zarith.
rewrite Zdiv_small; auto with zarith.
Qed.

(* Why3 goal *)
Lemma Mod_1_left : forall (y:Z), (1%Z < y)%Z -> ((mod1 1%Z y) = 1%Z).
intros y Hy.
unfold mod1.
rewrite Div_1_left; auto with zarith.
Qed.

(* Why3 goal *)
Lemma Mod_minus1_left : forall (y:Z), (1%Z < y)%Z -> ((mod1 (-1%Z)%Z
  y) = (y - 1%Z)%Z).
intros y Hy.
unfold mod1.
rewrite Div_minus1_left; auto with zarith.
Qed.

202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226
Open Scope Z_scope.

(* Why3 goal *)
Lemma Div_mult : forall (x:Z) (y:Z) (z:Z), (0%Z < x)%Z ->
  ((div ((x * y)%Z + z)%Z x) = (y + (div z x))%Z).
intros x y z h.
unfold div.
destruct (Z_le_dec 0 (z mod x)).
destruct (Z_le_dec 0 ((x*y+z) mod x)).
rewrite Zmult_comm.
rewrite Z_div_plus_full_l; auto with zarith.
generalize (Z_mod_lt (x * y + z) x); auto with zarith.
generalize (Z_mod_lt z x); auto with zarith.
Qed.

(* Why3 goal *)
Lemma Mod_mult : forall (x:Z) (y:Z) (z:Z), (0%Z < x)%Z ->
  ((mod1 ((x * y)%Z + z)%Z x) = (mod1 z x)).
intros x y z h.
unfold mod1.
rewrite Div_mult.
ring.
auto with zarith.
Qed.