从类型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)).
这里的问题是要=对类型本身进行操作，而且，即使可以将此定义简化为更好的定义，也将需要大量的管道。
一种方法是定义一个称为的属性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中采用的方法（请参见此处的定义和用法）。
除非开发了内射函数理论，否则将函数及其内射性捆绑在一起可能不是最好的方法。
本文收集自互联网，转载请注明来源。
如有侵权，请联系 [email protected] 删除。
我来说两句