Documentation

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 : NatNatNat
  | 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 : NatNat → 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

  1. 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.

  2. 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])
    
  3. 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 …)
  4. 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.

  5. 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.

  6. 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:

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
    @[reducible, inline]

    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
      Instances For
        Equations
        • act.eval = do let __do_liftact.run pure __do_lift.fst
        Instances For
          Equations
          • act.exec = do let __do_liftact.run pure __do_lift.snd
          Instances For
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              Equations
              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
                      partial def Lean.Tactic.FunInd.cleanupAfter.go (mvarId : Lean.MVarId) (index : Nat) (firstPass : Bool) :
                      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
                          @[reducible, inline]

                          Second helper monad collecting the cases as mvars

                          Equations
                          Instances For
                            Equations
                            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
                                    def Lean.Tactic.FunInd.maskArray {α : Type u_1} (mask : Array Bool) (xs : Array α) :

                                    maskArray mask xs keeps those x where the corresponding entry in mask is true

                                    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
                                      • 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
                                                  • One or more equations did not get rendered due to their size.
                                                  Instances For
                                                    @[irreducible]
                                                    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
                                                          Instances For