(********************************************************************) (* *) (* The Why3 Verification Platform / The Why3 Development Team *) (* Copyright 2010-2018 -- 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. Require number.Parity. (* Hack so that Why3 does not override the notation below. (* Why3 assumption *) Definition divides (d:Z) (n:Z) : Prop := ((d = 0%Z) -> (n = 0%Z)) /\ (~ (d = 0%Z) -> ((ZArith.BinInt.Z.rem n d) = 0%Z)). *) Require Import Znumtheory. Notation divides := Zdivide (only parsing). (* Why3 goal *) Lemma divides_spec : forall (d:Z) (n:Z), (divides d n) <-> exists q:Z, (n = (q * d)%Z). Proof. intros d n. easy. Qed. (* Why3 goal *) Lemma divides_refl : forall (n:Z), divides n n. Proof. exact Zdivide_refl. Qed. (* Why3 goal *) Lemma divides_1_n : forall (n:Z), divides 1%Z n. Proof. exact Zone_divide. Qed. (* Why3 goal *) Lemma divides_0 : forall (n:Z), divides n 0%Z. Proof. exact Zdivide_0. Qed. (* Why3 goal *) Lemma divides_left : forall (a:Z) (b:Z) (c:Z), (divides a b) -> divides (c * a)%Z (c * b)%Z. Proof. exact Zmult_divide_compat_l. Qed. (* Why3 goal *) Lemma divides_right : forall (a:Z) (b:Z) (c:Z), (divides a b) -> divides (a * c)%Z (b * c)%Z. Proof. exact Zmult_divide_compat_r. Qed. (* Why3 goal *) Lemma divides_oppr : forall (a:Z) (b:Z), (divides a b) -> divides a (-b)%Z. Proof. exact Zdivide_opp_r. Qed. (* Why3 goal *) Lemma divides_oppl : forall (a:Z) (b:Z), (divides a b) -> divides (-a)%Z b. Proof. exact Zdivide_opp_l. Qed. (* Why3 goal *) Lemma divides_oppr_rev : forall (a:Z) (b:Z), (divides (-a)%Z b) -> divides a b. Proof. exact Zdivide_opp_l_rev. Qed. (* Why3 goal *) Lemma divides_oppl_rev : forall (a:Z) (b:Z), (divides a (-b)%Z) -> divides a b. Proof. exact Zdivide_opp_r_rev. Qed. (* Why3 goal *) Lemma divides_plusr : forall (a:Z) (b:Z) (c:Z), (divides a b) -> (divides a c) -> divides a (b + c)%Z. Proof. exact Zdivide_plus_r. Qed. (* Why3 goal *) Lemma divides_minusr : forall (a:Z) (b:Z) (c:Z), (divides a b) -> (divides a c) -> divides a (b - c)%Z. Proof. exact Zdivide_minus_l. Qed. (* Why3 goal *) Lemma divides_multl : forall (a:Z) (b:Z) (c:Z), (divides a b) -> divides a (c * b)%Z. Proof. intros a b c. apply Zdivide_mult_r. Qed. (* Why3 goal *) Lemma divides_multr : forall (a:Z) (b:Z) (c:Z), (divides a b) -> divides a (b * c)%Z. Proof. exact Zdivide_mult_l. Qed. (* Why3 goal *) Lemma divides_factorl : forall (a:Z) (b:Z), divides a (b * a)%Z. Proof. exact Zdivide_factor_l. Qed. (* Why3 goal *) Lemma divides_factorr : forall (a:Z) (b:Z), divides a (a * b)%Z. Proof. exact Zdivide_factor_r. Qed. (* Why3 goal *) Lemma divides_n_1 : forall (n:Z), (divides n 1%Z) -> (n = 1%Z) \/ (n = (-1%Z)%Z). Proof. exact Zdivide_1. Qed. (* Why3 goal *) Lemma divides_antisym : forall (a:Z) (b:Z), (divides a b) -> (divides b a) -> (a = b) \/ (a = (-b)%Z). Proof. exact Zdivide_antisym. Qed. (* Why3 goal *) Lemma divides_trans : forall (a:Z) (b:Z) (c:Z), (divides a b) -> (divides b c) -> divides a c. Proof. exact Zdivide_trans. Qed. (* Why3 goal *) 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). Proof. exact Zdivide_bounds. Qed. Import EuclideanDivision. (* Why3 goal *) Lemma mod_divides_euclidean : forall (a:Z) (b:Z), ~ (b = 0%Z) -> ((int.EuclideanDivision.mod1 a b) = 0%Z) -> divides b a. Proof. intros a b Zb H. exists (div a b). rewrite (Div_mod a b Zb) at 1. rewrite H. ring. Qed. (* Why3 goal *) Lemma divides_mod_euclidean : forall (a:Z) (b:Z), ~ (b = 0%Z) -> (divides b a) -> ((int.EuclideanDivision.mod1 a b) = 0%Z). 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 *) Lemma mod_divides_computer : forall (a:Z) (b:Z), ~ (b = 0%Z) -> ((ZArith.BinInt.Z.rem a b) = 0%Z) -> divides b a. Proof. intros a b Zb H. exists (Z.quot a b). rewrite Zmult_comm. now apply Zquot.Z_quot_exact_full. Qed. (* Why3 goal *) Lemma divides_mod_computer : forall (a:Z) (b:Z), ~ (b = 0%Z) -> (divides b a) -> ((ZArith.BinInt.Z.rem a b) = 0%Z). Proof. intros a b Zb (q,H). rewrite H. apply Zquot.Z_rem_mult. Qed. (* Why3 goal *) Lemma even_divides : forall (a:Z), (number.Parity.even a) <-> (divides 2%Z a). Proof. split ; intros (q,H) ; exists q ; now rewrite Zmult_comm. Qed. (* Why3 goal *) Lemma odd_divides : forall (a:Z), (number.Parity.odd a) <-> ~ (divides 2%Z a). 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.