我該如何說服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.將然後將其分成兩個目標。

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 "/\".產生解決了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. 

Answer 3

如果你有A /\ B /\ C作爲一個假設，你的目標是(A /\ B) /\ C，您可以使用戰術tauto。這種策略解決了命題演算中的所有重言式。還有一種策略firstorder可以用量詞解決一些公式。

如果您有A /\ B /\ C並且您想要通過(A /\ B) /\ C作爲引理的參數，那麼您需要多做一些工作。一種方法是設置(A /\ B) /\ C作爲中間目標，並證明這一點：

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

如果A，B和C大表達式，你可以使用一個複合的策略，以配合在假設H : 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