Interval Arithmetic Tactics

This file provides tactics for proving bounds on expressions using interval arithmetic.

Main tactics

• interval_le, interval_ge, interval_lt, interval_gt - Prove bounds using native_decide

Design notes

We provide two sets of lemmas:

Core (computable) - uses evalIntervalCore1

For expressions in ExprSupportedCore (const, var, add, mul, neg, sin, cos), the bound checking is fully computable and works with native_decide.

Extended (noncomputable) - uses evalInterval1

For expressions in ExprSupported (core + exp), the bound checking requires noncomputable evaluation due to Real.exp. These cannot use native_decide.

The tactics use the core evaluator to enable native_decide.

Helper lemmas for decidable bounds (core, computable)

theorem LeanCert.Tactic.intervalCore_hi_le_decide (e : Core.Expr) (I : Core.IntervalRat) (c : ℚ) (cfg : Engine.EvalConfig := { }) : (Engine.evalIntervalCore1 e I cfg).hi ≤ c ↔ decide ((Engine.evalIntervalCore1 e I cfg).hi ≤ c) = true

Decidable version of hi ≤ c for core rational bounds

theorem LeanCert.Tactic.intervalCore_lo_ge_decide (e : Core.Expr) (I : Core.IntervalRat) (c : ℚ) (cfg : Engine.EvalConfig := { }) : c ≤ (Engine.evalIntervalCore1 e I cfg).lo ↔ decide (c ≤ (Engine.evalIntervalCore1 e I cfg).lo) = true

Decidable version of c ≤ lo for core rational bounds

theorem LeanCert.Tactic.intervalCore_hi_lt_decide (e : Core.Expr) (I : Core.IntervalRat) (c : ℚ) (cfg : Engine.EvalConfig := { }) : (Engine.evalIntervalCore1 e I cfg).hi < c ↔ decide ((Engine.evalIntervalCore1 e I cfg).hi < c) = true

Decidable version of hi < c for core rational bounds

theorem LeanCert.Tactic.intervalCore_lo_gt_decide (e : Core.Expr) (I : Core.IntervalRat) (c : ℚ) (cfg : Engine.EvalConfig := { }) : c < (Engine.evalIntervalCore1 e I cfg).lo ↔ decide (c < (Engine.evalIntervalCore1 e I cfg).lo) = true

Decidable version of c < lo for core rational bounds

Combined lemmas for tactic use (core, computable)

theorem LeanCert.Tactic.proveCore_le_by_interval (e : Core.Expr) (hsupp : Core.ExprSupportedCore e) (I : Core.IntervalRat) (c : ℚ) (cfg : Engine.EvalConfig := { }) (x : ℝ) (hx : x ∈ I) (hdom : Engine.evalDomainValid1 e I cfg) (hdec : decide ((Engine.evalIntervalCore1 e I cfg).hi ≤ c) = true) : Core.Expr.eval (fun (x_1 : ℕ) => x) e ≤ ↑c

Prove f(x) ≤ c by core interval arithmetic with decidable check. This combines the correctness theorem with decidability and works with native_decide. Requires domain validity (e.g., log arguments must be positive).

theorem LeanCert.Tactic.proveCore_ge_by_interval (e : Core.Expr) (hsupp : Core.ExprSupportedCore e) (I : Core.IntervalRat) (c : ℚ) (cfg : Engine.EvalConfig := { }) (x : ℝ) (hx : x ∈ I) (hdom : Engine.evalDomainValid1 e I cfg) (hdec : decide (c ≤ (Engine.evalIntervalCore1 e I cfg).lo) = true) : ↑c ≤ Core.Expr.eval (fun (x_1 : ℕ) => x) e

Prove c ≤ f(x) by core interval arithmetic with decidable check. Requires domain validity (e.g., log arguments must be positive).

theorem LeanCert.Tactic.proveCore_lt_by_interval (e : Core.Expr) (hsupp : Core.ExprSupportedCore e) (I : Core.IntervalRat) (c : ℚ) (cfg : Engine.EvalConfig := { }) (x : ℝ) (hx : x ∈ I) (hdom : Engine.evalDomainValid1 e I cfg) (hdec : decide ((Engine.evalIntervalCore1 e I cfg).hi < c) = true) : Core.Expr.eval (fun (x_1 : ℕ) => x) e < ↑c

Prove f(x) < c by core interval arithmetic with decidable check. Requires domain validity (e.g., log arguments must be positive).

