Coq 功能扩展性

Question

我有一个目标，我想重写一个函数体，但是一些函数参数妨碍了重写。我用身份函数重新创建了这种情况。

如果函数是Defined，那么它可以工作，但是当函数是一个参数，我有一个公理说明如何重写，我是无法重写。

我只能通过假设功能可扩展性来让它工作。是否可以在不假设功能可扩展性的情况下以某种方式重写？

Axiom functional_extensionality: forall {A B} (f g:A->B) , (forall x, f x = g x) -> f = g.

Variables A B : Type.
Variable f : A -> B.

Definition Id (x : B) := x.         (* here my function is Defined *)

Goal (fun x => Id (f x)) = f.       (* I'd like to rewrite inside the fun *)

Proof. auto. Qed.                   (* This works (eta reduction). *)

Variable Id' : B -> B.              (* Here I don't have the function definition *)
Axiom ID     : forall x, Id' x = x. (* only proof that it does the same thing *)
Goal (fun x => Id' (f x)) = f. 
Proof.
  rewrite ID.                       (* this doesnt work *)
  eauto using functional_extensionality, ID. (* but this works *)

Answer 1

不幸的是，如果不假设功能可扩展性，就不可能证明这一点； Coq 要求 fun x => Id' (f x)) = fun x => f x “定义地”成立。

这里的“定义上”是什么意思？简而言之，这意味着这两个术语在语法上 必须具有相同的范式。回想一下，在 Coq 中，每个项都有一个(主要)由 beta 缩减引起的范式。

然而，我们只知道 Id' x = x “判断”。因此，Coq 无法执行归约 Id' x ~> x，从而防止上述两项“定义上”变得相等。

这确实是 Coq 理论的局限性，据我所知，类型检查仍然是可判定的。

完成此证明的另一种方法是推导满足此等式的唯一函数是 fun x => x(参数化)。这将为您提供一个假设 Hid: ID' = (fun x => x)，您可以使用它来完成证明。不幸的是，Hid 在 Coq 内部是不可证明的。