Claude-2.1's answer to a question about a custom `simp` tactic in Lean

claude-my-simp.md

Q: In Lean 4, how do I write a tactic that adds a fixed list of lemmas to a simp call?

A: Here is one way to write a tactic in Lean 4 that adds a fixed list of lemmas to a simp call:

import tactic

-- List of lemmas we want to add
def my_simp_lemmas : list name := [`foo, `bar, `baz]

-- Tactic that does simp with extra lemmas
meta def my_simp (t : tactic unit) : tactic unit :=
do 
  lemmas ← my_simp_lemmas.mmap fun n => mk_const n,
  t,
  simp lemmas

-- Usage:
example : my_bool ∧ my_bool → my_bool
| h => my_simp $ simp [h]

The key parts:

• my_simp_lemmas defines the fixed list of lemma names we want to add
• my_simp takes an existing tactic t, runs t, runs simp with the lemmas
• We use mmap to convert the name list into concrete lemma expressions
• When calling my_simp, we pass the normal simp call as the argument t

So this allows wrapping any tactic with an automated simp call with the added lemmas.

Q: Basically, I just want to write a tactic my_simp such that my_simp [lemma_1, lemma_2, ...] expands to simp only [lemma_1, lemma_2, ..., my_lemma_1, my_lemma_2, ...]. How would I do it?

A: Here is how to write my_simp to automatically add some lemmas to any simp call:

meta def my_simp (lemmas : list expr) : tactic unit :=
do
  let my_lemmas := [`my_lemma_1, `my_lemma_2] |>.mmap mk_const,
  t ← lemmas.mmap mk_const,
  simp only t my_lemmas

-- Usage:
example : my_bool ∧ my_bool → my_bool  
| h => my_simp [h]

The key points:

• Define my_lemmas to contain the default lemmas to add
• Convert the input lemmas to expressions
• Concatenate the input lemmas and my_lemmas
• Pass them all to simp only

So now my_simp will take the user's lemmas, combine them with my_lemmas, and call simp only automatically.