證明共同自然數的coinduction原理

Question

我不得不承認，我不是很擅長coinduction。我試圖在共自然數上展示一個互模擬原則，但我被困在一對（對稱）情況下。

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.