在 Coq 中生成一个函数，将每个证人输出到一个存在唯一性公理

Question

所以，我很确定这应该是没有选择的可能。也许我错了。

这是我正在尝试做的最小可重复示例：

Record MRE :=
{ set : Prop
; elem : set
; op : set -> set -> set
; subset : Prop
; subset_incl : subset -> set
; exist_axiom : forall (f : subset -> set), exists (x : set), f = fun y => op (subset_incl y) x
; uniq_axiom : forall (f : subset -> set), forall (x : set),
  f = (fun y => op (subset_incl y) x) -> x = ex_proj1 (exist_axiom f)
}.

我在这里使用了“内涵”平等，但我不确定这是否过于严格。为了做我想做的事，也许需要在唯一性公理的假设中使用“外延”等式。

本质上，我们有这个结构的一个子集，这样从子集到结构中的任何函数都可以使用内部操作op 来表示。确实是一个非常强大的属性。由于这种表示是唯一的，因此应该有一种方法可以生成从结构到自身的任何给定函数的“导数”。这就是我的意思：

Definition witness_fcn : forall (M : MRE),
  forall (f : set M -> set M),
  exists (fn : set M -> set M),
  forall (x : subset M),
  (fun y => f (op M (subset_incl M x) y)) = (fun y => op M (subset_incl M x) (fn y)).
Proof.
intros M f.
pose (fn0 := fun y => exist_axiom M (fun x => f (op M (subset_incl M x) y))).
exists (fun y => ex_proj1 (fn0 y)).
intros x.
unfold fn0.

我完全不确定如何从那里继续证明，或者我什至是否正确启动它。

This question 提出了类似的问题，但没有假设唯一性。该问题已回答here，但并未真正详细说明如何在证明中使用这样的唯一性属性。

假设，至少在常规数学中，它应该直接遵循fn0 的定义，但我不确定如何表达。

Answer 1

在您提到的两个链接中，问题是 Coq 在命题（Prop 类型的那些类型）和其他类型（Set 或 Type 类型的类型）之间强制执行的隔离，其想法是程序运行不需要证明。但是，在您的情况下，set M 和 subset M 都是命题，因此这种分离不是问题：正如您在定义 fn0 时所见，Coq 非常乐意使用您的存在类型的第一个组件来构建函数你正在寻找。这是建设性数学的一个好点：对Prop 和Type 之间的分离取模，选择就是正确的！

相反，问题来自证明的第二部分，即函数相等的证明。 Coq 的一个微妙问题是函数的相等性不是外延的，即以下公理通常不能被证明

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

我对此的直觉是，Coq 中的函数相等比输出相等更细粒度，因为它区分了以不同方式计算相同输出的函数。这有点明智，因为您可能希望区分具有不同复杂性的函数。然而，这通常被认为是一个缺陷，并且 Coq 类型理论的各种扩展/变体试图提供这个公理成立的系统。

使用这个公理，你的定理变得非常直接可证明（不是唯一性不起作用，只有存在）：

Definition witness_fcn : forall (M : MRE),
  forall (f : set M -> set M),
  exists (fn : set M -> set M),
  forall (x : subset M),
  (fun y => f (op M (subset_incl M x) y)) = (fun y => op M (subset_incl M x) (fn y)).
Proof.
intros M f.
pose (fn0 := fun y => exist_axiom M (fun x => f (op M (subset_incl M x) y))).
exists (fun y => ex_proj1 (fn0 y)).
intros x.
unfold fn0.
eapply fun_ext.
intros z.
destruct (fn0 z).
cbn.
etransitivity.
1: change (f (op M (subset_incl M x) z)) with ((fun x' => f (op M (subset_incl M x') z)) x) ; rewrite e.
all: reflexivity.
Defined.

我不完全确定你的定理在没有函数外延的情况下是不可证明的，但这对我来说似乎很有可能。如果你想避免它，你应该尝试摆脱函数的相等性。通常的做法是直接使用逐点相等，即将f = g替换为forall x, f x = g x。