blob: c789e67039a1e51a5b852201ff4476981682ed77 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
|
From mathcomp Require Import ssreflect.
From Coq Require Export ssrfun.
From mathcomp Require Export ssrnotations.
(******************************************************************************)
(* Local additions: *)
(* void == a notation for the Empty_set type of the standard library. *)
(* of_void T == the canonical injection void -> T. *)
(******************************************************************************)
Lemma Some_inj {T : nonPropType} : injective (@Some T).
Proof. by move=> x y []. Qed.
Notation void := Empty_set.
Definition of_void T (x : void) : T := match x with end.
Lemma of_voidK T : pcancel (of_void T) [fun _ => None].
Proof. by case. Qed.
Lemma inj_compr A B C (f : B -> A) (h : C -> B) :
injective (f \o h) -> injective h.
Proof. by move=> fh_inj x y /(congr1 f) /fh_inj. Qed.
Definition injective2 (rT aT1 aT2 : Type) (f : aT1 -> aT2 -> rT) :=
forall (x1 x2 : aT1) (y1 y2 : aT2), f x1 y1 = f x2 y2 -> (x1 = x2) * (y1 = y2).
Arguments injective2 [rT aT1 aT2] f.
|
