functional-programming - 如何在 coq 中证明 "~(nat = False)"、 "~(nat = bool)"和 "~(nat = True)"

Question

以下两个命题很容易证明。

Theorem nat_eq_nat : nat = nat.
Proof.
  trivial.
Qed.

Theorem True_neq_False : ~(True = False).
Proof.
  unfold not.
  intros.
  symmetry in H.
  rewrite H.
  trivial.
Qed.

但是当我试图证明一个稍微不同的命题 ~(nat = False) 时，我发现重写策略不起作用。它报告

Error: Refiner was given an argument "fun x : Set => x" of type "Set -> Set" instead of "Set -> Prop".

所以我试着写一个引理。

Lemma Type_eq_prod : forall (a : Type) (b : Type), a = b -> (a -> b).
Proof.
  intros.
  rewrite <- H.
  trivial.
Qed.

Theorem nat_neq_False : ~(nat = False).
Proof.
  unfold not.
  intros.
  apply (Type_eq_prod nat False) in H.
  inversion H.
  apply 0. (*no subgoals left*)

到目前为止一切正常。但是当我尝试Qed它时，它报告了

Error: Illegal application (Type Error): 
The term "Type_eq_prod" of type "forall a b : Type, a = b -> a -> b"
cannot be applied to the terms
 "nat" : "Set"
 "False" : "Prop"
 "H" : "nat = False"
 "0" : "nat"
The 3rd term has type "nat = False" which should be coercible to
 "nat = False".

以下是另外两个让我卡住的命题。

Theorem nat_neq_bool : ~(nat = bool).
Proof.
  unfold not.
  intros.
Abort.

Theorem nat_neq_true : ~(nat = True).
Proof.
  unfold not.
  intros.
Abort.

我的问题是:

 1.Why the rewrite tactic doesn't work with proposition ~(nat = False).
 2.Why can't I Qed it when there is no subgoals.
 3.How to prove the aborted propositions above or is it possible to prove or prove the negates of them in coq.

Answer 1

1. 由于 Coq 处理其 Universe 的方式，重写策略不起作用，Prop , Set和 Type .有一种包含的概念，它允许使用 Prop好像它是一个 Set或 Type .这就是为什么你被允许写 nat = False首先，因为平等只允许在相同类型的事物之间。问题在于，对于 Coq，False : Prop不同于 False : Set . not用 False : Prop 定义，这意味着重写将产生不匹配，这解释了您收到的错误消息。

   以下是可行的类似方法。注意对 Set 的显式强制.

   Lemma nat_neq_False_2 : (nat = False) -> (False : Set).
   Proof.
     intros H.
     rewrite <- H.
     apply 0.
   Qed.
   
   Lemma nat_neq_False_3 : ~(nat = False).
   Proof.
     intros H.
     destruct (nat_neq_False_2 H).
   Qed.
   

2. 当您使用策略编写证明时，Coq 本质上是在内部构建一个证明术语，但并没有真正对其进行类型检查。从这个意义上说，它有点像元编程。一旦你点击 Qed ，由策略构建的术语被发送到类型检查器以确保它是正确的。大多数时候，策略会产生正确的证明，但每隔一段时间就会发现不被接受的证明，您的案例就是一个例子。

   打印的错误信息不是很清楚，但是可以通过使用命令 Set Printing All 更好地了解发生了什么。 ，这会导致 Coq 打印所有没有符号的术语和语句，并显示隐含的参数。这就是您的错误消息在执行此操作时的样子:

   Set Printing All.
   
   Lemma Type_eq_prod : forall (a : Type) (b : Type), a = b -> (a -> b).
   Proof.
     intros.
     rewrite <- H.
     trivial.
   Qed.
   
   Theorem nat_neq_False : ~(nat = False).
   Proof.
     unfold not.
     intros.
     apply (Type_eq_prod nat False) in H.
     inversion H.
     apply 0. (*no subgoals left*)
   Qed.
   
   
   (* Error: Illegal application (Type Error):  *)
   (* The term "Type_eq_prod" of type "forall a b : Type, @eq Type a b -> a -> b" *)
   (* cannot be applied to the terms *)
   (*  "nat" : "Set" *)
   (*  "False" : "Prop" *)
   (*  "H" : "@eq Set nat False" *)
   (*  "O" : "nat" *)
   (* The 3rd term has type "@eq Set nat False" which should be coercible to *)
   (*  "@eq Type nat False". *)
   

   在那里，我们可以看到问题是再次出现了全域不匹配:Type 中存在一个相等性。 , 而另一个在 Set .有几种方法可以解决这个问题；最简单的可能是将您的第一个定理更改为:

   Lemma Type_eq_prod : forall (a : Set) (b : Set), a = b -> (a -> b).
   

3. 这两个命题在 Coq 中都是可证明的。在 Coq 的基础理论中，唯一可以证明简单类型如 nat和 bool不同的是基数论点。因此，nat <> bool因为bool只有两个元素，而 nat不止于此。因此，通过证明 bool有两个元素，一个可以重写等式nat = bool找出 nat也应该有两个元素，然后利用它来得到一个矛盾。类似的论点将表明 nat <> True .