§ Mutual recursion elaboration in Lean

Lean has four backends for elaborating mutual definitions.

§ Simp Bottlenecks

Benchmarking simp with perf showed us that the bottleneck in one example was in congr, which recursively calls simp and dsimp (dsimp is a variant of simp which preserves definitional equality). This needs to be investigated further. Another bottleneck could be that simp processes bottom-up. This can lead to quadratic behaviour on certain tests. For example, consider:
(not (and A  B) = (or (not A) (not B)
We denote the currently processed node with square brackets [.] If we proceed top-down, see that we would need a quadratic number of steps, because we need a linear number of steps to reach the top from the bottom, where we push down the not. We must repeat this till fixpoint.
(not (and (and  a   b )  c ))
(not (and (and  a   b ) [c]))
(not (and (and  a  [b])  c))
(not (and (and [a]  b)   c))
(not (and [and  a   b]   c))
(not [and (and  a   b)   c])
[not (and (and  a   b)   c]
(or (not  (and a b) (not c))
;; ...

§ Simp lemma generation

If we define functions in a mutual def block, and we tag these functions as simp, then simp must generate simp lemmas. If we have a definition of the form:
inductive X where
| X1 | X2 .. | Xn

def foo: X -> X -> Bool
| X1, _ => True
| _, X2 => False
the theorems will be:
theorem foo.simp1 (x x': X) (h: x = X1): foo x x' = True.
theorem foo.simp2 (x x': X) (h: x /= X1) (h': x' = X2): foo x x' = False.
This could be very expensive in case we have complicated mutual definitions, since Lean can blow up if we have many inductives.