From 815f7c14299ef85936f005acc24de562146fe314 Mon Sep 17 00:00:00 2001 From: hy7pc8gfmf-dotcom <168888@live.cn> Date: Thu, 15 Oct 2026 02:49:07 +0800 Subject: [PATCH] Add escape-window separation for the fast constructive reals Add reals/fast/CrnEscapeSep.v: an abstract irrationality criterion for the fast constructive reals CR. From a family of positive window widths that eventually escape the dyadic approximations of x, it derives that x is apart from every embedded rational, with an extractable side certificate (CRapartT). Compared with the standard-library CReal engine, no Archimedean index pushdown is needed: the positivity witness of CRpos_char is a single positive rational, so the witness is the quarter of the escape margin and the coherence of the approximation function transports the escape inequality across precisions. The file is picked up automatically by SCons and by configure/make (reals is already listed). No new external dependencies. --- reals/fast/CrnEscapeSep.v | 287 ++++++++++++++++++++++++++++++++++++++ 1 file changed, 287 insertions(+) create mode 100644 reals/fast/CrnEscapeSep.v 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.