Computable Acc.rec and WellFounded.fix #

This file exports no public definitions / theorems, but by importing it the compiler will be able to compile Acc.rec and functions that use it. For example:

Before:

-- failed to compile definition, consider marking it as 'noncomputable'
-- because it depends on 'WellFounded.fix', and it does not have executable code
def log2p1 : Nat → Nat :=
  WellFounded.fix Nat.lt_wfRel.2 fun n IH =>
    let m := n / 2
    if h : m < n then
      IH m h + 1
    else
      0

After:

import Std.WF

def log2p1 : Nat → Nat := -- works!
  WellFounded.fix Nat.lt_wfRel.2 fun n IH =>
    let m := n / 2
    if h : m < n then
      IH m h + 1
    else
      0

#eval log2p1 4   -- 3

source

instance Acc.wfRel {α : Sort u_1} {r : α → α → Prop} :

WellFoundedRelation { val : α // Acc r val }

Equations

Acc.wfRel = { rel := InvImage r fun (x : { val : α // Acc r val }) => x.val, wf := (_ : WellFounded (InvImage r fun (x : { val : α // Acc r val }) => x.val)) }

source

def WellFounded.wrap {α : Sort u} {r : α → α → Prop} (h : WellFounded r) (x : α) :

{ x : α // Acc r x }

Attaches to x the proof that x is accessible in the given well-founded relation. This can be used in recursive function definitions to explicitly use a differerent relation than the one inferred by default:

def otherWF : WellFounded Nat := …
def foo (n : Nat) := …
termination_by otherWF.wrap n

Equations

WellFounded.wrap h x = { val := x, property := (_ : Acc r x) }

Instances For