This module implements the preprocessing of function definitions involved in well-founded recursion. The goal is to change higher order functions to add more information to the context, e.g. change `List.map (fun x => …) xs` to `List.map (fun ⟨x, h⟩ => …) xs.attach`. This extra information can then be used by the termination proof tactic to determine that a recursive call is indeed decreasing.

The process proceeds in these steps, to guide the transformation:

1. The parameters of the function are annotated with the `wfParam` gadget.

   We could be more selective here and only annotate those that have a `SizeOf` instance. We cannot (easily) only consider the parameters that appear in the termination measure, as that is not known yet.

2. The `wfParam` gadget is pushed around:

   - `f (wfParam x) ==> wfParam (f x)` if `f` is a projection

   - `match (wfParam x) with con y => alt[y] ==> match x with con y => alt[wfParam y]`

     In a match with multiple targets it suffices for any of the targets to be annotated with `wfParam`, and all parameters of the match arms are annotated with `wfParam`. This is an overapproximation.

3. The `wf_preprocess` simpset is applied to do the actual transformation. It typically contains two rules for each higher-order function of interest

   - `(wfParam xs).map f = xs.attach.unattach.map f`
   - `xs.unattach.map f = xs.map (fun ⟨x, h⟩ => binderNameHint x f (f (wfParam x)))`

   The first rule “activates” the call, the second rule actually performs it. They are separated like this so that for chains of the form `(xs.reverse.filter p).map f` the `.attach` is attached to `xs` and we get the basic `x ∈ xs` in the context of `f`.

   The `binderNameHint` preserves the user-chosen name in `f` if that is a lambda.

   The `wfParam` on the right hand side ensurses that doubly-nested recursion works.

4. All left-over `wfParam` gadgets are removed.

The simplifier is used to perform steps 2 (using simprocs) and 3 (using rewrite rules) together.

source
opaque wf.preprocess :
Lean.Option Bool
source
opaque Lean.Elab.WF.wfPreprocessSimpExtension :
Meta.SimpExtension
source
def Lean.Elab.WF.isWfParam? (e : Expr) :
Option Expr
Equations

- Lean.Elab.WF.isWfParam? e = if e.isAppOfArity `wfParam 2 = true then some e.appArg! else none

Instances For

source
def Lean.Elab.WF.mkWfParam (e : Expr) :
MetaM Expr
Equations

- Lean.Elab.WF.mkWfParam e = Lean.Meta.mkAppM `wfParam #[e]

Instances For

source
def Lean.Elab.WF.paramProj :
Meta.Simp.DSimproc

`f (wfParam x) ==> wfParam (f x)` if `f` is a projection

Equations

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

Instances For

source
def Lean.Elab.WF.paramMatcher :
Meta.Simp.DSimproc

`match (wfParam x) with con y => alt[y] ==> match x with con y => alt[wfParam y]

Equations

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

Instances For

source
def Lean.Elab.WF.paramLet :
Meta.Simp.DSimproc

`let x : T := (wfParam e); body[x] ==> let x : T := e; body[wfParam y]` if `T` is not a proposition, otherwise `... ==> let x : T := e; body[x]`. (Applies to `have`s too.)

Note: simprocs are provided the head of a let telescope, but not intermediate lets.

Equations

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

Instances For

source
def Lean.Elab.WF.preprocess (e : Expr) :
MetaM Meta.Simp.Result
Equations

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

Instances For