WF.lean

-- https://arxiv.org/abs/1911.08174
def T : Prop := ∀ p, (p → p) → p → p
def δ (z : T) : T := fun p η h => η (z (T → T) id id z p η h)
def ω : T := fun _ _ h => propext ⟨fun _ => h, fun _ => id⟩ ▸ δ
def Ω : T := δ ω

noncomputable def WellFounded.fix' {α : Sort u} {r : α → α → Prop} (hwf : WellFounded r) {C : α → Sort v} (F : ∀ x, (∀ y, r y x → C y) → C x) x : C x :=
  @Acc.rec α r (fun x _ => C x) (fun x _ => F x) x (Ω (∀ x, Acc r x) (fun wf x => ⟨x, fun y _ => wf y⟩) hwf.apply x)

theorem WellFounded.fix'_eq : @WellFounded.fix' α r hwf C F x = F x fun y _ => hwf.fix' F y := rfl

noncomputable def log2 : Nat → Nat := WellFounded.fix' (r := LT.lt) Nat.lt_wfRel.wf fun n log2 => if h : n ≥ 2 then log2 (n / 2) (by omega) + 1 else 0

example : log2 n = if n ≥ 2 then log2 (n / 2) + 1 else 0 := rfl