English
Coinductive shape of equality: if motive relates s1 and s2 and step preserves motive across cons-cases, then s1 = s2.
Русский
Коинддуктивная форма равенства: если motive связывает s1 и s2 и шаг сохраняет motive в отношении конструкторов, то s1 = s2.
LaTeX
$$$\\text{eq_of_bisim}'(motive, base, step) : \\forall s_1 s_2,\\ motive(s_1,s_2) \\Rightarrow s_1 = s_2.$$$
Lean4
/-- Coinductive principle for equality on sequences.
This is a version of `eq_of_bisim` that looks more like an induction principle. -/
theorem eq_of_bisim' {s₁ s₂ : Seq α} (motive : Seq α → Seq α → Prop) (base : motive s₁ s₂)
(step :
∀ s₁ s₂,
motive s₁ s₂ → (s₁ = nil ∧ s₂ = nil) ∨ (∃ x s₁' s₂', s₁ = cons x s₁' ∧ s₂ = cons x s₂' ∧ motive s₁' s₂')) :
s₁ = s₂ := by
apply eq_of_bisim motive _ base
intro s₁ s₂ h
rcases step s₁ s₂ h with ⟨h_nil₁, h_nil₂⟩ | ⟨_, _, _, h₁, h₂, _⟩
· simp [h_nil₁, h_nil₂]
· simpa [h₁, h₂]
