Documentation

Mathlib.Data.PFunctor.Univariate.M

M-types #

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

inductive PFunctor.Approx.CofixA (F : PFunctor) :
Type u

CofixA F n is an n level approximation of an M-type

Instances For

    default inhabitant of CofixA

    Equations
    Instances For

      The label of the root of the tree for a non-trivial approximation of the cofix of a pfunctor.

      Instances For

        for a non-trivial approximation, return all the subtrees of the root

        Instances For

          Relation between two approximations of the cofix of a pfunctor that state they both contain the same data until one of them is truncated

          Instances For

            Given an infinite series of approximations approx, AllAgree approx states that they are all consistent with each other.

            Instances For

              truncate a turns a into a more limited approximation

              Equations
              Instances For
                def PFunctor.Approx.sCorec {F : PFunctor} {X : Type w} (f : XPFunctor.Obj F X) :
                X(n : ) → PFunctor.Approx.CofixA F n

                sCorec f i n creates an approximation of height n of the final coalgebra of f

                Equations
                Instances For

                  Path F provides indices to access internal nodes in Corec F

                  Instances For
                    structure PFunctor.MIntl (F : PFunctor) :

                    Internal definition for M. It is needed to avoid name clashes between M.mk and M.cases_on and the declarations generated for the structure

                    Instances For
                      def PFunctor.M (F : PFunctor) :

                      For polynomial functor F, M F is its final coalgebra

                      Instances For
                        theorem PFunctor.M.ext' (F : PFunctor) (x : PFunctor.M F) (y : PFunctor.M F) (H : ∀ (i : ), PFunctor.MIntl.approx x i = PFunctor.MIntl.approx y i) :
                        x = y
                        def PFunctor.M.corec {F : PFunctor} {X : Type u_1} (f : XPFunctor.Obj F X) (i : X) :

                        Corecursor for the M-type defined by F.

                        Instances For
                          def PFunctor.M.head {F : PFunctor} (x : PFunctor.M F) :
                          F.A

                          given a tree generated by F, head gives us the first piece of data it contains

                          Instances For

                            return all the subtrees of the root of a tree x : M F

                            Instances For

                              select a subtree using an i : F.Idx or return an arbitrary tree if i designates no subtree of x

                              Instances For

                                unfold an M-type

                                Instances For

                                  generates the approximations needed for M.mk

                                  Instances For

                                    constructor for M-types

                                    Instances For
                                      inductive PFunctor.M.Agree' {F : PFunctor} :
                                      PFunctor.M FPFunctor.M FProp

                                      Agree' n relates two trees of type M F that are the same up to depth n

                                      Instances For
                                        def PFunctor.M.cases {F : PFunctor} {r : PFunctor.M FSort w} (f : (x : PFunctor.Obj F (PFunctor.M F)) → r (PFunctor.M.mk x)) (x : PFunctor.M F) :
                                        r x

                                        destructor for M-types

                                        Instances For
                                          def PFunctor.M.casesOn {F : PFunctor} {r : PFunctor.M FSort w} (x : PFunctor.M F) (f : (x : PFunctor.Obj F (PFunctor.M F)) → r (PFunctor.M.mk x)) :
                                          r x

                                          destructor for M-types

                                          Instances For
                                            def PFunctor.M.casesOn' {F : PFunctor} {r : PFunctor.M FSort w} (x : PFunctor.M F) (f : (a : F.A) → (f : PFunctor.B F aPFunctor.M F) → r (PFunctor.M.mk { fst := a, snd := f })) :
                                            r x

                                            destructor for M-types, similar to casesOn but also gives access directly to the root and subtrees on an M-type

                                            Instances For
                                              theorem PFunctor.M.approx_mk {F : PFunctor} (a : F.A) (f : PFunctor.B F aPFunctor.M F) (i : ) :
                                              @[simp]
                                              @[simp]
                                              theorem PFunctor.M.cases_mk {F : PFunctor} {r : PFunctor.M FSort u_2} (x : PFunctor.Obj F (PFunctor.M F)) (f : (x : PFunctor.Obj F (PFunctor.M F)) → r (PFunctor.M.mk x)) :
                                              @[simp]
                                              theorem PFunctor.M.casesOn_mk {F : PFunctor} {r : PFunctor.M FSort u_2} (x : PFunctor.Obj F (PFunctor.M F)) (f : (x : PFunctor.Obj F (PFunctor.M F)) → r (PFunctor.M.mk x)) :
                                              @[simp]
                                              theorem PFunctor.M.casesOn_mk' {F : PFunctor} {r : PFunctor.M FSort u_2} {a : F.A} (x : PFunctor.B F aPFunctor.M F) (f : (a : F.A) → (f : PFunctor.B F aPFunctor.M F) → r (PFunctor.M.mk { fst := a, snd := f })) :
                                              PFunctor.M.casesOn' (PFunctor.M.mk { fst := a, snd := x }) f = f a x

                                              IsPath p x tells us if p is a valid path through x

                                              Instances For
                                                theorem PFunctor.M.isPath_cons {F : PFunctor} {xs : PFunctor.Approx.Path F} {a : F.A} {a' : F.A} {f : PFunctor.B F aPFunctor.M F} {i : PFunctor.B F a'} :
                                                PFunctor.M.IsPath ({ fst := a', snd := i } :: xs) (PFunctor.M.mk { fst := a, snd := f })a = a'
                                                theorem PFunctor.M.isPath_cons' {F : PFunctor} {xs : PFunctor.Approx.Path F} {a : F.A} {f : PFunctor.B F aPFunctor.M F} {i : PFunctor.B F a} :
                                                PFunctor.M.IsPath ({ fst := a, snd := i } :: xs) (PFunctor.M.mk { fst := a, snd := f })PFunctor.M.IsPath xs (f i)

                                                follow a path through a value of M F and return the subtree found at the end of the path if it is a valid path for that value and return a default tree

                                                Equations
                                                Instances For

                                                  similar to isubtree but returns the data at the end of the path instead of the whole subtree

                                                  Instances For
                                                    theorem PFunctor.M.children_mk {F : PFunctor} {a : F.A} (x : PFunctor.B F aPFunctor.M F) (i : PFunctor.B F (PFunctor.M.head (PFunctor.M.mk { fst := a, snd := x }))) :
                                                    PFunctor.M.children (PFunctor.M.mk { fst := a, snd := x }) i = x (cast (_ : PFunctor.B F (PFunctor.M.head (PFunctor.M.mk { fst := a, snd := x })) = PFunctor.B F a) i)
                                                    @[simp]
                                                    theorem PFunctor.M.isubtree_cons {F : PFunctor} [DecidableEq F.A] [Inhabited (PFunctor.M F)] (ps : PFunctor.Approx.Path F) {a : F.A} (f : PFunctor.B F aPFunctor.M F) {i : PFunctor.B F a} :
                                                    PFunctor.M.isubtree ({ fst := a, snd := i } :: ps) (PFunctor.M.mk { fst := a, snd := f }) = PFunctor.M.isubtree ps (f i)
                                                    @[simp]
                                                    theorem PFunctor.M.iselect_nil {F : PFunctor} [DecidableEq F.A] [Inhabited (PFunctor.M F)] {a : F.A} (f : PFunctor.B F aPFunctor.M F) :
                                                    PFunctor.M.iselect [] (PFunctor.M.mk { fst := a, snd := f }) = a
                                                    @[simp]
                                                    theorem PFunctor.M.iselect_cons {F : PFunctor} [DecidableEq F.A] [Inhabited (PFunctor.M F)] (ps : PFunctor.Approx.Path F) {a : F.A} (f : PFunctor.B F aPFunctor.M F) {i : PFunctor.B F a} :
                                                    PFunctor.M.iselect ({ fst := a, snd := i } :: ps) (PFunctor.M.mk { fst := a, snd := f }) = PFunctor.M.iselect ps (f i)
                                                    theorem PFunctor.M.corec_def {F : PFunctor} {X : Type u} (f : XPFunctor.Obj F X) (x₀ : X) :
                                                    theorem PFunctor.M.ext_aux {F : PFunctor} [Inhabited (PFunctor.M F)] [DecidableEq F.A] {n : } (x : PFunctor.M F) (y : PFunctor.M F) (z : PFunctor.M F) (hx : PFunctor.M.Agree' n z x) (hy : PFunctor.M.Agree' n z y) (hrec : ∀ (ps : PFunctor.Approx.Path F), n = List.length psPFunctor.M.iselect ps x = PFunctor.M.iselect ps y) :

                                                    Bisimulation is the standard proof technique for equality between infinite tree-like structures

                                                    Instances For
                                                      theorem PFunctor.M.nth_of_bisim {F : PFunctor} (R : PFunctor.M FPFunctor.M FProp) [Inhabited (PFunctor.M F)] (bisim : PFunctor.M.IsBisimulation R) (s₁ : PFunctor.M F) (s₂ : PFunctor.M F) (ps : PFunctor.Approx.Path F) :
                                                      R s₁ s₂PFunctor.M.IsPath ps s₁ PFunctor.M.IsPath ps s₂PFunctor.M.iselect ps s₁ = PFunctor.M.iselect ps s₂ a f f', PFunctor.M.isubtree ps s₁ = PFunctor.M.mk { fst := a, snd := f } PFunctor.M.isubtree ps s₂ = PFunctor.M.mk { fst := a, snd := f' } ((i : PFunctor.B F a) → R (f i) (f' i))
                                                      theorem PFunctor.M.eq_of_bisim {F : PFunctor} (R : PFunctor.M FPFunctor.M FProp) [Nonempty (PFunctor.M F)] (bisim : PFunctor.M.IsBisimulation R) (s₁ : PFunctor.M F) (s₂ : PFunctor.M F) :
                                                      R s₁ s₂s₁ = s₂
                                                      def PFunctor.M.corecOn {F : PFunctor} {X : Type u_2} (x₀ : X) (f : XPFunctor.Obj F X) :

                                                      corecursor for M F with swapped arguments

                                                      Instances For
                                                        theorem PFunctor.M.dest_corec {P : PFunctor} {α : Type u} (g : αPFunctor.Obj P α) (x : α) :
                                                        theorem PFunctor.M.bisim {P : PFunctor} (R : PFunctor.M PPFunctor.M PProp) (h : ∀ (x y : PFunctor.M P), R x ya f f', PFunctor.M.dest x = { fst := a, snd := f } PFunctor.M.dest y = { fst := a, snd := f' } ((i : PFunctor.B P a) → R (f i) (f' i))) (x : PFunctor.M P) (y : PFunctor.M P) :
                                                        R x yx = y
                                                        theorem PFunctor.M.bisim' {P : PFunctor} {α : Type u_2} (Q : αProp) (u : αPFunctor.M P) (v : αPFunctor.M P) (h : ∀ (x : α), Q xa f f', PFunctor.M.dest (u x) = { fst := a, snd := f } PFunctor.M.dest (v x) = { fst := a, snd := f' } ∀ (i : PFunctor.B P a), x', Q x' f i = u x' f' i = v x') (x : α) :
                                                        Q xu x = v x
                                                        theorem PFunctor.M.bisim_equiv {P : PFunctor} (R : PFunctor.M PPFunctor.M PProp) (h : ∀ (x y : PFunctor.M P), R x ya f f', PFunctor.M.dest x = { fst := a, snd := f } PFunctor.M.dest y = { fst := a, snd := f' } ((i : PFunctor.B P a) → R (f i) (f' i))) (x : PFunctor.M P) (y : PFunctor.M P) :
                                                        R x yx = y
                                                        theorem PFunctor.M.corec_unique {P : PFunctor} {α : Type u} (g : αPFunctor.Obj P α) (f : αPFunctor.M P) (hyp : ∀ (x : α), PFunctor.M.dest (f x) = f <$> g x) :
                                                        def PFunctor.M.corec₁ {P : PFunctor} {α : Type u} (F : (X : Type u) → (αX) → αPFunctor.Obj P X) :
                                                        αPFunctor.M P

                                                        corecursor where the state of the computation can be sent downstream in the form of a recursive call

                                                        Instances For
                                                          def PFunctor.M.corec' {P : PFunctor} {α : Type u} (F : {X : Type u} → (αX) → αPFunctor.M P PFunctor.Obj P X) (x : α) :

                                                          corecursor where it is possible to return a fully formed value at any point of the computation

                                                          Instances For