This module finds lexicographic termination arguments 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 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:

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

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

- Lean.Elab.WF.GuessLex.originalVarNames preDef = Lean.Meta.lambdaTelescope preDef.value fun (xs : Array Lean.Expr) (x : Lean.Expr) => Array.mapM (fun (x : Lean.Expr) => x.fvarId!.getUserName) xs

## Instances For

Given the original parameter names from `originalVarNames`

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

## Instances For

A termination measure with extra fields for use within GuessLex

- ref : Lean.Syntax
- arity : Nat
- extraParams : Nat
- fn : Lean.Expr
- natFn : Lean.Expr
Like

`.fn`

, but unconditionally with`sizeOf`

at the right type. We use this one when in`evalRecCall`

## Instances For

## Equations

- Lean.Elab.WF.GuessLex.instInhabitedMeasure = { default := { toTerminationArgument := default, natFn := default } }

String desription of this measure

## Equations

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

## 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 argument does not depend on
the other varying parameters, and its `WellFoundedRelation`

instance goes via `SizeOf`

.

For mutual definitions, we omit `sizeOf`

only when the argument is (at reducible transparency!) of
type `Nat`

(else we'd have to worry about differently-typed measures from different functions to
line up).

## Equations

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

## Instances For

Sets the user names for the given freevars in `xs`

.

## Equations

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

## Instances For

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

## Equations

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

## Instances For

Internal monad used by `withRecApps`

## Equations

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

## Instances For

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.

## Instances For

## Equations

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

## Instances For

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

## Instances For

Capture the `MetaM`

state including local context.

## Equations

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

## Instances For

Run a `MetaM`

action in the saved state.

## Equations

- slc.run k = Lean.withoutModifyingState (Lean.Meta.withLCtx slc.savedLocalContext slc.savedLocalInstances do slc.savedState.restore k)

## 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 : Lean.Syntax
Syntax location of recursive call

- caller : Nat
Function index of caller

Parameters of caller (including fixed prefix)

- callee : Nat
Function index of callee

Arguments to callee (including fixed prefix)

## Instances For

Store the current recursive call and its context.

## Equations

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

## 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

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

## Instances For

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.

## Instances For

## Equations

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

## Instances For

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

## Instances For

## Equations

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

## Equations

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

## Equations

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

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.

## Instances For

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.

## Instances For

- mk'' :: (
- decrTactic? : Option Lean.Elab.WF.DecreasingBy
- callerMeasures : Array Lean.Elab.WF.GuessLex.Measure
- calleeMeasures : Array Lean.Elab.WF.GuessLex.Measure
- cache : IO.Ref (Array (Array (Option Lean.Elab.WF.GuessLex.GuessLexRel)))
- )

## Instances For

Create a cache to memoize calls to `evalRecCall descTactic? rcc`

## Equations

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

## Instances For

Run `evalRecCall`

and cache there result

## Equations

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

## Instances For

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

## Equations

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

## Instances For

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

## Instances For

Evaluate a recursive call at a given `MutualMeasure`

## Equations

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

## Instances For

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

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

## Instances For

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.

## Instances For

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 #[]

## Instances For

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.

## Instances For

Concise textual representation of the source location of a recursive call

## Equations

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

## Instances For

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

## Equations

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

## Instances For

## Equations

- Lean.Elab.WF.GuessLex.collectHeaders a = do let __discr ← a.run (0, "") match __discr with | (x, fst, footer) => pure (x, footer)

## Instances For

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.

## Instances For

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

## 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

For `#[x₁, .., xₙ]`

create `(x₁, .., xₙ)`

.

## 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

Shows the inferred termination argument to the user, and implements `termination_by?`

## Equations

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

## Instances For

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.