Commit 08e24f3a authored by François Bobot's avatar François Bobot

Remove coq proof of computer division to euclidean division since now done in why3

parent e390a42d
(********************************************************************)
(* *)
(* The Why3 Verification Platform / The Why3 Development Team *)
(* Copyright 2010-2019 -- Inria - CNRS - Paris-Sud University *)
(* *)
(* 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. *)
(* *)
(********************************************************************)
(* 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.
Lemma on_pos_euclidean_is_div:
forall n d, (int.EuclideanDivision.div n (Zpos d)) = Zdiv n (Zpos d).
intros n d.
unfold EuclideanDivision.div.
assert (0 < Z.pos d)%Z by reflexivity.
destruct (Z.mod_pos_bound n (Zpos d) H).
case (Z_le_dec 0 (n mod (Zpos d))); intros H2.
* reflexivity.
* destruct (H2 H0).
Qed.
(* Why3 goal *)
Lemma cdiv_cases :
forall (n:Numbers.BinNums.Z) (d:Numbers.BinNums.Z),
((0%Z <= n)%Z -> (0%Z < d)%Z ->
((ZArith.BinInt.Z.quot n d) = (int.EuclideanDivision.div n d))) /\
((n <= 0%Z)%Z -> (0%Z < d)%Z ->
((ZArith.BinInt.Z.quot n d) = (-(int.EuclideanDivision.div (-n)%Z d))%Z)) /\
((0%Z <= n)%Z -> (d < 0%Z)%Z ->
((ZArith.BinInt.Z.quot n d) = (-(int.EuclideanDivision.div n (-d)%Z))%Z)) /\
((n <= 0%Z)%Z -> (d < 0%Z)%Z ->
((ZArith.BinInt.Z.quot n d) = (int.EuclideanDivision.div (-n)%Z (-d)%Z))).
intros n d.
destruct d as [|d|d]; destruct n as [|n|n]; intuition (try contradiction; try discriminate; auto).
+ assert (NZ_d:((Zpos d) <> 0)%Z) by discriminate.
rewrite (Z.quot_div (Z.pos n) (Z.pos d) NZ_d).
rewrite on_pos_euclidean_is_div.
rewrite Z.mul_1_l.
reflexivity.
+ assert (NZ_d:((Zpos d) <> 0)%Z) by discriminate.
rewrite (Z.quot_div (Z.neg n) (Z.pos d) NZ_d).
rewrite on_pos_euclidean_is_div.
reflexivity.
+ assert (NZ_d:((Z.neg d) <> 0)%Z) by discriminate.
rewrite (Z.quot_div (Z.pos n) (Z.neg d) NZ_d).
simpl.
rewrite on_pos_euclidean_is_div.
reflexivity.
+ assert (NZ_d:((Z.neg d) <> 0)%Z) by discriminate.
rewrite (Z.quot_div (Z.neg n) (Z.neg d) NZ_d).
simpl.
rewrite on_pos_euclidean_is_div.
destruct (Z.pos n / Z.pos d)%Z;reflexivity.
Qed.
(* Why3 goal *)
Lemma cmod_cases :
forall (n:Numbers.BinNums.Z) (d:Numbers.BinNums.Z),
((0%Z <= n)%Z -> (0%Z < d)%Z ->
((ZArith.BinInt.Z.rem n d) = (int.EuclideanDivision.mod1 n d))) /\
((n <= 0%Z)%Z -> (0%Z < d)%Z ->
((ZArith.BinInt.Z.rem n d) = (-(int.EuclideanDivision.mod1 (-n)%Z d))%Z)) /\
((0%Z <= n)%Z -> (d < 0%Z)%Z ->
((ZArith.BinInt.Z.rem n d) = (int.EuclideanDivision.mod1 n (-d)%Z))) /\
((n <= 0%Z)%Z -> (d < 0%Z)%Z ->
((ZArith.BinInt.Z.rem n d) =
(-(int.EuclideanDivision.mod1 (-n)%Z (-d)%Z))%Z)).
intros n d.
unfold int.EuclideanDivision.mod1.
assert (Z.rem n d = n - (d * (Z.quot n d)))%Z.
assert (H:= Z.quot_rem' n d).
omega.
rewrite H.
assert (H2:=cdiv_cases n d).
intuition.
+ rewrite H1.
reflexivity.
+ rewrite H4.
rewrite Z.mul_opp_r.
omega.
+ rewrite H1.
rewrite Z.mul_opp_r.
rewrite Z.mul_opp_l.
reflexivity.
+ rewrite H4.
rewrite Z.mul_opp_l.
omega.
Qed.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment