English
Mapping over a concatenation distributes over concatenation: map f (s.append t) = (map f s).append (map f t).
Русский
Покрытие отображением над конкатенацией распределяется по конкатенации: map f (s.append t) = (map f s).append (map f t).
LaTeX
$$$\forall {f} {s t : Seq \alpha}, map f (append s t) = append (map f s) (map f t)$$$
Lean4
@[simp]
theorem map_append (f : α → β) (s t) : map f (append s t) = append (map f s) (map f t) :=
by
apply eq_of_bisim (fun s1 s2 => ∃ s t, s1 = map f (append s t) ∧ s2 = append (map f s) (map f t)) _ ⟨s, t, rfl, rfl⟩
intro s1 s2 h
exact
match s1, s2, h with
| _, _, ⟨s, t, rfl, rfl⟩ => by
cases s <;> simp
case nil =>
cases t <;> simp
case cons _ t => refine ⟨nil, t, ?_, ?_⟩ <;> simp
case cons _ s => exact ⟨s, t, rfl, rfl⟩
