6

私の証明では、A /\ B /\ C私の仮定に がある問題に出くわし、証明する必要があり(A /\ B) /\ Cます。これらは論理的にはまったく同じですが、coq はこれらを では解決しませんassumption.。

私は公理を適用してこれらを解決してきましたが、これを処理するためのよりエレガントな (そして正しい) 方法はありますか?

4

3 に答える 3

5

私が行ってきた方法は、補題を定義することです。

Lemma conj_assoc : forall A B C, A /\ (B /\ C) <-> (A /\ B) /\ C.

それは一方が他方を意味します。

intros. split.次に、これを 2 つの目標に分割します。

  1. A /\ (B /\ C) -> (A /\ B) /\ C
  2. (A /\ B) /\ C -> A /\ (B /\ C)

これらのそれぞれを証明することは、ほぼ同じです。(1)については、

  • intro Habc.左手サイズから仮定を得る。
  • destruct Habc as [Ha Hbc]. destruct Hbc as [Hb Hc]. 個々の仮定を取得します。
  • autoこれらの仮定を使用します。

(2) はあなたに任せますが、非常によく似ています。

それでQed.

于 2012-06-01T11:09:31.463 に答える
5

A /\ B /\ C仮定として があり、目標がである場合(A /\ B) /\ C、戦術 を使用できますtauto。このタクティックは、命題計算におけるすべてのトートロジーを解決します。firstorder量指定子を使っていくつかの式を解くことができる戦術もあります。

A /\ B /\ Cがあり、補題に引数として渡したい場合(A /\ B) /\ Cは、もう少し作業する必要があります。1 つの方法は(A /\ B) /\ C、中間目標として設定し、それを証明することです。

assert ((A /\ B) /\ C). tauto.

とが大きな式の場合、複合戦術を使用して仮説を照合し、Aそれにトート戦術を適用できます。これは手間のかかるアプローチであり、この場合はやり過ぎですが、多くの同様のケースで証明を自動化する必要がある、より複雑な状況では役立ちます。BCH : A /\ B /\ C

match type of H with ?x /\ ?y /\ ?z =>
  assert (x /\ (y /\ z)); [tauto | clear H]
end.

変換を実行する既知のレンマを適用する、より簡単な方法があります。

apply and_assoc in H.

ライブラリのドキュメントを参照すると、補題を見つけることができます。検索することもできます。これは同値であり、検索ツールは含意と同値を対象としているため、検索するのが最も簡単な補題ではありません。を使用SearchPattern (_ /\ _ /\ _).して、フォームのレンマを探すことができますforall x1 … xn, ?A /\ ?B /\ ?C(where ?A, ?Band?Cは任意の式です)。SearchRewrite (_ /\ _ /\ _)形式の補題を探すために使用できますforall x1 … xn, (?A /\ ?B /\ ?C) = ?D。残念ながら、これは私たちが求めているものを見つけられません。これは、形式の補題ですforall x1 … xn, (?A /\ ?B /\ ?C) <-> ?D。仕事とは何か

Coq < SearchPattern (_ <-> (_ /\ _ /\ _))
and_assoc: forall A B C : Prop, (A /\ B) /\ C <-> A /\ B /\ C
于 2012-06-03T22:03:03.490 に答える
3

一般的なヒントとして、明らかであると思われるこのようなものがある場合は、標準ライブラリを確認してください。方法は次のとおりです。私たちLocate "/\".のために解決する応答を生成します。Notation

Notation            Scope     
"A /\ B" := and A B  : type_scope
                      (default interpretation)

これで、コマンドを発行してSearchAbout and.、範囲内にあるものを確認しand_assoc、関心のある影響を確認できます。実際、直感からヒントを得ることができます。戦術はintuition、この影響を単独で利用できます。

Lemma conj_example : forall A B C D,
  (A /\ B) /\ C -> (A /\ (B /\ C) -> D) -> D.
Proof. intuition. Qed.
于 2012-06-01T15:54:49.740 に答える