mathlib documentation

data.​qpf.​multivariate.​constructions.​cofix

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 a 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 definecofix F αin terms of the M-type of the polynomial functorPofF. We define the relationMcongrand take its quotient as the definition ofcofix 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 (n + 1)Type u} [mvfunctor F] [q : mvqpf F] {α : typevec n} {β : Type u} :
(β → 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
theorem mvqpf.​corecF_eq {n : } {F : typevec (n + 1)Type u} [mvfunctor F] [q : mvqpf F] {α : typevec n} {β : Type u} (g : β → F ::: β)) (x : β) :

def mvqpf.​is_precongr {n : } {F : typevec (n + 1)Type u} [mvfunctor F] [q : mvqpf F] {α : typevec n} :
((mvqpf.P F).M α(mvqpf.P F).M α → Prop) → Prop

Characterization of desirable equivalence relations on M-types

Equations
def mvqpf.​Mcongr {n : } {F : typevec (n + 1)Type u} [mvfunctor F] [q : mvqpf F] {α : typevec n} :
(mvqpf.P F).M α(mvqpf.P F).M α → Prop

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

Equations
def mvqpf.​cofix {n : } (F : typevec (n + 1)Type u) [mvfunctor F] [q : mvqpf F] :
typevec nType u

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
@[instance]
def mvqpf.​inhabited {n : } {F : typevec (n + 1)Type u} [mvfunctor F] [q : mvqpf F] {α : typevec n} [inhabited (mvqpf.P F).A] [Π (i : fin2 n), inhabited (α i)] :

Equations
def mvqpf.​Mrepr {n : } {F : typevec (n + 1)Type u} [mvfunctor F] [q : mvqpf F] {α : typevec n} :
(mvqpf.P F).M α(mvqpf.P F).M α

maps every element of the W type to a canonical representative

Equations
def mvqpf.​cofix.​map {n : } {F : typevec (n + 1)Type u} [mvfunctor F] [q : mvqpf F] {α β : typevec n} :
α.arrow βmvqpf.cofix F αmvqpf.cofix F β

the map function for the functor cofix F

Equations
@[instance]
def mvqpf.​cofix.​mvfunctor {n : } {F : typevec (n + 1)Type u} [mvfunctor F] [q : mvqpf F] :

Equations
def mvqpf.​cofix.​corec {n : } {F : typevec (n + 1)Type u} [mvfunctor F] [q : mvqpf F] {α : typevec n} {β : Type u} :
(β → F ::: β))β → mvqpf.cofix F α

Corecursor for cofix F

Equations
def mvqpf.​cofix.​dest {n : } {F : typevec (n + 1)Type u} [mvfunctor F] [q : mvqpf F] {α : typevec n} :
mvqpf.cofix F αF ::: mvqpf.cofix F α)

Destructor for cofix F

Equations
def mvqpf.​cofix.​abs {n : } {F : typevec (n + 1)Type u} [mvfunctor F] [q : mvqpf F] {α : typevec n} :
(mvqpf.P F).M αmvqpf.cofix F α

Abstraction function for cofix F α

Equations
def mvqpf.​cofix.​repr {n : } {F : typevec (n + 1)Type u} [mvfunctor F] [q : mvqpf F] {α : typevec n} :
mvqpf.cofix F α(mvqpf.P F).M α

Representation function for cofix F α

Equations
def mvqpf.​cofix.​corec'₁ {n : } {F : typevec (n + 1)Type u} [mvfunctor F] [q : mvqpf F] {α : typevec n} {β : Type u} :
(Π {X : Type u}, (β → X)F ::: X))β → mvqpf.cofix F α

Corecursor for cofix F

Equations
def mvqpf.​cofix.​corec' {n : } {F : typevec (n + 1)Type u} [mvfunctor F] [q : mvqpf F] {α : typevec n} {β : Type u} :
(β → F ::: (mvqpf.cofix F α β)))β → mvqpf.cofix F α

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

Equations
def mvqpf.​cofix.​corec₁ {n : } {F : typevec (n + 1)Type u} [mvfunctor F] [q : mvqpf F] {α : typevec n} {β : Type u} :
(Π {X : Type u}, (mvqpf.cofix F α → X)(β → X)β → F ::: X))β → mvqpf.cofix F α

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

Equations
theorem mvqpf.​cofix.​dest_corec {n : } {F : typevec (n + 1)Type u} [mvfunctor F] [q : mvqpf F] {α : typevec n} {β : Type u} (g : β → F ::: β)) (x : β) :

def mvqpf.​cofix.​mk {n : } {F : typevec (n + 1)Type u} [mvfunctor F] [q : mvqpf F] {α : typevec n} :
F ::: mvqpf.cofix F α)mvqpf.cofix F α

constructor for cofix F

