Documentation

Lean.Elab.PreDefinition.WF.GuessLex

This module finds lexicographic termination measures for well-founded recursion.

Starting with basic measures (sizeOf xᵢ for all parameters xᵢ), and complex measures (e.g. e₂ - e₁ if e₁ < e₂ is found in the context of a recursive call) it tries all combinations until it finds one where all proof obligations go through with the given tactic (decerasing_by), if given, or the default decreasing_tactic.

For mutual recursion, a single measure is not just one parameter, but one from each recursive function. Enumerating these can lead to a combinatoric explosion, so we bound the number of measures tried.

In addition to measures derived from sizeOf xᵢ, it also considers measures that assign an order to the functions themselves. This way we can support mutual function definitions where no arguments decrease from one function to another.

The result of this module is a TerminationWF, which is then passed on to wfRecursion; this design is crucial so that whatever we infer in this module could also be written manually by the user. It would be bad if there are function definitions that can only be processed with the guessed lexicographic order.

The following optimizations are applied to make this feasible:

  1. The crucial optimization is to look at each measure of each recursive call once, try to prove < and (if that fails ), and then look at that table to pick a suitable measure.

  2. The next-crucial optimization is to fill that table lazily. This way, we run the (likely expensive) tactics as few times as possible, while still being able to consider a possibly large number of combinations.

  3. Before we even try to prove <, we check if the measures are equal (=). No well-founded measure will relate equal terms, likely this check is faster than firing up the tactic engine, and it adds more signal to the output.

  4. Instead of traversing the whole function body over and over, we traverse it once and store the arguments (in unpacked form) and the local MetaM state at each recursive call (see collectRecCalls), which we then re-use for the possibly many proof attempts.

The logic here is based on “Finding Lexicographic Orders for Termination Proofs in Isabelle/HOL” by Lukas Bulwahn, Alexander Krauss, and Tobias Nipkow, 10.1007/978-3-540-74591-4_5 https://www21.in.tum.de/~nipkow/pubs/tphols07.pdf.

We got the idea of considering the measure e₂ - e₁ if we see e₁ < e₂ from “Termination Analysis with Calling Context Graphs” by Panagiotis Manolios & Daron Vroon, https://doi.org/10.1007/11817963_36.

Given a predefinition, return the variable names in the outermost lambdas. Includes the “fixed prefix”.

The length of the returned array is also used to determine the arity of the function, so it should match what packDomain does.

