Library Flocq.Core.Fcore_Zaux
This file is part of the Flocq formalization of floating-point
arithmetic in Coq: http://flocq.gforge.inria.fr/
Copyright (C) 2011-2013 Sylvie Boldo
Copyright (C) 2011-2013 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-2013 Guillaume Melquiond
About Z
Theorem Zopp_le_cancel :
∀ x y : Z,
(-y ≤ -x)%Z → Zle 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.
∀ x y : Z,
(-y ≤ -x)%Z → Zle 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.
Zeven, used for rounding to nearest, ties to even
Definition Zeven (n : Z) :=
match n with
| Zpos (xO _) ⇒ true
| Zneg (xO _) ⇒ true
| Z0 ⇒ true
| _ ⇒ false
end.
Theorem Zeven_mult :
∀ x y, Zeven (x × y) = orb (Zeven x) (Zeven y).
Theorem Zeven_opp :
∀ x, Zeven (- x) = Zeven x.
Theorem Zeven_ex :
∀ x, ∃ p, x = (2 × p + if Zeven x then 0 else 1)%Z.
Theorem Zeven_2xp1 :
∀ n, Zeven (2 × n + 1) = false.
Theorem Zeven_plus :
∀ x y, Zeven (x + y) = Bool.eqb (Zeven x) (Zeven y).
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 (Zabs_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 :
∀ b e, (0 < e)%Z →
Zeven (Zpower b e) = Zeven b.
Theorem Zeven_Zpower_odd :
∀ b e, (0 ≤ e)%Z → Zeven b = false →
Zeven (Zpower b e) = false.
match n with
| Zpos (xO _) ⇒ true
| Zneg (xO _) ⇒ true
| Z0 ⇒ true
| _ ⇒ false
end.
Theorem Zeven_mult :
∀ x y, Zeven (x × y) = orb (Zeven x) (Zeven y).
Theorem Zeven_opp :
∀ x, Zeven (- x) = Zeven x.
Theorem Zeven_ex :
∀ x, ∃ p, x = (2 × p + if Zeven x then 0 else 1)%Z.
Theorem Zeven_2xp1 :
∀ n, Zeven (2 × n + 1) = false.
Theorem Zeven_plus :
∀ x y, Zeven (x + y) = Bool.eqb (Zeven x) (Zeven y).
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 (Zabs_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 :
∀ b e, (0 < e)%Z →
Zeven (Zpower b e) = Zeven b.
Theorem Zeven_Zpower_odd :
∀ b e, (0 ≤ e)%Z → Zeven b = false →
Zeven (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.
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 →
(Zdiv (Zmod n (a × b)) a) = Zmod (Zdiv 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,
(Zabs a < b)%Z → Z.quot a b = Z0.
Theorem ZOmod_small_abs :
∀ a b,
(Zabs 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.
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 →
(Zdiv (Zmod n (a × b)) a) = Zmod (Zdiv 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,
(Zabs a < b)%Z → Z.quot a b = Z0.
Theorem ZOmod_small_abs :
∀ a b,
(Zabs 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.
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.
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.
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 (Zcompare x y).
Theorem Zcompare_Lt :
∀ x y,
(x < y)%Z → Zcompare x y = Lt.
Theorem Zcompare_Eq :
∀ x y,
(x = y)%Z → Zcompare x y = Eq.
Theorem Zcompare_Gt :
∀ x y,
(y < x)%Z → Zcompare x y = Gt.
End Zcompare.
Section cond_Zopp.
Definition cond_Zopp (b : bool) m := if b then Zopp m else m.
Theorem abs_cond_Zopp :
∀ b m,
Zabs (cond_Zopp b m) = Zabs m.
Theorem cond_Zopp_Zlt_bool :
∀ m,
cond_Zopp (Zlt_bool m 0) m = Zabs m.
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,
Zdiv_eucl a b = (Zdiv 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, 0)%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, 0)%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 = Zdiv_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).
Fixpoint iter_pos (n : positive) (x : A) {struct n} : A :=
match n with
| xI n' ⇒ iter_pos n' (iter_pos n' (f x))
| xO n' ⇒ iter_pos n' (iter_pos n' x)
| xH ⇒ f x
end.
Lemma iter_pos_nat :
∀ (p : positive) (x : A),
iter_pos p x = iter_nat (Pos.to_nat p) x.
End Iter.