Awkwardness with coinductive universes

Using Coq
1

I’ve been playing with coinductive universes.

It’s very awkward to manipulate though.

I think my problem might be related to subject reduction?

I think I ought to refactor

CoInductive U :=
| const (T: Type)
| sum (_ _: U)
| prod (_ _: U)
.

To a style like

Variant Tag := Const | Sum | Prod.
CoInductive U := {
  tag: Tag ;
  const_u: if tag is Const then Type else Unit: Type ;
}.

Not quite sure how to handle sum/prod here but anyway the point is that cofix plays much nicer with record projections than pattern matching and so I should be able to have a more natural El implementation.

Really the whole deal is very awkward though and so I thought I should go here for advice.

2

Hi

I have found a technique for doing that kind of thing some time ago (I don’t claim any credit, but I haven’t seen it anywhere before in the context of handling “positive” coinductive types), not sure how widely known it is in the Coq community.

Here’s a proposal I made that contains a basic description of the technqiue: Convenient syntax sugar for coinductive types that could also possibly fix problems with positive coinductives · Issue #14020 · coq/coq · GitHub

In case of your universe, this would be

Inductive UX (X : Type) :=
    | ConstX (T : Type)
    | SumX   (u v : X)
    | ProdX  (u v : X).

CoInductive U : Type :=
{
    Out : UX U;
}.

Basically, you define the “base functor” of the type you want as an Inductive type (here it’s called UX). This base functor looks like the type you want to define (your original U), but it’s only “one layer deep”, i.e. you replace occurrences of the original U by the parameter X. Then, you tie the knot by defining a CoInductive type with one field that represents the fixpoint of the base functor (here this is U).

For convenience, you may then set implicit arguments and define smart constructors for your type, which will just refer to the constructors of the base functor.

Arguments ConstX {X} _.
Arguments SumX   {X} _ _.
Arguments ProdX  {X} _ _.

Definition Const (T : Type) : U :=
{|
    Out := ConstX T;
|}.

Definition Sum (u v : U) : U :=
{|
    Out := SumX u v;
|}.

Definition Prod (u v : U) : U :=
{|
    Out := ProdX u v;
|}.

Proofs by coinduction with this representation are pretty OK, and you can easily destruct an u : U using destruct u as [[T | u v | u v]] (note the double square brackets - you need to first destruct the coinductive, then the base functor).

Hope this helps. Any motivation for why you want coinductive universes? Any resources on that topic? The typical thing you do with a universe is defining an interpretation function El : U -> Type, but in your case you can’t use recursion for that, because U is not inductive, and you can’t use corecursion, because Type is not coinductive, so you’re kind of stuck.

1 Like
3

Your approach definitely seems usable and I’ll have to play with.

It’s more than a bit awkward but you can do something like.

#[universes(cumulative)]
Inductive El (u: U) :=
| El_const:
    (if is_const u is Some T then T else False) → El u
| El_pair:
    El (if is_prod u is Some (A, _) then A else const Empty_set) →
    El (if is_prod u is Some (_, B) then B else const Empty_set) →
    El u
| El_inl:
    El (if is_sum u is Some (A, _) then A else const Empty_set) →
    El u
| El_inr:
    El (if is_sum u is Some (_, B) then B else const Empty_set) →
    El u
.

So the main thing is I’ve been struggling with higher order abstract syntax lately and I thought experimenting with coinductive universes might help a bit. I’m not so sure the technique is so useful though