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 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 …`

)

- the matcher is replaced by its splitter, which brings extra assumptions into scope when
patterns are overlapping (using
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 auxiliary 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 functions 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.

Opens the body of a lambda, *without* putting the free variable into the local context.
This is used when replacing parameters with different expressions.
This way it will not be picked up by metavariables.

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

A monad to help collecting inductive hypothesis.

In `foldAndCollect`

it's a writer monad (with variants of the `local`

combinator),
and in `buildInductionBody`

it is more of a reader monad, with inductive hypotheses
being passed down (hence the `ask`

and `branch`

combinator).

## Equations

## Instances For

## Equations

- act.run = StateT.run act #[]

## Instances For

## Instances For

## Instances For

## Equations

- Lean.Tactic.FunInd.M.tell x xs = pure ((), xs.push x)

## Instances For

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

## Equations

- Lean.Tactic.FunInd.M.localMapM f act = Lean.Tactic.FunInd.M.localM (fun (x : Array Lean.Expr) => Array.mapM f x) act

## Instances For

## Equations

## Instances For

## Equations

- act.branch = Lean.Tactic.FunInd.M.localM (fun (x : Array Lean.Expr) => pure #[]) act

## Instances For

The `foldAndCollect`

function performs two operations together:

- it fold recursive calls: applications (and projectsions) of
`oldIH`

in`e`

correspond to recursive calls, so this function rewrites that back to recursive calls - it collects induction hypotheses: after replacing
`oldIH`

with`newIH`

, applications thereof are valuable as induction hypotheses for the cases.

For well-founded recursion (unary, non-mutual by construction) the terms are rather simple: they
are `oldIH arg proof`

, and can be rewritten to `f arg`

resp. `newIH arg proof`

. But for
structural recursion this can be a more complicted mix of function applications (due to reflexive
data types or extra function arguments) and `PProd`

projections (due to the below construction and
mutual function packing), and the main function argument isn't even present.

To avoid having to think about this, we apply a nice trick:

We compositionally replace `oldIH`

with `newIH`

. This likely changes the result type, so when
re-assembling we have to be supple (mainly around `PProd.fst`

/`PProd.snd`

). As we re-assemble
the term we check if it has type `motive xs..`

. If it has, then know we have just found and
rewritten a recursive call, and this type nicely provides us the arguments `xs`

. So at this point
we store the rewritten expression as a new induction hypothesis (using `M.tell`

) and rewrite to
`f xs..`

, which now again has the same type as the original term, and the further re-assembly should
work. Half this logic is in the `isRecCall`

parameter.

If this process fails we’ll get weird type errors (caught later on). We'll see if we need to
improve the errors, for example by passing down a flag whether we expect the same type (and no
occurrences of `newIH`

), or whether we are in “supple mode”, and catch it earlier if the rewriting
fails.

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

Goal cleanup:
Substitutes equations (with `substVar`

) to remove superfluous variables, and clears unused
let bindings.

Substitutes from the outside in so that the inner-bound variable name wins, but does a first pass looking only at variables with names with macro scope, so that preferably they disappear.

Careful to only touch the context after the motives (given by the index) as the motive could depend
on anything before, and `substVar`

would happily drop equations about these fixed parameters.

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

Second helper monad collecting the cases as mvars

## Equations

## Instances For

## Equations

- act.run = (StateT.run act #[]).eval

## Instances For

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

Base case of `buildInductionBody`

: Construct a case for the final induction hypthesis.

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

Like `mkLambdaFVars (usedOnly := true)`

, but

- silently skips expression in
`xs`

that are not`.isFVar`

- returns a mask (same size as
`xs`

) indicating which variables have been abstracted (`true`

means was abstracted).

The result `r`

can be applied with `r.beta (maskArray mask args)`

.

We use this when generating the functional induction principle to refine the goal through a `match`

,
here `xs`

are the discriminants of the `match`

.
We do not expect non-trivial discriminants to appear in the goal (and if they do, the user will
get a helpful equality into the context).

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

Builds an expression of type `goal`

by replicating the expression `e`

into its tail-call-positions,
where it calls `buildInductionCase`

. Collects the cases of the final induction hypothesis
as `MVars`

as it goes.

Given an expression `e`

with metavariables `mvars`

- performs more cleanup:
- removes unused let-expressions after index
`index`

- tries to substitute variables after index
`index`

- removes unused let-expressions after index
- lifts them to the current context by reverting all local declarations after index
`index`

- introducing a local variable for each of the meta variable
- assigning that local variable to the mvar
- and finally lambda-abstracting over these new local variables.

This operation only works if the metavariables are independent from each other.

The resulting meta variable assignment is no longer valid (mentions out-of-scope variables), so after this operations, terms that still mention these meta variables must not be used anymore.

We are not using `mkLambdaFVars`

on mvars directly, nor `abstractMVars`

, as these at the moment
do not handle delayed assignments correctly.

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

Given a unary definition `foo`

defined via `WellFounded.fixF`

, derive a suitable induction principle
`foo.induct`

for it. See module doc for details.

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

Given `foo.mutual_induct`

, defined `foo.induct`

, `bar.induct`

etc.
Used for well-founded and structural recursion.

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

In the type of `value`

, reduces

- Beta-redexes
`PSigma.casesOn (PSigma.mk a b) (fun x y => k x y) --> k a b`

`PSum.casesOn (PSum.inl x) k₁ k₂ --> k₁ x`

`foo._unary (PSum.inl (PSigma.mk a b)) --> foo a b`

and then wraps`value`

in an appropriate type hint.

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

Takes `foo._unary.induct`

, where the motive is a `PSigma`

/`PSum`

type and
unpacks it into a n-ary and (possibly) joint induction principle.

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

Given `foo._unary.induct`

, define `foo.mutual_induct`

and then `foo.induct`

, `bar.induct`

, …

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

## Equations

## Instances For

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

Given a recursive definition `foo`

defined via structural recursion, derive `foo.mutual_induct`

,
if needed, and `foo.induct`

for all functions in the group.
See module doc for details.

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

Given a recursively defined function `foo`

, derives `foo.induct`

. See the module doc for details.

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

## Equations

- One or more equations did not get rendered due to their size.
- Lean.Tactic.FunInd.isFunInductName env (indName.str str) = (pure false).run
- Lean.Tactic.FunInd.isFunInductName env name = (pure false).run