Proving a coinduction principle for co-natural numbers

Question

I have to admit that I'm not very good at coinduction. I'm trying to show a bisimulation principle on co-natural numbers, but I'm stuck on a pair of (symmetric) cases.

CoInductive conat :=
  | cozero : conat
  | cosucc : conat -> conat.

CoInductive conat_eq : conat -> conat -> Prop :=
  | eqbase : conat_eq cozero cozero
  | eqstep : forall m n, conat_eq m n -> conat_eq (cosucc m) (cosucc n).

Section conat_eq_coind.
  Variable R : conat -> conat -> Prop.

  Hypothesis H1 : R cozero cozero.
  Hypothesis H2 : forall (m n : conat), R (cosucc m) (cosucc n) -> R m n.

  Theorem conat_eq_coind : forall m n : conat,
    R m n -> conat_eq m n.
  Proof.
    cofix. intros m n H.
    destruct m, n.
    simpl in H1.
    - exact eqbase.
    - admit.
    - admit.
    - specialize (H2 H).
      specialize (conat_eq_coind _ _ H2).
      exact (eqstep conat_eq_coind).
  Admitted.
End conat_eq_coind.

This is what the context looks like when focused on the first admitted case:

1 subgoal
R : conat -> conat -> Prop
H1 : R cozero cozero
H2 : forall m n : conat, R (cosucc m) (cosucc n) -> R m n
conat_eq_coind : forall m n : conat, R m n -> conat_eq m n
n : conat
H : R cozero (cosucc n)
______________________________________(1/1)
conat_eq cozero (cosucc n)

Thoughts?

eponier eponier · Accepted Answer · 2017-07-11T09:13:05

I do not understand what you try to prove here. This is wrong. Take the trivial predicate that is always True for example.

Theorem conat_eq_coind_false :
  ~ forall (R : conat -> conat -> Prop) (H1 : R cozero cozero)
  (H2 : forall (m n : conat), R (cosucc m) (cosucc n) -> R m n)
  (m n : conat) (H3 : R m n), conat_eq m n.
Proof.
  intros contra.
  specialize (contra (fun _ _ => True) I (fun _ _ _ => I)
                     cozero (cosucc cozero) I).
  inversion contra.
Qed.

Proving a coinduction principle for co-natural numbers

1 Answers