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

  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
    • 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 …)
  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 collectIHs, which are then asserted as inductive hyptheses in the MVar.

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

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

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

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

    PProd.fst or And.left

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For

      PProd.snd or And.right

      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
          partial def Lean.Tactic.FunInd.foldCalls (is_wf : Bool) (fn : Lean.Expr) (oldIH : Lean.FVarId) (newIH : Lean.FVarId) (e : Lean.Expr) :

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

                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
                      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
                        partial def Lean.Tactic.FunInd.buildInductionBody (is_wf : Bool) (fn : Lean.Expr) (toClear : Array Lean.FVarId) (toPreserve : Array Lean.FVarId) (goal : Lean.Expr) (oldIH : Lean.FVarId) (newIH : Lean.FVarId) (IHs : Array Lean.Expr) (e : Lean.Expr) :

                        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 wraps value 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.
                                          Instances For