私は造語があまり得意ではないことを認めなければなりません。共自然数の二重シミュレーションの原理を示そうとしていますが、(対称) ケースのペアで立ち往生しています。
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)
考え?