Documentation

Mathlib.Data.QPF.Multivariate.Constructions.Cofix

The final co-algebra of a multivariate qpf is again a qpf. #

For a (n+1)-ary QPF F (α₀,..,αₙ), we take the least fixed point of F with regards to its last argument αₙ. The result is an n-ary functor: Fix F (α₀,..,αₙ₋₁). Making Fix F into a functor allows us to take the fixed point, compose with other functors and take a fixed point again.

Main definitions #

Implementation notes #

For F a QPF, we define Cofix F α in terms of the M-type of the polynomial functor P of F. We define the relation Mcongr and take its quotient as the definition of Cofix F α.

Mcongr is taken as the weakest bisimulation on M-type. See [avigad-carneiro-hudon2019] for more details.

Reference #

def MvQPF.corecF {n : } {F : TypeVec.{u} (n + 1)Type u} [q : MvQPF F] {α : TypeVec.{u} n} {β : Type u} (g : βF (α ::: β)) :
β(MvQPF.P F).M α

corecF is used as a basis for defining the corecursor of Cofix F α. corecF uses corecursion to construct the M-type generated by q.P and uses function on F as a corecursive step

Equations
Instances For
    theorem MvQPF.corecF_eq {n : } {F : TypeVec.{u} (n + 1)Type u} [q : MvQPF F] {α : TypeVec.{u} n} {β : Type u} (g : βF (α ::: β)) (x : β) :
    def MvQPF.IsPrecongr {n : } {F : TypeVec.{u} (n + 1)Type u} [q : MvQPF F] {α : TypeVec.{u} n} (r : (MvQPF.P F).M α(MvQPF.P F).M αProp) :

    Characterization of desirable equivalence relations on M-types

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      def MvQPF.Mcongr {n : } {F : TypeVec.{u} (n + 1)Type u} [q : MvQPF F] {α : TypeVec.{u} n} (x : (MvQPF.P F).M α) (y : (MvQPF.P F).M α) :

      Equivalence relation on M-types representing a value of type Cofix F

      Equations
      Instances For
        def MvQPF.Cofix {n : } (F : TypeVec.{u} (n + 1)Type u) [MvQPF F] (α : TypeVec.{u} n) :

        Greatest fixed point of functor F. The result is a functor with one fewer parameters than the input. For F a b c a ternary functor, fix F is a binary functor such that

        Cofix F a b = F a b (Cofix F a b)
        
        Equations
        Instances For
          instance MvQPF.instInhabitedCofixOfAP {n : } {F : TypeVec.{u} (n + 1)Type u} [q : MvQPF F] {α : TypeVec.{u} n} [Inhabited (MvQPF.P F).A] [(i : Fin2 n) → Inhabited (α i)] :
          Equations
          • MvQPF.instInhabitedCofixOfAP = { default := Quot.mk MvQPF.Mcongr default }
          def MvQPF.mRepr {n : } {F : TypeVec.{u} (n + 1)Type u} [q : MvQPF F] {α : TypeVec.{u} n} :
          (MvQPF.P F).M α(MvQPF.P F).M α

          maps every element of the W type to a canonical representative

          Equations
          Instances For
            def MvQPF.Cofix.map {n : } {F : TypeVec.{u} (n + 1)Type u} [q : MvQPF F] {α : TypeVec.{u} n} {β : TypeVec.{u} n} (g : α.Arrow β) :
            MvQPF.Cofix F αMvQPF.Cofix F β

            the map function for the functor Cofix F

            Equations
            Instances For
              instance MvQPF.Cofix.mvfunctor {n : } {F : TypeVec.{u} (n + 1)Type u} [q : MvQPF F] :
              Equations
              def MvQPF.Cofix.corec {n : } {F : TypeVec.{u} (n + 1)Type u} [q : MvQPF F] {α : TypeVec.{u} n} {β : Type u} (g : βF (α ::: β)) :
              βMvQPF.Cofix F α

              Corecursor for Cofix F

              Equations
              Instances For
                def MvQPF.Cofix.dest {n : } {F : TypeVec.{u} (n + 1)Type u} [q : MvQPF F] {α : TypeVec.{u} n} :
                MvQPF.Cofix F αF (α ::: MvQPF.Cofix F α)

                Destructor for Cofix F

                Equations
                Instances For
                  def MvQPF.Cofix.abs {n : } {F : TypeVec.{u} (n + 1)Type u} [q : MvQPF F] {α : TypeVec.{u} n} :
                  (MvQPF.P F).M αMvQPF.Cofix F α

                  Abstraction function for cofix F α

                  Equations
                  Instances For
                    def MvQPF.Cofix.repr {n : } {F : TypeVec.{u} (n + 1)Type u} [q : MvQPF F] {α : TypeVec.{u} n} :
                    MvQPF.Cofix F α(MvQPF.P F).M α

                    Representation function for Cofix F α

                    Equations
                    Instances For
                      def MvQPF.Cofix.corec'₁ {n : } {F : TypeVec.{u} (n + 1)Type u} [q : MvQPF F] {α : TypeVec.{u} n} {β : Type u} (g : {X : Type u} → (βX)F (α ::: X)) (x : β) :

                      Corecursor for Cofix F

                      Equations
                      Instances For
                        def MvQPF.Cofix.corec' {n : } {F : TypeVec.{u} (n + 1)Type u} [q : MvQPF F] {α : TypeVec.{u} n} {β : Type u} (g : βF (α ::: (MvQPF.Cofix F α β))) (x : β) :

                        More flexible corecursor for Cofix F. Allows the return of a fully formed value instead of making a recursive call

                        Equations
                        Instances For
                          def MvQPF.Cofix.corec₁ {n : } {F : TypeVec.{u} (n + 1)Type u} [q : MvQPF F] {α : TypeVec.{u} n} {β : Type u} (g : {X : Type u} → (MvQPF.Cofix F αX)(βX)βF (α ::: X)) (x : β) :

                          Corecursor for Cofix F. The shape allows recursive calls to look like recursive calls.

                          Equations
                          Instances For
                            theorem MvQPF.Cofix.dest_corec {n : } {F : TypeVec.{u} (n + 1)Type u} [q : MvQPF F] {α : TypeVec.{u} n} {β : Type u} (g : βF (α ::: β)) (x : β) :
                            (MvQPF.Cofix.corec g x).dest = MvFunctor.map (TypeVec.id ::: MvQPF.Cofix.corec g) (g x)
                            def MvQPF.Cofix.mk {n : } {F : TypeVec.{u} (n + 1)Type u} [q : MvQPF F] {α : TypeVec.{u} n} :
                            F (α ::: MvQPF.Cofix F α)MvQPF.Cofix F α

                            constructor for Cofix F

                            Equations
                            Instances For

                              Bisimulation principles for Cofix F #

                              The following theorems are bisimulation principles. The general idea is to use a bisimulation relation to prove the equality between specific values of type Cofix F α.

                              A bisimulation relation R for values x y : Cofix F α:

                              theorem MvQPF.Cofix.bisim_rel {n : } {F : TypeVec.{u} (n + 1)Type u} [q : MvQPF F] {α : TypeVec.{u} n} (r : MvQPF.Cofix F αMvQPF.Cofix F αProp) (h : ∀ (x y : MvQPF.Cofix F α), r x yMvFunctor.map (TypeVec.id ::: Quot.mk r) x.dest = MvFunctor.map (TypeVec.id ::: Quot.mk r) y.dest) (x : MvQPF.Cofix F α) (y : MvQPF.Cofix F α) :
                              r x yx = y

                              Bisimulation principle using map and Quot.mk to match and relate children of two trees.

                              theorem MvQPF.Cofix.bisim {n : } {F : TypeVec.{u} (n + 1)Type u} [q : MvQPF F] {α : TypeVec.{u} n} (r : MvQPF.Cofix F αMvQPF.Cofix F αProp) (h : ∀ (x y : MvQPF.Cofix F α), r x yMvFunctor.LiftR (fun {i : Fin2 (n + 1)} => α.RelLast r) x.dest y.dest) (x : MvQPF.Cofix F α) (y : MvQPF.Cofix F α) :
                              r x yx = y

                              Bisimulation principle using LiftR to match and relate children of two trees.

                              theorem MvQPF.Cofix.bisim₂ {n : } {F : TypeVec.{u} (n + 1)Type u} [q : MvQPF F] {α : TypeVec.{u} n} (r : MvQPF.Cofix F αMvQPF.Cofix F αProp) (h : ∀ (x y : MvQPF.Cofix F α), r x yMvFunctor.LiftR' (α.RelLast' r) x.dest y.dest) (x : MvQPF.Cofix F α) (y : MvQPF.Cofix F α) :
                              r x yx = y

                              Bisimulation principle using LiftR' to match and relate children of two trees.

                              theorem MvQPF.Cofix.bisim' {n : } {F : TypeVec.{u} (n + 1)Type u} [q : MvQPF F] {α : TypeVec.{u} n} {β : Type u_1} (Q : βProp) (u : βMvQPF.Cofix F α) (v : βMvQPF.Cofix F α) (h : ∀ (x : β), Q x∃ (a : (MvQPF.P F).A) (f' : ((MvQPF.P F).drop.B a).Arrow α) (f₀ : (MvQPF.P F).last.B aMvQPF.Cofix F α) (f₁ : (MvQPF.P F).last.B aMvQPF.Cofix 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 xu x = v x

                              Bisimulation principle the values ⟨a,f⟩ of the polynomial functor representing Cofix F α as well as an invariant Q : β → Prop and a state β generating the left-hand side and right-hand side of the equality through functions u v : β → Cofix F α

                              theorem MvQPF.Cofix.mk_dest {n : } {F : TypeVec.{u} (n + 1)Type u} [q : MvQPF F] {α : TypeVec.{u} n} (x : MvQPF.Cofix F α) :
                              MvQPF.Cofix.mk x.dest = x
                              theorem MvQPF.Cofix.dest_mk {n : } {F : TypeVec.{u} (n + 1)Type u} [q : MvQPF F] {α : TypeVec.{u} n} (x : F (α ::: MvQPF.Cofix F α)) :
                              (MvQPF.Cofix.mk x).dest = x
                              theorem MvQPF.Cofix.ext {n : } {F : TypeVec.{u} (n + 1)Type u} [q : MvQPF F] {α : TypeVec.{u} n} (x : MvQPF.Cofix F α) (y : MvQPF.Cofix F α) (h : x.dest = y.dest) :
                              x = y
                              theorem MvQPF.Cofix.ext_mk {n : } {F : TypeVec.{u} (n + 1)Type u} [q : MvQPF F] {α : TypeVec.{u} n} (x : F (α ::: MvQPF.Cofix F α)) (y : F (α ::: MvQPF.Cofix F α)) (h : MvQPF.Cofix.mk x = MvQPF.Cofix.mk y) :
                              x = y

                              liftR_map, liftR_map_last and liftR_map_last' are useful for reasoning about the induction step in bisimulation proofs.

                              theorem MvQPF.liftR_map {n : } {α : TypeVec.{u_1} n} {β : TypeVec.{u_1} n} {F' : TypeVec.{u_1} nType u} [MvFunctor F'] [LawfulMvFunctor F'] (R : (β.prod β).Arrow (TypeVec.repeat n Prop)) (x : F' α) (f : α.Arrow β) (g : α.Arrow β) (h : α.Arrow (TypeVec.Subtype_ R)) (hh : TypeVec.comp (TypeVec.subtypeVal R) h = TypeVec.comp (TypeVec.prod.map f g) TypeVec.prod.diag) :
                              theorem MvQPF.liftR_map_last {n : } {F : TypeVec.{u} (n + 1)Type u} [q : MvQPF F] [lawful : LawfulMvFunctor F] {α : TypeVec.{u} n} {ι : Type u} {ι' : Type u} (R : ι'ι'Prop) (x : F (α ::: ι)) (f : ιι') (g : ιι') (hh : ∀ (x : ι), R (f x) (g x)) :
                              MvFunctor.LiftR' (α.RelLast' R) (MvFunctor.map (TypeVec.id ::: f) x) (MvFunctor.map (TypeVec.id ::: g) x)
                              theorem MvQPF.liftR_map_last' {n : } {F : TypeVec.{u} (n + 1)Type u} [q : MvQPF F] [LawfulMvFunctor F] {α : TypeVec.{u} n} {ι : Type u} (R : ιιProp) (x : F (α ::: ι)) (f : ιι) (hh : ∀ (x : ι), R (f x) x) :
                              MvFunctor.LiftR' (α.RelLast' R) (MvFunctor.map (TypeVec.id ::: f) x) x
                              theorem MvQPF.Cofix.abs_repr {n : } {F : TypeVec.{u} (n + 1)Type u} [q : MvQPF F] {α : TypeVec.{u} n} (x : MvQPF.Cofix F α) :
                              Quot.mk MvQPF.Mcongr x.repr = x

                              tactic for proof by bisimulation

                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                theorem MvQPF.corec_roll {n : } {F : TypeVec.{u} (n + 1)Type u} [q : MvQPF F] {α : TypeVec.{u} n} {X : Type u} {Y : Type u} {x₀ : X} (f : XY) (g : YF (α ::: X)) :
                                MvQPF.Cofix.corec (g f) x₀ = MvQPF.Cofix.corec (MvFunctor.map (TypeVec.id ::: f) g) (f x₀)
                                theorem MvQPF.Cofix.dest_corec' {n : } {F : TypeVec.{u} (n + 1)Type u} [q : MvQPF F] {α : TypeVec.{u} n} {β : Type u} (g : βF (α ::: (MvQPF.Cofix F α β))) (x : β) :
                                (MvQPF.Cofix.corec' g x).dest = MvFunctor.map (TypeVec.id ::: Sum.elim id (MvQPF.Cofix.corec' g)) (g x)
                                theorem MvQPF.Cofix.dest_corec₁ {n : } {F : TypeVec.{u} (n + 1)Type u} [q : MvQPF F] {α : TypeVec.{u} n} {β : Type u} (g : {X : Type u} → (MvQPF.Cofix F αX)(βX)βF (α ::: X)) (x : β) (h : ∀ (X Y : Type u) (f : MvQPF.Cofix F αX) (f' : βX) (k : XY), g (k f) (k f') x = MvFunctor.map (TypeVec.id ::: k) (g f f' x)) :
                                instance MvQPF.mvqpfCofix {n : } {F : TypeVec.{u} (n + 1)Type u} [q : MvQPF F] :
                                Equations