New attribute to mark theorems

Stream: lean4

[Tomas Skrivan]

Is it possible to define a new attribute to mark theorems and then tell rw or simp to use these theorems?

[Leonardo de Moura]

We do not have a command for creating a new simp attribute, but we have APIs for doing that. That is, users can import Lean and invoke these APIs and create their own simp or simp-variant.
https://github.com/leanprover/lean4/blob/master/src/Lean/Meta/Tactic/Simp/SimpLemmas.lean#L227-L230
We had simp with <simp-attr-nam> in Lean 3, but we assumed it was a not very popular feature. That being said, I just searched Mathlib and found

simp only with mfld_simps
simp with functor_norm
simp with parity_simps

[Johan Commelin]

@Leonardo de Moura Just FYI, I found the following uses of mk_simp_attribute. I think that most of these are used a fair amount. But I'm sure that the new APIs are more powerful.

src/logic/nontrivial.lean
165:mk_simp_attribute nontriviality "Simp lemmas for `nontriviality` tactic"

src/tactic/norm_cast.lean
64:mk_simp_attribute push_cast "The `push_cast` simp attribute uses `norm_cast` lemmas

src/tactic/equiv_rw.lean
187:mk_simp_attribute equiv_rw_simp "The simpset `equiv_rw_simp` is used by the tactic `equiv_rw` to

src/tactic/transport.lean
22:mk_simp_attribute transport_simps

src/algebra/group_with_zero/basic.lean
43:mk_simp_attribute field_simps "The simpset `field_simps` is used by the tactic `field_simp` to

src/control/monad/basic.lean
38:mk_simp_attribute monad_norm none with functor_norm

src/ring_theory/witt_vector/is_poly.lean
100:mk_simp_attribute ghost_simps

src/measure_theory/integral/bochner.lean
1395:mk_simp_attribute integral_simps "Simp set for integral rules."

src/data/nat/parity.lean
85:mk_simp_attribute parity_simps "Simp attribute for lemmas about `even`"

src/data/equiv/local_equiv.lean
67:mk_simp_attribute mfld_simps "The simpset `mfld_simps` records several simp lemmas that are

[Leonardo de Moura]

@Johan Commelin Thanks for posting the information. Do you know which ones are "fixed" collection of simp which does to change? For fixed collections, we don't use attributes in Lean 4, but create the fixed collection programmatically. For example, the split tactic in Lean 4 uses

    let mut s : SimpLemmas := {}
    s ← s.addConst ``if_pos
    s ← s.addConst ``if_neg
    s ← s.addConst ``dif_pos
    s ← s.addConst ``dif_neg

[Tomas Skrivan]

And where am I supposed to call this API? I have tried bunch of things but nothing really worked.

[Leonardo de Moura]

@Tomas Skrivan
Sorry, we don't have documentation for that yet :(
Right now, the only documentation is our code and its docstrings.
We will try to add more documentation soon.
Unfortunately, there is no short answer here. One has to declare the attribute, and then have a simp tactic that uses it.
That being said, it is easier to create an extensible rw tactic using just macros.

constant f : Nat → Nat
constant g : Nat → Nat
axiom f_eq (x : Nat) : f x = x + 1
axiom g_eq (x : Nat) : g (f x) = x

syntax "myrw_step" : tactic --

macro_rules
  | `(tactic| myrw_step) => `(tactic| rw [f_eq])

macro "myrw" : tactic => `(repeat myrw_step)

example : f x = x + 1 := by
  myrw

example : f (g (f x)) = x + 1 := by
  myrw
  done -- unsolved goal

macro_rules
  | `(tactic| myrw_step) => `(tactic| rw [g_eq])  -- extend `myrw_step`

example : f (g (f x)) = x + 1 := by
  myrw
  done -- worked

https://leanprover.github.io/theorem_proving_in_lean4/tactics.html#extensible-tactics

[Johan Commelin]

@Leonardo de Moura The results are mixed. But I think that parity_simps and field_simps are basically fixed.

[Johan Commelin]

The others occasionally might get a new lemma added to the set.

[Leonardo de Moura]

@Johan Commelin Thanks.