如何在 Coq 中隐式构建函数？

Question

我想证明每个群都有反函数。

我定义了一个组如下：

Record Group:Type := {
G:Set;
mult:G->G->G;
e:G;
assoc:forall x y z:G, mult x (mult y z)=mult (mult x y) z;
neut:forall x:G, mult e x=x /\ mult x e=x;
inverse:forall x:G,exists y:G, mult x y = e
}.

我知道最好用 inverse:forall x:G, {y: mult x y = e}. 甚至 inverse:G->G. is_inverse:forall x:G, mult x (inverse x)=e. 替换逆公理，但我更喜欢我的定义，主要是因为我希望定义与一个在教室里给的。

所以我已经包含了一个合适的选择公理版本：

Axiom indefinite_description : forall (A : Type) (P: A->Prop), ex P -> sig P.
Axiom functional_choice : forall A B (R:A->B->Prop), (forall x, exists y, R x y) -> (exists f, forall x, R x (f x)).

现在我可以证明我的主张了：

Lemma inv_func_exists(H:Group):exists inv_func:G H->G H, (forall x:G H, mult H x (inv_func(x))=e H).
generalize (inverse H).
apply functional_choice.
Qed.

既然证明了存在性，我想定义一个实际的函数。在这里，我觉得事情开始变得混乱。下面的定义创建了一个实际的函数，但看起来又丑又复杂：

Definition inv_func(H:Group):G H->G H.
pose (inv_func_exists H).
pose indefinite_description.
generalize e0 s.
trivial.
Qed.

最后，我想证明inv_func其实是一个反函数：

Lemma inv_func_is_inverse:forall (H:Group), forall x:(G H), mult H x (inv_func H x)=e H.

我可以看到 Coq 知道 inv_func 是如何定义的（例如 Print inv_func），但我不知道如何正式证明引理。

总而言之，对于如何证明最后一个引理以及定义 inv_func 的更好方法的建议，我将不胜感激（但根据我对组的定义，不包括在组定义。我相信这个问题在许多其他情况下可能是相关的，当人们可以证明每个元素的某种对应关系并且需要将这种对应关系构建为一个函数时）。

Answer 1

你的问题里面有不少问题。我将尝试解决所有这些问题：

首先，没有理由比 {x | P} 更喜欢 exists x, P + 描述，事实上，你这样做似乎很奇怪。 {x | P} 与 "there exists a x that can be computed" 一样完全有效，我宁愿在您的小组中使用该定义。
其次，在使用策略创建定义时，应使用命令Defined结束证明。使用 Qed 将声明定义 "Opaque"，这意味着它不能扩展，然后阻止你证明。
从定义中提取见证的方法是使用投影。在这种情况下，proj1_sig.

使用以上所有我们得出：

Definition inv_func' (H:Group) (x : G H) : G H.
Proof.
destruct (inverse H x) as [y _].
exact y.
Defined.

Definition inv_func (H:Group) (x : G H) : G H := proj1_sig (inverse H x).

Lemma inv_func_is_inverse (H:Group) (x: G H) : mult H x (inv_func H x) = e H.
Proof. now unfold inv_func; destruct (inverse H x). Qed.

如何在 Coq 中隐式构建函数？

How to build a function implicitly in Coq?

coq