我怎么说服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

如果你有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并将tauto策略应用于它.这是一种严厉的方法,在这种情况下过度杀伤,但在更复杂的情况下非常有用,在这种情况下,您希望自动化具有许多类似情况的证明.

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