coq - 证明函数应用在两个等价函数上的相等性

Question

我如何在 Coq 中证明以下内容？

Variables f g : nat->nat.
Hypothesis Hfg : forall x, f x = g x.
Variable F : (nat->nat)->nat.
Goal F f = F g.

我们有两个函数，f 和g，它们不一定相等，但它们是等价的。例如f x可以是0+x，g x可以是x+0。

F 返回一个 nat，并且由于 F 无法查看其函数参数，因此返回值应该与是否被馈送相同f 或 g。我如何证明这一点？

(相当于Proper (f_eq ==> eq) F的证明，其中f_eq = forall (f g:nat->nat), f x = g x )

---

在 Anton Trunov 的回答后编辑:我真的在问 expressive power Coq 的逻辑，所以我宁愿不添加公理，或证明这等同于其他公理的某种弱形式。例如，我认为这比 Functional Extensionality 弱.

Answer 1

可以使用功能扩展性来证明目标。

From Coq Require Import FunctionalExtensionality.

Section Foo.
Variables f g : nat->nat.
Hypothesis Hfg : forall x, f x = g x.
Variable F : (nat->nat)->nat.

Goal F f = F g.
Proof. now apply functional_extensionality in Hfg; subst. Qed.
End Foo.

但是这里真的有必要吗？答案是"is"，因为如果你有一般证明，你可以为 F 实例化它，这是身份函数，这意味着 (forall x, f x = g x) -> f = g。或者，更正式和更一般的情况:

Axiom axiom : forall A B C (f g : A -> B) (eqv : forall x, f x = g x)
              (F : (A -> B) -> C), F f = F g.

Lemma fun_ext A B (f g : A -> B) :
  (forall x, f x = g x) -> f = g.
Proof.
  intros eqv; apply (axiom A B _ f g eqv (fun x => x)).
Qed.