coq - 直觉定义中令人惊讶的隐含假设

Question

我正在尝试弄清楚让我吃惊的事情。考虑以下两个定义。

Require Import List.
Variable A:Type.

Inductive NoDup : list A -> Prop :=
  NoDup_nil : NoDup nil
| NoDup_cons : forall x l, ~ In x l -> NoDup l -> NoDup (x :: l).

Inductive Dup : list A -> Prop :=
  Dup_hd : forall x l, In x l -> Dup (x :: l)
| Dup_tl : forall x l, Dup l  -> Dup (x :: l).

我的第一直觉是他们说的是同一件事(但被否定了)。然而，@Arthur Azevedo De Amorim表明它们并不完全相同(or see here)。如果~ NoDup l -> Dup l那么一定是forall (a b:A), ~ a <> b -> a = b .因此，对 A 类型的额外假设如果有人使用 ~ NoDup 就会偷偷溜进来而不是 Dup在陈述一个人的证明目标时。

我试图找出引入这个额外假设的位置，以获得发生的事情的心智模型，所以下次我会亲自去看看。我目前的解释是

• 它是 ~ In x l NoDup_cons 的参数这是负责任的，因为
• ~ In x l只有在可以证明某个 x与列表中的第一个元素、列表中的第二个元素等不同

所以当我销毁一个术语 om type NoDup (_::_)我得到一个术语 ~ In _ _只能为类型 A 创建为此 ~ a <> b -> a = b必须持有。

问:这是一种不错的“非正式”思考方式，还是有更好的方式来理解它，这样我就不会再次掉进那个陷阱？

另外，我发现 Coq library contains NoDup 而不是 Dup , 所以也许有些引理比它们需要的弱，因为它们是使用 NoDup 制定的而不是 Dup .然而，它们可以用 Dup 来制定。因为~Dup l -> NoDup l .

Answer 1

我认为从这个例子中得出的教训是，在考虑直觉逻辑中的否定时需要更加小心。特别是，您的陈述“他们说同样的话(但被否定)”在经典逻辑中是有意义的:它意味着等价陈述中的任何一个 P <-> ~Q或 ~P <-> Q .然而，在直觉逻辑中，这两个陈述不是等价的，因此您必须更具体地确定这两个陈述中的哪一个(如果有的话)实际上是真的。

在这种情况下，NoDup l 是是真的相当于~ Dup l .一般不是Dup l是一个正规命题(回想一下命题 P 被称为正规命题如果 ~~P -> P ，在这种情况下很容易得出 P <-> ~~P 的结论)。因此，~ NoDup l相当于~~ Dup l ，这通常是一个比 Dup l 更弱的陈述.

思考两者之间差异的一种可能方法是:从 Dup l 的具体证明, 可以提取一对索引，使得 l 的相应条目是相等的(由于从 Prop 到 Type 消除的限制，在 Coq 中不是字面上的函数，但你绝对可以证明存在这样一对索引的引理)。另一方面，~ NoDup l的具体证明只是提供了一种方法来获取所谓的 NoDup l 的证据并从中得出矛盾 - 您不一定能从中提取任何特定的索引对。

(我同意标准库只有 NoDup 而没有 Dup 有点奇怪。)