diff --git a/reals/fast/CrnEscapeSep.v b/reals/fast/CrnEscapeSep.v new file mode 100644 index 00000000..549d1aa2 --- /dev/null +++ b/reals/fast/CrnEscapeSep.v @@ -0,0 +1,287 @@ +(************************************************************************) +(* * The Rocq Prover / The Rocq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* Q] be a family of positive window + widths with the escape property [crn_escape_window x e]: every + rational [q] eventually escapes the window of width [e n] centered + at the [2^(-n)] approximation of [x], while the width dominates + twice the dyadic resolution at the same index. Then [x] is apart + from every embedded rational ['q] in the sense of [CRapartT]: the + disjoint-sum certificate that exhibits on which side of [q] the + number [x] lies. + + The main statement is [crn_escape_window_apart]. Compared with the + corresponding construction for the standard-library [CReal], the + engine is shorter: the positivity witness of [CRpos_char] is a + single positive rational value, so no Archimedean index pushdown is + needed; the witness is the quarter of the escape margin + [M = e n - 2 * 2^(-n)] at the escape index [n], and the coherence + of the approximation function transports the escape inequality from + the [2^(-n)] approximation to the [M/8] approximation. + + Dependencies. CoRN [metric2]/[model]/[reals.fast] hierarchy + ([CRmetric], [Qmetric], [QposMinMax], [CRFieldOps], [CRArith]); + stdlib [QArith], [Qabs], [Qpower]. + + Constructivity. Statements are carried by [Set] and by the sum + type [CRapartT]; the only [Prop] occurrences are [Qlt] predicates + inside the sigma type and inside [CRlt]. No axiom and no classical + logic is used; the main proof is a fully explicit chain of + rational-order lemmas, decidability of [Q] being used only to + branch on the sign. + + WARNING: this file is experimental and likely to change in future + releases. *) + +Require Import CoRN.metric2.Metric. +Require Import CoRN.metric2.UniformContinuity. +Require Import CoRN.model.metric2.Qmetric. +Require Import CoRN.model.totalorder.QposMinMax. +Require Import CoRN.model.metric2.CRmetric. +Require Import CoRN.reals.fast.CRFieldOps. +Require Import CoRN.reals.fast.CRArith. +From Coq Require Import QArith Qabs Qpower. + +Set Implicit Arguments. + +Local Open Scope Q_scope. +Local Open Scope CR_scope. + +(* -- Positive-rational packings -- *) + +Lemma crn_two_pos : (0 < 2)%Q. +Proof. unfold Qlt. cbn. reflexivity. Qed. + +Lemma crn_pow2_pos : forall z : Z, (0 < 2 ^ z)%Q. +Proof. intros z. apply Qpower_0_lt. exact crn_two_pos. Qed. + +(** The dyadic resolution [2^(-n)] of index [n], packed as a positive + rational. The projection [proj1_sig] of this packing reduces to + the plain rational [2^(-n)], so the [Q]-side chain runs on the + unpacked values. *) +Definition crn_dyadic (n : nat) : Qpos := + exist (Qlt 0) (2 ^ Z.opp (Z.of_nat n))%Q (crn_pow2_pos (Z.opp (Z.of_nat n))). + +(** A positive rational seen as such. This packing keeps the type of + the witness the constant [Qpos], which the [Qpos]-to-[QposInf] + coercion requires. *) +Definition crn_qpos (q : Q) (H : (0 < q)%Q) : Qpos := exist (Qlt 0) q H. + +(* -- Definitional reductions of the approximations -- *) + +(** The coherence of the approximation function: any two approximations + of [x] differ by at most the sum of their precisions (the [Q]-side + form of the record field of [x]). *) +Lemma crn_reg_le : forall (x : CR) (e1 e2 : Qpos), + (-(proj1_sig e1 + proj1_sig e2) + <= approximate x e1 - approximate x e2 + <= proj1_sig e1 + proj1_sig e2)%Q. +Proof. intros [xapprox xreg] e1 e2. exact (xreg e1 e2). Qed. + +(** Adding two nonnegative rationals stays nonnegative. *) +Lemma crn_add_ge0 : forall a b : Q, + (0 <= a)%Q -> (0 <= b)%Q -> (0 <= a + b)%Q. +Proof. + intros a b Ha Hb. + rewrite <- (Qplus_0_r 0%Q). + apply (Qplus_le_compat 0%Q a%Q 0%Q b%Q Ha Hb). +Qed. + +(** Adding a nonnegative rational increases, or preserves, a bound. *) +Lemma crn_le_add_r : forall x w : Q, (0 <= w)%Q -> (x <= x + w)%Q. +Proof. + intros x w Hw. + apply (Qle_trans x%Q (x + 0)%Q (x + w)%Q). + - rewrite Qplus_0_r. apply Qle_refl. + - apply (Qplus_le_compat x%Q x%Q 0%Q w%Q (Qle_refl x%Q) Hw). +Qed. + +(* -- The escape-window structure and the separation engine -- *) + +Definition crn_escape_window (x : CR) (e : nat -> Q) : Set := + forall q : Q, + { n : nat | + (Qlt (2 * proj1_sig (crn_dyadic n)) (e n) + /\ Qlt (e n) (Qabs (q - approximate x (crn_dyadic n))))%Q }. + +Theorem crn_escape_window_apart : + forall (x : CR) (e : nat -> Q), + crn_escape_window x e -> + forall q : Q, CRapartT x ('q)%CR. +Proof. + intros x e Hw q. + destruct (Hw q) as [n0 [Hres Hesc]]. + set (E := e n0) in *. + assert (Hd0val : proj1_sig (crn_dyadic n0) = (2 ^ Z.opp (Z.of_nat n0))%Q) + by reflexivity. + set (d0 := (2 ^ Z.opp (Z.of_nat n0))%Q) in *. + rewrite Hd0val in Hres. + assert (Hd0le : (0 <= d0)%Q) by (apply (Qlt_le_weak 0 d0); apply crn_pow2_pos). + (* The margin [M = E - 2 * d0] is positive. *) + assert (HM : (0 < E + -2*d0)%Q). + { pose proof (Qplus_lt_le_compat (2*d0) E (-2*d0) (-2*d0) + Hres (Qle_refl (-2*d0))) as HH. + assert (Heq0 : (2*d0 + -2*d0 == 0)%Q) by ring. + rewrite Heq0 in HH. exact HH. } + set (M := (E + -2*d0)%Q) in *. + assert (Hd2 : (d0 <= 2*d0)%Q). + { assert (Heq : (2*d0 == d0 + d0)%Q) by ring. rewrite Heq. + apply (Qle_trans _ (d0 + 0)%Q). + - rewrite Qplus_0_r. apply Qle_refl. + - apply (Qplus_le_compat d0 d0 0 d0 (Qle_refl d0) Hd0le). } + assert (H14 : (0 < (1#4))%Q) by (unfold Qlt; cbn; reflexivity). + assert (HpM : (0 < M * (1#4))%Q). + { pose proof (Qmult_lt_compat_r 0 M (1#4) H14 HM) as HH. + rewrite Qmult_0_l in HH. exact HH. } + assert (H38le : (0 <= M * (3#8))%Q) + by (apply Qmult_le_0_compat; + [apply (Qlt_le_weak 0 M HM) + | apply (Qlt_le_weak 0 (3#8)); unfold Qlt; cbn; reflexivity]). + assert (Hval2 : proj1_sig (crn_qpos HpM) = (M * (1#4))%Q) + by reflexivity. + destruct (Qlt_le_dec 0 (q - approximate x (crn_dyadic n0))) as [Hs | Hs]. + - (* [q] lies above the approximation: [x < 'q]. *) + left. + unfold CRltT. + apply (CRpos_char (crn_qpos HpM)). + assert (HabsS : + (Qabs (q - approximate x (crn_dyadic n0)) + == q - approximate x (crn_dyadic n0))%Q). + { apply Qabs_pos. apply Qlt_le_weak. exact Hs. } + rewrite HabsS in Hesc. + assert (Hgate : + ((2#1) * (M * (1#4)) + <= q - approximate x (((1#2) * crn_qpos HpM)%Qpos))%Q). + { remember (approximate x ((1#2) * crn_qpos HpM)%Qpos) + as b0 eqn:Eb0. + pose proof (crn_reg_le x (crn_dyadic n0) + ((1#2) * crn_qpos HpM)%Qpos) as Hreg. + destruct Hreg as [Hlow Hupper]. + cbn [proj1_sig Qpos_mult] in Hupper. + rewrite Hd0val, Hval2 in Hupper. + rewrite <- Eb0 in Hupper. + (* Hupper : approximate x (crn_dyadic n0) - b0 <= d0 + (1#2)*(M*(1#4)) *) + assert (Hlow2 : + (-(d0 + (1#2)*(M*(1#4))) <= approximate x (crn_dyadic n0) - b0)%Q). + { cbn [proj1_sig Qpos_mult] in Hlow. + rewrite Hd0val, Hval2 in Hlow. + rewrite <- Eb0 in Hlow. + exact Hlow. } + assert (Hshift : + ((q - approximate x (crn_dyadic n0)) + + -(d0 + (1#2)*(M*(1#4))) <= q - b0)%Q). + { assert (Heq2 : (q - b0 + == (q - approximate x (crn_dyadic n0)) + + (approximate x (crn_dyadic n0) - b0))%Q) by ring. + rewrite Heq2. + apply (Qplus_le_compat (q - approximate x (crn_dyadic n0)) + (q - approximate x (crn_dyadic n0)) + (-(d0 + (1#2)*(M*(1#4)))) + (approximate x (crn_dyadic n0) - b0) + (Qle_refl _) Hlow2). } + assert (Hesc2 : (E + -(d0 + (1#2)*(M*(1#4))) < q - b0)%Q). + { pose proof (Qplus_lt_le_compat E (q - approximate x (crn_dyadic n0)) + (-(d0 + (1#2)*(M*(1#4)))) (-(d0 + (1#2)*(M*(1#4)))) + Hesc (Qle_refl _)) as HH. + apply (Qlt_le_trans (E + -(d0 + (1#2)*(M*(1#4))))%Q + ((q - approximate x (crn_dyadic n0)) + + -(d0 + (1#2)*(M*(1#4))))%Q + (q - b0)%Q HH Hshift). } + assert (HzeroW : (0 <= M * (3#8) + d0)%Q). + { exact (crn_add_ge0 H38le Hd0le). } + apply (Qle_trans ((2#1) * (M * (1#4)))%Q + (M * (7#8) + d0)%Q + (q - b0)%Q). + - assert (HeqL : ((2#1) * (M * (1#4)) == M * (1#2))%Q) by ring. + rewrite HeqL. + assert (HeqR : (M * (7#8) + d0 + == M * (1#2) + (M * (3#8) + d0))%Q) by ring. + rewrite HeqR. + apply (crn_le_add_r (M * (1#2))%Q HzeroW). + - assert (HEM : (M == E + -2*d0)%Q) by reflexivity. + assert (HEM2 : (E == M + 2*d0)%Q) by (rewrite HEM; ring). + rewrite HEM2 in Hesc2. + assert (HeqR2 : (((M + 2*d0) + -(d0 + (1#2)*(M*(1#4)))) + == M * (7#8) + d0)%Q) by ring. + rewrite HeqR2 in Hesc2. + apply (Qlt_le_weak _ _ Hesc2). } + exact Hgate. + - (* [q] lies below the approximation: ['q < x]. *) + right. + unfold CRltT. + apply (CRpos_char (crn_qpos HpM)). + assert (HabsS : + (Qabs (q - approximate x (crn_dyadic n0)) + == -(q - approximate x (crn_dyadic n0)))%Q). + { apply Qabs_neg. exact Hs. } + rewrite HabsS in Hesc. + assert (HeqH : (-(q - approximate x (crn_dyadic n0)) + == approximate x (crn_dyadic n0) - q)%Q) by ring. + rewrite HeqH in Hesc. + assert (Hgate : + ((2#1) * (M * (1#4)) + <= approximate x (((1#2) * crn_qpos HpM)%Qpos) - q)%Q). + { remember (approximate x ((1#2) * crn_qpos HpM)%Qpos) + as b0 eqn:Eb0. + pose proof (crn_reg_le x (crn_dyadic n0) + ((1#2) * crn_qpos HpM)%Qpos) as Hreg. + destruct Hreg as [Hlow Hupper]. + cbn [proj1_sig Qpos_mult] in Hupper. + rewrite Hd0val, Hval2 in Hupper. + rewrite <- Eb0 in Hupper. + assert (Hshift : + ((approximate x (crn_dyadic n0) - q) + + -(d0 + (1#2)*(M*(1#4))) <= b0 - q)%Q). + { pose proof (Qopp_le_compat (approximate x (crn_dyadic n0) - b0) + (d0 + (1#2)*(M*(1#4))) Hupper) as H1. + assert (Heq1 : (-(approximate x (crn_dyadic n0) - b0) + == b0 - approximate x (crn_dyadic n0))%Q) by ring. + rewrite Heq1 in H1. + assert (Heq2 : (b0 - q + == (approximate x (crn_dyadic n0) - q) + + (b0 - approximate x (crn_dyadic n0)))%Q) by ring. + rewrite Heq2. + apply (Qplus_le_compat (approximate x (crn_dyadic n0) - q) + (approximate x (crn_dyadic n0) - q) + (-(d0 + (1#2)*(M*(1#4)))) + (b0 - approximate x (crn_dyadic n0)) + (Qle_refl _) H1). } + assert (Hesc2 : (E + -(d0 + (1#2)*(M*(1#4))) < b0 - q)%Q). + { pose proof (Qplus_lt_le_compat E (approximate x (crn_dyadic n0) - q) + (-(d0 + (1#2)*(M*(1#4)))) (-(d0 + (1#2)*(M*(1#4)))) + Hesc (Qle_refl _)) as HH. + apply (Qlt_le_trans (E + -(d0 + (1#2)*(M*(1#4))))%Q + ((approximate x (crn_dyadic n0) - q) + + -(d0 + (1#2)*(M*(1#4))))%Q + (b0 - q)%Q HH Hshift). } + assert (HzeroW : (0 <= M * (3#8) + d0)%Q). + { exact (crn_add_ge0 H38le Hd0le). } + apply (Qle_trans ((2#1) * (M * (1#4)))%Q + (M * (7#8) + d0)%Q + (b0 - q)%Q). + - assert (HeqL : ((2#1) * (M * (1#4)) == M * (1#2))%Q) by ring. + rewrite HeqL. + assert (HeqR : (M * (7#8) + d0 + == M * (1#2) + (M * (3#8) + d0))%Q) by ring. + rewrite HeqR. + apply (crn_le_add_r (M * (1#2))%Q HzeroW). + - assert (HEM : (M == E + -2*d0)%Q) by reflexivity. + assert (HEM2 : (E == M + 2*d0)%Q) by (rewrite HEM; ring). + rewrite HEM2 in Hesc2. + assert (HeqR2 : (((M + 2*d0) + -(d0 + (1#2)*(M*(1#4)))) + == M * (7#8) + d0)%Q) by ring. + rewrite HeqR2 in Hesc2. + apply (Qlt_le_weak _ _ Hesc2). } + exact Hgate. +Qed.