ReflectInterval — 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:

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

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

source

inductive Linglib.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].

Instances For

source

instance Linglib.Interval.instReprRExpr :

Repr RExpr

Equations

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

source

def Linglib.Interval.instReprRExpr.repr :

RExpr → ℕ → Std.Format

Equations

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

Instances For

source

def Linglib.Interval.instInhabitedRExpr.default :

RExpr

Equations

Linglib.Interval.instInhabitedRExpr.default = Linglib.Interval.RExpr.nat default

Instances For

source

instance Linglib.Interval.instInhabitedRExpr :

Inhabited RExpr

Equations

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

source

def Linglib.Interval.instBEqRExpr.beq :

RExpr → RExpr → Bool

Equations

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

Instances For

source

instance Linglib.Interval.instBEqRExpr :

BEq RExpr

Equations

Linglib.Interval.instBEqRExpr = { beq := Linglib.Interval.instBEqRExpr.beq }

source

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

Decidable (x✝ = x✝¹)

Equations

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

Instances For

source

instance Linglib.Interval.instDecidableEqRExpr :

DecidableEq RExpr

Equations

Linglib.Interval.instDecidableEqRExpr = Linglib.Interval.instDecidableEqRExpr.decEq

source

noncomputable def Linglib.Interval.RExpr.denote :

RExpr → ℝ

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

Equations

(Linglib.Interval.RExpr.nat 0).denote = 0
(Linglib.Interval.RExpr.nat 1).denote = 1
(Linglib.Interval.RExpr.nat n).denote = ↑n
(Linglib.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

Instances For

source

def Linglib.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.
(Linglib.Interval.RExpr.nat a).eval = Linglib.Interval.QInterval.exact ↑a
(Linglib.Interval.RExpr.ratCast a).eval = Linglib.Interval.QInterval.exact a
(a.add a_1).eval = Linglib.Interval.c✝ (a.eval.add a_1.eval)
a.neg.eval = a.eval.neg
(a.sub a_1).eval = Linglib.Interval.c✝ (a.eval.sub a_1.eval)
a.rexp.eval = Linglib.Interval.c✝ (Linglib.Interval.expInterval a.eval)
a.inv.eval = if h : 0 < a.eval.lo then Linglib.Interval.c✝ (a.eval.invPos h) else { lo := -1, hi := 1, valid := Linglib.Interval.RExpr.eval._proof_1 }

Instances For

source

def Linglib.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

(Linglib.Interval.RExpr.nat a).evalValid = true
(Linglib.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))

Instances For

source

def Linglib.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

Instances For

source

def Linglib.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.
(Linglib.Interval.RExpr.nat a).evalBoth = (Linglib.Interval.QInterval.exact ↑a, true )
(Linglib.Interval.RExpr.ratCast a).evalBoth = (Linglib.Interval.QInterval.exact a, true )
(a.add a_1).evalBoth = match a.evalBoth with | (ra, va) => match a_1.evalBoth with | (rb, vb) => (Linglib.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) => (Linglib.Interval.c✝ (ra.sub rb), va && vb)
a.rexp.evalBoth = match a.evalBoth with | (ra, va) => (Linglib.Interval.c✝ (Linglib.Interval.expInterval ra), va)

Instances For

source

theorem Linglib.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.

source

theorem Linglib.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.

source

theorem Linglib.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.

source

instance Linglib.Interval.instDecidableLtRatHiEvalLo (lhs rhs : RExpr) :

Decidable (rhs.eval.hi < lhs.eval.lo)

Decidable separation check (for native_decide).

Equations

Linglib.Interval.instDecidableLtRatHiEvalLo lhs rhs = inferInstance

source

theorem Linglib.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.

source

instance Linglib.Interval.instDecidableLeRatHiEvalLo (lhs rhs : RExpr) :

Decidable (lhs.eval.hi ≤ rhs.eval.lo)

Equations

Linglib.Interval.instDecidableLeRatHiEvalLo lhs rhs = inferInstance

source

def Linglib.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

Instances For

source

def Linglib.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.
(Linglib.Interval.RExpr.nat a).evalBothOpt = (Linglib.Interval.QInterval.exact ↑a, true )
(Linglib.Interval.RExpr.ratCast a).evalBothOpt = (Linglib.Interval.QInterval.exact a, true )
(a.add a_1).evalBothOpt = match a.evalBothOpt with | (ra, va) => match a_1.evalBothOpt with | (rb, vb) => (Linglib.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) => (Linglib.Interval.c✝ (ra.sub rb), va && vb)
a.rexp.evalBothOpt = a.evalRexpOpt

