私はcoqに（A/\ B）/ \ C == A/\ B/\ Cを納得させるにはどうすればよいですか？

Question

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

私は公理を適用してこれらを解決していますが、これを処理するよりエレガントな（正しい）方法がありますか？

Answer 1

だから私はそれについて行ってきた方法は私の補題を定義することで、

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.

Answer 2

あなたが明白であることを疑うこのような何かを持っている場合、標準ライブラリを確認してください。 Locate "/\".は、今、私たちがスコープ内にあるものを参照してください、とand_assoc証人は意味合いあなたが興味を持っていることを見つけるために、コマンド、SearchAbout and.を発行することができ、私たちのためにNotationを解決し、応答を生成

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

事実：ここでは方法です。あなたは直感のから手がかりを得ることができます：intuition戦術は、この意味合いを単独で利用することができます。

Lemma conj_example : forall A B C D, 
    (A /\ B) /\ C -> (A /\ (B /\ C) -> D) -> D. 
Proof. intuition. Qed. 

Answer 3

あなたは前提としてA /\ B /\ Cを持って、そしてあなたの目標は(A /\ B) /\ Cであれば、あなたは戦術tautoを使用することができます。この手法は命題計算のすべてのトートロジーを解きます。いくつかの数式を数量子で解くことができる方針のfirstorderもあります。

A /\ B /\ Cがあり、(A /\ B) /\ Cを補題に引数として渡す場合は、もう少し作業する必要があります。あなたは仮説H : A /\ B /\ Cの上に一致するように、化合物の戦術を使用して、それにtauto戦術を適用することができ、

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

A、BとCが大きい式である場合は、次の一つの方法は、中間目標として(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（?A,?Bおよび?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