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

Question

这里是 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 post
https://www.reddit.com/r/logic/comments/fxjypn/what_is_not_constructive_in_this_proof/

但我不明白it/didn不适合我。

那么，我想知道的是：

如何在 coq 中指定选择公理（prove/disprove 这个）？
一般来说，我将如何构造一个函数来为存在的目标提供见证？（我还想证明所有单射函数都有左逆）

Answer 1

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中一个proof的计算内容隐藏到一个Prop值中，只能被检查产生更多的Prop值。特别是，从计算的角度来看，这个公理是非常无害的，因为它只在 Prop 中产生值。还有更多非计算性的选择示例，例如全局选择，可以表示为：

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

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

Answer 2

这是一个完整脚本的答案（使用 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.

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

How do I prove an existential goal that asks for a certain function in Coq?

proof

coq