IndProp: ev_plus_plus

(** **** Exercise: 3 stars, standard, optional (ev_plus_plus)

    This exercise just requires applying existing lemmas.  No
    induction or even case analysis is needed, though some of the
    rewriting may be tedious. *)

Theorem ev_plus_plus : forall n m p,
  even (n+m) -> even (n+p) -> even (m+p).
Proof.
  intros n m p H1 H2.

Вот что я получил:

1 subgoal (ID 89)

n, m, p : nat
H1 : even (n + m)
H2 : even (n + p)
============================
even (m + p)

Я доказал предыдущую теорему:

Theorem ev_ev__ev : forall n m,
  even (n+m) -> even n -> even m.

И хотел применить его к H1, но

apply ev_ev__ev in H1.

выдает ошибку:

Error: Unable to find an instance for the variable m.

Почему он не может найти "м" в выражении even (n + m)? Как исправить?

Обновить

apply ev_ev__ev with (m:=m) in H1.

дает очень странный результат:

2 subgoals (ID 90)

n, m, p : nat
H1 : even m
H2 : even (n + p)
============================
even (m + p)

subgoal 2 (ID 92) is:
 even (n + m + m)

Я думал, что это преобразует гипотезу H1 в 2:

H11 : even n
H12 : even m

Но вместо этого он дал 2 подзадачи, вторая, которую нам нужно доказать, более сложна, чем исходная:

even (n + m + m)

Что тут происходит?

Источник

3 ответа

Решение

Заявление forall n m, even (n+m) -> even n -> even m. не означает, что "если мы имеем, что (n + m) является четным, то мы имеем и то, что n четное, и что m четное" (это неверно, рассмотрим n = m = 1). Вместо этого это означает, что "если мы имеем, что (n + m) является четным, и мы имеем, что n является четным, то мы имеем, что m является четным".

Нет возможности получить H11 : even n а также H12 : even m только из H1 : even (n + m) не предполагая противоречия. Я хотел бы предложить выяснить, как доказать свою теорему с ручкой и бумагой, прежде чем пытаться доказать это в Coq.

Источник

Дело в том, что Coq объединяет H1 с even n аргумент ev_ev__ev вместо even (n+m),

Вы можете сказать Coq точно, где вы хотите H1 идти и использовать _ подстановочные знаки для мест, где вы позволяете Coq проработать детали.

Вы, вероятно, хотели этот термин ev_ev__ev n m H1 с типом even n -> even m но твой apply произвел термин ev_ev__ev (n+m) m _ H1 что также оставило вам еще кое-что, чтобы доказать. Чтобы взглянуть на контекст доказательства, сделайте

Check ev_ev__ev (n+m) m _ H1.
Источник

Потому что Coq не может понять, какое значение он должен дать для m. Вы можете применить тактику eapply ev_ev__ev in H1. и увидеть цели

  n, m, p : nat
  H2 : even (n + p)
  H1 : even ?m
  ============================
  even (m + p)

subgoal 2 (ID 17) is:
 even (n + m + ?m)

Coq инстанцировал m мета-переменной? M, и вам нужно дать свидетельство для этой мета-переменной в конце, чтобы закончить доказательство.

Второй подход - просто применить тактику с созданием значения m apply ev_ev__ev with (m := m) in H1.

Вы можете узнать больше о применении с тактикой в ​​основах программного обеспечения https://softwarefoundations.cis.upenn.edu/lf-current/Tactics.html

Источник
Другие вопросы по тегам