Library Flocq.Core.Zaux
This file is part of the Flocq formalization of floating-point
arithmetic in Coq: https://flocq.gitlabpages.inria.fr/
Copyright (C) 2011-2018 Sylvie Boldo
Copyright (C) 2011-2018 Guillaume Melquiond
This library is free software; you can redistribute it and/or
modify it under the terms of the GNU Lesser General Public
License as published by the Free Software Foundation; either
version 3 of the License, or (at your option) any later version.
This library is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
COPYING file for more details.
Copyright (C) 2011-2018 Guillaume Melquiond
From Coq Require Import ZArith Lia Zquot.
From Coq Require SpecFloat.
Notation cond_Zopp := SpecFloat.cond_Zopp (only parsing).
Notation iter_pos := SpecFloat.iter_pos (only parsing).
Section Zmissing.
About Z
Theorem Zopp_le_cancel :
∀ x y : Z,
(-y ≤ -x)%Z → Z.le x y.
Theorem Zgt_not_eq :
∀ x y : Z,
(y < x)%Z → (x ≠ y)%Z.
End Zmissing.
Section Proof_Irrelevance.
Scheme eq_dep_elim := Induction for eq Sort Type.
Definition eqbool_dep P (h1 : P true) b :=
match b return P b → Prop with
| true ⇒ fun (h2 : P true) ⇒ h1 = h2
| false ⇒ fun (h2 : P false) ⇒ False
end.
Lemma eqbool_irrelevance : ∀ (b : bool) (h1 h2 : b = true), h1 = h2.
End Proof_Irrelevance.
Section Even_Odd.
Theorem Zeven_ex :
∀ x, ∃ p, x = (2 × p + if Z.even x then 0 else 1)%Z.
End Even_Odd.
Section Zpower.
Theorem Zpower_plus :
∀ n k1 k2, (0 ≤ k1)%Z → (0 ≤ k2)%Z →
Zpower n (k1 + k2) = (Zpower n k1 × Zpower n k2)%Z.
Theorem Zpower_Zpower_nat :
∀ b e, (0 ≤ e)%Z →
Zpower b e = Zpower_nat b (Z.abs_nat e).
Theorem Zpower_nat_S :
∀ b e,
Zpower_nat b (S e) = (b × Zpower_nat b e)%Z.
Theorem Zpower_pos_gt_0 :
∀ b p, (0 < b)%Z →
(0 < Zpower_pos b p)%Z.
Theorem Zeven_Zpower_odd :
∀ b e, (0 ≤ e)%Z → Z.even b = false →
Z.even (Zpower b e) = false.
∀ x y : Z,
(-y ≤ -x)%Z → Z.le x y.
Theorem Zgt_not_eq :
∀ x y : Z,
(y < x)%Z → (x ≠ y)%Z.
End Zmissing.
Section Proof_Irrelevance.
Scheme eq_dep_elim := Induction for eq Sort Type.
Definition eqbool_dep P (h1 : P true) b :=
match b return P b → Prop with
| true ⇒ fun (h2 : P true) ⇒ h1 = h2
| false ⇒ fun (h2 : P false) ⇒ False
end.
Lemma eqbool_irrelevance : ∀ (b : bool) (h1 h2 : b = true), h1 = h2.
End Proof_Irrelevance.
Section Even_Odd.
Theorem Zeven_ex :
∀ x, ∃ p, x = (2 × p + if Z.even x then 0 else 1)%Z.
End Even_Odd.
Section Zpower.
Theorem Zpower_plus :
∀ n k1 k2, (0 ≤ k1)%Z → (0 ≤ k2)%Z →
Zpower n (k1 + k2) = (Zpower n k1 × Zpower n k2)%Z.
Theorem Zpower_Zpower_nat :
∀ b e, (0 ≤ e)%Z →
Zpower b e = Zpower_nat b (Z.abs_nat e).
Theorem Zpower_nat_S :
∀ b e,
Zpower_nat b (S e) = (b × Zpower_nat b e)%Z.
Theorem Zpower_pos_gt_0 :
∀ b p, (0 < b)%Z →
(0 < Zpower_pos b p)%Z.
Theorem Zeven_Zpower_odd :
∀ b e, (0 ≤ e)%Z → Z.even b = false →
Z.even (Zpower b e) = false.
The radix must be greater than 1
Record radix := { radix_val :> Z ; radix_prop : Zle_bool 2 radix_val = true }.
Theorem radix_val_inj :
∀ r1 r2, radix_val r1 = radix_val r2 → r1 = r2.
Definition radix2 := Build_radix 2 (refl_equal _).
Variable r : radix.
Theorem radix_gt_0 : (0 < r)%Z.
Theorem radix_gt_1 : (1 < r)%Z.
Theorem Zpower_gt_1 :
∀ p,
(0 < p)%Z →
(1 < Zpower r p)%Z.
Theorem Zpower_gt_0 :
∀ p,
(0 ≤ p)%Z →
(0 < Zpower r p)%Z.
Theorem Zpower_ge_0 :
∀ e,
(0 ≤ Zpower r e)%Z.
Theorem Zpower_le :
∀ e1 e2, (e1 ≤ e2)%Z →
(Zpower r e1 ≤ Zpower r e2)%Z.
Theorem Zpower_lt :
∀ e1 e2, (0 ≤ e2)%Z → (e1 < e2)%Z →
(Zpower r e1 < Zpower r e2)%Z.
Theorem Zpower_lt_Zpower :
∀ e1 e2,
(Zpower r (e1 - 1) < Zpower r e2)%Z →
(e1 ≤ e2)%Z.
Theorem Zpower_gt_id :
∀ n, (n < Zpower r n)%Z.
End Zpower.
Section Div_Mod.
Theorem Zmod_mod_mult :
∀ n a b, (0 < a)%Z → (0 ≤ b)%Z →
Zmod (Zmod n (a × b)) b = Zmod n b.
Theorem ZOmod_eq :
∀ a b,
Z.rem a b = (a - Z.quot a b × b)%Z.
Theorem ZOmod_mod_mult :
∀ n a b,
Z.rem (Z.rem n (a × b)) b = Z.rem n b.
Theorem Zdiv_mod_mult :
∀ n a b, (0 ≤ a)%Z → (0 ≤ b)%Z →
(Z.div (Zmod n (a × b)) a) = Zmod (Z.div n a) b.
Theorem ZOdiv_mod_mult :
∀ n a b,
(Z.quot (Z.rem n (a × b)) a) = Z.rem (Z.quot n a) b.
Theorem ZOdiv_small_abs :
∀ a b,
(Z.abs a < b)%Z → Z.quot a b = Z0.
Theorem ZOmod_small_abs :
∀ a b,
(Z.abs a < b)%Z → Z.rem a b = a.
Theorem ZOdiv_plus :
∀ a b c, (0 ≤ a × b)%Z →
(Z.quot (a + b) c = Z.quot a c + Z.quot b c + Z.quot (Z.rem a c + Z.rem b c) c)%Z.
End Div_Mod.
Section Same_sign.
Theorem Zsame_sign_trans :
∀ v u w, v ≠ Z0 →
(0 ≤ u × v)%Z → (0 ≤ v × w)%Z → (0 ≤ u × w)%Z.
Theorem Zsame_sign_trans_weak :
∀ v u w, (v = Z0 → w = Z0) →
(0 ≤ u × v)%Z → (0 ≤ v × w)%Z → (0 ≤ u × w)%Z.
Theorem Zsame_sign_imp :
∀ u v,
(0 < u → 0 ≤ v)%Z →
(0 < -u → 0 ≤ -v)%Z →
(0 ≤ u × v)%Z.
Theorem Zsame_sign_odiv :
∀ u v, (0 ≤ v)%Z →
(0 ≤ u × Z.quot u v)%Z.
End Same_sign.
Theorem radix_val_inj :
∀ r1 r2, radix_val r1 = radix_val r2 → r1 = r2.
Definition radix2 := Build_radix 2 (refl_equal _).
Variable r : radix.
Theorem radix_gt_0 : (0 < r)%Z.
Theorem radix_gt_1 : (1 < r)%Z.
Theorem Zpower_gt_1 :
∀ p,
(0 < p)%Z →
(1 < Zpower r p)%Z.
Theorem Zpower_gt_0 :
∀ p,
(0 ≤ p)%Z →
(0 < Zpower r p)%Z.
Theorem Zpower_ge_0 :
∀ e,
(0 ≤ Zpower r e)%Z.
Theorem Zpower_le :
∀ e1 e2, (e1 ≤ e2)%Z →
(Zpower r e1 ≤ Zpower r e2)%Z.
Theorem Zpower_lt :
∀ e1 e2, (0 ≤ e2)%Z → (e1 < e2)%Z →
(Zpower r e1 < Zpower r e2)%Z.
Theorem Zpower_lt_Zpower :
∀ e1 e2,
(Zpower r (e1 - 1) < Zpower r e2)%Z →
(e1 ≤ e2)%Z.
Theorem Zpower_gt_id :
∀ n, (n < Zpower r n)%Z.
End Zpower.
Section Div_Mod.
Theorem Zmod_mod_mult :
∀ n a b, (0 < a)%Z → (0 ≤ b)%Z →
Zmod (Zmod n (a × b)) b = Zmod n b.
Theorem ZOmod_eq :
∀ a b,
Z.rem a b = (a - Z.quot a b × b)%Z.
Theorem ZOmod_mod_mult :
∀ n a b,
Z.rem (Z.rem n (a × b)) b = Z.rem n b.
Theorem Zdiv_mod_mult :
∀ n a b, (0 ≤ a)%Z → (0 ≤ b)%Z →
(Z.div (Zmod n (a × b)) a) = Zmod (Z.div n a) b.
Theorem ZOdiv_mod_mult :
∀ n a b,
(Z.quot (Z.rem n (a × b)) a) = Z.rem (Z.quot n a) b.
Theorem ZOdiv_small_abs :
∀ a b,
(Z.abs a < b)%Z → Z.quot a b = Z0.
Theorem ZOmod_small_abs :
∀ a b,
(Z.abs a < b)%Z → Z.rem a b = a.
Theorem ZOdiv_plus :
∀ a b c, (0 ≤ a × b)%Z →
(Z.quot (a + b) c = Z.quot a c + Z.quot b c + Z.quot (Z.rem a c + Z.rem b c) c)%Z.
End Div_Mod.
Section Same_sign.
Theorem Zsame_sign_trans :
∀ v u w, v ≠ Z0 →
(0 ≤ u × v)%Z → (0 ≤ v × w)%Z → (0 ≤ u × w)%Z.
Theorem Zsame_sign_trans_weak :
∀ v u w, (v = Z0 → w = Z0) →
(0 ≤ u × v)%Z → (0 ≤ v × w)%Z → (0 ≤ u × w)%Z.
Theorem Zsame_sign_imp :
∀ u v,
(0 < u → 0 ≤ v)%Z →
(0 < -u → 0 ≤ -v)%Z →
(0 ≤ u × v)%Z.
Theorem Zsame_sign_odiv :
∀ u v, (0 ≤ v)%Z →
(0 ≤ u × Z.quot u v)%Z.
End Same_sign.
Boolean comparisons
Section Zeq_bool.
Inductive Zeq_bool_prop (x y : Z) : bool → Prop :=
| Zeq_bool_true_ : x = y → Zeq_bool_prop x y true
| Zeq_bool_false_ : x ≠ y → Zeq_bool_prop x y false.
Theorem Zeq_bool_spec :
∀ x y, Zeq_bool_prop x y (Zeq_bool x y).
Theorem Zeq_bool_true :
∀ x y, x = y → Zeq_bool x y = true.
Theorem Zeq_bool_false :
∀ x y, x ≠ y → Zeq_bool x y = false.
Theorem Zeq_bool_diag :
∀ x, Zeq_bool x x = true.
Theorem Zeq_bool_opp :
∀ x y,
Zeq_bool (Z.opp x) y = Zeq_bool x (Z.opp y).
Theorem Zeq_bool_opp' :
∀ x y,
Zeq_bool (Z.opp x) (Z.opp y) = Zeq_bool x y.
End Zeq_bool.
Section Zle_bool.
Inductive Zle_bool_prop (x y : Z) : bool → Prop :=
| Zle_bool_true_ : (x ≤ y)%Z → Zle_bool_prop x y true
| Zle_bool_false_ : (y < x)%Z → Zle_bool_prop x y false.
Theorem Zle_bool_spec :
∀ x y, Zle_bool_prop x y (Zle_bool x y).
Theorem Zle_bool_true :
∀ x y : Z,
(x ≤ y)%Z → Zle_bool x y = true.
Theorem Zle_bool_false :
∀ x y : Z,
(y < x)%Z → Zle_bool x y = false.
Theorem Zle_bool_opp_l :
∀ x y,
Zle_bool (Z.opp x) y = Zle_bool (Z.opp y) x.
Theorem Zle_bool_opp :
∀ x y,
Zle_bool (Z.opp x) (Z.opp y) = Zle_bool y x.
Theorem Zle_bool_opp_r :
∀ x y,
Zle_bool x (Z.opp y) = Zle_bool y (Z.opp x).
End Zle_bool.
Section Zlt_bool.
Inductive Zlt_bool_prop (x y : Z) : bool → Prop :=
| Zlt_bool_true_ : (x < y)%Z → Zlt_bool_prop x y true
| Zlt_bool_false_ : (y ≤ x)%Z → Zlt_bool_prop x y false.
Theorem Zlt_bool_spec :
∀ x y, Zlt_bool_prop x y (Zlt_bool x y).
Theorem Zlt_bool_true :
∀ x y : Z,
(x < y)%Z → Zlt_bool x y = true.
Theorem Zlt_bool_false :
∀ x y : Z,
(y ≤ x)%Z → Zlt_bool x y = false.
Theorem negb_Zle_bool :
∀ x y : Z,
negb (Zle_bool x y) = Zlt_bool y x.
Theorem negb_Zlt_bool :
∀ x y : Z,
negb (Zlt_bool x y) = Zle_bool y x.
Theorem Zlt_bool_opp_l :
∀ x y,
Zlt_bool (Z.opp x) y = Zlt_bool (Z.opp y) x.
Theorem Zlt_bool_opp_r :
∀ x y,
Zlt_bool x (Z.opp y) = Zlt_bool y (Z.opp x).
Theorem Zlt_bool_opp :
∀ x y,
Zlt_bool (Z.opp x) (Z.opp y) = Zlt_bool y x.
End Zlt_bool.
Section Zcompare.
Inductive Zcompare_prop (x y : Z) : comparison → Prop :=
| Zcompare_Lt_ : (x < y)%Z → Zcompare_prop x y Lt
| Zcompare_Eq_ : x = y → Zcompare_prop x y Eq
| Zcompare_Gt_ : (y < x)%Z → Zcompare_prop x y Gt.
Theorem Zcompare_spec :
∀ x y, Zcompare_prop x y (Z.compare x y).
Theorem Zcompare_Lt :
∀ x y,
(x < y)%Z → Z.compare x y = Lt.
Theorem Zcompare_Eq :
∀ x y,
(x = y)%Z → Z.compare x y = Eq.
Theorem Zcompare_Gt :
∀ x y,
(y < x)%Z → Z.compare x y = Gt.
End Zcompare.
Section cond_Zopp.
Theorem cond_Zopp_0 :
∀ sx, cond_Zopp sx 0 = 0%Z.
Theorem cond_Zopp_negb :
∀ x y, cond_Zopp (negb x) y = Z.opp (cond_Zopp x y).
Theorem abs_cond_Zopp :
∀ b m,
Z.abs (cond_Zopp b m) = Z.abs m.
Theorem cond_Zopp_Zlt_bool :
∀ m,
cond_Zopp (Zlt_bool m 0) m = Z.abs m.
Theorem Zeq_bool_cond_Zopp :
∀ s m n,
Zeq_bool (cond_Zopp s m) n = Zeq_bool m (cond_Zopp s n).
End cond_Zopp.
Section fast_pow_pos.
Fixpoint Zfast_pow_pos (v : Z) (e : positive) : Z :=
match e with
| xH ⇒ v
| xO e' ⇒ Z.square (Zfast_pow_pos v e')
| xI e' ⇒ Zmult v (Z.square (Zfast_pow_pos v e'))
end.
Theorem Zfast_pow_pos_correct :
∀ v e, Zfast_pow_pos v e = Zpower_pos v e.
End fast_pow_pos.
Section faster_div.
Lemma Zdiv_eucl_unique :
∀ a b,
Z.div_eucl a b = (Z.div a b, Zmod a b).
Fixpoint Zpos_div_eucl_aux1 (a b : positive) {struct b} :=
match b with
| xO b' ⇒
match a with
| xO a' ⇒ let (q, r) := Zpos_div_eucl_aux1 a' b' in (q, 2 × r)%Z
| xI a' ⇒ let (q, r) := Zpos_div_eucl_aux1 a' b' in (q, 2 × r + 1)%Z
| xH ⇒ (Z0, Zpos a)
end
| xH ⇒ (Zpos a, Z0)
| xI _ ⇒ Z.pos_div_eucl a (Zpos b)
end.
Lemma Zpos_div_eucl_aux1_correct :
∀ a b,
Zpos_div_eucl_aux1 a b = Z.pos_div_eucl a (Zpos b).
Definition Zpos_div_eucl_aux (a b : positive) :=
match Pos.compare a b with
| Lt ⇒ (Z0, Zpos a)
| Eq ⇒ (1%Z, Z0)
| Gt ⇒ Zpos_div_eucl_aux1 a b
end.
Lemma Zpos_div_eucl_aux_correct :
∀ a b,
Zpos_div_eucl_aux a b = Z.pos_div_eucl a (Zpos b).
Definition Zfast_div_eucl (a b : Z) :=
match a with
| Z0 ⇒ (0, 0)%Z
| Zpos a' ⇒
match b with
| Z0 ⇒ (0, (match (1 mod 0) with | 0 ⇒ 0 | _ ⇒ a end))%Z
| Zpos b' ⇒ Zpos_div_eucl_aux a' b'
| Zneg b' ⇒
let (q, r) := Zpos_div_eucl_aux a' b' in
match r with
| Z0 ⇒ (-q, 0)%Z
| Zpos _ ⇒ (-(q + 1), (b + r))%Z
| Zneg _ ⇒ (-(q + 1), (b + r))%Z
end
end
| Zneg a' ⇒
match b with
| Z0 ⇒ (0, (match (1 mod 0) with | 0 ⇒ 0 | _ ⇒ a end))%Z
| Zpos b' ⇒
let (q, r) := Zpos_div_eucl_aux a' b' in
match r with
| Z0 ⇒ (-q, 0)%Z
| Zpos _ ⇒ (-(q + 1), (b - r))%Z
| Zneg _ ⇒ (-(q + 1), (b - r))%Z
end
| Zneg b' ⇒ let (q, r) := Zpos_div_eucl_aux a' b' in (q, (-r)%Z)
end
end.
Theorem Zfast_div_eucl_correct :
∀ a b : Z,
Zfast_div_eucl a b = Z.div_eucl a b.
End faster_div.
Section Iter.
Context {A : Type}.
Variable (f : A → A).
Fixpoint iter_nat (n : nat) (x : A) {struct n} : A :=
match n with
| S n' ⇒ iter_nat n' (f x)
| O ⇒ x
end.
Lemma iter_nat_plus :
∀ (p q : nat) (x : A),
iter_nat (p + q) x = iter_nat p (iter_nat q x).
Lemma iter_nat_S :
∀ (p : nat) (x : A),
iter_nat (S p) x = f (iter_nat p x).
Lemma iter_pos_nat :
∀ (p : positive) (x : A),
iter_pos f p x = iter_nat (Pos.to_nat p) x.
End Iter.