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
cofix.mk- constructor- `cofix.dest - destructor
cofix.corec- corecursor: useful for formulating infinite, productive computationscofix.bisim- bisimulation: proof technique to show the equality of possibly infinite values ofcofix F α
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
- [Jeremy Avigad, Mario M. Carneiro and Simon Hudon, Data Types as Quotients of Polynomial Functors][avigad-carneiro-hudon2019]
def
mvqpf.corecF
{n : ℕ}
{F : typevec (n + 1) → Type u}
[mvfunctor F]
[q : mvqpf F]
{α : typevec n}
{β : Type u} :
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
- mvqpf.corecF g = mvpfunctor.M.corec (mvqpf.P F) (λ (x : β), mvqpf.repr (g x))
theorem
mvqpf.corecF_eq
{n : ℕ}
{F : typevec (n + 1) → Type u}
[mvfunctor F]
[q : mvqpf F]
{α : typevec n}
{β : Type u}
(g : β → F (α ::: β))
(x : β) :
mvpfunctor.M.dest (mvqpf.P F) (mvqpf.corecF g x) = mvfunctor.map (typevec.id ::: mvqpf.corecF g) (mvqpf.repr (g x))
def
mvqpf.is_precongr
{n : ℕ}
{F : typevec (n + 1) → Type u}
[mvfunctor F]
[q : mvqpf F]
{α : typevec n} :
Characterization of desirable equivalence relations on M-types
Equations
- mvqpf.is_precongr r = ∀ ⦃x y : (mvqpf.P F).M α⦄, r x y → mvqpf.abs (mvfunctor.map (typevec.id ::: quot.mk r) (mvpfunctor.M.dest (mvqpf.P F) x)) = mvqpf.abs (mvfunctor.map (typevec.id ::: quot.mk r) (mvpfunctor.M.dest (mvqpf.P F) y))
def
mvqpf.Mcongr
{n : ℕ}
{F : typevec (n + 1) → Type u}
[mvfunctor F]
[q : mvqpf F]
{α : typevec n} :
Equivalence relation on M-types representing a value of type cofix F
Equations
- mvqpf.Mcongr x y = ∃ (r : (mvqpf.P F).M α → (mvqpf.P F).M α → Prop), mvqpf.is_precongr r ∧ r x y
def
mvqpf.cofix
{n : ℕ}
(F : typevec (n + 1) → Type u)
[mvfunctor F]
[q : mvqpf F] :
typevec n → Type 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
- mvqpf.cofix F α = quot mvqpf.Mcongr
@[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)] :
inhabited (mvqpf.cofix F α)
Equations
- mvqpf.inhabited = {default := quot.mk mvqpf.Mcongr (inhabited.default ((mvqpf.P F).M α))}
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
- mvqpf.cofix.map g = quot.lift (λ (x : (mvqpf.P F).M α), quot.mk mvqpf.Mcongr (mvfunctor.map g x)) _
@[instance]
def
mvqpf.cofix.mvfunctor
{n : ℕ}
{F : typevec (n + 1) → Type u}
[mvfunctor F]
[q : mvqpf F] :
mvfunctor (mvqpf.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 α
Corecursor for cofix F
Equations
- mvqpf.cofix.corec g = λ (x : β), quot.mk mvqpf.Mcongr (mvqpf.corecF g x)
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
- mvqpf.cofix.dest = quot.lift (λ (x : (mvqpf.P F).M α), mvfunctor.map (typevec.id ::: quot.mk mvqpf.Mcongr) (mvqpf.abs (mvpfunctor.M.dest (mvqpf.P F) x))) mvqpf.cofix.dest._proof_1
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
- mvqpf.cofix.abs = quot.mk mvqpf.Mcongr
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
- mvqpf.cofix.corec'₁ g x = mvqpf.cofix.corec (λ (x : β), g id) x
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
- mvqpf.cofix.corec' g x = let f : (α ::: mvqpf.cofix F α).arrow (α ::: (mvqpf.cofix F α ⊕ β)) := typevec.id ::: sum.inl in mvqpf.cofix.corec (sum.elim (mvfunctor.map f ∘ mvqpf.cofix.dest) g) (sum.inr x)
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
- mvqpf.cofix.corec₁ g x = mvqpf.cofix.corec' (λ (x : β), g sum.inl sum.inr x) 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 : β) :
(mvqpf.cofix.corec g x).dest = mvfunctor.map (typevec.id ::: mvqpf.cofix.corec g) (g 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
- mvqpf.cofix.mk = mvqpf.cofix.corec (λ (x : F (α ::: mvqpf.cofix F α)), mvfunctor.map (typevec.id ::: λ (i : mvqpf.cofix F α), i.dest) x)
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 ythat satisfyR, their root has the same shape and their children can be paired in such a way that they satisfyR.
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 y → mvfunctor.map (typevec.id ::: quot.mk r) x.dest = mvfunctor.map (typevec.id ::: quot.mk r) y.dest)
(x y : mvqpf.cofix F α) :
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 : mvqpf.cofix F α → mvqpf.cofix F α → Prop)
(h : ∀ (x y : mvqpf.cofix F α), r x y → mvfunctor.liftr (α.rel_last r) x.dest y.dest)
(x y : mvqpf.cofix F α) :
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 : mvqpf.cofix F α → mvqpf.cofix F α → Prop)
(h : ∀ (x y : mvqpf.cofix F α), r x y → mvfunctor.liftr' (α.rel_last' r) x.dest y.dest)
(x y : mvqpf.cofix F α) :
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 : β → 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 a → mvqpf.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 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 : mvqpf.cofix F α) :
mvqpf.cofix.mk x.dest = x
theorem
mvqpf.cofix.dest_mk
{n : ℕ}
{F : typevec (n + 1) → Type u}
[mvfunctor F]
[q : mvqpf F]
{α : typevec n}
(x : F (α ::: mvqpf.cofix F α)) :
(mvqpf.cofix.mk x).dest = x
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 α)) :
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 n}
{F' : typevec n → Type u}
[mvfunctor F']
[is_lawful_mvfunctor F']
(R : (β.prod β).arrow (typevec.repeat n Prop))
(x : F' α)
(f g : α.arrow β)
(h : α.arrow (typevec.subtype_ R)) :
typevec.comp (typevec.subtype_val R) h = typevec.comp (typevec.prod.map f g) typevec.prod.diag → mvfunctor.liftr' R (mvfunctor.map f x) (mvfunctor.map 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 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
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)) :
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 (n + 1) → Type u}
[mvfunctor F]
[q : mvqpf F]
{α : typevec 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 (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] :
mvqpf (mvqpf.cofix F)
Equations
- mvqpf.mvqpf_cofix = {P := (mvqpf.P F).Mp, abs := λ (α : typevec n), quot.mk mvqpf.Mcongr, repr := λ (α : typevec n), mvqpf.cofix.repr, abs_repr := _, abs_map := _}