Доказательство принципа коиндукции для натуральных чисел

Должен признать, что я не очень хорошо разбираюсь в коиндукции. Я пытаюсь показать принцип бисимуляции на натуральных числах, но я застрял на паре (симметричных) случаев.

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)

Мысли?


coq coq-tactic coinduction
person Carl Patenaude Poulin    schedule 10.07.2017    source источник

Ответы (1)


arrow_upward
1
arrow_downward

Я не понимаю, что вы пытаетесь здесь доказать. Это не правильно. Возьмем, к примеру, тривиальный предикат, который всегда 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.
person eponier    schedule 11.07.2017