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

Starting with basic measures (sizeOf xᵢ for all parameters xᵢ), 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 nubmer 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 optimiziation is to look at each argument 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 arguments 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 .

opaque Lean.Elab.WF.GuessLex.showInferredTerminationBy : Lean.Option Bool

def Lean.Elab.WF.GuessLex.originalVarNames (preDef : Lean.Elab.PreDefinition) : Lean.MetaM (Array Lake.Name)

Given a predefinition, return the variabe 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

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

def Lean.Elab.WF.GuessLex.naryVarNames (fixedPrefixSize : Nat) (xs : Array Lake.Name) : Lean.MetaM (Array Lake.Name)

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

The names ought to accessible (no macro scopes) and new names 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

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

partial def Lean.Elab.WF.GuessLex.naryVarNames.freshen (ns : Array Lake.Name) (n : Lake.Name) : Lean.MetaM Lake.Name

@[inline, reducible]

abbrev Lean.Elab.WF.GuessLex.M (recFnName : Lake.Name) (α : Type) (β : Type) : Type

Internal monad used by withRecApps

Equations

• Lean.Elab.WF.GuessLex.M recFnName α β = StateRefT' IO.RealWorld (Array α) (StateRefT' IO.RealWorld (Lean.HasConstCache recFnName) Lean.MetaM) β

def Lean.Elab.WF.GuessLex.withRecApps {α : Type} (recFnName : Lake.Name) (fixedPrefixSize : Nat) (param : Lean.Expr) (e : Lean.Expr) (k : Lean.Expr → Array Lean.Expr → Lean.MetaM α) : Lean.MetaM (Array α)

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

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

partial def Lean.Elab.WF.GuessLex.withRecApps.processRec {α : Type} (recFnName : Lake.Name) (fixedPrefixSize : Nat) (k : Lean.Expr → Array Lean.Expr → Lean.MetaM α) (param : Lean.Expr) (e : Lean.Expr) : Lean.Elab.WF.GuessLex.M recFnName α Unit

partial def Lean.Elab.WF.GuessLex.withRecApps.processApp {α : Type} (recFnName : Lake.Name) (fixedPrefixSize : Nat) (k : Lean.Expr → Array Lean.Expr → Lean.MetaM α) (param : Lean.Expr) (e : Lean.Expr) : Lean.Elab.WF.GuessLex.M recFnName α Unit

def Lean.Elab.WF.GuessLex.withRecApps.containsRecFn {α : Type} (recFnName : Lake.Name) (e : Lean.Expr) : Lean.Elab.WF.GuessLex.M recFnName α Bool

Equations

• Lean.Elab.WF.GuessLex.withRecApps.containsRecFn recFnName e = modifyGetThe (Lean.HasConstCache recFnName) fun (x : Lean.HasConstCache recFnName) => Lean.HasConstCache.contains e x

partial def Lean.Elab.WF.GuessLex.withRecApps.loop {α : Type} (recFnName : Lake.Name) (fixedPrefixSize : Nat) (k : Lean.Expr → Array Lean.Expr → Lean.MetaM α) (param : Lean.Expr) (e : Lean.Expr) : Lean.Elab.WF.GuessLex.M recFnName α Unit

structure Lean.Elab.WF.GuessLex.SavedLocalContext : Type

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

• savedLocalContext : Lean.LocalContext
• savedLocalInstances : Lean.LocalInstances
• savedState : Lean.Meta.SavedState

def Lean.Elab.WF.GuessLex.SavedLocalContext.create : Lean.MetaM Lean.Elab.WF.GuessLex.SavedLocalContext

Capture the MetaM state including local context.

Equations

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

def Lean.Elab.WF.GuessLex.SavedLocalContext.run {α : Type} (slc : Lean.Elab.WF.GuessLex.SavedLocalContext) (k : Lean.MetaM α) : Lean.MetaM α

Run a MetaM action in the saved state.

Equations

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

structure Lean.Elab.WF.GuessLex.RecCallWithContext : Type

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

• ref : Lean.Syntax

  Syntax location of recursive call

• caller : Nat

  Function index of caller

• params : Array Lean.Expr

  Parameters of caller

• callee : Nat

  Function index of callee

• args : Array Lean.Expr

  Arguments to callee

• ctxt : Lean.Elab.WF.GuessLex.SavedLocalContext

def Lean.Elab.WF.GuessLex.RecCallWithContext.create (ref : Lean.Syntax) (caller : Nat) (params : Array Lean.Expr) (callee : Nat) (args : Array Lean.Expr) : Lean.MetaM Lean.Elab.WF.GuessLex.RecCallWithContext

Store the current recursive call and its context.

Equations

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

def Lean.Elab.WF.GuessLex.filterSubsumed (rcs : Array Lean.Elab.WF.GuessLex.RecCallWithContext) : Array Lean.Elab.WF.GuessLex.RecCallWithContext

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

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

def Lean.Elab.WF.GuessLex.collectRecCalls (unaryPreDef : Lean.Elab.PreDefinition) (fixedPrefixSize : Nat) (arities : Array Nat) : Lean.MetaM (Array Lean.Elab.WF.GuessLex.RecCallWithContext)

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

