使用Coq的案例证明

Question

我有一个简单的定理,我想通过案例证明.下面给出一个例子.

Goal forall a b : Set, a = b \/ a <> b.
Proof
  intros a b.
  ...

我将如何解决这个问题.而且,我究竟如何使用两个可能的相等值(True或False)来定义证明？

任何帮助,将不胜感激.谢谢,

Answer 1

我很确定Set在Coq 中s的相等性是不可判定的.原因(我的理解有限)将是它不是一个归纳定义的集合(因此,对你来说没有案例分析......),它也不是一个封闭的集合:每当你定义一个新的数据类型时,你创造一个新的居民家庭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