List.unfold

[Seasawher]

Lean では停止保証ができないので定義が難しい。
Haskell では遅延評価なので問題なかった。
これを 帰納的述語の例にできるかも？

[Seasawher]

むりやり停止保証して、Lean で実行可能な関数として定義できないだろうか…？

[Seasawher]

無理やり停止保証をしようとした例

cf. Zulip: List.unfold

inductive EventuallyNone {α : Type} (f : α → Option α) : α → Prop where
  | base (h : (f a).isNone) : EventuallyNone f a
  | cons {a'} (h : (f a) = some a') : EventuallyNone f a' → EventuallyNone f a

variable {α β : Type}

/- fail to show termination -/
def List.unfold (a : α) (f : α → Option α) (h : ∀ a, EventuallyNone f a) : List α :=
  match f a with
  | none => []
  | some a' => a' :: List.unfold a' f h

section
/- examples of `EventuallyNone` -/

def prev : Nat → Option Nat
  | 0 => none
  | n + 1 => some n

theorem prev_eventually_none (n : Nat) : EventuallyNone prev n := by
  induction n

  case zero =>
    apply EventuallyNone.base
    rfl

  case succ n ih =>
    apply EventuallyNone.cons
    rfl
    exact ih

end