Equations

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

inductive Lean.Elab.WF.GuessLex.GuessLexRel : Type

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

• lt: Lean.Elab.WF.GuessLex.GuessLexRel
• eq: Lean.Elab.WF.GuessLex.GuessLexRel
• le: Lean.Elab.WF.GuessLex.GuessLexRel
• no_idea: Lean.Elab.WF.GuessLex.GuessLexRel

instance Lean.Elab.WF.GuessLex.instReprGuessLexRel : Repr Lean.Elab.WF.GuessLex.GuessLexRel

Equations

• Lean.Elab.WF.GuessLex.instReprGuessLexRel = { reprPrec := Lean.Elab.WF.GuessLex.reprGuessLexRel✝ }

instance Lean.Elab.WF.GuessLex.instDecidableEqGuessLexRel : DecidableEq Lean.Elab.WF.GuessLex.GuessLexRel

Equations

• Lean.Elab.WF.GuessLex.instDecidableEqGuessLexRel x y = if h : Lean.Elab.WF.GuessLex.GuessLexRel.toCtorIdx x = Lean.Elab.WF.GuessLex.GuessLexRel.toCtorIdx y then isTrue ⋯ else isFalse ⋯

instance Lean.Elab.WF.GuessLex.instToStringGuessLexRel : ToString Lean.Elab.WF.GuessLex.GuessLexRel

Equations

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

instance Lean.Elab.WF.GuessLex.instToFormatGuessLexRel : Lean.ToFormat Lean.Elab.WF.GuessLex.GuessLexRel

Equations

• Lean.Elab.WF.GuessLex.instToFormatGuessLexRel = { format := fun (r : Lean.Elab.WF.GuessLex.GuessLexRel) => Std.Format.text (toString r) }

def Lean.Elab.WF.GuessLex.GuessLexRel.toNatRel : Lean.Elab.WF.GuessLex.GuessLexRel → Lean.Expr

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

Equations

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

def Lean.Elab.WF.GuessLex.mkSizeOf (e : Lean.Expr) : Lean.MetaM Lean.Expr

Given an expression e, produce sizeOf e with a suitable instance.

Equations

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

def Lean.Elab.WF.GuessLex.evalRecCall (decrTactic? : Option Lean.Elab.WF.DecreasingBy) (rcc : Lean.Elab.WF.GuessLex.RecCallWithContext) (paramIdx : Nat) (argIdx : Nat) : Lean.MetaM Lean.Elab.WF.GuessLex.GuessLexRel

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

Equations

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

structure Lean.Elab.WF.GuessLex.RecCallCache : Type

• mk'' :: (
• decrTactic? : Option Lean.Elab.WF.DecreasingBy
• rcc : Lean.Elab.WF.GuessLex.RecCallWithContext
• cache : IO.Ref (Array (Array (Option Lean.Elab.WF.GuessLex.GuessLexRel)))
• )

def Lean.Elab.WF.GuessLex.RecCallCache.mk (decrTactics : Array (Option Lean.Elab.WF.DecreasingBy)) (rcc : Lean.Elab.WF.GuessLex.RecCallWithContext) : BaseIO Lean.Elab.WF.GuessLex.RecCallCache

Create a cache to memoize calls to evalRecCall descTactic? rcc

Equations

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

def Lean.Elab.WF.GuessLex.RecCallCache.eval (rc : Lean.Elab.WF.GuessLex.RecCallCache) (paramIdx : Nat) (argIdx : Nat) : Lean.MetaM Lean.Elab.WF.GuessLex.GuessLexRel

Run evalRecCall and cache there result

Equations

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

def Lean.Elab.WF.GuessLex.RecCallCache.prettyEntry (rcc : Lean.Elab.WF.GuessLex.RecCallCache) (paramIdx : Nat) (argIdx : Nat) : Lean.MetaM String

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

Equations

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

inductive Lean.Elab.WF.GuessLex.MutualMeasure : Type

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

• args: Array Nat → Lean.Elab.WF.GuessLex.MutualMeasure

  For every function, the given argument index

• func: Nat → Lean.Elab.WF.GuessLex.MutualMeasure

  The given function index is assigned 1, the rest 0

def Lean.Elab.WF.GuessLex.inspectCall (rc : Lean.Elab.WF.GuessLex.RecCallCache) : Lean.Elab.WF.GuessLex.MutualMeasure → Lean.MetaM Lean.Elab.WF.GuessLex.GuessLexRel

Evaluate a recursive call at a given MutualMeasure

Equations

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

def Lean.Elab.WF.GuessLex.getForbiddenByTrivialSizeOf (fixedPrefixSize : Nat) (preDef : Lean.Elab.PreDefinition) : Lean.MetaM (Array Nat)

Given a predefinition with value fun (x_₁ ... xₙ) (y_₁ : α₁)... (yₘ : αₘ) => ..., where n = fixedPrefixSize, return an array A s.t. i ∈ A iff sizeOf yᵢ reduces to a literal. This is the case for types such as Prop, Type u, etc. These arguments should not be considered when guessing a well-founded relation. See generateCombinations?

