Documentation

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
    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.

                                                      Equations
                                                        Instances For