Lean.Meta.Tactic.FunInd

This module contains code to derive, from the definition of a recursive function (structural or well-founded, possibly mutual), a functional induction principle tailored to proofs about that function(s).

For example from:

def ackermann : Nat → Nat → Nat
  | 0, m => m + 1
  | n+1, 0 => ackermann n 1
  | n+1, m+1 => ackermann n (ackermann (n + 1) m)

we get

ackermann.induct (motive : Nat → Nat → Prop) (case1 : ∀ (m : Nat), motive 0 m)
  (case2 : ∀ (n : Nat), motive n 1 → motive (Nat.succ n) 0)
  (case3 : ∀ (n m : Nat), motive (n + 1) m → motive n (ackermann (n + 1) m) → motive (Nat.succ n) (Nat.succ m))
  (x x : Nat) : motive x x

Specification #

The functional induction principle takes the same fixed parameters as the function, and the motive takes the same non-fixed parameters as the original function.

For each branch of the original function, there is a case in the induction principle. Here "branch" roughly corresponds to tail-call positions: branches of top-level if-then-else and of match expressions.

For every recursive call in that branch, an induction hypothesis asserting the motive for the arguments of the recursive call is provided. If the recursive call is under binders and it, or its proof of termination, depend on the the bound values, then these become assumptions of the inductive hypothesis.

Additionally, the local context of the branch (e.g. the condition of an if-then-else; a let-binding, a have-binding) is provided as assumptions in the corresponding induction case, if they are likely to be useful (as determined by MVarId.cleanup).

Mutual recursion is supported and results in multiple motives.

Implementation overview (well-founded recursion) #

For a non-mutual, unary function foo (or else for the _unary function), we

expect its definition to be of the form
```
def foo := fun x₁ … xₙ (y : a) => WellFounded.fix (fun y' oldIH => body) y
```
where xᵢ… are the fixed parameter prefix and y is the varying parameter of the function.

From this structure we derive the type of the motive, and start assembling the induction principle:

def foo.induct := fun x₁ … xₙ (motive : (y : a) → Prop) =>
 fix (fun y' newIH => T[body])

The first phase, transformation T1[body] (implemented in buildInductionBody) mirrors the branching structure of foo, i.e. replicates dite and some matcher applications, while adjusting their motive. It also unfolds calls to oldIH and collects induction hypotheses in conditions (see below).

In particular, when translating a match it is prepared to recognize the idiom as introduced by mkFix via Lean.Meta.MatcherApp.addArg?, which refines the type of oldIH throughout the match. The transformation will replace oldIH with newIH here.
```
     T[(match (motive := fun oldIH => …) y with | … => fun oldIH' => body) oldIH]
 ==> (match (motive := fun newIH => …) y with | … => fun newIH' => T[body]) newIH
```
In addition, the information gathered from the match is preserved, so that when performing the proof by induction, the user can reliably enter the right case. To achieve this
- the matcher is replaced by its splitter, which brings extra assumptions into scope when patterns are overlapping (using matcherApp.transform (useSplitter := true))
- simple discriminants that are mentioned in the goal (i.e plain parameters) are instantiated in the goal.
- for discriminants that are not instantiated that way, equalities connecting the discriminant to the instantiation are added (just as if the user wrote match h : x with …)
When a tail position (no more branching) is found, function buildInductionCase assembles the type of the case: a fresh MVar asserts the current goal, unwanted values from the local context are cleared, and the current body is searched for recursive calls using foldAndCollect, which are then asserted as inductive hyptheses in the MVar.
The function foldAndCollect walks the term and performs two operations:
- collects the induction hypotheses for the current case (with proofs).
- recovering the recursive calls
So when it encounters a saturated application of oldIH arg proof, it
- returns f arg and
- remembers the expression newIH arg proof : motive x as an inductive hypothesis.
Since arg and proof can contain further recursive calls, they are folded there as well. This assumes that the termination proof proof works nevertheless.

Again, foldAndCollect may encounter the Lean.Meta.Matcherapp.addArg? idiom, and again it threads newIH through, replacing the extra argument. The resulting type of this induction hypothesis is now itself a match statement (cf. Lean.Meta.MatcherApp.inferMatchType)

The termination proof of foo may have abstracted over some proofs; these proofs must be transferred, so auxillary lemmas are unfolded if needed.
After this construction, the MVars introduced by buildInductionCase are turned into parameters.

The resulting term then becomes foo.induct at its inferred type.

Implementation overview (mutual/non-unary well-founded recursion) #

If foo is not unary and/or part of a mutual reduction, then the induction theorem for foo._unary (i.e. the unary non-mutual recursion function produced by the equation compiler) of the form

foo._unary.induct : {motive : (a ⊗' b) ⊕' c → Prop} →
  (case1 : ∀ …, motive (PSum.inl (x,y)) →  …) → … →
  (x : (a ⊗' b) ⊕' c) → motive x

will first in unpackMutualInduction be turned into a joint induction theorem of the form

foo.mutual_induct : {motive1 : a → b → Prop} {motive2 : c → Prop} →
  (case1 : ∀ …, motive1 x y  →  …) → … →
  ((x : a) → (y : b) → motive1 x y) ∧ ((z : c) → motive2 z)

where all the PSum/PSigma encoding has been resolved. This theorem is attached to the name of the first function in the mutual group, like the ._unary definition.

Finally, in deriveUnpackedInduction, for each of the funtions in the mutual group, a simple projection yields the final foo.induct theorem:

foo.induct : {motive1 : a → b → Prop} {motive2 : c → Prop} →
  (case1 : ∀ …, motive1 x y  →  …) → … →
  (x : a) → (y : b) → motive1 x y

Implementation overview (structural recursion) #

When handling structural recursion, the overall approach is the same, with the following differences:

Instead of WellFounded.fix we look for a .brecOn application, using isBRecOnRecursor

Despite its name, this function does not recognize the .brecOn of inductive predicates, which we also do not support at this point.

Since (for now) we only support Prop in the induction principle, we rewrite to .binductionOn.
The elaboration of structurally recursive function can handle extra arguments. We keep the motive parameters in the original order.