coq - 我该如何说服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.然后将其分为两个目标。

A /\ (B /\ C) -> (A /\ B) /\ C

(A /\ B) /\ C -> A /\ (B /\ C)

证明每个都大致相同。对于(1)，

intro Habc.从左手边的大小得到假设。

destruct Habc as [Ha Hbc]. destruct Hbc as [Hb Hc].以获取各个假设。

auto使用这些假设。

我把它留给你算出来(2)，但是非常相似。

然后 Qed.