List.unfold を帰納的述語として定義する例

[Seasawher]

プログラム意味論に代わって帰納的述語のいい例になるかと期待したが、冷静に考えると計算不能という帰納的述語のデメリットが顕著に出る例なので、例としては適さないようだ。

universe u v

variable {α : Type u} {β : Type v}

namespace Haskell
/- ## Haskell 通りにやった場合

fail to show termination となってしまう。
これは、f を繰り返し適用した結果 none になるとは限らないため。

Haskell は遅延評価なので終わらない処理を簡潔に書くことができたようだ。
-/

partial def List.unfoldr (f : β → Option (α × β)) (init : β) : List α :=
  match f init with
  | none => []
  | some (a, b) =>
    a :: unfoldr f b

/- `List.unfoldr f init = as` であることを、帰納的述語として表現するとどうなるか？ -/


end Haskell

/- ## 帰納的述語として定義する -/

/-- `unfold` の帰納的述語として定義されたバージョン -/
inductive Unfold (f : β → Option (α × β)) : β → List α → Prop where
  | nil (h : f init = none) : Unfold f init []
  | cons (a : α) (b : β) (h : f init = some (a, b)) (ih : Unfold f b as) :
    Unfold f init (a :: as)