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.