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 (см. определение и использование, например здесь ).

Объединение функции и доказательство ее инъективности может быть не лучшим способом, если вы не разрабатываете теорию инъективных функций.