扩展性公理：为什么还不健全

Question

可扩展性公理说，如果两个函数在域的每个自变量上的作用相等，则它们相等。

Axiom func_ext_dep : forall (A : Type) (B : A -> Type) (f g : forall x, B x),
  (forall x, f x = g x) -> f = g.

定理语句两侧的

Equality =是命题相等（具有单个eq_refl构造函数的数据类型）。使用该公理可以证明f = a + b和g = b + a在命题上相等。

但是f和g显然不等于数据结构。

您能解释一下我在这里想念的吗？函数对象可能不具有正常形式吗？

Answer 1

从评论：

[AFAIU，=在Coq / CIC中具有非常精确的含义-正规形式的句法相等。

这是不对的。例如，我们可以证明以下内容：

Lemma and_comm : forall a b : bool, (* a && b = b && a *)
   match a with
   | true => b
   | false => false
   end = match b with
         | true => a
         | false => false
         end.
Proof.
  destruct a, b; reflexivity.
Qed.

[我们只能在语法上相等的两侧使用eq_refl，但是除了归纳命题的构造函数之外，还有更多的推理规则，尤其是依赖模式匹配，如果可以接受，则还有功能扩展性。

但是f和g显然不等于数据结构。

此陈述似乎混淆了可证明性和真实性。区分这两个世界很重要。 （而且我不是逻辑学家，所以请一言以蔽之。）

Coq是一个符号推送游戏，具有定义某些类型的术语的定义明确的规则。这是可证明的。当Coq接受证明时，我们所知道的就是我们按照规则构造了一个术语。

当然，我们还希望这些术语和类型有意义。当我们证明一个命题时，我们希望它能告诉我们一些有关世界状况的信息。这是真话。在某种程度上，Coq在这件事上几乎没有发言权。读f = g时，将给符号f赋予含义，给g赋予含义，也给=赋予含义。这完全取决于我们（嗯，总有规则要遵循），并且有不止一种解释（或“模型”）。

大多数人心目中的“天真模型”起着输入和输出之间的关系（也称为图）的作用。在此模型中，功能可扩展性成立：一个函数不过是输入和输出之间的映射，因此具有相同映射的两个函数相等。在Coq中功能扩展性是合理的（我们无法导出False），因为至少有一个有效的模型。

在您拥有的模型中，一个函数的特征在于其代码，对一些方程取模。 （这或多或少是“句法模型”，您可以在其中将每个表达式解释为本身，同时尽可能减少语义行为。）然后，实际上确实存在一些函数在扩展上是相等的，但是具有不同的代码。因此，扩展等式在此模型中无效，但这并不意味着它在Coq中是错误的（您可以证明其取反），如前所述。

[f和g不是“显然相等”，因为平等与其他所有事物一样，都是相对于特定的解释而言的。