List.attach 使用例

[Seasawher]

Lean のdiscordサーバから引用。

this recursive definition fails to show termination🤔

def generate (f: List A → A): Nat → A :=
  fun n => match n with
  | 0 => f []
  | p + 1 => f (List.map (generate f) (List.range p))

[Seasawher]

someone on Lean zulip gave this proof

def generate (f: List A → A): Nat → A :=
  fun n => match n with
  | 0 => f []
  | p + 1 => f (List.map (fun ⟨l, h⟩ => generate f l) (List.range p).attach)
    decreasing_by
    exact Nat.lt_succ_of_lt (List.mem_range.mp h)