theorem LeanCert.Tactic.proveCore_gt_by_interval (e : Core.Expr) (hsupp : Core.ExprSupportedCore e) (I : Core.IntervalRat) (c : ℚ) (cfg : Engine.EvalConfig := { }) (x : ℝ) (hx : x ∈ I) (hdom : Engine.evalDomainValid1 e I cfg) (hdec : decide (c < (Engine.evalIntervalCore1 e I cfg).lo) = true) : ↑c < Core.Expr.eval (fun (x_1 : ℕ) => x) e

Prove c < f(x) by core interval arithmetic with decidable check. Requires domain validity (e.g., log arguments must be positive).

Universal quantifier versions (core, computable)

theorem LeanCert.Tactic.proveCore_forall_le_by_interval (e : Core.Expr) (hsupp : Core.ExprSupportedCore e) (I : Core.IntervalRat) (c : ℚ) (cfg : Engine.EvalConfig := { }) (hdom : Engine.evalDomainValid1 e I cfg) (hdec : decide ((Engine.evalIntervalCore1 e I cfg).hi ≤ c) = true) (x : ℝ) : x ∈ I → Core.Expr.eval (fun (x_1 : ℕ) => x) e ≤ ↑c

Prove ∀ x ∈ I, f(x) ≤ c by core interval arithmetic. Works with native_decide for expressions in ExprSupportedCore. Requires domain validity (e.g., log arguments must be positive).

theorem LeanCert.Tactic.proveCore_forall_ge_by_interval (e : Core.Expr) (hsupp : Core.ExprSupportedCore e) (I : Core.IntervalRat) (c : ℚ) (cfg : Engine.EvalConfig := { }) (hdom : Engine.evalDomainValid1 e I cfg) (hdec : decide (c ≤ (Engine.evalIntervalCore1 e I cfg).lo) = true) (x : ℝ) : x ∈ I → ↑c ≤ Core.Expr.eval (fun (x_1 : ℕ) => x) e

Prove ∀ x ∈ I, c ≤ f(x) by core interval arithmetic. Requires domain validity (e.g., log arguments must be positive).

theorem LeanCert.Tactic.proveCore_forall_lt_by_interval (e : Core.Expr) (hsupp : Core.ExprSupportedCore e) (I : Core.IntervalRat) (c : ℚ) (cfg : Engine.EvalConfig := { }) (hdom : Engine.evalDomainValid1 e I cfg) (hdec : decide ((Engine.evalIntervalCore1 e I cfg).hi < c) = true) (x : ℝ) : x ∈ I → Core.Expr.eval (fun (x_1 : ℕ) => x) e < ↑c

Prove ∀ x ∈ I, f(x) < c by core interval arithmetic. Requires domain validity (e.g., log arguments must be positive).

theorem LeanCert.Tactic.proveCore_forall_gt_by_interval (e : Core.Expr) (hsupp : Core.ExprSupportedCore e) (I : Core.IntervalRat) (c : ℚ) (cfg : Engine.EvalConfig := { }) (hdom : Engine.evalDomainValid1 e I cfg) (hdec : decide (c < (Engine.evalIntervalCore1 e I cfg).lo) = true) (x : ℝ) : x ∈ I → ↑c < Core.Expr.eval (fun (x_1 : ℕ) => x) e

Prove ∀ x ∈ I, c < f(x) by core interval arithmetic. Requires domain validity (e.g., log arguments must be positive).

Extended versions (noncomputable, for reference)

theorem LeanCert.Tactic.prove_le_by_interval (e : Core.Expr) (hsupp : Core.ExprSupported e) (I : Core.IntervalRat) (c : ℚ) (x : ℝ) (hx : x ∈ I) (hhi : (Engine.evalInterval1 e I).hi ≤ c) : Core.Expr.eval (fun (x_1 : ℕ) => x) e ≤ ↑c

Prove f(x) ≤ c by extended interval arithmetic. NOTE: Cannot use native_decide due to noncomputability of exp.

theorem LeanCert.Tactic.prove_ge_by_interval (e : Core.Expr) (hsupp : Core.ExprSupported e) (I : Core.IntervalRat) (c : ℚ) (x : ℝ) (hx : x ∈ I) (hlo : c ≤ (Engine.evalInterval1 e I).lo) : ↑c ≤ Core.Expr.eval (fun (x_1 : ℕ) => x) e

Prove c ≤ f(x) by extended interval arithmetic.

Tactic Macros

These macros provide an ergonomic interface for proving bounds. They use the CORE (computable) evaluator, so native_decide works.

