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 formdef 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 in)buildInductionBody
, 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
- 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 freshMVar
asserts the current goal, unwanted values from the local context are cleared, and the currentbody
is searched for recursive calls usingcollectIHs
, which are then asserted as inductive hyptheses in theMVar
.The function
collectIHs
walks the term and collects the induction hypotheses for the current case (with proofs). When it encounters a saturated application ofoldIH x proof
, it returnsnewIH x proof : motive x
.Since
x
andproof
can contain further recursive calls, it usesfoldCalls
to replace these with calls tofoo
. This assumes that the termination proofproof
works nevertheless.Again,
collectIHs
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 auxillary lemmas are unfolded if needed.The function
foldCalls
replaces calls tooldIH
with calls tofoo
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, 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.The “induction hyothesis” in a
.brecOn
call is abelow x
term that contains all the possible recursive calls, whic are projected out using.fst.snd.…
. Theis_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 argumentm
of the nested callih.fst.snd acc
. To do so reliably, we replace theih
with the “newih
”, which will have typemotive m acc
, and sincemotive
is a FVar we can then read off the arguments off this nicely.There exist inductive types where the
.brecOn
only supports motives producingType u
, but notSort u
, but our induction principles produceProp
. We recognize this case and, rather hazardously, replace.brecOn
with.binductionOn
(and thus.below
with.ibelow
andPProd
withAnd
). This assumes that these definitions are highly analogous.
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
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
Structural recursion only:
Recognizes oldIH.fst.snd a₁ a₂
and returns newIH.fst.snd
.
Possibly switching from PProd.fst
to And.left
if needed
Structural recursion only:
Recognizes oldIH.fst.snd a₁ a₂
and returns newIH.fst.snd
and #[a₁, a₂]
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Replace calls to oldIH back to calls to the original function. At the end, if oldIH
occurs, an
error is thrown.
The newIH
will not show up in the output of foldCalls
, we use it as a helper to infer the
argument of nested recursive calls when we have structural recursion.
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
Substitutes equations, but makes sure to only substitute variables introduced after the motive
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
Helper monad to traverse the function body, collecting the cases as mvars
Equations
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 discriminans 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
- collects all these meta-variables,
- lifts them to the current context by reverting all local declarations up to
x
- 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 assignemnts correctly.
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
This function looks that the body of a recursive function and looks for either users of
fix
, fixF
or a .brecOn
, and abstracts over the differences between them. It passes
to the continuation
- whether we are using well-founded recursion
- the fixed parameters of the function body
- the varying parameters of the function body (this includes both the targets of the recursion and extra parameters passed to the recursor)
- the position of the motive/induction hypothesis in the body's arguments
- the body, as passed to the recursor. Expected to be a lambda that takes the varying paramters and the motive
- a function to re-assemble the call with a new Motive. The resulting expression expects the new body next, so that the expected type of the body can be inferred
- a function to finish assembling the call with the new body.
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
Given a 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
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 wrapsvalue
in an appropriate type hint.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Takes an induction principle 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
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.