Init.Simproc

A user-defined simplification procedure used by the simp tactic, and its variants. Here is an example.

theorem and_false_eq {p : Prop} (q : Prop) (h : p = False) : (p ∧ q) = False := by simp [*]

open Lean Meta Simp
simproc ↓ shortCircuitAnd (And _ _) := fun e => do
  let_expr And p q := e | return .continue
  let r ← simp p
  let_expr False := r.expr | return .continue
  let proof ← mkAppM ``and_false_eq #[q, (← r.getProof)]
  return .done { expr := r.expr, proof? := some proof }

The simp tactic invokes shortCircuitAnd whenever it finds a term of the form And _ _. The simplification procedures are stored in an (imperfect) discrimination tree. The procedure should not assume the term e perfectly matches the given pattern. The body of a simplification procedure must have type Simproc, which is an alias for Expr → SimpM Step You can instruct the simplifier to apply the procedure before its sub-expressions have been simplified by using the modifier ↓ before the procedure name. Simplification procedures can be also scoped or local.

Equations

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

source

def Lean.Parser.«command__Dsimproc__[_]_(_):=_» :

Lean.ParserDescr

Similar to simproc, but resulting expression must be definitionally equal to the input one.

Equations

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

source

def Lean.Parser.«command_Simproc_decl_(_):=_» :

Lean.ParserDescr

A user-defined simplification procedure declaration. To activate this procedure in simp tactic, we must provide it as an argument, or use the command attribute to set its [simproc] attribute.

Equations

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

source

def Lean.Parser.«command_Dsimproc_decl_(_):=_» :

Lean.ParserDescr

A user-defined defeq simplification procedure declaration. To activate this procedure in simp tactic, we must provide it as an argument, or use the command attribute to set its [simproc] attribute.

Equations