Reflection — Proof by Reflection for Interval Arithmetic

Defines a reified expression type RExpr with:

• RExpr.denote : RExpr → ℝ — the real-valued denotation
• RExpr.eval : RExpr → QInterval — computable interval evaluation
• RExpr.eval_sound — soundness (under evalValid precondition)

The rsa_decide tactic reifies ℝ expressions into RExpr values, then:

1. native_decide checks evalValid (always true for RSA expressions)
2. native_decide evaluates (rhs.eval).hi < (lhs.eval).lo in compiled code
3. The kernel verifies only eval_sound applications + native_decide

This eliminates the 5M+ Nat.cast kernel reductions from the old Expr-based approach.

inductive Interval.RExpr : Type

Reified arithmetic expression over ℝ.

Each constructor corresponds to an operation the rsa_decide tactic can reify. The denote function maps back to ℝ; the eval function computes a QInterval bounding the value.

• nat : ℕ → RExpr
• ratCast : ℚ → RExpr

  ℚ→ℝ cast leaf. denote produces ↑q : ℝ via Rat.cast, matching goal expressions that originated from ℚ→ℝ coercions (e.g., ↑(prior h)). Using nat for these would produce Nat.cast n which is not definitionally equal to Rat.cast (n : ℚ) in the kernel.

• add : RExpr → RExpr → RExpr
• mul : RExpr → RExpr → RExpr
• div : RExpr → RExpr → RExpr
• neg : RExpr → RExpr
• sub : RExpr → RExpr → RExpr
• rexp : RExpr → RExpr
• rlog : RExpr → RExpr
• rpow : RExpr → ℕ → RExpr
• inv : RExpr → RExpr
• iteZero : RExpr → RExpr → RExpr → RExpr

  iteZero cond thenBr elseBr = if cond.denote = 0 then thenBr else elseBr

• expMulLogSub : RExpr → RExpr → RExpr → RExpr

  expMulLogSub α x c = exp(α * (log(x) - c)). eval uses algebraic identity x^α * exp(-α*c) when α is a concrete natural, avoiding Padé log+exp calls that produce enormous rationals.

• rsqrt : RExpr → RExpr

  rsqrt x = √x (Real.sqrt). denote uses Real.sqrt, eval uses sqrtInterval (= exp(log/2)) for positive intervals, exact 0 for [0,0].

@[implicit_reducible]

instance Interval.instReprRExpr : Repr RExpr

Equations

• Interval.instReprRExpr = { reprPrec := Interval.instReprRExpr.repr }

def Interval.instReprRExpr.repr : RExpr → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Interval.instInhabitedRExpr : Inhabited RExpr

Equations

• Interval.instInhabitedRExpr = { default := Interval.instInhabitedRExpr.default }

def Interval.instInhabitedRExpr.default : RExpr

Equations

• Interval.instInhabitedRExpr.default = Interval.RExpr.nat default

@[implicit_reducible]

instance Interval.instDecidableEqRExpr : DecidableEq RExpr

Equations

• Interval.instDecidableEqRExpr = Interval.instDecidableEqRExpr.decEq

def Interval.instDecidableEqRExpr.decEq (x✝ x✝¹ : RExpr) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Interval.RExpr.denote : RExpr → ℝ

Map a reified expression to its real value. Noncomputable (uses Real.exp, etc.).

Equations

• (Interval.RExpr.nat 0).denote = 0
• (Interval.RExpr.nat 1).denote = 1
• (Interval.RExpr.nat n).denote = ↑n
• (Interval.RExpr.ratCast q).denote = ↑q
• (a.add b).denote = a.denote + b.denote
• (a.mul b).denote = a.denote * b.denote
• (a.div b).denote = a.denote / b.denote
• a.neg.denote = -a.denote
• (a.sub b).denote = a.denote - b.denote
• a.rexp.denote = Real.exp a.denote
• a.rlog.denote = Real.log a.denote
• (a.rpow 0).denote = a.denote.rpow 0
• (a.rpow 1).denote = a.denote.rpow 1
• (a.rpow n).denote = a.denote.rpow ↑n
• a.inv.denote = a.denote⁻¹
• (c.iteZero t e).denote = if c.denote = 0 then t.denote else e.denote
• (α.expMulLogSub x_1 cost).denote = Real.exp (α.denote * (Real.log x_1.denote - cost.denote))
• a.rsqrt.denote = √a.denote

