English
For any weak sequence s, its length in the computation sense equals the length of the list produced by toList, after mapping List.length.
Русский
Для любой слабой последовательности s её длина в вычислительном смысле равна длине списка, получаемого из toList s после применения List.length.
LaTeX
$$$$ \mathrm{length}(s) = \mathrm{Computation.map}(\mathrm{List.length})(\mathrm{toList}(s)). $$$$
Lean4
theorem length_eq_map (s : WSeq α) : length s = Computation.map List.length (toList s) :=
by
refine
Computation.eq_of_bisim
(fun c1 c2 =>
∃ (l : List α) (s : WSeq α),
c1 =
Computation.corec
(fun ⟨n, s⟩ =>
match Seq.destruct s with
| none => Sum.inl n
| some (none, s') => Sum.inr (n, s')
| some (some _, s') => Sum.inr (n + 1, s'))
(l.length, s) ∧
c2 =
Computation.map List.length
(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 with
| nil => simp [nil]
| cons a s => simpa using ⟨a :: l, s, by simp, by simp⟩
| think s => simpa using ⟨l, s, by simp, by simp⟩
