English
Mapping ret and then joining yields back the original sequence, i.e., map ret s, then join, is equivalent to s.
Русский
После применения ret внутри map и затем объединения (join) получаем эквивалентность исходной последовательности: join (map ret s) ≃ s.
LaTeX
$$$ \forall s : \mathrm{WSeq}\,\alpha,\; \mathrm{join}(\mathrm{map}\, \mathrm{ret}\, s) \sim_W s$$$
Lean4
@[simp]
theorem join_map_ret (s : WSeq α) : join (map ret s) ~ʷ s :=
by
refine ⟨fun s1 s2 => join (map ret s2) = s1, rfl, ?_⟩
intro s' s h; rw [← h]
apply liftRel_rec fun c1 c2 => ∃ s, c1 = destruct (join (map ret s)) ∧ c2 = destruct s
·
exact fun {c1 c2} h =>
match c1, c2, h with
| _, _, ⟨s, rfl, rfl⟩ => by
clear h
have (s : WSeq α) :
∃ s' : WSeq α, (map ret s).join.destruct = (map ret s').join.destruct ∧ destruct s = s'.destruct :=
⟨s, rfl, rfl⟩
induction s using WSeq.recOn <;> simp [ret, this]
· exact ⟨s, rfl, rfl⟩