Equations

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

def Lean.Elab.WF.GuessLex.generateCombinations? (forbiddenArgs : Array (Array Nat)) (numArgs : Array Nat) (threshold : optParam Nat 32) : Option (Array (Array Nat))

Generate all combination of arguments, skipping those that are forbidden.

Sorts 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

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

def Lean.Elab.WF.GuessLex.generateCombinations?.isForbidden (forbiddenArgs : Array (Array Nat)) (fidx : Nat) (argIdx : Nat) : Bool

Equations

• Lean.Elab.WF.GuessLex.generateCombinations?.isForbidden forbiddenArgs fidx argIdx = if h : fidx < Array.size forbiddenArgs then Array.contains forbiddenArgs[fidx] argIdx else false

partial def Lean.Elab.WF.GuessLex.generateCombinations?.goUniform (forbiddenArgs : Array (Array Nat)) (numArgs : Array Nat) (argIdx : Nat) : OptionT (StateM (Array (Array Nat))) Unit

partial def Lean.Elab.WF.GuessLex.generateCombinations?.go (forbiddenArgs : Array (Array Nat)) (numArgs : Array Nat) (threshold : optParam Nat 32) (fidx : Nat) : OptionT (ReaderT (Array Nat) (StateM (Array (Array Nat)))) Unit

def Lean.Elab.WF.GuessLex.generateMeasures (forbiddenArgs : Array (Array Nat)) (arities : Array Nat) : Lean.MetaM (Array Lean.Elab.WF.GuessLex.MutualMeasure)

Enumerate all meausures we want to try: All arguments (resp. combinations thereof) and possible orderings of functions (if more than one)

Equations

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

def Lean.Elab.WF.GuessLex.solve {m : Type → Type} {α : Type} [Monad m] (measures : Array α) (calls : Array (α → m Lean.Elab.WF.GuessLex.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

• Lean.Elab.WF.GuessLex.solve measures calls = Lean.Elab.WF.GuessLex.solve.go measures calls #[]

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

def Lean.Elab.WF.GuessLex.mkTupleSyntax : Array Lean.Term → Lean.MetaM Lean.Term

Create Tuple syntax (() if the array is empty, and just the value if its a singleton)

Equations

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

def Lean.Elab.WF.GuessLex.buildTermWF (originalVarNamess : Array (Array Lake.Name)) (varNamess : Array (Array Lake.Name)) (measures : Array Lean.Elab.WF.GuessLex.MutualMeasure) : Lean.MetaM Lean.Elab.WF.TerminationWF

Given an array of MutualMeasures, creates a TerminationWF that specifies the lexicographic combination of these measures. The parameters are

• originalVarNamess: For each function in the clique, the original parameter names, including the fixed prefix. Used to determine if we need to fully qualify sizeOf.
• varNamess: For each function in the clique, the parameter names to be used in the termination relation. Excludes the fixed prefix. Includes names like x1 for unnamed parameters.
• measures: The measures to be used.

Equations

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

def Lean.Elab.WF.GuessLex.trimTermWF (extraParams : Array Nat) (elems : Lean.Elab.WF.TerminationWF) : Lean.Elab.WF.TerminationWF

The TerminationWF produced by GuessLex may mention more variables than allowed in the surface syntax (in case of unnamed or shadowed parameters). So how to print this to the user? Invalid syntax with more information, or valid syntax with (possibly) unresolved variable names? The latter works fine in many cases, and is still useful to the user in the tricky corner cases, so we do that.

Equations

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

def Lean.Elab.WF.GuessLex.formatTable : Array (Array String) → String

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

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

def Lean.Elab.WF.GuessLex.RecCallWithContext.posString (rcc : Lean.Elab.WF.GuessLex.RecCallWithContext) : Lean.MetaM String

Concise textual representation of the source location of a recursive call

Equations

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

def Lean.Elab.WF.GuessLex.explainNonMutualFailure (varNames : Array Lake.Name) (rcs : Array Lean.Elab.WF.GuessLex.RecCallCache) : Lean.MetaM Lean.Format

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

Equations

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

def Lean.Elab.WF.GuessLex.explainMutualFailure (declNames : Array Lake.Name) (varNamess : Array (Array Lake.Name)) (rcs : Array Lean.Elab.WF.GuessLex.RecCallCache) : Lean.MetaM Lean.Format

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

Equations

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

def Lean.Elab.WF.GuessLex.explainFailure (declNames : Array Lake.Name) (varNamess : Array (Array Lake.Name)) (rcs : Array Lean.Elab.WF.GuessLex.RecCallCache) : Lean.MetaM Lean.Format

Equations

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

def Lean.Elab.WF.guessLex (preDefs : Array Lean.Elab.PreDefinition) (unaryPreDef : Lean.Elab.PreDefinition) (fixedPrefixSize : Nat) : Lean.MetaM Lean.Elab.WF.TerminationWF

Main entry point of this module:

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

Equations

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