Counter-Example Search

This file provides machinery for finding counter-examples to bound claims. Finding a counter-example is just global optimization: to disprove f(x) ≤ C, we maximize f(x) and check if the result exceeds C.

Main definitions

• CounterExampleStatus - Whether a counter-example is verified or just a candidate
• CounterExample - A point that violates (or may violate) a bound
• findViolation - Search for counter-examples to f(x) ≤ limit
• findViolationLower - Search for counter-examples to limit ≤ f(x)

Counter-Example Types

• Verified: The rigorous lower bound of max(f) exceeds the limit. This is a mathematical proof that the bound is false.

• Candidate: The upper bound exceeds the limit, but the lower bound doesn't. This might indicate a true violation (precision too low) or a false positive (interval wrapping).

Usage

-- Check if x² ≤ 3 on [-2, 2]
let result := findViolation (Expr.mul (Expr.var 0) (Expr.var 0)) [⟨-2, 2, by norm_num⟩] 3
-- Returns some { status := .Verified, ... } because max(x²) = 4 > 3

Counter-example types

inductive LeanCert.Engine.Search.CounterExampleStatus : Type

Status of a counter-example

• Verified : CounterExampleStatus

  Definitely violates the bound (proof of negation possible)

• Candidate : CounterExampleStatus

  Likely violates the bound (or precision too low)

instance LeanCert.Engine.Search.instReprCounterExampleStatus : Repr CounterExampleStatus

Equations

• LeanCert.Engine.Search.instReprCounterExampleStatus = { reprPrec := LeanCert.Engine.Search.instReprCounterExampleStatus.repr }

def LeanCert.Engine.Search.instReprCounterExampleStatus.repr : CounterExampleStatus → ℕ → Std.Format

Equations

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

instance LeanCert.Engine.Search.instDecidableEqCounterExampleStatus : DecidableEq CounterExampleStatus

Equations

• LeanCert.Engine.Search.instDecidableEqCounterExampleStatus x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def LeanCert.Engine.Search.instInhabitedCounterExampleStatus.default : CounterExampleStatus

Equations

• LeanCert.Engine.Search.instInhabitedCounterExampleStatus.default = LeanCert.Engine.Search.CounterExampleStatus.Verified

instance LeanCert.Engine.Search.instInhabitedCounterExampleStatus : Inhabited CounterExampleStatus

Equations

• LeanCert.Engine.Search.instInhabitedCounterExampleStatus = { default := LeanCert.Engine.Search.instInhabitedCounterExampleStatus.default }

structure LeanCert.Engine.Search.CounterExample : Type

A counter-example to a bound claim

• point : List ℚ

  The input point (midpoint of the best box)

• valueLo : ℚ

  The computed output interval at/near the point

• valueHi : ℚ
• status : CounterExampleStatus

  Whether the counter-example is verified or just a candidate

• box : Optimization.Box

  The box containing the counter-example

• iterations : ℕ

  Number of iterations used

instance LeanCert.Engine.Search.instReprCounterExample : Repr CounterExample

Equations

• LeanCert.Engine.Search.instReprCounterExample = { reprPrec := LeanCert.Engine.Search.instReprCounterExample.repr }

def LeanCert.Engine.Search.instReprCounterExample.repr : CounterExample → ℕ → Std.Format

Equations

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

def LeanCert.Engine.Search.CounterExample.isVerified (ce : CounterExample) : Bool

Is this a verified counter-example?

Equations

• ce.isVerified = (ce.status == LeanCert.Engine.Search.CounterExampleStatus.Verified)

def LeanCert.Engine.Search.CounterExample.boxMidpoint (B : Optimization.Box) : List ℚ

Get the midpoint of each interval in the box

Equations

• LeanCert.Engine.Search.CounterExample.boxMidpoint B = List.map (fun (x : LeanCert.Core.IntervalRat) => x.midpoint) B

Upper bound violation (f(x) ≤ limit)

def LeanCert.Engine.Search.findViolation (e : Core.Expr) (domain : Optimization.Box) (limit : ℚ) (cfg : Optimization.GlobalOptConfig := { }) : Option CounterExample

Search for a counter-example to the claim ∀ x ∈ domain, f(x) ≤ limit.

Returns some CounterExample if the bound cannot be verified. Returns none if the theorem appears to be true (no violation found).

Algorithm: Maximize f(x) over the domain. If max(f).lo > limit, the bound is definitely false. If max(f).hi > limit but lo ≤ limit, there might be a violation.

Equations

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

def LeanCert.Engine.Search.findViolationDiv (e : Core.Expr) (domain : Optimization.Box) (limit : ℚ) (cfg : Optimization.GlobalOptConfig := { }) : Option CounterExample

Variant of findViolation with division support.

Equations

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

Lower bound violation (limit ≤ f(x))

def LeanCert.Engine.Search.findViolationLower (e : Core.Expr) (domain : Optimization.Box) (limit : ℚ) (cfg : Optimization.GlobalOptConfig := { }) : Option CounterExample

Search for a counter-example to the claim ∀ x ∈ domain, limit ≤ f(x).

Returns some CounterExample if the bound cannot be verified.

Algorithm: Minimize f(x) over the domain. If min(f).hi < limit, the bound is definitely false.

Equations

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

def LeanCert.Engine.Search.findViolationLowerDiv (e : Core.Expr) (domain : Optimization.Box) (limit : ℚ) (cfg : Optimization.GlobalOptConfig := { }) : Option CounterExample

Variant with division support.

Equations

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

Strict bound violations

def LeanCert.Engine.Search.findViolationStrict (e : Core.Expr) (domain : Optimization.Box) (limit : ℚ) (cfg : Optimization.GlobalOptConfig := { }) : Option CounterExample

Search for a counter-example to ∀ x ∈ domain, f(x) < limit. A violation means f(x) ≥ limit for some x.

Equations

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

def LeanCert.Engine.Search.findViolationStrictLower (e : Core.Expr) (domain : Optimization.Box) (limit : ℚ) (cfg : Optimization.GlobalOptConfig := { }) : Option CounterExample

Search for a counter-example to ∀ x ∈ domain, limit < f(x). A violation means f(x) ≤ limit for some x.

Equations

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

Pretty printing

def LeanCert.Engine.Search.CounterExample.format (ce : CounterExample) (limit : ℚ) : String

Format a counter-example for display

Equations

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