IndProp: ev_plus_plus - PullRequest
Новая
       19

IndProp: ev_plus_plus

0 голосов
/ 25 мая 2019 
(** **** 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.

Почему он не может найти "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 ]

2 голосов
/ 26 мая 2019

Утверждение 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.

1 голос
/ 26 мая 2019

Дело в том, что 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.
1 голос
/ 26 мая 2019

Потому что 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

...