Defining and using bisimilarity for negatively-defined conatural numbers

Question

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?

Answer 1

You must recognize that you really have two mutually defined types here: conat and option conat. (In general, you should think of (co)inductives that recurse "through" a previously-defined parametrized (co)inductive as being mutually-(co)inductively defined, where one (or more) of the definitions just happens to have a name that is an application.) Clarifying this is important because the form of recursion used in the definition of the type is also how you're going to define further objects in terms of the type.

Since conat and option conat are mutually defined, there should be two mutually defined bisimilarity relations, one on conat and one on option conat. For fun (and lack of a good name otherwise), I will write the second with a parametrized inductive, too.

Inductive option_rel {A} (rel : A -> A -> Prop) : option A -> option A -> Prop :=
| Some_rel : forall x y, rel x y -> option_rel rel (Some x) (Some y)
| None_rel : option_rel rel None None.
CoInductive equal (x y : conat) : Prop := mk_equal {
  pred_equal : option_rel equal (pred x) (pred y)
}.

Effectively, I've just converted your attempt with match to use an inductive instead of a match, but now Coq can see that equal is strictly positive.

This relation now has reflexivity, as you want:

CoFixpoint equal_refl (x : conat) : equal x x :=
  mk_equal x x
    match pred x with
    | Some p => Some_rel equal p p (equal_refl p)
    | None => None_rel equal
    end.

Answer 2

This is not really an answer, but in case you decide not to use coinductive types at all, you can have a look at how the Brown-Pradic result is formalized in Martín Escardó's CantorSchroederBernstein Agda formalization, where N∞ is formalized as the type of decreasing sequences ℕ → 2.