List.unfold

Stream: general

[Asei Inoue]

I want to define List.unfold function. Since Lean requires a termination guarantee, it cannot be defined by using the Haskell definition as it is.

In order to guarantee the termination of List.unfold in Lean, I created a predicate that expresses that ‘eventually it will be none’.

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

However, I do not know how to write a proof of termination...
Could you give me some help?

[Violeta Hernández]

What does it mean for a list to be eventually none? What does it mean to unfold a list?

[Mauricio Collares]

This works, but I had to change the inductive from Prop to Type:

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

variable {α β : Type}

def List.unfold (a : α) (f : α → Option α) (h : EventuallyNone f a) : List α :=
  match he : f a, h with
  | some a', .cons a'' eq h' =>
      have : a' = a'' := Option.some_inj.1 (he.symm.trans eq)
      a' :: List.unfold a' f (this ▸ h')
  | _, _ => []

[Mauricio Collares]

Violeta Hernández said:

What does it mean for a list to be eventually none? What does it mean to unfold a list?

The function f either produces some a', the next value of the iteration, or none to stop. unfolding this function means producing a list with all the values produced during the iterations. It's a very useful function in Haskell.

[Mauricio Collares]

Although, in Haskell I believe the function returns the next output and the value to be used as the next input instead of using the same value for both

[RustyYato]

I've found a way to make List.unfold more permissive (EventuallyNone f a instead of forall a, EventuallyNone f a) while keeping EventuallyNone f a a Prop.

lean playground

[RustyYato]

And here's a version like Haskell's unfold
lean playground

[François G. Dorais]

Please use WellFounded rather than reinventing the wheel.

[Asei Inoue]

Thank you all !! I will try again