# Library CoLoR.Util.Function.FunUtil

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
• Frederic Blanqui, 2014-12-11
useful definitions and lemmas on functions

Set Implicit Arguments.

Some properties of functions.

Section functions.

Variables (A B : Type) (f : A -> B).

Definition injective := forall x y, f x = f y -> x = y.

Definition surjective := forall y, exists x, y = f x.

Definition bijective := injective /\ surjective.

End functions.

Function composition.

Section comp.

Variables (A B C : Type) (f : B -> C) (g : A -> B).

Definition comp x := f (g x).

Lemma inj_comp : injective f -> injective g -> injective comp.

Lemma inj_comp_elim : injective comp -> injective g.

Lemma surj_comp : surjective f -> surjective g -> surjective comp.

Lemma surj_comp_elim : surjective comp -> surjective f.

Lemma bij_comp : bijective f -> bijective g -> bijective comp.

End comp.

Infix "o" := comp (at level 70).

Inverse of a surjective function, using Hilbert's epsilon operator.

Section inverse.

Variables (A B : Type) (f : A -> B) (f_surj : surjective f).

Definition inverse : B -> A.

Lemma inverse_eq y : f (inverse y) = y.

Lemma inj_inverse : injective inverse.

End inverse.

Tactics for injectivity, surjective and bijectivity.

Ltac inj :=
match goal with
| |- injective (_ o _) => apply inj_comp; inj
| |- injective (inverse _) => apply inj_inverse; inj
| |- injective _ => auto
end.

Ltac surj :=
match goal with
| |- surjective (_ o _) => apply surj_comp; surj
| |- surjective _ => auto
end.

Ltac bij :=
match goal with
| |- bijective (_ o _) => apply bij_comp; bij
| |- bijective _ => hyp || (split; [inj | surj])
end.