6

在我的证明中,我偶然发现了A /\ B /\ C假设中存在的问题,我需要证明(A /\ B) /\ C. 这些在逻辑上是完全一样的,但是 coq 不会用assumption..

我一直在通过应用公理来解决这些问题,但是有没有更优雅(和正确)的方法来处理这个问题?

4

3 回答 3

5

所以我的方法是定义我的引理,

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.

于 2012-06-01T11:09:31.463 回答
5

如果您有A /\ B /\ C一个假设,并且您的目标是(A /\ B) /\ C,则可以使用该策略tauto。这种策略解决了命题演算中的所有重言式。还有一种策略firstorder可以用量词解决一些公式。

如果你有A /\ B /\ C并且你想(A /\ B) /\ C作为一个引理的参数传递,你需要做更多的工作。一种方法是设定(A /\ B) /\ C一个中间目标并加以证明:

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

如果A,BC是大型表达式,您可以使用复合策略来匹配假设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?CSearchRewrite (_ /\ _ /\ _)forall x1 … xn, (?A /\ ?B /\ ?C) = ?Dforall x1 … xn, (?A /\ ?B /\ ?C) <-> ?D

Coq < SearchPattern (_ <-> (_ /\ _ /\ _))
and_assoc: forall A B C : Prop, (A /\ B) /\ C <-> A /\ B /\ C
于 2012-06-03T22:03:03.490 回答
3

作为一般提示,如果您怀疑有类似的东西很明显,请检查标准库。方法如下: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.
于 2012-06-01T15:54:49.740 回答