recOn, (3) well founded induction via
WF, and (4)
casesOn, which allows us to split the recursion into the pattern matching part (casesOn) and the recursion part (brecOn).
recOnis primitive recursion, and is synthesized by the kernel for every inductive declaration. It is often complicated to elaborate pattern matching syntax into a primitive recursor, and is a research question for the mathematically correct, complete solution which handles all cases. This is the lowest level of recursion in Lean, and supports good definitional equality. However, the code generator does not currently generate code for
recOnof mutal inductives, and thus cannot be executed. When working with objects that live in
Type, it is a good idea to use
recOnright now, since (a) it reduces correctly, and (b) has no computational content.
WFis well founded recursion on a terminating metric, which allows one to express functions more easily than primitive recursion. Currently, mutual recursion elaborates into
WF. The drawback is that it has poor definitional equality, and thus breaks a lot of convenient reasoning. It has support in the code generator, since the code generator supports evaluating
recOnof non-mutual definitions (which
WFis more convenient than
recOn, think of ackermann in first order logic. It's not primitive recursive, but does terminate by well founded induction on the lexicographic metric of the naturals. Another example is the hydra tree, which is a crazy game which is known to be finite, but any proof system that can prove the game is finite has at least as much proof strength as PA (Kirby and Paris).
casesOnwhich is used to elaborate inductive predicates.
brecis bounded recursion, which allows using -inductoin: using inductive hypothesis upto children behind you. Useful for encoding things like fibonacci, where for a depends on and (2-induction). This way of elaborating mutual inductives splits the matching part (
casesOn) from the indction part (
brecOn), and is thus more convenient to elaborate into than a lower level
recOn. There are some bugs luring in the lean elaborator for inductive predicates, so this is not fully figured out.
matchin the kernel, and they have guardedness checks in the kernel which checks that the fix is structurally decreasing or whatever. This is complicated, and has led to many soundness bugs in the kernel. Thus, Lean wishes to avoid this.
rec, and would teach the code generator how to code generate mutual
congr, which recursively calls
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:
We denote the currently processed node with square brackets
(not (and A B) = (or (not A) (not B)
[.]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] ;; TRANSFORM=> (or (not (and a b) (not c)) ;; ...
simp, then simp must generate simp lemmas. If we have a definition of the form:
the theorems will be:
inductive X where | X1 | X2 .. | Xn def foo: X -> X -> Bool | X1, _ => True | _, X2 => False
This could be very expensive in case we have complicated mutual definitions, since Lean can blow up if we have many inductives.
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.