Equations

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 (n + 1)Type u} [mvfunctor F] [q : mvqpf F] {α : typevec 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 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 (n + 1)Type u} [mvfunctor F] [q : mvqpf F] {α : typevec n} (r : mvqpf.cofix F αmvqpf.cofix F α → Prop) (h : ∀ (x y : mvqpf.cofix F α), r x ymvfunctor.liftr (α.rel_last r) x.dest y.dest) (x 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 (n + 1)Type u} [mvfunctor F] [q : mvqpf F] {α : typevec n} (r : mvqpf.cofix F αmvqpf.cofix F α → Prop) (h : ∀ (x y : mvqpf.cofix F α), r x ymvfunctor.liftr' (α.rel_last' r) x.dest y.dest) (x 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 (n + 1)Type u} [mvfunctor F] [q : mvqpf F] {α : typevec n} {β : Type u_1} (Q : β → Prop) (u v : β → mvqpf.cofix F α) (h : ∀ (x : β), Q x(∃ (a : (mvqpf.P F).A) (f' : ((mvqpf.P F).drop.B a).arrow α) (f₀ f₁ : (mvqpf.P F).last.B amvqpf.cofix F α), (u x).dest = mvqpf.abs a, (mvqpf.P F).append_contents f' f₀ (v x).dest = mvqpf.abs a, (mvqpf.P F).append_contents 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 (n + 1)Type u} [mvfunctor F] [q : mvqpf F] {α : typevec n} (x : mvqpf.cofix F α) :

theorem mvqpf.​cofix.​dest_mk {n : } {F : typevec (n + 1)Type u} [mvfunctor F] [q : mvqpf F] {α : typevec n} (x : F ::: mvqpf.cofix F α)) :

theorem mvqpf.​cofix.​ext {n : } {F : typevec (n + 1)Type u} [mvfunctor F] [q : mvqpf F] {α : typevec n} (x y : mvqpf.cofix F α) :
x.dest = y.destx = y

theorem mvqpf.​cofix.​ext_mk {n : } {F : typevec (n + 1)Type u} [mvfunctor F] [q : mvqpf F] {α : typevec n} (x y : F ::: mvqpf.cofix F α)) :

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 n} {F' : typevec nType u} [mvfunctor F'] [is_lawful_mvfunctor F'] (R : (β.prod β).arrow (typevec.repeat n Prop)) (x : F' α) (f g : α.arrow β) (h : α.arrow (typevec.subtype_ R)) :

theorem mvqpf.​liftr_map_last {n : } {F : typevec (n + 1)Type u} [mvfunctor F] [is_lawful_mvfunctor F] {α : typevec n} {ι ι' : Type u} (R : ι' → ι' → Prop) (x : F ::: ι)) (f g : ι → ι') :
(∀ (x : ι), R (f x) (g x))mvfunctor.liftr' (α.rel_last' R) (mvfunctor.map (typevec.id ::: f) x) (mvfunctor.map (typevec.id ::: g) x)

theorem mvqpf.​liftr_map_last' {n : } {F : typevec (n + 1)Type u} [mvfunctor F] [is_lawful_mvfunctor F] {α : typevec n} {ι : Type u} (R : ι → ι → Prop) (x : F ::: ι)) (f : ι → ι) :
(∀ (x : ι), R (f x) x)mvfunctor.liftr' (α.rel_last' R) (mvfunctor.map (typevec.id ::: f) x) x

theorem mvqpf.​cofix.​abs_repr {n : } {F : typevec (n + 1)Type u} [mvfunctor F] [q : mvqpf F] {α : typevec n} (x : mvqpf.cofix F α) :
quot.mk mvqpf.Mcongr x.repr = x

theorem mvqpf.​corec_roll {n : } {F : typevec (n + 1)Type u} [mvfunctor F] [q : mvqpf F] {α : typevec n} {X Y : Type u} {x₀ : X} (f : X → Y) (g : Y → F ::: X)) :

theorem mvqpf.​cofix.​dest_corec' {n : } {F : typevec (n + 1)Type u} [mvfunctor F] [q : mvqpf F] {α : typevec n} {β : Type u} (g : β → F ::: (mvqpf.cofix F α β))) (x : β) :

theorem mvqpf.​cofix.​dest_corec₁ {n : } {F : typevec (n + 1)Type u} [mvfunctor F] [q : mvqpf F] {α : typevec n} {β : Type u} (g : Π {X : Type u}, (mvqpf.cofix F α → X)(β → X)β → F ::: X)) (x : β) :
(∀ (X Y : Type u) (f : mvqpf.cofix F α → X) (f' : β → X) (k : X → Y), g (k f) (k f') x = mvfunctor.map (typevec.id ::: k) (g f f' x))(mvqpf.cofix.corec₁ g x).dest = g id (mvqpf.cofix.corec₁ g) x

@[instance]
def mvqpf.​mvqpf_cofix {n : } {F : typevec (n + 1)Type u} [mvfunctor F] [q : mvqpf F] :

Equations