MvQPF.Cofix.bisim_rel
theorem MvQPF.Cofix.bisim_rel :
∀ {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [mvf : MvFunctor F] [q : MvQPF F] {α : TypeVec.{u} n}
(r : MvQPF.Cofix F α → MvQPF.Cofix F α → Prop),
(∀ (x y : MvQPF.Cofix F α),
r x y → MvFunctor.map (TypeVec.id ::: Quot.mk r) x.dest = MvFunctor.map (TypeVec.id ::: Quot.mk r) y.dest) →
∀ (x y : MvQPF.Cofix F α), r x y → x = y
This theorem, `MvQPF.Cofix.bisim_rel`, states the bisimulation principle for the greatest fixed point of a functor `F`. It states that given any multivariate functor `F` and a relation `r` on the greatest fixed point of `F`, if for all pairs `(x, y)` of elements of the greatest fixed point of `F` such that `r x y` holds, the results of mapping the identity function and `Quot.mk r` function over the children of `x` and `y` are the same, then for each pair `(x, y)` in the relation `r`, `x` is indeed equal to `y`. This theorem essentially provides a method for proving the equality of two elements of the greatest fixed point of a functor `F` based on their children's correspondence under a specific relation.
More concisely: Given a multivariate functor `F` and a relation `r` on the greatest fixed point of `F`, if for all pairs `(x, y)` in `r`, the identity function and `Quot.mk r` maps of their children are equal, then `x` and `y` are equal.
|
MvQPF.Cofix.bisim'
theorem MvQPF.Cofix.bisim' :
∀ {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [mvf : MvFunctor F] [q : MvQPF F] {α : TypeVec.{u} n} {β : Type u_1}
(Q : β → Prop) (u v : β → MvQPF.Cofix F α),
(∀ (x : β),
Q x →
∃ a f' f₀ f₁,
(u x).dest = MvQPF.abs ⟨a, (MvQPF.P F).appendContents f' f₀⟩ ∧
(v x).dest = MvQPF.abs ⟨a, (MvQPF.P F).appendContents f' f₁⟩ ∧
∀ (i : (MvQPF.P F).last.B a), ∃ x', Q x' ∧ f₀ i = u x' ∧ f₁ i = v x') →
∀ (x : β), Q x → u x = v x
The theorem `MvQPF.Cofix.bisim'` states that for any natural number `n`, functor `F` with domain `TypeVec.{u} (n + 1)` and codomain `Type u`, which is also an instance of `MvFunctor` and `MvQPF`, and any types `α` of the form `TypeVec.{u} n` and `β` of the form `Type u_1`, if we have an invariant `Q : β → Prop` and two functions `u, v : β → MvQPF.Cofix F α`, then for every `x : β` satisfying `Q x`, there exist `a`, `f'`, `f₀`, `f₁` such that the destination of `u x` equals to the absolute value of `⟨a, (MvQPF.P F).appendContents f' f₀⟩`, the destination of `v x` equals to the absolute value of `⟨a, (MvQPF.P F).appendContents f' f₁⟩`, and for each `i : (MvQPF.P F).last.B a`, there exists `x'` satisfying `Q x'` and `f₀ i = u x'` and `f₁ i = v x'`. If these conditions are met, then for any `x : β` satisfying `Q x`, `u x` equals to `v x`. This is a bisimulation principle that ensures the equality between two instances of the greatest fixed point of a functor under certain conditions.
More concisely: Given a natural number `n`, an `MvFunctor` and `MvQPF` instance functor `F` with domain of size `n+1` and codomain of type `α`, and types `α` of size `n` and `β`, if functions `u, v : β → MvQPF.Cofix F α`, an invariant `Q : β → Prop`, and for all `x : β` satisfying `Q x`, there exist `a, f', f₀, f₁` such that the absolute values of their destinations under `u x` and `v x` are equal and for each index `i` of the last component of `a`, there exists an `x'` satisfying `Q x'` with `u x'` equal to `f₀ i` and `v x'` equal to `f₁ i`, then `u x` equals to `v x` for all `x` satisfying `Q x`.
|
MvQPF.Cofix.bisim
theorem MvQPF.Cofix.bisim :
∀ {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [mvf : MvFunctor F] [q : MvQPF F] {α : TypeVec.{u} n}
(r : MvQPF.Cofix F α → MvQPF.Cofix F α → Prop),
(∀ (x y : MvQPF.Cofix F α), r x y → MvFunctor.LiftR (fun {i} => α.RelLast r) x.dest y.dest) →
∀ (x y : MvQPF.Cofix F α), r x y → x = y
The theorem `MvQPF.Cofix.bisim` states that for any natural number `n`, any multivariate functor `F` of type vector with `n+1` types, any multivariate quasi-coherent state monad `q` on `F`, and any type vector `α` of length `n`, if there exists a relation `r` between fixed points of `F` on `α` such that for any two fixed points `x` and `y`, `r x y` implies a relational lifting of the last relation of `α` and `r` on the destinations of `x` and `y`, then `r x y` implies `x = y`. In simpler terms, this is a bisimulation principle stating that if two trees can be matched and related by a function `r` through all their children, then the two trees are the same.
More concisely: Given a natural number `n`, a multivariate functor `F` of type vector with `n+1` types, a multivariate quasi-coherent state monad `q` on `F`, and a type vector `α` of length `n`, if there exists a relation `r` between fixed points of `F` on `α` such that for any two fixed points `x` and `y`, `r x y` implies `r (F.map q x) (F.map q y)` and `last α x = last α y`, then `x = y`.
|
MvQPF.Cofix.bisim₂
theorem MvQPF.Cofix.bisim₂ :
∀ {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [mvf : MvFunctor F] [q : MvQPF F] {α : TypeVec.{u} n}
(r : MvQPF.Cofix F α → MvQPF.Cofix F α → Prop),
(∀ (x y : MvQPF.Cofix F α), r x y → MvFunctor.LiftR' (α.RelLast' r) x.dest y.dest) →
∀ (x y : MvQPF.Cofix F α), r x y → x = y
The theorem `MvQPF.Cofix.bisim₂` establishes a bisimulation principle using the `LiftR'` function to match and relate children of two trees. For any natural number `n`, functor `F` of type `TypeVec.{u} (n + 1) → Type u`, and `α` of type `TypeVec.{u} n`, it states that if for any two objects `x` and `y` of type `MvQPF.Cofix F α` satisfying a relation `r`, their destinations `x.dest` and `y.dest` lift the relation `r` to the last coordinate of `α`, then `x` and `y` are equal whenever they satisfy the relation `r`. In other words, it asserts that if two trees are related by a certain property and their children also satisfy the same property, then the two trees are equal.
More concisely: If for any trees x and y of type `MvQPF.Cofix F α` satisfying relation r, and their destinations lift r to the last coordinate of α, then x and y are equal whenever they satisfy relation r.
|