print simp set

Stream: mathlib4

[Yury G. Kudryashov]

How can I find out whether a given lemma belongs to a given simp set?

[Yury G. Kudryashov]

I have some strange simp only [mfld_simps] failures and I want to find out whether simps! (config := mfld_cfg) correctly assigns these attrs.

[Yury G. Kudryashov]

@Gabriel Ebner @Mario Carneiro :up:

[Yury G. Kudryashov]

The errors appear in !4#2231

[Yury G. Kudryashov]

@Floris van Doorn :up:

[Floris van Doorn]

You are correct, the support for custom attributes was not yet implemented in simps. I'll prioritize that.

[Yury G. Kudryashov]

Then I'll fix the proofs and add a porting note. Anyway, is there some command (or a simple metaprogram) that prints all lemmas tagged with a given simp attr?

[Floris van Doorn]

Here are some useful functions. I'll PR them. @Mario Carneiro are these welcome in Std (or Core)?

import Mathlib.Tactic.ToAdditive -- just to transitively import some things
open Lean Meta Elab Command Tactic Simp

/-- Checks whether `declName` is in `SimpTheorems` as either a lemma or definition to unfold. -/
def Lean.Meta.SimpTheorems.hasAttribute (d : SimpTheorems) (declName : Name) :=
  d.isLemma (.decl declName) || d.isDeclToUnfold declName

/-- Tests whether `decl` has `simp`-attribute `simpAttr`. Returns `false` is `simpAttr` is not a
valid simp-attribute. -/
def isInSimpSet (simpAttr decl : Name) : CoreM Bool := do
  let .some simpDecl ← getSimpExtension? simpAttr | return false
  return (← simpDecl.getTheorems).hasAttribute decl

/-- Returns all declarations with the `simp`-attribute `simpAttr`.
  Note: this also returns many auxiliary declarations. -/
def getAllSimpDecls (simpAttr : Name) : CoreM (List Name) := do
  let .some simpDecl ← getSimpExtension? simpAttr | return []
  let thms ← simpDecl.getTheorems
  return thms.toUnfold.toList ++ thms.lemmaNames.toList.filterMap fun
    | .decl decl => some decl
    | _ => none

/-- Gets all simp-attributes given to declaration `decl`. -/
def getAllSimpAttrs (decl : Name) : CoreM (Array Name) := do
  let mut simpAttrs := #[]
  for (simpAttr, simpDecl) in (← simpExtensionMapRef.get).toList do
    if (← simpDecl.getTheorems).hasAttribute decl then
      simpAttrs := simpAttrs.push simpAttr
  return simpAttrs

@[simp] def foo := 1

run_cmd liftCoreM do logInfo m!"{← isInSimpSet `simp `foo}"

attribute [-simp] foo

run_cmd liftCoreM do
  logInfo m!"{← isInSimpSet `simp `foo}"
  logInfo m!"{← getAllSimpAttrs `foo}"
  logInfo m!"{← getAllSimpDecls `simp}"

[Mario Carneiro]

It could go in either std4 or mathlib4 Lean directory

[Yury G. Kudryashov]

I opened !4#2350 so that I can reference it in comments.

[Floris van Doorn]

Fixed in !4#2398