如何证明函数相等，知道它们的身体相等？答案

【问题标题】：How to prove functions equal, knowing their bodies are equal?如何证明函数相等，知道它们的身体相等？
【发布时间】：2015-01-23 21:08:41
【问题描述】：

我们如何证明以下内容？：

Lemma forfun: forall (A B : nat->nat), (forall x:nat, A x = B x) ->
                                       (fun x => A x) = (fun x => B x).
Proof.

【问题讨论】：

@HoboSapiens 这是一个关于在 Coq 证明助手中编程的合理问题，参见。 Coq 标签上的其他相关问题。
@HoboSapiens：coq 是一种自动定理证明器，也是一种编程语言。（将鼠标悬停在coq 标签上：186 位关注者和 410 个问题在这里。）这个问题是关于如何使用 coq 语言，而不是如何证明一般的数学事实。也就是说，我认为它在 Math.SE 上不会不合适。

标签： coq proof

【解决方案1】：

您想要的原则称为功能扩展性；以最一般的形式，它说

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

不幸的是，尽管很有用，但这个原理独立独立于 Coq 的基本逻辑，这意味着无法证明或反驳它。然而，Coq 的逻辑被设计成可以安全地将这个原则假设为理论中的公理，并且Coq's standard library 已经定义了这个原则，以便您可以使用它。

【讨论】：