在我的证明中,我偶然发现了A /\ B /\ C
假设中存在的问题,我需要证明(A /\ B) /\ C
. 这些在逻辑上是完全一样的,但是 coq 不会用assumption.
.
我一直在通过应用公理来解决这些问题,但是有没有更优雅(和正确)的方法来处理这个问题?
在我的证明中,我偶然发现了A /\ B /\ C
假设中存在的问题,我需要证明(A /\ B) /\ C
. 这些在逻辑上是完全一样的,但是 coq 不会用assumption.
.
我一直在通过应用公理来解决这些问题,但是有没有更优雅(和正确)的方法来处理这个问题?
所以我的方法是定义我的引理,
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.
如果您有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
作为一般提示,如果您怀疑有类似的东西很明显,请检查标准库。方法如下: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.