0 
(** **** 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 つのサブゴールが与えられました。証明する必要がある 2 番目のサブゴールは、最初のものよりも複雑です。

even (n + m + m)

ここで何が起こっているのですか？

4

3 に答える 3

1

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 でインスタンス化しました。証明を完了するには、最後にこのメタ変数の証人を与える必要があります。

2番目のアプローチは、mの値をインスタンス化して戦術を適用するだけですapply ev_ev__ev with (m := m) in H1.

ソフトウェア ファウンデーションhttps://softwarefoundations.cis.upenn.edu/lf-current/Tactics.htmlで戦術を適用する方法について詳しく見ることができます。

于 2019-05-26T01:14:15.687 に答える