3

我有一个简单的定理，我想用案例证明来证明。下面给出一个例子。

目标 forall ab ：设置，a = b \/ a <> b。
证明
  介绍 a b.
  ...

我将如何解决这个问题。而且，我将如何使用相等的两个可能值（真或假）来定义证明？

任何帮助，将不胜感激。谢谢，

4

2 回答 2

7

我很确定Sets 的相等性在 Coq 中是不可判定的。原因（据我有限的理解）是它不是一个归纳定义的集合（所以，没有案例分析给你......），它也不是一个封闭的集合：每次定义一个新的数据类型时，你创建一个新的居民家庭Set。因此，证明您显示的目标的术语需要更新以反映这些新居民。

正如@hardmath 在他的评论中提到的那样，您可以使用Classical假设 ( Axiom classic : forall P:Prop, P \/ ~ P.) 来证明您的目标。

正如@Robin Green 在此处的评论中提到的那样，您可以证明这种类型的目标是确定相等的类型。为此，您可能希望从该decide equality策略中获得帮助。见：http ://coq.inria.fr/distrib/V8.4/refman/Reference-Manual011.html#@tactic121

于 2013-03-05T15:22:27.503 回答
4

您的问题涉及 Coq 的一个有趣方面：命题（即 的成员Prop）和布尔值（即 的成员）之间的区别bool。详细解释这种差异有点过于技术性，所以我将尝试专注于您的特定示例。

粗略地说，PropCoq 中的 a 不是像常规布尔值那样计算为Trueor的东西。False相反，Props 具有可以组合来推断事实的推理规则。使用这些，我们可以证明一个命题成立，或者证明它是矛盾的。使事情变得微妙的是，还有第三种可能性，即我们既不能证明也不能反驳这个命题。这是因为 Coq 是一个建设性的逻辑。最广为人知的结果之一是在 Coq 中无法证明被称为排中( ) 的熟悉推理原理：如果您断言，这意味着您可以证明或证明forall P : Prop, P \/ ~ PP \/ ~ PP~ P. 在不知道哪一个成立的情况下，您无法断言这一点。

事实证明，对于某些命题，我们可以证明它P \/ ~ P成立。例如，不难展示forall n m : nat, n = m \/ n <> m。按照上面的说法，这意味着对于每一对自然数，我们都可以证明它们相等或不相等。

另一方面，如果我们更改nat为Set，就像在您的示例中一样，那么我们将永远无法证明该定理。要了解原因，请考虑Set nat * nat自然数对。如果我们能够证明你的定理，那么它将遵循nat = nat * nat \/ nat <> nat * nat。同样，通过上面的评论，这意味着我们要么能够证明nat = nat * nat要么nat <> nat * nat。但是，由于两种类型之间存在双射，我们不能说假设是矛盾的nat = nat * nat，但是由于类型在语法上不相等，所以假设它们不同也是可以的。从技术上讲，命题的有效性nat = nat * nat独立于Coq 的逻辑。

如果您确实需要您提到的事实，那么您需要将排中断言为公理 ( Axiom classical : forall P, P \/ ~ P.)，这将允许您在\/没有任何一方的明确证明的情况下产生证明，并通过案例进行推理。然后你就可以用类似的东西来证明你的示例定理

介绍 a b. 破坏（经典（a = b））。
  左边。假设。
  正确的。假设。

希望这可以帮助。

于 2013-03-08T06:54:49.040 回答