1

我不得不承认我不是很擅长共同归纳。我试图展示关于自然数的互模拟原理，但我被困在一对（对称）案例上。

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)

想法？

4

1 回答 1

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.
于 2017-07-11T09:13:05.503 回答