Timings for ConstructiveCauchyRealsMult.v
- /home/gitlab-runner/builds/v6HyzL39/0/coq/coq/_bench/opam.OLD/ocaml-OLD/.opam-switch/build/coq-stdlib.dev/_build/default/theories//./Reals/Cauchy/ConstructiveCauchyRealsMult.timing
- /home/gitlab-runner/builds/v6HyzL39/0/coq/coq/_bench/opam.NEW/ocaml-NEW/.opam-switch/build/coq-stdlib.dev/_build/default/theories//./Reals/Cauchy/ConstructiveCauchyRealsMult.timing
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * Copyright INRIA, CNRS and contributors *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
(************************************************************************)
(** The multiplication and division of Cauchy reals.
WARNING: this file is experimental and likely to change in future releases.
*)
Require Import QArith Qabs Qround Qpower.
Require Import Logic.ConstructiveEpsilon.
Require Export ConstructiveCauchyReals.
Local Open Scope CReal_scope.
Definition CReal_mult_seq (x y : CReal) :=
(fun n : Z => seq x (n - scale y - 1)%Z
* seq y (n - scale x - 1)%Z).
Definition CReal_mult_scale (x y : CReal) : Z :=
x.(scale) + y.(scale).
Local Ltac simplify_Qpower_exponent :=
match goal with |- context [(_ ^ ?a)%Q] => ring_simplify a end.
Local Ltac simplify_Qabs :=
match goal with |- context [(Qabs ?a)%Q] => ring_simplify a end.
Local Ltac simplify_Qabs_in H :=
match type of H with context [(Qabs ?a)%Q] => ring_simplify a in H end.
Local Ltac field_simplify_Qabs :=
match goal with |- context [(Qabs ?a)%Q] => field_simplify a end.
Local Ltac pose_Qabs_pos :=
match goal with |- context [(Qabs ?a)%Q] => pose proof Qabs_nonneg a end.
Local Ltac simplify_Qle :=
match goal with |- (?l <= ?r)%Q => ring_simplify l; ring_simplify r end.
Local Ltac simplify_Qle_in H :=
match type of H with (?l <= ?r)%Q => ring_simplify l in H; ring_simplify r in H end.
Local Ltac simplify_Qlt :=
match goal with |- (?l < ?r)%Q => ring_simplify l; ring_simplify r end.
Local Ltac simplify_Qlt_in H :=
match type of H with (?l < ?r)%Q => ring_simplify l in H; ring_simplify r in H end.
Local Ltac simplify_seq_idx :=
match goal with |- context [seq ?x ?n] => progress ring_simplify n end.
Local Lemma Weaken_Qle_QpowerAddExp: forall (q : Q) (n m : Z),
(m >= 0)%Z
-> (q <= 2^n)%Q
-> (q <= 2^(n+m))%Q.
pose proof Qpower_le_compat_l 2 n (n+m) ltac:(lia) ltac:(lra).
Local Lemma Weaken_Qle_QpowerRemSubExp: forall (q : Q) (n m : Z),
(m >= 0)%Z
-> (q <= 2^(n-m))%Q
-> (q <= 2^n)%Q.
pose proof Qpower_le_compat_l 2 (n-m) n ltac:(lia) ltac:(lra).
Local Lemma Weaken_Qle_QpowerFac: forall (q r : Q) (n : Z),
(r >= 1)%Q
-> (q <= 2^n)%Q
-> (q <= r * 2^n)%Q.
rewrite <- (Qmult_1_l (2^n)%Q) in Hle.
pose proof Qmult_le_compat_r 1 r (2^n)%Q Hrge1 (Qpower_pos 2 n ltac:(lra)) as Hpow.
Lemma CReal_mult_cauchy: forall (x y : CReal),
QCauchySeq (CReal_mult_seq x y).
assert(forall xp xq yp yq : Q, xp * yp - xq * yq == (xp - xq) * yp + xq * (yp - yq))%Q
as H by (intros; ring).
apply (Qle_lt_trans _ _ _ (Qabs_triangle _ _)).
replace n with ((n-1)+1)%Z by ring.
rewrite Qpower_plus by lra.
setoid_replace (2 ^ (n - 1) * 2 ^1)%Q with (2 ^ (n - 1) + 2 ^ (n - 1))%Q by ring.
apply Qplus_lt_le_compat.
apply (Qle_lt_trans _ ((2 ^ (n - scale y - 1)) * Qabs (seq y (p - scale x - 1)))).
apply (Qmult_lt_l _ _ (2 ^ -(n - scale y - 1))%Q).
rewrite Qmult_assoc, <- Qpower_plus by lra.
rewrite <- Qpower_plus by lra.
simplify_Qpower_exponent; rewrite Qpower_0_r, Qmult_1_l.
simplify_Qpower_exponent.
apply (Qle_lt_trans _ ((2 ^ (n - scale x - 1)) * Qabs (seq x (q - scale y - 1)))).
rewrite Qmult_comm; apply Qmult_le_compat_r.
apply Qlt_le_weak; apply (cauchy y); lia.
apply (Qmult_lt_l _ _ (2 ^ -(n - scale x - 1))%Q).
rewrite Qmult_assoc, <- Qpower_plus by lra.
rewrite <- Qpower_plus by lra.
simplify_Qpower_exponent; rewrite Qpower_0_r, Qmult_1_l.
simplify_Qpower_exponent.
Lemma CReal_mult_bound : forall (x y : CReal),
QBound (CReal_mult_seq x y) (CReal_mult_scale x y).
unfold CReal_mult_seq, CReal_mult_scale.
pose proof (bound x (k - scale y - 1)%Z) as Hxbnd.
pose proof (bound y (k - scale x - 1)%Z) as Hybnd.
pose proof Qabs_nonneg (seq x (k - scale y - 1)) as Habsx.
pose proof Qabs_nonneg (seq y (k - scale x - 1)) as Habsy.
rewrite Qabs_Qmult; rewrite Qpower_plus by lra.
apply Qmult_lt_compat_nonneg; lra.
Definition CReal_mult (x y : CReal) : CReal :=
{|
seq := CReal_mult_seq x y;
scale := CReal_mult_scale x y;
cauchy := CReal_mult_cauchy x y;
bound := CReal_mult_bound x y
|}.
Infix "*" := CReal_mult : CReal_scope.
Lemma CReal_mult_comm : forall x y : CReal, x * y == y * x.
assert (forall x y : CReal, x * y <= y * x) as H.
apply (Qlt_not_le _ _ nmaj).
unfold CReal_mult, CReal_mult_seq; do 2 rewrite CReal_red_seq.
pose proof Qpower_0_lt 2 n ltac:(lra); lra.
(* ToDo: make a tactic for this *)
Lemma CReal_red_scale: forall (a : Z -> Q) (b : Z) (c : QCauchySeq a) (d : QBound a b),
scale (mkCReal a b c d) = b.
Lemma CReal_mult_proper_0_l : forall x y : CReal,
y == 0 -> x * y == 0.
apply CRealEq_diff; intros n.
unfold CReal_mult, CReal_mult_seq, inject_Q; do 2 rewrite CReal_red_seq.
rewrite CRealEq_diff in Hyeq0.
unfold inject_Q in Hyeq0; rewrite CReal_red_seq in Hyeq0.
specialize (Hyeq0 (n - scale x - 1)%Z).
rewrite Qpower_minus_pos in Hyeq0 by lra; simplify_Qle_in Hyeq0.
pose proof bound x (n - scale y - 1)%Z as Hxbnd.
apply Weaken_Qle_QpowerFac; [lra|].
(* Now split the power of 2 and solve the goal*)
replace n with ((scale x) + (n - scale x))%Z at 3 by ring.
rewrite Qpower_plus by lra.
apply Qmult_le_compat_nonneg;
(pose_Qabs_pos; lra).
Lemma CReal_mult_0_r : forall r, r * 0 == 0.
apply CReal_mult_proper_0_l.
Lemma CReal_mult_0_l : forall r, 0 * r == 0.
Lemma CReal_scale_sep0_limit : forall (x : CReal) (n : Z),
(2 * (2^n)%Q < seq x n)%Q
-> (n <= scale x - 2)%Z.
pose proof bound x n as Hxbnd.
apply Qabs_Qlt_condition in Hxbnd.
destruct Hxbnd as [_ Hxbnd].
apply (Qlt_trans _ _ _ Hnx) in Hxbnd.
replace n with ((n+1)-1)%Z in Hxbnd by lia.
rewrite Qpower_minus_pos in Hxbnd by lra.
apply (Qpower_lt_compat_l_inv) in Hxbnd.
(* Correctness lemma for the Definition CReal_mult_lt_0_compat below. *)
Lemma CReal_mult_lt_0_compat_correct
: forall (x y : CReal) (Hx : 0 < x) (Hy : 0 < y),
(2 * 2^(proj1_sig Hx + proj1_sig Hy - 1)%Z <
seq (x * y)%CReal (proj1_sig Hx + proj1_sig Hy - 1)%Z -
seq (inject_Q 0) (proj1_sig Hx + proj1_sig Hy - 1)%Z)%Q.
destruct Hx as [nx Hx], Hy as [ny Hy]; unfold proj1_sig.
unfold inject_Q, Qminus in Hx.
rewrite CReal_red_seq, Qplus_0_r in Hx.
unfold inject_Q, Qminus in Hy.
rewrite CReal_red_seq, Qplus_0_r in Hy.
unfold CReal_mult, CReal_mult_seq, inject_Q; do 2 rewrite CReal_red_seq.
rewrite Qpower_minus_pos by lra.
rewrite Qpower_plus by lra.
apply Qmult_lt_compat_nonneg.
pose proof Qpower_0_lt 2 nx; lra.
pose proof CReal_scale_sep0_limit y ny Hy as Hlimy.
pose proof cauchy x nx nx (nx + ny - scale y - 2)%Z ltac:(lia) ltac:(lia) as Hbndx.
apply Qabs_Qlt_condition in Hbndx.
pose proof Qpower_0_lt 2 ny; lra.
pose proof CReal_scale_sep0_limit x nx Hx as Hlimx.
pose proof cauchy y ny ny (nx + ny - scale x - 2)%Z ltac:(lia) ltac:(lia) as Hbndy.
apply Qabs_Qlt_condition in Hbndy.
(* Strict inequality on CReal is in sort Type, for example
used in the computation of division. *)
Definition CReal_mult_lt_0_compat : forall x y : CReal,
0 < x -> 0 < y -> 0 < x * y
:= fun x y Hx Hy => exist _ (proj1_sig Hx + proj1_sig Hy - 1)%Z
(CReal_mult_lt_0_compat_correct
x y Hx Hy).
Lemma CReal_mult_plus_distr_l : forall r1 r2 r3 : CReal,
r1 * (r2 + r3) == (r1 * r2) + (r1 * r3).
intros x y z; apply CRealEq_diff; intros n.
unfold CReal_mult, CReal_mult_seq, CReal_mult_scale, CReal_plus, CReal_plus_seq, CReal_plus_scale.
do 5 rewrite CReal_red_seq.
do 1 rewrite CReal_red_scale.
do 2 rewrite Qred_correct.
assert (forall y' z': CReal,
Qabs (
seq x (n - Z.max (scale y') (scale z') - 2) * seq y' (n - scale x - 2)
- seq x (n - scale y' - 2) * seq y' (n - scale x - 2))
<= 2 ^ n )%Q as Hdiffbnd.
assert (forall a b c : Q, a*c-b*c==(a-b)*c)%Q as H by (intros; ring).
pose proof cauchy x (n - (scale y') - 2)%Z (n - Z.max (scale y') (scale z') - 2)%Z (n - scale y' - 2)%Z
ltac:(lia) ltac:(lia) as Hxbnd.
pose proof bound y' (n - scale x - 2)%Z as Hybnd.
replace n with ((n - scale y' - 2) + scale y' + 2)%Z at 4 by lia.
apply Weaken_Qle_QpowerAddExp.
rewrite Qpower_plus, Qabs_Qmult by lra.
apply Qmult_le_compat_nonneg; (split; [apply Qabs_nonneg | lra]).
pose proof Hdiffbnd y z as Hyz.
pose proof Hdiffbnd z y as Hzy; clear Hdiffbnd.
pose proof Qplus_le_compat _ _ _ _ Hyz Hzy as Hcomb; clear Hyz Hzy.
apply (Qle_trans _ _ _ (Qabs_triangle _ _)) in Hcomb.
rewrite (Z.max_comm (scale z) (scale y)) in Hcomb .
rewrite Qabs_Qle_condition in Hcomb |- *.
Lemma CReal_mult_plus_distr_r : forall r1 r2 r3 : CReal,
(r2 + r3) * r1 == (r2 * r1) + (r3 * r1).
rewrite CReal_mult_comm, CReal_mult_plus_distr_l,
<- (CReal_mult_comm r1), <- (CReal_mult_comm r1).
Lemma CReal_opp_mult_distr_r
: forall r1 r2 : CReal, - (r1 * r2) == r1 * (- r2).
apply (CReal_plus_eq_reg_l (r1*r2)).
rewrite CReal_plus_opp_r, <- CReal_mult_plus_distr_l.
apply CReal_mult_proper_0_l.
Lemma CReal_mult_proper_l : forall x y z : CReal,
y == z -> x * y == x * z.
apply (CReal_plus_eq_reg_l (-(x*z))).
rewrite CReal_plus_opp_l, CReal_opp_mult_distr_r.
rewrite <- CReal_mult_plus_distr_l.
apply CReal_mult_proper_0_l.
Lemma CReal_mult_proper_r : forall x y z : CReal,
y == z -> y * x == z * x.
rewrite CReal_mult_comm, (CReal_mult_comm z).
apply CReal_mult_proper_l, H.
Lemma CReal_mult_assoc : forall x y z : CReal,
(x * y) * z == x * (y * z).
intros x y z; apply CRealEq_diff; intros n.
(* Expand and simplify the goal *)
unfold CReal_mult, CReal_mult_seq, CReal_mult_scale.
do 4 rewrite CReal_red_seq.
do 2 rewrite CReal_red_scale.
(* Todo: it is a bug in ring_simplify that the scales are not sorted *)
replace (n - scale z - scale y)%Z with (n - scale y - scale z)%Z by ring.
replace (n - scale z - scale x)%Z with (n - scale x - scale z)%Z by ring.
(* Rearrange the goal such that it used only scale and cauchy bounds *)
(* Todo: it is also a bug in ring_simplify that the seq terms are not sorted by the first variable *)
assert (forall a1 a2 b c1 c2 : Q, a1*b*c1+(-1)*b*a2*c2==(a1*c1-a2*c2)*b)%Q as H by (intros; ring).
remember (seq x (n - scale y - scale z - 1) - seq x (n - scale y - scale z - 2))%Q as dx eqn:Heqdx.
remember (seq z (n - scale x - scale y - 1) - seq z (n - scale x - scale y - 2))%Q as dz eqn:Heqdz.
setoid_replace (seq x (n - scale y - scale z - 1)) with (seq x (n - scale y - scale z - 2) + dx)%Q
by (rewrite Heqdx; ring).
setoid_replace (seq z (n - scale x - scale y - 1)) with (seq z (n - scale x - scale y - 2) + dz)%Q
by (rewrite Heqdz; ring).
match goal with |- (Qabs (?a * _) <= _)%Q => ring_simplify a end.
(* Now pose the scale and cauchy bounds we need to prove this, so that we see how to split the deviation budget *)
pose proof bound x (n - scale y - scale z - 2)%Z as Hbndx.
pose proof bound z (n - scale x - scale y - 2)%Z as Hbndz.
pose proof bound y (n - scale x - scale z - 2)%Z as Hbndy.
pose proof cauchy x (n - scale y - scale z - 1)%Z (n - scale y - scale z - 1)%Z (n - scale y - scale z - 2)%Z
ltac:(lia) ltac:(lia) as Hbnddx; rewrite <- Heqdx in Hbnddx; clear Heqdx.
pose proof cauchy z (n - scale x - scale y - 1)%Z (n - scale x - scale y - 1)%Z (n - scale x - scale y - 2)%Z
ltac:(lia) ltac:(lia) as Hbnddz; rewrite <- Heqdz in Hbnddz; clear Heqdz.
(* The rest is elementary arithmetic ... *)
replace n with ((n - scale y) + scale y)%Z at 4 by lia.
rewrite Qpower_plus by lra.
apply Qmult_le_compat_nonneg.
2: (split; [apply Qabs_nonneg | lra]).
split; [apply Qabs_nonneg|].
apply (Qle_trans _ _ _ (Qabs_triangle _ _)).
setoid_replace (2 * 2 ^ (n - scale y))%Q with (2 ^ (n - scale y) + 2 ^ (n - scale y))%Q by ring.
replace (n - scale y)%Z with (scale x + (n - scale x - scale y))%Z at 2 by lia.
rewrite Qpower_plus by lra.
apply Qmult_le_compat_nonneg.
(split; [apply Qabs_nonneg | lra]).
split; [apply Qabs_nonneg|].
apply (Weaken_Qle_QpowerRemSubExp _ _ 1 ltac:(lia)), Qlt_le_weak, Hbnddz.
replace (n - scale y)%Z with (scale z + (n - scale y - scale z))%Z by lia.
rewrite Qpower_plus by lra.
apply Qmult_le_compat_nonneg.
split; [apply Qabs_nonneg|].
rewrite <- Qabs_opp; simplify_Qabs; lra.
split; [apply Qabs_nonneg|].
apply (Weaken_Qle_QpowerRemSubExp _ _ 1 ltac:(lia)), Qlt_le_weak, Hbnddx.
Lemma CReal_mult_1_l : forall r: CReal,
1 * r == r.
intros r; apply CRealEq_diff; intros n.
unfold inject_Q, CReal_mult, CReal_mult_seq, CReal_mult_scale.
do 2 rewrite CReal_red_seq.
do 1 rewrite CReal_red_scale.
change (Qbound_ltabs_ZExp2 1)%Z with 1%Z.
pose proof cauchy r n (n-2)%Z n ltac:(lia) ltac:(lia) as Hrbnd.
apply Qabs_Qlt_condition in Hrbnd.
apply Qabs_Qle_condition.
Lemma CReal_isRingExt : ring_eq_ext CReal_plus CReal_mult CReal_opp CRealEq.
apply CReal_plus_morph; assumption.
apply (CRealEq_trans _ (CReal_mult x t)).
apply CReal_mult_proper_l.
apply (CRealEq_trans _ (CReal_mult t x)).
apply (CRealEq_trans _ (CReal_mult t y)).
apply CReal_mult_proper_l.
apply (CReal_plus_eq_reg_l x).
apply (CRealEq_trans _ (inject_Q 0)).
apply (CRealEq_trans _ (CReal_plus y (CReal_opp y))).
apply CReal_plus_proper_r.
Lemma CReal_isRing : ring_theory (inject_Q 0) (inject_Q 1)
CReal_plus CReal_mult
CReal_minus CReal_opp
CRealEq.
rewrite <- (CReal_mult_comm z).
rewrite CReal_mult_plus_distr_l.
apply (CRealEq_trans _ (CReal_plus (CReal_mult x z) (CReal_mult z y))).
apply CReal_plus_proper_r.
apply CReal_plus_proper_l.
Add Parametric Morphism : CReal_mult
with signature CRealEq ==> CRealEq ==> CRealEq
as CReal_mult_morph.
#[global]
Instance CReal_mult_morph_T
: CMorphisms.Proper
(CMorphisms.respectful CRealEq (CMorphisms.respectful CRealEq CRealEq)) CReal_mult.
Add Parametric Morphism : CReal_opp
with signature CRealEq ==> CRealEq
as CReal_opp_morph.
apply (Ropp_ext CReal_isRingExt).
#[global]
Instance CReal_opp_morph_T
: CMorphisms.Proper
(CMorphisms.respectful CRealEq CRealEq) CReal_opp.
Add Parametric Morphism : CReal_minus
with signature CRealEq ==> CRealEq ==> CRealEq
as CReal_minus_morph.
#[global]
Instance CReal_minus_morph_T
: CMorphisms.Proper
(CMorphisms.respectful CRealEq (CMorphisms.respectful CRealEq CRealEq)) CReal_minus.
Add Ring CRealRing : CReal_isRing.
Lemma CReal_mult_1_r : forall r, r * 1 == r.
Lemma CReal_opp_mult_distr_l
: forall r1 r2 : CReal, - (r1 * r2) == (- r1) * r2.
Lemma CReal_mult_lt_compat_l : forall x y z : CReal,
0 < x -> y < z -> x*y < x*z.
apply (CReal_plus_lt_reg_l
(CReal_opp (CReal_mult x y))).
pose proof CReal_plus_opp_r.
unfold CReal_minus in H1.
rewrite CReal_mult_comm, CReal_opp_mult_distr_l, CReal_mult_comm.
rewrite <- CReal_mult_plus_distr_l.
apply CReal_mult_lt_0_compat.
apply (CReal_plus_lt_reg_l y).
rewrite CReal_plus_comm, CReal_plus_0_l.
rewrite <- CReal_plus_assoc, H1, CReal_plus_0_l.
Lemma CReal_mult_lt_compat_r : forall x y z : CReal,
0 < x -> y < z -> y*x < z*x.
rewrite <- (CReal_mult_comm x), <- (CReal_mult_comm x).
apply (CReal_mult_lt_compat_l x); assumption.
Lemma CReal_mult_eq_reg_l : forall (r r1 r2 : CReal),
r # 0
-> r * r1 == r * r2
-> r1 == r2.
apply (CReal_mult_lt_compat_l (-r)) in abs.
rewrite <- CReal_opp_mult_distr_l, <- CReal_opp_mult_distr_l, H0 in abs.
exact (CRealLe_refl _ abs).
apply (CReal_plus_lt_reg_l r).
rewrite CReal_plus_opp_r, CReal_plus_comm, CReal_plus_0_l.
apply (CReal_mult_lt_compat_l (-r)) in abs.
rewrite <- CReal_opp_mult_distr_l, <- CReal_opp_mult_distr_l, H0 in abs.
exact (CRealLe_refl _ abs).
apply (CReal_plus_lt_reg_l r).
rewrite CReal_plus_opp_r, CReal_plus_comm, CReal_plus_0_l.
apply (CReal_mult_lt_compat_l r) in abs.
exact (CRealLe_refl _ abs).
apply (CReal_mult_lt_compat_l r) in abs.
exact (CRealLe_refl _ abs).
Lemma CReal_abs_appart_zero : forall (x : CReal) (n : Z),
(2*2^n < Qabs (seq x n))%Q
-> 0 # x.
destruct (Qlt_le_dec 0 (seq x n)).
rewrite Qabs_pos in Hapart; lra.
rewrite Qabs_neg in Hapart; lra.
(*********************************************************)
(** * Field *)
(*********************************************************)
Lemma CRealArchimedean
: forall x:CReal, { n:Z & x < inject_Z n < x+2 }.
(* We add 3/2: 1/2 for the average rounding of floor + 1 to center in the interval.
This gives a margin of 1/2 in each inequality.
Since we need margin for Qlt of 2*2^-n plus 2^-n for the real addition, we need n=-3 *)
remember (seq x (-3)%Z + (3#2))%Q as q eqn: Heqq.
pose proof (Qlt_floor q) as Hltfloor; unfold QArith_base.inject_Z in Hltfloor.
pose proof (Qfloor_le q) as Hfloorle; unfold QArith_base.inject_Z in Hfloorle.
exists (Qfloor q); split.
unfold inject_Z, inject_Q, CRealLt.
setoid_replace (2 * 2 ^ (-3))%Q with (1#4)%Q by reflexivity.
subst q; rewrite <- Qinv_plus_distr in Hltfloor.
unfold inject_Z, inject_Q, CReal_plus, CReal_plus_seq, CRealLt.
do 3 rewrite CReal_red_seq.
setoid_replace (2 * 2 ^ (-3))%Q with (1#4)%Q by reflexivity.
simplify_seq_idx; rewrite Qred_correct.
pose proof cauchy x (-3)%Z (-3)%Z (-4)%Z ltac:(lia) ltac:(lia) as Hbnddx.
rewrite Qabs_Qlt_condition in Hbnddx.
setoid_replace (2 ^ (-3))%Q with (1#8)%Q in Hbnddx by reflexivity.
subst q; rewrite <- Qinv_plus_distr in Hltfloor.
(* ToDo: This is not efficient.
We take the n for the 2^n lower bound fro x>0.
This limit can be arbitrarily small and far away from beeing tight.
To make this really computational, we need to compute a tight
limit starting from scale x and going down in steps of say 16 bits,
something which is still easy to compute but likely to succeed. *)
Definition CRealLowerBound (x : CReal) (xPos : 0<x) : Z :=
proj1_sig (xPos).
Lemma CRealLowerBoundSpec: forall (x : CReal) (xPos : 0<x),
forall p : Z, (p <= (CRealLowerBound x xPos))%Z
-> (seq x p > 2^(CRealLowerBound x xPos))%Q.
unfold CRealLowerBound in *.
destruct xPos as [n Hn]; unfold proj1_sig in *.
unfold inject_Q in Hn; rewrite CReal_red_seq in Hn.
pose proof cauchy x n n p ltac:(lia) ltac:(lia) as Hxbnd.
rewrite Qabs_Qlt_condition in Hxbnd.
Lemma CRealLowerBound_lt_scale: forall (r : CReal) (Hrpos : 0 < r),
(CRealLowerBound r Hrpos < scale r)%Z.
pose proof CRealLowerBoundSpec r Hrpos (CRealLowerBound r Hrpos) ltac:(lia) as Hlow.
pose proof bound r (CRealLowerBound r Hrpos) as Hup; unfold QBound in Hup.
apply Qabs_Qlt_condition in Hup.
pose proof Qlt_trans _ _ _ Hlow Hup as Hpow.
apply Qpower_lt_compat_l_inv in Hpow.
(**
Note on the convergence modulus for x when computing 1/x:
Thinking in terms of absolute and relative errors and scales we get:
- 2^n is absolute error of 1/x (the requested error)
- 2^k is a lower bound of x -> 2^-k is an upper bound of 1/x
For simplicity lets’ say 2^k is the scale of x and 2^-k is the scale of 1/x.
With this we get:
- relative error of 1/x = absolute error of 1/x / scale of 1/x = 2^n / 2^-k = 2^(n+k)
- 1/x maintains relative error
- relative error of x = relative error 1/x = 2^(n+k)
- absolute error of x = relative error x * scale of x = 2^(n+k) * 2^k
- absolute error of x = 2^(n+2*k)
*)
Definition CReal_inv_pos_cm (x : CReal) (xPos : 0 < x) (n : Z):=
(Z.min (CRealLowerBound x xPos) (n + 2 * (CRealLowerBound x xPos)))%Z.
Definition CReal_inv_pos_seq (x : CReal) (xPos : 0 < x) (n : Z) :=
(/ seq x (CReal_inv_pos_cm x xPos n))%Q.
Definition CReal_inv_pos_scale (x : CReal) (xPos : 0 < x) : Z :=
(- (CRealLowerBound x xPos))%Z.
Lemma CReal_inv_pos_cauchy: forall (x : CReal) (xPos : 0 < x),
QCauchySeq (CReal_inv_pos_seq x xPos).
intros x Hxpos n p q Hp Hq; unfold CReal_inv_pos_seq.
unfold CReal_inv_pos_cm; remember (CRealLowerBound x Hxpos) as k.
(* These auxilliary lemmas are required a few times below *)
assert (forall m:Z, (2^k < seq x (Z.min k (m + 2 * k))))%Q as AuxAppart.
pose proof CRealLowerBoundSpec x Hxpos (Z.min k (m + 2 * k))%Z ltac:(lia) as H1.
assert (forall m:Z, (0 < seq x (Z.min k (m + 2 * k))))%Q as AuxPos.
pose proof AuxAppart m as H1.
pose proof Qpower_0_lt 2 k as H2.
assert( forall a b : Q, (a>0)%Q -> (b>0)%Q -> (/a - /b == (b - a) / (a * b))%Q )
as H by (intros; field; lra); rewrite H by apply AuxPos; clear H.
setoid_rewrite Qabs_Qmult; setoid_rewrite Qabs_Qinv.
setoid_rewrite <- (Qmult_0_l 0); setoid_rewrite Qabs_Qmult.
apply Qmult_lt_compat_nonneg.
1,2: split; [lra | apply Qabs_gt, AuxPos].
assert( forall r:Q, (r == (r/2^k/2^k)*(2^k*2^k))%Q )
as H by (intros r; field; apply Qpower_not_0; lra); rewrite H; clear H.
apply Qmult_lt_compat_nonneg.
do 2 (apply Qle_shift_div_l; [ apply Qpower_0_lt; lra | rewrite Qmult_0_l ]).
do 2 (apply Qlt_shift_div_r; [apply Qpower_0_lt; lra|]).
do 2 rewrite <- Qpower_plus by lra.
apply (cauchy x (n+k+k)%Z); lia.
rewrite <- Qpower_plus by lra.
setoid_rewrite Qabs_Qmult; apply Qmult_lt_compat_nonneg.
1,2: split; [apply Qpower_pos; lra | ].
1,2: apply Qabs_gt, AuxAppart.
Lemma CReal_inv_pos_bound : forall (x : CReal) (Hxpos : 0 < x),
QBound (CReal_inv_pos_seq x Hxpos) (CReal_inv_pos_scale x Hxpos).
unfold CReal_inv_pos_seq, CReal_inv_pos_scale, CReal_inv_pos_cm.
remember (CRealLowerBound x Hxpos) as k.
pose proof CRealLowerBoundSpec x Hxpos (Z.min k (n + 2 * k))%Z ltac:(lia) as Hlb.
2: apply Qinv_le_0_compat; pose proof Qpower_pos 2 k; lra.
rewrite Qpower_opp; apply -> Qinv_lt_contravar.
pose proof Qpower_0_lt 2 k; lra.
Definition CReal_inv_pos (x : CReal) (Hxpos : 0 < x) : CReal :=
{|
seq := CReal_inv_pos_seq x Hxpos;
scale := CReal_inv_pos_scale x Hxpos;
cauchy := CReal_inv_pos_cauchy x Hxpos;
bound := CReal_inv_pos_bound x Hxpos
|}.
Definition CReal_neg_lt_pos : forall x : CReal, x < 0 -> 0 < -x.
unfold CReal_opp_seq, Qminus.
abstract now rewrite Qplus_0_r, <- (Qplus_0_l (- seq x n)).
Definition CReal_inv (x : CReal) (xnz : x # 0) : CReal
:= match xnz with
| inl xNeg => - CReal_inv_pos (-x) (CReal_neg_lt_pos x xNeg)
| inr xPos => CReal_inv_pos x xPos
end.
Notation "/ x" := (CReal_inv x) (at level 35, right associativity) : CReal_scope.
Lemma CReal_inv_0_lt_compat
: forall (r : CReal) (rnz : r # 0),
0 < r -> 0 < ((/ r) rnz).
intros r Hrnz Hrpos; unfold CReal_inv; cbn.
apply CRealLt_asym in Hrpos.
exists (- (scale r) - 1)%Z.
unfold inject_Q; rewrite CReal_red_seq; simplify_Qlt.
unfold CReal_inv_pos; rewrite CReal_red_seq.
unfold CReal_inv_pos_seq.
pose proof bound r as Hrbnd; unfold QBound in Hrbnd.
rewrite Qpower_minus by lra.
field_simplify (2 * (2 ^ (- scale r) / 2 ^ 1))%Q.
rewrite Qpower_opp; apply -> Qinv_lt_contravar.
setoid_rewrite Qabs_Qlt_condition in Hrbnd.
specialize (Hrbnd (CReal_inv_pos_cm r c (- scale r - 1))%Z).
pose proof CRealLowerBoundSpec r c
((Z.min (CRealLowerBound r c) (- scale r - 1 + 2 * CRealLowerBound r c)))%Z ltac:(lia) as Hlowbnd.
pose proof Qpower_0_lt 2 (CRealLowerBound r c) as Hpow.
Lemma CReal_inv_l_pos : forall (r:CReal) (Hrpos : 0 < r),
(CReal_inv_pos r Hrpos) * r == 1.
intros r Hrpos; apply CRealEq_diff; intros n.
unfold CReal_mult, CReal_mult_seq, CReal_mult_scale;
unfold CReal_inv_pos, CReal_inv_pos_seq, CReal_inv_pos_scale, CReal_inv_pos_cm;
unfold inject_Q.
do 3 rewrite CReal_red_seq.
do 1 rewrite CReal_red_scale.
(* This is needed several times below *)
remember (Z.min (CRealLowerBound r Hrpos) (n - scale r - 1 + 2 * CRealLowerBound r Hrpos))%Z as k.
assert (0 < seq r k)%Q as Hrseqpos.
pose proof Qpower_0_lt 2 (CRealLowerBound r Hrpos)%Z ltac:(lra) as Hpow.
pose proof CRealLowerBoundSpec r Hrpos k ltac:(lia) as Hlowbnd.
field_simplify_Qabs; [|lra]; unfold Qdiv.
rewrite Qabs_Qmult, Qabs_Qinv.
pose proof cauchy r (n + CRealLowerBound r Hrpos)%Z
(n + CRealLowerBound r Hrpos - 1)%Z k as Hrbnd.
pose proof CRealLowerBound_lt_scale r Hrpos as Hscale_lowbnd.
specialize (Hrbnd ltac:(lia) ltac:(lia)).
simplify_Qabs_in Hrbnd; simplify_Qabs.
rewrite Qplus_comm in Hrbnd.
apply Qlt_le_weak in Hrbnd.
apply (Qle_trans _ _ _ Hrbnd).
pose proof CRealLowerBoundSpec r Hrpos k ltac:(lia) as Hlowbnd.
rewrite Qpower_plus; [|lra].
apply Qmult_le_compat_nonneg.
pose proof Qpower_pos 2 n; split; lra.
rewrite Qabs_pos; [lra|].
pose proof Qpower_0_lt 2 (CRealLowerBound r Hrpos)%Z ltac:(lra) as Hpow.
Lemma CReal_inv_l : forall (r:CReal) (rnz : r # 0),
((/ r) rnz) * r == 1.
rewrite <- CReal_opp_mult_distr_l, CReal_opp_mult_distr_r.
Lemma CReal_inv_r : forall (r:CReal) (rnz : r # 0),
r * ((/ r) rnz) == 1.
rewrite CReal_mult_comm, CReal_inv_l.
Lemma CReal_inv_1 : forall nz : 1 # 0, (/ 1) nz == 1.
rewrite <- (CReal_mult_1_l ((/1) nz)).
Lemma CReal_inv_mult_distr :
forall r1 r2 (r1nz : r1 # 0) (r2nz : r2 # 0) (rmnz : (r1*r2) # 0),
(/ (r1 * r2)) rmnz == (/ r1) r1nz * (/ r2) r2nz.
apply (CReal_mult_eq_reg_l r1).
rewrite <- CReal_mult_assoc.
apply (CReal_mult_eq_reg_l r2).
rewrite <- CReal_mult_assoc.
rewrite (CReal_mult_comm r2 r1).
Lemma Rinv_eq_compat : forall x y (rxnz : x # 0) (rynz : y # 0),
x == y
-> (/ x) rxnz == (/ y) rynz.
apply (CReal_mult_eq_reg_l x).
rewrite CReal_inv_r, H, CReal_inv_r.
Lemma CReal_mult_lt_reg_l : forall r r1 r2, 0 < r -> r * r1 < r * r2 -> r1 < r2.
apply (CReal_mult_lt_compat_l ((/z) (inr H))) in H0.
repeat rewrite <- CReal_mult_assoc in H0.
rewrite CReal_inv_l in H0.
repeat rewrite CReal_mult_1_l in H0.
apply CReal_inv_0_lt_compat.
Lemma CReal_mult_lt_reg_r : forall r r1 r2, 0 < r -> r1 * r < r2 * r -> r1 < r2.
apply CReal_mult_lt_reg_l with r.
now rewrite 2!(CReal_mult_comm r).
Lemma CReal_mult_eq_reg_r : forall r r1 r2, r1 * r == r2 * r -> r # 0 -> r1 == r2.
apply (CReal_mult_eq_reg_l r).
now rewrite 2!(CReal_mult_comm r).
Lemma CReal_mult_eq_compat_l : forall r r1 r2, r1 == r2 -> r * r1 == r * r2.
Lemma CReal_mult_eq_compat_r : forall r r1 r2, r1 == r2 -> r1 * r == r2 * r.
(* In particular x * y == 1 implies that 0 # x, 0 # y and
that x and y are inverses of each other. *)
Lemma CReal_mult_pos_appart_zero : forall x y : CReal, 0 < x * y -> 0 # x.
unfold CRealLt, CReal_mult, CReal_mult_seq, CReal_mult_scale in H0ltxy;
rewrite CReal_red_seq in H0ltxy.
destruct H0ltxy as [n nmaj].
cbn in nmaj; setoid_rewrite Qplus_0_r in nmaj.
destruct (Q_dec 0 (seq y (n - scale x - 1)))%Q as [[H0lty|Hylt0]|Hyeq0].
apply (Qmult_lt_compat_r _ _ (/(seq y (n - scale x - 1)))%Q ) in nmaj.
2: apply Qinv_lt_0_compat, H0lty.
setoid_rewrite <- Qmult_assoc in nmaj at 2.
setoid_rewrite Qmult_inv_r in nmaj.
setoid_rewrite Qmult_1_r in nmaj.
pose proof bound y (n - scale x - 1)%Z as Hybnd.
apply Qabs_Qlt_condition, proj2 in Hybnd.
apply Qinv_lt_contravar in Hybnd.
3: apply Qpower_0_lt; lra.
apply (Qmult_lt_l _ _ (2 * (2 ^ n))) in Hybnd.
2: pose proof Qpower_0_lt 2 n; lra.
apply (Qlt_trans _ _ _ Hybnd) in nmaj; clear Hybnd.
rewrite <- Qpower_opp, <- Qmult_assoc, <- Qpower_plus in nmaj by lra.
apply (CReal_abs_appart_zero x (n - scale y - 1)%Z), Qabs_gt.
rewrite Qpower_minus_pos.
ring_simplify (n + - scale y)%Z in nmaj.
pose proof Qpower_0_lt 2 (n - scale y)%Z; lra.
(* This proof is the same as above, except that we swap the signs of x and y *)
(* ToDo: maybe assert teh goal for arbitrary y>0 and then apply twice *)
assert (forall a b : Q, ((-a)*(-b)==a*b)%Q) by (intros; ring).
setoid_rewrite <- H in nmaj at 2; clear H.
apply (Qmult_lt_compat_r _ _ (/-(seq y (n - scale x - 1)))%Q ) in nmaj.
2: apply Qinv_lt_0_compat; lra.
setoid_rewrite <- Qmult_assoc in nmaj at 2.
setoid_rewrite Qmult_inv_r in nmaj.
setoid_rewrite Qmult_1_r in nmaj.
pose proof bound y (n - scale x - 1)%Z as Hybnd.
apply Qabs_Qlt_condition, proj1 in Hybnd.
apply Qopp_lt_compat in Hybnd; rewrite Qopp_involutive in Hybnd.
apply Qinv_lt_contravar in Hybnd.
3: apply Qpower_0_lt; lra.
apply (Qmult_lt_l _ _ (2 * (2 ^ n))) in Hybnd.
2: pose proof Qpower_0_lt 2 n; lra.
apply (Qlt_trans _ _ _ Hybnd) in nmaj; clear Hybnd.
rewrite <- Qpower_opp, <- Qmult_assoc, <- Qpower_plus in nmaj by lra.
apply (CReal_abs_appart_zero x (n - scale y - 1)%Z).
pose proof Qpower_0_lt 2 (n + - scale y)%Z ltac:(lra) as Hpowpos.
rewrite Qpower_minus_pos.
ring_simplify (n + - scale y)%Z in nmaj.
pose proof Qpower_0_lt 2 (n - scale y)%Z; lra.
pose proof Qpower_0_lt 2 n ltac:(lra).
rewrite <- Hyeq0 in nmaj.
Fixpoint pow (r:CReal) (n:nat) : CReal :=
match n with
| O => 1
| S n => r * (pow r n)
end.
Lemma CReal_mult_le_compat_l_half : forall r r1 r2,
0 < r -> r1 <= r2 -> r * r1 <= r * r2.
apply (CReal_mult_lt_reg_l) in abs.
Lemma CReal_invQ : forall (b : positive) (pos : Qlt 0 (Z.pos b # 1)),
CReal_inv (inject_Q (Z.pos b # 1)) (inr (CReal_injectQPos (Z.pos b # 1) pos))
== inject_Q (1 # b).
apply (CReal_mult_eq_reg_l (inject_Q (Z.pos b # 1))).
rewrite CReal_mult_comm, CReal_inv_l.
do 2 rewrite Pos.mul_1_r.
pose proof Qpower_pos 2 n ltac:(lra).
rewrite Z.abs_0, Qreduce_zero.
Definition CRealQ_dense (a b : CReal)
: a < b -> { q : Q & a < inject_Q q < b }.
(* Locate a and b at the index given by a<b,
and pick the middle rational number. *)
exists ((seq a p + seq b p) * (1#2))%Q.
apply (CReal_le_lt_trans _ _ _ (inject_Q_compare a p)).
apply (CReal_plus_lt_reg_l (-b)).
rewrite CReal_plus_opp_l.
apply (CReal_plus_lt_reg_r
(-inject_Q ((seq a p + seq b p) * (1 # 2)))).
rewrite CReal_plus_assoc, CReal_plus_opp_r, CReal_plus_0_r, CReal_plus_0_l.
apply (CReal_le_lt_trans _ _ _ (inject_Q_compare (-b) p)).
destruct b as [bseq]; simpl in pmaj |- *.
unfold CReal_opp_seq; rewrite CReal_red_seq.
Lemma inject_Q_mult : forall q r : Q,
inject_Q (q * r) == inject_Q q * inject_Q r.
intros [n maj]; cbn in maj.
unfold CReal_mult_seq in maj; cbn in maj.
pose proof Qpower_0_lt 2 n; lra.
intros [n maj]; cbn in maj.
unfold CReal_mult_seq in maj; cbn in maj.
pose proof Qpower_0_lt 2 n; lra.
Definition Rup_nat (x : CReal)
: { n : nat & x < inject_Q (Z.of_nat n #1) }.
destruct (CRealArchimedean x) as [p maj].
apply (CReal_lt_trans _ (inject_Q (Z.neg p # 1))).
Lemma CReal_mult_le_0_compat : forall (a b : CReal),
0 <= a -> 0 <= b -> 0 <= a * b.
(* Limit of (a + 1/n)*b when n -> infty. *)
assert (0 < -(a*b)) as epsPos.
apply CReal_opp_gt_lt_contravar.
destruct (Rup_nat (b * (/ (-(a*b))) (inr epsPos)))
as [n maj].
apply (CReal_mult_lt_compat_r (-(a*b))) in maj.
rewrite CReal_mult_0_l, CReal_mult_assoc, CReal_inv_l, CReal_mult_1_r in maj.
assert (0 < inject_Q (Z.of_nat (S n) #1)) as nPos.
apply -> Nat.succ_le_mono; apply Nat.le_0_l.
assert (b * (/ inject_Q (Z.of_nat (S n) #1)) (inr nPos) < -(a*b)).
apply (CReal_mult_lt_reg_r (inject_Q (Z.of_nat (S n) #1))).
rewrite CReal_mult_assoc, CReal_inv_l, CReal_mult_1_r.
apply (CReal_mult_lt_compat_r (-(a*b))) in maj.
rewrite CReal_mult_assoc, CReal_inv_l, CReal_mult_1_r in maj.
pose proof (CReal_mult_le_compat_l_half
(a + (/ inject_Q (Z.of_nat (S n) #1)) (inr nPos)) 0 b).
assert (0 + 0 < a + (/ inject_Q (Z.of_nat (S n) #1)) (inr nPos)).
apply CReal_plus_le_lt_compat.
apply CReal_inv_0_lt_compat.
rewrite CReal_plus_0_l in H3.
rewrite CReal_mult_0_r in H2.
rewrite CReal_mult_plus_distr_r.
apply (CReal_plus_lt_compat_l (a*b)) in H1.
rewrite CReal_plus_opp_r in H1.
rewrite (CReal_mult_comm ((/ inject_Q (Z.of_nat (S n) #1)) (inr nPos))).
Lemma CReal_mult_le_compat_l : forall (r r1 r2:CReal),
0 <= r -> r1 <= r2 -> r * r1 <= r * r2.
apply (CReal_plus_le_reg_r (-(r*r1))).
rewrite CReal_plus_opp_r, CReal_opp_mult_distr_r.
rewrite <- CReal_mult_plus_distr_l.
apply CReal_mult_le_0_compat.
apply (CReal_plus_le_reg_r r1).
rewrite CReal_plus_0_l, CReal_plus_assoc, CReal_plus_opp_l, CReal_plus_0_r.
Lemma CReal_mult_le_compat_r : forall (r r1 r2:CReal),
0 <= r -> r1 <= r2 -> r1 * r <= r2 * r.
apply (CReal_plus_le_reg_r (-(r1*r))).
rewrite CReal_plus_opp_r, CReal_opp_mult_distr_l.
rewrite <- CReal_mult_plus_distr_r.
apply CReal_mult_le_0_compat.
apply (CReal_plus_le_reg_r r1).
Lemma CReal_mult_le_reg_l :
forall x y z : CReal,
0 < x -> x * y <= x * z -> y <= z.
apply (CReal_mult_lt_compat_l x) in abs.
Lemma CReal_mult_le_reg_r :
forall x y z : CReal,
0 < x -> y * x <= z * x -> y <= z.
apply (CReal_mult_lt_compat_r x) in abs.