在证明范围内定义函数

如何解决在证明范围内定义函数

我试图证明单射函数在 Coq 中是可逆的。在我的证明中，我的目标是一个“存在”命题。我想定义一个函数，该函数使用来自证明范围的术语（我之前介绍过的类型和函数），然后将该函数显示到“存在”目标。这是我目前所写的内容：

(* function composition *)
Definition fun_comp {A B C: Type} (f:A -> B) (g:B -> C) : A -> C :=
  fun a: A => g (f a).

Notation "g .o f" := (fun_comp f g) (at level 70).

Definition nonempty (A: Type) := exists a: A,a = a.

(* identity function for any given type *)
Definition fun_id (A: Type) := fun a: A => a.

(* left invertible *)
Definition l_invertible {A B: Type} (f: A -> B) :=
  exists fl:B->A,fl .o f = fun_id A.

Definition injective {A B: Type} (f: A -> B) :=
  forall a a':  A,f a = f a' -> a = a'.

(* is a given element in a function's image? *)
Definition elem_in_fun_image {A B: Type} (b: B) (f: A -> B) :=
  exists a: A,f a = b.

Theorem injective_is_l_invertible:
  forall (A B: Type) (f: A -> B),nonempty A /\ injective f -> l_invertible f.
Proof.
  intros A B f H.
  destruct H as [Hnempty Hinj].
  unfold l_invertible.
  unfold nonempty in Hnempty.
  destruct Hnempty as [a0].
  (* here would go my function definition and invoking "exists myfun" *)

这是我要定义的函数：

Definition fL (b: B) := if elem_in_fun_image b f 
                        then f a 
                        else a0.

这是证明窗口的样子：

 1 subgoal    
                                                    
A : Type
B : Type
f : A -> B
a0 : A
H : a0 = a0
Hinj : injective f

========================= (1 / 1)
                              
exists fl : B -> A,(fl .o f) = fun_id A     

我该怎么做？我对 Coq 很陌生，欢迎提出其他意见和建议。

解决方法

这个定义不能在基本逻辑中进行。您需要添加一些额外的公理：

$arrayToObject

目标是定义一个关系 (* from Coq.Logic.FunctionalExtensionality *) functional_extensionality : forall A B (f g : A -> B),(forall x,f x = g x) -> f = g (* from Coq.Logic.Classical *) classic : forall P : Prop,P \/ ~ P (* from Coq.Logic.ClassicalChoice *) choice : forall (A B : Type) (R : A->B->Prop),(forall x : A,exists y : B,R x y) -> exists f : A->B,R x (f x)). 来表征您要构造的左逆。存在量化的 R 然后将是相反的！您将需要 f 公理来显示 classic 的前提条件，并且您将需要函数外延性来显示您想要的等式。我将把它留作练习，以找出 choice 需要什么以及如何完成证明。

,

您的脚本应以以下行开头。

Require Import ClassicalChoice FunctionalEquality.

因为，正如@arthur-azevedo-de-amorim 所建议的，您将需要这些公理。

然后，您应该使用 choice 与关系“R y x”为 “f x = A 或者 A 中没有元素使得 f 的图像是 y”。

您将需要公理 classic 来证明 choice 所需的存在陈述：

assert (pointwise : forall y: B,exists x : A,f x = y \/ (forall x : A f x <> y)).

choice 将为您提供返回所需值的函数的存在性语句。你只需要说这个功能是对的。您可以通过键入 destruct (choice ... pointwise) 为该函数命名（您必须填写 ...）。

您必须证明两个函数之间的相等性，但使用公理 functional_extensionality，您可以将此问题简化为仅证明两个函数在任何 x 上相等。

对于那个 x，只需实例化函数的特征属性（由 destruct (choice ... pointwise) 产生， 值 f x。有一个分歧，但右手边的情况是自相矛盾的，因为显然 f x 对于某些 f x 来说是 x。

对于左侧的情况，您将得到形式的假设（我将 (choice ... pointwise) 产生的函数命名为 it：

f (it (f x)) = f x

在这里您可以应用您的注入假设。推断出it (f x) = x。

这几乎说明了证据。在我自己的实验中，我使用了 classic、NNP、not_all_ex_not、functional_extensionality，它们是来自 ClassicalChoice 的 FunctionalEquality 的引理。