# mathlib3documentation

data.qpf.multivariate.constructions.cofix

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

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

• cofix.mk - constructor
• cofix.dest - destructor
• cofix.corec - corecursor: useful for formulating infinite, productive computations
• cofix.bisim - bisimulation: proof technique to show the equality of possibly infinite values of cofix F α

## 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 [ACH19] for more details.

## Reference #

def mvqpf.corecF {n : } {F : typevec (n + 1) Type u} [mvfunctor F] [q : mvqpf F] {α : typevec 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
theorem mvqpf.corecF_eq {n : } {F : typevec (n + 1) Type u} [mvfunctor F] [q : mvqpf F] {α : typevec n} {β : Type u} (g : β F ::: β)) (x : β) :
x) = (mvqpf.repr (g x))
def mvqpf.is_precongr {n : } {F : typevec (n + 1) Type u} [mvfunctor F] [q : mvqpf F] {α : typevec n} (r : (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} (x y : (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 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 mvqpf.cofix
@[protected, instance]
def mvqpf.cofix.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} (g : α.arrow β) :
α β

the map function for the functor cofix F

Equations
@[protected, 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} (g : β F ::: β)) :
β α

Corecursor for cofix F

Equations
def mvqpf.cofix.dest {n : } {F : typevec (n + 1) Type u} [mvfunctor F] [q : mvqpf F] {α : typevec n} :
α 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 α α

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.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} (g : Π {X : Type u}, X) F ::: X)) (x : β) :
α

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} (g : β F ::: α β))) (x : β) :
α

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} (g : Π {X : Type u}, α X) X) β F ::: X)) (x : β) :
α

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 : β) :
x).dest = (g x)
def mvqpf.cofix.mk {n : } {F : typevec (n + 1) Type u} [mvfunctor F] [q : mvqpf F] {α : typevec n} :
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 α:

• holds for x y: R x y
• for any values x y that satisfy R, their root has the same shape and their children can be paired in such a way that they satisfy R.
theorem mvqpf.cofix.bisim_rel {n : } {F : typevec (n + 1) Type u} [mvfunctor F] [q : mvqpf F] {α : typevec n} (r : α α Prop) (h : (x y : α), r x y mvfunctor.map (typevec.id ::: quot.mk r) x.dest = mvfunctor.map (typevec.id ::: quot.mk r) y.dest) (x y : α) :
r x y x = 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 : α α Prop) (h : (x y : α), r x y mvfunctor.liftr (α.rel_last r) x.dest y.dest) (x y : α) :
r x y x = 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 : α α Prop) (h : (x y : α), r x y x.dest y.dest) (x y : α) :
r x y x = 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 : β α) (h : (x : β), Q x ( (a : (mvqpf.P F).A) (f' : ((mvqpf.P F).drop.B a).arrow α) (f₀ f₁ : (mvqpf.P F).last.B a α), (u x).dest = mvqpf.abs a, f' f₀ (v x).dest = mvqpf.abs a, f' f₁ (i : (mvqpf.P F).last.B a), (x' : β), Q x' f₀ i = u x' f₁ i = v x')) (x : β) :
Q x u 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 : α) :
theorem mvqpf.cofix.dest_mk {n : } {F : typevec (n + 1) Type u} [mvfunctor F] [q : mvqpf F] {α : typevec n} (x : F ::: α)) :
.dest = x
theorem mvqpf.cofix.ext {n : } {F : typevec (n + 1) Type u} [mvfunctor F] [q : mvqpf F] {α : typevec n} (x y : α) (h : x.dest = y.dest) :
x = y
theorem mvqpf.cofix.ext_mk {n : } {F : typevec (n + 1) Type u} [mvfunctor F] [q : mvqpf F] {α : typevec n} (x y : F ::: α)) (h : = ) :
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 n} {F' : Type u} [mvfunctor F'] (R : (β.prod β).arrow Prop)) (x : F' α) (f g : α.arrow β) (h : α.arrow ) (hh : = ) :
x) x)
theorem mvqpf.liftr_map_last {n : } {F : typevec (n + 1) Type u} [mvfunctor F] {α : typevec n} {ι ι' : Type u} (R : ι' ι' Prop) (x : F ::: ι)) (f g : ι ι') (hh : (x : ι), R (f x) (g x)) :
x) x)
theorem mvqpf.liftr_map_last' {n : } {F : typevec (n + 1) Type u} [mvfunctor F] {α : typevec n} {ι : Type u} (R : ι ι Prop) (x : F ::: ι)) (f : ι ι) (hh : (x : ι), R (f x) x) :
x) x
theorem mvqpf.cofix.abs_repr {n : } {F : typevec (n + 1) Type u} [mvfunctor F] [q : mvqpf F] {α : typevec n} (x : α) :
quot.mk mvqpf.Mcongr x.repr = x

tactic for proof by bisimulation

tactic for proof by bisimulation

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 ::: α β))) (x : β) :
x).dest = (g 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}, α X) X) β F ::: X)) (x : β) (h : (X Y : Type u) (f : α X) (f' : β X) (k : X Y), g (k f) (k f') x = (g f f' x)) :
x).dest = g id x
@[protected, instance]
def mvqpf.mvqpf_cofix {n : } {F : typevec (n + 1) Type u} [mvfunctor F] [q : mvqpf F] :
Equations