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

Question

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

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

Answer 1

你想要的原则被称为功能外延性；它以最一般的形式说

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

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