Instances For

source

theorem Linglib.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.

source

def Linglib.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)

Instances For

source

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

lhs.denote > rhs.denote

If checkGt succeeds, the denotations are ordered.

source

def Linglib.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)

Instances For

source

theorem Linglib.Interval.RExpr.not_gt_of_checkNotGt (lhs rhs : RExpr) (h : lhs.checkNotGt rhs = true) :

¬lhs.denote > rhs.denote

If checkNotGt succeeds, ¬(lhs > rhs).

source

def Linglib.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

Instances For

source

def Linglib.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)

Instances For

source

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

e.denote = 0

If isZero succeeds, the denotation is 0.

source

theorem Linglib.Interval.RExpr.denote_ne_zero (e : RExpr) (h : e.isPos = true) :

e.denote ≠ 0

If isPos succeeds, the denotation is nonzero.

source

def Linglib.Interval.RExpr.normalize :

RExpr → RExpr

Normalize an RExpr by:

Resolving iteZero with constant conditions (dead-branch elimination)
Eliminating mul with provably-zero operands
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
(Linglib.Interval.RExpr.nat n).normalize = Linglib.Interval.RExpr.nat n
(Linglib.Interval.RExpr.ratCast q).normalize = Linglib.Interval.RExpr.ratCast q
(a.add b).normalize = a.normalize.add b.normalize
(a.mul b).normalize = if a.normalize.isZero = true then Linglib.Interval.RExpr.nat 0 else if b.normalize.isZero = true then Linglib.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

Instances For

source

def Linglib.Interval.RExpr.normalize_denote (e : RExpr) :

e.normalize.denote = e.denote

Normalization preserves denotation.

Equations

⋯ = ⋯

Instances For

source

theorem Linglib.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.

source

def Linglib.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)

Instances For

source

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

Bool

Tree-based comparison for ¬(>).

Equations

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

Instances For

source

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

lhs.denote > rhs.denote

If checkGtOpt succeeds, the denotations are ordered.

source

theorem Linglib.Interval.RExpr.not_gt_of_checkNotGtOpt (lhs rhs : RExpr) (h : lhs.checkNotGtOpt rhs = true) :

¬lhs.denote > rhs.denote

If checkNotGtOpt succeeds, ¬(lhs > rhs).

source

@[implemented_by _private.Linglib.Core.Interval.ReflectInterval.0.Linglib.Interval.RExpr.checkGtOptCachedImpl]

def Linglib.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

Instances For

source

@[implemented_by _private.Linglib.Core.Interval.ReflectInterval.0.Linglib.Interval.RExpr.checkNotGtOptCachedImpl]

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

Bool

Equations

lhs.checkNotGtOptMemo rhs = lhs.checkNotGtOpt rhs

Instances For

source

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

lhs.denote > rhs.denote

source

theorem Linglib.Interval.RExpr.not_gt_of_checkNotGtOptMemo (lhs rhs : RExpr) (h : lhs.checkNotGtOptMemo rhs = true) :

¬lhs.denote > rhs.denote

source

def Linglib.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

(Linglib.Interval.RExpr.nat n).evalExact = some ↑n
(Linglib.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 = Linglib.Interval.evalExpExact✝ a
a.rlog.evalExact = none
a.rsqrt.evalExact = none
(a.expMulLogSub a_1 a_2).evalExact = none

Instances For

source

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

e.denote = ↑q

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

source

def Linglib.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

Instances For

source

theorem Linglib.Interval.RExpr.not_gt_of_checkExactNotGt (lhs rhs : RExpr) (h : lhs.checkExactNotGt rhs = true) :

¬lhs.denote > rhs.denote

Soundness of exact ¬(>) check.

source

def Linglib.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

Instances For

source

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

lhs.denote > rhs.denote

Soundness of exact (>) check.

source

def Linglib.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

Instances For

source

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

lhs.denote = rhs.denote

Soundness of exact equality check.

source

@[irreducible]

def Linglib.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

Instances For

source

theorem Linglib.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.

source

theorem Linglib.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.

source

theorem Linglib.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.