Usage

example : ∀ x ∈ I01, Expr.eval (fun _ => x) exprXSq ≤ 1 := by
  interval_le exprXSq exprXSq_supp I01 1

Note: For expressions containing exp, use manual proofs with expr_le_of_interval_hi and explicit bound computation, as native_decide won't work.

def LeanCert.Tactic.«tacticInterval_le_,_,_,_» : Lean.ParserDescr

Prove ∀ x ∈ I, f(x) ≤ c using core interval arithmetic. Usage: interval_le e supp I c Requires ExprSupportedCore e for native_decide to work.

Equations

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

def LeanCert.Tactic.«tacticInterval_ge_,_,_,_» : Lean.ParserDescr

Prove ∀ x ∈ I, c ≤ f(x) using core interval arithmetic. Usage: interval_ge e supp I c

Equations

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

def LeanCert.Tactic.«tacticInterval_lt_,_,_,_» : Lean.ParserDescr

Prove ∀ x ∈ I, f(x) < c using core interval arithmetic. Usage: interval_lt e supp I c

Equations

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

def LeanCert.Tactic.«tacticInterval_gt_,_,_,_» : Lean.ParserDescr

Prove ∀ x ∈ I, c < f(x) using core interval arithmetic. Usage: interval_gt e supp I c

Equations

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

def LeanCert.Tactic.«tacticInterval_le_pt_,_,_,_,_,_» : Lean.ParserDescr

Prove a pointwise bound f(x) ≤ c given x ∈ I. Usage: interval_le_pt e supp I c x hx

Equations

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

def LeanCert.Tactic.«tacticInterval_ge_pt_,_,_,_,_,_» : Lean.ParserDescr

Prove a pointwise bound c ≤ f(x) given x ∈ I. Usage: interval_ge_pt e supp I c x hx

Equations

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

Extended interval tactics (noncomputable, for exp-containing expressions)

These tactics work with ExprSupported (which includes exp) but cannot use native_decide. They reduce the goal to an interval inequality that must be proved by other means (linarith, norm_num, or manual computation).

Usage

-- Reduces to goal: (evalInterval1 exprExp I01).hi ≤ 3
theorem exp_le_three_on_01 :
    ∀ x ∈ I01, Expr.eval (fun _ => x) exprExp ≤ (3 : ℚ) := by
  interval_ext_le exprExp, exprExp_supp, I01, 3
  -- Then prove the interval bound manually
  sorry

def LeanCert.Tactic.«tacticInterval_ext_le_,_,_,_» : Lean.ParserDescr

Extended interval tactic for ≤ (supports exp). Reduces ∀ x ∈ I, f(x) ≤ c to (evalInterval1 e I).hi ≤ c. Usage: interval_ext_le e, supp, I, c

Equations

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

def LeanCert.Tactic.«tacticInterval_ext_ge_,_,_,_» : Lean.ParserDescr

Extended interval tactic for ≥ (supports exp). Reduces ∀ x ∈ I, c ≤ f(x) to c ≤ (evalInterval1 e I).lo. Usage: interval_ext_ge e, supp, I, c

Equations

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

def LeanCert.Tactic.«tacticInterval_ext_lt_,_,_,_» : Lean.ParserDescr

Extended interval tactic for < (supports exp). Reduces ∀ x ∈ I, f(x) < c to (evalInterval1 e I).hi < c. Usage: interval_ext_lt e, supp, I, c

Equations

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

def LeanCert.Tactic.«tacticInterval_ext_gt_,_,_,_» : Lean.ParserDescr

Extended interval tactic for > (supports exp). Reduces ∀ x ∈ I, c < f(x) to c < (evalInterval1 e I).lo. Usage: interval_ext_gt e, supp, I, c

Equations

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

def LeanCert.Tactic.«tacticInterval_ext_le_pt_,_,_,_,_,_» : Lean.ParserDescr

Extended pointwise tactic for ≤ (supports exp). Reduces f(x) ≤ c (given x ∈ I) to (evalInterval1 e I).hi ≤ c. Usage: interval_ext_le_pt e, supp, I, c, x, hx

Equations

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

def LeanCert.Tactic.«tacticInterval_ext_ge_pt_,_,_,_,_,_» : Lean.ParserDescr

Extended pointwise tactic for ≥ (supports exp). Reduces c ≤ f(x) (given x ∈ I) to c ≤ (evalInterval1 e I).lo. Usage: interval_ext_ge_pt e, supp, I, c, x, hx

Equations

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