SimpTheorems

Stream: lean4

[Marcus Rossel]

Is there documentation on the data structures used for simp somewhere? In particular, I don't understand how to use docs4#Lean.Meta.SimpTheorems.
As an example of my confusion: to elaborate a list of arguments to simp, there's the function docs4#Lean.Elab.Tactic.elabSimpArgs. Among other things it returns an array of SimpTheorems. First, I don't understand why it returns an array of SimpTheorems, as the latter seems to already be a collection of simp theorems. Then, in the SimpTheorems structure there seem to be two ways of accessing the theorems. First, via the discrimination trees (though I don't understand what pre vs. post is) and second via the lemmaNames. Is the lemmaNames field the preferred way of accessing the list of theorems? E.g., I want to check if the simp theorems all hold by reflexivity, but I'm not sure how to do this based only on lemmaNames.

[Jannis Limperg]

• Array of SimpTheorems because simp can use multiple sets of simp theorems, each of which is a SimpTheorems structure. Alternatively, one could implement a merge operation for SimpTheorems (I had this in Aesop at some point), but that's harder and possibly slower.
• pre and post lemmas are used at different points during simp, but I forget the details.
• lemmaNames is a cache containing the names (more precisely: origins) of all lemmas contained in the structure. This enables fast membership queries.
• There are some additional operations on DiscrTrees in mathlib, e.g. docs#Lean.Meta.DiscrTree.fold.

None of this is documented afaik; I learned it from staring at the simp code at lot.

[Kyle Miller]

The core loop in simp (docs#Lean.Meta.Simp.simp.simpLoop) looks like:

1. Check to see if there is a pre lemma that applies to the current expression. If so, apply it and continue looking for applicable pre lemmas.
2. Apply a congruence lemma to the current expression. This creates subproblems -- recursively apply simp to these subproblems. (This implements how simp is able to visit subexpressions.)
3. Check to see if a post lemma applies to the current expression. If so, apply it and start back at 1.