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.

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
  | truefun (h2 : P true) ⇒ h1 = h2
  | falsefun (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.

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
  | xHv
  | 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)
  | GtZpos_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)
  | Ox
  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.