Since positive coinductive types in Coq are evil and break subject reduction, I am trying to develop the theory of the conatural numbers using the following negative formulation (within a module CoNat
):
CoInductive t : Set := mk { pred : option conat }.
Definition zero := {| pred := None |}.
Definition succ (x:t) := {| pred := Some x |}.
Ideally I would like, after defining the appropriate bisimilarity predicate equal : t -> t -> Prop
, to prove the constructive "omniscience" of the resulting setoid as shown in a preprint by Pradic-Brown. I have already done this exercise using the more typical positive formulation, so I know it should in principle be possible.
The problem is that I find it hard to do much at all with this type since i don't see how to define a usable bisimilarity predicate. My first attempt is to just recreate the usual positive formulation using the "constructors" zero
and succ
:
CoInductive equal : t -> t -> Prop :=
| equal_zero : equal zero zero
| equal_succ : forall x y, equal x y -> equal (succ x) (succ y).
But this is extremely hard to prove anything about! I cannot even see a way to prove reflexivity: I can reduce it to proving the essential lemma expand_eq : forall x, equal x {| pred := pred x |}
but this itself seems out of reach. My intuition is that this is because I cannot eliminate x:t
as I could with a positive definition, to see that it is either zero
or a successor, and that I need a proposition that is itself defined in terms of its negative projection(s) to match the type I am using.
But I can't find any way at all to write a negative formulation of equal
. The best I was able to come up with was
CoInductive equal (x y : t) : Prop :=
{
equal_pred : match pred x, pred y with
| Some x', Some y' => equal x' y'
| Some _, None => False
| None, Some _ => False
| None, None => True
end
}.
which, aside from being a big ugly mess, fails due to a non-strictly-positive occurrence of equal
(since x'
and y'
are not strictly a result of destructing x
and y
, but rather their optional-predecessors). If there is a better way to write this, I haven't thought of it yet.
Is there any way to do what I am trying to do here, or should I just give up and embrace the evil?