English
Let R be a bisimulation on Computation α. If s1 and s2 are related by a bisimulation r: s1 ~ s2, then s1 = s2.
Русский
Пусть R — бисимуляция над Computation α. Если состояния s1 и s2 связаны отношением бисимуляции, то s1 = s2.
LaTeX
$$$\forall (R : \mathrm{Computation}\, \alpha \to \mathrm{Computation}\, \alpha \to \mathrm{Prop}),\; \text{IsBisimulation } R \to \forall \{s_1\, s_2\}, \; s_1 ~ s_2 \Rightarrow s_1 = s_2.$$$
Lean4
theorem eq_of_bisim (bisim : IsBisimulation R) {s₁ s₂} (r : s₁ ~ s₂) : s₁ = s₂ :=
by
apply Subtype.eq
apply Stream'.eq_of_bisim fun x y => ∃ s s' : Computation α, s.1 = x ∧ s'.1 = y ∧ R s s'
· dsimp [Stream'.IsBisimulation]
intro t₁ t₂ e
match t₁, t₂, e with
| _, _,
⟨s, s', rfl, rfl,
r⟩ =>
suffices head s = head s' ∧ R (tail s) (tail s') from
And.imp id (fun r => ⟨tail s, tail s', by cases s; rfl, by cases s'; rfl, r⟩) this
have h := bisim r; revert r h
refine recOn s ?_ ?_ <;> intro r' <;> refine recOn s' ?_ ?_ <;> intro a' r h
· constructor <;> dsimp at h
· rw [h]
· rw [h] at r
rw [tail_pure, tail_pure, h]
assumption
· rw [destruct_pure, destruct_think] at h
exact False.elim h
· rw [destruct_pure, destruct_think] at h
exact False.elim h
· simp_all
· exact ⟨s₁, s₂, rfl, rfl, r⟩
