euler001_DivModHints_mod_succ_1_1.v 1.07 KB
Newer Older
1
(* This file is generated by Why3's Coq 8.4 driver *)
MARCHE Claude's avatar
MARCHE Claude committed
2
(* Beware! Only edit allowed sections below    *)
3
Require Import BuiltIn.
MARCHE Claude's avatar
MARCHE Claude committed
4
Require Import ZOdiv.
5 6 7 8
Require BuiltIn.
Require int.Int.
Require int.Abs.
Require int.ComputerDivision.
MARCHE Claude's avatar
MARCHE Claude committed
9

10 11 12
Axiom mod_div_unique : forall (x:Z) (y:Z) (q:Z) (r:Z), ((0%Z <= x)%Z /\
  ((0%Z < y)%Z /\ ((x = ((q * y)%Z + r)%Z) /\ ((0%Z <= r)%Z /\
  (r < y)%Z)))) -> ((q = (ZOdiv x y)) /\ (r = (ZOmod x y))).
MARCHE Claude's avatar
MARCHE Claude committed
13 14 15

Open Scope Z_scope.

16 17
(* Why3 goal *)
Theorem mod_succ_1 : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (0%Z < y)%Z) ->
MARCHE Claude's avatar
MARCHE Claude committed
18 19
  ((~ ((ZOmod (x + 1%Z)%Z y) = 0%Z)) ->
  ((ZOmod (x + 1%Z)%Z y) = ((ZOmod x y) + 1%Z)%Z)).
20
(* Why3 intros x y (h1,h2) h3. *)
MARCHE Claude's avatar
MARCHE Claude committed
21 22 23 24
intros x y (Hx,Hy) H.
assert (h: y>0) by omega.
generalize (ZO_div_mod_eq x y); intro h1.
generalize (ZO_div_mod_eq (x+1) y); intro h2.
25 26
assert (h3:x = y * (ZOdiv (x + 1) y) + (ZOmod (x + 1) y - 1)) by omega.
generalize (mod_div_unique x y (ZOdiv (x + 1) y) (ZOmod (x + 1) y - 1)).
MARCHE Claude's avatar
MARCHE Claude committed
27
intuition.
28
destruct H1 ; auto with zarith.
MARCHE Claude's avatar
MARCHE Claude committed
29 30
rewrite h3 at 1.
ring.
31 32
assert (0 <= ZOmod (x + 1) y < y).
  apply Zquot.Zrem_lt_pos_pos; omega.
MARCHE Claude's avatar
MARCHE Claude committed
33 34 35 36
omega.
Qed.