Индпроп: 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.

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

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


coq logical-foundations
person user4035    schedule 25.05.2019    source источник
comment
Нет, вы не получите H11 и H12, применив ev_ev__ev. Вы можете получить только гипотезу even n -> even m.   -  person larsr    schedule 26.05.2019

Ответы (3)


arrow_upward
2
arrow_downward

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

person Jason Gross    schedule 26.05.2019

arrow_upward
1
arrow_downward

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

person keep_learning    schedule 26.05.2019
comment
@user4035 user4035 Извините, пару дней не проверял. Я не обращал внимания на детали доказательства, но был больше сосредоточен на том, чтобы убедиться, что применяемая тактика увенчалась успехом. - person keep_learning; 28.05.2019

arrow_upward
1
arrow_downward

Дело в том, что 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.
person larsr    schedule 26.05.2019