Coq define a type constructor for injective functions

Question

An injective function from type A to B maps distinct inputs to distinct outputs, but might not cover the entire range.

e.g.

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

I'm trying to figure out how to express such a thing in Coq.

I think the Coq way of talking about such an object would be some kind of product type where one element is the is the "raw" function A -> B itself and another is a proof that said function is injective.

I don't know how to express this in the syntax of Coq though ... more specifically how to be able to refer to the name of the function in the definition of a type in the same "structure" and what kind of product-like thing is most appropriate.

I've tried putting a number of things in the ellpises here, but am not able to capture the function.

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

I'm stuck on what to put in the ellipses.

Another example definition that doesn't capture the right thing is something like this:

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

The problem here is that = is operating on the types themselves ... and, even if this definition could be massaged into a better one, it would require an obnoxious amount of plumbing.

Answer 1

One way is to define a property called injective and add it as a condition to the lemmas requiring their functions to be 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)).

This is the approach taken in Mathcomp/SSReflect (see the definition and a usage e.g. here).

Bundling a function and a proof of its injectivity might not be the best way to go, unless you are developing a theory of injective functions.