English
If a relation R on sequences is a bisimulation, then any two streams s1, s2 related by R are equal.
Русский
Если отношение R на последовательностях является бисимиляцией, то любые две последовательности, связанные через R, равны.
LaTeX
$$$IsBisimulation(R) \\rightarrow (s_1 ~ s_2) \\rightarrow s_1 = s_2$$$
Lean4
/-- If two streams are bisimilar, then they are equal. There are also versions
`eq_of_bisim'` and `eq_of_bisim_strong` that does not mention `IsBisimulation` and look
more like an induction principles. -/
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' : Seq α, s.1 = x ∧ s'.1 = y ∧ R s s'
· dsimp [Stream'.IsBisimulation]
intro t₁ t₂ e
exact
match t₁, t₂, e with
| _, _, ⟨s, s', rfl, rfl, r⟩ =>
by
suffices head s = head s' ∧ R (tail s) (tail s') from
And.imp id
(fun r => ⟨tail s, tail s', by cases s using Subtype.recOn; rfl, by cases s' using Subtype.recOn; rfl, r⟩)
this
have := bisim r; revert r this
cases s <;> cases s'
· intro r _
constructor
· rfl
· assumption
· intro _ this
rw [destruct_nil, destruct_cons] at this
exact False.elim this
· intro _ this
rw [destruct_nil, destruct_cons] at this
exact False.elim this
· simp
· exact ⟨s₁, s₂, rfl, rfl, r⟩
