我如何证明在 Coq 中要求某个函数的存在目标？

如何解决我如何证明在 Coq 中要求某个函数的存在目标？

对 coq 完全陌生。

我知道证明存在目标的 exists 策略，但在这种情况下，它需要来自两个集合的函数映射。演示这种函数的语法是什么？

如果没有这样的功能，我将如何反驳这一点？（我会通过一个矛盾来假设，但是我如何提出一个矛盾的假设？）

上下文：试图找出所有满射函数都有右逆的证明。

1 subgoal
A,B : Set
f : A → B
H : ∀ b : B,∃ a : A,f a = b
______________________________________(1/1)
∃ g : B → A,∀ b : B,f (g b) = b

当然，函数 g 是否存在取决于接受选择公理，那么这在 coq 中体现在哪里？

我确实找到了这个解决方案：
https://gist.github.com/pedrominicz/0d9004b82713d9244b762eb250b9c808
以及相关的 reddit 帖子
https://www.reddit.com/r/logic/comments/fxjypn/what_is_not_constructive_in_this_proof/

但我不明白/不适合我。

所以，我想知道的是：

您如何在 coq 中指定选择公理（以证明/反驳这一点）？
一般来说，我将如何构建一个函数来为存在主义目标提供见证？（我还想证明所有单射函数都有左逆）

解决方法

Coq 类型理论中的选择公理有多种变体。您可以查看 Coq.Logic.ChoiceFacts 模块，了解各种公式及其相对能力的相当全面的列表。

据我所知，你的例子相当于函数选择公理。一种优雅的表述和假设方式如下。

Axiom functional_choice : forall (A : Type) (B : A -> Type),(forall x : A,inhabited (B x)) -> inhabited (forall x : A,B x).

inhabited 类型是一个归纳框，它将 Type 中证明的计算内容隐藏到一个 Prop 值中，该值只能被检查以产生更多的 Prop 值。特别是，从计算的角度来看，这个公理非常无害，因为它只在 Prop 中产生值。还有更多非计算性的选择示例，例如全局选择，可以表示为：

Axiom global_choice : forall (A : Type),inhabited A -> A.

这个允许凭空提取计算内容。

这是一个完整脚本的答案（使用 coq 8.13.2 测试）。默认情况下，Coq 没有加载选择公理，因此您需要明确说明您将使用它。

Require Import ClassicalChoice.

Lemma question (A B : Set) (f : A -> B) :
   (forall b,exists a,f a = b) -> exists g,forall b,f (g b) = b.
Proof.
intros H.
apply (choice (fun y x => f x = y)).
exact H.
Qed.