Counter-Example Hunting Tactic

This file provides a tactic for hunting counter-examples to bound claims. Unlike interval_bound which proves bounds, interval_refute searches for violations.

Main tactics

• interval_refute - Search for counter-examples to the current goal

Usage

-- A false theorem: x² ≤ 3 on [-2, 2]
example : ∀ x ∈ Set.Icc (-2 : ℝ) 2, x * x ≤ 3 := by
  interval_refute  -- ERROR: Counter-example found at x = 2, value = 4

-- A true theorem (no counter-example found)
example : ∀ x ∈ Set.Icc (0 : ℝ) 1, x * x ≤ 1 := by
  interval_refute  -- INFO: No counter-example found, theorem appears true!
  interval_bound   -- Actually proves it

How it works

interval_refute uses global optimization to search for violations:

• For f(x) ≤ c: maximizes f(x), checks if max > c
• For c ≤ f(x): minimizes f(x), checks if min < c

A Verified counter-example is a rigorous proof of falsity. A Candidate counter-example might be a precision issue.

@[reducible, inline]

abbrev LeanCert.Tactic.LBExpr : Type

Equations

• LeanCert.Tactic.LBExpr = LeanCert.Core.Expr

Configuration

structure LeanCert.Tactic.RefuteConfig : Type

Configuration for the refute tactic

• maxIterations : ℕ

  Maximum iterations for optimization

• taylorDepth : ℕ

  Taylor depth for evaluation

• tolerance : ℚ

  Tolerance for optimization

def LeanCert.Tactic.instReprRefuteConfig.repr : RefuteConfig → ℕ → Std.Format

Equations

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

instance LeanCert.Tactic.instReprRefuteConfig : Repr RefuteConfig

Equations

• LeanCert.Tactic.instReprRefuteConfig = { reprPrec := LeanCert.Tactic.instReprRefuteConfig.repr }

instance LeanCert.Tactic.instInhabitedRefuteConfig : Inhabited RefuteConfig

Equations

• LeanCert.Tactic.instInhabitedRefuteConfig = { default := { } }

Helper functions

Main tactic implementation

Syntax and tactic

def LeanCert.Tactic.intervalRefute : Lean.ParserDescr

Syntax for the refute tactic

Equations

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

def LeanCert.Tactic.evalIntervalRefute : Lean.Elab.Tactic.Tactic

Equations

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