为什么 coq 无法识别 `None = Some v` 是 false？

Question

我有一个功能：

Fixpoint eval (fuel : nat) (env : environment) (e : exp) := 
  match fuel with 
    | 0       => None 
    | S fuel' => (...)
  end

我现在正在证明这个函数的一个性质，并且我有一个假设：

IHfuel : eval 0 env (IfThenElse e1 e2 e3) = Some v -> star red (Interm (IfThenElse e1 e2 e3, env)) (Result v)

我使用了

simpl in IHfuel.

策略，得到了：

IHfuel : None = Some v -> star red (Interm (IfThenElse e1 e2 e3, env)) (Result v)

现在我期望的是

None = Some v

是

False

，因此含义应该是微不足道的

True

。

Coq 似乎不同意。我什至尝试使用

destruct (Some v)

，看看它会做什么，它创建了两个目标：一个是：

IHfuel : None = Some v0 -> star red (Interm (IfThenElse e1 e2 e3, env)) (Result v)

另一个是：

IHfuel : None = None -> star red (Interm (IfThenElse e1 e2 e3, env)) (Result v)

为什么？我没想到

Some v

会分裂成

Some v0

和

None

...

Answer 1

你的问题提供了两件事：一是直接问题，二是总体上对 Coq 的一些更大的困惑。

为了回答直接问题，这就是为什么

destruct (Some v)

给你两种情况：这就是

destruct

的工作原理：它查看你正在破坏的东西的类型，然后对其进行大小写区分。在这种情况下，您正在对

option T

类型的内容进行大小写区分，因此您会得到新的目标，其中所有出现的

Some v

都被

None

或

Some v2

替换（对于新的

v2

） ， 分别。现在通常，您会破坏一个其他自由变量，或者可能是某些函数调用的结果（例如

n1 <=? n2

来区分

n1 <= n2

与

n1 > n2

，即区分它们的顺序）。正如您所注意到的，当您已经知道某物的形状时，

destruct

就没有多大意义了。

在间接问题中，您期望 Coq 在这里做某事，但它没有。不幸的是，您没有完全说出您期望发生的情况。所以这里是对发生的事情的解释，这样你也许就能发现你的思路哪里出了问题。

当您简化表达式时，Coq 会简化它。 Coq 中的归约是非常具体的事情，它基本上意味着您接受函数调用（或常量）并对它们进行更多评估。在您的示例中，这将

eval 0 env (IfThenElse e1 e2 e3)

评估为

None

，因为这就是该函数简化为的内容。一旦发生这种情况，您的术语就得到了充分的评估——其中没有进一步的函数调用。

现在，您似乎已经预料到平等

None = Some v

会以某种方式发生变化。然而，它永远不会：平等不是一个具有计算内容的函数。相反，它是一个“一流的”命题，不会进一步降低。作为一个命题，它可以是真或假，²但由于决定它是哪一个通常是不可判定的，所以你需要证明这一点。即使 Coq 有办法知道这个特定的等式是矛盾的，但这并不意味着它是

False

：在 Coq 的类型论中，一切都有类型，并且类型

False

与类型不同

None = Some v

。两者都可能没有居民，但这是一个非常特殊的极端情况。一般来说，你不能采用两种不同的类型，然后将一种类型更改为另一种类型，这不是事情的运作方式。

现在，

None = Some v

确实总是矛盾的，即没有证据证明它。这意味着它相当于

False

，但并不是说它是 相同。 要利用它的矛盾性，您可以使用

discriminate H

策略，假设您有一些假设

H : None = Some v

。所以 Coq 确实认识到这两个不相等，但你需要告诉它看。

但是，就您而言，没有什么可利用的。你有假设

IHfuel

，但它没有用，因为它（正如你所说）“微不足道”。从一个平凡的真实命题中无法获得任何有意义的信息，因此你无能为力。你可以把它变成

False -> ...

，但这没有用，因为你仍然无法对假设做任何事情。最有用的事情是将其从您的上下文中删除，即使用

clean IHfuel

。如果您仍然想在您的上下文中使用

IHfuel : True

，只需

pose proof (I:True) as IHfuel

（但这同样没有用）。

---

1：您实际上可以在逻辑中定义它，但这对您来说可能有点太先进了。

2：假设我们的逻辑是经典的，但 Coq 中不是。