Simp builtins

Stream: lean4

[Heather Macbeth]

Is there a simp option which turns off the use of the simpOnlyBuiltins? That is,

#check eq_self -- ∀ {α : Sort u} (a : α), (a = a) = True
#check iff_self -- ∀ (p : Prop), (p ↔ p) = True

If I understand correctly, these lemmas are pretty fundamental to simp's operation as a finishing tactic, since they often constitute the final step in closing the goal. But for the use case I have in mind I would only be using simp as a non-finishing tactic.

[Scott Morrison]

I found https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/making.20a.20TacticM/near/322818507, in which Mario is invoking simp and adding the simpOnlyBuiltins by hand, so presumably you could omit them by that method! It is far from a porcelain option, however.

[Jeremy Salwen]

May not be exactly what you are looking for, but this code may be relevant: https://github.com/leanprover-community/mathlib4/blob/acdc73ba2d14eb2ad72a801acfbd9f592e924e30/Mathlib/Lean/Meta/Simp.lean#LL174C1-L186C25

This is an implementation for doing simplification when metaprogramming:

/-- Construct a `SimpTheorems` from a list of names. (i.e. as with `simp only`). -/
def simpTheoremsOfNames (lemmas : List Name) : MetaM SimpTheorems := do
  lemmas.foldlM (·.addConst ·) (← simpOnlyBuiltins.foldlM (·.addConst ·) {})

/-- Simplify an expression using only a list of lemmas specified by name. -/
-- TODO We need to write a `mkSimpContext` in `MetaM`
-- that supports all the bells and whistles in `simp`.
-- It should generalize this, and another partial implementation in `Tactic.Simps.Basic`.
def simpOnlyNames (lemmas : List Name) (e : Expr) (config : Simp.Config := {}) :
    MetaM Simp.Result := do
  (·.1) <$> simp e
    { simpTheorems := #[← simpTheoremsOfNames lemmas], congrTheorems := ← getSimpCongrTheorems,
      config := config }

You see where simpOnlyBuiltins is explicitly added. If you rewrote this same code without those lemmas included, you would get what you want.

You can also see a complete example of defining an elaborator that uses simpOnlyLemma: https://github.com/leanprover-community/mathlib4/blob/acdc73ba2d14eb2ad72a801acfbd9f592e924e30/Mathlib/Tactic/Reassoc.lean#L39 if you need help wiring it up.

[Heather Macbeth]

Aha, thank you both. My planned use case is a wrapper-for-simp tactic, so it wouldn't matter too much if it's messy underneath. I won't be able to try this out immediately but it looks doable.

[Kyle Miller]

In addition to simpOnlyNames and simpType, there's also simpEq for simplifying both sides of an equality separately. I thought I'd mention this in case turning off eq_self was to help keep simp from simplifying a proposition away from being an equality.