Collect independent results on functions.

Lebesgue/Set_theory/Set_fun.v

+(**
+This file is part of the Elfic library
+
+Copyright (C) Boldo, Clément, Martin, Mayero, Mouhcine
+
+This library is free software; you can redistribute it and/or
+modify it under the terms of the GNU Lesser General Public
+License as published by the Free Software Foundation; either
+version 3 of the License, or (at your option) any later version.
+
+This library is distributed in the hope that it will be useful,
+but WITHOUT ANY WARRANTY; without even the implied warranty of
+MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+COPYING file for more details.
+*)
+
+(** Operations on sets (properties). *)
+
+From Coq Require Import ClassicalChoice.
+
+Require Import Set_def.
+
+
+Section Fun_Facts0.
+
+Context {U1 U2 : Type}.
+
+(** Facts about same_fun. *)
+
+(** It is an equivalence binary relation. *)
+
+(* Useless?
+Lemma same_fun_refl :
+  forall (f : U1 -> U2),
+    same_fun f f.
+Proof.
+easy.
+Qed.
+*)
+
+(* Useful? *)
+Lemma same_fun_sym :
+  forall (f g : U1 -> U2),
+    same_fun f g -> same_fun g f.
+Proof.
+easy.
+Qed.
+
+Lemma same_fun_trans :
+  forall (f g h : U1 -> U2),
+    same_fun f g -> same_fun g h -> same_fun f h.
+Proof.
+intros f g h H1 H2 x; now rewrite (H1 x).
+Qed.
+
+End Fun_Facts0.
+
+
+Section Fun_Facts1.
+
+Context {U1 U2 : Type}.
+Variable f : U1 -> U2.
+
+(** Facts about injective*/surjective/bijective. *)
+
+Lemma injective_equiv : injective f <-> injective_alt f.
+Proof.
+split; intros Hf x1 y1 H1; auto.
+destruct (classic (x1 = y1)) as [H2 | H2]; try easy.
+contradict H1; auto.
+Qed.
+
+Lemma bijective_equiv : bijective f <-> bijective_alt f.
+Proof.
+split.
+(* *)
+intros [Hf1 Hf2] x2; destruct (Hf2 x2) as [x1 Hx1]; exists x1; split; try easy.
+intros y1 Hy1; apply Hf1; rewrite Hy1; easy.
+(* *)
+intros Hf; split.
+intros x1 y1 H1; destruct (Hf (f y1)) as [z1 [_ Hz1]]; apply eq_trans with z1;
+  [symmetry | ]; apply Hz1; easy.
+intros x2; destruct (Hf x2) as [x1 [Hx1 _]]; exists x1; easy.
+Qed.
+
+Lemma bijective_equiv_fun :
+  bijective f <->
+  exists g, (forall z1, compose g f z1 = z1) /\ (forall z2, compose f g z2 = z2).
+Proof.
+unfold compose; split.
+(* *)
+intros [Hf1 Hf2]; destruct (choice _ Hf2) as [g Hg].
+exists g; split; try easy.
+intros x1; apply Hf1; rewrite Hg; easy.
+(* *)
+intros [g [Hg1 Hg2]]; split.
+intros x1 y1 H1; rewrite <- (Hg1 x1), <- (Hg1 y1); f_equal; easy.
+intros x2; exists (g x2); auto.
+Qed.
+
+End Fun_Facts1.
+
+
+Section Fun_Facts2.
+
+(** Facts about composition of functions. *)
+
+Context {U1 U2 U3 U4 : Type}.
+Variable f12 : U1 -> U2.
+Variable f23 : U2 -> U3.
+Variable f34 : U3 -> U4.
+
+(* Useful? *)
+Lemma compose_assoc :
+  compose3 f34 f23 f12 = compose (compose f34 f23) f12.
+Proof.
+easy.
+Qed.
+
+Lemma image_compose_fun :
+  image (compose f23 f12) = fun A1 => image f23 (image f12 A1).
+Proof.
+apply fun_ext; intros A1; apply set_ext_equiv; split; intros x3 Hx3.
+induction Hx3 as [x1 Hx1]; easy.
+induction Hx3 as [x2 Hx2], Hx2 as [x1 Hx1].
+replace (f23 (f12 x1)) with (compose f23 f12 x1); easy.
+Qed.
+
+Lemma image_compose :
+  forall A1, image (compose f23 f12) A1 = image f23 (image f12 A1).
+Proof.
+rewrite image_compose_fun; easy.
+Qed.
+
+(* Useful? *)
+Lemma preimage_compose_fun :
+  preimage (compose f23 f12) = fun A3 => preimage f12 (preimage f23 A3).
+Proof.
+easy.
+Qed.
+
+Lemma preimage_compose :
+  forall A3, preimage (compose f23 f12) A3 = preimage f12 (preimage f23 A3).
+Proof.
+easy.
+Qed.
+
+End Fun_Facts2.