Commit b6bc4d4e authored by Guillaume Melquiond's avatar Guillaume Melquiond

Move theorems about integers in their own file.

parent e1a849c5
......@@ -20,6 +20,7 @@ COPYING file for more details.
(** * Missing definitions/lemmas *)
Require Export Reals.
Require Export ZArith.
Require Export Fcore_Zaux.
Section Rmissing.
......@@ -305,47 +306,6 @@ Qed.
End Rmissing.
Section Zmissing.
(** About Z *)
Theorem Zopp_le_cancel :
forall x y : Z,
(-y <= -x)%Z -> Zle x y.
Proof.
intros x y Hxy.
apply Zplus_le_reg_r with (-x - y)%Z.
now ring_simplify.
Qed.
Theorem Zgt_not_eq :
forall x y : Z,
(y < x)%Z -> (x <> y)%Z.
Proof.
intros x y H Hn.
apply Zlt_irrefl with x.
now rewrite Hn at 1.
Qed.
Theorem Zmin_left :
forall x y : Z,
(x <= y)%Z -> Zmin x y = x.
Proof.
intros x y.
generalize (Zmin_spec x y).
omega.
Qed.
Theorem Zmin_right :
forall x y : Z,
(y <= x)%Z -> Zmin x y = y.
Proof.
intros x y.
generalize (Zmin_spec x y).
omega.
Qed.
End Zmissing.
Section Z2R.
(** Z2R function (Z -> R) *)
......@@ -525,196 +485,6 @@ Qed.
End Z2R.
(** Useful 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).
Proof.
intros x y.
generalize (Zeq_is_eq_bool x y).
case (Zeq_bool x y) ; intros (H1, H2) ; constructor.
now apply H2.
intros H.
specialize (H1 H).
discriminate H1.
Qed.
Theorem Zeq_bool_true :
forall x y, x = y -> Zeq_bool x y = true.
Proof.
intros x y.
apply -> Zeq_is_eq_bool.
Qed.
Theorem Zeq_bool_false :
forall x y, x <> y -> Zeq_bool x y = false.
Proof.
intros x y.
generalize (proj2 (Zeq_is_eq_bool x y)).
case Zeq_bool.
intros He Hn.
elim Hn.
now apply He.
now intros _ _.
Qed.
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).
Proof.
intros x y.
generalize (Zle_is_le_bool x y).
case Zle_bool ; intros (H1, H2) ; constructor.
now apply H2.
destruct (Zle_or_lt x y) as [H|H].
now specialize (H1 H).
exact H.
Qed.
Theorem Zle_bool_true :
forall x y : Z,
(x <= y)%Z -> Zle_bool x y = true.
Proof.
intros x y.
apply (proj1 (Zle_is_le_bool x y)).
Qed.
Theorem Zle_bool_false :
forall x y : Z,
(y < x)%Z -> Zle_bool x y = false.
Proof.
intros x y Hxy.
generalize (Zle_cases x y).
case Zle_bool ; intros H.
elim (Zlt_irrefl x).
now apply Zle_lt_trans with y.
apply refl_equal.
Qed.
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).
Proof.
intros x y.
generalize (Zlt_is_lt_bool x y).
case Zlt_bool ; intros (H1, H2) ; constructor.
now apply H2.
destruct (Zle_or_lt y x) as [H|H].
exact H.
now specialize (H1 H).
Qed.
Theorem Zlt_bool_true :
forall x y : Z,
(x < y)%Z -> Zlt_bool x y = true.
Proof.
intros x y.
apply (proj1 (Zlt_is_lt_bool x y)).
Qed.
Theorem Zlt_bool_false :
forall x y : Z,
(y <= x)%Z -> Zlt_bool x y = false.
Proof.
intros x y Hxy.
generalize (Zlt_cases x y).
case Zlt_bool ; intros H.
elim (Zlt_irrefl x).
now apply Zlt_le_trans with y.
apply refl_equal.
Qed.
Theorem negb_Zle_bool :
forall x y : Z,
negb (Zle_bool x y) = Zlt_bool y x.
Proof.
intros x y.
case Zle_bool_spec ; intros H.
now rewrite Zlt_bool_false.
now rewrite Zlt_bool_true.
Qed.
Theorem negb_Zlt_bool :
forall x y : Z,
negb (Zlt_bool x y) = Zle_bool y x.
Proof.
intros x y.
case Zlt_bool_spec ; intros H.
now rewrite Zle_bool_false.
now rewrite Zle_bool_true.
Qed.
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).
Proof.
intros x y.
destruct (Z_dec x y) as [[H|H]|H].
generalize (Zlt_compare _ _ H).
case (Zcompare x y) ; try easy.
now constructor.
generalize (Zgt_compare _ _ H).
case (Zcompare x y) ; try easy.
constructor.
now apply Zgt_lt.
generalize (proj2 (Zcompare_Eq_iff_eq _ _) H).
case (Zcompare x y) ; try easy.
now constructor.
Qed.
Theorem Zcompare_Lt :
forall x y,
(x < y)%Z -> Zcompare x y = Lt.
Proof.
easy.
Qed.
Theorem Zcompare_Eq :
forall x y,
(x = y)%Z -> Zcompare x y = Eq.
Proof.
intros x y.
apply <- Zcompare_Eq_iff_eq.
Qed.
Theorem Zcompare_Gt :
forall x y,
(y < x)%Z -> Zcompare x y = Gt.
Proof.
intros x y.
apply Zlt_gt.
Qed.
End Zcompare.
Section Rcompare.
Definition Rcompare x y :=
......@@ -1524,77 +1294,6 @@ Qed.
End Floor_Ceil.
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).
Proof.
now intros [|[xp|xp|]|[xp|xp|]] [|[yp|yp|]|[yp|yp|]].
Qed.
Theorem Zeven_opp :
forall x, Zeven (- x) = Zeven x.
Proof.
now intros [|[n|n|]|[n|n|]].
Qed.
Theorem Zeven_ex :
forall x, exists p, x = (2 * p + if Zeven x then 0 else 1)%Z.
Proof.
intros [|[n|n|]|[n|n|]].
now exists Z0.
now exists (Zpos n).
now exists (Zpos n).
now exists Z0.
exists (Zneg n - 1)%Z.
change (2 * Zneg n - 1 = 2 * (Zneg n - 1) + 1)%Z.
ring.
now exists (Zneg n).
now exists (-1)%Z.
Qed.
Theorem Zeven_2xp1 :
forall n, Zeven (2 * n + 1) = false.
Proof.
intros n.
destruct (Zeven_ex (2 * n + 1)) as (p, Hp).
revert Hp.
case (Zeven (2 * n + 1)) ; try easy.
intros H.
apply False_ind.
omega.
Qed.
Theorem Zeven_plus :
forall x y, Zeven (x + y) = Bool.eqb (Zeven x) (Zeven y).
Proof.
intros x y.
destruct (Zeven_ex x) as (px, Hx).
rewrite Hx at 1.
destruct (Zeven_ex y) as (py, Hy).
rewrite Hy at 1.
replace (2 * px + (if Zeven x then 0 else 1) + (2 * py + (if Zeven y then 0 else 1)))%Z
with (2 * (px + py) + ((if Zeven x then 0 else 1) + (if Zeven y then 0 else 1)))%Z by ring.
case (Zeven x) ; case (Zeven y).
rewrite Zplus_0_r.
now rewrite Zeven_mult.
apply Zeven_2xp1.
apply Zeven_2xp1.
replace (2 * (px + py) + (1 + 1))%Z with (2 * (px + py + 1))%Z by ring.
now rewrite Zeven_mult.
Qed.
End Even_Odd.
Section Zdiv_Rdiv.
Theorem Zfloor_div :
......@@ -1657,57 +1356,10 @@ Qed.
End Zdiv_Rdiv.
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.
Proof.
assert (forall (h : true = true), refl_equal true = h).
apply (eq_dep_elim bool true (eqbool_dep _ _) (refl_equal _)).
intros b.
case b.
intros h1 h2.
now rewrite <- (H h1).
intros h.
discriminate h.
Qed.
End Proof_Irrelevance.
Section pow.
(** 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.
Proof.
intros (r1, H1) (r2, H2) H.
simpl in H.
revert H1.
rewrite H.
intros H1.
apply f_equal.
apply eqbool_irrelevance.
Qed.
Variable r : radix.
Theorem radix_gt_1 : (1 < r)%Z.
Proof.
destruct r as (v, Hr). simpl.
apply Zlt_le_trans with 2%Z.
easy.
now apply Zle_bool_imp_le.
Qed.
Theorem radix_pos : (0 < Z2R r)%R.
Proof.
destruct r as (v, Hr). simpl.
......@@ -1842,27 +1494,9 @@ apply bpow_gt_0.
assert (0 < e2 - e1)%Z by omega.
destruct (e2 - e1)%Z ; try discriminate H0.
clear.
unfold bpow.
rewrite <- Z2R_Zpower by easy.
apply (Z2R_lt 1).
rewrite Zpower_pos_nat.
case_eq (nat_of_P p).
intros H.
elim (lt_irrefl 0).
pattern O at 2 ; rewrite <- H.
apply lt_O_nat_of_P.
intros n _.
assert (1 < Zpower_nat r 1)%Z.
unfold Zpower_nat, iter_nat.
rewrite Zmult_1_r.
apply radix_gt_1.
induction n.
exact H.
change (S (S n)) with (1 + (S n))%nat.
rewrite Zpower_nat_is_exp.
change 1%Z with (1 * 1)%Z.
apply Zmult_lt_compat.
now split.
now split.
now apply Zpower_gt_1.
Qed.
Theorem lt_bpow :
......@@ -1930,20 +1564,16 @@ unfold Z2R at 2.
rewrite P2R_INR.
induction (nat_of_P e).
rewrite Rmult_0_l.
unfold Zpower_nat, iter_nat.
now rewrite exp_0.
change (S n) with (1 + n)%nat.
rewrite plus_INR.
rewrite Zpower_nat_is_exp.
rewrite Zpower_nat_S.
rewrite S_INR.
rewrite Rmult_plus_distr_r.
rewrite exp_plus.
rewrite Rmult_1_l.
rewrite exp_ln.
rewrite <- IHn.
rewrite <- Z2R_mult.
apply f_equal.
unfold Zpower_nat at 1, iter_nat.
now rewrite Zmult_1_r.
now rewrite Zmult_comm.
apply radix_pos.
(* general case *)
intros [|e|e].
......@@ -2193,102 +1823,6 @@ clear -Zm.
zify ; omega.
Qed.
Theorem Zpower_pos_gt_0 :
forall b p, (0 < b)%Z ->
(0 < Zpower_pos b p)%Z.
Proof.
intros b p Hb.
apply lt_Z2R.
rewrite Z2R_Zpower_pos.
apply powerRZ_lt.
now apply (Z2R_lt 0).
Qed.
Theorem Zpower_gt_1 :
forall p,
(0 < p)%Z ->
(1 < Zpower r p)%Z.
Proof.
intros.
apply lt_Z2R.
rewrite Z2R_Zpower.
now apply (bpow_lt 0).
now apply Zlt_le_weak.
Qed.
Theorem Zpower_gt_0 :
forall p,
(0 <= p)%Z ->
(0 < Zpower r p)%Z.
Proof.
intros.
apply lt_Z2R.
rewrite Z2R_Zpower.
apply bpow_gt_0.
exact H.
Qed.
Theorem Zpower_ge_0 :
forall e,
(0 <= Zpower r e)%Z.
Proof.
intros [|e|e].
apply Zle_0_1.
apply le_Z2R.
rewrite Z2R_Zpower.
apply bpow_ge_0.
discriminate.
apply Zle_refl.
Qed.
Theorem Zpower_Zpower_nat :
forall b e, (0 <= e)%Z ->
Zpower b e = Zpower_nat b (Zabs_nat e).
Proof.
intros b [|e|e] He.
apply refl_equal.
apply Zpower_pos_nat.
elim He.
apply refl_equal.
Qed.
Theorem Zeven_Zpower :
forall b e, (0 < e)%Z ->
Zeven (Zpower b e) = Zeven b.
Proof.
intros b e He.
case_eq (Zeven b) ; intros Hb.
(* b even *)
replace e with (e - 1 + 1)%Z by ring.
rewrite Zpower_exp.
rewrite Zeven_mult.
replace (Zeven (b ^ 1)) with true.
apply Bool.orb_true_r.
unfold Zpower, Zpower_pos, iter_pos.
now rewrite Zmult_1_r.
omega.
discriminate.
(* b odd *)
rewrite Zpower_Zpower_nat.
induction (Zabs_nat e).
easy.
unfold Zpower_nat. simpl.
rewrite Zeven_mult.
now rewrite Hb.
now apply Zlt_le_weak.
Qed.
Theorem Zeven_Zpower_odd :
forall b e, (0 <= e)%Z -> Zeven b = false ->
Zeven (Zpower b e) = false.
Proof.
intros b e He Hb.
destruct (Z_le_lt_eq_dec _ _ He) as [He'|He'].
rewrite <- Hb.
now apply Zeven_Zpower.
now rewrite <- He'.
Qed.
End pow.
Section Bool.
......
(**
This file is part of the Flocq formalization of floating-point
arithmetic in Coq: http://flocq.gforge.inria.fr/
Copyright (C) 2011 Sylvie Boldo
#<br />#
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.
Proof.
intros x y Hxy.
apply Zplus_le_reg_r with (-x - y)%Z.
now ring_simplify.
Qed.
Theorem Zgt_not_eq :
forall x y : Z,
(y < x)%Z -> (x <> y)%Z.
Proof.
intros x y H Hn.
apply Zlt_irrefl with x.
now rewrite Hn at 1.
Qed.
Theorem Zmin_left :
forall x y : Z,
(x <= y)%Z -> Zmin x y = x.
Proof.
intros x y.
generalize (Zmin_spec x y).
omega.
Qed.
Theorem Zmin_right :
forall x y : Z,
(y <= x)%Z -> Zmin x y = y.
Proof.
intros x y.
generalize (Zmin_spec x y).
omega.
Qed.
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