sim*_*djo 1 theorem-proving coq
外延公理说，如果两个函数在域的每个参数上的动作相等，则它们是相等的。
Axiom func_ext_dep : forall (A : Type) (B : A -> Type) (f g : forall x, B x),
(forall x, f x = g x) -> f = g.
平等=的定理声明的两侧是命题平等（具有单个数据类型eq_refl构造函数）。使用这个公理可以证明f = a + b和g = b + a在命题上是相等的。
但是f和g显然不等于数据结构。
你能解释一下我在这里遗漏了什么吗？可能函数对象没有正常形式？
编辑：在评论中进一步讨论后，实际的混淆点是：
不会以同样的方式立即
match a with... = match b with给我吗？FalseS S Z = S Z
您可以对 进行模式匹配nat，但不能对函数进行模式匹配。依赖模式匹配是我们证明构造函数的注入性和不相交性的方式，而我们对函数唯一能做的就是应用它。（另请参阅我们如何知道所有 Coq 构造函数都是单射和不相交的？）
尽管如此，我希望下面的其余答案仍然具有指导意义。
来自评论：
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不是“显然不相等”，因为平等和其他一切一样，都与特定的解释有关。