def Interval.RExpr.eval : RExpr → QInterval

Evaluate a reified expression to a bounding QInterval. Fully computable. Every compound operation is coarsened to bounded-precision rationals.

Equations

• One or more equations did not get rendered due to their size.
• (Interval.RExpr.nat a).eval = Interval.QInterval.exact ↑a
• (Interval.RExpr.ratCast a).eval = Interval.QInterval.exact a
• (a.add a_1).eval = Interval.c✝ (a.eval.add a_1.eval)
• a.neg.eval = a.eval.neg
• (a.sub a_1).eval = Interval.c✝ (a.eval.sub a_1.eval)
• a.rexp.eval = Interval.c✝ (Interval.expInterval a.eval)
• a.inv.eval = if h : 0 < a.eval.lo then Interval.c✝ (a.eval.invPos h) else { lo := -1, hi := 1, valid := Interval.RExpr.eval._proof_1 }

def Interval.RExpr.evalValid : RExpr → Bool

Whether eval avoids unsound fallback branches.

The fallback intervals in eval (e.g., ⟨-1, 1⟩ for division with non-positive denominator) are hard-coded constants that do not soundly bound the result for arbitrary inputs. evalValid returns true exactly when no such fallback is reached — i.e., every division has a positive denominator, every log/inv has a positive argument, and every rpow has a nonneg base (or zero exponent).

In practice, rsa_decide only builds RExpr values from RSA computations (positive probabilities, positive denominators), so evalValid is always true. The tactic verifies this via native_decide as a precondition.

Equations

• (Interval.RExpr.nat a).evalValid = true
• (Interval.RExpr.ratCast a).evalValid = true
• (a.add a_1).evalValid = (a.evalValid && a_1.evalValid)
• (a.mul a_1).evalValid = (a.evalValid && a_1.evalValid)
• (a.div a_1).evalValid = (a.evalValid && a_1.evalValid && (a.eval.lo == 0 && a.eval.hi == 0 || decide (0 ≤ a.eval.lo) && decide (0 < a_1.eval.lo)))
• a.neg.evalValid = a.evalValid
• (a.sub a_1).evalValid = (a.evalValid && a_1.evalValid)
• a.rexp.evalValid = a.evalValid
• a.rlog.evalValid = (a.evalValid && (decide (0 < a.eval.lo) || a.eval.lo == 0 && a.eval.hi == 0))
• (a.rpow a_1).evalValid = (a.evalValid && (a_1 == 0 || decide (0 ≤ a.eval.lo)))
• a.inv.evalValid = (a.evalValid && decide (0 < a.eval.lo))
• (a.iteZero a_1 a_2).evalValid = (a.evalValid && have rc := a.eval; if rc.lo = 0 ∧ rc.hi = 0 then a_1.evalValid else if 0 < rc.lo then a_2.evalValid else a_1.evalValid && a_2.evalValid)
• (a.expMulLogSub a_1 a_2).evalValid = (a.evalValid && a_1.evalValid && a_2.evalValid && decide (0 < a_1.eval.lo))
• a.rsqrt.evalValid = (a.evalValid && (decide (0 < a.eval.lo) || a.eval.lo == 0 && a.eval.hi == 0))

def Interval.RExpr.tryExtractLogProduct : RExpr → Option (List (RExpr × ℚ))

Extract (xᵢ, bᵢ) pairs from a sum-of-weighted-logs RExpr. Returns none if the expression doesn't match the pattern Σ bᵢ · log(xᵢ). Coefficients bᵢ are rational (not just integer), enabling exact evaluation when log arguments coincide and coefficients sum to an integer (e.g., 1/3 · log(x) + 1/3 · log(x) + 1/3 · log(x) → x^1 exactly).

Equations

• One or more equations did not get rendered due to their size.
• x_1.rlog.tryExtractLogProduct = some [(x_1, 1)]
• (a.add b).tryExtractLogProduct = do let la ← a.tryExtractLogProduct let lb ← b.tryExtractLogProduct some (la ++ lb)
• x✝.tryExtractLogProduct = if (x✝.eval.lo == 0 && x✝.eval.hi == 0) = true then some [] else none

