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
Instances For
Similar to simproc
, but resulting expression must be definitionally equal to the input one.
Equations
Instances For
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
Instances For
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
Instances For
A builtin simplification procedure.
Equations
Instances For
A builtin defeq simplification procedure.
Equations
Instances For
A builtin simplification procedure declaration.
Equations
Instances For
A builtin defeq simplification procedure declaration.
Equations
Instances For
Auxiliary command for associating a pattern with a simplification procedure.
Equations
Instances For
Auxiliary command for associating a pattern with a builtin simplification procedure.
Equations
Instances For
Auxiliary attribute for simplification procedures.
Equations
Instances For
Auxiliary attribute for symbolic evaluation procedures.
Equations
Instances For
Auxiliary attribute for builtin simplification procedures.
Equations
Instances For
Auxiliary attribute for builtin symbolic evaluation procedures.