Coq：如何在 lambda 中重写？

Question

基本上，我想证明以下引理，但我遇到了麻烦，因为我似乎无法直接重写 lambdas 内部。

但是我觉得这应该是可能的，因为如果我是 "inside" lambda，我可以很容易地证明它对于任何给定的 x。

Lemma lemma :
  forall {A B : Type} (f : A -> B) (g : A -> B), 
    (forall (x : A), f x = g x) -> (fun x => f x) = (fun x => g x).

Answer 1

您要证明的陈述（本质上）是函数扩展性，is well-known 在没有额外公理的情况下无法在 Coq 中证明。基本上，想法是 f 和 g 可以有意地非常不同（它们的定义看起来可能不同），但仍然采用相同的值。函数相等 (fun x => f x) = (fun x => g x) 将（没有任何附加公理）暗示这两个函数在句法上是相同的。

例如，取f(n) = 0和g(n) = 1 if x^(3 + n) + y^(3 + n) = z^(3 + n) has a non-trivial solution in integers, otherwise 0（都是从自然数到自然数的函数）。然后 f 和 g 是有意不同的 - 一个在句法上不会减少到另一个。然而，感谢 Andrew Wiles，我们知道 f 和 g 在扩展上是相同的，因为 g(n) = 0 对于所有 n。

您可以自由地将引理（或各种强化）作为公理添加到 Coq 而不必担心不一致。

Coq：如何在 lambda 中重写？

Coq: How to rewrite inside a lambda?

coq

coq-tactic