def Interval.RExpr.evalBoth : RExpr → QInterval × Bool

Merged eval + evalValid in a single traversal. Returns (interval, valid). This eliminates the redundant eval calls that evalValid makes on subexpressions — each node computes its interval exactly once. Uses a flat pair instead of Option to avoid heap allocation overhead in compiled code.

Equations

• One or more equations did not get rendered due to their size.
• (Interval.RExpr.nat a).evalBoth = (Interval.QInterval.exact ↑a, true)
• (Interval.RExpr.ratCast a).evalBoth = (Interval.QInterval.exact a, true)
• (a.add a_1).evalBoth = match a.evalBoth with | (ra, va) => match a_1.evalBoth with | (rb, vb) => (Interval.c✝ (ra.add rb), va && vb)
• a.neg.evalBoth = match a.evalBoth with | (ra, va) => (ra.neg, va)
• (a.sub a_1).evalBoth = match a.evalBoth with | (ra, va) => match a_1.evalBoth with | (rb, vb) => (Interval.c✝ (ra.sub rb), va && vb)
• a.rexp.evalBoth = match a.evalBoth with | (ra, va) => (Interval.c✝ (Interval.expInterval ra), va)
• a.inv.evalBoth = match a.evalBoth with | (ra, va) => if h : 0 < ra.lo then (Interval.c✝ (ra.invPos h), va) else ({ lo := -1, hi := 1, valid := Interval.RExpr.eval._proof_1 }, false)

theorem Interval.RExpr.evalBoth_sound (e : RExpr) : e.evalBoth.2 = true → e.evalBoth.1.containsReal e.denote

Soundness of the merged eval+validity check. If evalBoth returns (I, true), then I contains the real denotation. This mirrors eval_sound but avoids the redundant subexpression evaluation that plagues the separate evalValid + eval approach.

theorem Interval.RExpr.eval_sound (e : RExpr) : e.evalValid = true → e.eval.containsReal e.denote

Soundness of interval evaluation by reflection.

Every well-formed RExpr (one where evalValid = true) evaluates to a QInterval that contains the real denotation. The evalValid precondition excludes expressions with degenerate operations (division by non-positive, log of non-positive, etc.) whose fallback intervals are unsound.

theorem Interval.RExpr.gt_of_eval_separated (lhs rhs : RExpr) (hlv : lhs.evalValid = true) (hrv : rhs.evalValid = true) (h : rhs.eval.hi < lhs.eval.lo) : lhs.denote > rhs.denote

If interval evaluation proves separation, the denotations are ordered. Requires evalValid for both sides to ensure the intervals are sound.

@[implicit_reducible]

instance Interval.instDecidableLtRatHiEvalLo (lhs rhs : RExpr) : Decidable (rhs.eval.hi < lhs.eval.lo)

Decidable separation check (for native_decide).

Equations

• Interval.instDecidableLtRatHiEvalLo lhs rhs = inferInstance

theorem Interval.RExpr.not_gt_of_eval_bounded (lhs rhs : RExpr) (hlv : lhs.evalValid = true) (hrv : rhs.evalValid = true) (h : lhs.eval.hi ≤ rhs.eval.lo) : ¬lhs.denote > rhs.denote

Non-separation for ¬(>) goals.

@[implicit_reducible]

instance Interval.instDecidableLeRatHiEvalLo (lhs rhs : RExpr) : Decidable (lhs.eval.hi ≤ rhs.eval.lo)

Equations

• Interval.instDecidableLeRatHiEvalLo lhs rhs = inferInstance

def Interval.RExpr.evalRexpOpt : RExpr → QInterval × Bool

Optimized evaluation for rexp nodes: recursively decomposes the inner expression using exp identities:

• exp(a + b) = exp(a) · exp(b) — splits sums
• exp(n · log(x)) = x^n when n ∈ ℕ, x > 0 — exact power
• exp(n · body) = exp(body)^n when n ∈ ℕ — factors out nat multiplier
• exp(other) via Padé — fallback

