English
A stronger coinductive principle: given motive and step producing either equality or a one-step cons from which motive recurses, then s1 = s2.
Русский
Усиленная коинддуктивная принцип: дано motive и шаг, порождающий либо равенство, либо конструируемую через cons пару и рекурсивный motive, следовательно s1 = s2.
LaTeX
$$$\\text{eq_of_bisim_strong}(motive, base, step) : \\forall s_1 s_2, motive(s_1,s_2) \\rightarrow (\\forall s_1 s_2,\\ motive(s_1,s_2) \\rightarrow (\\text{Eq}(s_1,s_2) \\lor \\exists x,s_1',s_2', s_1 = cons\\ x\\ s_1' \\land s_2 = cons\\ x\\ s_2' \\land 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 requires proving only `s₁ = s₂`
instead of `s₁ = nil ∧ s₂ = nil` in `step`. -/
theorem eq_of_bisim_strong {s₁ s₂ : Seq α} (motive : Seq α → Seq α → Prop) (base : motive s₁ s₂)
(step : ∀ s₁ s₂, motive s₁ s₂ → (s₁ = s₂) ∨ (∃ x s₁' s₂', s₁ = cons x s₁' ∧ s₂ = cons x s₂' ∧ (motive s₁' s₂'))) :
s₁ = s₂ := by
let motive' : Seq α → Seq α → Prop := fun s₁ s₂ => s₁ = s₂ ∨ motive s₁ s₂
apply eq_of_bisim' motive' (by grind)
intro s₁ s₂ ih
simp only [motive'] at ih ⊢
rcases ih with (rfl | ih)
· cases s₁ <;> grind
rcases step s₁ s₂ ih with (rfl | ⟨hd, s₁', s₂', _⟩)
· cases s₁ <;> grind
· grind
