English
There is a distributive law connecting eval via tr, showing eval after applying tr equals map over eval.
Русский
Существует распределительный закон, связывающий eval через tr; после применения tr вычисление эквивалентно отображению по маппингу eval.
LaTeX
$$$\\forall {\\sigma_1 \\sigma_2} (f_1 : \\sigma_1 \\to \\mathrm{Option}\\,\\sigma_1) (f_2 : \\sigma_2 \\to \\mathrm{Option}\\,\\sigma_2) (tr : \\sigma_1 \\to \\sigma_2),\\n (\\mathrm{Respects} f_1 f_2 (\\lambda a b => tr\\ a = b)) \\to \\forall {a_1}, \\mathrm{eval}\\ f_2 (tr\\ a_1) = \\mathrm{map}\\ tr (\\mathrm{eval}\\ f_1 a_1)$$$
Lean4
theorem tr_eval' {σ₁ σ₂} (f₁ : σ₁ → Option σ₁) (f₂ : σ₂ → Option σ₂) (tr : σ₁ → σ₂)
(H : Respects f₁ f₂ fun a b ↦ tr a = b) (a₁) : eval f₂ (tr a₁) = tr <$> eval f₁ a₁ :=
Part.ext fun b₂ ↦
⟨fun h ↦
let ⟨b₁, bb, hb⟩ := tr_eval_rev H rfl h
(Part.mem_map_iff _).2 ⟨b₁, hb, bb⟩,
fun h ↦ by
rcases (Part.mem_map_iff _).1 h with ⟨b₁, ab, bb⟩
rcases tr_eval H rfl ab with ⟨_, rfl, h⟩
rwa [bb] at h⟩