def Interval.RExpr.evalBothOpt : RExpr → QInterval × Bool

Like evalBoth but intercepts .rexp nodes to use the exp-log product rewrite via evalRexpOpt. All other cases are identical to evalBoth. evalRexpOpt itself calls evalBoth (not evalBothOpt) for leaf sub-expressions, avoiding mutual recursion — this is correct because .rexp nodes don't nest inside each other in RSA expression trees.

Equations

• One or more equations did not get rendered due to their size.
• (Interval.RExpr.nat a).evalBothOpt = (Interval.QInterval.exact ↑a, true)
• (Interval.RExpr.ratCast a).evalBothOpt = (Interval.QInterval.exact a, true)
• (a.add a_1).evalBothOpt = match a.evalBothOpt with | (ra, va) => match a_1.evalBothOpt with | (rb, vb) => (Interval.c✝ (ra.add rb), va && vb)
• a.neg.evalBothOpt = match a.evalBothOpt with | (ra, va) => (ra.neg, va)
• (a.sub a_1).evalBothOpt = match a.evalBothOpt with | (ra, va) => match a_1.evalBothOpt with | (rb, vb) => (Interval.c✝ (ra.sub rb), va && vb)
• a.rexp.evalBothOpt = a.evalRexpOpt
• a.inv.evalBothOpt = match a.evalBothOpt with | (ra, va) => if h : 0 < ra.lo then (Interval.c✝ (ra.invPos h), va) else ({ lo := -1, hi := 1, valid := Interval.RExpr.eval._proof_1 }, false)

theorem Interval.RExpr.evalBothOpt_sound (e : RExpr) : e.evalBothOpt.2 = true → e.evalBothOpt.1.containsReal e.denote

Soundness of evalBothOpt. Mirrors evalBoth_sound — all cases except .rexp are structurally identical; .rexp delegates to evalRexpOpt which needs separate soundness reasoning.

def Interval.RExpr.checkGt (lhs rhs : RExpr) : Bool

Combined check: eval + validity + separation in a single pass via evalBoth. Each subexpression is evaluated exactly once.

Equations

• lhs.checkGt rhs = match lhs.evalBoth with | (li, lv) => match rhs.evalBoth with | (ri, rv) => lv && rv && decide (ri.hi < li.lo)

theorem Interval.RExpr.gt_of_checkGt (lhs rhs : RExpr) (h : lhs.checkGt rhs = true) : lhs.denote > rhs.denote

If checkGt succeeds, the denotations are ordered.

def Interval.RExpr.checkNotGt (lhs rhs : RExpr) : Bool

Combined check for ¬(>): eval + validity + upper bound in a single pass.

Equations

• lhs.checkNotGt rhs = match lhs.evalBoth with | (li, lv) => match rhs.evalBoth with | (ri, rv) => lv && rv && decide (li.hi ≤ ri.lo)

theorem Interval.RExpr.not_gt_of_checkNotGt (lhs rhs : RExpr) (h : lhs.checkNotGt rhs = true) : ¬lhs.denote > rhs.denote

If checkNotGt succeeds, ¬(lhs > rhs).

def Interval.RExpr.isZero (e : RExpr) : Bool

Check if an RExpr is provably zero via interval arithmetic.

Equations

• e.isZero = match e.evalBothOpt with | (iv, valid) => valid && iv.lo == 0 && iv.hi == 0

def Interval.RExpr.isPos (e : RExpr) : Bool

Check if an RExpr is provably positive via interval arithmetic.

Equations

• e.isPos = match e.evalBothOpt with | (iv, valid) => valid && decide (0 < iv.lo)

theorem Interval.RExpr.denote_eq_zero (e : RExpr) (h : e.isZero = true) : e.denote = 0

If isZero succeeds, the denotation is 0.

theorem Interval.RExpr.denote_ne_zero (e : RExpr) (h : e.isPos = true) : e.denote ≠ 0

If isPos succeeds, the denotation is nonzero.

def Interval.RExpr.normalize : RExpr → RExpr

Normalize an RExpr by:

