Prouver un principe de coinduction pour les nombres co-naturels

Question

Je dois admettre que je ne suis pas très bon en coinduction. J'essaie de montrer un principe de bisimulation sur les nombres co-naturels, mais je suis coincé sur une paire de cas (symétriques).

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. 

C'est ce que le contexte ressemble lorsqu'elle se concentre sur le premier cas admis:

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) 

pensées?

Answer 1

Je ne comprends pas ce que vous essayez de prouver ici. C'est faux. Prenez le prédicat trivial qui est toujours True par exemple.

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.