coq - 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)).

这里的问题是=对类型本身进行操作......而且，即使这个定义可以被按摩成一个更好的定义，它也需要大量的管道。

标签： coq

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 中采用的方法（参见定义和用法，例如此处）。

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