Computable Acc.rec and WellFounded.fix

This file adds csimp theorems so that the compiler will be able to compile Acc.rec, WellFounded.fix and related operations.

Without this change, the following code will fail to compile as WellFounded.fix is noncomputable.

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

@[instance_reducible]

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

@[irreducible, specialize #[]]

def Acc.recC {α : Sort u_1} {r : α → α → Prop} {motive : (a : α) → Acc r a → Sort v} (intro : (x : α) → (h : ∀ (y : α), r y x → Acc r y) → ((y : α) → (hr : r y x) → motive y ⋯) → motive x ⋯) {a : α} (t : Acc r a) : motive a t

A computable version of Acc.rec.

Equations

• Acc.recC intro t = intro a ⋯ fun (x : α) (hr : r x a) => Acc.recC intro ⋯

@[csimp]

theorem Acc.rec_eq_recC : @rec = @recC

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

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.

Equations

• n.ndrecOnC m = Acc.recC m n

@[csimp]

theorem Acc.ndrecOn_eq_ndrecOnC : @ndrecOn = @ndrecOnC

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

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.

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