1. Resolving iteZero with constant conditions (dead-branch elimination)
2. Eliminating mul with provably-zero operands
3. Rewriting rexp(mul(α, sub(rlog(x), c))) → expMulLogSub(α, x, c) All transformations preserve denotation. Dead-branch elimination is critical for proving ¬(>) on symmetric models, where two expressions become structurally identical after resolving iteZero branches.

Equations

• (α.mul (x_1.rlog.sub cost)).rexp.normalize = α.normalize.expMulLogSub x_1.normalize cost.normalize
• (Interval.RExpr.nat n).normalize = Interval.RExpr.nat n
• (Interval.RExpr.ratCast q).normalize = Interval.RExpr.ratCast q
• (a.add b).normalize = a.normalize.add b.normalize
• (a.mul b).normalize = if a.normalize.isZero = true then Interval.RExpr.nat 0 else if b.normalize.isZero = true then Interval.RExpr.nat 0 else a.normalize.mul b.normalize
• (a.div b).normalize = a.normalize.div b.normalize
• a.neg.normalize = a.normalize.neg
• (a.sub b).normalize = a.normalize.sub b.normalize
• a.rexp.normalize = a.normalize.rexp
• inner.rexp.rlog.normalize = inner.normalize
• a.rlog.normalize = a.normalize.rlog
• (a.rpow n).normalize = a.normalize.rpow n
• a.inv.normalize = a.normalize.inv
• (c.iteZero t e).normalize = if c.normalize.isZero = true then t.normalize else if c.normalize.isPos = true then e.normalize else c.normalize.iteZero t.normalize e.normalize
• a.rsqrt.normalize = a.normalize.rsqrt
• (α.expMulLogSub x_1 cost).normalize = α.normalize.expMulLogSub x_1.normalize cost.normalize

def Interval.RExpr.normalize_denote (e : RExpr) : e.normalize.denote = e.denote

Normalization preserves denotation.

Equations

• ⋯ = ⋯

theorem Interval.RExpr.not_gt_of_normalize_eq (lhs rhs : RExpr) (h : lhs.normalize = rhs.normalize) : ¬lhs.denote > rhs.denote

If two RExprs normalize to the same tree, their denotations are equal, so neither is greater than the other.

def Interval.RExpr.checkGtOpt (lhs rhs : RExpr) : Bool

Tree-based comparison using evalBothOpt. Used by rsa_predict for sorry-free soundness proofs.

Equations

• lhs.checkGtOpt rhs = match lhs.normalize.evalBothOpt with | (l_iv, l_valid) => match rhs.normalize.evalBothOpt with | (r_iv, r_valid) => l_valid && r_valid && decide (r_iv.hi < l_iv.lo)

def Interval.RExpr.checkNotGtOpt (lhs rhs : RExpr) : Bool

Tree-based comparison for ¬(>).

Equations

• One or more equations did not get rendered due to their size.

theorem Interval.RExpr.gt_of_checkGtOpt (lhs rhs : RExpr) (h : lhs.checkGtOpt rhs = true) : lhs.denote > rhs.denote

If checkGtOpt succeeds, the denotations are ordered.

theorem Interval.RExpr.not_gt_of_checkNotGtOpt (lhs rhs : RExpr) (h : lhs.checkNotGtOpt rhs = true) : ¬lhs.denote > rhs.denote

If checkNotGtOpt succeeds, ¬(lhs > rhs).

@[implemented_by _private.Linglib.Tactics.RSAPredict.Backend.Reflection.0.Interval.RExpr.checkGtOptCachedImpl]

def Interval.RExpr.checkGtOptMemo (lhs rhs : RExpr) : Bool

Memoized gt check. The @[implemented_by] annotation makes native_decide use the fast memoized implementation while the reference implementation (identical to checkGtOpt) is used for kernel verification.

Equations

• lhs.checkGtOptMemo rhs = lhs.checkGtOpt rhs

@[implemented_by _private.Linglib.Tactics.RSAPredict.Backend.Reflection.0.Interval.RExpr.checkNotGtOptCachedImpl]

def Interval.RExpr.checkNotGtOptMemo (lhs rhs : RExpr) : Bool

Equations

• lhs.checkNotGtOptMemo rhs = lhs.checkNotGtOpt rhs

