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 andy
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 inbuildInductionBody
) mirrors the branching structure offoo
, i.e. replicatesdite
and some matcher applications, while adjusting their motive. It also unfolds calls tooldIH
and collects induction hypotheses in conditions (see below).In particular, when translating a
match
it is prepared to recognize the idiom as introduced bymkFix
viaLean.Meta.MatcherApp.addArg?
, which refines the type ofoldIH
throughout the match. The transformation will replaceoldIH
withnewIH
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 …
) - also, simple discriminants (
FVars
) are remembered astoClear
, as they are unlikely to provide useful context, and are redundant given the context that comes from the pattern match.
- 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 freshMVar
asserts the current goal, unwanted values from the local context are cleared, and the currentbody
is searched for recursive calls usingfoldAndCollect
, which are then asserted as inductive hypotheses in theMVar
.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
andproof
can contain further recursive calls, they are folded there as well. This assumes that the termination proofproof
works nevertheless.Again,
foldAndCollect
may encounter theLean.Meta.Matcherapp.addArg?
idiom, and again it threadsnewIH
through, replacing the extra argument. The resulting type of this induction hypothesis is now itself amatch
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, usingisBRecOnRecursor
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.
Unfolding principles #
The code can also create a variant of the induction/cases principles that automatically unfolds the function application. It's motive abstracts over the function call, so for the ackermann function one gets
ackermann.fun_cases_unfolding
(motive : Nat → Nat → Nat → Prop)
(case1 : ∀ (m : Nat), motive 0 m (m + 1))
(case2 : ∀ (n : Nat), motive n.succ 0 (ackermann n 1))
(case3 : ∀ (n m : Nat), motive n.succ m.succ (ackermann n (ackermann (n + 1) m)))
(x✝ x✝¹ : Nat) : motive x✝ x✝¹ (ackermann x✝ x✝¹)
To implement this, in the initial goal motive x (ackermann x)
of buildInductionBody
we unfold the
function definition, and then reduce is as we go into match, ite or let expressions, using the
withRewrittenMotive
function.
This gives us great control over the reduction, for example to move let
expressions to the context
simultaneously.
The combinators passed to withRewrittenMotive
are forgiving, so when unfolding := false
, or when
something goes wrong, one still gets a useful induction principle, just maybe with the function
not fully simplified.
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.