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, possibly after some whnf’ing, 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
- simple discriminants that are mentioned in the goal (i.e plain parameters) are instantiated in the code.
- 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 collectIHs, which are then asserted as inductive hyptheses in the MVar.
The function collectIHs walks the term and collects the induction hypotheses for the current case (with proofs). When it encounters a saturated application of oldIH x proof, it returns newIH x proof : motive x.

Since x and proof can contain further recursive calls, it uses foldCalls to replace these with calls to foo. This assumes that the termination proof proof works nevertheless.

Again, collectIHs 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.
The function foldCalls replaces calls to oldIH with calls to foo that make sense to the user.

At the end of this transformation, no mention of oldIH must remain.
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.
The elaboration of structurally recursive function can handle extra arguments. We keep the motive parameters in the original order.
The “induction hyothesis” in a .brecOn call is a below x term that contains all the possible recursive calls, whic are projected out using .fst.snd.…. The is_wf flag that we pass down tells us which form of induction hypothesis we are looking for.
If we have nested recursion (foo n (foo m acc))), then we need to infer the argument m of the nested call ih.fst.snd acc. To do so reliably, we replace the ih with the “new ih”, which will have type motive m acc, and since motive is a FVar we can then read off the arguments off this nicely.
There exist inductive types where the .brecOn only supports motives producing Type u, but not Sort u, but our induction principles produce Prop. We recognize this case and, rather hazardously, replace .brecOn with .binductionOn (and thus .below with .ibelow and PProd with And). This assumes that these definitions are highly analogous.