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 Sylvie Boldo
Copyright (C) 2011 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.

Require Import ZArith.
Require Import ZOdiv.

Section Zmissing.

About Z
Theorem Zopp_le_cancel :
  forall x y : Z,
  (-y <= -x)%Z -> Zle x y.

Theorem Zgt_not_eq :
  forall 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 : forall (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 :
  forall x y, Zeven (x * y) = orb (Zeven x) (Zeven y).

Theorem Zeven_opp :
  forall x, Zeven (- x) = Zeven x.

Theorem Zeven_ex :
  forall x, exists p, x = (2 * p + if Zeven x then 0 else 1)%Z.

Theorem Zeven_2xp1 :
  forall n, Zeven (2 * n + 1) = false.

Theorem Zeven_plus :
  forall x y, Zeven (x + y) = Bool.eqb (Zeven x) (Zeven y).

End Even_Odd.

Section Zpower.

Theorem Zpower_plus :
  forall n k1 k2, (0 <= k1)%Z -> (0 <= k2)%Z ->
  Zpower n (k1 + k2) = (Zpower n k1 * Zpower n k2)%Z.

Theorem Zpower_Zpower_nat :
  forall b e, (0 <= e)%Z ->
  Zpower b e = Zpower_nat b (Zabs_nat e).

Theorem Zpower_nat_S :
  forall b e,
  Zpower_nat b (S e) = (b * Zpower_nat b e)%Z.

Theorem Zpower_pos_gt_0 :
  forall b p, (0 < b)%Z ->
  (0 < Zpower_pos b p)%Z.

Theorem Zeven_Zpower :
  forall b e, (0 < e)%Z ->
  Zeven (Zpower b e) = Zeven b.

Theorem Zeven_Zpower_odd :
  forall 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 :
  forall r1 r2, radix_val r1 = radix_val r2 -> r1 = r2.

Variable r : radix.

Theorem radix_gt_0 : (0 < r)%Z.

Theorem radix_gt_1 : (1 < r)%Z.

Theorem Zpower_gt_1 :
  forall p,
  (0 < p)%Z ->
  (1 < Zpower r p)%Z.

Theorem Zpower_gt_0 :
  forall p,
  (0 <= p)%Z ->
  (0 < Zpower r p)%Z.

Theorem Zpower_ge_0 :
  forall e,
  (0 <= Zpower r e)%Z.

Theorem Zpower_le :
  forall e1 e2, (e1 <= e2)%Z ->
  (Zpower r e1 <= Zpower r e2)%Z.

Theorem Zpower_lt :
  forall e1 e2, (0 <= e2)%Z -> (e1 < e2)%Z ->
  (Zpower r e1 < Zpower r e2)%Z.

Theorem Zpower_lt_Zpower :
  forall e1 e2,
  (Zpower r (e1 - 1) < Zpower r e2)%Z ->
  (e1 <= e2)%Z.

End Zpower.

Section Div_Mod.

Theorem Zmod_mod_mult :
  forall n a b, (0 < a)%Z -> (0 <= b)%Z ->
  Zmod (Zmod n (a * b)) b = Zmod n b.

Theorem ZOmod_eq :
  forall a b,
  ZOmod a b = (a - ZOdiv a b * b)%Z.

Theorem ZOmod_mod_mult :
  forall n a b,
  ZOmod (ZOmod n (a * b)) b = ZOmod n b.

Theorem Zdiv_mod_mult :
  forall n a b, (0 <= a)%Z -> (0 <= b)%Z ->
  (Zdiv (Zmod n (a * b)) a) = Zmod (Zdiv n a) b.

Theorem ZOdiv_mod_mult :
  forall n a b,
  (ZOdiv (ZOmod n (a * b)) a) = ZOmod (ZOdiv n a) b.

Theorem ZOdiv_small_abs :
  forall a b,
  (Zabs a < b)%Z -> ZOdiv a b = Z0.

Theorem ZOmod_small_abs :
  forall a b,
  (Zabs a < b)%Z -> ZOmod a b = a.

Theorem ZOdiv_plus :
  forall a b c, (0 <= a * b)%Z ->
  (ZOdiv (a + b) c = ZOdiv a c + ZOdiv b c + ZOdiv (ZOmod a c + ZOmod b c) c)%Z.

End Div_Mod.

Section Same_sign.

Theorem Zsame_sign_trans :
  forall v u w, v <> Z0 ->
  (0 <= u * v)%Z -> (0 <= v * w)%Z -> (0 <= u * w)%Z.

Theorem Zsame_sign_trans_weak :
  forall v u w, (v = Z0 -> w = Z0) ->
  (0 <= u * v)%Z -> (0 <= v * w)%Z -> (0 <= u * w)%Z.

Theorem Zsame_sign_imp :
  forall u v,
  (0 < u -> 0 <= v)%Z ->
  (0 < -u -> 0 <= -v)%Z ->
  (0 <= u * v)%Z.

Theorem Zsame_sign_odiv :
  forall u v, (0 <= v)%Z ->
  (0 <= u * ZOdiv 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 :
  forall x y, Zeq_bool_prop x y (Zeq_bool x y).

Theorem Zeq_bool_true :
  forall x y, x = y -> Zeq_bool x y = true.

Theorem Zeq_bool_false :
  forall 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 :
  forall x y, Zle_bool_prop x y (Zle_bool x y).

Theorem Zle_bool_true :
  forall x y : Z,
  (x <= y)%Z -> Zle_bool x y = true.

Theorem Zle_bool_false :
  forall 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 :
  forall x y, Zlt_bool_prop x y (Zlt_bool x y).

Theorem Zlt_bool_true :
  forall x y : Z,
  (x < y)%Z -> Zlt_bool x y = true.

Theorem Zlt_bool_false :
  forall x y : Z,
  (y <= x)%Z -> Zlt_bool x y = false.

Theorem negb_Zle_bool :
  forall x y : Z,
  negb (Zle_bool x y) = Zlt_bool y x.

Theorem negb_Zlt_bool :
  forall 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 :
  forall x y, Zcompare_prop x y (Zcompare x y).

Theorem Zcompare_Lt :
  forall x y,
  (x < y)%Z -> Zcompare x y = Lt.

Theorem Zcompare_Eq :
  forall x y,
  (x = y)%Z -> Zcompare x y = Eq.

Theorem Zcompare_Gt :
  forall x y,
  (y < x)%Z -> Zcompare x y = Gt.

End Zcompare.