English
Specialized bisimulation modulo an equivalence relation: if R is an equivalence and dest x and dest y correspond to equal head and tails modulo R, then x and y are equal.
Русский
Спец-бимилизацию по эквивалентности: если R — эквивалентность, и dest x,dest y совпадают по головам и хвостам modulo R, то x=y.
LaTeX
$$$\forall {n} {P} (R : P.M α → P.M α → Prop) (h₀ : Equivalence R) (h : ∀ (x y), R x y → (id ::: Quot.mk R) <$$> M.dest _ x = (id ::: Quot.mk R) <$$> M.dest _ y) (x y) (r : R x y) : x = y$$$
Lean4
theorem bisim₀ {α : TypeVec n} (R : P.M α → P.M α → Prop) (h₀ : Equivalence R)
(h : ∀ x y, R x y → (id ::: Quot.mk R) <$$> M.dest _ x = (id ::: Quot.mk R) <$$> M.dest _ y) (x y) (r : R x y) :
x = y := by
apply M.bisim P R _ _ _ r
clear r x y
introv Hr
specialize h _ _ Hr
clear Hr
revert h
rcases M.dest P x with ⟨ax, fx⟩
rcases M.dest P y with ⟨ay, fy⟩
intro h
rw [map_eq, map_eq] at h
injection h with h₀ h₁
subst ay
simp only [heq_eq_eq] at h₁
have Hdrop : dropFun fx = dropFun fy := by
replace h₁ := congr_arg dropFun h₁
simpa using h₁
exists ax, dropFun fx, lastFun fx, lastFun fy
rw [split_dropFun_lastFun, Hdrop, split_dropFun_lastFun]
simp only [true_and]
intro i
replace h₁ := congr_fun (congr_fun h₁ Fin2.fz) i
simp only [TypeVec.comp, appendFun, splitFun] at h₁
replace h₁ := Quot.eqvGen_exact h₁
rw [h₀.eqvGen_iff] at h₁
exact h₁
