Library Flocq.Core.Fcore_Raux
This file is part of the Flocq formalization of floating-point
arithmetic in Coq: http://flocq.gforge.inria.fr/
Copyright (C) 2010-2013 Sylvie Boldo
Copyright (C) 2010-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) 2010-2013 Guillaume Melquiond
Missing definitions/lemmas
About R
Theorem Rle_0_minus :
∀ x y, (x ≤ y)%R → (0 ≤ y - x)%R.
Theorem Rabs_eq_Rabs :
∀ x y : R,
Rabs x = Rabs y → x = y ∨ x = Ropp y.
Theorem Rabs_minus_le:
∀ x y : R,
(0 ≤ y)%R → (y ≤ 2×x)%R →
(Rabs (x-y) ≤ x)%R.
Theorem Rplus_eq_reg_r :
∀ r r1 r2 : R,
(r1 + r = r2 + r)%R → (r1 = r2)%R.
Theorem Rplus_lt_reg_l :
∀ r r1 r2 : R,
(r + r1 < r + r2)%R → (r1 < r2)%R.
Theorem Rplus_lt_reg_r :
∀ r r1 r2 : R,
(r1 + r < r2 + r)%R → (r1 < r2)%R.
Theorem Rplus_le_reg_r :
∀ r r1 r2 : R,
(r1 + r ≤ r2 + r)%R → (r1 ≤ r2)%R.
Theorem Rmult_lt_reg_r :
∀ r r1 r2 : R, (0 < r)%R →
(r1 × r < r2 × r)%R → (r1 < r2)%R.
Theorem Rmult_le_reg_r :
∀ r r1 r2 : R, (0 < r)%R →
(r1 × r ≤ r2 × r)%R → (r1 ≤ r2)%R.
Theorem Rmult_lt_compat :
∀ r1 r2 r3 r4,
(0 ≤ r1)%R → (0 ≤ r3)%R → (r1 < r2)%R → (r3 < r4)%R →
(r1 × r3 < r2 × r4)%R.
Theorem Rmult_eq_reg_r :
∀ r r1 r2 : R, (r1 × r)%R = (r2 × r)%R →
r ≠ 0%R → r1 = r2.
Theorem Rmult_minus_distr_r :
∀ r r1 r2 : R,
((r1 - r2) × r = r1 × r - r2 × r)%R.
Lemma Rmult_neq_reg_r: ∀ r1 r2 r3:R, (r2 × r1 ≠ r3 × r1)%R → r2 ≠ r3.
Lemma Rmult_neq_compat_r: ∀ r1 r2 r3:R, (r1 ≠ 0)%R → (r2 ≠ r3)%R
→ (r2 ×r1 ≠ r3×r1)%R.
Theorem Rmult_min_distr_r :
∀ r r1 r2 : R,
(0 ≤ r)%R →
(Rmin r1 r2 × r)%R = Rmin (r1 × r) (r2 × r).
Theorem Rmult_min_distr_l :
∀ r r1 r2 : R,
(0 ≤ r)%R →
(r × Rmin r1 r2)%R = Rmin (r × r1) (r × r2).
Theorem exp_le :
∀ x y : R,
(x ≤ y)%R → (exp x ≤ exp y)%R.
Theorem Rinv_lt :
∀ x y,
(0 < x)%R → (x < y)%R → (/y < /x)%R.
Theorem Rinv_le :
∀ x y,
(0 < x)%R → (x ≤ y)%R → (/y ≤ /x)%R.
Theorem sqrt_ge_0 :
∀ x : R,
(0 ≤ sqrt x)%R.
Lemma sqrt_neg : ∀ x, (x ≤ 0)%R → (sqrt x = 0)%R.
Theorem Rabs_le :
∀ x y,
(-y ≤ x ≤ y)%R → (Rabs x ≤ y)%R.
Theorem Rabs_le_inv :
∀ x y,
(Rabs x ≤ y)%R → (-y ≤ x ≤ y)%R.
Theorem Rabs_ge :
∀ x y,
(y ≤ -x ∨ x ≤ y)%R → (x ≤ Rabs y)%R.
Theorem Rabs_ge_inv :
∀ x y,
(x ≤ Rabs y)%R → (y ≤ -x ∨ x ≤ y)%R.
Theorem Rabs_lt :
∀ x y,
(-y < x < y)%R → (Rabs x < y)%R.
Theorem Rabs_lt_inv :
∀ x y,
(Rabs x < y)%R → (-y < x < y)%R.
Theorem Rabs_gt :
∀ x y,
(y < -x ∨ x < y)%R → (x < Rabs y)%R.
Theorem Rabs_gt_inv :
∀ x y,
(x < Rabs y)%R → (y < -x ∨ x < y)%R.
End Rmissing.
Section Z2R.
∀ x y, (x ≤ y)%R → (0 ≤ y - x)%R.
Theorem Rabs_eq_Rabs :
∀ x y : R,
Rabs x = Rabs y → x = y ∨ x = Ropp y.
Theorem Rabs_minus_le:
∀ x y : R,
(0 ≤ y)%R → (y ≤ 2×x)%R →
(Rabs (x-y) ≤ x)%R.
Theorem Rplus_eq_reg_r :
∀ r r1 r2 : R,
(r1 + r = r2 + r)%R → (r1 = r2)%R.
Theorem Rplus_lt_reg_l :
∀ r r1 r2 : R,
(r + r1 < r + r2)%R → (r1 < r2)%R.
Theorem Rplus_lt_reg_r :
∀ r r1 r2 : R,
(r1 + r < r2 + r)%R → (r1 < r2)%R.
Theorem Rplus_le_reg_r :
∀ r r1 r2 : R,
(r1 + r ≤ r2 + r)%R → (r1 ≤ r2)%R.
Theorem Rmult_lt_reg_r :
∀ r r1 r2 : R, (0 < r)%R →
(r1 × r < r2 × r)%R → (r1 < r2)%R.
Theorem Rmult_le_reg_r :
∀ r r1 r2 : R, (0 < r)%R →
(r1 × r ≤ r2 × r)%R → (r1 ≤ r2)%R.
Theorem Rmult_lt_compat :
∀ r1 r2 r3 r4,
(0 ≤ r1)%R → (0 ≤ r3)%R → (r1 < r2)%R → (r3 < r4)%R →
(r1 × r3 < r2 × r4)%R.
Theorem Rmult_eq_reg_r :
∀ r r1 r2 : R, (r1 × r)%R = (r2 × r)%R →
r ≠ 0%R → r1 = r2.
Theorem Rmult_minus_distr_r :
∀ r r1 r2 : R,
((r1 - r2) × r = r1 × r - r2 × r)%R.
Lemma Rmult_neq_reg_r: ∀ r1 r2 r3:R, (r2 × r1 ≠ r3 × r1)%R → r2 ≠ r3.
Lemma Rmult_neq_compat_r: ∀ r1 r2 r3:R, (r1 ≠ 0)%R → (r2 ≠ r3)%R
→ (r2 ×r1 ≠ r3×r1)%R.
Theorem Rmult_min_distr_r :
∀ r r1 r2 : R,
(0 ≤ r)%R →
(Rmin r1 r2 × r)%R = Rmin (r1 × r) (r2 × r).
Theorem Rmult_min_distr_l :
∀ r r1 r2 : R,
(0 ≤ r)%R →
(r × Rmin r1 r2)%R = Rmin (r × r1) (r × r2).
Theorem exp_le :
∀ x y : R,
(x ≤ y)%R → (exp x ≤ exp y)%R.
Theorem Rinv_lt :
∀ x y,
(0 < x)%R → (x < y)%R → (/y < /x)%R.
Theorem Rinv_le :
∀ x y,
(0 < x)%R → (x ≤ y)%R → (/y ≤ /x)%R.
Theorem sqrt_ge_0 :
∀ x : R,
(0 ≤ sqrt x)%R.
Lemma sqrt_neg : ∀ x, (x ≤ 0)%R → (sqrt x = 0)%R.
Theorem Rabs_le :
∀ x y,
(-y ≤ x ≤ y)%R → (Rabs x ≤ y)%R.
Theorem Rabs_le_inv :
∀ x y,
(Rabs x ≤ y)%R → (-y ≤ x ≤ y)%R.
Theorem Rabs_ge :
∀ x y,
(y ≤ -x ∨ x ≤ y)%R → (x ≤ Rabs y)%R.
Theorem Rabs_ge_inv :
∀ x y,
(x ≤ Rabs y)%R → (y ≤ -x ∨ x ≤ y)%R.
Theorem Rabs_lt :
∀ x y,
(-y < x < y)%R → (Rabs x < y)%R.
Theorem Rabs_lt_inv :
∀ x y,
(Rabs x < y)%R → (-y < x < y)%R.
Theorem Rabs_gt :
∀ x y,
(y < -x ∨ x < y)%R → (x < Rabs y)%R.
Theorem Rabs_gt_inv :
∀ x y,
(x < Rabs y)%R → (y < -x ∨ x < y)%R.
End Rmissing.
Section Z2R.
Z2R function (Z -> R)
Fixpoint P2R (p : positive) :=
match p with
| xH ⇒ 1%R
| xO xH ⇒ 2%R
| xO t ⇒ (2 × P2R t)%R
| xI xH ⇒ 3%R
| xI t ⇒ (1 + 2 × P2R t)%R
end.
Definition Z2R n :=
match n with
| Zpos p ⇒ P2R p
| Zneg p ⇒ Ropp (P2R p)
| Z0 ⇒ R0
end.
Theorem P2R_INR :
∀ n, P2R n = INR (nat_of_P n).
Theorem Z2R_IZR :
∀ n, Z2R n = IZR n.
Theorem Z2R_opp :
∀ n, Z2R (-n) = (- Z2R n)%R.
Theorem Z2R_plus :
∀ m n, (Z2R (m + n) = Z2R m + Z2R n)%R.
Theorem minus_IZR :
∀ n m : Z,
IZR (n - m) = (IZR n - IZR m)%R.
Theorem Z2R_minus :
∀ m n, (Z2R (m - n) = Z2R m - Z2R n)%R.
Theorem Z2R_mult :
∀ m n, (Z2R (m × n) = Z2R m × Z2R n)%R.
Theorem le_Z2R :
∀ m n, (Z2R m ≤ Z2R n)%R → (m ≤ n)%Z.
Theorem Z2R_le :
∀ m n, (m ≤ n)%Z → (Z2R m ≤ Z2R n)%R.
Theorem lt_Z2R :
∀ m n, (Z2R m < Z2R n)%R → (m < n)%Z.
Theorem Z2R_lt :
∀ m n, (m < n)%Z → (Z2R m < Z2R n)%R.
Theorem Z2R_le_lt :
∀ m n p, (m ≤ n < p)%Z → (Z2R m ≤ Z2R n < Z2R p)%R.
Theorem le_lt_Z2R :
∀ m n p, (Z2R m ≤ Z2R n < Z2R p)%R → (m ≤ n < p)%Z.
Theorem eq_Z2R :
∀ m n, (Z2R m = Z2R n)%R → (m = n)%Z.
Theorem neq_Z2R :
∀ m n, (Z2R m ≠ Z2R n)%R → (m ≠ n)%Z.
Theorem Z2R_neq :
∀ m n, (m ≠ n)%Z → (Z2R m ≠ Z2R n)%R.
Theorem Z2R_abs :
∀ z, Z2R (Zabs z) = Rabs (Z2R z).
End Z2R.
match p with
| xH ⇒ 1%R
| xO xH ⇒ 2%R
| xO t ⇒ (2 × P2R t)%R
| xI xH ⇒ 3%R
| xI t ⇒ (1 + 2 × P2R t)%R
end.
Definition Z2R n :=
match n with
| Zpos p ⇒ P2R p
| Zneg p ⇒ Ropp (P2R p)
| Z0 ⇒ R0
end.
Theorem P2R_INR :
∀ n, P2R n = INR (nat_of_P n).
Theorem Z2R_IZR :
∀ n, Z2R n = IZR n.
Theorem Z2R_opp :
∀ n, Z2R (-n) = (- Z2R n)%R.
Theorem Z2R_plus :
∀ m n, (Z2R (m + n) = Z2R m + Z2R n)%R.
Theorem minus_IZR :
∀ n m : Z,
IZR (n - m) = (IZR n - IZR m)%R.
Theorem Z2R_minus :
∀ m n, (Z2R (m - n) = Z2R m - Z2R n)%R.
Theorem Z2R_mult :
∀ m n, (Z2R (m × n) = Z2R m × Z2R n)%R.
Theorem le_Z2R :
∀ m n, (Z2R m ≤ Z2R n)%R → (m ≤ n)%Z.
Theorem Z2R_le :
∀ m n, (m ≤ n)%Z → (Z2R m ≤ Z2R n)%R.
Theorem lt_Z2R :
∀ m n, (Z2R m < Z2R n)%R → (m < n)%Z.
Theorem Z2R_lt :
∀ m n, (m < n)%Z → (Z2R m < Z2R n)%R.
Theorem Z2R_le_lt :
∀ m n p, (m ≤ n < p)%Z → (Z2R m ≤ Z2R n < Z2R p)%R.
Theorem le_lt_Z2R :
∀ m n p, (Z2R m ≤ Z2R n < Z2R p)%R → (m ≤ n < p)%Z.
Theorem eq_Z2R :
∀ m n, (Z2R m = Z2R n)%R → (m = n)%Z.
Theorem neq_Z2R :
∀ m n, (Z2R m ≠ Z2R n)%R → (m ≠ n)%Z.
Theorem Z2R_neq :
∀ m n, (m ≠ n)%Z → (Z2R m ≠ Z2R n)%R.
Theorem Z2R_abs :
∀ z, Z2R (Zabs z) = Rabs (Z2R z).
End Z2R.
Decidable comparison on reals
Section Rcompare.
Definition Rcompare x y :=
match total_order_T x y with
| inleft (left _) ⇒ Lt
| inleft (right _) ⇒ Eq
| inright _ ⇒ Gt
end.
Inductive Rcompare_prop (x y : R) : comparison → Prop :=
| Rcompare_Lt_ : (x < y)%R → Rcompare_prop x y Lt
| Rcompare_Eq_ : x = y → Rcompare_prop x y Eq
| Rcompare_Gt_ : (y < x)%R → Rcompare_prop x y Gt.
Theorem Rcompare_spec :
∀ x y, Rcompare_prop x y (Rcompare x y).
Global Opaque Rcompare.
Theorem Rcompare_Lt :
∀ x y,
(x < y)%R → Rcompare x y = Lt.
Theorem Rcompare_Lt_inv :
∀ x y,
Rcompare x y = Lt → (x < y)%R.
Theorem Rcompare_not_Lt :
∀ x y,
(y ≤ x)%R → Rcompare x y ≠ Lt.
Theorem Rcompare_not_Lt_inv :
∀ x y,
Rcompare x y ≠ Lt → (y ≤ x)%R.
Theorem Rcompare_Eq :
∀ x y,
x = y → Rcompare x y = Eq.
Theorem Rcompare_Eq_inv :
∀ x y,
Rcompare x y = Eq → x = y.
Theorem Rcompare_Gt :
∀ x y,
(y < x)%R → Rcompare x y = Gt.
Theorem Rcompare_Gt_inv :
∀ x y,
Rcompare x y = Gt → (y < x)%R.
Theorem Rcompare_not_Gt :
∀ x y,
(x ≤ y)%R → Rcompare x y ≠ Gt.
Theorem Rcompare_not_Gt_inv :
∀ x y,
Rcompare x y ≠ Gt → (x ≤ y)%R.
Theorem Rcompare_Z2R :
∀ x y, Rcompare (Z2R x) (Z2R y) = Zcompare x y.
Theorem Rcompare_sym :
∀ x y,
Rcompare x y = CompOpp (Rcompare y x).
Theorem Rcompare_plus_r :
∀ z x y,
Rcompare (x + z) (y + z) = Rcompare x y.
Theorem Rcompare_plus_l :
∀ z x y,
Rcompare (z + x) (z + y) = Rcompare x y.
Theorem Rcompare_mult_r :
∀ z x y,
(0 < z)%R →
Rcompare (x × z) (y × z) = Rcompare x y.
Theorem Rcompare_mult_l :
∀ z x y,
(0 < z)%R →
Rcompare (z × x) (z × y) = Rcompare x y.
Theorem Rcompare_middle :
∀ x d u,
Rcompare (x - d) (u - x) = Rcompare x ((d + u) / 2).
Theorem Rcompare_half_l :
∀ x y, Rcompare (x / 2) y = Rcompare x (2 × y).
Theorem Rcompare_half_r :
∀ x y, Rcompare x (y / 2) = Rcompare (2 × x) y.
Theorem Rcompare_sqr :
∀ x y,
(0 ≤ x)%R → (0 ≤ y)%R →
Rcompare (x × x) (y × y) = Rcompare x y.
Theorem Rmin_compare :
∀ x y,
Rmin x y = match Rcompare x y with Lt ⇒ x | Eq ⇒ x | Gt ⇒ y end.
End Rcompare.
Section Rle_bool.
Definition Rle_bool x y :=
match Rcompare x y with
| Gt ⇒ false
| _ ⇒ true
end.
Inductive Rle_bool_prop (x y : R) : bool → Prop :=
| Rle_bool_true_ : (x ≤ y)%R → Rle_bool_prop x y true
| Rle_bool_false_ : (y < x)%R → Rle_bool_prop x y false.
Theorem Rle_bool_spec :
∀ x y, Rle_bool_prop x y (Rle_bool x y).
Theorem Rle_bool_true :
∀ x y,
(x ≤ y)%R → Rle_bool x y = true.
Theorem Rle_bool_false :
∀ x y,
(y < x)%R → Rle_bool x y = false.
End Rle_bool.
Section Rlt_bool.
Definition Rlt_bool x y :=
match Rcompare x y with
| Lt ⇒ true
| _ ⇒ false
end.
Inductive Rlt_bool_prop (x y : R) : bool → Prop :=
| Rlt_bool_true_ : (x < y)%R → Rlt_bool_prop x y true
| Rlt_bool_false_ : (y ≤ x)%R → Rlt_bool_prop x y false.
Theorem Rlt_bool_spec :
∀ x y, Rlt_bool_prop x y (Rlt_bool x y).
Theorem negb_Rlt_bool :
∀ x y,
negb (Rle_bool x y) = Rlt_bool y x.
Theorem negb_Rle_bool :
∀ x y,
negb (Rlt_bool x y) = Rle_bool y x.
Theorem Rlt_bool_true :
∀ x y,
(x < y)%R → Rlt_bool x y = true.
Theorem Rlt_bool_false :
∀ x y,
(y ≤ x)%R → Rlt_bool x y = false.
End Rlt_bool.
Section Req_bool.
Definition Req_bool x y :=
match Rcompare x y with
| Eq ⇒ true
| _ ⇒ false
end.
Inductive Req_bool_prop (x y : R) : bool → Prop :=
| Req_bool_true_ : (x = y)%R → Req_bool_prop x y true
| Req_bool_false_ : (x ≠ y)%R → Req_bool_prop x y false.
Theorem Req_bool_spec :
∀ x y, Req_bool_prop x y (Req_bool x y).
Theorem Req_bool_true :
∀ x y,
(x = y)%R → Req_bool x y = true.
Theorem Req_bool_false :
∀ x y,
(x ≠ y)%R → Req_bool x y = false.
End Req_bool.
Section Floor_Ceil.
Definition Rcompare x y :=
match total_order_T x y with
| inleft (left _) ⇒ Lt
| inleft (right _) ⇒ Eq
| inright _ ⇒ Gt
end.
Inductive Rcompare_prop (x y : R) : comparison → Prop :=
| Rcompare_Lt_ : (x < y)%R → Rcompare_prop x y Lt
| Rcompare_Eq_ : x = y → Rcompare_prop x y Eq
| Rcompare_Gt_ : (y < x)%R → Rcompare_prop x y Gt.
Theorem Rcompare_spec :
∀ x y, Rcompare_prop x y (Rcompare x y).
Global Opaque Rcompare.
Theorem Rcompare_Lt :
∀ x y,
(x < y)%R → Rcompare x y = Lt.
Theorem Rcompare_Lt_inv :
∀ x y,
Rcompare x y = Lt → (x < y)%R.
Theorem Rcompare_not_Lt :
∀ x y,
(y ≤ x)%R → Rcompare x y ≠ Lt.
Theorem Rcompare_not_Lt_inv :
∀ x y,
Rcompare x y ≠ Lt → (y ≤ x)%R.
Theorem Rcompare_Eq :
∀ x y,
x = y → Rcompare x y = Eq.
Theorem Rcompare_Eq_inv :
∀ x y,
Rcompare x y = Eq → x = y.
Theorem Rcompare_Gt :
∀ x y,
(y < x)%R → Rcompare x y = Gt.
Theorem Rcompare_Gt_inv :
∀ x y,
Rcompare x y = Gt → (y < x)%R.
Theorem Rcompare_not_Gt :
∀ x y,
(x ≤ y)%R → Rcompare x y ≠ Gt.
Theorem Rcompare_not_Gt_inv :
∀ x y,
Rcompare x y ≠ Gt → (x ≤ y)%R.
Theorem Rcompare_Z2R :
∀ x y, Rcompare (Z2R x) (Z2R y) = Zcompare x y.
Theorem Rcompare_sym :
∀ x y,
Rcompare x y = CompOpp (Rcompare y x).
Theorem Rcompare_plus_r :
∀ z x y,
Rcompare (x + z) (y + z) = Rcompare x y.
Theorem Rcompare_plus_l :
∀ z x y,
Rcompare (z + x) (z + y) = Rcompare x y.
Theorem Rcompare_mult_r :
∀ z x y,
(0 < z)%R →
Rcompare (x × z) (y × z) = Rcompare x y.
Theorem Rcompare_mult_l :
∀ z x y,
(0 < z)%R →
Rcompare (z × x) (z × y) = Rcompare x y.
Theorem Rcompare_middle :
∀ x d u,
Rcompare (x - d) (u - x) = Rcompare x ((d + u) / 2).
Theorem Rcompare_half_l :
∀ x y, Rcompare (x / 2) y = Rcompare x (2 × y).
Theorem Rcompare_half_r :
∀ x y, Rcompare x (y / 2) = Rcompare (2 × x) y.
Theorem Rcompare_sqr :
∀ x y,
(0 ≤ x)%R → (0 ≤ y)%R →
Rcompare (x × x) (y × y) = Rcompare x y.
Theorem Rmin_compare :
∀ x y,
Rmin x y = match Rcompare x y with Lt ⇒ x | Eq ⇒ x | Gt ⇒ y end.
End Rcompare.
Section Rle_bool.
Definition Rle_bool x y :=
match Rcompare x y with
| Gt ⇒ false
| _ ⇒ true
end.
Inductive Rle_bool_prop (x y : R) : bool → Prop :=
| Rle_bool_true_ : (x ≤ y)%R → Rle_bool_prop x y true
| Rle_bool_false_ : (y < x)%R → Rle_bool_prop x y false.
Theorem Rle_bool_spec :
∀ x y, Rle_bool_prop x y (Rle_bool x y).
Theorem Rle_bool_true :
∀ x y,
(x ≤ y)%R → Rle_bool x y = true.
Theorem Rle_bool_false :
∀ x y,
(y < x)%R → Rle_bool x y = false.
End Rle_bool.
Section Rlt_bool.
Definition Rlt_bool x y :=
match Rcompare x y with
| Lt ⇒ true
| _ ⇒ false
end.
Inductive Rlt_bool_prop (x y : R) : bool → Prop :=
| Rlt_bool_true_ : (x < y)%R → Rlt_bool_prop x y true
| Rlt_bool_false_ : (y ≤ x)%R → Rlt_bool_prop x y false.
Theorem Rlt_bool_spec :
∀ x y, Rlt_bool_prop x y (Rlt_bool x y).
Theorem negb_Rlt_bool :
∀ x y,
negb (Rle_bool x y) = Rlt_bool y x.
Theorem negb_Rle_bool :
∀ x y,
negb (Rlt_bool x y) = Rle_bool y x.
Theorem Rlt_bool_true :
∀ x y,
(x < y)%R → Rlt_bool x y = true.
Theorem Rlt_bool_false :
∀ x y,
(y ≤ x)%R → Rlt_bool x y = false.
End Rlt_bool.
Section Req_bool.
Definition Req_bool x y :=
match Rcompare x y with
| Eq ⇒ true
| _ ⇒ false
end.
Inductive Req_bool_prop (x y : R) : bool → Prop :=
| Req_bool_true_ : (x = y)%R → Req_bool_prop x y true
| Req_bool_false_ : (x ≠ y)%R → Req_bool_prop x y false.
Theorem Req_bool_spec :
∀ x y, Req_bool_prop x y (Req_bool x y).
Theorem Req_bool_true :
∀ x y,
(x = y)%R → Req_bool x y = true.
Theorem Req_bool_false :
∀ x y,
(x ≠ y)%R → Req_bool x y = false.
End Req_bool.
Section Floor_Ceil.
Zfloor and Zceil
Definition Zfloor (x : R) := (up x - 1)%Z.
Theorem Zfloor_lb :
∀ x : R,
(Z2R (Zfloor x) ≤ x)%R.
Theorem Zfloor_ub :
∀ x : R,
(x < Z2R (Zfloor x) + 1)%R.
Theorem Zfloor_lub :
∀ n x,
(Z2R n ≤ x)%R →
(n ≤ Zfloor x)%Z.
Theorem Zfloor_imp :
∀ n x,
(Z2R n ≤ x < Z2R (n + 1))%R →
Zfloor x = n.
Theorem Zfloor_Z2R :
∀ n,
Zfloor (Z2R n) = n.
Theorem Zfloor_le :
∀ x y, (x ≤ y)%R →
(Zfloor x ≤ Zfloor y)%Z.
Definition Zceil (x : R) := (- Zfloor (- x))%Z.
Theorem Zceil_ub :
∀ x : R,
(x ≤ Z2R (Zceil x))%R.
Theorem Zceil_glb :
∀ n x,
(x ≤ Z2R n)%R →
(Zceil x ≤ n)%Z.
Theorem Zceil_imp :
∀ n x,
(Z2R (n - 1) < x ≤ Z2R n)%R →
Zceil x = n.
Theorem Zceil_Z2R :
∀ n,
Zceil (Z2R n) = n.
Theorem Zceil_le :
∀ x y, (x ≤ y)%R →
(Zceil x ≤ Zceil y)%Z.
Theorem Zceil_floor_neq :
∀ x : R,
(Z2R (Zfloor x) ≠ x)%R →
(Zceil x = Zfloor x + 1)%Z.
Definition Ztrunc x := if Rlt_bool x 0 then Zceil x else Zfloor x.
Theorem Ztrunc_Z2R :
∀ n,
Ztrunc (Z2R n) = n.
Theorem Ztrunc_floor :
∀ x,
(0 ≤ x)%R →
Ztrunc x = Zfloor x.
Theorem Ztrunc_ceil :
∀ x,
(x ≤ 0)%R →
Ztrunc x = Zceil x.
Theorem Ztrunc_le :
∀ x y, (x ≤ y)%R →
(Ztrunc x ≤ Ztrunc y)%Z.
Theorem Ztrunc_opp :
∀ x,
Ztrunc (- x) = Zopp (Ztrunc x).
Theorem Ztrunc_abs :
∀ x,
Ztrunc (Rabs x) = Zabs (Ztrunc x).
Theorem Ztrunc_lub :
∀ n x,
(Z2R n ≤ Rabs x)%R →
(n ≤ Zabs (Ztrunc x))%Z.
Definition Zaway x := if Rlt_bool x 0 then Zfloor x else Zceil x.
Theorem Zaway_Z2R :
∀ n,
Zaway (Z2R n) = n.
Theorem Zaway_ceil :
∀ x,
(0 ≤ x)%R →
Zaway x = Zceil x.
Theorem Zaway_floor :
∀ x,
(x ≤ 0)%R →
Zaway x = Zfloor x.
Theorem Zaway_le :
∀ x y, (x ≤ y)%R →
(Zaway x ≤ Zaway y)%Z.
Theorem Zaway_opp :
∀ x,
Zaway (- x) = Zopp (Zaway x).
Theorem Zaway_abs :
∀ x,
Zaway (Rabs x) = Zabs (Zaway x).
End Floor_Ceil.
Section Zdiv_Rdiv.
Theorem Zfloor_div :
∀ x y,
y ≠ Z0 →
Zfloor (Z2R x / Z2R y) = (x / y)%Z.
End Zdiv_Rdiv.
Section pow.
Variable r : radix.
Theorem radix_pos : (0 < Z2R r)%R.
Theorem Zfloor_lb :
∀ x : R,
(Z2R (Zfloor x) ≤ x)%R.
Theorem Zfloor_ub :
∀ x : R,
(x < Z2R (Zfloor x) + 1)%R.
Theorem Zfloor_lub :
∀ n x,
(Z2R n ≤ x)%R →
(n ≤ Zfloor x)%Z.
Theorem Zfloor_imp :
∀ n x,
(Z2R n ≤ x < Z2R (n + 1))%R →
Zfloor x = n.
Theorem Zfloor_Z2R :
∀ n,
Zfloor (Z2R n) = n.
Theorem Zfloor_le :
∀ x y, (x ≤ y)%R →
(Zfloor x ≤ Zfloor y)%Z.
Definition Zceil (x : R) := (- Zfloor (- x))%Z.
Theorem Zceil_ub :
∀ x : R,
(x ≤ Z2R (Zceil x))%R.
Theorem Zceil_glb :
∀ n x,
(x ≤ Z2R n)%R →
(Zceil x ≤ n)%Z.
Theorem Zceil_imp :
∀ n x,
(Z2R (n - 1) < x ≤ Z2R n)%R →
Zceil x = n.
Theorem Zceil_Z2R :
∀ n,
Zceil (Z2R n) = n.
Theorem Zceil_le :
∀ x y, (x ≤ y)%R →
(Zceil x ≤ Zceil y)%Z.
Theorem Zceil_floor_neq :
∀ x : R,
(Z2R (Zfloor x) ≠ x)%R →
(Zceil x = Zfloor x + 1)%Z.
Definition Ztrunc x := if Rlt_bool x 0 then Zceil x else Zfloor x.
Theorem Ztrunc_Z2R :
∀ n,
Ztrunc (Z2R n) = n.
Theorem Ztrunc_floor :
∀ x,
(0 ≤ x)%R →
Ztrunc x = Zfloor x.
Theorem Ztrunc_ceil :
∀ x,
(x ≤ 0)%R →
Ztrunc x = Zceil x.
Theorem Ztrunc_le :
∀ x y, (x ≤ y)%R →
(Ztrunc x ≤ Ztrunc y)%Z.
Theorem Ztrunc_opp :
∀ x,
Ztrunc (- x) = Zopp (Ztrunc x).
Theorem Ztrunc_abs :
∀ x,
Ztrunc (Rabs x) = Zabs (Ztrunc x).
Theorem Ztrunc_lub :
∀ n x,
(Z2R n ≤ Rabs x)%R →
(n ≤ Zabs (Ztrunc x))%Z.
Definition Zaway x := if Rlt_bool x 0 then Zfloor x else Zceil x.
Theorem Zaway_Z2R :
∀ n,
Zaway (Z2R n) = n.
Theorem Zaway_ceil :
∀ x,
(0 ≤ x)%R →
Zaway x = Zceil x.
Theorem Zaway_floor :
∀ x,
(x ≤ 0)%R →
Zaway x = Zfloor x.
Theorem Zaway_le :
∀ x y, (x ≤ y)%R →
(Zaway x ≤ Zaway y)%Z.
Theorem Zaway_opp :
∀ x,
Zaway (- x) = Zopp (Zaway x).
Theorem Zaway_abs :
∀ x,
Zaway (Rabs x) = Zabs (Zaway x).
End Floor_Ceil.
Section Zdiv_Rdiv.
Theorem Zfloor_div :
∀ x y,
y ≠ Z0 →
Zfloor (Z2R x / Z2R y) = (x / y)%Z.
End Zdiv_Rdiv.
Section pow.
Variable r : radix.
Theorem radix_pos : (0 < Z2R r)%R.
Well-used function called bpow for computing the power function β^e
Definition bpow e :=
match e with
| Zpos p ⇒ Z2R (Zpower_pos r p)
| Zneg p ⇒ Rinv (Z2R (Zpower_pos r p))
| Z0 ⇒ R1
end.
Theorem Z2R_Zpower_pos :
∀ n m,
Z2R (Zpower_pos n m) = powerRZ (Z2R n) (Zpos m).
Theorem bpow_powerRZ :
∀ e,
bpow e = powerRZ (Z2R r) e.
Theorem bpow_ge_0 :
∀ e : Z, (0 ≤ bpow e)%R.
Theorem bpow_gt_0 :
∀ e : Z, (0 < bpow e)%R.
Theorem bpow_plus :
∀ e1 e2 : Z, (bpow (e1 + e2) = bpow e1 × bpow e2)%R.
Theorem bpow_1 :
bpow 1 = Z2R r.
Theorem bpow_plus1 :
∀ e : Z, (bpow (e + 1) = Z2R r × bpow e)%R.
Theorem bpow_opp :
∀ e : Z, (bpow (-e) = /bpow e)%R.
Theorem Z2R_Zpower_nat :
∀ e : nat,
Z2R (Zpower_nat r e) = bpow (Z_of_nat e).
Theorem Z2R_Zpower :
∀ e : Z,
(0 ≤ e)%Z →
Z2R (Zpower r e) = bpow e.
Theorem bpow_lt :
∀ e1 e2 : Z,
(e1 < e2)%Z → (bpow e1 < bpow e2)%R.
Theorem lt_bpow :
∀ e1 e2 : Z,
(bpow e1 < bpow e2)%R → (e1 < e2)%Z.
Theorem bpow_le :
∀ e1 e2 : Z,
(e1 ≤ e2)%Z → (bpow e1 ≤ bpow e2)%R.
Theorem le_bpow :
∀ e1 e2 : Z,
(bpow e1 ≤ bpow e2)%R → (e1 ≤ e2)%Z.
Theorem bpow_inj :
∀ e1 e2 : Z,
bpow e1 = bpow e2 → e1 = e2.
Theorem bpow_exp :
∀ e : Z,
bpow e = exp (Z2R e × ln (Z2R r)).
match e with
| Zpos p ⇒ Z2R (Zpower_pos r p)
| Zneg p ⇒ Rinv (Z2R (Zpower_pos r p))
| Z0 ⇒ R1
end.
Theorem Z2R_Zpower_pos :
∀ n m,
Z2R (Zpower_pos n m) = powerRZ (Z2R n) (Zpos m).
Theorem bpow_powerRZ :
∀ e,
bpow e = powerRZ (Z2R r) e.
Theorem bpow_ge_0 :
∀ e : Z, (0 ≤ bpow e)%R.
Theorem bpow_gt_0 :
∀ e : Z, (0 < bpow e)%R.
Theorem bpow_plus :
∀ e1 e2 : Z, (bpow (e1 + e2) = bpow e1 × bpow e2)%R.
Theorem bpow_1 :
bpow 1 = Z2R r.
Theorem bpow_plus1 :
∀ e : Z, (bpow (e + 1) = Z2R r × bpow e)%R.
Theorem bpow_opp :
∀ e : Z, (bpow (-e) = /bpow e)%R.
Theorem Z2R_Zpower_nat :
∀ e : nat,
Z2R (Zpower_nat r e) = bpow (Z_of_nat e).
Theorem Z2R_Zpower :
∀ e : Z,
(0 ≤ e)%Z →
Z2R (Zpower r e) = bpow e.
Theorem bpow_lt :
∀ e1 e2 : Z,
(e1 < e2)%Z → (bpow e1 < bpow e2)%R.
Theorem lt_bpow :
∀ e1 e2 : Z,
(bpow e1 < bpow e2)%R → (e1 < e2)%Z.
Theorem bpow_le :
∀ e1 e2 : Z,
(e1 ≤ e2)%Z → (bpow e1 ≤ bpow e2)%R.
Theorem le_bpow :
∀ e1 e2 : Z,
(bpow e1 ≤ bpow e2)%R → (e1 ≤ e2)%Z.
Theorem bpow_inj :
∀ e1 e2 : Z,
bpow e1 = bpow e2 → e1 = e2.
Theorem bpow_exp :
∀ e : Z,
bpow e = exp (Z2R e × ln (Z2R r)).
Another well-used function for having the logarithm of a real number x to the base β
Record ln_beta_prop x := {
ln_beta_val :> Z ;
_ : (x ≠ 0)%R → (bpow (ln_beta_val - 1)%Z ≤ Rabs x < bpow ln_beta_val)%R
}.
Definition ln_beta :
∀ x : R, ln_beta_prop x.
Theorem bpow_lt_bpow :
∀ e1 e2,
(bpow (e1 - 1) < bpow e2)%R →
(e1 ≤ e2)%Z.
Theorem bpow_unique :
∀ x e1 e2,
(bpow (e1 - 1) ≤ x < bpow e1)%R →
(bpow (e2 - 1) ≤ x < bpow e2)%R →
e1 = e2.
Theorem ln_beta_unique :
∀ (x : R) (e : Z),
(bpow (e - 1) ≤ Rabs x < bpow e)%R →
ln_beta x = e :> Z.
Theorem ln_beta_opp :
∀ x,
ln_beta (-x) = ln_beta x :> Z.
Theorem ln_beta_abs :
∀ x,
ln_beta (Rabs x) = ln_beta x :> Z.
Theorem ln_beta_unique_pos :
∀ (x : R) (e : Z),
(bpow (e - 1) ≤ x < bpow e)%R →
ln_beta x = e :> Z.
Theorem ln_beta_le_abs :
∀ x y,
(x ≠ 0)%R → (Rabs x ≤ Rabs y)%R →
(ln_beta x ≤ ln_beta y)%Z.
Theorem ln_beta_le :
∀ x y,
(0 < x)%R → (x ≤ y)%R →
(ln_beta x ≤ ln_beta y)%Z.
Lemma ln_beta_lt_pos :
∀ x y,
(0 < x)%R → (0 < y)%R →
(ln_beta x < ln_beta y)%Z → (x < y)%R.
Theorem ln_beta_bpow :
∀ e, (ln_beta (bpow e) = e + 1 :> Z)%Z.
Theorem ln_beta_mult_bpow :
∀ x e, x ≠ R0 →
(ln_beta (x × bpow e) = ln_beta x + e :>Z)%Z.
Theorem ln_beta_le_bpow :
∀ x e,
x ≠ R0 →
(Rabs x < bpow e)%R →
(ln_beta x ≤ e)%Z.
Theorem ln_beta_gt_bpow :
∀ x e,
(bpow e ≤ Rabs x)%R →
(e < ln_beta x)%Z.
Theorem ln_beta_ge_bpow :
∀ x e,
(bpow (e - 1) ≤ Rabs x)%R →
(e ≤ ln_beta x)%Z.
Theorem bpow_ln_beta_gt :
∀ x,
(Rabs x < bpow (ln_beta x))%R.
Theorem ln_beta_le_Zpower :
∀ m e,
m ≠ Z0 →
(Zabs m < Zpower r e)%Z→
(ln_beta (Z2R m) ≤ e)%Z.
Theorem ln_beta_gt_Zpower :
∀ m e,
m ≠ Z0 →
(Zpower r e ≤ Zabs m)%Z →
(e < ln_beta (Z2R m))%Z.
Lemma ln_beta_mult :
∀ x y,
(x ≠ 0)%R → (y ≠ 0)%R →
(ln_beta x + ln_beta y - 1 ≤ ln_beta (x × y) ≤ ln_beta x + ln_beta y)%Z.
Lemma ln_beta_plus :
∀ x y,
(0 < y)%R → (y ≤ x)%R →
(ln_beta x ≤ ln_beta (x + y) ≤ ln_beta x + 1)%Z.
Lemma ln_beta_minus :
∀ x y,
(0 < y)%R → (y < x)%R →
(ln_beta (x - y) ≤ ln_beta x)%Z.
Lemma ln_beta_minus_lb :
∀ x y,
(0 < x)%R → (0 < y)%R →
(ln_beta y ≤ ln_beta x - 2)%Z →
(ln_beta x - 1 ≤ ln_beta (x - y))%Z.
Lemma ln_beta_div :
∀ x y : R,
(0 < x)%R → (0 < y)%R →
(ln_beta x - ln_beta y ≤ ln_beta (x / y) ≤ ln_beta x - ln_beta y + 1)%Z.
Lemma ln_beta_sqrt :
∀ x,
(0 < x)%R →
(2 × ln_beta (sqrt x) - 1 ≤ ln_beta x ≤ 2 × ln_beta (sqrt x))%Z.
End pow.
Section Bool.
Theorem eqb_sym :
∀ x y, Bool.eqb x y = Bool.eqb y x.
Theorem eqb_false :
∀ x y, x = negb y → Bool.eqb x y = false.
Theorem eqb_true :
∀ x y, x = y → Bool.eqb x y = true.
End Bool.
Section cond_Ropp.
Definition cond_Ropp (b : bool) m := if b then Ropp m else m.
Theorem Z2R_cond_Zopp :
∀ b m,
Z2R (cond_Zopp b m) = cond_Ropp b (Z2R m).
Theorem abs_cond_Ropp :
∀ b m,
Rabs (cond_Ropp b m) = Rabs m.
Theorem cond_Ropp_Rlt_bool :
∀ m,
cond_Ropp (Rlt_bool m 0) m = Rabs m.
Theorem cond_Ropp_involutive :
∀ b x,
cond_Ropp b (cond_Ropp b x) = x.
Theorem cond_Ropp_even_function :
∀ {A : Type} (f : R → A),
(∀ x, f (Ropp x) = f x) →
∀ b x, f (cond_Ropp b x) = f x.
Theorem cond_Ropp_odd_function :
∀ (f : R → R),
(∀ x, f (Ropp x) = Ropp (f x)) →
∀ b x, f (cond_Ropp b x) = cond_Ropp b (f x).
Theorem cond_Ropp_inj :
∀ b x y,
cond_Ropp b x = cond_Ropp b y → x = y.
Theorem cond_Ropp_mult_l :
∀ b x y,
cond_Ropp b (x × y) = (cond_Ropp b x × y)%R.
Theorem cond_Ropp_mult_r :
∀ b x y,
cond_Ropp b (x × y) = (x × cond_Ropp b y)%R.
Theorem cond_Ropp_plus :
∀ b x y,
cond_Ropp b (x + y) = (cond_Ropp b x + cond_Ropp b y)%R.
End cond_Ropp.
ln_beta_val :> Z ;
_ : (x ≠ 0)%R → (bpow (ln_beta_val - 1)%Z ≤ Rabs x < bpow ln_beta_val)%R
}.
Definition ln_beta :
∀ x : R, ln_beta_prop x.
Theorem bpow_lt_bpow :
∀ e1 e2,
(bpow (e1 - 1) < bpow e2)%R →
(e1 ≤ e2)%Z.
Theorem bpow_unique :
∀ x e1 e2,
(bpow (e1 - 1) ≤ x < bpow e1)%R →
(bpow (e2 - 1) ≤ x < bpow e2)%R →
e1 = e2.
Theorem ln_beta_unique :
∀ (x : R) (e : Z),
(bpow (e - 1) ≤ Rabs x < bpow e)%R →
ln_beta x = e :> Z.
Theorem ln_beta_opp :
∀ x,
ln_beta (-x) = ln_beta x :> Z.
Theorem ln_beta_abs :
∀ x,
ln_beta (Rabs x) = ln_beta x :> Z.
Theorem ln_beta_unique_pos :
∀ (x : R) (e : Z),
(bpow (e - 1) ≤ x < bpow e)%R →
ln_beta x = e :> Z.
Theorem ln_beta_le_abs :
∀ x y,
(x ≠ 0)%R → (Rabs x ≤ Rabs y)%R →
(ln_beta x ≤ ln_beta y)%Z.
Theorem ln_beta_le :
∀ x y,
(0 < x)%R → (x ≤ y)%R →
(ln_beta x ≤ ln_beta y)%Z.
Lemma ln_beta_lt_pos :
∀ x y,
(0 < x)%R → (0 < y)%R →
(ln_beta x < ln_beta y)%Z → (x < y)%R.
Theorem ln_beta_bpow :
∀ e, (ln_beta (bpow e) = e + 1 :> Z)%Z.
Theorem ln_beta_mult_bpow :
∀ x e, x ≠ R0 →
(ln_beta (x × bpow e) = ln_beta x + e :>Z)%Z.
Theorem ln_beta_le_bpow :
∀ x e,
x ≠ R0 →
(Rabs x < bpow e)%R →
(ln_beta x ≤ e)%Z.
Theorem ln_beta_gt_bpow :
∀ x e,
(bpow e ≤ Rabs x)%R →
(e < ln_beta x)%Z.
Theorem ln_beta_ge_bpow :
∀ x e,
(bpow (e - 1) ≤ Rabs x)%R →
(e ≤ ln_beta x)%Z.
Theorem bpow_ln_beta_gt :
∀ x,
(Rabs x < bpow (ln_beta x))%R.
Theorem ln_beta_le_Zpower :
∀ m e,
m ≠ Z0 →
(Zabs m < Zpower r e)%Z→
(ln_beta (Z2R m) ≤ e)%Z.
Theorem ln_beta_gt_Zpower :
∀ m e,
m ≠ Z0 →
(Zpower r e ≤ Zabs m)%Z →
(e < ln_beta (Z2R m))%Z.
Lemma ln_beta_mult :
∀ x y,
(x ≠ 0)%R → (y ≠ 0)%R →
(ln_beta x + ln_beta y - 1 ≤ ln_beta (x × y) ≤ ln_beta x + ln_beta y)%Z.
Lemma ln_beta_plus :
∀ x y,
(0 < y)%R → (y ≤ x)%R →
(ln_beta x ≤ ln_beta (x + y) ≤ ln_beta x + 1)%Z.
Lemma ln_beta_minus :
∀ x y,
(0 < y)%R → (y < x)%R →
(ln_beta (x - y) ≤ ln_beta x)%Z.
Lemma ln_beta_minus_lb :
∀ x y,
(0 < x)%R → (0 < y)%R →
(ln_beta y ≤ ln_beta x - 2)%Z →
(ln_beta x - 1 ≤ ln_beta (x - y))%Z.
Lemma ln_beta_div :
∀ x y : R,
(0 < x)%R → (0 < y)%R →
(ln_beta x - ln_beta y ≤ ln_beta (x / y) ≤ ln_beta x - ln_beta y + 1)%Z.
Lemma ln_beta_sqrt :
∀ x,
(0 < x)%R →
(2 × ln_beta (sqrt x) - 1 ≤ ln_beta x ≤ 2 × ln_beta (sqrt x))%Z.
End pow.
Section Bool.
Theorem eqb_sym :
∀ x y, Bool.eqb x y = Bool.eqb y x.
Theorem eqb_false :
∀ x y, x = negb y → Bool.eqb x y = false.
Theorem eqb_true :
∀ x y, x = y → Bool.eqb x y = true.
End Bool.
Section cond_Ropp.
Definition cond_Ropp (b : bool) m := if b then Ropp m else m.
Theorem Z2R_cond_Zopp :
∀ b m,
Z2R (cond_Zopp b m) = cond_Ropp b (Z2R m).
Theorem abs_cond_Ropp :
∀ b m,
Rabs (cond_Ropp b m) = Rabs m.
Theorem cond_Ropp_Rlt_bool :
∀ m,
cond_Ropp (Rlt_bool m 0) m = Rabs m.
Theorem cond_Ropp_involutive :
∀ b x,
cond_Ropp b (cond_Ropp b x) = x.
Theorem cond_Ropp_even_function :
∀ {A : Type} (f : R → A),
(∀ x, f (Ropp x) = f x) →
∀ b x, f (cond_Ropp b x) = f x.
Theorem cond_Ropp_odd_function :
∀ (f : R → R),
(∀ x, f (Ropp x) = Ropp (f x)) →
∀ b x, f (cond_Ropp b x) = cond_Ropp b (f x).
Theorem cond_Ropp_inj :
∀ b x y,
cond_Ropp b x = cond_Ropp b y → x = y.
Theorem cond_Ropp_mult_l :
∀ b x y,
cond_Ropp b (x × y) = (cond_Ropp b x × y)%R.
Theorem cond_Ropp_mult_r :
∀ b x y,
cond_Ropp b (x × y) = (x × cond_Ropp b y)%R.
Theorem cond_Ropp_plus :
∀ b x y,
cond_Ropp b (x + y) = (cond_Ropp b x + cond_Ropp b y)%R.
End cond_Ropp.
Ltac bpow_simplify :=
repeat
match goal with
| |- context [(bpow _ _ × bpow _ _)] ⇒
rewrite <- bpow_plus
| |- context [(?X1 × bpow _ _ × bpow _ _)] ⇒
rewrite (Rmult_assoc X1); rewrite <- bpow_plus
| |- context [(?X1 × (?X2 × bpow _ _) × bpow _ _)] ⇒
rewrite <- (Rmult_assoc X1 X2); rewrite (Rmult_assoc (X1 × X2));
rewrite <- bpow_plus
end;
repeat
match goal with
| |- context [(bpow _ ?X)] ⇒
progress ring_simplify X
end;
change (bpow _ 0) with 1;
repeat
match goal with
| |- context [(_ × 1)] ⇒
rewrite Rmult_1_r
end.
repeat
match goal with
| |- context [(bpow _ _ × bpow _ _)] ⇒
rewrite <- bpow_plus
| |- context [(?X1 × bpow _ _ × bpow _ _)] ⇒
rewrite (Rmult_assoc X1); rewrite <- bpow_plus
| |- context [(?X1 × (?X2 × bpow _ _) × bpow _ _)] ⇒
rewrite <- (Rmult_assoc X1 X2); rewrite (Rmult_assoc (X1 × X2));
rewrite <- bpow_plus
end;
repeat
match goal with
| |- context [(bpow _ ?X)] ⇒
progress ring_simplify X
end;
change (bpow _ 0) with 1;
repeat
match goal with
| |- context [(_ × 1)] ⇒
rewrite Rmult_1_r
end.