Set of all auxiliary lemmas

Stream: lean4 dev

[Leni Aniva]

Should AuxLemmas store a set of all auxiliary lemmas?

structure AuxLemmas where
  lemmas : PHashMap Expr (Name × List Name) := {}
  deriving Inhabited

The data structure in this environment extension is not conducive for searching for the name of a lemma, so the unfold aux lemma function in Mathlib takes a guess based on pattern matching of a name to determine if it is an aux lemma.

def Lean.Name.isAuxLemma (n : Name) : Bool :=
  match n with
  -- `mkAuxLemma` generally allows for arbitrary prefixes but these are the ones produced by core.
  | .str _ s => "_proof_".isPrefixOf s || "_simp_".isPrefixOf s
  | _ => false

If the aux lemma env extension is modified to be something like this instead, this process would not involve any heuristics.

structure AuxLemmas where
  lemmasSet : PHashSet Name
  lemmas : PHashMap Expr (Name × List Name) := {}
  deriving Inhabited

[Leni Aniva]

Maybe this isn't possible since AuxLemmas is just a cache