Documentation

Mathlib.Data.PFunctor.Multivariate.M

The M construction as a multivariate polynomial functor. #

M types are potentially infinite tree-like structures. They are defined as the greatest fixpoint of a polynomial functor.

Main definitions #

Implementation notes #

Dual view of M-types:

Specifically, we define the polynomial functor Mp as:

As a result Mp.obj α is made of a dataless tree and a function from its valid paths to values of α

The difference with the polynomial functor of an initial algebra is that A is a possibly infinite tree.

Reference #

inductive MvPFunctor.M.Path {n : } (P : MvPFunctor (n + 1)) :

A path from the root of a tree to one of its node

Instances For
    def MvPFunctor.mp {n : } (P : MvPFunctor (n + 1)) :

    Polynomial functor of the M-type of P. A is a data-less possibly infinite tree whereas, for a given a : A, B a is a valid path in tree a so that mp.Obj α is made of a tree and a function from its valid paths to the values it contains

    Instances For
      def MvPFunctor.M {n : } (P : MvPFunctor (n + 1)) (α : TypeVec n) :

      n-ary M-type for P

      Instances For
        instance MvPFunctor.inhabitedM {n : } (P : MvPFunctor (n + 1)) {α : TypeVec n} [I : Inhabited P.A] [(i : Fin2 n) → Inhabited (α i)] :
        def MvPFunctor.M.corecShape {n : } (P : MvPFunctor (n + 1)) {β : Type u} (g₀ : βP.A) (g₂ : (b : β) → PFunctor.B (MvPFunctor.last P) (g₀ b)β) :

        construct through corecursion the shape of an M-type without its contents

        Instances For
          def MvPFunctor.castDropB {n : } (P : MvPFunctor (n + 1)) {a : P.A} {a' : P.A} (h : a = a') :

          Proof of type equality as an arrow

          Instances For
            def MvPFunctor.castLastB {n : } (P : MvPFunctor (n + 1)) {a : P.A} {a' : P.A} (h : a = a') :

            Proof of type equality as a function

            Instances For
              def MvPFunctor.M.corecContents {n : } (P : MvPFunctor (n + 1)) {α : TypeVec n} {β : Type u} (g₀ : βP.A) (g₁ : (b : β) → TypeVec.Arrow (MvPFunctor.B (MvPFunctor.drop P) (g₀ b)) α) (g₂ : (b : β) → PFunctor.B (MvPFunctor.last P) (g₀ b)β) (x : PFunctor.M (MvPFunctor.last P)) (b : β) (h : x = MvPFunctor.M.corecShape P g₀ g₂ b) :

              Using corecursion, construct the contents of an M-type

              Equations
              Instances For
                def MvPFunctor.M.corec' {n : } (P : MvPFunctor (n + 1)) {α : TypeVec n} {β : Type u} (g₀ : βP.A) (g₁ : (b : β) → TypeVec.Arrow (MvPFunctor.B (MvPFunctor.drop P) (g₀ b)) α) (g₂ : (b : β) → PFunctor.B (MvPFunctor.last P) (g₀ b)β) :
                βMvPFunctor.M P α

                Corecursor for M-type of P

                Instances For
                  def MvPFunctor.M.corec {n : } (P : MvPFunctor (n + 1)) {α : TypeVec n} {β : Type u} (g : βMvPFunctor.Obj P (α ::: β)) :
                  βMvPFunctor.M P α

                  Corecursor for M-type of P

                  Instances For
                    def MvPFunctor.M.pathDestLeft {n : } (P : MvPFunctor (n + 1)) {α : TypeVec n} {x : PFunctor.M (MvPFunctor.last P)} {a : P.A} {f : PFunctor.B (MvPFunctor.last P) aPFunctor.M (MvPFunctor.last P)} (h : PFunctor.M.dest x = { fst := a, snd := f }) (f' : TypeVec.Arrow (MvPFunctor.M.Path P x) α) :

                    Implementation of destructor for M-type of P

                    Instances For
                      def MvPFunctor.M.pathDestRight {n : } (P : MvPFunctor (n + 1)) {α : TypeVec n} {x : PFunctor.M (MvPFunctor.last P)} {a : P.A} {f : PFunctor.B (MvPFunctor.last P) aPFunctor.M (MvPFunctor.last P)} (h : PFunctor.M.dest x = { fst := a, snd := f }) (f' : TypeVec.Arrow (MvPFunctor.M.Path P x) α) (j : PFunctor.B (MvPFunctor.last P) a) :

                      Implementation of destructor for M-type of P

                      Instances For
                        def MvPFunctor.M.dest' {n : } (P : MvPFunctor (n + 1)) {α : TypeVec n} {x : PFunctor.M (MvPFunctor.last P)} {a : P.A} {f : PFunctor.B (MvPFunctor.last P) aPFunctor.M (MvPFunctor.last P)} (h : PFunctor.M.dest x = { fst := a, snd := f }) (f' : TypeVec.Arrow (MvPFunctor.M.Path P x) α) :

                        Destructor for M-type of P

                        Instances For
                          def MvPFunctor.M.dest {n : } (P : MvPFunctor (n + 1)) {α : TypeVec n} (x : MvPFunctor.M P α) :

                          Destructor for M-types

                          Instances For
                            def MvPFunctor.M.mk {n : } (P : MvPFunctor (n + 1)) {α : TypeVec n} :

                            Constructor for M-types

                            Instances For
                              theorem MvPFunctor.M.dest'_eq_dest' {n : } (P : MvPFunctor (n + 1)) {α : TypeVec n} {x : PFunctor.M (MvPFunctor.last P)} {a₁ : P.A} {f₁ : PFunctor.B (MvPFunctor.last P) a₁PFunctor.M (MvPFunctor.last P)} (h₁ : PFunctor.M.dest x = { fst := a₁, snd := f₁ }) {a₂ : P.A} {f₂ : PFunctor.B (MvPFunctor.last P) a₂PFunctor.M (MvPFunctor.last P)} (h₂ : PFunctor.M.dest x = { fst := a₂, snd := f₂ }) (f' : TypeVec.Arrow (MvPFunctor.M.Path P x) α) :
                              theorem MvPFunctor.M.dest_eq_dest' {n : } (P : MvPFunctor (n + 1)) {α : TypeVec n} {x : PFunctor.M (MvPFunctor.last P)} {a : P.A} {f : PFunctor.B (MvPFunctor.last P) aPFunctor.M (MvPFunctor.last P)} (h : PFunctor.M.dest x = { fst := a, snd := f }) (f' : TypeVec.Arrow (MvPFunctor.M.Path P x) α) :
                              MvPFunctor.M.dest P { fst := x, snd := f' } = MvPFunctor.M.dest' P h f'
                              theorem MvPFunctor.M.dest_corec' {n : } (P : MvPFunctor (n + 1)) {α : TypeVec n} {β : Type u} (g₀ : βP.A) (g₁ : (b : β) → TypeVec.Arrow (MvPFunctor.B (MvPFunctor.drop P) (g₀ b)) α) (g₂ : (b : β) → PFunctor.B (MvPFunctor.last P) (g₀ b)β) (x : β) :
                              MvPFunctor.M.dest P (MvPFunctor.M.corec' P g₀ g₁ g₂ x) = { fst := g₀ x, snd := TypeVec.splitFun (g₁ x) (MvPFunctor.M.corec' P g₀ g₁ g₂ g₂ x) }
                              theorem MvPFunctor.M.dest_corec {n : } (P : MvPFunctor (n + 1)) {α : TypeVec n} {β : Type u} (g : βMvPFunctor.Obj P (α ::: β)) (x : β) :
                              theorem MvPFunctor.M.bisim_lemma {n : } (P : MvPFunctor (n + 1)) {α : TypeVec n} {a₁ : (MvPFunctor.mp P).A} {f₁ : TypeVec.Arrow (MvPFunctor.B (MvPFunctor.mp P) a₁) α} {a' : P.A} {f' : TypeVec.Arrow (TypeVec.drop (MvPFunctor.B P a')) α} {f₁' : TypeVec.last (MvPFunctor.B P a')MvPFunctor.M P α} (e₁ : MvPFunctor.M.dest P { fst := a₁, snd := f₁ } = { fst := a', snd := TypeVec.splitFun f' f₁' }) :
                              g₁' e₁', f' = MvPFunctor.M.pathDestLeft P e₁' f₁ f₁' = fun x => { fst := g₁' x, snd := MvPFunctor.M.pathDestRight P e₁' f₁ x }
                              theorem MvPFunctor.M.bisim {n : } (P : MvPFunctor (n + 1)) {α : TypeVec n} (R : MvPFunctor.M P αMvPFunctor.M P αProp) (h : ∀ (x y : MvPFunctor.M P α), R x ya f f₁ f₂, MvPFunctor.M.dest P x = { fst := a, snd := TypeVec.splitFun f f₁ } MvPFunctor.M.dest P y = { fst := a, snd := TypeVec.splitFun f f₂ } ((i : TypeVec.last (MvPFunctor.B P a)) → R (f₁ i) (f₂ i))) (x : MvPFunctor.M P α) (y : MvPFunctor.M P α) (r : R x y) :
                              x = y
                              theorem MvPFunctor.M.bisim₀ {n : } (P : MvPFunctor (n + 1)) {α : TypeVec n} (R : MvPFunctor.M P αMvPFunctor.M P αProp) (h₀ : Equivalence R) (h : ∀ (x y : MvPFunctor.M P α), R x yMvFunctor.map (TypeVec.id ::: Quot.mk R) (MvPFunctor.M.dest P x) = MvFunctor.map (TypeVec.id ::: Quot.mk R) (MvPFunctor.M.dest P y)) (x : MvPFunctor.M P α) (y : MvPFunctor.M P α) (r : R x y) :
                              x = y
                              theorem MvPFunctor.M.bisim' {n : } (P : MvPFunctor (n + 1)) {α : TypeVec n} (R : MvPFunctor.M P αMvPFunctor.M P αProp) (h : ∀ (x y : MvPFunctor.M P α), R x yMvFunctor.map (TypeVec.id ::: Quot.mk R) (MvPFunctor.M.dest P x) = MvFunctor.map (TypeVec.id ::: Quot.mk R) (MvPFunctor.M.dest P y)) (x : MvPFunctor.M P α) (y : MvPFunctor.M P α) (r : R x y) :
                              x = y
                              theorem MvPFunctor.M.dest_map {n : } (P : MvPFunctor (n + 1)) {α : TypeVec n} {β : TypeVec n} (g : TypeVec.Arrow α β) (x : MvPFunctor.M P α) :