theorem Interval.RExpr.gt_of_checkGtOptMemo (lhs rhs : RExpr) (h : lhs.checkGtOptMemo rhs = true) : lhs.denote > rhs.denote

theorem Interval.RExpr.not_gt_of_checkNotGtOptMemo (lhs rhs : RExpr) (h : lhs.checkNotGtOptMemo rhs = true) : ¬lhs.denote > rhs.denote

def Interval.RExpr.evalExact : RExpr → Option ℚ

Evaluate an RExpr to an exact ℚ value, if possible. Handles exp nodes via log factor grouping (e.g., exp(1/2·log(x) + 1/2·log(x)) groups to exp(1·log(x)) = x). Returns none for log, expMulLogSub, or when log factor coefficients don't sum to natural numbers. Used for ¬(>) goals where interval arithmetic is too imprecise.

Equations

• (Interval.RExpr.nat n).evalExact = some ↑n
• (Interval.RExpr.ratCast q).evalExact = some q
• (a.add b).evalExact = do let __do_lift ← a.evalExact let __do_lift_1 ← b.evalExact pure (__do_lift + __do_lift_1)
• (a.mul b).evalExact = do let __do_lift ← a.evalExact let __do_lift_1 ← b.evalExact pure (__do_lift * __do_lift_1)
• (a.div b).evalExact = do let vb ← b.evalExact guard (vb ≠ 0) let __do_lift ← a.evalExact pure (__do_lift / vb)
• (a.sub b).evalExact = do let __do_lift ← a.evalExact let __do_lift_1 ← b.evalExact pure (__do_lift - __do_lift_1)
• a.neg.evalExact = do let __do_lift ← a.evalExact pure (-__do_lift)
• a.inv.evalExact = do let va ← a.evalExact guard (va ≠ 0) pure (1 / va)
• (a.rpow n).evalExact = do let va ← a.evalExact guard (0 ≤ va) pure (va ^ n)
• (c.iteZero t e).evalExact = do let vc ← c.evalExact if vc = 0 then t.evalExact else e.evalExact
• a.rexp.evalExact = Interval.evalExpExact✝ a
• a.rlog.evalExact = none
• a.rsqrt.evalExact = none
• (a.expMulLogSub a_1 a_2).evalExact = none

theorem Interval.RExpr.evalExact_sound (e : RExpr) (q : ℚ) (h : e.evalExact = some q) : e.denote = ↑q

Soundness: if evalExact returns q, then denote = (q : ℝ).

def Interval.RExpr.checkExactNotGt (lhs rhs : RExpr) : Bool

If both sides have the same exact ℚ value, ¬(lhs > rhs).

Equations

• lhs.checkExactNotGt rhs = match lhs.evalExact, rhs.evalExact with | some q₁, some q₂ => decide ¬q₁ > q₂ | x, x_1 => false

theorem Interval.RExpr.not_gt_of_checkExactNotGt (lhs rhs : RExpr) (h : lhs.checkExactNotGt rhs = true) : ¬lhs.denote > rhs.denote

Soundness of exact ¬(>) check.

def Interval.RExpr.checkExactGt (lhs rhs : RExpr) : Bool

If lhs evaluates to a strictly greater ℚ than rhs, lhs.denote > rhs.denote.

Equations

• lhs.checkExactGt rhs = match lhs.evalExact, rhs.evalExact with | some q₁, some q₂ => decide (q₁ > q₂) | x, x_1 => false

theorem Interval.RExpr.gt_of_checkExactGt (lhs rhs : RExpr) (h : lhs.checkExactGt rhs = true) : lhs.denote > rhs.denote

Soundness of exact (>) check.

def Interval.RExpr.checkExactEq (lhs rhs : RExpr) : Bool

Check exact equality: both sides evaluate to the same ℚ.

Equations

• lhs.checkExactEq rhs = match lhs.evalExact, rhs.evalExact with | some q₁, some q₂ => q₁ == q₂ | x, x_1 => false

theorem Interval.RExpr.eq_of_checkExactEq (lhs rhs : RExpr) (h : lhs.checkExactEq rhs = true) : lhs.denote = rhs.denote

Soundness of exact equality check.

@[irreducible]

