PFunctor.Approx.head_succ'
theorem PFunctor.Approx.head_succ' :
∀ {F : PFunctor.{u}} (n m : ℕ) (x : (n : ℕ) → PFunctor.Approx.CofixA F n),
PFunctor.Approx.AllAgree x → PFunctor.Approx.head' (x n.succ) = PFunctor.Approx.head' (x m.succ)
The theorem `PFunctor.Approx.head_succ'` states that for any pfunctor `F` and natural numbers `n` and `m`, if we have an infinite sequence of approximations `x` of the cofix of `F` such that all of these approximations agree with each other (i.e., `PFunctor.Approx.AllAgree x` holds), then the label of the root of the tree for the `n+1`-th approximation is the same as the label of the root of the tree for the `m+1`-th approximation (i.e., `PFunctor.Approx.head' (x (Nat.succ n)) = PFunctor.Approx.head' (x (Nat.succ m))` holds). This theorem essentially establishes the consistency of the root labels when the sequence of approximations is consistent.
More concisely: For any pfunctor F and infinite sequence of approximations x of its cofix such that all approximations agree, the labels of the roots of their respective trees for successor natural numbers are equal.
|
PFunctor.M.dest_mk
theorem PFunctor.M.dest_mk : ∀ {F : PFunctor.{u}} (x : ↑F F.M), (PFunctor.M.mk x).dest = x
The theorem `PFunctor.M.dest_mk` states that for any polynomial functor `F` and any value `x` of type `F` indexed by `M F` (the final coalgebra of `F`), when we create an `M F` type element using the constructor `PFunctor.M.mk` with `x` as an argument, and then apply the `PFunctor.M.dest` function to it, we get back the original value `x`. Essentially, this theorem provides a property of the `M` type's constructor and deconstructor: the deconstruction of any constructed value returns the original value.
More concisely: For any polynomial functor `F` and its final coalgebra element `x` of type `M F`, applying the `PFunctor.M.dest` function to the element `PFunctor.M.mk x` returns the original value `x`.
|
PFunctor.M.IsBisimulation.tail
theorem PFunctor.M.IsBisimulation.tail :
∀ {F : PFunctor.{u}} {R : F.M → F.M → Prop},
PFunctor.M.IsBisimulation R →
∀ {a : F.A} {f f' : F.B a → F.M},
R (PFunctor.M.mk ⟨a, f⟩) (PFunctor.M.mk ⟨a, f'⟩) → ∀ (i : F.B a), R (f i) (f' i)
This theorem, named `PFunctor.M.IsBisimulation.tail`, states that for any polynomial functor `F` and any relation `R` between elements of `F.M`, if `R` is a bisimulation, then for all `a` in `F.A` and functions `f` and `f'` from `F.B a` to `F.M`, if the relation `R` holds between the M-types constructed by `PFunctor.M.mk` from the pair `⟨a, f⟩` and the pair `⟨a, f'⟩`, then for every `i` in `F.B a`, the relation `R` also holds between `f i` and `f' i`.
In other words, if `R` is a bisimulation relation, and `R` relates two elements of the M-type constructed from the same `a` but different functions `f` and `f'`, then `R` must also relate the results of applying `f` and `f'` to the same argument `i`.
More concisely: If `R` is a bisimulation relation between elements of a polynomial functor `F.M`, then for all `a` in `F.A` and functions `f` and `f'` from `F.B a` to `F.M`, if `R` holds between `PFunctor.M.mk (a, f)` and `PFunctor.M.mk (a, f')`, then for all `i` in `F.B a`, `R` holds between `f i` and `f' i`.
|
PFunctor.MIntl.consistent
theorem PFunctor.MIntl.consistent : ∀ {F : PFunctor.{u}} (self : F.MIntl), PFunctor.Approx.AllAgree self.approx := by
sorry
The theorem `PFunctor.MIntl.consistent` states that for any PFunctor `F` and `self` which is an instance of `F.MIntl`, all the iterative approximations available via the `self.approx` are consistent with each other. In other words, for every natural number `n`, the `n`-th approximation (obtained as `self.approx n`) is in agreement with its successor approximation (obtained as `self.approx n.succ`).
More concisely: For any PFunctor `F` and instance `self` of `F.MIntl`, the sequence of approximations `self.approx n` is monotonic increasing.
|
PFunctor.M.IsBisimulation.head
theorem PFunctor.M.IsBisimulation.head :
∀ {F : PFunctor.{u}} {R : F.M → F.M → Prop},
PFunctor.M.IsBisimulation R →
∀ {a a' : F.A} {f : F.B a → F.M} {f' : F.B a' → F.M},
R (PFunctor.M.mk ⟨a, f⟩) (PFunctor.M.mk ⟨a', f'⟩) → a = a'
This theorem, `PFunctor.M.IsBisimulation.head`, states that for any given polynomial functor `F`, and any relation `R` between `F.M -> F.M`, if `R` is a bisimulation (as per `PFunctor.M.IsBisimulation`), then for all `a` and `a'` in `F.A` and all functions `f` and `f'` from `F.B a` and `F.B a'` to `F.M` respectively, if the relation `R` holds between the M-types constructed using `a, f` and `a', f'` (as per `PFunctor.M.mk`), then `a` must be equal to `a'`. In simpler terms, it asserts that if two M-types are related under a bisimulation, their associated elements in `F.A` must be identical.
More concisely: If `R` is a bisimulation relation between `M-types` generated by a polynomial functor `F`, then for all `a` and `a'` in `F.A` such that `R(F.M a, F.M a')` holds, it follows that `a = a'`.
|