Dischargers for Conditional Rewrite Rules

This module provides dischargers for handling conditional rewrite rules in Sym.simp. A discharger attempts to prove side conditions that arise during rewriting.

Overview

When applying a conditional rewrite rule h : P → a = b, the simplifier must prove the precondition P before using the rule. A Discharger is a function that attempts to construct such proofs.

Example: Consider the rewrite rule:

theorem div_self (n : Nat) (h : n ≠ 0) : n / n = 1

When simplifying x / x, the discharger must prove x ≠ 0 to apply this rule.

Design

Dischargers work by:

1. Attempting to simplify the side condition to True
2. If successful, extracting a proof from the simplification result
3. Returning .failed if the condition cannot be discharged

Each discharge result also carries a contextDependent flag indicating whether the discharge used context-dependent information (e.g., local hypotheses). This enables the simplifier's two-tier cache to correctly handle context-dependent results.

inductive Lean.Meta.Sym.Simp.DischargeResult : Type

Result of a discharge attempt.

• failed (contextDependent : Bool := false) : DischargeResult

  Discharge failed. If contextDependent = true, it might succeed in another local context.

• solved (proof : Expr) (contextDependent : Bool := false) : DischargeResult

  Discharge succeeded with the given proof.

@[reducible, inline]

abbrev Lean.Meta.Sym.Simp.Discharger : Type

A discharger attempts to prove propositions that arise as side conditions during rewriting.

Given a proposition e : Prop, returns:

• .solved proof if e can be proven
• .failed otherwise

Both carry a contextDependent flag indicating whether context-dependent information was used during the attempt.

Equations

• Lean.Meta.Sym.Simp.Discharger = (Lean.Expr → Lean.Meta.Sym.Simp.SimpM Lean.Meta.Sym.Simp.DischargeResult)

def Lean.Meta.Sym.Simp.mkDischargerFromSimproc (p : Simproc) : Discharger

Converts a simplification procedure into a discharger.

A Simproc can be used as a discharger by simplifying the side condition and checking if it reduces to True. If so, the equality proof is converted to a proof of the original proposition.

Algorithm:

1. Apply the simproc to the side condition e
2. If e simplifies to True (via proof h : e = True), return ofEqTrue h : e
3. Otherwise, return .failed (cannot discharge)

Parameters:

• p: A simplification procedure to use for discharging conditions

Example: If p simplifies 5 < 10 to True via proof h : (5 < 10) = True, then mkDischargerFromSimproc p returns ofEqTrue h : 5 < 10.

Equations

• Lean.Meta.Sym.Simp.mkDischargerFromSimproc p e = do let __do_lift ← p e pure (Lean.Meta.Sym.Simp.resultToDischargeResult✝ e __do_lift)

def Lean.Meta.Sym.Simp.dischargeSimpSelf : Discharger

The default discharger uses the simplifier itself to discharge side conditions.

This creates a natural recursive behavior: when applying conditional rules, the simplifier is invoked to prove their preconditions. This is effective because:

1. Ground terms: Conditions like 5 ≠ 0 are evaluated by simprocs
2. Recursive simplification: Complex conditions are reduced to simpler ones
3. Lemma application: The simplifier can apply other rewrite rules to conditions

It ensures the cached results are discarded, and increases the discharge depth to avoid infinite recursion.

Equations

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

def Lean.Meta.Sym.Simp.dischargeNone : Discharger

A discharger that fails to prove any side condition.

This is used when conditional rewrite rules should not be applied. It immediately returns .failed for all propositions, effectively disabling conditional rewriting.

Use cases:

• Testing: Isolating unconditional rewriting behavior
• Performance: Avoiding expensive discharge attempts when conditions are unlikely to hold
• Controlled rewriting: Explicitly disabling conditional rules in specific contexts

Equations

• Lean.Meta.Sym.Simp.dischargeNone x✝ = pure Lean.Meta.Sym.Simp.DischargeResult.failed

def Lean.Meta.Sym.Simp.dischargeAssumption : Discharger

A discharger for testing that proves side conditions using hypotheses from the local context. Always context-dependent: available hypotheses change when entering binders.

Equations

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