def Interval.RExpr.checkSemanticEq (a b : RExpr) : Bool

Semantic equality: walk two RExpr trees in parallel, using evalExact at each node when possible. Handles exp/log cases where evalExact returns none by checking structural match and recursing into children. This enables proving exp(log(1/(0+1+1))) = exp(log(1/(1+0+1))) — the exp/log match structurally, and the arithmetic children both evalExact to 1/2.

Equations

• One or more equations did not get rendered due to their size.
• (a₁.add a₂).checkSemanticEq (b₁.add b₂) = match (a₁.add a₂).evalExact, (b₁.add b₂).evalExact with | some q₁, some q₂ => q₁ == q₂ | x, x_1 => a₁.checkSemanticEq b₁ && a₂.checkSemanticEq b₂
• (a₁.mul a₂).checkSemanticEq (b₁.mul b₂) = match (a₁.mul a₂).evalExact, (b₁.mul b₂).evalExact with | some q₁, some q₂ => q₁ == q₂ | x, x_1 => a₁.checkSemanticEq b₁ && a₂.checkSemanticEq b₂
• (a₁.div a₂).checkSemanticEq (b₁.div b₂) = match (a₁.div a₂).evalExact, (b₁.div b₂).evalExact with | some q₁, some q₂ => q₁ == q₂ | x, x_1 => a₁.checkSemanticEq b₁ && a₂.checkSemanticEq b₂
• (a₁.sub a₂).checkSemanticEq (b₁.sub b₂) = match (a₁.sub a₂).evalExact, (b₁.sub b₂).evalExact with | some q₁, some q₂ => q₁ == q₂ | x, x_1 => a₁.checkSemanticEq b₁ && a₂.checkSemanticEq b₂
• a₁.neg.checkSemanticEq b₁.neg = match a₁.neg.evalExact, b₁.neg.evalExact with | some q₁, some q₂ => q₁ == q₂ | x, x_1 => a₁.checkSemanticEq b₁
• a₁.inv.checkSemanticEq b₁.inv = match a₁.inv.evalExact, b₁.inv.evalExact with | some q₁, some q₂ => q₁ == q₂ | x, x_1 => a₁.checkSemanticEq b₁
• (a₁.rpow n₁).checkSemanticEq (b₁.rpow n₂) = match (a₁.rpow n₁).evalExact, (b₁.rpow n₂).evalExact with | some q₁, some q₂ => q₁ == q₂ | x, x_1 => a₁.checkSemanticEq b₁ && n₁ == n₂
• a₁.rexp.checkSemanticEq b₁.rexp = match a₁.rexp.evalExact, b₁.rexp.evalExact with | some q₁, some q₂ => q₁ == q₂ | x, x_1 => a₁.checkSemanticEq b₁
• a₁.rsqrt.checkSemanticEq b₁.rsqrt = match a₁.rsqrt.evalExact, b₁.rsqrt.evalExact with | some q₁, some q₂ => q₁ == q₂ | x, x_1 => a₁.checkSemanticEq b₁
• a₁.rlog.checkSemanticEq b₁.rlog = match a₁.rlog.evalExact, b₁.rlog.evalExact with | some q₁, some q₂ => q₁ == q₂ | x, x_1 => a₁.checkSemanticEq b₁
• a.checkSemanticEq b = match a.evalExact, b.evalExact with | some q₁, some q₂ => q₁ == q₂ | x, x_1 => false

theorem Interval.RExpr.eq_of_checkSemanticEq (lhs rhs : RExpr) (h : lhs.checkSemanticEq rhs = true) : lhs.denote = rhs.denote

Soundness of semantic equality: if checkSemanticEq returns true, then the two expressions denote the same real number.

theorem Interval.RExpr.not_gt_of_checkSemanticEq (lhs rhs : RExpr) (h : lhs.checkSemanticEq rhs = true) : ¬lhs.denote > rhs.denote

If semantically equal, neither side is strictly greater.

theorem Interval.RExpr.not_gt_of_denote_eq (lhs rhs : RExpr) (h : lhs.denote = rhs.denote) : ¬lhs.denote > rhs.denote

When lhs and rhs denote the same value, lhs > rhs is impossible.