English
toList' distributes the map f across toList: toList'(l, s) equals the map of toList(s) by the function that conses reversed l.
Русский
toList' распределяет отображение по toList: toList'(l, s) равняется отображению toList(s) функцией, добавляющей в начало обратный список.
LaTeX
$$$$toList'\,(l, s) = (l.reverse ++ \cdot) \leftarrow \mathrm{toList}\,s.$$$$
Lean4
theorem toList'_map (l : List α) (s : WSeq α) :
Computation.corec
(fun ⟨l, s⟩ =>
match Seq.destruct s with
| none => Sum.inl l.reverse
| some (none, s') => Sum.inr (l, s')
| some (some a, s') => Sum.inr (a :: l, s'))
(l, s) =
(l.reverse ++ ·) <$> toList s :=
by
refine
Computation.eq_of_bisim
(fun c1 c2 =>
∃ (l' : List α) (s : WSeq α),
c1 =
Computation.corec
(fun ⟨l, s⟩ =>
match Seq.destruct s with
| none => Sum.inl l.reverse
| some (none, s') => Sum.inr (l, s')
| some (some a, s') => Sum.inr (a :: l, s'))
(l' ++ l, s) ∧
c2 =
Computation.map (l.reverse ++ ·)
(Computation.corec
(fun ⟨l, s⟩ =>
match Seq.destruct s with
| none => Sum.inl l.reverse
| some (none, s') => Sum.inr (l, s')
| some (some a, s') => Sum.inr (a :: l, s'))
(l', s)))
?_ ⟨[], s, rfl, rfl⟩
intro s1 s2 h; rcases h with ⟨l', s, h⟩; rw [h.left, h.right]
induction s using WSeq.recOn <;> simp [nil, cons, think]
case cons a s => refine ⟨a :: l', s, ?_, ?_⟩ <;> simp
case think s => refine ⟨l', s, ?_, ?_⟩ <;> simp
