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

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 := ⋯ }

@[reducible, inline]

abbrev Acc.ndrecC {α : Sort u_1} {r : α → α → Prop} {C : α → Sort v} (m : (x : α) → (∀ (y : α), r y x → Acc r y) → ((y : α) → r y x → C y) → C x) {a : α} (n : Acc r a) : C a

A computable version of Acc.ndrec. Workaround until Lean has native support for this.

Equations

• Acc.ndrecC m n = Acc.recC✝ m n

@[csimp]

theorem Acc.ndrec_eq_ndrecC : @ndrec = @ndrecC

@[reducible, inline]

abbrev Acc.ndrecOnC {α : Sort u_1} {r : α → α → Prop} {C : α → Sort v} {a : α} (n : Acc r a) (m : (x : α) → (∀ (y : α), r y x → Acc r y) → ((y : α) → r y x → C y) → C x) : C a

A computable version of Acc.ndrecOn. Workaround until Lean has native support for this.

Equations

• n.ndrecOnC m = Acc.recC✝ m n

@[csimp]

theorem Acc.ndrecOn_eq_ndrecOnC : @ndrecOn = @ndrecOnC

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 different relation than the one inferred by default:

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

Equations

• h.wrap x = ⟨x, ⋯⟩

@[simp]

theorem WellFounded.val_wrap {α : Sort u} {r : α → α → Prop} (h : WellFounded r) (x : α) : (h.wrap x).val = x

@[inline]

def WellFounded.fixFC {α : Sort u} {r : α → α → Prop} {C : α → Sort v} (F : (x : α) → ((y : α) → r y x → C y) → C x) (x : α) (a : Acc r x) : C x

A computable version of WellFounded.fixF. Workaround until Lean has native support for this.

Equations

• WellFounded.fixFC F x a = Acc.recC✝ (fun (x₁ : α) (h : ∀ (y : α), r y x₁ → Acc r y) (ih : (y : α) → r y x₁ → C y) => F x₁ ih) a

@[csimp]

theorem WellFounded.fixF_eq_fixFC : @fixF = @fixFC

@[irreducible, specialize #[]]

def WellFounded.fixC {α : Sort u} {C : α → Sort v} {r : α → α → Prop} (hwf : WellFounded r) (F : (x : α) → ((y : α) → r y x → C y) → C x) (x : α) : C x

A computable version of fix. Workaround until Lean has native support for this.

Equations

• hwf.fixC F x = F x fun (y : α) (x : r y x) => hwf.fixC F y

@[csimp]

theorem WellFounded.fix_eq_fixC : @fix = @fixC