Coq 为单射函数定义类型构造函数

Question

从A 到B 类型的单射函数将不同的输入映射到不同的输出，但可能不会覆盖整个范围。

例如

f : ℕ -> ℕ
f = λx. 2*x

我正试图弄清楚如何在 Coq 中表达这样的事情。

我认为 Coq 谈论此类对象的方式是某种产品类型，其中一个元素是“原始”函数 A -> B 本身，另一个是该函数是单射的证明。

我不知道如何在 Coq 的语法中表达这一点......更具体地说，如何能够在相同“结构”中的类型定义中引用函数的名称以及类型类似产品的东西是最合适的。

我尝试在此处的省略号中添加一些内容，但无法捕获该函数。

Definition injection (A : Prop) (B: Prop) :=
  A -> B /\ ...

我不知道要在省略号中添加什么。

另一个没有捕捉到正确内容的示例定义是这样的：

Definition injection (A : Prop) (B: Prop) :=
  A * (not (A = A)) -> B * (not (B = B)).

这里的问题是 = 正在对类型本身进行操作......而且，即使可以将此定义修改为更好的定义，它也需要大量的管道。

Answer 1

一种方法是定义一个名为injective 的属性并将其作为条件添加到要求其函数为单射的引理：

Definition injective {A B} (f : A -> B) := forall x1 x2, f x1 = f x2 -> x1 = x2.

Lemma inj_comp {A B C} (f : B -> C) (g : A -> B) :
  injective f -> injective g -> injective (fun x => f (g x)).

这是 Mathcomp/SSReflect 中采用的方法（参见 definition 和用法，例如 here）。

捆绑一个函数并证明它的单射性可能不是最好的方法，除非您正在开发单射函数理论。