euler001_DivModHints_mod_succ_1_1.v 1.07 KB
 Guillaume Melquiond committed Aug 20, 2013 1 ``````(* This file is generated by Why3's Coq 8.4 driver *) `````` MARCHE Claude committed Sep 29, 2011 2 ``````(* Beware! Only edit allowed sections below *) `````` Guillaume Melquiond committed Aug 20, 2013 3 ``````Require Import BuiltIn. `````` MARCHE Claude committed Sep 29, 2011 4 ``````Require Import ZOdiv. `````` Guillaume Melquiond committed Aug 20, 2013 5 6 7 8 ``````Require BuiltIn. Require int.Int. Require int.Abs. Require int.ComputerDivision. `````` MARCHE Claude committed Sep 29, 2011 9 `````` `````` Guillaume Melquiond committed Aug 20, 2013 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 committed Sep 29, 2011 13 14 15 `````` Open Scope Z_scope. `````` Guillaume Melquiond committed Aug 20, 2013 16 17 ``````(* Why3 goal *) Theorem mod_succ_1 : forall (x:Z) (y:Z), ((0%Z <= x)%Z /\ (0%Z < y)%Z) -> `````` MARCHE Claude committed Sep 29, 2011 18 19 `````` ((~ ((ZOmod (x + 1%Z)%Z y) = 0%Z)) -> ((ZOmod (x + 1%Z)%Z y) = ((ZOmod x y) + 1%Z)%Z)). `````` Guillaume Melquiond committed Aug 20, 2013 20 ``````(* Why3 intros x y (h1,h2) h3. *) `````` MARCHE Claude committed Sep 29, 2011 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. `````` Guillaume Melquiond committed Aug 20, 2013 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 committed Sep 29, 2011 27 ``````intuition. `````` Guillaume Melquiond committed Aug 20, 2013 28 ``````destruct H1 ; auto with zarith. `````` MARCHE Claude committed Sep 29, 2011 29 30 ``````rewrite h3 at 1. ring. `````` Guillaume Melquiond committed Aug 20, 2013 31 32 ``````assert (0 <= ZOmod (x + 1) y < y). apply Zquot.Zrem_lt_pos_pos; omega. `````` MARCHE Claude committed Sep 29, 2011 33 34 35 36 ``````omega. Qed. ``````