Equations
    Instances For

      Given the original parameter names from originalVarNames, find good variable names to be used when talking about termination measures: Use user-given parameter names if present; use x1...xn otherwise.

      The names ought to accessible (no macro scopes) and fresh wrt to the current environment, so that with showInferredTerminationBy we can print them to the user reliably. We do that by appending ' as needed.

      It is possible (but unlikely without malice) that some of the user-given names shadow each other, and the guessed relation refers to the wrong one. In that case, the user gets to keep both pieces (and may have to rename variables).

      Equations
        Instances For

          A termination measure with extra fields for use within GuessLex

          Instances For

            String description of this measure

            Equations
              Instances For

                Determine if the measure for parameter x should be sizeOf x or just x.

                For non-mutual definitions, we omit sizeOf when the measure does not depend on the other varying parameters, and its WellFoundedRelation instance goes via SizeOf.

                For mutual definitions, we omit sizeOf only when the measure is (at reducible transparency!) of type Nat (else we'd have to worry about differently-typed measures from different functions to line up).

                Equations
                  Instances For
                    def Lean.Elab.WF.GuessLex.withUserNames {α : Type} (xs : Array Expr) (ns : Array Name) (k : MetaM α) :

                    Sets the user names for the given freevars in xs.

                    Equations
                      Instances For

                        Create one measure for each (eligible) parameter of the given predefintion.

                        Equations
                          Instances For
                            @[reducible, inline]
                            abbrev Lean.Elab.WF.GuessLex.M (recFnName : Name) (α β : Type) :

                            Internal monad used by withRecApps

                            Equations
                              Instances For
                                def Lean.Elab.WF.GuessLex.withRecApps {α : Type} (recFnName : Name) (fixedPrefixSize : Nat) (param e : Expr) (k : ExprArray ExprMetaM α) :

                                Traverses the given expression e, and invokes the continuation k at every saturated call to recFnName.

                                The expression param is passed along, and refined when going under a matcher or casesOn application.

                                Equations
                                  Instances For
                                    partial def Lean.Elab.WF.GuessLex.withRecApps.processRec {α : Type} (recFnName : Name) (fixedPrefixSize : Nat) (k : ExprArray ExprMetaM α) (param e : Expr) :
                                    M recFnName α Unit
                                    partial def Lean.Elab.WF.GuessLex.withRecApps.processApp {α : Type} (recFnName : Name) (fixedPrefixSize : Nat) (k : ExprArray ExprMetaM α) (param e : Expr) :
                                    M recFnName α Unit
                                    def Lean.Elab.WF.GuessLex.withRecApps.containsRecFn {α : Type} (recFnName : Name) (e : Expr) :
                                    M recFnName α Bool
                                    Equations
                                      Instances For
                                        partial def Lean.Elab.WF.GuessLex.withRecApps.loop {α : Type} (recFnName : Name) (fixedPrefixSize : Nat) (k : ExprArray ExprMetaM α) (param e : Expr) :
                                        M recFnName α Unit

                                        A SavedLocalContext captures the state and local context of a MetaM, to be continued later.

                                        Instances For

                                          Capture the MetaM state including local context.

                                          Equations
                                            Instances For

                                              Run a MetaM action in the saved state.

                                              Equations
                                                Instances For

                                                  A RecCallWithContext focuses on a single recursive call in a unary predefinition, and runs the given action in the context of that call.

                                                  • ref : Syntax

                                                    Syntax location of recursive call

                                                  • caller : Nat

                                                    Function index of caller

                                                  • params : Array Expr

                                                    Parameters of caller (including fixed prefix)

                                                  • callee : Nat

                                                    Function index of callee

                                                  • args : Array Expr

                                                    Arguments to callee (including fixed prefix)

                                                  Instances For

                                                    Store the current recursive call and its context.

                                                    Equations
                                                      Instances For

                                                        The elaborator is prone to duplicate terms, including recursive calls, even if the user only wrote a single one. This duplication is wasteful if we run the tactics on duplicated calls, and confusing in the output of GuessLex. So prune the list of recursive calls, and remove those where another call exists that has the same goal and context that is no more specific.

                                                        Equations
                                                          Instances For

                                                            Traverse a unary PreDefinition, and returns a WithRecCall closure for each recursive call site.

                                                            Equations
                                                              Instances For

                                                                Is the expression a <-like comparison of Nat expressions

                                                                Equations
                                                                  Instances For

                                                                    A GuessLexRel described how a recursive call affects a measure; whether it decreases strictly, non-strictly, is equal, or else.

                                                                    Instances For

                                                                      Given a GuessLexRel, produce a binary Expr that relates two Nat values accordingly.

                                                                      Equations
                                                                        Instances For
                                                                          def Lean.Elab.WF.GuessLex.evalRecCall (callerName : Name) (decrTactic? : Option DecreasingBy) (callerMeasures calleeMeasures : Array BasicMeasure) (rcc : RecCallWithContext) (callerMeasureIdx calleeMeasureIdx : Nat) :

                                                                          For a given recursive call, and a choice of parameter and argument index, try to prove equality, < or ≤.

                                                                          Equations
                                                                            Instances For
                                                                              Instances For

                                                                                Create a cache to memoize calls to evalRecCall descTactic? rcc

                                                                                Equations
                                                                                  Instances For
                                                                                    def Lean.Elab.WF.GuessLex.RecCallCache.eval (rc : RecCallCache) (callerMeasureIdx calleeMeasureIdx : Nat) :

                                                                                    Run evalRecCall and cache there result

                                                                                    Equations
                                                                                      Instances For
                                                                                        def Lean.Elab.WF.GuessLex.RecCallCache.prettyEntry (rcc : RecCallCache) (callerMeasureIdx calleeMeasureIdx : Nat) :

                                                                                        Print a single cache entry as a string, without forcing it

                                                                                        Equations
                                                                                          Instances For

                                                                                            The measures that we order lexicographically can be comparing basic measures, or numbering the functions

                                                                                            Instances For

                                                                                              Evaluate a recursive call at a given MutualMeasure

                                                                                              Equations
                                                                                                Instances For
                                                                                                  def Lean.Elab.WF.GuessLex.generateCombinations? (numMeasures : Array Nat) (threshold : Nat := 32) :

                                                                                                  Generate all combination of measures. Assumes we have numbered the measures of each function, and their counts is in numMeasures.

                                                                                                  This puts the uniform combinations ([0,0,0], [1,1,1]) to the front; they are commonly most useful to try first, when the mutually recursive functions have similar argument structures

                                                                                                  Equations
                                                                                                    Instances For
                                                                                                      partial def Lean.Elab.WF.GuessLex.generateCombinations?.go (numMeasures : Array Nat) (threshold : Nat := 32) (fidx : Nat) :

                                                                                                      Enumerate all measures we want to try.

                                                                                                      All measures (resp. combinations thereof) and possible orderings of functions (if more than one)

                                                                                                      Equations
                                                                                                        Instances For
                                                                                                          def Lean.Elab.WF.GuessLex.solve {m : TypeType} {α : Type} [Monad m] (measures : Array α) (calls : Array (αm GuessLexRel)) :
                                                                                                          m (Option (Array α))

                                                                                                          The core logic of guessing the lexicographic order Given a matrix that for each call and measure indicates whether that measure is decreasing, equal, less-or-equal or unknown, It finds a sequence of measures that is lexicographically decreasing.

                                                                                                          The matrix is implemented here as an array of monadic query methods only so that we can fill is lazily. Morally, this is a pure function

                                                                                                          Equations
                                                                                                            Instances For
                                                                                                              partial def Lean.Elab.WF.GuessLex.solve.go {m : TypeType} {α : Type} [Monad m] (measures : Array α) (calls : Array (αm GuessLexRel)) (acc : Array α) :
                                                                                                              m (Option (Array α))

                                                                                                              Given a matrix (row-major) of strings, arranges them in tabular form. First column is left-aligned, others right-aligned. Single space as column separator.

                                                                                                              Equations
                                                                                                                Instances For

                                                                                                                  Concise textual representation of the source location of a recursive call

                                                                                                                  Equations
                                                                                                                    Instances For

                                                                                                                      How to present the basic measure in the table header, possibly abbreviated.

                                                                                                                      Equations
                                                                                                                        Instances For
                                                                                                                          Equations
                                                                                                                            Instances For

                                                                                                                              Explain what we found out about the recursive calls (non-mutual case)

                                                                                                                              Equations
                                                                                                                                Instances For

                                                                                                                                  Explain what we found out about the recursive calls (mutual case)

                                                                                                                                  Equations
                                                                                                                                    Instances For
                                                                                                                                      Equations
                                                                                                                                        Instances For

                                                                                                                                          For #[x₁, .., xₙ] create (x₁, .., xₙ).

                                                                                                                                          Equations
                                                                                                                                            Instances For
                                                                                                                                              Equations
                                                                                                                                                Instances For

                                                                                                                                                  Shows the inferred termination measure to the user, and implements termination_by?

                                                                                                                                                  Equations
                                                                                                                                                    Instances For
                                                                                                                                                      def Lean.Elab.WF.guessLex (preDefs : Array PreDefinition) (unaryPreDef : PreDefinition) (fixedParamPerms : FixedParamPerms) (argsPacker : Meta.ArgsPacker) :

                                                                                                                                                      Main entry point of this module:

                                                                                                                                                      Try to find a lexicographic ordering of the basic measures for which the recursive definition terminates. See the module doc string for a high-level overview.

                                                                                                                                                      The preDefs are used to determine arity and types of parameters; the bodies are ignored.

                                                                                                                                                      Equations
                                                                                                                                                        Instances For