共自然数の共導入原理を証明する

Question

私は共導入があまりよくないと認めなければなりません。私は共自然数で二重共鳴の原理を示すことを試みていますが、私は（対称の）対の場合についています。

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. 

これは最初の入院の場合に焦点を当てたときにコンテキストは次のようになります。

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) 

思考？

Answer 1

あなたがここで何を証明しようとしているのか分かりません。これは間違っています。たとえば、常にTrueという簡単な述語を取ってください。

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.