logic - 使用 Coq 的案例证明

Question

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

Goal forall a b : Set, a = b\/a <> b.
证明
介绍 a b.
...

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

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

Answer 1

我很确定 Set 的相等性s 在 Coq 中是不可判定的。原因(据我有限的理解)是它不是一个归纳定义的集合(所以，没有对你进行案例分析......)，而且它也不是一个封闭集:每次你定义一个新的数据类型时，你创建新的居民家庭Set .因此，证明您展示的目标的术语需要更新以反射(reflect)这些新居民。

正如@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