Library sset2
Require Import ssreflect ssrbool eqtype ssrnat ssrfun.
Set Implicit Arguments.
Unset Strict Implicit.
Import Prenex Implicits.
Require Export sset1.
Properties of the empty set
Lemma sub_emptyset : forall x,
sub x emptyset = (x = emptyset).
Proof.
move=> x; apply iff_eq; last by move=> -> ; fprops.
by move => h; empty_tac t tx; case (h _ tx); case.
Qed.
We say related r x y if the pair (x,y) is in the graph
Proposition 1: existence and uniqueness of range and domain
Theorem range_domain_exists: forall r,
is_graph r ->
(exists_unique (fun a=> (forall x, inc x a = (exists y, inc (J x y) r))) &
exists_unique (fun b=> (forall y, inc y b = (exists x, inc (J x y) r)))).
Proof.
move=> r g; split; split.
by exists (domain r); move=> t; dw.
by move=> x y Hx Hy; set_extens t; rewrite Hx Hy.
by exists (range r); move=> t; dw.
by move=> x y Hx Hy; set_extens t; rewrite Hx Hy.
Qed.
Lemma sub_graph_prod: forall r, is_graph r ->
sub r (product (domain r)(range r)).
Proof.
move=> r gr t tr.
have pt: is_pair t by apply gr.
by aw; dw; ee; ex_tac; rewrite pt.
Qed.
Lemma empty_graph1: forall r, is_graph r ->
(domain r = emptyset) = (r = emptyset).
Proof.
move=>r gr; apply iff_eq=> es; empty_tac t ts.
by empty_tac1 (P t); dw; ex_tac; rewrite gr.
move: ts; dw;rewrite // es; case=>y; apply emptyset_pr.
Qed.
Lemma empty_graph2: forall r, is_graph r ->
(range r = emptyset) = (r = emptyset).
Proof.
move=>r gr; apply iff_eq=> es; empty_tac t ts.
by empty_tac1 (Q t); dw; ex_tac; rewrite gr.
move: ts; rewrite range_rw // es; case=>y; apply emptyset_pr.
Qed.
is_graph r ->
(exists_unique (fun a=> (forall x, inc x a = (exists y, inc (J x y) r))) &
exists_unique (fun b=> (forall y, inc y b = (exists x, inc (J x y) r)))).
Proof.
move=> r g; split; split.
by exists (domain r); move=> t; dw.
by move=> x y Hx Hy; set_extens t; rewrite Hx Hy.
by exists (range r); move=> t; dw.
by move=> x y Hx Hy; set_extens t; rewrite Hx Hy.
Qed.
Lemma sub_graph_prod: forall r, is_graph r ->
sub r (product (domain r)(range r)).
Proof.
move=> r gr t tr.
have pt: is_pair t by apply gr.
by aw; dw; ee; ex_tac; rewrite pt.
Qed.
Lemma empty_graph1: forall r, is_graph r ->
(domain r = emptyset) = (r = emptyset).
Proof.
move=>r gr; apply iff_eq=> es; empty_tac t ts.
by empty_tac1 (P t); dw; ex_tac; rewrite gr.
move: ts; dw;rewrite // es; case=>y; apply emptyset_pr.
Qed.
Lemma empty_graph2: forall r, is_graph r ->
(range r = emptyset) = (r = emptyset).
Proof.
move=>r gr; apply iff_eq=> es; empty_tac t ts.
by empty_tac1 (Q t); dw; ex_tac; rewrite gr.
move: ts; rewrite range_rw // es; case=>y; apply emptyset_pr.
Qed.
A product is a special graph
Lemma sub_product_is_graph: forall u x y,
sub u (product x y) -> is_graph u.
Proof. move=> u x y su t tu; move: (su _ tu); aw; intuition. Qed.
Lemma product_is_graph: forall x y,
is_graph (product x y).
Proof. by move=> x y t; aw; intuition. Qed.
Hint Resolve product_is_graph: fprops.
Lemma product_related: forall x y a b,
related (product x y) a b = (inc a x & inc b y).
Proof. by rewrite /related=> x y a b; aw; apply iff_eq; intuition. Qed.
Lemma product_domain: forall x y,
nonempty y -> domain (product x y) = x.
Proof.
move=> x y [z] zy; set_extens t; rewrite domain0_rw.
by case=>p; aw; move=> [[ _ [u _]] v]; rewrite - v.
by move=> tx; exists (J t z); aw; fprops.
Qed.
Lemma product_range: forall x y,
nonempty x -> range (product x y) = y.
Proof.
move=> x y [z] zy; set_extens t; rewrite range0_rw.
by case=>p; aw; move=> [[ _ [ _ u ]] v]; rewrite - v.
by move=> tx; exists (J z t); aw; fprops.
Qed.
Lemma constant_function_p1: forall x y,
fgraph (product x (singleton y)).
Proof.
move=> x y; split; first by fprops.
move=> a b; aw; move=> [pa [_ qa]] [pb [ _ qb]] p.
by apply pair_exten=> //; rewrite qb.
Qed.
Lemma emptyset_graph: is_graph (emptyset).
Proof. by move=> t ; case; case. Qed.
Hint Resolve emptyset_graph : fprops.
Lemma emptyset_range: range emptyset = emptyset.
Proof. by rewrite empty_graph2; fprops. Qed.
Lemma emptyset_domain: domain emptyset = emptyset.
Proof. by rewrite empty_graph1; fprops. Qed.
Lemma emptyset_fgraph: fgraph emptyset.
Proof. by split; [fprops | move=> x y; case; case]. Qed.
Hint Rewrite emptyset_range emptyset_domain : sw.
Diagonal of a set: this is a functional graph x -> x
Definition diagonal x := Zo (product x x)(fun y=> P y = Q y).
Lemma diagonal_is_identity: forall x, diagonal x = identity_g x.
Proof.
rewrite /identity_g /diagonal /L => x.
set_extens t; rewrite Z_rw; aw.
by move=> [[pt [Pt _]] eql]; exists (P t); rewrite {3} eql; aw; auto.
by move=> [z [zx eql]]; rewrite - eql; aw; fprops.
Qed.
Lemma inc_diagonal_rw: forall x u,
inc u (identity_g x) = (is_pair u & inc (P u) x & P u = Q u).
Proof.
move=> x y; rewrite -diagonal_is_identity /diagonal Z_rw; aw.
by apply iff_eq ; [| move=> [? [? ]] <- ]; intuition.
Qed.
Lemma inc_pair_diagonal: forall x u v,
inc (J u v) (identity_g x) = (inc u x & u = v).
Proof. by move=> x u v; rewrite inc_diagonal_rw; aw; apply iff_eq; intuition.
Qed.
Hint Rewrite inc_pair_diagonal : aw.
Lemma identity_graph: forall x, is_graph (identity_g x).
Proof. by move => x; case (identity_fgraph x). Qed.
Hint Resolve identity_graph : fprops.
For Bourbaki, a correspondence between A and B is a triple (G,A,B),
graph, source and target, with constraints.
We use a record, convertible to a triple
A triple (G,A,B) or a record F is a correspondence only if
G is a subset of the product of A and B. This can be restated as:
G is a graph, domain and range are subsets of source and target
Definition is_triple f := is_pair f & is_pair (Q f).
Definition source x := P (Q x).
Definition target x := Q (Q x).
Definition graph x := P x.
Definition corresp s t g := J g (J s t).
Definition is_correspondence f :=
is_triple f & sub (graph f) (product (source f) (target f)).
Lemma corr_propcc: forall s t g,
sub g (product s t) = (is_graph g & sub (domain g) s & sub (range g) t).
Proof.
move=> s t g; apply iff_eq => [sg | [gg [sd sr]] x xg ].
move: (sub_product_is_graph sg)=> gg; split =>//.
by split; move=> z; dw; move=> [y pg]; move: (sg _ pg); aw; intuition.
move: (gg _ xg) => px; aw; ee.
by apply sd; apply inc_pr1_domain.
by apply sr; apply inc_pr2_range.
Qed.
Lemma corr_propc: forall f, let g := graph f in
is_correspondence f ->
(is_graph g & sub (domain g) (source f) & sub (range g) (target f)).
Proof. move=> f g [tf sg]; by rewrite - corr_propcc. Qed.
Lemma is_triple_corr: forall s t g, is_triple (corresp s t g).
Proof. by rewrite/corresp=> s t g; split; [| aw]; fprops. Qed.
Lemma corresp_recov: forall f, is_triple f ->
corresp (source f) (target f) (graph f) = f.
Proof.
rewrite /corresp /source /target /graph => f [pf pqf].
by apply pair_exten;aw; fprops.
Qed.
Lemma corresp_recov1: forall f, is_correspondence f ->
corresp (source f) (target f) (graph f) = f.
Proof. by move => f [t _]; apply corresp_recov. Qed.
Lemma corresp_source: forall s t g, source (corresp s t g) = s.
Proof. rewrite /corresp /source=> s t g; aw. Qed.
Lemma corresp_target: forall s t g, target (corresp s t g) = t.
Proof. rewrite /corresp /target=> s t g; aw. Qed.
Lemma corresp_graph: forall s t g, graph (corresp s t g) = g.
Proof. rewrite /corresp /graph=> s t g; aw. Qed.
Hint Rewrite corresp_source corresp_target corresp_graph : aw.
Lemma corresp_create: forall s t g,
sub g (product s t) -> is_correspondence (corresp s t g).
Proof. by move=> s t g h; split; [apply is_triple_corr | aw ]. Qed.
Definition source x := P (Q x).
Definition target x := Q (Q x).
Definition graph x := P x.
Definition corresp s t g := J g (J s t).
Definition is_correspondence f :=
is_triple f & sub (graph f) (product (source f) (target f)).
Lemma corr_propcc: forall s t g,
sub g (product s t) = (is_graph g & sub (domain g) s & sub (range g) t).
Proof.
move=> s t g; apply iff_eq => [sg | [gg [sd sr]] x xg ].
move: (sub_product_is_graph sg)=> gg; split =>//.
by split; move=> z; dw; move=> [y pg]; move: (sg _ pg); aw; intuition.
move: (gg _ xg) => px; aw; ee.
by apply sd; apply inc_pr1_domain.
by apply sr; apply inc_pr2_range.
Qed.
Lemma corr_propc: forall f, let g := graph f in
is_correspondence f ->
(is_graph g & sub (domain g) (source f) & sub (range g) (target f)).
Proof. move=> f g [tf sg]; by rewrite - corr_propcc. Qed.
Lemma is_triple_corr: forall s t g, is_triple (corresp s t g).
Proof. by rewrite/corresp=> s t g; split; [| aw]; fprops. Qed.
Lemma corresp_recov: forall f, is_triple f ->
corresp (source f) (target f) (graph f) = f.
Proof.
rewrite /corresp /source /target /graph => f [pf pqf].
by apply pair_exten;aw; fprops.
Qed.
Lemma corresp_recov1: forall f, is_correspondence f ->
corresp (source f) (target f) (graph f) = f.
Proof. by move => f [t _]; apply corresp_recov. Qed.
Lemma corresp_source: forall s t g, source (corresp s t g) = s.
Proof. rewrite /corresp /source=> s t g; aw. Qed.
Lemma corresp_target: forall s t g, target (corresp s t g) = t.
Proof. rewrite /corresp /target=> s t g; aw. Qed.
Lemma corresp_graph: forall s t g, graph (corresp s t g) = g.
Proof. rewrite /corresp /graph=> s t g; aw. Qed.
Hint Rewrite corresp_source corresp_target corresp_graph : aw.
Lemma corresp_create: forall s t g,
sub g (product s t) -> is_correspondence (corresp s t g).
Proof. by move=> s t g h; split; [apply is_triple_corr | aw ]. Qed.
Some properties of a correspondence
Lemma corresp_is_graph: forall g,
is_correspondence g -> is_graph (graph g).
Proof. move=> g cg; move: (corr_propc cg); intuition. Qed.
Lemma corresp_sub_range: forall g,
is_correspondence g -> sub (range (graph g)) (target g).
Proof. move=> g cg; move: (corr_propc cg); intuition. Qed.
Lemma corresp_sub_domain: forall g,
is_correspondence g -> sub (domain (graph g)) (source g).
Proof. by move=> g cg; move: (corr_propc cg); intuition. Qed.
Hint Resolve corresp_sub_range corresp_sub_domain corresp_is_graph: fprops.
is_correspondence g -> is_graph (graph g).
Proof. move=> g cg; move: (corr_propc cg); intuition. Qed.
Lemma corresp_sub_range: forall g,
is_correspondence g -> sub (range (graph g)) (target g).
Proof. move=> g cg; move: (corr_propc cg); intuition. Qed.
Lemma corresp_sub_domain: forall g,
is_correspondence g -> sub (domain (graph g)) (source g).
Proof. by move=> g cg; move: (corr_propc cg); intuition. Qed.
Hint Resolve corresp_sub_range corresp_sub_domain corresp_is_graph: fprops.
The set of correspondences E->F is the product of P and singleton E and singleton F, where P is powerset (product E F) is the set of graphs of
correspondences
Definition set_of_correspondences (x y:Set) :=
product (powerset (product x y))
(product (singleton x) (singleton y)).
Lemma set_of_correspondences_rw: forall x y z,
inc z (set_of_correspondences x y) =
(is_correspondence z & source z = x & target z = y).
Proof.
rewrite /set_of_correspondences/is_correspondence/graph/source/target/is_triple.
move=> x y z; aw.
apply iff_eq.
move=> [pz [spz [p_qz [pqz qqz]]]]; rewrite {} pqz {} qqz; intuition.
by move => [ aux [pqz qqz]]; move: aux; rewrite {} pqz {} qqz; intuition.
Qed.
Lemma set_of_correspondences_propa: forall f,
is_correspondence f ->
inc f (set_of_correspondences (source f) (target f)).
Proof. by move=> f cf; rewrite set_of_correspondences_rw. Qed.
We create a correspondence from a map f:a->b
Definition gacreate (a b:Set) (f:a->b) := IM (fun y:a => J (Ro y) (Ro (f y))).
Definition acreate (a b:Set) (f:a->b) := corresp a b (gacreate f).
Lemma acreate_corresp: forall (a b:Set) (f:a->b),
is_correspondence (acreate f).
Proof.
rewrite /acreate=> a b f; apply corresp_create.
rewrite /gacreate => t tIM.
by case (IM_exists tIM)=> v <-; aw; intuition; fprops ; apply R_inc.
Qed.
Image by the graph r of a set u
Definition image_by_graph r u:=
Zo (range r) (fun y=>exists x, inc x u & inc (J x y) r).
Definition image_by_fun r u :=
image_by_graph (graph r) u.
Definition image_of_fun f :=
image_by_graph (graph f) (source f).
Lemma image_by_graph_rw: forall u r y,
inc y (image_by_graph r u) = exists x, (inc x u & inc (J x y) r).
Proof.
rewrite /image_by_graph => u r y; rewrite Z_rw.
set p := ex _.
apply iff_eq; first (by intuition); move=> hp;ee.
by move: hp=> [x [ _]] Hr; rewrite range0_rw; ex_tac; aw.
Qed.
Hint Rewrite image_by_graph_rw : aw.
Lemma sub_image_by_graph: forall u r,
sub (image_by_graph r u) (range r).
Proof. move=> u r; apply Z_sub. Qed.
Lemma image_by_graph_domain: forall r, is_graph r ->
image_by_graph r (domain r) = range r.
Proof.
move=> r gt; apply extensionality; first by apply sub_image_by_graph.
by move => t; aw; dw; case=>x; exists x; ee; ex_tac.
Qed.
Lemma image_by_emptyset: forall r,
image_by_graph r emptyset = emptyset.
Proof.
rewrite /image_by_graph=> r; empty_tac3 t; rewrite Z_rw.
move => [_ [x [xe]]]; empty_tac0.
Qed.
Lemma image_by_nonemptyset: forall u r,
is_graph r -> nonempty u -> sub u (domain r)
-> nonempty (image_by_graph r u).
Proof.
move=> u r gr [x] xu udr; move: (udr _ xu); dw; move=> [y iJ].
by exists y; aw; ex_tac.
Qed.
Theorem image_by_increasing: forall u u' r,
sub u u' -> sub (image_by_graph r u) (image_by_graph r u').
Proof.
move=> u u' r uu' t; rewrite 2! image_by_graph_rw.
by move=> [x [xu Jr]]; exists x; ee; apply uu'.
Qed.
Lemma image_of_large: forall u r, is_graph r ->
sub (domain r) u -> image_by_graph r u = range r.
Proof.
move=> u r gr s; apply extensionality; first by apply sub_image_by_graph.
by rewrite -image_by_graph_domain=> // ; apply image_by_increasing.
Qed.
Section of the graph r at x
Definition im_singleton r x := image_by_graph r (singleton x).
Lemma im_singleton_pr: forall r x y,
inc y (im_singleton r x) = inc (J x y) r.
Proof.
rewrite /im_singleton=> r x y; aw; apply iff_eq; last by exists x; fprops.
by case=>a; aw; move=> [] ->.
Qed.
Hint Rewrite im_singleton_pr : aw.
Lemma im_singleton_inclusion: forall r r', is_graph r -> is_graph r' ->
(forall x, sub (im_singleton r x) (im_singleton r' x)) = sub r r'.
Proof.
move=> r r' gr gr'; apply iff_eq; last by move=> s x t; aw; apply s.
move=> s t tr;move: (gr _ tr) => eql; rewrite - eql - im_singleton_pr.
by apply s; aw; rewrite eql.
Qed.
Inverse graph of r
Definition inverse_graph r :=
Zo (product(range r)(domain r)) (fun y=> inc (J (Q y)(P y)) r).
Lemma inverse_graph_is_graph: forall r, is_graph (inverse_graph r).
Proof.
move=> r x; rewrite Z_rw; move=> [xp _]; apply (pair_in_product xp).
Qed.
Hint Resolve inverse_graph_is_graph: fprops.
Lemma inverse_graph_rw: forall r y,
inc y (inverse_graph r) = (is_pair y & inc (J (Q y)(P y)) r).
Proof.
move=> r y; rewrite Z_rw product_inc_rw.
apply iff_eq; move=> [h1 h2]; ee.
by move:(inc_pr2_range h2); rewrite pr2_pair.
by move:(inc_pr1_domain h2); rewrite pr1_pair.
Qed.
Lemma inverse_graph_alt: forall r, is_graph r ->
inverse_graph r = fun_image r (fun z => J (Q z) (P z)).
Proof.
move=> r gr; set_extens t; rewrite inverse_graph_rw =>//; aw.
move=> [pt Jr]; ex_tac; aw.
by case=> x [xr] <-; ee; aw; rewrite gr.
Qed.
Lemma inverse_graph_pair: forall r x y,
inc (J x y) (inverse_graph r) = inc (J y x) r.
Proof.
move=> r x y; rewrite inverse_graph_rw; aw.
apply iff_eq; [ by case | move=> jr;ee ].
Qed.
Lemma inverse_graph_pr2: forall r x y,
related (inverse_graph r) y x = related r x y.
Proof. rewrite /related=> r x y; apply inverse_graph_pair. Qed.
Hint Rewrite inverse_graph_pair : aw.
Hint Rewrite inverse_graph_pr2: bw.
Lemma inverse_graph_involutive: forall r, is_graph r ->
inverse_graph (inverse_graph r) = r.
Proof.
move=> r gr;set_extens x; rewrite 2! inverse_graph_rw.
by move=>[px [_]]; aw; rewrite px.
by move=> px; ee; aw; rewrite gr.
Qed.
Lemma range_inverse: forall r, is_graph r ->
range (inverse_graph r) = domain r.
Proof.
move=> r gr; set_extens x;dw; fprops.
by case=>z; aw=> h; ex_tac.
by case=>y; exists y; aw.
Qed.
Lemma domain_inverse: forall r, is_graph r ->
domain (inverse_graph r) = range r.
Proof.
move=> r gr; set_extens x; dw; fprops.
by case=>z; aw=> h; ex_tac.
by case=>y; exists y; aw.
Qed.
Lemma inverse_graph_emptyset: inverse_graph (emptyset) = emptyset.
Proof.
rewrite/inverse_graph; srw.
empty_tac3 y; rewrite Z_rw ; case; case; case.
Qed.
Hint Rewrite inverse_graph_emptyset: sw.
Lemma inverse_product: forall x y,
inverse_graph (product x y) = product y x.
Proof.
move=>x y; set_extens t; rewrite inverse_graph_rw=>//; aw; intuition.
Qed.
Lemma inverse_identity_g: forall x,
inverse_graph (identity_g x) = identity_g x.
Proof.
rewrite/inverse_graph=>x; rewrite identity_range identity_domain.
set_extens z; rewrite Z_rw 2! inc_diagonal_rw;
aw; [ | move=> [pz [Pz]] <-]; intuition.
Qed.
Hint Rewrite inverse_identity_g inverse_product: aw.
Inverse correspondence
Definition inverse_fun m :=
corresp (target m) (source m) (inverse_graph (graph m)).
Lemma inverse_correspondence: forall m,
is_correspondence m -> is_correspondence (inverse_fun m).
Proof.
rewrite /inverse_fun=>m cm; apply corresp_create.
move=> x; aw; rewrite inverse_graph_rw.
by case cm=> tm su [px iJ]; move: (su _ iJ); aw; intuition.
Qed.
Lemma inverse_fun_involutive: forall m,
is_correspondence m -> inverse_fun (inverse_fun m) = m.
Proof.
move=>m cm.
rewrite /inverse_fun; aw; rewrite inverse_graph_involutive; fprops.
by apply corresp_recov1.
Qed.
Lemma inverse_source: forall f, source (inverse_fun f) = target f.
Proof. rewrite/inverse_fun=> f; aw. Qed.
Lemma inverse_target: forall f, target (inverse_fun f) = source f.
Proof. rewrite/inverse_fun=> f; aw. Qed.
Hint Rewrite inverse_source inverse_target : aw.
Hint Resolve inverse_correspondence: fprops.
Inverse image by a graph r of a set x
Definition inv_image_by_graph r x :=
image_by_graph (inverse_graph r) x.
Definition inv_image_by_fun r x:=
inv_image_by_graph(graph r) x.
Lemma inv_image_by_fun_pr: forall r x,
inv_image_by_fun r x = image_by_fun (inverse_fun r) x.
Proof. rewrite /inv_image_by_fun /inverse_fun /image_by_fun => r x; aw. Qed.
Lemma inv_image_graph_rw: forall x r y,
(inc y (inv_image_by_graph r x)) = (exists u, inc u x & inc (J y u) r).
Proof.
rewrite /inv_image_by_graph=> r x y; aw.
by apply iff_eq; move=> [z]; [aw |]; move=> [zr Ji]; ex_tac; aw.
Qed.
Lemma inv_image_fun_rw: forall x r y,
(inc y (inv_image_by_fun r x)) = (exists u, inc u x & inc (J y u) (graph r)).
Proof. by move=>x r y; rewrite /inv_image_by_fun inv_image_graph_rw. Qed.
Hint Rewrite inv_image_graph_rw: aw.
Composition of two graphs
Definition compose_graph r' r :=
Zo (product(domain r)(range r'))
(fun w => exists y, (inc (J (P w) y) r & inc (J y (Q w)) r')).
Lemma composition_is_graph: forall r r',
is_graph (compose_graph r r').
Proof.
rewrite/compose_graph => r r' t; rewrite Z_rw.
by move=> [tp _ ]; apply (pair_in_product tp).
Qed.
Hint Resolve composition_is_graph: fprops.
Lemma inc_compose_rw: forall r r' x,
inc x (compose_graph r' r) =
(is_pair x &( exists y, inc (J (P x) y) r& inc (J y (Q x)) r')).
Proof.
rewrite/compose_graph/domain/range => r r' t; rewrite Z_rw product_inc_rw.
apply iff_eq; first intuition.
move=> [p ey]; ee; by case: ey=> [y [j1 j2]]; aw; ee; ex_tac; aw.
Qed.
Hint Rewrite inc_compose_rw: aw.
Lemma compose_related: forall r r' x z,
(related (compose_graph r' r) x z=
exists y, related r x y & related r' y z).
Proof.
by rewrite /related=> r r' x z; apply iff_eq; aw; intuition; aw.
Qed.
Hint Rewrite compose_related: aw.
Lemma compose_domain1: forall r r',
sub (domain (compose_graph r' r)) (domain r).
Proof.
rewrite/domain=> r r' t; aw; case=>x; aw.
by move => [[_ [y [p1y _]]] Px]; ex_tac; aw.
Qed.
Lemma compose_range1: forall r r',
sub (range (compose_graph r' r)) (range r').
Proof.
rewrite/range=> r r' t; aw; case=>x; aw.
by move => [[_ [y [_ p2y]]] Px]; ex_tac; aw.
Qed.
Zo (product(domain r)(range r'))
(fun w => exists y, (inc (J (P w) y) r & inc (J y (Q w)) r')).
Lemma composition_is_graph: forall r r',
is_graph (compose_graph r r').
Proof.
rewrite/compose_graph => r r' t; rewrite Z_rw.
by move=> [tp _ ]; apply (pair_in_product tp).
Qed.
Hint Resolve composition_is_graph: fprops.
Lemma inc_compose_rw: forall r r' x,
inc x (compose_graph r' r) =
(is_pair x &( exists y, inc (J (P x) y) r& inc (J y (Q x)) r')).
Proof.
rewrite/compose_graph/domain/range => r r' t; rewrite Z_rw product_inc_rw.
apply iff_eq; first intuition.
move=> [p ey]; ee; by case: ey=> [y [j1 j2]]; aw; ee; ex_tac; aw.
Qed.
Hint Rewrite inc_compose_rw: aw.
Lemma compose_related: forall r r' x z,
(related (compose_graph r' r) x z=
exists y, related r x y & related r' y z).
Proof.
by rewrite /related=> r r' x z; apply iff_eq; aw; intuition; aw.
Qed.
Hint Rewrite compose_related: aw.
Lemma compose_domain1: forall r r',
sub (domain (compose_graph r' r)) (domain r).
Proof.
rewrite/domain=> r r' t; aw; case=>x; aw.
by move => [[_ [y [p1y _]]] Px]; ex_tac; aw.
Qed.
Lemma compose_range1: forall r r',
sub (range (compose_graph r' r)) (range r').
Proof.
rewrite/range=> r r' t; aw; case=>x; aw.
by move => [[_ [y [_ p2y]]] Px]; ex_tac; aw.
Qed.
Proposition 3, inverse of composition
Theorem inverse_compose:forall r r',
inverse_graph (compose_graph r' r) =
compose_graph (inverse_graph r)(inverse_graph r').
Proof.
move=> r r'; set_extens x; aw; rewrite inverse_graph_rw; aw; fprops.
by move => [px [ _ [y [ ir ir']]]]; split=>//; exists y; aw; intuition.
move=> [px [y ]]; aw; move=> [ir' ir]; ee.
by exists y.
Qed.
inverse_graph (compose_graph r' r) =
compose_graph (inverse_graph r)(inverse_graph r').
Proof.
move=> r r'; set_extens x; aw; rewrite inverse_graph_rw; aw; fprops.
by move => [px [ _ [y [ ir ir']]]]; split=>//; exists y; aw; intuition.
move=> [px [y ]]; aw; move=> [ir' ir]; ee.
by exists y.
Qed.
Proposition 4, associativity of composition
Theorem composition_associative: forall r r' r'',
compose_graph r'' (compose_graph r' r) =
compose_graph (compose_graph r'' r') r.
Proof.
move=> r r' r''; set_extens x; aw; move=> [px h]; split=>//.
case: h=> y; aw; move => [[_ [z [ir ir']]] ir'' ].
by exists z; ee; aw; ee; exists y.
case: h=> y; aw; move => [ir [_ [z [ir' ir'']]]].
by exists z; ee; aw; ee; exists y.
Qed.
compose_graph r'' (compose_graph r' r) =
compose_graph (compose_graph r'' r') r.
Proof.
move=> r r' r''; set_extens x; aw; move=> [px h]; split=>//.
case: h=> y; aw; move => [[_ [z [ir ir']]] ir'' ].
by exists z; ee; aw; ee; exists y.
case: h=> y; aw; move => [ir [_ [z [ir' ir'']]]].
by exists z; ee; aw; ee; exists y.
Qed.
Proposition 5 Image of composition
Theorem image_composition: forall r r' x,
image_by_graph(compose_graph r' r) x = image_by_graph r' (image_by_graph r x).
Proof.
move=> r r' x; set_extens t; aw; case=> z [iz1 iz2] .
by move: iz2; aw; move=> [_ [y [ir ir']]]; ex_tac; aw; ex_tac.
by move: iz1; aw; move=> [y [yx Jr]]; ex_tac; aw; split; fprops; ex_tac.
Qed.
image_by_graph(compose_graph r' r) x = image_by_graph r' (image_by_graph r x).
Proof.
move=> r r' x; set_extens t; aw; case=> z [iz1 iz2] .
by move: iz2; aw; move=> [_ [y [ir ir']]]; ex_tac; aw; ex_tac.
by move: iz1; aw; move=> [y [yx Jr]]; ex_tac; aw; split; fprops; ex_tac.
Qed.
More properties of composition
Lemma compose_domain:forall r r',
is_graph r' ->
domain (compose_graph r' r) = inv_image_by_graph r (domain r').
Proof.
move=>r r' gr; move: (@composition_is_graph r' r) => cg.
set_extens t; aw; dw; case => [z]; aw;dw.
by move =>[_ [y [ir ir']]]; ex_tac; ex_tac.
by move=> [[y ir'] ir]; exists y; aw; ee; ex_tac.
Qed.
Lemma compose_range: forall r r',
is_graph r ->
range (compose_graph r' r) =
image_by_graph r' (range r).
Proof.
move=>r r' gr; move: (@composition_is_graph r' r) => cg.
set_extens t; aw; dw; case => [z]; aw; dw.
by move =>[_ [y [ir ir']]]; ex_tac; ex_tac.
by move=> [[y ir'] ir]; exists y; aw; ee; ex_tac.
Qed.
Lemma inverse_direct_image: forall r x,
is_graph r -> sub x (domain r) ->
sub x (inv_image_by_graph r (image_by_graph r x)).
Proof.
move=> r x gt xd t tx; aw.
by move: (xd _ tx); dw; move=> [y Jr]; ex_tac; aw; ex_tac.
Qed.
Lemma composition_increasing: forall r r' s s',
sub r s -> sub r' s' -> sub (compose_graph r' r) (compose_graph s' s).
Proof.
move=> r r' s s' rs rs' t; aw; move => [ tp [ x [ir ir']]].
by ee; exists x; split; [apply rs | apply rs'].
Qed.
Composition of two correspondences
Definition composableC r' r :=
is_correspondence r & is_correspondence r' & source r' = target r.
Definition compose r' r :=
corresp (source r)(target r') (compose_graph (graph r')(graph r)).
Notation "f1 \co f2" := (compose f1 f2) (at level 50).
Lemma compose_correspondence: forall r' r,
is_correspondence r -> is_correspondence r' ->
is_correspondence (r' \co r).
Proof.
rewrite/compose=> r' r cr cr'; apply corresp_create.
move=>t; aw; move=> [pt [y [ir ir']]]; split=>//.
move: cr => [_ sr]; move: (sr _ ir).
move: cr' => [_ sr']; move: (sr' _ ir').
by aw; intuition.
Qed.
Lemma compose_of_sets: forall r' r x,
image_by_fun(r' \co r) x = image_by_fun r' (image_by_fun r x).
Proof.
rewrite /image_by_fun=> r' r x.
have: graph (compose r' r) = compose_graph (graph r') (graph r).
by rewrite /compose /corresp /graph; aw.
by move => ->; apply image_composition.
Qed.
Lemma inverse_compose_cor: forall r r',
inverse_fun (r' \co r) = (inverse_fun r) \co (inverse_fun r').
Proof.
rewrite /inverse_fun /compose /corresp /source /target /graph => r r'.
by aw; rewrite inverse_compose.
Qed.
Identity correspondence, will be shown to be a function later
Definition identity x := corresp x x (identity_g x).
Lemma identity_corresp: forall x,
is_correspondence (identity x).
Proof.
rewrite /identity=> x; apply corresp_create.
by rewrite -diagonal_is_identity /diagonal; apply Z_sub.
Qed.
Lemma identity_source: forall x, source (identity x) = x.
Proof. rewrite/identity=> x; aw. Qed.
Lemma identity_target: forall x, target (identity x) = x.
Proof. rewrite/identity=> x; aw. Qed.
Lemma identity_graph0: forall x, graph (identity x) = identity_g x.
Proof. rewrite/identity=> x; aw. Qed.
Hint Rewrite identity_source identity_target: aw.
Lemma compose_identity_left: forall m,
is_correspondence m -> (identity (target m)) \co m = m.
Proof.
rewrite /compose=> m cm.
suff : (compose_graph (identity_g(target m)) (graph m) = graph m).
by aw; move=> eql; rewrite identity_graph0 eql; apply corresp_recov1.
set_extens t; aw.
by move=> [pt [y [ p1 ]]]; aw; move=> [_ eql]; move: p1; rewrite eql pt.
have gm: (is_graph (graph m)) by fprops.
move => tg; move: (gm _ tg)=>pt; ee.
move: cm => [ _ s]; move: (s _ tg); aw.
move=> [_ [Pt Qt]]; exists (Q t); aw; rewrite pt;ee.
Qed.
Lemma compose_identity_right: forall m,
is_correspondence m -> m \co (identity (source m)) = m.
Proof.
rewrite /compose=> m cm.
suff : (compose_graph (graph m) (identity_g (source m))= graph m).
by aw; move=> eql; rewrite identity_graph0 eql; apply corresp_recov1.
set_extens t; aw.
by move=> [pt [y]]; aw; move=> [ [_ eql]]; rewrite -eql pt.
have gm: (is_graph (graph m)) by fprops.
move => tg; move: (gm _ tg)=>pt; split => //.
move: cm => [ _ s]; move: (s _ tg); aw.
move=> [_ [Pt Qt]]; exists (P t); aw; rewrite pt;ee.
Qed.
Lemma compose_identity_identity: forall x,
(identity x) \co (identity x) = (identity x).
Proof.
move=> x; move: (@identity_corresp x)=> aux.
by move: (compose_identity_right aux); aw.
Qed.
Lemma identity_self_inverse: forall x,
inverse_fun (identity x) = (identity x).
Proof. rewrite /inverse_fun /identity=> x; aw. Qed.
End Correspondence.
Export Correspondence.
Lemma identity_corresp: forall x,
is_correspondence (identity x).
Proof.
rewrite /identity=> x; apply corresp_create.
by rewrite -diagonal_is_identity /diagonal; apply Z_sub.
Qed.
Lemma identity_source: forall x, source (identity x) = x.
Proof. rewrite/identity=> x; aw. Qed.
Lemma identity_target: forall x, target (identity x) = x.
Proof. rewrite/identity=> x; aw. Qed.
Lemma identity_graph0: forall x, graph (identity x) = identity_g x.
Proof. rewrite/identity=> x; aw. Qed.
Hint Rewrite identity_source identity_target: aw.
Lemma compose_identity_left: forall m,
is_correspondence m -> (identity (target m)) \co m = m.
Proof.
rewrite /compose=> m cm.
suff : (compose_graph (identity_g(target m)) (graph m) = graph m).
by aw; move=> eql; rewrite identity_graph0 eql; apply corresp_recov1.
set_extens t; aw.
by move=> [pt [y [ p1 ]]]; aw; move=> [_ eql]; move: p1; rewrite eql pt.
have gm: (is_graph (graph m)) by fprops.
move => tg; move: (gm _ tg)=>pt; ee.
move: cm => [ _ s]; move: (s _ tg); aw.
move=> [_ [Pt Qt]]; exists (Q t); aw; rewrite pt;ee.
Qed.
Lemma compose_identity_right: forall m,
is_correspondence m -> m \co (identity (source m)) = m.
Proof.
rewrite /compose=> m cm.
suff : (compose_graph (graph m) (identity_g (source m))= graph m).
by aw; move=> eql; rewrite identity_graph0 eql; apply corresp_recov1.
set_extens t; aw.
by move=> [pt [y]]; aw; move=> [ [_ eql]]; rewrite -eql pt.
have gm: (is_graph (graph m)) by fprops.
move => tg; move: (gm _ tg)=>pt; split => //.
move: cm => [ _ s]; move: (s _ tg); aw.
move=> [_ [Pt Qt]]; exists (P t); aw; rewrite pt;ee.
Qed.
Lemma compose_identity_identity: forall x,
(identity x) \co (identity x) = (identity x).
Proof.
move=> x; move: (@identity_corresp x)=> aux.
by move: (compose_identity_right aux); aw.
Qed.
Lemma identity_self_inverse: forall x,
inverse_fun (identity x) = (identity x).
Proof. rewrite /inverse_fun /identity=> x; aw. Qed.
End Correspondence.
Export Correspondence.
This is a different but equivalent definition
Definition functional_graph r :=
forall x y y', related r x y -> related r x y' -> y=y'.
Lemma is_functional: forall r,
(is_graph r & functional_graph r) = (fgraph r).
Proof.
rewrite /functional_graph /related=> r; apply iff_eq; last first.
by move=> fr; split; fprops; move=> x y y'; apply fgraph_pr.
move => [gr eql]; split=>//.
move=> x y xr yr eqP.
move: (xr) (yr); rewrite -(gr _ xr) - (gr _ yr) -eqP => pa pb.
by rewrite (eql _ _ _ pa pb).
Qed.
forall x y y', related r x y -> related r x y' -> y=y'.
Lemma is_functional: forall r,
(is_graph r & functional_graph r) = (fgraph r).
Proof.
rewrite /functional_graph /related=> r; apply iff_eq; last first.
by move=> fr; split; fprops; move=> x y y'; apply fgraph_pr.
move => [gr eql]; split=>//.
move=> x y xr yr eqP.
move: (xr) (yr); rewrite -(gr _ xr) - (gr _ yr) -eqP => pa pb.
by rewrite (eql _ _ _ pa pb).
Qed.
A function is a correspondence with a functional graph whose
source is the domain of the graph
Definition is_function f :=
is_correspondence f &
fgraph (graph f) & source f = domain (graph f).
Lemma is_function_pr: forall s t g,
fgraph g -> sub (range g) t -> s = domain g ->
is_function (corresp s t g).
Proof.
rewrite /is_function=> s t g fg sr d; aw; intuition.
by apply corresp_create; rewrite d corr_propcc; case fg; fprops.
Qed.
Lemma function_fgraph: forall f ,
is_function f -> fgraph (graph f).
Proof. by move=> f; case; intuition. Qed.
Lemma function_graph: forall f,
is_function f -> is_graph (graph f).
Proof. by move=> f; case; intuition. Qed.
Lemma f_domain_graph: forall f, is_function f -> domain (graph f) = source f.
Proof. by move=> f; case; intuition. Qed.
Lemma f_range_graph: forall f, is_function f -> sub (range (graph f))(target f).
Proof. by move=> f; case; intuition. Qed.
Hint Rewrite f_domain_graph : aw.
Hint Resolve function_graph function_fgraph : fprops.
Lemma image_by_fun_source: forall f, is_function f ->
image_by_fun f (source f) = range (graph f).
Proof.
move=> f ff; rewrite /image_by_fun -f_domain_graph => //.
by apply image_by_graph_domain; fprops.
Qed.
Lemma related_inc_source: forall f x y,
is_function f -> related (graph f) x y -> inc x (source f).
Proof.
move=> f x y; rewrite/ related; case; move=> _ [ fgf sf] jg.
by rewrite sf domain_rw; fprops; ex_tac.
Qed.
The value of the function f at x is W x f
Definition W x f := V x (graph f).
Lemma W_pr3: forall f x,
is_function f -> inc x (source f) -> inc (J x (W x f)) (graph f).
Proof. by move=> f x ff xf; apply fdomain_pr1; fprops; aw. Qed.
Lemma in_graph_W: forall f x,
is_function f -> inc x (graph f) -> x = (J (P x) (W (P x) f)).
Proof. by move=> f x ff xf; apply in_graph_V; fprops. Qed.
Lemma W_pr2: forall f x, is_function f ->
inc x (graph f) -> Q x = W (P x) f.
Proof. by move=> f x xg; apply pr2_V; fprops. Qed.
Lemma W_pr: forall f x y, is_function f ->
inc (J x y) (graph f) -> W x f = y.
Proof.
by move=> f x y ff Jg; symmetry; move: (in_graph_W ff Jg); aw; apply pr2_def.
Qed.
Lemma range_inc_rw: forall f y, is_function f ->
inc y (range (graph f)) = exists x, (inc x (source f) & y = W x f).
Proof. by rewrite /W=> f y ff; rewrite frange_inc_rw; aw; fprops. Qed.
Lemma inc_W_range_graph: forall f x, is_function f -> inc x (source f)
-> inc (W x f) (range (graph f)).
Proof. move=> f x ff xsf; rewrite range_inc_rw=> //; ex_tac. Qed.
Lemma inc_W_target: forall f x, is_function f -> inc x (source f)
-> inc (W x f) (target f).
Proof.
move => f x ff xsf; move: (inc_W_range_graph ff xsf).
apply (f_range_graph ff).
Qed.
Hint Resolve inc_W_target : fprops.
Lemma inc_pr1graph_source: forall f x y, is_function f ->
inc (J x y) (graph f) -> inc x (source f).
Proof. move => f x y ff Jgf; apply (related_inc_source ff Jgf).
Qed.
Lemma inc_pr2graph_target: forall f x y, is_function f ->
inc (J x y) (graph f) -> inc y (target f).
Proof.
move=> f x y ff Jgf; rewrite -(W_pr ff Jgf).
by move: (inc_pr1graph_source ff Jgf); fprops.
Qed.
Lemma inc_pr1graph_source1:forall f x, is_function f ->
inc x (graph f) -> inc (P x) (source f).
Proof.
move=> f x ff xgf; move:(in_graph_W ff xgf)=> eql; rewrite eql in xgf.
apply (inc_pr1graph_source ff xgf).
Qed.
Lemma inc_pr2graph_target1:forall f x, is_function f ->
inc x (graph f) -> inc (Q x) (target f).
Proof.
move=> f x ff xgf; move: (in_graph_W ff xgf)=>->; aw.
by apply inc_W_target => //; apply inc_pr1graph_source1.
Qed.
Lemma W_image: forall f x y, is_function f -> sub x (source f) ->
(inc y (image_by_fun f x) = exists u, inc u x & W u f = y).
Proof.
rewrite /image_by_fun=> f x y ff ss; aw.
apply iff_eq.
by move => [a [ax Jg]]; ex_tac; apply W_pr.
by move=> [u [ux Wy]]; ex_tac; rewrite - Wy; apply W_pr3=>//; apply ss.
Qed.
Hint Rewrite W_image : aw.
Ltac graph_tac :=
match goal with
| |- inc (J ?x (W ?x ?f)) (graph ?f) => apply W_pr3 ; fprops
| h:inc (J ?x ?y) (graph ?f) |- W ?x ?f = ?y => apply W_pr ; fprops
| h:inc (J ?x ?y) (graph ?f) |- ?y = W ?x ?f
=> symmetry; apply W_pr ; fprops
| |- inc (W _ ?f) (range (graph ?f)) => apply inc_W_range_graph ; fprops
| |- inc (W _ ?f) (target ?f) => apply inc_W_target ; fprops
| Ha:is_function ?X1, Hb: inc (J _ ?X2) (graph ?X1)
|- inc ?X2 (target ?X1)
=> apply (inc_pr2graph_target Ha Hb)
| Ha:is_function ?X1, Hb: inc (J ?X2 _) (graph ?X1)
|- inc ?X2 (source ?X1)
=> apply (inc_pr1graph_source Ha Hb)
| Ha:is_function ?X1, Hb: inc ?X2 (graph ?X1)
|- inc (P ?X2) (source ?X1)
=> apply (inc_pr1graph_source1 Ha Hb)
| Ha:is_function ?X1, Hb: inc ?X2 (graph ?X1)
|- inc (Q ?X2) (target ?X1)
=> apply (inc_pr2graph_target1 Ha Hb)
end.
Lemma is_function_functional: forall f, is_correspondence f->
is_function f = (forall x, inc x (source f) ->
exists_unique (fun y => related (graph f) x y)).
Proof.
rewrite/related=> f cf; apply iff_eq.
move=> ff x xsf; split; first by exists (W x f); graph_tac.
case ff; rewrite -is_functional /functional_graph/related.
by move=> _ [ [_ h] _]; apply h.
move => eu; split=>//; rewrite -is_functional.
have sd:source f = domain (graph f).
apply extensionality; last by fprops.
move=> t ts; move: (eu _ ts); case; move=> [y Jg] _.
by rewrite domain0_rw; ex_tac; aw.
ee; move=> x y y'; rewrite /related; move => h1.
have isf: inc x (source f) by rewrite sd domain0_rw; ex_tac; aw.
by move: h1; case (eu _ isf); intuition.
Qed.
Lemma image_of_fun_pr: forall f, image_of_fun f = image_by_fun f (source f).
Proof. move=> f //. Qed.
Lemma sub_image_target:
forall f, is_function f -> sub (image_of_fun f) (target f).
Proof.
move=> f ff t; rewrite image_of_fun_pr; aw; fprops.
by move => [u [usf]] <-; fprops.
Qed.
Lemma sub_image_target1: forall g x, is_function g ->
sub (image_by_fun g x) (target g).
Proof.
rewrite /image_by_fun=>g x fg.
apply sub_trans with (range (graph g)); first by apply sub_image_by_graph.
by apply f_range_graph.
Qed.
Lemma W_pr3: forall f x,
is_function f -> inc x (source f) -> inc (J x (W x f)) (graph f).
Proof. by move=> f x ff xf; apply fdomain_pr1; fprops; aw. Qed.
Lemma in_graph_W: forall f x,
is_function f -> inc x (graph f) -> x = (J (P x) (W (P x) f)).
Proof. by move=> f x ff xf; apply in_graph_V; fprops. Qed.
Lemma W_pr2: forall f x, is_function f ->
inc x (graph f) -> Q x = W (P x) f.
Proof. by move=> f x xg; apply pr2_V; fprops. Qed.
Lemma W_pr: forall f x y, is_function f ->
inc (J x y) (graph f) -> W x f = y.
Proof.
by move=> f x y ff Jg; symmetry; move: (in_graph_W ff Jg); aw; apply pr2_def.
Qed.
Lemma range_inc_rw: forall f y, is_function f ->
inc y (range (graph f)) = exists x, (inc x (source f) & y = W x f).
Proof. by rewrite /W=> f y ff; rewrite frange_inc_rw; aw; fprops. Qed.
Lemma inc_W_range_graph: forall f x, is_function f -> inc x (source f)
-> inc (W x f) (range (graph f)).
Proof. move=> f x ff xsf; rewrite range_inc_rw=> //; ex_tac. Qed.
Lemma inc_W_target: forall f x, is_function f -> inc x (source f)
-> inc (W x f) (target f).
Proof.
move => f x ff xsf; move: (inc_W_range_graph ff xsf).
apply (f_range_graph ff).
Qed.
Hint Resolve inc_W_target : fprops.
Lemma inc_pr1graph_source: forall f x y, is_function f ->
inc (J x y) (graph f) -> inc x (source f).
Proof. move => f x y ff Jgf; apply (related_inc_source ff Jgf).
Qed.
Lemma inc_pr2graph_target: forall f x y, is_function f ->
inc (J x y) (graph f) -> inc y (target f).
Proof.
move=> f x y ff Jgf; rewrite -(W_pr ff Jgf).
by move: (inc_pr1graph_source ff Jgf); fprops.
Qed.
Lemma inc_pr1graph_source1:forall f x, is_function f ->
inc x (graph f) -> inc (P x) (source f).
Proof.
move=> f x ff xgf; move:(in_graph_W ff xgf)=> eql; rewrite eql in xgf.
apply (inc_pr1graph_source ff xgf).
Qed.
Lemma inc_pr2graph_target1:forall f x, is_function f ->
inc x (graph f) -> inc (Q x) (target f).
Proof.
move=> f x ff xgf; move: (in_graph_W ff xgf)=>->; aw.
by apply inc_W_target => //; apply inc_pr1graph_source1.
Qed.
Lemma W_image: forall f x y, is_function f -> sub x (source f) ->
(inc y (image_by_fun f x) = exists u, inc u x & W u f = y).
Proof.
rewrite /image_by_fun=> f x y ff ss; aw.
apply iff_eq.
by move => [a [ax Jg]]; ex_tac; apply W_pr.
by move=> [u [ux Wy]]; ex_tac; rewrite - Wy; apply W_pr3=>//; apply ss.
Qed.
Hint Rewrite W_image : aw.
Ltac graph_tac :=
match goal with
| |- inc (J ?x (W ?x ?f)) (graph ?f) => apply W_pr3 ; fprops
| h:inc (J ?x ?y) (graph ?f) |- W ?x ?f = ?y => apply W_pr ; fprops
| h:inc (J ?x ?y) (graph ?f) |- ?y = W ?x ?f
=> symmetry; apply W_pr ; fprops
| |- inc (W _ ?f) (range (graph ?f)) => apply inc_W_range_graph ; fprops
| |- inc (W _ ?f) (target ?f) => apply inc_W_target ; fprops
| Ha:is_function ?X1, Hb: inc (J _ ?X2) (graph ?X1)
|- inc ?X2 (target ?X1)
=> apply (inc_pr2graph_target Ha Hb)
| Ha:is_function ?X1, Hb: inc (J ?X2 _) (graph ?X1)
|- inc ?X2 (source ?X1)
=> apply (inc_pr1graph_source Ha Hb)
| Ha:is_function ?X1, Hb: inc ?X2 (graph ?X1)
|- inc (P ?X2) (source ?X1)
=> apply (inc_pr1graph_source1 Ha Hb)
| Ha:is_function ?X1, Hb: inc ?X2 (graph ?X1)
|- inc (Q ?X2) (target ?X1)
=> apply (inc_pr2graph_target1 Ha Hb)
end.
Lemma is_function_functional: forall f, is_correspondence f->
is_function f = (forall x, inc x (source f) ->
exists_unique (fun y => related (graph f) x y)).
Proof.
rewrite/related=> f cf; apply iff_eq.
move=> ff x xsf; split; first by exists (W x f); graph_tac.
case ff; rewrite -is_functional /functional_graph/related.
by move=> _ [ [_ h] _]; apply h.
move => eu; split=>//; rewrite -is_functional.
have sd:source f = domain (graph f).
apply extensionality; last by fprops.
move=> t ts; move: (eu _ ts); case; move=> [y Jg] _.
by rewrite domain0_rw; ex_tac; aw.
ee; move=> x y y'; rewrite /related; move => h1.
have isf: inc x (source f) by rewrite sd domain0_rw; ex_tac; aw.
by move: h1; case (eu _ isf); intuition.
Qed.
Lemma image_of_fun_pr: forall f, image_of_fun f = image_by_fun f (source f).
Proof. move=> f //. Qed.
Lemma sub_image_target:
forall f, is_function f -> sub (image_of_fun f) (target f).
Proof.
move=> f ff t; rewrite image_of_fun_pr; aw; fprops.
by move => [u [usf]] <-; fprops.
Qed.
Lemma sub_image_target1: forall g x, is_function g ->
sub (image_by_fun g x) (target g).
Proof.
rewrite /image_by_fun=>g x fg.
apply sub_trans with (range (graph g)); first by apply sub_image_by_graph.
by apply f_range_graph.
Qed.
The image of singleton by a function is a singleton
Lemma image_singleton: forall f x,
is_function f -> inc x (source f) ->
image_by_fun f (singleton x) = singleton (W x f).
Proof.
move=> f x ff xsf; move: (sub_singleton xsf) => ixs.
set_extens t; aw.
by move=> [u [us ]] <-; awi us; rewrite us.
by move=> ->; exists x; aw.
Qed.
is_function f -> inc x (source f) ->
image_by_fun f (singleton x) = singleton (W x f).
Proof.
move=> f x ff xsf; move: (sub_singleton xsf) => ixs.
set_extens t; aw.
by move=> [u [us ]] <-; awi us; rewrite us.
by move=> ->; exists x; aw.
Qed.
A lemma that says when two functions are equal
Lemma function_exten3: forall f g,
is_function f -> is_function g -> graph f = graph g ->
target f = target g -> source f = source g ->
f = g.
Proof.
move=> f g [ [ ff _] _ ] [ [fg _] _ ] e1 e2 e3.
rewrite -(corresp_recov ff); rewrite -(corresp_recov fg).
by congr (corresp _ _ _).
Qed.
Lemma function_exten1: forall f g,
is_function f -> is_function g -> graph f = graph g ->
target f = target g ->
f = g.
Proof.
move => f g ff fg e1 e2; apply function_exten3=>//.
by do 2 rewrite -f_domain_graph=>//; rewrite e1.
Qed.
Lemma function_exten: forall f g,
is_function f -> is_function g -> source f = source g ->
target f = target g -> (forall x, inc x (source f) -> W x f = W x g)
-> f = g.
Proof.
move=> f g ff fg e1 r2 e2; apply function_exten3=> //.
set_extens x => xg.
have Pf : (inc (P x) (source f)) by graph_tac.
by rewrite (in_graph_W ff xg) (e2 _ Pf); graph_tac; rewrite -e1.
have Pg : (inc (P x) (source f)) by rewrite e1; graph_tac.
by rewrite (in_graph_W fg xg) -(e2 _ Pg); graph_tac.
Qed.
Lemma inv_image_complement: forall g x,
is_function g ->
inv_image_by_fun g (complement (target g) x) =
complement (source g) (inv_image_by_fun g x).
Proof.
rewrite /inv_image_by_fun => g x fg.
have gg: is_graph (graph g) by fprops.
set_extens t; aw.
move=> [u [uf Jg]]; move: uf; srw; move=> [ut nux].
split; first by graph_tac.
aw; case; move => w [wx Jwg].
by case nux; case fg => [_ [fgg _]]; rewrite (fgraph_pr fgg Jg Jwg).
srw; aw; move => [ts neu].
have Jg: (inc (J t (W t g))(graph g)) by graph_tac.
by ex_tac; srw; split; fprops; dneg Wx; ex_tac.
Qed.
The correspondence acreate f is a function
Lemma prop_acreate: forall (A B:Set) (f:A->B) x,
inc x (graph (acreate f)) = exists u:A, J (Ro u) (Ro (f u)) = x.
Proof. by rewrite /acreate /gacreate=> A B f x; aw; rewrite IM_rw. Qed.
Lemma acreate_function : forall (A B:Set) (f:A->B),
is_function (acreate f).
Proof.
move=> A B f; move : (acreate_corresp f)=>cf.
red;ee.
split; fprops; move=> x y; rewrite 2! prop_acreate.
case=>v1 <-; case=>v2 <-; aw=> eql.
by rewrite (R_inj eql).
rewrite /acreate /gacreate /domain; aw.
set_extens t; aw.
move=> tA; exists (J t (Ro (f (Bo tA)))).
by split; aw; apply IM_inc; exists (Bo tA); by rewrite B_eq.
by case=>x; rewrite IM_rw; move=> [[a]] <- <-; aw; apply R_inc.
Qed.
Hint Resolve acreate_function: fprops.
Lemma acreate_W : forall (A B:Set) (f:A->B) (x:A),
W (Ro x) (acreate f) = Ro (f x).
Proof.
move=> A B f x.
have rs: (inc (Ro x) (source (acreate f))) by rewrite/acreate; aw; apply R_inc.
move: (W_pr3 (acreate_function f) rs); rewrite prop_acreate.
move=> [u eql];rewrite -(pr2_def eql).
by rewrite (R_inj (pr1_def eql)).
Qed.
We define bcreate1 f of type source f-> target f
so that acreate (bcreate1 f) = f
Definition bcreate1 f (H:is_function f) :=
fun x:source f => Bo (inc_W_target H (R_inc x)).
Lemma prop_bcreate1: forall f (H:is_function f) (x:source f),
Ro (bcreate1 H x) = W (Ro x) f.
Proof. by move=> f H x; apply B_eq. Qed.
Lemma bcreate_inv1: forall f (H:is_function f),
acreate (bcreate1 H) = f.
Proof.
move=> f ff; apply function_exten; fprops; rewrite {1}/acreate; aw.
by move=> x xs; rewrite - (B_eq xs) acreate_W; apply prop_bcreate1.
Qed.
Lemma W_mapping: forall f A B (Ha:source f =A)(Hb:target f =B) x,
is_function f -> inc x A -> inc (W x f) B.
Proof. by move =>f A B <- <- x ff; fprops. Qed.
We define bcreate f a b of type a->b,
it satisfies acreate (bcreate f a b) = f
Definition bcreate f A B
(H:is_function f)(Ha:source f = A)(Hb:target f = B):=
fun x:A => Bo (W_mapping Ha Hb H (R_inc x)).
Lemma prop_bcreate2: forall f A B
(H:is_function f) (Ha:source f=A)(Hb:target f=B)(x:A),
Ro(bcreate H Ha Hb x) = W (Ro x) f.
Proof. move=> f A B H HA Hb x; apply B_eq. Qed.
Lemma bcreate_inv2: forall f A B
(H:is_function f) (Ha:source f=A)(Hb:target f=B),
acreate (bcreate H Ha Hb) = f.
Proof.
move=> f A B H Ha Hb.
apply function_exten; fprops; rewrite /acreate; aw =>//.
by move=> x xs; rewrite -(B_eq xs) acreate_W; apply prop_bcreate2.
Qed.
Lemma acreate_source: forall (A B:Set) (f:A->B), source (acreate f)= A.
Proof. by rewrite /acreate=> A B f; aw. Qed.
Lemma acreate_target: forall (A B:Set) (f:A->B), target (acreate f)= B.
Proof. by rewrite /acreate=> A B f; aw. Qed.
Hint Rewrite acreate_source acreate_target: aw.
Lemma bcreate_inv3: forall (A B:Set) (f:A->B),
bcreate (acreate_function f) (acreate_source f)(acreate_target f) =1 f.
Proof.
move=> A B f a.
by apply R_inj; rewrite prop_bcreate2 acreate_W.
Qed.
Lemma bcreate_eq: forall f (H:is_function f),
bcreate1 H =1 bcreate H (refl_equal (source f)) (refl_equal (target f)).
Proof.
by move=> f H a; apply R_inj; rewrite prop_bcreate2 prop_bcreate1.
Qed.
(H:is_function f)(Ha:source f = A)(Hb:target f = B):=
fun x:A => Bo (W_mapping Ha Hb H (R_inc x)).
Lemma prop_bcreate2: forall f A B
(H:is_function f) (Ha:source f=A)(Hb:target f=B)(x:A),
Ro(bcreate H Ha Hb x) = W (Ro x) f.
Proof. move=> f A B H HA Hb x; apply B_eq. Qed.
Lemma bcreate_inv2: forall f A B
(H:is_function f) (Ha:source f=A)(Hb:target f=B),
acreate (bcreate H Ha Hb) = f.
Proof.
move=> f A B H Ha Hb.
apply function_exten; fprops; rewrite /acreate; aw =>//.
by move=> x xs; rewrite -(B_eq xs) acreate_W; apply prop_bcreate2.
Qed.
Lemma acreate_source: forall (A B:Set) (f:A->B), source (acreate f)= A.
Proof. by rewrite /acreate=> A B f; aw. Qed.
Lemma acreate_target: forall (A B:Set) (f:A->B), target (acreate f)= B.
Proof. by rewrite /acreate=> A B f; aw. Qed.
Hint Rewrite acreate_source acreate_target: aw.
Lemma bcreate_inv3: forall (A B:Set) (f:A->B),
bcreate (acreate_function f) (acreate_source f)(acreate_target f) =1 f.
Proof.
move=> A B f a.
by apply R_inj; rewrite prop_bcreate2 acreate_W.
Qed.
Lemma bcreate_eq: forall f (H:is_function f),
bcreate1 H =1 bcreate H (refl_equal (source f)) (refl_equal (target f)).
Proof.
by move=> f H a; apply R_inj; rewrite prop_bcreate2 prop_bcreate1.
Qed.
Function with empty graph
Definition empty_functionC : emptyset -> emptyset := fun x => x.
Definition empty_function:= acreate empty_functionC.
Lemma empty_function_function: is_function empty_function.
Proof. rewrite /empty_function; fprops. Qed.
Lemma empty_function_graph: graph empty_function = emptyset.
Proof.
rewrite /empty_function /acreate /gacreate; aw.
empty_tac t te; case (IM_exists te); case.
Qed.
Lemma special_empty_function: forall f, is_function f ->
graph f = emptyset -> source f = emptyset.
Proof. by move => f ff ge; case ff; rewrite ge; move => _ [_] ->; srw.
Qed.
Lemma empty_function_prop:
bcreate empty_function_function (acreate_source empty_functionC)
(acreate_target empty_functionC)
=1 empty_functionC.
Proof. move=> t; case t. Qed.
Definition empty_function:= acreate empty_functionC.
Lemma empty_function_function: is_function empty_function.
Proof. rewrite /empty_function; fprops. Qed.
Lemma empty_function_graph: graph empty_function = emptyset.
Proof.
rewrite /empty_function /acreate /gacreate; aw.
empty_tac t te; case (IM_exists te); case.
Qed.
Lemma special_empty_function: forall f, is_function f ->
graph f = emptyset -> source f = emptyset.
Proof. by move => f ff ge; case ff; rewrite ge; move => _ [_] ->; srw.
Qed.
Lemma empty_function_prop:
bcreate empty_function_function (acreate_source empty_functionC)
(acreate_target empty_functionC)
=1 empty_functionC.
Proof. move=> t; case t. Qed.
Properties of the identity function
Lemma identity_function: forall x,
is_function (identity x).
Proof.
rewrite /identity=>x; apply is_function_pr.
by apply identity_fgraph.
by rewrite identity_range; fprops.
by rewrite identity_domain.
Qed.
Lemma identity_W: forall x y,
inc y x -> W y (identity x) = y.
Proof. by rewrite /W /identity=> x y; aw; apply identity_ev. Qed.
Hint Rewrite identity_W: sw.
Hint Resolve identity_function: fprops.
Definition identityC (a:Set): a->a := @id a.
Lemma identity_prop: forall a:Set, acreate (@id a) = identity a.
Proof. move=> a; apply function_exten; fprops. Qed.
Lemma identity_prop2: forall a,
bcreate (identity_function a) (identity_source a) (identity_target a) =1
@id a.
Proof.
by move=> a x; apply R_inj; rewrite prop_bcreate2 -identity_prop acreate_W.
Qed.
Definition of a constant function and of the constant function
Definition is_constant_function f :=
(is_function f) &
(forall x x', inc x (source f) -> inc x' (source f) -> W x f = W x' f).
Definition is_constant_functionC x y (f:x->y) := forall a b, f a = f b.
Definition constant_function (x y a:Set) (H:inc a y) :=
acreate ([fun :x => Bo H] ).
Implicit Arguments constant_function [].
Lemma constant_source: forall x y a (H:inc a y),
source (constant_function x y a H) = x.
Proof. rewrite /constant_function=> x y a H; aw. Qed.
Lemma constant_target: forall x y a (H:inc a y),
target (constant_function x y a H) = y.
Proof. rewrite /constant_function=> x y a H; aw. Qed.
Lemma constant_graph: forall x y a (H:inc a y),
graph (constant_function x y a H) = product x (singleton a).
Proof.
rewrite/constant_function /acreate /gacreate =>x y a ay; aw.
set_extens t; rewrite IM_rw.
by move => [b] <-; aw;split; fprops; split; [ apply R_inc | rewrite B_eq].
aw; move=> [ tp [pt qt]]; exists (Bo pt).
by apply pair_exten; fprops;aw; rewrite B_eq.
Qed.
Lemma constant_function_fun: forall x y a (H: inc a y),
is_function(constant_function x y a H).
Proof. rewrite/constant_function; fprops. Qed.
Lemma constant_W: forall x y a (H:inc a y) b,
inc b x -> W b (constant_function x y a H) = a.
Proof.
move=> x y a ay b bx; apply W_pr.
by apply constant_function_fun.
rewrite constant_graph;fprops.
Qed.
Lemma constant_function_pr: forall f,
is_function f -> (is_constant_function f =
small_set (range (graph f))).
Proof.
rewrite /small_set=> f ff; apply iff_eq.
move=> cff u v; do 2 rewrite range_inc_rw=>//.
by move=> [x [xs]] ->; move=> [y [ys]] ->; case cff => _; apply.
move=> pr; split=> //.
move=> x x' xs x's; apply pr; graph_tac.
Qed.
Lemma constant_constant_fun: forall x y a (H: inc a y),
is_constant_function(constant_function x y a H).
Proof.
move=> x y a H; split; first by apply constant_function_fun.
rewrite (constant_source x H).
move=> u v us vs; do 2 rewrite constant_W=>//.
Qed.
Lemma constant_fun_constantC: forall x y (a:y),
is_constant_functionC ([fun:x => a]).
Proof. move=> x y a; split. Qed.
Lemma constant_function_prop2: forall (x y:Set) (a:y),
bcreate (constant_function_fun x (R_inc a)) (constant_source x (R_inc a))
(constant_target x (R_inc a)) =1 [fun:x => a].
Proof.
move=>x y a t; apply R_inj; rewrite prop_bcreate2 constant_W //;apply R_inc.
Qed.
Lemma constant_fun_prC: forall x y (f:x->y)(b:x), is_constant_functionC f ->
exists a:y, f =1 [fun :x => a].
Proof.
move=> x y f b cf; exists (f b); move=> t; apply cf.
Qed.
Lemma constant_fun_pr: forall f (H:nonempty(graph f)),
is_constant_function f ->
exists a: target f,
f = constant_function (source f) (target f) (Ro a) (R_inc a).
Proof.
move=> f [x xg] [ff cf].
have Ps: (inc (P x) (source f)) by graph_tac.
have PWt: inc (W (P x) f) (target f) by fprops.
exists (Bo PWt); apply function_exten=>//.
by apply constant_function_fun.
by rewrite /constant_function; aw.
by rewrite /constant_function acreate_target.
by move=> y ys; rewrite constant_W=>//; rewrite B_eq; apply cf.
Qed.
(is_function f) &
(forall x x', inc x (source f) -> inc x' (source f) -> W x f = W x' f).
Definition is_constant_functionC x y (f:x->y) := forall a b, f a = f b.
Definition constant_function (x y a:Set) (H:inc a y) :=
acreate ([fun :x => Bo H] ).
Implicit Arguments constant_function [].
Lemma constant_source: forall x y a (H:inc a y),
source (constant_function x y a H) = x.
Proof. rewrite /constant_function=> x y a H; aw. Qed.
Lemma constant_target: forall x y a (H:inc a y),
target (constant_function x y a H) = y.
Proof. rewrite /constant_function=> x y a H; aw. Qed.
Lemma constant_graph: forall x y a (H:inc a y),
graph (constant_function x y a H) = product x (singleton a).
Proof.
rewrite/constant_function /acreate /gacreate =>x y a ay; aw.
set_extens t; rewrite IM_rw.
by move => [b] <-; aw;split; fprops; split; [ apply R_inc | rewrite B_eq].
aw; move=> [ tp [pt qt]]; exists (Bo pt).
by apply pair_exten; fprops;aw; rewrite B_eq.
Qed.
Lemma constant_function_fun: forall x y a (H: inc a y),
is_function(constant_function x y a H).
Proof. rewrite/constant_function; fprops. Qed.
Lemma constant_W: forall x y a (H:inc a y) b,
inc b x -> W b (constant_function x y a H) = a.
Proof.
move=> x y a ay b bx; apply W_pr.
by apply constant_function_fun.
rewrite constant_graph;fprops.
Qed.
Lemma constant_function_pr: forall f,
is_function f -> (is_constant_function f =
small_set (range (graph f))).
Proof.
rewrite /small_set=> f ff; apply iff_eq.
move=> cff u v; do 2 rewrite range_inc_rw=>//.
by move=> [x [xs]] ->; move=> [y [ys]] ->; case cff => _; apply.
move=> pr; split=> //.
move=> x x' xs x's; apply pr; graph_tac.
Qed.
Lemma constant_constant_fun: forall x y a (H: inc a y),
is_constant_function(constant_function x y a H).
Proof.
move=> x y a H; split; first by apply constant_function_fun.
rewrite (constant_source x H).
move=> u v us vs; do 2 rewrite constant_W=>//.
Qed.
Lemma constant_fun_constantC: forall x y (a:y),
is_constant_functionC ([fun:x => a]).
Proof. move=> x y a; split. Qed.
Lemma constant_function_prop2: forall (x y:Set) (a:y),
bcreate (constant_function_fun x (R_inc a)) (constant_source x (R_inc a))
(constant_target x (R_inc a)) =1 [fun:x => a].
Proof.
move=>x y a t; apply R_inj; rewrite prop_bcreate2 constant_W //;apply R_inc.
Qed.
Lemma constant_fun_prC: forall x y (f:x->y)(b:x), is_constant_functionC f ->
exists a:y, f =1 [fun :x => a].
Proof.
move=> x y f b cf; exists (f b); move=> t; apply cf.
Qed.
Lemma constant_fun_pr: forall f (H:nonempty(graph f)),
is_constant_function f ->
exists a: target f,
f = constant_function (source f) (target f) (Ro a) (R_inc a).
Proof.
move=> f [x xg] [ff cf].
have Ps: (inc (P x) (source f)) by graph_tac.
have PWt: inc (W (P x) f) (target f) by fprops.
exists (Bo PWt); apply function_exten=>//.
by apply constant_function_fun.
by rewrite /constant_function; aw.
by rewrite /constant_function acreate_target.
by move=> y ys; rewrite constant_W=>//; rewrite B_eq; apply cf.
Qed.
Composition of Coq function
Lemma compositionC_associative: forall a b c d (f: c->d)(g:b->c)(h:a->b),
(f \o g) \o h = f \o (g \o h).
Proof. trivial. Qed.
Lemma composeC_ev: forall a b c (g:b->c) (f: a->b) x,
(g \o f) x = g (f x).
Proof. by move => a b c g f x. Qed.
Lemma compose_id_leftC: forall (a b:Set) (f:a->b),
(@id b) \o f =1 f.
Proof. by move=> a b f t. Qed.
Lemma compose_id_rightC: forall (a b:Set) (f:a->b),
f \o (@id a) =1 f.
Proof. by move=> a b f t. Qed.
Function associated to set inclusion
Definition inclusionC x y (H: sub x y):=
[fun u:x => Bo (H (Ro u) (R_inc u))].
Lemma inclusionC_pr: forall x y (H: sub x y) (a:x),
Ro(inclusionC H a) = Ro a.
Proof. by move => x y sxy a /=; apply B_eq. Qed.
Lemma inclusionC_identity: forall x,
inclusionC (sub_refl (x:=x)) =1 @id x.
Proof.
by move => x v; apply R_inj;rewrite inclusionC_pr.
Qed.
Lemma inclusionC_compose: forall x y z (Ha:sub x y)(Hb: sub y z),
(inclusionC Hb) \o (inclusionC Ha) =1 inclusionC (sub_trans Ha Hb).
Proof.
move=> x y z sxy syz t; by apply R_inj; rewrite 3! inclusionC_pr.
Qed.
Restriction of a Coq function; agreement of subsets
Definition restrictionC (x a b:Set) (f:a->b)(H: sub x a) :=
f \o (inclusionC H).
Definition agreeC (x a a' b b':Set) (f:a->b) (f':a'-> b')
(Ha: sub x a)(Hb: sub x a') :=
forall u:x, Ro(restrictionC f Ha u) = Ro(restrictionC f' Hb u).
The functions agree on x if they take the same value
Definition agrees_on x f f' :=
(sub x (source f)) & (sub x (source f')) &
(forall a, inc a x -> W a f = W a f').
Lemma same_graph_agrees: forall f f',
is_function f -> is_function f' -> graph f = graph f' ->
agrees_on (source f) f f'.
Proof.
move=> f f' ff ff' geq.
have seq: (source f = source f')
by do 2 rewrite -f_domain_graph=>//; rewrite geq.
rewrite /agrees_on -seq; split; fprops; split; fprops.
move=> a asf; move: (W_pr3 ff asf)=> aux.
by rewrite geq in aux; rewrite -(W_pr ff' aux).
Qed.
Lemma function_exten2: forall f f',
is_function f -> is_function f' ->
(f = f') = ((source f = source f') & (target f = target f') &
(agrees_on (source f) f f')).
Proof.
move=> f f' ff ff'; apply iff_eq.
by rewrite /agrees_on; move => ->; intuition.
move => [seq [teq [_ [_ ag]]]]; apply function_exten; fprops.
Qed.
Lemma sub_function: forall f g,
is_function f -> is_function g ->
(sub (graph f) (graph g)) = (agrees_on (source f) f g).
Proof.
move=> f g ff fg; apply iff_eq=> hyp.
red; ee.
by do 2 rewrite -f_domain_graph=>//; apply sub_graph_domain.
by move=> a af;rewrite- (W_pr fg (hyp _ (W_pr3 ff af))).
move => t tg; move: hyp => [_ [sg ag]].
have Ptsf: (inc (P t) (source f)) by graph_tac.
move: (in_graph_W ff tg)=> ->; rewrite (ag _ Ptsf); graph_tac.
Qed.
(sub x (source f)) & (sub x (source f')) &
(forall a, inc a x -> W a f = W a f').
Lemma same_graph_agrees: forall f f',
is_function f -> is_function f' -> graph f = graph f' ->
agrees_on (source f) f f'.
Proof.
move=> f f' ff ff' geq.
have seq: (source f = source f')
by do 2 rewrite -f_domain_graph=>//; rewrite geq.
rewrite /agrees_on -seq; split; fprops; split; fprops.
move=> a asf; move: (W_pr3 ff asf)=> aux.
by rewrite geq in aux; rewrite -(W_pr ff' aux).
Qed.
Lemma function_exten2: forall f f',
is_function f -> is_function f' ->
(f = f') = ((source f = source f') & (target f = target f') &
(agrees_on (source f) f f')).
Proof.
move=> f f' ff ff'; apply iff_eq.
by rewrite /agrees_on; move => ->; intuition.
move => [seq [teq [_ [_ ag]]]]; apply function_exten; fprops.
Qed.
Lemma sub_function: forall f g,
is_function f -> is_function g ->
(sub (graph f) (graph g)) = (agrees_on (source f) f g).
Proof.
move=> f g ff fg; apply iff_eq=> hyp.
red; ee.
by do 2 rewrite -f_domain_graph=>//; apply sub_graph_domain.
by move=> a af;rewrite- (W_pr fg (hyp _ (W_pr3 ff af))).
move => t tg; move: hyp => [_ [sg ag]].
have Ptsf: (inc (P t) (source f)) by graph_tac.
move: (in_graph_W ff tg)=> ->; rewrite (ag _ Ptsf); graph_tac.
Qed.
Restriction of the function to a part of it source
Lemma restr_domain2: forall f x,
is_function f-> sub x (source f) ->
domain (restr (graph f) x) = x.
Proof.
by move => f x [_ [ fgf ssd]] sxs; rewrite restr_domain1=>//; rewrite -ssd.
Qed.
Lemma restr_range: forall f x,
is_function f-> sub x (source f) ->
sub (range (restr (graph f) x)) (target f).
Proof.
rewrite /range /restr; move=> f x ff sxdf t; aw.
move=> [z]; rewrite Z_rw; move=> [ [zg Pzx] ] <-; graph_tac.
Qed.
Definition restriction f x :=
corresp x (target f) (restr (graph f) x).
Definition restriction1 f x :=
corresp x (image_by_fun f x) (restr (graph f) x).
Lemma restriction_function: forall f x,
is_function f -> sub x (source f) ->
is_function (restriction f x).
Proof.
rewrite /restriction=>f x ff xs; apply is_function_pr.
by fprops.
by apply restr_range.
by rewrite restr_domain2.
Qed.
Lemma restriction1_function: forall f x,
is_function f -> sub x (source f) ->
is_function (restriction1 f x).
Proof.
rewrite /restriction1=>f x ff ssf; apply is_function_pr; fprops.
rewrite /range /restr => t; aw; move=> [z []].
by rewrite Z_rw; move=> [zg Px] <-; ex_tac; rewrite - (W_pr2 ff zg).
by rewrite restr_domain2.
Qed.
Hint Resolve restriction_function restriction1_function: fprops.
Lemma restriction_W: forall f x a,
is_function f -> sub x (source f) ->
inc a x -> W a (restriction f x) = W a f.
Proof. rewrite /W/restriction => f x a ff ss xa; aw; bw; fprops; aw.
Qed.
Lemma restriction1_W: forall f x a,
is_function f -> sub x (source f) ->
inc a x -> W a (restriction1 f x) = W a f.
Proof. rewrite /W/restriction1 => f x a ff ss xa; aw; bw; fprops; aw. Qed.
g extends f if its restriction to the source of f is f
Definition extends g f :=
(is_function f) & (is_function g) & (sub (graph f) (graph g))
& (sub (target f)(target g)).
Definition extendsC (a b a' b':Set) (g:a'->b')(f:a->b)(H: sub a a') :=
sub b b' & agreeC g f H (sub_refl (x:=a)).
Lemma source_extends: forall f g,
extends g f -> sub (source f) (source g).
Proof.
move=> f g [ff [fg [sg st]]]; do 2 rewrite -f_domain_graph=>//.
by apply sub_graph_domain.
Qed.
Lemma W_extends: forall f g x,
extends g f -> inc x (source f) -> W x f = W x g.
Proof.
move=> f g x ext xf; move : (source_extends ext) => ss.
move: ext => [ff [fg [sg _]]].
have pg: (inc (J x (W x f)) (graph g)) by apply sg; graph_tac.
by rewrite (W_pr fg pg).
Qed.
Lemma extendsC_pr : forall (a b a' b':Set) (g:a'->b')(f:a->b)(H: sub a a'),
extendsC g f H -> forall x:a, Ro (f x) = Ro(g (inclusionC H x)).
Proof.
move=> a b a' b' g f saa' [e1].
rewrite /agreeC => eq x; rewrite eq.
by rewrite /restrictionC composeC_ev inclusionC_identity.
Qed.
Lemma function_extends_restr: forall f x,
is_function f -> sub x (source f) ->
extends f (restriction f x).
Proof.
move => f x ff ssf; split; fprops; split=>//.
rewrite /restriction; aw.
split; fprops; apply restr_sub.
Qed.
Lemma function_extends_restC: forall (x a b:Set) (f:a->b)(H:sub x a),
extendsC f (restrictionC f H) H.
Proof.
move=> x a b f xa; split; fprops.
move => t; rewrite /restrictionC compositionC_associative 2! composeC_ev.
rewrite inclusionC_compose.
apply f_equal. apply f_equal.
by apply R_inj; rewrite B_eq B_eq.
Qed.
Lemma agrees_same_restriction: forall f g x,
is_function f -> is_function g -> agrees_on x f g ->
target f = target g ->
restriction f x =
restriction g x.
Proof.
move=> f g x ff fg [ sf [sg vfg]] t.
apply function_exten; fprops; try solve [rewrite /restriction; aw].
rewrite {1} /restriction; aw=> z zs.
by do 2 rewrite restriction_W=>//; apply vfg.
Qed.
Lemma agrees_same_restrictionC: forall (a a' b x:Set) (f:a->b)(g:a'->b)
(Ha: sub x a)(Hb: sub x a'),
agreeC f g Ha Hb -> restrictionC f Ha =1 restrictionC g Hb.
Proof.
move => a a' b x f g xa xb ag z; apply R_inj; apply ag.
Qed.
Lemma restriction_graph1: forall f x,
is_function f -> sub x (source f) ->
graph (restriction f x) =
intersection2 (graph f)(product x (target f)).
Proof.
rewrite /restriction => f x ff xs; aw; set_extens t; aw; last by intuition.
move => [tg Ptx]; intuition; last by graph_tac.
have: (is_graph (graph f)) by fprops.
by apply.
Qed.
Lemma restriction_recovers: forall f x,
is_function f -> sub x (source f) ->
restriction f x = corresp x (target f)
(intersection2 (graph f)(product x (target f))).
Proof.
move=>f x ff ss; rewrite- (restriction_graph1 ff ss).
rewrite /restriction; aw.
Qed.
(is_function f) & (is_function g) & (sub (graph f) (graph g))
& (sub (target f)(target g)).
Definition extendsC (a b a' b':Set) (g:a'->b')(f:a->b)(H: sub a a') :=
sub b b' & agreeC g f H (sub_refl (x:=a)).
Lemma source_extends: forall f g,
extends g f -> sub (source f) (source g).
Proof.
move=> f g [ff [fg [sg st]]]; do 2 rewrite -f_domain_graph=>//.
by apply sub_graph_domain.
Qed.
Lemma W_extends: forall f g x,
extends g f -> inc x (source f) -> W x f = W x g.
Proof.
move=> f g x ext xf; move : (source_extends ext) => ss.
move: ext => [ff [fg [sg _]]].
have pg: (inc (J x (W x f)) (graph g)) by apply sg; graph_tac.
by rewrite (W_pr fg pg).
Qed.
Lemma extendsC_pr : forall (a b a' b':Set) (g:a'->b')(f:a->b)(H: sub a a'),
extendsC g f H -> forall x:a, Ro (f x) = Ro(g (inclusionC H x)).
Proof.
move=> a b a' b' g f saa' [e1].
rewrite /agreeC => eq x; rewrite eq.
by rewrite /restrictionC composeC_ev inclusionC_identity.
Qed.
Lemma function_extends_restr: forall f x,
is_function f -> sub x (source f) ->
extends f (restriction f x).
Proof.
move => f x ff ssf; split; fprops; split=>//.
rewrite /restriction; aw.
split; fprops; apply restr_sub.
Qed.
Lemma function_extends_restC: forall (x a b:Set) (f:a->b)(H:sub x a),
extendsC f (restrictionC f H) H.
Proof.
move=> x a b f xa; split; fprops.
move => t; rewrite /restrictionC compositionC_associative 2! composeC_ev.
rewrite inclusionC_compose.
apply f_equal. apply f_equal.
by apply R_inj; rewrite B_eq B_eq.
Qed.
Lemma agrees_same_restriction: forall f g x,
is_function f -> is_function g -> agrees_on x f g ->
target f = target g ->
restriction f x =
restriction g x.
Proof.
move=> f g x ff fg [ sf [sg vfg]] t.
apply function_exten; fprops; try solve [rewrite /restriction; aw].
rewrite {1} /restriction; aw=> z zs.
by do 2 rewrite restriction_W=>//; apply vfg.
Qed.
Lemma agrees_same_restrictionC: forall (a a' b x:Set) (f:a->b)(g:a'->b)
(Ha: sub x a)(Hb: sub x a'),
agreeC f g Ha Hb -> restrictionC f Ha =1 restrictionC g Hb.
Proof.
move => a a' b x f g xa xb ag z; apply R_inj; apply ag.
Qed.
Lemma restriction_graph1: forall f x,
is_function f -> sub x (source f) ->
graph (restriction f x) =
intersection2 (graph f)(product x (target f)).
Proof.
rewrite /restriction => f x ff xs; aw; set_extens t; aw; last by intuition.
move => [tg Ptx]; intuition; last by graph_tac.
have: (is_graph (graph f)) by fprops.
by apply.
Qed.
Lemma restriction_recovers: forall f x,
is_function f -> sub x (source f) ->
restriction f x = corresp x (target f)
(intersection2 (graph f)(product x (target f))).
Proof.
move=>f x ff ss; rewrite- (restriction_graph1 ff ss).
rewrite /restriction; aw.
Qed.
Restriction of a function on the source and target
Definition restriction2 f x y :=
corresp x y (intersection2 (graph f) (product x (target f))).
Definition restriction2_axioms f x y :=
is_function f &
sub x (source f) & sub y (target f) & sub (image_by_fun f x) y.
Lemma restriction2_graph: forall f x y,
sub (graph (restriction2 f x y)) (graph f).
Proof. by rewrite /restriction2=> f x y; aw; apply intersection2sub_first. Qed.
Lemma inc_graph_restriction2: forall f x y a b,
(inc (J a b) (graph (restriction2 f x y))) =
(inc (J a b) (graph f) & inc a x & inc b (target f)).
Proof.
rewrite /restriction2=> f x y a b; aw; apply iff_eq; intuition.
Qed.
Lemma restriction2_props: forall f x y,
restriction2_axioms f x y ->
domain (intersection2 (graph f) (product x (target f))) = x.
Proof.
move=> f x y ra; set i := intersection2 _ _.
have gi: (is_graph i) by rewrite /i => t; aw; intuition.
rewrite /i; set_extens t; dw; first by case=> z; aw; intuition.
move => tx; exists (W t f); aw; move:ra => [ ff [ xsf [ysf etc]]].
by split; fprops; graph_tac.
Qed.
Lemma restriction2_function: forall f x y,
restriction2_axioms f x y ->
is_function (restriction2 f x y).
Proof.
move=> f x y ra; move:(ra) => [ff [ss [st etc]]].
rewrite /restriction2.
move:(restriction2_props ra); set g := intersection2 _ _ => dg.
have fg: fgraph g.
rewrite /g; apply sub_graph_fgraph with (graph f); fprops.
by apply intersection2sub_first.
apply is_function_pr=>//.
rewrite /g; move=> t; dw; fprops.
move=> [u]; aw; move=> [Jg [ ip [ux tt]]].
by apply etc; aw; ex_tac; graph_tac.
Qed.
Hint Resolve restriction2_function: fprops.
Lemma restriction2_W: forall f x y a,
restriction2_axioms f x y ->
inc a x -> W a (restriction2 f x y) = W a f.
Proof.
move =>f x y a ra ax; move: (ra) => [aa bb].
rewrite /W/restriction2; aw.
apply sub_graph_ev; fprops; first by apply intersection2sub_first.
by rewrite (restriction2_props ra).
Qed.
Lemma function_rest_of_prolongation: forall f g,
extends g f -> f = restriction2 g (source f) (target f).
Proof.
move=> f g [ff [fg []]].
rewrite (sub_function ff fg); move => [_ [sts sg]] st.
have au: (sub (image_by_fun g (source f)) (target f)).
by move =>t; aw; move=>[u [us]] <-; rewrite -sg=>//; fprops.
have ax: (restriction2_axioms g (source f) (target f)) by hnf; auto.
apply function_exten;fprops; try solve [rewrite /restriction2; aw].
by move => x sf; rewrite restriction2_W // sg.
Qed.
Definition restriction2C (a a' b b':Set) (f:a->b)(Ha:sub a' a)
(H: forall u:a', inc (Ro (f (inclusionC Ha u))) b') :=
fun u=> Bo (H u).
Lemma restriction2C_pr: forall (a a' b b':Set) (f:a->b)(Ha:sub a' a)
(H: forall u:a', inc (Ro (f (inclusionC Ha u))) b') (x:a'),
Ro (restriction2C H x) = W (Ro x) (acreate f).
Proof.
rewrite /restriction2C=> a a' b b' f Ha H x; rewrite B_eq.
set (y:=inclusionC Ha x).
have RR: (Ro y = Ro x) by rewrite /y/inclusionC B_eq.
by rewrite -RR acreate_W.
Qed.
Lemma restriction2C_pr1: forall (a a' b b':Set) (f:a->b)
(Ha:sub a' a)(Hb:sub b' b)
(H: forall u:a', inc (Ro (f (inclusionC Ha u))) b'),
f \o (inclusionC Ha) =1 (inclusionC Hb) \o (restriction2C H).
Proof.
move=> a a' b b' f Ha Hb H t.
by rewrite /restriction2C; apply R_inj; rewrite B_eq B_eq.
Qed.
Function from a to b associated to the mapping f
Definition BL f a b := corresp a b (L a f).
Lemma bl_source : forall f a b, source (BL f a b) = a.
Proof. rewrite /BL/L=> f a b; aw. Qed.
Lemma bl_target : forall f a b, target (BL f a b) = b.
Proof. rewrite /BL/L=> f a b; aw. Qed.
Hint Rewrite bl_source bl_target : aw.
Lemma bl_graph1: forall f a b c,
inc c (graph (BL f a b)) -> c = J (P c) (f (P c)).
Proof.
by rewrite/BL/L=> f a b c; aw; move=> [z [_]] <-; aw.
Qed.
Lemma bl_graph2: forall f a b c,
inc c a -> inc (J c (f c)) (graph (BL f a b)).
Proof. by rewrite /BL/L=> f a b c ca; aw; ex_tac. Qed.
Lemma bl_graph3: forall f a b c,
inc c (graph (BL f a b)) -> inc (P c) a.
Proof. by rewrite /BL/L => f a b c; aw; move=> [z [za]] <-; aw.
Qed.
Lemma bl_graph4: forall f a b c,
inc c (graph (BL f a b)) -> f (P c) = (Q c).
Proof. by rewrite /BL/L => f a b c; aw; move => [z [_]] <-; aw. Qed.
Lemma bl_source : forall f a b, source (BL f a b) = a.
Proof. rewrite /BL/L=> f a b; aw. Qed.
Lemma bl_target : forall f a b, target (BL f a b) = b.
Proof. rewrite /BL/L=> f a b; aw. Qed.
Hint Rewrite bl_source bl_target : aw.
Lemma bl_graph1: forall f a b c,
inc c (graph (BL f a b)) -> c = J (P c) (f (P c)).
Proof.
by rewrite/BL/L=> f a b c; aw; move=> [z [_]] <-; aw.
Qed.
Lemma bl_graph2: forall f a b c,
inc c a -> inc (J c (f c)) (graph (BL f a b)).
Proof. by rewrite /BL/L=> f a b c ca; aw; ex_tac. Qed.
Lemma bl_graph3: forall f a b c,
inc c (graph (BL f a b)) -> inc (P c) a.
Proof. by rewrite /BL/L => f a b c; aw; move=> [z [za]] <-; aw.
Qed.
Lemma bl_graph4: forall f a b c,
inc c (graph (BL f a b)) -> f (P c) = (Q c).
Proof. by rewrite /BL/L => f a b c; aw; move => [z [_]] <-; aw. Qed.
In order for (BL f a b) to be a function, the following must be satisfied
Definition transf_axioms f a b :=
forall c, inc c a -> inc (f c) b.
Lemma bl_function: forall f a b,
transf_axioms f a b -> is_function (BL f a b).
Proof.
rewrite /BL=> f b c ta; apply is_function_pr; bw; gprops.
by move=> t; rewrite L_range; aw; move=> [z [zb]] <-; apply ta.
Qed.
Lemma bl_W: forall f a b c,
transf_axioms f a b -> inc c a-> W c (BL f a b) = f c.
Proof.
move=> f a b c ta ca; apply W_pr; [ by apply bl_function | by apply bl_graph2].
Qed.
Hint Rewrite bl_W : aw.
Lemma bl_recovers: forall f,
is_function f -> BL (fun z => W z f)(source f)(target f) = f.
Proof.
move=> f ff.
have ta: (transf_axioms (fun z => W z f) (source f) (target f))
by move=> x /=; fprops.
apply function_exten; aw; [ by apply bl_function | by move => x sx; aw].
Qed.
forall c, inc c a -> inc (f c) b.
Lemma bl_function: forall f a b,
transf_axioms f a b -> is_function (BL f a b).
Proof.
rewrite /BL=> f b c ta; apply is_function_pr; bw; gprops.
by move=> t; rewrite L_range; aw; move=> [z [zb]] <-; apply ta.
Qed.
Lemma bl_W: forall f a b c,
transf_axioms f a b -> inc c a-> W c (BL f a b) = f c.
Proof.
move=> f a b c ta ca; apply W_pr; [ by apply bl_function | by apply bl_graph2].
Qed.
Hint Rewrite bl_W : aw.
Lemma bl_recovers: forall f,
is_function f -> BL (fun z => W z f)(source f)(target f) = f.
Proof.
move=> f ff.
have ta: (transf_axioms (fun z => W z f) (source f) (target f))
by move=> x /=; fprops.
apply function_exten; aw; [ by apply bl_function | by move => x sx; aw].
Qed.
Functions associated to P and Q
Definition first_proj g := BL P g (domain g).
Definition second_proj g := BL Q g (range g).
Lemma first_proj_W: forall g x,
inc x g -> W x (first_proj g) = P x.
Proof. by rewrite /first_proj=> g x xg; aw; move=>t; apply inc_pr1_domain.
Qed.
Lemma second_proj_W: forall g x,
inc x g -> W x (second_proj g) = Q x.
Proof. by rewrite /second_proj=> g x xg; aw; move=>t; apply inc_pr2_range.
Qed.
Lemma first_proj_function:forall g,
is_function (first_proj g).
Proof.
by rewrite /first_proj =>g; apply bl_function; move=>t; apply inc_pr1_domain.
Qed.
Lemma second_proj_function :forall g,
is_function (second_proj g).
Proof.
by rewrite /second_proj=> g; apply bl_function; move=>t; apply inc_pr2_range.
Qed.
Condition for composition to be a function
Definition composable g f :=
is_function g & is_function f & source g = target f.
Notation "f1 \coP f2" := (composable f1 f2) (at level 50).
Lemma composable_pr: forall f g, g \coP f ->
fcomposable (graph g) (graph f).
Proof.
move=> f g [fg [ff st]]; split; fprops; split; fprops.
by aw; rewrite st; apply f_range_graph.
Qed.
Lemma composable_pr1: forall f g, g \coP f ->
graph (g \co f) = fcompose (graph g) (graph f).
Proof.
move=> f g cfg; move:(composable_pr cfg)=> ac.
rewrite -alternate_compose=> //.
move: cfg=> [ff [fg etc]].
have fgf: (fgraph (graph f)) by fprops.
have fgg: (fgraph (graph g)) by fprops.
rewrite /compose /gcompose/L; aw.
set_extens t; aw.
move => [pt [y [Jgf Jgg]]].
exists (P t); split; first by graph_tac.
move: (pr2_V fgf Jgf); aw; move=> <-.
move: (pr2_V fgg Jgg); aw; move <-.
by aw.
move => [z [zsf]] <-; aw; split; first by fprops.
have zd: (inc z (domain (graph f))) by aw.
move: (fdomain_pr1 fgf zd).
set y := V z _.
move=> yp; exists y; split=>//.
by apply fdomain_pr1 =>//; aw; rewrite etc /y; graph_tac.
Qed.
Lemma compose_domain:forall g f, g \coP f->
domain (graph (g \co f)) = domain (graph f).
Proof.
move => g f cfg;rewrite composable_pr1=>//.
by apply fcomposable_domain; apply composable_pr.
Qed.
Lemma compose_source: forall f g, source (g \co f) = source f.
Proof. rewrite /compose=> f g; aw. Qed.
Lemma compose_target: forall f g, target (g \co f) = target g.
Proof. rewrite /compose=> f g; aw. Qed.
Hint Rewrite compose_source compose_target : aw.
is_function g & is_function f & source g = target f.
Notation "f1 \coP f2" := (composable f1 f2) (at level 50).
Lemma composable_pr: forall f g, g \coP f ->
fcomposable (graph g) (graph f).
Proof.
move=> f g [fg [ff st]]; split; fprops; split; fprops.
by aw; rewrite st; apply f_range_graph.
Qed.
Lemma composable_pr1: forall f g, g \coP f ->
graph (g \co f) = fcompose (graph g) (graph f).
Proof.
move=> f g cfg; move:(composable_pr cfg)=> ac.
rewrite -alternate_compose=> //.
move: cfg=> [ff [fg etc]].
have fgf: (fgraph (graph f)) by fprops.
have fgg: (fgraph (graph g)) by fprops.
rewrite /compose /gcompose/L; aw.
set_extens t; aw.
move => [pt [y [Jgf Jgg]]].
exists (P t); split; first by graph_tac.
move: (pr2_V fgf Jgf); aw; move=> <-.
move: (pr2_V fgg Jgg); aw; move <-.
by aw.
move => [z [zsf]] <-; aw; split; first by fprops.
have zd: (inc z (domain (graph f))) by aw.
move: (fdomain_pr1 fgf zd).
set y := V z _.
move=> yp; exists y; split=>//.
by apply fdomain_pr1 =>//; aw; rewrite etc /y; graph_tac.
Qed.
Lemma compose_domain:forall g f, g \coP f->
domain (graph (g \co f)) = domain (graph f).
Proof.
move => g f cfg;rewrite composable_pr1=>//.
by apply fcomposable_domain; apply composable_pr.
Qed.
Lemma compose_source: forall f g, source (g \co f) = source f.
Proof. rewrite /compose=> f g; aw. Qed.
Lemma compose_target: forall f g, target (g \co f) = target g.
Proof. rewrite /compose=> f g; aw. Qed.
Hint Rewrite compose_source compose_target : aw.
Proposition 6: composition of functions is a function
Theorem compose_function: forall g f, g \coP f
-> is_function (g \co f).
Proof.
move=> g f cgf; move: (compose_domain cgf)=>cd.
have fggc: (fgraph (fcompose (graph g) (graph f))) by apply fcompose_fgraph.
move: (composable_pr1 cgf)=> cg; rewrite cg in cd.
move: cg; rewrite /compose; aw; move=> ->.
move: cgf => [fg [ff etc]].
apply is_function_pr =>//.
apply sub_trans with (range (graph g)).
by apply fcompose_range; fprops.
by apply f_range_graph.
by rewrite cd; rewrite f_domain_graph.
Qed.
-> is_function (g \co f).
Proof.
move=> g f cgf; move: (compose_domain cgf)=>cd.
have fggc: (fgraph (fcompose (graph g) (graph f))) by apply fcompose_fgraph.
move: (composable_pr1 cgf)=> cg; rewrite cg in cd.
move: cg; rewrite /compose; aw; move=> ->.
move: cgf => [fg [ff etc]].
apply is_function_pr =>//.
apply sub_trans with (range (graph g)).
by apply fcompose_range; fprops.
by apply f_range_graph.
by rewrite cd; rewrite f_domain_graph.
Qed.
Definition of injectivity, surjectivity and bijectivity
Definition injection f:=
is_function f &
(forall x y, inc x (source f) -> inc y (source f) ->
W x f = W y f -> x = y).
Definition surjection f :=
is_function f & image_of_fun f = target f.
Definition bijection f :=
injection f & surjection f.
is_function f &
(forall x y, inc x (source f) -> inc y (source f) ->
W x f = W y f -> x = y).
Definition surjection f :=
is_function f & image_of_fun f = target f.
Definition bijection f :=
injection f & surjection f.
We give here here some characterizations of injective, surjective, bijective functions
Lemma inj_is_function: forall f, injection f -> is_function f.
Proof. by move=> f; case. Qed.
Lemma surj_is_function: forall f, surjection f-> is_function f.
Proof. by move=> f; case. Qed.
Lemma bij_is_function: forall f, bijection f-> is_function f.
Proof. by move=> f; case; case. Qed.
Ltac fct_tac :=
match goal with
| H:bijection ?X1 |- is_function ?X1 => exact (bij_is_function H)
| H:injection ?X1 |- is_function ?X1 => exact (inj_is_function H)
| H:surjection ?X1 |- is_function ?X1 => exact (surj_is_function H)
| H:is_function ?X1 |- is_correspondence ?X1 =>
by case H
| H:is_function ?g |- sub (range (graph ?g)) (target ?g)
=> apply (f_range_graph H)
| H:composable ?X1 _ |- is_function ?X1 => destruct H as [H _ ]; exact H
| H:composable _ ?X1 |- is_function ?X1 => destruct H as [_ [H _ ]]; exact H
| H:composable ?f ?g |- is_function (compose ?f ?g ) =>
apply (compose_function H)
| H:is_function ?f |- is_function (compose ?f ?g ) =>
apply compose_function; apply conj=>//; apply conj
| H:is_function ?g |- is_function (compose ?f ?g ) =>
apply compose_function; apply conj; last apply conj=>//
| Ha:is_function ?f, Hb:is_function ?g |- ?f = ?g =>
apply function_exten
end.
More properties of function composition
Lemma compose_W: forall g f x, g \coP f ->
inc x (source f) -> W x (g \co f) = W (W x f) g.
Proof.
rewrite /W => g f x cgf xs; rewrite composable_pr1=>//.
apply fcompose_ev; [ by apply composable_pr | aw; fct_tac].
Qed.
Hint Rewrite compose_W: aw.
Lemma composable_acreate:forall (a b c:Set) (f: a-> b)(g: b->c),
(acreate g) \coP (acreate f).
Proof. rewrite/composable => a b c f g; aw; fprops.
Qed.
Lemma compose_acreate:forall (a b c:Set) (g: b->c)(f: a-> b),
(acreate g) \co (acreate f) = acreate (g \o f).
Proof.
move => a b c g f; move: (composable_acreate f g) => cfg.
apply function_exten; try fct_tac; fprops; aw.
by move=> x xa; aw; rewrite -(B_eq xa) 3! acreate_W.
Qed.
Lemma compose_assoc: forall f g h, f \coP g -> g \coP h ->
(f \co g) \co h = f \co (g \co h).
Proof.
move=> f g h cfg chg.
have: g \coP h by [].
move=> [gg [fh sgth]].
have ffg: (is_function (f \co g)) by fct_tac.
have fgh: (is_function (g \co h)) by fct_tac.
have cfgh: (f \co g) \coP h by hnf; aw.
have cfgh': (f \coP (g \co h)) by move: cfg=> [ff [_ etc]];hnf; aw.
apply function_exten; try fct_tac; aw.
by move=> x xh; aw; rewrite sgth; fprops.
Qed.
Lemma compose_id_left: forall m,
is_function m-> (identity (target m)) \co m = m.
Proof. move=> m fm; apply compose_identity_left; fct_tac. Qed.
Lemma compose_id_right: forall m,
is_function m-> m \co (identity (source m)) = m.
Proof. move=>m fm; apply compose_identity_right; fct_tac. Qed.
Lemma injective_pr: forall f x x' y,
injection f -> related (graph f) x y -> related (graph f) x' y -> x = x'.
Proof.
move=> f x x' y [ff injf] r1 r2; apply injf.
by apply (related_inc_source ff r1).
by apply (related_inc_source ff r2).
by rewrite (W_pr ff r1) (W_pr ff r2).
Qed.
Lemma injective_pr3: forall f x x' y,
injection f -> inc (J x y) (graph f) -> inc (J x' y) (graph f) -> x = x'.
Proof. move=> f x x' y; apply injective_pr. Qed.
Lemma injective_pr_bis: forall f,
is_function f ->
(forall x x' y, related (graph f) x y -> related (graph f) x' y -> x = x')
-> injection f.
Proof.
move=> f ff prop; hnf;ee.
move=> x y xs ys Weq; apply (prop x y (W x f)).
by apply (W_pr3 ff xs).
by rewrite Weq; apply (W_pr3 ff ys).
Qed.
Lemma surjective_pr: forall f y,
surjection f -> inc y (target f) ->
exists x, inc x (source f) & related (graph f) x y .
Proof. by move => f y [ff] => <-; rewrite/image_of_fun; aw. Qed.
Lemma surjective_pr2: forall f y,
surjection f -> inc y (target f) -> exists x, inc x (source f) & W x f = y.
Proof.
move=> f y sf yt; move:(surjective_pr sf yt)=> [x [xs px]].
by exists x; split=>//; apply W_pr =>//;fct_tac.
Qed.
Lemma surjective_pr3: forall f,
surjection f -> range (graph f) = target f.
Proof.
move => t sf; apply extensionality.
by move: sf =>[ff _] ; fct_tac.
move => x xt; case (surjective_pr sf xt)=> [y [yr yg]] .
by rewrite range0_rw; exists (J y x); split;aw.
Qed.
Lemma surjective_pr4: forall f,
is_function f-> range (graph f) = target f -> surjection f.
Proof.
move=> f ff rg; split=>//. move: ff=> [_ [[gr _] sd]].
by rewrite/image_of_fun sd image_by_graph_domain.
Qed.
Lemma surjective_pr5: forall f,
is_function f -> (forall y, inc y (target f) ->
exists x, inc x (source f) & related (graph f) x y) -> surjection f.
Proof.
move=> f ff prop; apply surjective_pr4=>//.
apply extensionality; first by fct_tac.
by move=> x xt; case (prop _ xt)=> y [ys rel]; dw; fprops; red in rel; ex_tac.
Qed.
Lemma surjective_pr6: forall f,
is_function f-> (forall y, inc y (target f) ->
exists x, inc x (source f) & W x f = y) -> surjection f.
Proof.
move=> f ff prop; apply surjective_pr5=>//.
by move=> y yt; case (prop _ yt)=> x [xs] => <-; ex_tac;red; graph_tac.
Qed.
Lemma bl_injective: forall f a b, transf_axioms f a b ->
(forall u v, inc u a-> inc v a -> f u = f v -> u = v) ->
injection (BL f a b).
Proof.
move=> f a b ta prop; split; first by apply bl_function.
by aw; move=> x y xs ys; do 2 rewrite bl_W=>//; apply prop.
Qed.
Lemma bl_surjective: forall f a b, transf_axioms f a b ->
(forall y, inc y b -> exists x, inc x a & f x = y) ->
surjection (BL f a b).
Proof.
move=> f a b ta prop; apply surjective_pr6; first by apply bl_function.
by aw; move=> y yt; case (prop _ yt)=> x [xa fy]; ex_tac; rewrite bl_W.
Qed.
Lemma bl_bijective: forall f a b, transf_axioms f a b ->
(forall u v, inc u a-> inc v a -> f u = f v -> u = v) ->
(forall y, inc y b -> exists x, inc x a & f x = y) ->
bijection (BL f a b).
Proof.
by move =>f a b ta pi ps; split; [apply bl_injective| apply bl_surjective].
Qed.
Lemma bijective_pr: forall f y,
bijection f -> inc y (target f) ->
exists_unique (fun x=> inc x (source f) & W x f = y).
Proof.
move=> f y [[_ inj] sf] yt.
split; first by apply surjective_pr2.
by move=> x x' [xs Wx] [x's Wx']; rewrite -Wx' in Wx; apply inj.
Qed.
Lemma function_exten4: forall f g, source f = source g ->
surjection f -> surjection g ->
(forall x, inc x (source f) -> W x f = W x g) -> f = g.
Proof.
move=> f g sfg sf sg Weq.
have ff: is_function f by fct_tac.
have fg: is_function g by fct_tac.
have geq: (graph f = graph g) by apply fgraph_exten; fprops; aw.
apply function_exten1=>//.
by rewrite -(surjective_pr3 sf) -(surjective_pr3 sg) geq.
Qed.
Bijectivity of Coq functions
Definition injectiveC (a b:Set) (f:a->b) := forall u v, f u = f v -> u =v.
Definition surjectiveC (a b:Set) (f:a->b) := forall u, exists v, f v = u.
Definition bijectiveC (a b:Set) (f:a->b) := injectiveC f & surjectiveC f.
Lemma bijectiveC_pr: forall (a b:Set) (f:a->b) (y:b),
bijectiveC f -> exists_unique (fun x:a=> f x =y).
Proof.
move=> a b f y [fi fs]; split; first by apply fs.
by move=> x x' <-; move=> veq; symmetry; apply fi.
Qed.
Lemma bcreate_injective: forall f a b
(H:is_function f)(Ha:source f =a)(Hb:target f =b),
injection f -> injectiveC (bcreate H Ha Hb).
Proof.
move=> f a b H Ha Hb [ff fi] x y eql; apply R_inj; apply fi.
by rewrite Ha; apply R_inc.
by rewrite Ha; apply R_inc.
by move: (f_equal (@Ro b) eql); rewrite 2! prop_bcreate2.
Qed.
Lemma bcreate_surjective: forall f a b
(H:is_function f)(Ha:source f =a)(Hb:target f =b),
surjection f -> surjectiveC (bcreate H Ha Hb).
Proof.
move=> f a b H Ha Hb sf u.
have Rt: (inc (Ro u) (target f)) by rewrite Hb; apply R_inc.
move: (surjective_pr2 sf Rt) => [x [xs xv]].
rewrite Ha in xs; exists (Bo xs).
by apply R_inj; rewrite -xv prop_bcreate2 B_eq.
Qed.
Lemma bcreate_bijective: forall f a b
(H:is_function f)(Ha:source f =a)(Hb:target f =b),
bijection f -> bijectiveC (bcreate H Ha Hb).
Proof.
move=> f a b H Ha Hb [fi fs].
by split ; [apply bcreate_injective | apply bcreate_surjective].
Qed.
Lemma bcreate1_injective: forall f (H:is_function f),
injection f -> injectiveC (bcreate1 H).
Proof.
by move=> f H fi x y; rewrite !(bcreate_eq H); apply bcreate_injective.
Qed.
Lemma bcreate1_surjective: forall f (H:is_function f),
surjection f -> surjectiveC (bcreate1 H).
Proof.
move=> f H sf x.
move: (bcreate_surjective H (refl_equal (source f))
(refl_equal (target f)) sf x) => [v xsf]; exists v.
by rewrite -xsf -(bcreate_eq H).
Qed.
Lemma bcreate1_bijective: forall f (H:is_function f),
bijection f -> bijectiveC (bcreate1 H).
Proof.
move=> f H [p1 p2];split.
apply bcreate1_injective =>//.
apply bcreate1_surjective =>//.
Qed.
Lemma acreate_injective: forall (a b:Set) (f:a->b),
injectiveC f -> injection (acreate f).
Proof.
move=> a b f fi; split; first by fprops.
move=> x y; rewrite {1 2} /acreate; aw => xa ya.
rewrite -(B_eq xa) - (B_eq ya) (acreate_W f (Bo xa)) (acreate_W f (Bo ya)).
by move=> eq; move: (R_inj eq)=> eqv; rewrite (fi _ _ eqv).
Qed.
Lemma acreate_surjective: forall (a b:Set) (f:a->b),
surjectiveC f -> surjection (acreate f).
Proof.
move=> a b f sf; apply surjective_pr6; fprops.
aw; move => y yb; move: (sf (Bo yb)) => [v fv].
by exists (Ro v); split; [by apply R_inc | rewrite acreate_W fv B_eq].
Qed.
Lemma acreate_bijective: forall (a b:Set) (f:a->b),
bijectiveC f -> bijection (acreate f).
Proof.
move=> a b f [i j].
by split; [ apply acreate_injective| apply acreate_surjective].
Qed.
Definition surjectiveC (a b:Set) (f:a->b) := forall u, exists v, f v = u.
Definition bijectiveC (a b:Set) (f:a->b) := injectiveC f & surjectiveC f.
Lemma bijectiveC_pr: forall (a b:Set) (f:a->b) (y:b),
bijectiveC f -> exists_unique (fun x:a=> f x =y).
Proof.
move=> a b f y [fi fs]; split; first by apply fs.
by move=> x x' <-; move=> veq; symmetry; apply fi.
Qed.
Lemma bcreate_injective: forall f a b
(H:is_function f)(Ha:source f =a)(Hb:target f =b),
injection f -> injectiveC (bcreate H Ha Hb).
Proof.
move=> f a b H Ha Hb [ff fi] x y eql; apply R_inj; apply fi.
by rewrite Ha; apply R_inc.
by rewrite Ha; apply R_inc.
by move: (f_equal (@Ro b) eql); rewrite 2! prop_bcreate2.
Qed.
Lemma bcreate_surjective: forall f a b
(H:is_function f)(Ha:source f =a)(Hb:target f =b),
surjection f -> surjectiveC (bcreate H Ha Hb).
Proof.
move=> f a b H Ha Hb sf u.
have Rt: (inc (Ro u) (target f)) by rewrite Hb; apply R_inc.
move: (surjective_pr2 sf Rt) => [x [xs xv]].
rewrite Ha in xs; exists (Bo xs).
by apply R_inj; rewrite -xv prop_bcreate2 B_eq.
Qed.
Lemma bcreate_bijective: forall f a b
(H:is_function f)(Ha:source f =a)(Hb:target f =b),
bijection f -> bijectiveC (bcreate H Ha Hb).
Proof.
move=> f a b H Ha Hb [fi fs].
by split ; [apply bcreate_injective | apply bcreate_surjective].
Qed.
Lemma bcreate1_injective: forall f (H:is_function f),
injection f -> injectiveC (bcreate1 H).
Proof.
by move=> f H fi x y; rewrite !(bcreate_eq H); apply bcreate_injective.
Qed.
Lemma bcreate1_surjective: forall f (H:is_function f),
surjection f -> surjectiveC (bcreate1 H).
Proof.
move=> f H sf x.
move: (bcreate_surjective H (refl_equal (source f))
(refl_equal (target f)) sf x) => [v xsf]; exists v.
by rewrite -xsf -(bcreate_eq H).
Qed.
Lemma bcreate1_bijective: forall f (H:is_function f),
bijection f -> bijectiveC (bcreate1 H).
Proof.
move=> f H [p1 p2];split.
apply bcreate1_injective =>//.
apply bcreate1_surjective =>//.
Qed.
Lemma acreate_injective: forall (a b:Set) (f:a->b),
injectiveC f -> injection (acreate f).
Proof.
move=> a b f fi; split; first by fprops.
move=> x y; rewrite {1 2} /acreate; aw => xa ya.
rewrite -(B_eq xa) - (B_eq ya) (acreate_W f (Bo xa)) (acreate_W f (Bo ya)).
by move=> eq; move: (R_inj eq)=> eqv; rewrite (fi _ _ eqv).
Qed.
Lemma acreate_surjective: forall (a b:Set) (f:a->b),
surjectiveC f -> surjection (acreate f).
Proof.
move=> a b f sf; apply surjective_pr6; fprops.
aw; move => y yb; move: (sf (Bo yb)) => [v fv].
by exists (Ro v); split; [by apply R_inc | rewrite acreate_W fv B_eq].
Qed.
Lemma acreate_bijective: forall (a b:Set) (f:a->b),
bijectiveC f -> bijection (acreate f).
Proof.
move=> a b f [i j].
by split; [ apply acreate_injective| apply acreate_surjective].
Qed.
Equipotent means there is a bijection between the sets
Definition equipotent x y :=
exists z, bijection z & source z = x & target z = y.
Notation "x \Eq y" := (equipotent x y) (at level 50).
Lemma equipotentC: forall x y, x \Eq y = exists f:x->y, bijectiveC f.
Proof.
move=> x y; apply iff_eq.
move=> [z [bz [sz tz]]].
have fz: (is_function z) by fct_tac.
by exists (bcreate fz sz tz); apply bcreate_bijective.
by move=> [f bf]; exists (acreate f); split; [apply acreate_bijective | aw].
Qed.
exists z, bijection z & source z = x & target z = y.
Notation "x \Eq y" := (equipotent x y) (at level 50).
Lemma equipotentC: forall x y, x \Eq y = exists f:x->y, bijectiveC f.
Proof.
move=> x y; apply iff_eq.
move=> [z [bz [sz tz]]].
have fz: (is_function z) by fct_tac.
by exists (bcreate fz sz tz); apply bcreate_bijective.
by move=> [f bf]; exists (acreate f); split; [apply acreate_bijective | aw].
Qed.
Injectivity and surjectivity of identity and restriction
Lemma identity_bijective: forall x,
bijection (identity x).
Proof.
move=> x; move: (identity_function x) => fi.
split; first by split; fprops; aw; move=> a b ax bx ; srw.
by apply surjective_pr6; aw; move=> y yx; ex_tac; srw.
Qed.
Lemma identityC_bijective: forall (x:Set),
bijectiveC (@id x).
Proof. by move=>x;split => //; move=> u; exists u. Qed.
Lemma restriction2_injective: forall f x y,
injection f -> restriction2_axioms f x y
-> injection (restriction2 f x y).
Proof.
move=> f x y [_ fi] ra; split; first by apply restriction2_function.
rewrite {1 2}/restriction2; aw=> a b ax bx.
move: ra=> [ff [sf etc]].
by do 2 rewrite restriction2_W=>//; apply fi; apply sf.
Qed.
Lemma restriction2_surjective: forall f x y,
restriction2_axioms f x y ->
source f = x -> image_of_fun f = y ->
surjection (restriction2 f x y).
Proof.
move=> f x y ra sf iy.
apply surjective_pr6; first by apply restriction2_function.
rewrite /restriction2; aw=> a ay.
move: ay; rewrite -{1} iy /image_of_fun sf; aw; move => [b [bx Jg]].
by ex_tac; rewrite restriction2_W=> //; move:ra=> [ff _]; apply W_pr.
Qed.
Lemma restriction1_surjective: forall f x,
is_function f -> sub x (source f) ->
surjection (restriction1 f x).
Proof.
move=> f x ff sxs; apply surjective_pr6; first by apply restriction1_function.
rewrite /restriction1; aw=> a ay.
move: ay; rewrite /image_of_fun; aw; move => [b [bx Jg]].
by ex_tac; rewrite restriction1_W=> //; move:ra=> [ff _]; apply W_pr.
Qed.
Lemma restriction1_bijective: forall f x,
injection f -> sub x (source f) ->
bijection (restriction1 f x).
Proof.
move=> f x [ff fi] sxf; split; last by apply restriction1_surjective.
split; first by apply restriction1_function.
rewrite /restriction1; aw=> a b ax bx.
by do 2 rewrite restriction1_W=>//; apply fi; apply sxf.
Qed.
bijection (identity x).
Proof.
move=> x; move: (identity_function x) => fi.
split; first by split; fprops; aw; move=> a b ax bx ; srw.
by apply surjective_pr6; aw; move=> y yx; ex_tac; srw.
Qed.
Lemma identityC_bijective: forall (x:Set),
bijectiveC (@id x).
Proof. by move=>x;split => //; move=> u; exists u. Qed.
Lemma restriction2_injective: forall f x y,
injection f -> restriction2_axioms f x y
-> injection (restriction2 f x y).
Proof.
move=> f x y [_ fi] ra; split; first by apply restriction2_function.
rewrite {1 2}/restriction2; aw=> a b ax bx.
move: ra=> [ff [sf etc]].
by do 2 rewrite restriction2_W=>//; apply fi; apply sf.
Qed.
Lemma restriction2_surjective: forall f x y,
restriction2_axioms f x y ->
source f = x -> image_of_fun f = y ->
surjection (restriction2 f x y).
Proof.
move=> f x y ra sf iy.
apply surjective_pr6; first by apply restriction2_function.
rewrite /restriction2; aw=> a ay.
move: ay; rewrite -{1} iy /image_of_fun sf; aw; move => [b [bx Jg]].
by ex_tac; rewrite restriction2_W=> //; move:ra=> [ff _]; apply W_pr.
Qed.
Lemma restriction1_surjective: forall f x,
is_function f -> sub x (source f) ->
surjection (restriction1 f x).
Proof.
move=> f x ff sxs; apply surjective_pr6; first by apply restriction1_function.
rewrite /restriction1; aw=> a ay.
move: ay; rewrite /image_of_fun; aw; move => [b [bx Jg]].
by ex_tac; rewrite restriction1_W=> //; move:ra=> [ff _]; apply W_pr.
Qed.
Lemma restriction1_bijective: forall f x,
injection f -> sub x (source f) ->
bijection (restriction1 f x).
Proof.
move=> f x [ff fi] sxf; split; last by apply restriction1_surjective.
split; first by apply restriction1_function.
rewrite /restriction1; aw=> a b ax bx.
by do 2 rewrite restriction1_W=>//; apply fi; apply sxf.
Qed.
Extension of a function by adding f(x)=y
Definition tack_on_f f x y:=
corresp (tack_on (source f) x)
(tack_on (target f) y) (tack_on (graph f) (J x y)).
Lemma tack_on_corresp: forall f x y,
is_correspondence f -> is_correspondence (tack_on_f f x y).
Proof.
rewrite /tack_on_f=> f x y cf; apply corresp_create.
move=> t; aw; case.
by move: cf => [_ sg] tg; move: (sg _ tg); aw; intuition.
by move=> ->; aw; intuition.
Qed.
Lemma tack_on_function: forall f x y,
is_function f -> ~ (inc x (source f)) -> is_function (tack_on_f f x y).
Proof.
rewrite /tack_on_f => f x y [cf [ff sf ]] nxsf; apply is_function_pr.
by rewrite sf in nxsf; apply tack_on_fgraph.
rewrite range_tack_on; move => t; aw;dw; fprops.
case ; last by intuition.
by move=> [v Jv]; left;case cf; move => _ s; move:(s _ Jv); aw; intuition.
by rewrite sf; rewrite domain_tack_on.
Qed.
Hint Resolve tack_on_function: fprops.
Lemma tack_on_W_in: forall f x y u,
is_function f -> ~(inc x (source f)) -> inc u (source f) ->
W u (tack_on_f f x y) = W u f.
Proof.
move=> f x y u ff nixs uf; apply W_pr; fprops.
by rewrite /tack_on_f; aw; left; graph_tac.
Qed.
Lemma tack_on_W_out: forall f x y,
is_function f -> ~(inc x (source f)) ->
W x (tack_on_f f x y) = y.
Proof.
by move=> f x y ff nixs; apply W_pr; fprops; rewrite /tack_on_f; aw; auto.
Qed.
Lemma tack_on_V_out: forall f x y,
fgraph f -> ~ (inc x (domain f)) ->
V x (tack_on f (J x y)) = y.
Proof.
move=> f x y ff nixs.
move: (tack_on_fgraph y ff nixs) => fg.
have h1: inc (J x y) (tack_on f (J x y)) by fprops.
symmetry; move: (pr2_V fg h1); aw.
Qed.
Lemma tack_on_V_in: forall f x y u,
fgraph f -> ~ (inc x (domain f)) -> inc u (domain f) ->
V u (tack_on f (J x y)) = V u f.
Proof.
move=> f x y u ff nixs udf.
move: (fdomain_pr1 ff udf) => aux.
move: (tack_on_fgraph y ff nixs) => fg.
have h1: inc (J u (V u f)) (tack_on f (J x y)) by fprops.
symmetry; move: (pr2_V fg h1); aw.
Qed.
Lemma tack_on_surjective: forall f x y,
surjection f -> ~(inc x (source f)) -> surjection (tack_on_f f x y).
Proof.
move=> f x y sf nixsf.
have ff: is_function f by fct_tac.
apply surjective_pr6; first by fprops.
rewrite /tack_on_f; aw => z; aw; case.
move=> zt; move: (surjective_pr2 sf zt)=> [u [us wu]].
by exists u; split; first (by aw ;intuition) ; rewrite tack_on_W_in.
by move =>->; exists x; split; fprops; rewrite tack_on_W_out.
Qed.
Lemma tack_on_f_injective: forall x f g a b,
is_function f -> is_function g -> target f = target g ->
source f = source g -> ~ (inc x (source f)) ->
(tack_on_f f x a = tack_on_f g x b) -> f = g.
Proof.
move=> x f g a b ff fg teq seq nixsf sv; apply function_exten; fprops.
move=>t ts; rewrite - (tack_on_W_in a ff nixsf ts).
by rewrite seq in nixsf ts; rewrite - (tack_on_W_in b fg nixsf ts) sv.
Qed.
Lemma tack_on_g_injective: forall x f g a b,
fgraph f -> fgraph g ->
domain f = domain g -> ~ (inc x (domain f)) ->
(tack_on f (J x a) = tack_on g (J x b)) -> f = g.
Proof.
move=> x f g a b ff fg seq nixsf sv.
apply fgraph_exten => //.
move=>t ts; rewrite - (tack_on_V_in a ff nixsf ts).
by rewrite seq in nixsf ts; rewrite - (tack_on_V_in b fg nixsf ts) sv.
Qed.
Lemma restr_tack_on: forall f x a,
fgraph f -> ~ (inc x (domain f)) ->
restr (tack_on f (J x a)) (domain f) = f.
Proof.
move=> f x a fgf xdf; rewrite /restr.
set_extens y; rewrite Z_rw tack_on_rw.
move=> [h Px]; case h => //.
by move=> aux; elim xdf; move: Px; rewrite aux pr1_pair.
by move=> yf; split; ee; apply inc_pr1_domain.
Qed.
Lemma tack_on_restr: forall f x E, fgraph f -> ~ (inc x E) ->
domain f = tack_on E x->
tack_on (restr f E) (J x (V x f)) = f.
Proof.
move=> f x E fgf nxE df.
have sEd: sub E (domain f) by rewrite df; fprops.
have dr: (domain (restr f E)) = E by rewrite restr_domain1 =>//.
have fgr: fgraph (restr f E) by fprops.
have nxe: ~ inc x (domain (restr f E)) by ue.
apply fgraph_exten =>//.
apply tack_on_fgraph =>//.
by rewrite domain_tack_on dr df.
move=> u; rewrite domain_tack_on dr tack_on_rw; case.
move=> uE.
have ud: inc u (domain (restr f E)) by rewrite dr.
rewrite tack_on_V_in // restr_ev //.
move=> ->; rewrite tack_on_V_out //.
Qed.
Canonical injection of a set into another
Definition canonical_injection a b :=
corresp a b (identity_g a).
Lemma ci_function: forall a b, sub a b ->
is_function (canonical_injection a b).
Proof.
rewrite/canonical_injection=> a b ab; apply is_function_pr.
by apply identity_fgraph.
by rewrite identity_range.
by rewrite identity_domain.
Qed.
Hint Resolve ci_function : fprops.
Lemma ci_W: forall a b x,
sub a b -> inc x a -> W x (canonical_injection a b) = x.
Proof.
by rewrite /W /canonical_injection=> a b x ab xa; aw; apply identity_ev.
Qed.
Lemma ci_injective: forall a b,
sub a b -> injection (canonical_injection a b).
Proof.
move=> a b ab; split; first by fprops.
rewrite /canonical_injection; aw=> x y xa ya.
by do 2 rewrite ci_W=>//.
Qed.
Lemma ci_range: forall a b, sub a b ->
range (graph (canonical_injection a b)) = a.
Proof. by rewrite /canonical_injection=> a b ab; aw; rewrite identity_range.
Qed.
Lemma inclusionC_injective: forall a b (H: sub a b),
injectiveC (inclusionC H).
Proof.
rewrite /inclusionC=> a b ab x y rql; apply R_inj.
transitivity (Ro (Bo (ab (Ro x) (R_inc x)))).
by symmetry; apply B_eq.
simpl in rql; by rewrite rql; apply B_eq.
Qed.
Definition set_of_gfunctions x y:=
Zo (powerset (product x y))(fun z => fgraph z & x = domain z).
corresp a b (identity_g a).
Lemma ci_function: forall a b, sub a b ->
is_function (canonical_injection a b).
Proof.
rewrite/canonical_injection=> a b ab; apply is_function_pr.
by apply identity_fgraph.
by rewrite identity_range.
by rewrite identity_domain.
Qed.
Hint Resolve ci_function : fprops.
Lemma ci_W: forall a b x,
sub a b -> inc x a -> W x (canonical_injection a b) = x.
Proof.
by rewrite /W /canonical_injection=> a b x ab xa; aw; apply identity_ev.
Qed.
Lemma ci_injective: forall a b,
sub a b -> injection (canonical_injection a b).
Proof.
move=> a b ab; split; first by fprops.
rewrite /canonical_injection; aw=> x y xa ya.
by do 2 rewrite ci_W=>//.
Qed.
Lemma ci_range: forall a b, sub a b ->
range (graph (canonical_injection a b)) = a.
Proof. by rewrite /canonical_injection=> a b ab; aw; rewrite identity_range.
Qed.
Lemma inclusionC_injective: forall a b (H: sub a b),
injectiveC (inclusionC H).
Proof.
rewrite /inclusionC=> a b ab x y rql; apply R_inj.
transitivity (Ro (Bo (ab (Ro x) (R_inc x)))).
by symmetry; apply B_eq.
simpl in rql; by rewrite rql; apply B_eq.
Qed.
Definition set_of_gfunctions x y:=
Zo (powerset (product x y))(fun z => fgraph z & x = domain z).
Diagonal application
Definition diagonal_application a :=
BL (fun x=> J x x) a (product a a).
Lemma diag_app_W: forall a x,
inc x a -> W x (diagonal_application a) = J x x.
Proof.
by rewrite /diagonal_application=> a x xa;aw; move=> y/=; fprops.
Qed.
Lemma diag_app_injective: forall a,
injection (diagonal_application a).
Proof.
rewrite /diagonal_application=> a; apply bl_injective.
by move=> y /=; fprops.
by move => u v _ _; apply pr1_def.
Qed.
Lemma diag_app_function: forall a,
is_function (diagonal_application a).
Proof. move=>a; by case (diag_app_injective a). Qed.
Lemma diag_app_range: forall a,
range (graph (diagonal_application a)) = diagonal a.
Proof.
move=>a;rewrite diagonal_is_identity /diagonal_application.
set_extens t; rewrite /BL corresp_graph L_range_rw inc_diagonal_rw.
by move => [b [ba]] <-; aw; fprops.
by move=> [pt [Pa PQ]]; ex_tac; apply pair_exten; fprops; aw.
Qed.
Injectivity and surjectivity of P and Q
Lemma second_proj_surjective: forall g,
surjection (second_proj g).
Proof.
move=> g; apply surjective_pr5; first by apply second_proj_function.
rewrite /second_proj; aw; rewrite /BL/range/related.
by move=> y; aw; move=> [z [zg]] <- ;ex_tac; aw; ex_tac.
Qed.
Lemma first_proj_surjective: forall g ,
surjection (first_proj g).
Proof.
move=> g; apply surjective_pr5; first by apply first_proj_function.
rewrite /first_proj; aw; rewrite /BL/domain/related.
by move=> y; aw; move=> [z [zg]] <- ;ex_tac; aw; ex_tac.
Qed.
Lemma first_proj_injective: forall g,
is_graph g -> (injection (first_proj g) = functional_graph g).
Proof.
move=> g gg.
have fpf: (is_function (first_proj g)) by apply first_proj_function.
have Ht: source (first_proj g) = g by rewrite/first_proj; aw.
rewrite /injection Ht.
apply iff_eq.
move=> [_ hyp] a b b'; rewrite /related => i1 i2.
suff: (J a b = J a b') by apply pr2_def.
by apply hyp=>//; rewrite first_proj_W=>//; rewrite first_proj_W=>//; aw.
split=>//; move=>x y xg yg; do 2 rewrite first_proj_W=>//.
have: fgraph g by rewrite -is_functional.
by move => [_]; apply.
Qed.
The function that maps J x y to J y x
Definition inv_graph_canon g :=
BL (fun x=> J (Q x) (P x)) g (inverse_graph g).
Lemma inv_graph_canon_W: forall g x,
is_graph g ->inc x g -> W x (inv_graph_canon g) = J (Q x) (P x).
Proof.
rewrite/inv_graph_canon=> g x gg xg; aw.
by move=> c cg /=; aw; rewrite gg.
Qed.
Lemma inv_graph_canon_function: forall g,
is_graph g -> is_function (inv_graph_canon g).
Proof.
rewrite /inv_graph_canon=> g gg; apply bl_function.
by move=> c cg /=; aw; rewrite gg.
Qed.
Lemma inv_graph_canon_bijective: forall g,
is_graph g -> bijection (inv_graph_canon g).
Proof.
rewrite /inv_graph_canon=> g gg; apply bl_bijective.
by move=> c cg /=; aw; rewrite gg.
move=> u v ug vg peq; apply pair_exten; try apply gg=>//.
by apply (pr2_def peq).
by apply (pr1_def peq).
move=> y; rewrite inverse_graph_rw=> //.
by move=> [py pg]; ex_tac; aw.
Qed.
BL (fun x=> J (Q x) (P x)) g (inverse_graph g).
Lemma inv_graph_canon_W: forall g x,
is_graph g ->inc x g -> W x (inv_graph_canon g) = J (Q x) (P x).
Proof.
rewrite/inv_graph_canon=> g x gg xg; aw.
by move=> c cg /=; aw; rewrite gg.
Qed.
Lemma inv_graph_canon_function: forall g,
is_graph g -> is_function (inv_graph_canon g).
Proof.
rewrite /inv_graph_canon=> g gg; apply bl_function.
by move=> c cg /=; aw; rewrite gg.
Qed.
Lemma inv_graph_canon_bijective: forall g,
is_graph g -> bijection (inv_graph_canon g).
Proof.
rewrite /inv_graph_canon=> g gg; apply bl_bijective.
by move=> c cg /=; aw; rewrite gg.
move=> u v ug vg peq; apply pair_exten; try apply gg=>//.
by apply (pr2_def peq).
by apply (pr1_def peq).
move=> y; rewrite inverse_graph_rw=> //.
by move=> [py pg]; ex_tac; aw.
Qed.
Example 5 page 17 of Bourbaki (page 85 in the English edition)
Lemma bourbaki_ex5_17: forall a b,
bijection (BL (fun x=> J x b) a (product a (singleton b))).
Proof.
move=> a b;apply bl_bijective.
by move=> x xa /=; aw; fprops.
by move=> u v _ _; apply pr1_def.
by move=> y; aw; move=> [py [Pya]] <-; ex_tac; aw.
Qed.
Lemma equipotent_aux: forall f a b,
bijection (BL f a b) -> a \Eq b.
Proof. move=> f a b p; exists (BL f a b); aw; fprops. Qed.
Lemma equipotent_prod_singleton:
forall a b, a \Eq (product a (singleton b)).
Proof.
move=> a b; move: (bourbaki_ex5_17 a b); apply equipotent_aux.
Qed.
Lemma restriction1_pr: forall f,
is_function f -> restriction2 f (source f) (image_by_fun f (source f)) =
restriction1 f (source f).
Proof.
rewrite/restriction2/restriction1=> f ff.
have rg: (restr (graph f) (source f) = graph f).
apply extensionality; first by apply restr_sub.
by move=> t tg; rewrite restr_inc_rw; split; fprops; graph_tac.
by move: ff=> [[_ p] _]; rewrite intersection2_sub in p; rewrite rg p.
Qed.
bijection (BL (fun x=> J x b) a (product a (singleton b))).
Proof.
move=> a b;apply bl_bijective.
by move=> x xa /=; aw; fprops.
by move=> u v _ _; apply pr1_def.
by move=> y; aw; move=> [py [Pya]] <-; ex_tac; aw.
Qed.
Lemma equipotent_aux: forall f a b,
bijection (BL f a b) -> a \Eq b.
Proof. move=> f a b p; exists (BL f a b); aw; fprops. Qed.
Lemma equipotent_prod_singleton:
forall a b, a \Eq (product a (singleton b)).
Proof.
move=> a b; move: (bourbaki_ex5_17 a b); apply equipotent_aux.
Qed.
Lemma restriction1_pr: forall f,
is_function f -> restriction2 f (source f) (image_by_fun f (source f)) =
restriction1 f (source f).
Proof.
rewrite/restriction2/restriction1=> f ff.
have rg: (restr (graph f) (source f) = graph f).
apply extensionality; first by apply restr_sub.
by move=> t tg; rewrite restr_inc_rw; split; fprops; graph_tac.
by move: ff=> [[_ p] _]; rewrite intersection2_sub in p; rewrite rg p.
Qed.
Proposition 7 summarizes next two theorems. Let f be a function; then
f is a bijection if and only if its inverse is a function
Theorem bijective_inv_function: forall f,
bijection f -> is_function (inverse_fun f).
Proof.
rewrite /inverse_fun=> f [fi fs].
have gf: (is_graph (graph f)) by move: fi=> [ff _]; fprops.
have fgf: fgraph (inverse_graph (graph f)).
split; fprops; move=> x y; do 2 rewrite inverse_graph_rw=>//.
move =>[px pf] [qx qf] peq; apply pair_exten =>//.
by rewrite -peq in qf; apply (injective_pr3 fi pf qf).
apply is_function_pr=>//.
by rewrite range_inverse=>//; aw; fprops; fct_tac.
by symmetry; rewrite domain_inverse=>//; apply surjective_pr3.
Qed.
Theorem inv_function_bijective: forall f,
is_function f -> is_function (inverse_fun f) -> bijection f.
Proof.
move=> f ff fif.
have geq: inverse_graph (graph f) = graph (inverse_fun f).
by rewrite/inverse_fun; aw.
split.
apply injective_pr_bis=>//; move=> x x' y.
rewrite /related -inverse_graph_pair geq => r1.
rewrite -inverse_graph_pair geq => r2.
by move: fif => [_ [ fg _ ]]; apply (fgraph_pr fg r1 r2).
apply surjective_pr4=> //; rewrite - domain_inverse; fprops.
by rewrite geq /inverse_fun; aw.
Qed.
bijection f -> is_function (inverse_fun f).
Proof.
rewrite /inverse_fun=> f [fi fs].
have gf: (is_graph (graph f)) by move: fi=> [ff _]; fprops.
have fgf: fgraph (inverse_graph (graph f)).
split; fprops; move=> x y; do 2 rewrite inverse_graph_rw=>//.
move =>[px pf] [qx qf] peq; apply pair_exten =>//.
by rewrite -peq in qf; apply (injective_pr3 fi pf qf).
apply is_function_pr=>//.
by rewrite range_inverse=>//; aw; fprops; fct_tac.
by symmetry; rewrite domain_inverse=>//; apply surjective_pr3.
Qed.
Theorem inv_function_bijective: forall f,
is_function f -> is_function (inverse_fun f) -> bijection f.
Proof.
move=> f ff fif.
have geq: inverse_graph (graph f) = graph (inverse_fun f).
by rewrite/inverse_fun; aw.
split.
apply injective_pr_bis=>//; move=> x x' y.
rewrite /related -inverse_graph_pair geq => r1.
rewrite -inverse_graph_pair geq => r2.
by move: fif => [_ [ fg _ ]]; apply (fgraph_pr fg r1 r2).
apply surjective_pr4=> //; rewrite - domain_inverse; fprops.
by rewrite geq /inverse_fun; aw.
Qed.
We define here an inverse of (f:a->b)
Lemma bijective_inv_aux: forall (a b:Set) (f:a->b),
bijectiveC f -> is_function (inverse_fun (acreate f)).
Proof.
by move=> a b f bf; apply bijective_inv_function; apply acreate_bijective.
Qed.
Lemma bijective_source_aux: forall (a b:Set) (f:a->b),
source (inverse_fun (acreate f)) = b.
Proof. rewrite /inverse_fun /acreate=> a b f; aw. Qed.
Lemma bijective_target_aux: forall (a b:Set) (f:a->b),
target (inverse_fun (acreate f)) = a.
Proof. rewrite /inverse_fun /acreate=> a b f; aw. Qed.
Definition inverseC (a b:Set) (f:a->b)(H:bijectiveC f): b->a :=
bcreate (bijective_inv_aux H) (bijective_source_aux f)
(bijective_target_aux f).
Lemma inverseC_pra: forall (a b:Set) (f:a->b)(H:bijectiveC f) (x:a),
(inverseC H) (f x) = x.
Proof.
rewrite /inverseC=> a b f bf x; apply R_inj.
rewrite prop_bcreate2 - (acreate_W f).
have ya: (inc (Ro x) a) by apply R_inc.
set g := (_ f).
have bg: (bijection g) by apply acreate_bijective.
have fg:(is_function g) by fct_tac.
apply W_pr; first by apply bijective_inv_function.
by rewrite /inverse_fun; aw; graph_tac; rewrite /g; aw.
Qed.
Lemma inverseC_prb: forall (a b:Set) (f:a->b)(H:bijectiveC f) (x:b),
f ((inverseC H) x) = x.
Proof.
move=> a b f bf x; have sf: (surjectiveC f) by move: bf=> [_].
by case (sf x); move=> y <-;rewrite (inverseC_pra bf).
Qed.
Lemma inverseC_prc: forall (a b:Set) (f:a-> b) (H:bijectiveC f),
inverse_fun(acreate f) = acreate(inverseC H).
Proof.
move=> a b f bf; move: (acreate_bijective bf) => ab.
apply function_exten.
- by apply bijective_inv_function.
- by fprops.
- by rewrite/acreate; aw.
- by rewrite/acreate; aw.
- by move => x; rewrite /inverseC bcreate_inv2.
Qed.
Lemma bij_left_inverseC: forall (a b:Set) (f:a->b)(H:bijectiveC f) ,
(inverseC H) \o f =1 @id a.
Proof.
by move=> a b f bf w; rewrite composeC_ev inverseC_pra.
Qed.
Lemma bij_right_inverseC: forall (a b:Set) (f:a->b)(H:bijectiveC f) ,
f \o (inverseC H) =1 @id b.
Proof.
by move=> a b f bf w; rewrite composeC_ev inverseC_prb.
Qed.
Lemma bijective_double_inverseC: forall (a b:Set) (f:a->b) g g',
g \o f =1 @id a -> f \o g' =1 @id b ->
bijectiveC f.
Proof.
move=> a b f g g' c1 c2; split.
move=> x x' feq; move: (f_equal g feq); rewrite -!(composeC_ev g f) !c1 //.
move=> x; exists (g' x); rewrite -!(composeC_ev f g') c2 //.
Qed.
Lemma bijective_double_inverseC1: forall (a b:Set) (f:a->b) g g'
(Ha: g \o f =1 @id a)(Hb: f \o g' =1 @id b),
g =1 inverseC (bijective_double_inverseC Ha Hb)
& g' =1 inverseC (bijective_double_inverseC Ha Hb).
Proof.
move=>a b f g g' Ha Hb.
have sg: (g' =1 g).
by move=> x; rewrite -{1} (Ha (g' x)) -{2} (Hb x) !composeC_ev.
set h := inverseC _.
have gh: (g' =1 h).
move => x; have e1: (f (g' x) = x) by apply (Hb x).
by rewrite /h -{2} e1 inverseC_pra.
split =>//; apply ftrans with g' => //.
Qed.
Lemma bijective_inverseC: forall (a b:Set) (f:a->b)(H:bijectiveC f) ,
bijectiveC (inverseC H).
Proof.
move=> a b f H; split.
by move=> x y sv; rewrite -(inverseC_prb H x) - (inverseC_prb H y) sv.
by move=> u; exists (f u); rewrite inverseC_pra.
Qed.
Lemma inverse_fun_involutiveC:forall (a b:Set) (f:a->b) (H: bijectiveC f),
f =1 inverseC(bijective_inverseC H).
Proof.
move=> a b f H x.
move: (bijective_inverseC H) => [i s]; apply i.
by rewrite inverseC_pra inverseC_prb.
Qed.
bijectiveC f -> is_function (inverse_fun (acreate f)).
Proof.
by move=> a b f bf; apply bijective_inv_function; apply acreate_bijective.
Qed.
Lemma bijective_source_aux: forall (a b:Set) (f:a->b),
source (inverse_fun (acreate f)) = b.
Proof. rewrite /inverse_fun /acreate=> a b f; aw. Qed.
Lemma bijective_target_aux: forall (a b:Set) (f:a->b),
target (inverse_fun (acreate f)) = a.
Proof. rewrite /inverse_fun /acreate=> a b f; aw. Qed.
Definition inverseC (a b:Set) (f:a->b)(H:bijectiveC f): b->a :=
bcreate (bijective_inv_aux H) (bijective_source_aux f)
(bijective_target_aux f).
Lemma inverseC_pra: forall (a b:Set) (f:a->b)(H:bijectiveC f) (x:a),
(inverseC H) (f x) = x.
Proof.
rewrite /inverseC=> a b f bf x; apply R_inj.
rewrite prop_bcreate2 - (acreate_W f).
have ya: (inc (Ro x) a) by apply R_inc.
set g := (_ f).
have bg: (bijection g) by apply acreate_bijective.
have fg:(is_function g) by fct_tac.
apply W_pr; first by apply bijective_inv_function.
by rewrite /inverse_fun; aw; graph_tac; rewrite /g; aw.
Qed.
Lemma inverseC_prb: forall (a b:Set) (f:a->b)(H:bijectiveC f) (x:b),
f ((inverseC H) x) = x.
Proof.
move=> a b f bf x; have sf: (surjectiveC f) by move: bf=> [_].
by case (sf x); move=> y <-;rewrite (inverseC_pra bf).
Qed.
Lemma inverseC_prc: forall (a b:Set) (f:a-> b) (H:bijectiveC f),
inverse_fun(acreate f) = acreate(inverseC H).
Proof.
move=> a b f bf; move: (acreate_bijective bf) => ab.
apply function_exten.
- by apply bijective_inv_function.
- by fprops.
- by rewrite/acreate; aw.
- by rewrite/acreate; aw.
- by move => x; rewrite /inverseC bcreate_inv2.
Qed.
Lemma bij_left_inverseC: forall (a b:Set) (f:a->b)(H:bijectiveC f) ,
(inverseC H) \o f =1 @id a.
Proof.
by move=> a b f bf w; rewrite composeC_ev inverseC_pra.
Qed.
Lemma bij_right_inverseC: forall (a b:Set) (f:a->b)(H:bijectiveC f) ,
f \o (inverseC H) =1 @id b.
Proof.
by move=> a b f bf w; rewrite composeC_ev inverseC_prb.
Qed.
Lemma bijective_double_inverseC: forall (a b:Set) (f:a->b) g g',
g \o f =1 @id a -> f \o g' =1 @id b ->
bijectiveC f.
Proof.
move=> a b f g g' c1 c2; split.
move=> x x' feq; move: (f_equal g feq); rewrite -!(composeC_ev g f) !c1 //.
move=> x; exists (g' x); rewrite -!(composeC_ev f g') c2 //.
Qed.
Lemma bijective_double_inverseC1: forall (a b:Set) (f:a->b) g g'
(Ha: g \o f =1 @id a)(Hb: f \o g' =1 @id b),
g =1 inverseC (bijective_double_inverseC Ha Hb)
& g' =1 inverseC (bijective_double_inverseC Ha Hb).
Proof.
move=>a b f g g' Ha Hb.
have sg: (g' =1 g).
by move=> x; rewrite -{1} (Ha (g' x)) -{2} (Hb x) !composeC_ev.
set h := inverseC _.
have gh: (g' =1 h).
move => x; have e1: (f (g' x) = x) by apply (Hb x).
by rewrite /h -{2} e1 inverseC_pra.
split =>//; apply ftrans with g' => //.
Qed.
Lemma bijective_inverseC: forall (a b:Set) (f:a->b)(H:bijectiveC f) ,
bijectiveC (inverseC H).
Proof.
move=> a b f H; split.
by move=> x y sv; rewrite -(inverseC_prb H x) - (inverseC_prb H y) sv.
by move=> u; exists (f u); rewrite inverseC_pra.
Qed.
Lemma inverse_fun_involutiveC:forall (a b:Set) (f:a->b) (H: bijectiveC f),
f =1 inverseC(bijective_inverseC H).
Proof.
move=> a b f H x.
move: (bijective_inverseC H) => [i s]; apply i.
by rewrite inverseC_pra inverseC_prb.
Qed.
Properties of the inverse of a bijection
Lemma inverse_bij_is_bij:forall f,
bijection f -> bijection (inverse_fun f).
Proof.
move=> f bf.
have ff:is_function f by fct_tac.
move: (bijective_inv_function bf)=> bif.
apply inv_function_bijective=> //; rewrite inverse_fun_involutive//; fct_tac.
Qed.
Lemma composable_f_inv:forall f,
bijection f -> f \coP (inverse_fun f).
Proof.
move=> f bf.
have fif: (is_function (inverse_fun f)) by apply bijective_inv_function.
red; ee; [fct_tac | aw].
Qed.
Lemma composable_inv_f: forall f,
bijection f -> (inverse_fun f) \coP f.
Proof.
move=> f bf;
have fif: is_function (inverse_fun f) by apply bijective_inv_function.
red; ee; [fct_tac | aw].
Qed.
Lemma acreate_exten: forall (a b: Set) (f g: a-> b),
f =1 g -> acreate f = acreate g.
Proof.
move=> a b f g h; apply function_exten; fprops; aw.
by move=> x [z za]; rewrite -za ! acreate_W h.
Qed.
Lemma bij_right_inverse:forall f,
bijection f -> f \co (inverse_fun f) = identity (target f).
Proof.
move=> f bf;
move: (refl_equal (source f)) (refl_equal (target f))=> ss tt.
rewrite -(identity_prop (target f)).
move: (bij_is_function bf)=>ff.
rewrite - (bcreate_inv2 ff ss tt) acreate_target.
rewrite (inverseC_prc (bcreate_bijective ff ss tt bf)).
rewrite compose_acreate.
apply acreate_exten; move=> t.
by rewrite (bij_right_inverseC (bcreate_bijective ff ss tt bf)) //.
Qed.
Lemma bij_left_inverse:forall f,
bijection f -> (inverse_fun f) \co f = identity (source f).
Proof.
move=> f bf;
move: (refl_equal (source f)) (refl_equal (target f))=> ss tt.
rewrite -(identity_prop (source f)).
move: (bij_is_function bf)=>ff.
rewrite - (bcreate_inv2 ff ss tt).
rewrite (inverseC_prc (bcreate_bijective ff ss tt bf)).
rewrite acreate_source compose_acreate ;apply acreate_exten.
by move=> t; rewrite bij_left_inverseC.
Qed.
Lemma W_inverse: forall f x y,
bijection f -> inc x (target f) ->
(y = W x (inverse_fun f)) -> (x = W y f).
Proof.
move=>f x y bf xt ->.
transitivity (W x (identity (target f))); first by srw.
by rewrite -(bij_right_inverse bf); aw; apply composable_f_inv.
Qed.
Lemma W_inverse2: forall f x y,
bijection f -> inc y (source f) ->
(x = W y f) -> (y = W x (inverse_fun f)).
Proof.
move=>f x y bf ys ->.
transitivity (W y (identity (source f))); first by srw.
by rewrite -(bij_left_inverse bf); aw; apply composable_inv_f.
Qed.
Lemma W_inverse3: forall f x,
bijection f -> inc x (target f) -> inc (W x (inverse_fun f)) (source f).
Proof.
move=> f x bf xt.
have: source f= (target (inverse_fun f)) by aw.
move=>->; apply inc_W_target; aw; apply (inverse_bij_is_bij bf).
Qed.
Properties of direct and inverse images
Lemma sub_inv_im_source:forall f y,
is_function f -> sub y (target f) ->
sub (inv_image_by_graph (graph f) y) (source f).
Proof. by move=> f y ff yt t; aw; move => [u [uy Jg]]; graph_tac. Qed.
Lemma direct_inv_im: forall f y,
is_function f -> sub y (target f) ->
sub (image_by_fun f (image_by_fun (inverse_fun f) y)) y.
Proof.
move=> f y ff yt x;
rewrite -inv_image_by_fun_pr; aw; last by apply sub_inv_im_source.
rewrite /inv_image_by_fun;move => [u]; aw; move=> [[v [vy Jg]]] <-.
by rewrite (W_pr ff Jg).
Qed.
Lemma direct_inv_im_surjective: forall f y,
surjection f -> sub y (target f) ->
(image_by_fun f (image_by_fun (inverse_fun f) y)) = y.
Proof.
move=> f y sf yt.
have ff: is_function f by fct_tac.
apply extensionality; first by apply direct_inv_im.
move=> x xs; rewrite -inv_image_by_fun_pr.
aw; last by apply sub_inv_im_source.
move: (surjective_pr2 sf (yt _ xs)) => [u [us Jg]].
exists u; split=>//.
by rewrite/inv_image_by_fun; aw; ex_tac; rewrite - Jg; graph_tac.
Qed.
Lemma inverse_direct_image:forall f x,
is_function f -> sub x (source f) ->
sub x (image_by_fun (inverse_fun f) (image_by_fun f x)).
Proof.
move=> f x ff sxf t tx.
have Jg: (inc (J t (W t f))(graph f)) by graph_tac.
rewrite /image_by_fun /inverse_fun; aw.
exists (W t f); aw; ee; ex_tac.
Qed.
Lemma inverse_direct_image_inj:forall f x,
injection f -> sub x (source f) ->
x = (image_by_fun (inverse_fun f) (image_by_fun f x)).
Proof.
move=> f x [ff fi] xsf.
apply extensionality; first by apply inverse_direct_image=>//; fct_tac.
move=> y; rewrite -inv_image_by_fun_pr /inv_image_by_fun.
aw; move=> [u [ui Jg]]. move: ui; aw. move=> [v [vx Wv]].
rewrite - (W_pr ff Jg) in Wv.
by rewrite - (fi _ _ (xsf _ vx) (inc_pr1graph_source ff Jg) Wv).
Qed.
is_function f -> sub y (target f) ->
sub (inv_image_by_graph (graph f) y) (source f).
Proof. by move=> f y ff yt t; aw; move => [u [uy Jg]]; graph_tac. Qed.
Lemma direct_inv_im: forall f y,
is_function f -> sub y (target f) ->
sub (image_by_fun f (image_by_fun (inverse_fun f) y)) y.
Proof.
move=> f y ff yt x;
rewrite -inv_image_by_fun_pr; aw; last by apply sub_inv_im_source.
rewrite /inv_image_by_fun;move => [u]; aw; move=> [[v [vy Jg]]] <-.
by rewrite (W_pr ff Jg).
Qed.
Lemma direct_inv_im_surjective: forall f y,
surjection f -> sub y (target f) ->
(image_by_fun f (image_by_fun (inverse_fun f) y)) = y.
Proof.
move=> f y sf yt.
have ff: is_function f by fct_tac.
apply extensionality; first by apply direct_inv_im.
move=> x xs; rewrite -inv_image_by_fun_pr.
aw; last by apply sub_inv_im_source.
move: (surjective_pr2 sf (yt _ xs)) => [u [us Jg]].
exists u; split=>//.
by rewrite/inv_image_by_fun; aw; ex_tac; rewrite - Jg; graph_tac.
Qed.
Lemma inverse_direct_image:forall f x,
is_function f -> sub x (source f) ->
sub x (image_by_fun (inverse_fun f) (image_by_fun f x)).
Proof.
move=> f x ff sxf t tx.
have Jg: (inc (J t (W t f))(graph f)) by graph_tac.
rewrite /image_by_fun /inverse_fun; aw.
exists (W t f); aw; ee; ex_tac.
Qed.
Lemma inverse_direct_image_inj:forall f x,
injection f -> sub x (source f) ->
x = (image_by_fun (inverse_fun f) (image_by_fun f x)).
Proof.
move=> f x [ff fi] xsf.
apply extensionality; first by apply inverse_direct_image=>//; fct_tac.
move=> y; rewrite -inv_image_by_fun_pr /inv_image_by_fun.
aw; move=> [u [ui Jg]]. move: ui; aw. move=> [v [vx Wv]].
rewrite - (W_pr ff Jg) in Wv.
by rewrite - (fi _ _ (xsf _ vx) (inc_pr1graph_source ff Jg) Wv).
Qed.
Definition of left and right inverse
Definition is_left_inverse r f :=
r \coP f & r \co f = identity (source f).
Definition is_right_inverse s f :=
f \coP s & f \co s = identity (target f).
Typechecking says that r:b->a and s:b->a
Definition is_left_inverseC (a b:Set) r (f:a->b) := r \o f =1 @id a.
Definition is_right_inverseC (a b:Set) s (f:a->b):= f \o s =1 @id b.
Lemma target_left_inverse: forall r f,
is_left_inverse r f -> target r = source f.
Proof.
by move=> r f [crf c]; move: (f_equal target c); aw.
Qed.
Lemma source_right_inverse: forall s f,
is_right_inverse s f -> source s = target f.
Proof.
by move=> s f [csf c]; move: (f_equal source c); aw.
Qed.
Lemma W_right_inverse: forall s f x,
is_right_inverse s f -> inc x (target f) -> W (W x s) f = x.
Proof.
move=> s f x rsf xtf; move: (xtf);rewrite - (source_right_inverse rsf).
move: rsf=> [csf c] xs; rewrite- compose_W // c; srw.
Qed.
Lemma W_left_inverse: forall r f x,
is_left_inverse r f -> inc x (source f) -> W (W x f) r = x.
Proof.
move=> r f x [ltf c] xsf; rewrite- compose_W // c; srw.
Qed.
Lemma w_right_inverse: forall (a b:Set) s (f:a->b) (x:b),
is_right_inverseC s f -> f (s x) = x.
Proof. by move=> a b s f x e; move: (e x); rewrite composeC_ev. Qed.
Lemma w_left_inverse: forall (a b:Set) r (f:a->b) (x:a),
is_left_inverseC r f -> r (f x) = x.
Proof. by move=> a b s f x e; move: (e x); rewrite composeC_ev. Qed.
Definition is_right_inverseC (a b:Set) s (f:a->b):= f \o s =1 @id b.
Lemma target_left_inverse: forall r f,
is_left_inverse r f -> target r = source f.
Proof.
by move=> r f [crf c]; move: (f_equal target c); aw.
Qed.
Lemma source_right_inverse: forall s f,
is_right_inverse s f -> source s = target f.
Proof.
by move=> s f [csf c]; move: (f_equal source c); aw.
Qed.
Lemma W_right_inverse: forall s f x,
is_right_inverse s f -> inc x (target f) -> W (W x s) f = x.
Proof.
move=> s f x rsf xtf; move: (xtf);rewrite - (source_right_inverse rsf).
move: rsf=> [csf c] xs; rewrite- compose_W // c; srw.
Qed.
Lemma W_left_inverse: forall r f x,
is_left_inverse r f -> inc x (source f) -> W (W x f) r = x.
Proof.
move=> r f x [ltf c] xsf; rewrite- compose_W // c; srw.
Qed.
Lemma w_right_inverse: forall (a b:Set) s (f:a->b) (x:b),
is_right_inverseC s f -> f (s x) = x.
Proof. by move=> a b s f x e; move: (e x); rewrite composeC_ev. Qed.
Lemma w_left_inverse: forall (a b:Set) r (f:a->b) (x:a),
is_left_inverseC r f -> r (f x) = x.
Proof. by move=> a b s f x e; move: (e x); rewrite composeC_ev. Qed.
Proposition 8 concerns the next 4 theorems; it is the link between injectivity, surjectivity and existence of left and right inverse
Lemma inj_if_exists_left_invC: forall (a b:Set) (f:a-> b),
(exists r, is_left_inverseC r f) -> injectiveC f.
Proof.
move=> a b f [r ilr] x x'.
by move /(congr1 r); move: (ilr x) (ilr x'); simpl; move => -> ->.
Qed.
Lemma surj_if_exists_right_invC: forall (a b:Set) (f:a->b),
(exists s, is_right_inverseC s f) -> surjectiveC f.
Proof.
by move=> a b f [s rsf] u; exists (s u); rewrite (w_right_inverse u rsf).
Qed.
Theorem inj_if_exists_left_inv: forall f,
(exists r, is_left_inverse r f) -> injection f.
Proof.
move=> f [r lrf]; split; first by move: lrf => [ cp _ ]; fct_tac.
move=> x y xs ys sv.
by rewrite - (W_left_inverse lrf xs) - (W_left_inverse lrf ys) sv.
Qed.
Theorem surj_if_exists_right_inv: forall f,
(exists s, is_right_inverse s f) -> surjection f.
Proof.
move=> f [s rsf]; move: (rsf) => [cp _]; move: (cp) =>[ff [fs ss]].
apply surjective_pr6 => //; move=> y yt; exists (W y s).
rewrite W_right_inverse //; split=>//.
rewrite -(source_right_inverse rsf) in yt; rewrite ss; fprops.
Qed.
Left inverse for an injective function (f: a->b)
Definition left_inverseC (a b:Set) (f: a->b)(H:nonemptyT a)
(v:b) := (chooseT (fun u:a => (~ (exists x:a, f x = v)) \/ (f u = v)) H).
Lemma left_inverseC_pr:forall (a b:Set) (f: a->b) (H:nonemptyT a) (u:a),
f(left_inverseC f H (f u)) = f u.
Proof.
rewrite /left_inverseC=> a b f nea u.
set p:= fun u:a => _.
have: (p (chooseT p nea)) by apply chooseT_pr; exists u; rewrite /p; auto.
case=>//; by case; exists u.
Qed.
Lemma left_inverse_comp_id: forall (a b:Set) (f:a->b) (H:nonemptyT a),
injectiveC f -> (left_inverseC f H) \o f =1 @id a.
Proof.
move=> a b f nea fi x; apply fi; rewrite composeC_ev;apply left_inverseC_pr.
Qed.
Lemma exists_left_inv_from_injC: forall (a b:Set) (f:a->b), nonemptyT a ->
injectiveC f -> exists r, is_left_inverseC r f.
Proof.
move=> a b f nea fi.
exists (left_inverseC f nea); by apply left_inverse_comp_id.
Qed.
(v:b) := (chooseT (fun u:a => (~ (exists x:a, f x = v)) \/ (f u = v)) H).
Lemma left_inverseC_pr:forall (a b:Set) (f: a->b) (H:nonemptyT a) (u:a),
f(left_inverseC f H (f u)) = f u.
Proof.
rewrite /left_inverseC=> a b f nea u.
set p:= fun u:a => _.
have: (p (chooseT p nea)) by apply chooseT_pr; exists u; rewrite /p; auto.
case=>//; by case; exists u.
Qed.
Lemma left_inverse_comp_id: forall (a b:Set) (f:a->b) (H:nonemptyT a),
injectiveC f -> (left_inverseC f H) \o f =1 @id a.
Proof.
move=> a b f nea fi x; apply fi; rewrite composeC_ev;apply left_inverseC_pr.
Qed.
Lemma exists_left_inv_from_injC: forall (a b:Set) (f:a->b), nonemptyT a ->
injectiveC f -> exists r, is_left_inverseC r f.
Proof.
move=> a b f nea fi.
exists (left_inverseC f nea); by apply left_inverse_comp_id.
Qed.
Right inverse for a surjective function (f: a->b)
Definition right_inverseC (a b:Set) (f: a->b) (H:surjectiveC f) (v:b) :=
(chooseT (fun k:a => f k = v)
match H v with | ex_intro x _ => nonemptyT_intro x end).
Lemma right_inverse_pr: forall (a b:Set) (f: a->b) (H:surjectiveC f) (x:b),
f(right_inverseC H x) = x.
Proof. by rewrite /right_inverseC=> a b f H x; apply chooseT_pr. Qed.
Lemma right_inverse_comp_id: forall (a b:Set) (f:a-> b) (H:surjectiveC f),
f \o (right_inverseC H) =1 @id b.
Proof.
move=> a b f h x; rewrite composeC_ev;apply right_inverse_pr.
Qed.
Lemma exists_right_inv_from_surjC: forall (a b:Set)(f:a-> b) (H:surjectiveC f),
exists s, is_right_inverseC s f.
Proof.
move=> a b f sf; exists (right_inverseC sf).
apply right_inverse_comp_id.
Qed.
Existence of left and right inverse for Bourbaki functions
Theorem exists_left_inv_from_inj: forall f,
injection f -> nonempty (source f) -> exists r, is_left_inverse r f.
Proof.
move=> f fi nesf; move: (inj_is_function fi)=> ff.
move: (bcreate1_injective (H:=ff) fi)=>ib.
rewrite -nonemptyT_not_empty0 in nesf.
case (exists_left_inv_from_injC nesf ib) => x px.
move: (compose_acreate x (bcreate1 ff));rewrite bcreate_inv1 => aux.
exists (acreate x).
split; first by split; fprops; aw.
rewrite aux;apply function_exten; fprops; aw.
move=> u usf; rewrite identity_W //.
by move: usf => [v vs];rewrite -vs acreate_W px.
Qed.
Theorem exists_right_inv_from_surj: forall f,
surjection f -> exists s, is_right_inverse s f.
Proof.
move=> f sf.
move: (surj_is_function sf)=> ff; move: (bcreate1_surjective ff sf)=> bs.
move: (exists_right_inv_from_surjC bs)=> [s ris].
move:(compose_acreate (bcreate1 ff) s); rewrite bcreate_inv1 => aux.
exists (acreate s); split; first by red; ee; aw;fprops.
rewrite aux;apply function_exten; fprops; aw.
move=> u usf; rewrite identity_W //.
by move: usf => [v vs];rewrite -vs acreate_W ris.
Qed.
If compositions in both order are the identity, then the functions are bijections
Lemma bijective_from_compose: forall g f,
g \coP f -> f \coP g -> g \co f = identity (source f)
-> f \co g = identity (source g)
-> (bijection f & bijection g & g = inverse_fun f).
Proof.
move=> g f cgf cfg cgfi cfgi.
move: (cfg) (cgf)=> [ff [fg seq]] [_ [_ teq]].
have injf: injection f by apply inj_if_exists_left_inv; exists g.
have injg: injection g by apply inj_if_exists_left_inv; exists f.
have bf: (bijection f).
by split =>//; apply surj_if_exists_right_inv; exists g; red; rewrite -teq.
split=>//; split.
by split=>//; apply surj_if_exists_right_inv; exists f; red; rewrite -seq.
symmetry.
move: (bijective_inv_function bf)=>fif.
apply function_exten=>//; aw; first by symmetry.
move=> x xs; apply W_pr=>//; rewrite/inverse_fun; aw;rewrite -teq in xs.
have aux : (x= (W (W x g) f)).
by rewrite -compose_W=>//;rewrite cfgi identity_W =>//.
by rewrite {2} aux; graph_tac; rewrite seq; apply inc_W_target.
Qed.
More links between left inverse and right inverse
Lemma right_inverse_from_leftC: forall (a b:Set) (r:b->a)(f:a->b),
is_left_inverseC r f -> is_right_inverseC f r.
Proof. trivial. Qed.
Lemma left_inverse_from_rightC: forall (a b:Set) (s:b->a)(f:a->b),
is_right_inverseC s f -> is_left_inverseC f s.
Proof. trivial. Qed.
Lemma left_inverse_surjectiveC: forall (a b:Set) (r:b->a)(f:a->b),
is_left_inverseC r f -> surjectiveC r.
Proof. by move=> a b r f h; apply surj_if_exists_right_invC; exists f.
Qed.
Lemma right_inverse_injectiveC: forall (a b:Set) (s:b->a)(f:a->b),
is_right_inverseC s f -> injectiveC s.
Proof. move=> a b s f h; apply inj_if_exists_left_invC; by exists f.
Qed.
Lemma section_uniqueC: forall (a b:Set) (f:a->b)(s:b->a)(s':b->a),
is_right_inverseC s f -> is_right_inverseC s' f ->
(forall x:a, (exists u:b, x = s u) = (exists u':b, x = s' u')) ->
s =1 s'.
Proof.
move=> a b f s s' r1 r2 sp x.
have [u' eql]: (exists u' : b, s x = s' u') by rewrite- (sp (s x)); exists x.
move: (f_equal f eql); rewrite (w_right_inverse x r1) (w_right_inverse u' r2).
by rewrite eql; move=>->.
Qed.
Lemma right_inverse_from_left: forall r f,
is_left_inverse r f -> is_right_inverse f r.
Proof.
move=> r f lrf. move: (target_left_inverse lrf) => Ha.
by move: lrf=> [c e]; split=>//;rewrite Ha.
Qed.
Lemma left_inverse_from_right: forall s f,
is_right_inverse s f -> is_left_inverse f s.
Proof.
move=> s f rsf. move: (source_right_inverse rsf) => Ha.
by move: rsf=> [c e]; split=>//;rewrite Ha.
Qed.
Lemma left_inverse_surjective: forall f r,
is_left_inverse r f -> surjection r.
Proof.
move=> f r lrf; apply surj_if_exists_right_inv.
by exists f; apply right_inverse_from_left.
Qed.
Lemma right_inverse_injective: forall f s,
is_right_inverse s f -> injection s.
Proof.
move=> f r lrf; apply inj_if_exists_left_inv.
by exists f; apply left_inverse_from_right.
Qed.
Lemma section_unique: forall f s s',
is_right_inverse s f -> is_right_inverse s' f ->
range (graph s) = range (graph s') -> s = s'.
Proof.
move=> f s s' rsf rs'f rg.
have fs: is_function s by move: rsf=> [c _]; fct_tac.
have fs': is_function s' by move: rs'f=> [c _]; fct_tac.
move: (source_right_inverse rsf)=> ss.
move: (source_right_inverse rs'f)=> ss'.
apply function_exten =>//.
by rewrite (source_right_inverse rsf).
by move: rs'f=> [[_ [_ c2]] _]; move: rsf=> [[_ [_ c3]] _]; rewrite -c3 -c2.
move=> x xs.
have w: (inc (W x s) (range (graph s))) by rewrite range_inc_rw=>//; exists x.
rewrite rg in w.
move: w; rewrite range_inc_rw=>//; move=> [y [ys ww]]; rewrite ww.
rewrite ss' in ys; move: (W_right_inverse rs'f ys).
rewrite ss in xs; move: (W_right_inverse rsf xs).
by rewrite ww; move => -> ->.
Qed.
is_left_inverseC r f -> is_right_inverseC f r.
Proof. trivial. Qed.
Lemma left_inverse_from_rightC: forall (a b:Set) (s:b->a)(f:a->b),
is_right_inverseC s f -> is_left_inverseC f s.
Proof. trivial. Qed.
Lemma left_inverse_surjectiveC: forall (a b:Set) (r:b->a)(f:a->b),
is_left_inverseC r f -> surjectiveC r.
Proof. by move=> a b r f h; apply surj_if_exists_right_invC; exists f.
Qed.
Lemma right_inverse_injectiveC: forall (a b:Set) (s:b->a)(f:a->b),
is_right_inverseC s f -> injectiveC s.
Proof. move=> a b s f h; apply inj_if_exists_left_invC; by exists f.
Qed.
Lemma section_uniqueC: forall (a b:Set) (f:a->b)(s:b->a)(s':b->a),
is_right_inverseC s f -> is_right_inverseC s' f ->
(forall x:a, (exists u:b, x = s u) = (exists u':b, x = s' u')) ->
s =1 s'.
Proof.
move=> a b f s s' r1 r2 sp x.
have [u' eql]: (exists u' : b, s x = s' u') by rewrite- (sp (s x)); exists x.
move: (f_equal f eql); rewrite (w_right_inverse x r1) (w_right_inverse u' r2).
by rewrite eql; move=>->.
Qed.
Lemma right_inverse_from_left: forall r f,
is_left_inverse r f -> is_right_inverse f r.
Proof.
move=> r f lrf. move: (target_left_inverse lrf) => Ha.
by move: lrf=> [c e]; split=>//;rewrite Ha.
Qed.
Lemma left_inverse_from_right: forall s f,
is_right_inverse s f -> is_left_inverse f s.
Proof.
move=> s f rsf. move: (source_right_inverse rsf) => Ha.
by move: rsf=> [c e]; split=>//;rewrite Ha.
Qed.
Lemma left_inverse_surjective: forall f r,
is_left_inverse r f -> surjection r.
Proof.
move=> f r lrf; apply surj_if_exists_right_inv.
by exists f; apply right_inverse_from_left.
Qed.
Lemma right_inverse_injective: forall f s,
is_right_inverse s f -> injection s.
Proof.
move=> f r lrf; apply inj_if_exists_left_inv.
by exists f; apply left_inverse_from_right.
Qed.
Lemma section_unique: forall f s s',
is_right_inverse s f -> is_right_inverse s' f ->
range (graph s) = range (graph s') -> s = s'.
Proof.
move=> f s s' rsf rs'f rg.
have fs: is_function s by move: rsf=> [c _]; fct_tac.
have fs': is_function s' by move: rs'f=> [c _]; fct_tac.
move: (source_right_inverse rsf)=> ss.
move: (source_right_inverse rs'f)=> ss'.
apply function_exten =>//.
by rewrite (source_right_inverse rsf).
by move: rs'f=> [[_ [_ c2]] _]; move: rsf=> [[_ [_ c3]] _]; rewrite -c3 -c2.
move=> x xs.
have w: (inc (W x s) (range (graph s))) by rewrite range_inc_rw=>//; exists x.
rewrite rg in w.
move: w; rewrite range_inc_rw=>//; move=> [y [ys ww]]; rewrite ww.
rewrite ss' in ys; move: (W_right_inverse rs'f ys).
rewrite ss in xs; move: (W_right_inverse rsf xs).
by rewrite ww; move => -> ->.
Qed.
Theorem one is next 14 lemmas. It studies left and right invertibility
of one of f g and the composition of f and g, given properties of the other objects.
Lemma composeC_inj: forall (a b c:Set) (f:a->b)(f':b->c),
injectiveC f-> injectiveC f' -> injectiveC (f' \o f).
Proof. by move=> a b c f f' fi fi' x y p; apply fi; apply fi'.
Qed.
Lemma composeC_surj: forall (a b c:Set) (f:a->b)(f':b->c),
surjectiveC f-> surjectiveC f' -> surjectiveC (f' \o f).
Proof.
move => a b c f f' sf sf' y.
move: (sf' y) => [w] <-; move: (sf w) => [z] <-.
by exists z.
Qed.
Lemma composeC_bij: forall (a b c:Set) (f:a->b)(f':b->c),
bijectiveC f-> bijectiveC f' -> bijectiveC (f' \o f).
Proof.
move=> a bb c f f' [fi fs] [fi' fs'].
by split; [apply composeC_inj| apply composeC_surj ].
Qed.
Lemma left_inverse_composeC: forall (a b c:Set)
(f:a->b) (f':b->c)(r:b->a)(r':c->b),
is_left_inverseC r' f' -> is_left_inverseC r f ->
is_left_inverseC (r \o r') (f' \o f).
Proof.
move=> a b c f f' r r' le' le x;rewrite !composeC_ev.
by rewrite (w_left_inverse (f x) le') (w_left_inverse x le).
Qed.
Lemma right_inverse_composeC:forall (a b c:Set)
(f:a->b) (f':b->c)(s:b->a)(s':c->b),
is_right_inverseC s' f' -> is_right_inverseC s f ->
is_right_inverseC (s \o s') (f' \o f).
Proof.
move=> a b c f f' s s' ri' ri x ;rewrite !composeC_ev.
by rewrite (w_right_inverse (s' x) ri) (w_right_inverse x ri').
Qed.
Lemma inj_right_composeC: forall (a b c:Set) (f:a->b) (f':b->c),
injectiveC (f' \o f) -> injectiveC f.
Proof. by move=> a b c f f' ci x y sv; apply ci; rewrite !composeC_ev sv. Qed.
Lemma surj_left_composeC: forall (a b c:Set) (f:a->b) (f':b->c),
surjectiveC (f' \o f) -> surjectiveC f'.
Proof.
by move=> a b c f f' sc x; move: (sc x)=> [y] <-; exists (f y). Qed.
Lemma surj_left_compose2C: forall (a b c:Set) (f:a->b) (f':b->c),
surjectiveC (f' \o f) -> injectiveC f' -> surjectiveC f.
Proof.
move => a b c f f' sc if' x.
by move: (sc (f' x)) => [y] => sv; exists y; apply if'.
Qed.
Lemma inj_left_compose2C: forall (a b c:Set) (f:a->b) (f':b->c),
injectiveC (f' \o f) -> surjectiveC f -> injectiveC f'.
Proof.
move=> a b c f f' ic sf x x' sv.
move: (sf x) => [y yv]; move: (sf x') => [y' y'v].
have: (y = y') by apply ic; rewrite !composeC_ev yv y'v sv.
by rewrite -yv -y'v; move=>->.
Qed.
Lemma left_inv_compose_rfC: forall (a b c:Set) (f:a->b) (f':b->c)(r'': c->a),
is_left_inverseC r'' (f' \o f) ->
is_left_inverseC (r'' \o f') f.
Proof.
by move=> a b c f f' r'' li x; apply (w_left_inverse x li).
Qed.
Lemma right_inv_compose_rfC : forall (a b c:Set) (f:a->b) (f':b->c)(s'': c->a),
is_right_inverseC s'' (f' \o f) ->
is_right_inverseC (f \o s'') f'.
Proof.
move=> a b c f f' s'' ri x; by apply (w_right_inverse x ri).
Qed.
Lemma left_inv_compose_rf2C: forall (a b c:Set) (f:a->b) (f':b->c)(r'': c->a),
is_left_inverseC r'' (f' \o f) -> surjectiveC f ->
is_left_inverseC (f \o r'') f'.
Proof.
move=> a b c f f' r'' li s t.
move: (s t) => [v] <-; exact: (f_equal f (li v)).
Qed.
Lemma right_inv_compose_rf2C: forall (a b c:Set) (f:a->b) (f':b->c)(s'': c->a),
is_right_inverseC s'' (f' \o f) -> injectiveC f'->
is_right_inverseC (s'' \o f') f.
Proof.
move=> a b c f f' s'' ri inj.
move=> t; apply inj; exact (ri (f' t)).
Qed.
Theorem compose_injective: forall f f',
injection f-> injection f' -> f' \coP f -> injection (f' \co f).
Proof.
move=> f f' fi fi' c; split; first by fct_tac.
aw=> x y xs ys; aw=>p.
move: fi=> [ _]; apply=>//.
move:c => [_ [ff c]].
by move: fi'=> [ _]; apply=>//; rewrite c; fprops.
Qed.
Theorem compose_surjective: forall f f',
surjection f-> surjection f' -> f' \coP f -> surjection (f' \co f).
Proof.
move=> f f' sf sf' c.
apply surjective_pr6; first by fct_tac.
aw => y yt.
move: (surjective_pr2 sf' yt) => [x [xs]] <-.
have xt: inc x (target f) by move: c => [_ [_ c]]; rewrite -c.
move: (surjective_pr2 sf xt) => [z [zs]] <-.
by ex_tac;aw.
Qed.
Lemma compose_bijective: forall f f',
bijection f-> bijection f' -> f' \coP f -> bijection (f' \co f).
Proof.
move=> f f' [inf sf] [inf' sf'].
by split ; [apply compose_injective | apply compose_surjective].
Qed.
Lemma bij_right_compose: forall f f',
f' \coP f -> bijection (f' \co f) -> bijection f' -> bijection f.
Proof.
move=> f f' c bc bf.
set g:= inverse_fun f'.
have bg: (bijection g) by rewrite /g; apply inverse_bij_is_bij.
have: (bijection (g \co (f' \co f))).
apply compose_bijective=>//.
by split; first (by fct_tac); split; [fct_tac| rewrite /g; aw].
rewrite -compose_assoc =>//; try apply (composable_inv_f bf).
have st: (source f' = target f) by move: c=> [_ [_]].
by rewrite /g bij_left_inverse=>//; rewrite st compose_id_left=>//; fct_tac.
Qed.
Lemma bij_left_compose: forall f f',
f' \coP f -> bijection (f' \co f) -> bijection f -> bijection f'.
Proof.
move=> f f' cff bc bf.
set g := inverse_fun f.
have bg: (bijection g) by apply inverse_bij_is_bij.
have : (bijection ((f' \co f) \co g)).
apply compose_bijective =>//.
by split; [ fct_tac | split ; [ fct_tac | rewrite /g; aw]].
rewrite compose_assoc=>//; try apply (composable_f_inv bf).
have st: (source f' = target f) by move: cff=> [_ [_]].
by rewrite /g bij_right_inverse=>//; rewrite -st compose_id_right=>//; fct_tac.
Qed.
Lemma left_inverse_composable: forall f f' r r', f' \coP f ->
is_left_inverse r' f' -> is_left_inverse r f -> r \coP r'.
Proof.
move=> f f' r r' [_ [_ c]] li1 [[fr [_ r1]] _].
move: (target_left_inverse li1)=> r2.
move: li1=> [[fr' _] _].
by red; ee; rewrite r1 -c r2.
Qed.
Lemma right_inverse_composable: forall f f' s s', f' \coP f ->
is_right_inverse s' f' -> is_right_inverse s f -> s \coP s'.
Proof.
move=> f f' s s' [_ [_ c]] [[_ [fs r1]] _] ri1.
move: (source_right_inverse ri1)=> r2 .
move: ri1=> [[_ [fs' _]] _].
by red; ee; rewrite r2 -c.
Qed.
Theorem left_inverse_compose: forall f f' r r', f' \coP f ->
is_left_inverse r' f' -> is_left_inverse r f ->
is_left_inverse (r \co r') (f' \co f).
Proof.
move=> f f' r r' c1 li1 li2.
move: (left_inverse_composable c1 li1 li2) =>cc.
move: (target_left_inverse li1)=> tr'sr'.
move:li1=> [crf' crfi']; move:li2=> [crf crfi].
have sr'tf' :source r' = target f' by move: crf'=> [_ [_ ]].
split.
by split; [ fct_tac | split; [ fct_tac | aw;rewrite sr'tf']].
have crrf: (r \co r') \coP f'.
by split; [ fct_tac | split; [fct_tac| aw ]].
rewrite- compose_assoc=>//. rewrite (@compose_assoc r r' f')=>//.
have sf'sr: (source f' = source r) by move:cc => [_ [_ rel]]; rewrite -tr'sr'.
by aw; rewrite crfi' sf'sr compose_id_right=>//; fct_tac.
Qed.
Theorem right_inverse_compose: forall f f' s s', f' \coP f ->
is_right_inverse s' f' -> is_right_inverse s f ->
is_right_inverse (s \co s') (f' \co f).
Proof.
move=> f f' s s' cf'f ri1 ri2.
move: (right_inverse_composable cf'f ri1 ri2)=> css'.
move: (source_right_inverse ri2)=> sstf.
move:ri1=> [cfs' cfsi']; move:ri2=> [cfs cfsi].
have sfts : source f = target s by move: cfs=> [_ [_ ]].
split.
by split; [ fct_tac | split; [ fct_tac | aw;rewrite sfts]].
have sf'sr: (target f = target s') by move:css' => [_ [_ rel]]; rewrite -sstf.
have crrf: f \coP (s \co s') .
by split; [ fct_tac | split; [fct_tac| aw ]].
rewrite compose_assoc=>//; rewrite - (@compose_assoc f s s')=>//.
by aw; rewrite cfsi sf'sr compose_id_left=>//; fct_tac.
Qed.
Theorem inj_right_compose: forall f f',
f' \coP f -> injection (f' \co f) -> injection f.
Proof.
move=> f f' cff [fc ic].
split; first by fct_tac.
by move=> x y xs ys eql; awi ic; apply ic=>//; aw; rewrite eql.
Qed.
Theorem surj_left_compose: forall f f',
f' \coP f -> surjection (f' \co f) -> surjection f'.
Proof.
move=> f f' cff sc.
apply surjective_pr6; first by fct_tac.
have: (target f' = target (f' \co f)) by aw.
move=> -> y yt; move: (surjective_pr2 sc yt)=> [x [xs]] <-.
exists (W x f); awi xs; aw.
by move:cff=> [_ [ff ]]=>->; fprops.
Qed.
Theorem surj_left_compose2: forall f f',
f' \coP f-> surjection (f' \co f) -> injection f' -> surjection f.
Proof.
move=> f f' cff sc [_ fi].
have aux: f' \coP f by []; move: aux=> [ff [ff' eq]].
apply surjective_pr6; first by fct_tac.
rewrite - eq=>y ytf.
have ytc: (inc (W y f') (target (f' \co f))) by aw; fprops.
move: (surjective_pr2 sc ytc)=> [x [xs wxt]].
awi xs; awi wxt=>//.
by exists x; intuition; apply fi=>//; rewrite eq; fprops.
Qed.
Theorem inj_left_compose2: forall f f',
f' \coP f -> injection (f' \co f) -> surjection f -> injection f'.
Proof.
move=> f f' cff [_ ic] sf.
split; first by fct_tac.
have sf'tf:(source f' = target f) by move: cff=> [_ [_]].
rewrite sf'tf=> x y xs ys.
move: (surjective_pr2 sf xs)=> [x' [x's] e1].
move: (surjective_pr2 sf ys)=> [y' [y's] e2].
awi ic; move: (ic _ _ x's y's); aw; rewrite -e1 -e2.
by move=> e3 e4; rewrite (e3 e4).
Qed.
Theorem left_inv_compose_rf: forall f f' r'',
f' \coP f -> is_left_inverse r'' (f' \co f) ->
is_left_inverse (r'' \co f') f.
Proof.
move=> f f' r'' cff [[ aa [bb cc]] crffi]; awi crffi; awi cc.
have aux: f' \coP f by []; move: aux=> [ff' [ff seq]].
have crf: r'' \coP f' by hnf; intuition.
split; last rewrite compose_assoc=>//.
by hnf; intuition; aw; fct_tac.
Qed.
Theorem right_inv_compose_rf : forall f f' s'',
f' \coP f -> is_right_inverse s'' (f' \co f) ->
is_right_inverse (f \co s'') f'.
Proof.
move=> f f' s cff [[ fc [fs cc]] cffsi]; awi cffsi; awi cc.
have aux: f' \coP f by []; move: aux=> [ff' [ff seq]].
have cfs: f \coP s by hnf;intuition.
split; last rewrite -compose_assoc=>//.
by hnf; intuition; aw; fct_tac.
Qed.
Theorem left_inv_compose_rf2: forall f f' r'',
f' \coP f -> is_left_inverse r'' (f' \co f) -> surjection f ->
is_left_inverse (f \co r'') f'.
Proof.
move=> f f' r cff lic sf.
have bf: (bijection f).
split=>//.
have: (injection (f' \co f)) by apply inj_if_exists_left_inv; exists r.
by apply (inj_right_compose cff).
move: (target_left_inverse lic); aw=> trsf; move:lic=> [crrf]; aw=> crrfi.
have cfr: f \coP r by hnf; intuition; try fct_tac; symmetry.
have fcfr:(is_function (f \co r)) by fct_tac.
split; first by hnf; intuition; try fct_tac; move: crrf=> [_ [ _]]; aw.
set (invf:= inverse_fun f).
have fi:(is_function invf) by apply bijective_inv_function.
have sfti: (source f = target invf) by rewrite /invf; aw.
have: f' = f' \co (f \co invf).
have tfsii: (target f = source f') by move: cff=> [_ [_]]->.
by rewrite/invf (bij_right_inverse bf) tfsii compose_id_right=>//; fct_tac.
rewrite -compose_assoc =>//; last by apply composable_f_inv.
move=> eq; rewrite {1} eq.
have cffi: (f' \co f) \coP invf by hnf; aw; intuition; fct_tac.
rewrite compose_assoc=>//.
rewrite - (@compose_assoc r (f' \co f) invf) // crrfi sfti.
rewrite compose_id_left // /invf bij_right_inverse //.
by move: cff=> [_ [_ ]]=> ->.
by hnf; intuition; try fct_tac;move: crrf=> [_ [_]]; aw.
Qed.
Theorem right_inv_compose_rf2 : forall f f' s'',
f' \coP f -> is_right_inverse s'' (f' \co f) -> injection f'->
is_right_inverse (s'' \co f') f.
Proof.
move=> f f' s cff risc fi.
have sc: (surjection (f' \co f)) by apply surj_if_exists_right_inv; exists s.
have bf': (bijection f') by split=>//; apply (surj_left_compose cff sc).
move: (source_right_inverse risc); aw=> sstf.
move: risc=> []; aw => cffs cffsi.
have csf: (s \coP f') by red; intuition; fct_tac.
have fcsf: is_function (s \co f') by fct_tac.
have cfc: f \coP (s \co f').
by red; intuition; try fct_tac; move: cffs=> [_ [_]]; aw.
move: (bijective_inv_function bf') => bif.
have sf'tf: source f' = target f by move: cff=> [_ [_]].
set (invf:= inverse_fun f').
have eq: (f = invf \co ( f' \co f)).
move: (composable_inv_f bf')=> cif.
rewrite -compose_assoc // (bij_left_inverse bf') sf'tf compose_id_left //.
by fct_tac.
have cic : (composable invf (f' \co f)).
by hnf; intuition; try fct_tac; rewrite /invf; aw.
have cffsf: (f' \co f) \coP (s \co f').
by hnf; intuition; [ fct_tac | move:cfc=> [_ [_]]; aw].
have ff: is_function f' by fct_tac.
split=>//.
rewrite {1} eq compose_assoc // -(@compose_assoc (f' \co f) s f') //.
by rewrite cffsi compose_id_left // (bij_left_inverse bf') sf'tf.
Qed.
Properties of equipotency
Lemma equipotent_reflexive: forall x, x \Eq x.
Proof.
move=> x; rewrite equipotentC.
exists (@id x); apply identityC_bijective.
Qed.
Lemma equipotent_symmetric: forall a b, a \Eq b -> b \Eq a.
Proof.
move=> a b; rewrite 2! equipotentC.
by move=>[f bf]; exists (inverseC bf); apply bijective_inverseC.
Qed.
Lemma equipotent_transitive: forall a b c,
a \Eq b -> b \Eq c -> a \Eq c.
Proof.
move=> a b c; rewrite 3! equipotentC.
by move=> [f bf] [g bg]; exists (g \o f); apply composeC_bij.
Qed.
Hint Resolve equipotent_reflexive: fprops.
Proof.
move=> x; rewrite equipotentC.
exists (@id x); apply identityC_bijective.
Qed.
Lemma equipotent_symmetric: forall a b, a \Eq b -> b \Eq a.
Proof.
move=> a b; rewrite 2! equipotentC.
by move=>[f bf]; exists (inverseC bf); apply bijective_inverseC.
Qed.
Lemma equipotent_transitive: forall a b c,
a \Eq b -> b \Eq c -> a \Eq c.
Proof.
move=> a b c; rewrite 3! equipotentC.
by move=> [f bf] [g bg]; exists (g \o f); apply composeC_bij.
Qed.
Hint Resolve equipotent_reflexive: fprops.
Proposition 9 is the next 6 lemmas (each in 2 variants). Given f and g,
when does there exists h such that the composition with f (in any order) is g
Lemma exists_left_composableC: forall (a b c:Set) (f:a->b)(g:a->c),
surjectiveC g ->
(exists h, h \o g =1 f) =
(forall (x y:a), g x = g y -> f x = f y).
Proof.
move=> a b c f g sg; apply iff_eq.
by move=> [h hp] x y; move: (hp x) (hp y) => /= <- <- <-.
move: (exists_right_inv_from_surjC sg) => [h hp] hyp.
exists (f \o h).
by move=> t /=; apply hyp; move:(hp (g t)).
Qed.
Theorem exists_left_composable: forall f g,
is_function f -> surjection g -> source f = source g ->
(exists h, h \coP g & h \co g = f) =
(forall x y, inc x (source g) -> inc y (source g) ->
W x g = W y g -> W x f = W y f).
Proof.
move=> f g ff sg sfsg; apply: iff_eq.
by move=> [h [chg]] <- x y xs ys; aw; move=>->.
have fg: is_function g by fct_tac.
move: (bcreate1_surjective fg sg) => scb.
set (bf:=bcreate ff sfsg (refl_equal (target f))).
move=> hyp.
have:(exists h : target g -> (target f), h \o (bcreate1 fg) =1 bf).
rewrite (exists_left_composableC bf scb).
move =>x y sv; apply R_inj; do 2 rewrite prop_bcreate2.
by apply: hyp; try apply: R_inc; rewrite -2! (prop_bcreate1 fg) sv.
move=> [h ch].
exists (acreate h); split; first by hnf; intuition; aw.
have: (acreate (h \o (bcreate1 fg)) = acreate bf) by apply acreate_exten.
by rewrite -compose_acreate (bcreate_inv1 fg) bcreate_inv2.
Qed.
Lemma exists_left_composable_auxC: forall (a b c:Set) (f:a->b) (g:a-> c) s h,
is_right_inverseC s g ->
h \o g =1 f -> h =1 f \o s.
Proof.
move=> a b c f g s h ri eq x /=; rewrite -eq /=.
by move: (ri x) => /= ->.
Qed.
Theorem exists_left_composable_aux: forall f g s h ,
is_function f -> source f = source g ->
is_right_inverse s g ->
h \coP g -> h \co g = f -> h = f \co s.
Proof.
move=> f g s h gg sfsg [csg cshi] chg <-.
have shtg:(source h= target g) by move: chg=> [_ [_]].
by rewrite compose_assoc // cshi -shtg compose_id_right //; fct_tac.
Qed.
Lemma exists_unique_left_composableC: forall (a b c:Set) (f:a->b)(g:a->c) h h',
surjectiveC g -> h \o g =1 f -> h' \o g =1 f -> h =1 h'.
Proof.
move=> a b c f g h h' sg chg chg' x.
move: (exists_right_inv_from_surjC sg) => [j jp].
rewrite (exists_left_composable_auxC jp chg).
by rewrite (exists_left_composable_auxC jp chg').
Qed.
Theorem exists_unique_left_composable: forall f g h h',
is_function f -> surjection g -> source f = source g ->
h \coP g -> h' \coP g ->
h \co g = f -> h' \co g = f -> h = h'.
Proof.
move=>f g h h' ff sg sfsg chg chg' chgf chgf'.
move:(exists_right_inv_from_surj sg)=> [j jp].
rewrite (exists_left_composable_aux ff sfsg jp chg chgf).
by rewrite (exists_left_composable_aux ff sfsg jp chg' chgf').
Qed.
Lemma left_composable_valueC: forall (a b c:Set) (f:a->b)(g:a->c) s h,
surjectiveC g -> (forall (x y:a), g x = g y -> f x = f y) ->
is_right_inverseC s g -> h =1 f \o s ->
h \o g =1 f.
Proof.
move=> a b c f g s h sg hyp rish eq x /=.
by rewrite eq /=; apply hyp; rewrite -{2} (rish (g x)).
Qed.
Theorem left_composable_value: forall f g s h,
is_function f -> surjection g -> source f = source g ->
(forall x y, inc x (source g) -> inc y (source g) ->
W x g = W y g -> W x f = W y f) ->
is_right_inverse s g -> h = f \co s -> h \co g = f.
Proof.
move=> f g s h ff sg sfsg hyp rish ->.
move: (source_right_inverse rish)=> sstg.
move: rish=> [cgs cgsi].
have cfs: f \coP s.
by hnf; intuition; [fct_tac |move:cgs => [_[_]] <-].
have cfsg: (f \co s) \coP g by red; intuition;aw;fct_tac.
apply function_exten; aw; first by fct_tac.
by symmetry.
move=> x xg.
have Ws: (inc (W x g) (source s)).
by rewrite sstg; apply inc_W_target=>//; fct_tac.
have WWs: inc (W (W x g) s) (source g).
by move:cgs => [_[_]]->; apply inc_W_target=>//; fct_tac.
by aw; apply hyp =>//; rewrite -compose_W // cgsi; srw; rewrite -sstg.
Qed.
Lemma exists_right_composable_auxC: forall (a b c:Set) (f:a->b) (g:c->b) h r,
is_left_inverseC r g -> g \o h =1 f
-> h =1 r \o f.
Proof.
move=> a b c f g h r li eq x /=; rewrite -(eq x); symmetry;exact: (li (h x)).
Qed.
Theorem exists_right_composable_aux: forall f g h r,
is_function f -> target f = target g ->
is_left_inverse r g -> g \coP h -> g \co h = f
-> h = r \co f.
Proof.
move=> f g h r ff tftg [crg crgi] chg <-.
rewrite -compose_assoc // crgi.
by move:chg=> [_[fh]] ->;rewrite compose_id_left.
Qed.
Lemma exists_right_composable_uniqueC: forall (a b c:Set)(f:a->b) (g:c->b) h h',
injectiveC g -> g \o h =1 f -> g \o h' =1 f -> h =1 h'.
Proof.
move=> a b c f g h h' ig c1 c2 x.
apply ig; by move: (c1 x)(c2 x) => /= -> ->.
Qed.
Theorem exists_right_composable_unique: forall f g h h',
is_function f -> injection g -> target f = target g ->
g \coP h -> g \coP h' ->
g \co h = f -> g \co h' = f -> h = h'.
Proof.
move=> f g h h' ff [_ ig] tftg cgh cgh' cghf cghf'.
move: (cgh)(cgh') => [p1 [p2 p3]] [_ [p5 p6]].
rewrite -cghf' in cghf.
have shh': source h = source h'.
by rewrite - (compose_source h g) -(compose_source h' g) cghf.
apply function_exten => //; first by ue.
move=> x xsh.
apply ig.
by rewrite p3; apply inc_W_target.
rewrite p6; apply inc_W_target => //; ue.
move: (f_equal (W x) cghf); aw; ue.
Qed.
Lemma exists_right_composableC: forall (a b c:Set) (f:a->b) (g:c->b),
injectiveC g ->
(exists h, g \o h =1 f) = (forall u, exists v, g v = f u).
Proof.
move=> a b c f g ig; apply iff_eq.
by move=> [h cgh] u; exists (h u); rewrite -cgh.
move => mh.
case (emptyset_dichot c) => hyp.
have ae: (a = emptyset).
apply is_emptyset => y ya.
by move: (mh (Bo ya)) => [x _]; rewrite hyp in x; case x.
symmetry in hyp; symmetry in ae.
move: empty_function_function => ef.
have se: (source empty_function = a) by rewrite /empty_function; aw.
have te: (target empty_function = c) by rewrite /empty_function; aw.
exists (bcreate ef se te); move=> v.
suff: False by done.
by rewrite -ae in v; case v.
move: hyp=> [x xc].
move: (exists_left_inv_from_injC (inc_nonempty xc) ig) => [r rv].
exists (r \o f).
move=> y /=; move: (mh y)=> [v] <-; exact (f_equal g (rv v)).
Qed.
Theorem exists_right_composable: forall f g,
is_function f -> injection g -> target f = target g ->
(exists h, g \coP h & g \co h = f) =
(sub (range (graph f)) (range (graph g))).
Proof.
move=> f g ff ig tftg; symmetry in tftg.
have fg: (is_function g) by fct_tac.
apply iff_eq.
move => [h [chg cghf]] x; dw; fprops.
have shsf: (source h = source f) by rewrite - cghf; aw.
move=> [y Jg].
move: (inc_pr1graph_source ff Jg); rewrite -shsf => xsh.
exists (W y h); rewrite - (W_pr ff Jg) -cghf; aw; graph_tac.
by move: chg => [_ [fh]]=> ->; fprops.
case (emptyset_dichot(source g)).
case (emptyset_dichot(source f)).
move=> ssfe sge hyp.
have cge: (g \coP empty_function).
hnf; intuition; first by apply empty_function_function.
by rewrite /empty_function; aw.
exists (empty_function); split=>//.
apply function_exten=>//; rewrite /empty_function;try fct_tac; aw.
by symmetry.
by move => x xe; empty_tac0.
move: ff=> [_ [fgf]] ->.
move=> [x xsf] sge hyp.
move: xsf;set (gf:=graph f); dw; last by fprops.
move=> [y Jgf].
have: (inc y (range (graph g))) by apply hyp; dw; fprops; exists x.
dw; fprops;move => [z Jg]; move: (inc_pr1graph_source fg Jg)=> pe.
by rewrite sge in pe; empty_tac0.
move=> nesg hyp.
move: (exists_left_inv_from_inj ig nesg)=> [r rli].
move: (target_left_inverse rli)=> trsg. move: rli=> [crg crgi].
have crf: (r \coP f).
by hnf; intuition; first (by fct_tac); move: crg=> [_[_]]->; symmetry.
have fcrf: (is_function (r \co f)) by fct_tac.
have cgrf: (g \coP (r \co f)) by hnf; aw; auto.
exists (r \co f); split=>//.
apply function_exten; try fct_tac; aw.
move=> x xsf; aw.
move: xsf; rewrite-(f_domain_graph ff) domain_rw; fprops.
move=> [y Jg]; rewrite (W_pr ff Jg).
have: (inc y (range (graph g))) by apply hyp; dw; fprops; ex_tac.
dw; fprops; move=> [z Jg1].
have zg: (inc z (source g)) by graph_tac.
rewrite - (W_pr fg Jg1).
have: (W z (r \co g) = z) by rewrite crgi; srw.
by aw; move=>->.
Qed.
Lemma right_composable_valueC: forall (a b c:Set) (f:a->b) (g:c->b) r h,
injectiveC g -> is_left_inverseC r g -> (forall u, exists v, g v = f u) ->
h =1 r \o f -> g \o h =1 f.
Proof.
move=> a b c f g r h ig lir hyp eq x /=; rewrite eq /=.
by move: (hyp x)=> [v] <-; rewrite (w_left_inverse v lir).
Qed.
Theorem right_composable_value: forall f g r h,
is_function f -> injection g -> target g = target f ->
is_left_inverse r g ->
(sub (range (graph f)) (range (graph g))) ->
h = r \co f -> g \co h = f.
Proof.
move=> f g r h ff ig tgtf lirg hyp ->.
move: (target_left_inverse lirg)=> trsg; move: lirg=> [crg crgi].
have srtg: source r = target g by move: crg=>[_[_]].
have crf: (r \coP f) by hnf; intuition; try fct_tac; rewrite srtg.
have cgrf: g \coP (r \co f) by hnf; intuition; try fct_tac; symmetry; aw.
have cgr: (g \coP r) by hnf; intuition; fct_tac.
apply function_exten; aw; try fct_tac.
move=> x xf.
have: (inc (W x f) (range (graph g))).
by apply hyp; rewrite range_inc_rw=>//; exists x; auto.
rewrite range_inc_rw; last by fct_tac.
aw;move=> [y [ys]] ->; move: (f_equal (fun z=> (W y z)) crgi); aw; srw.
by move=>->.
Qed.
Given a function f with two arguments and one argument, we obtain a function of one argument
Definition partial_fun2 f y :=
BL(fun x=> W (J x y) f) (im_singleton (inverse_graph (source f)) y) (target f).
Definition partial_fun1 f x :=
BL(fun y=> W (J x y) f)(im_singleton (source f) x) (target f).
Lemma partial_fun1_axioms: forall f x, is_function f -> is_graph(source f) ->
transf_axioms (fun y=> W (J x y) f)(im_singleton (source f) x) (target f).
Proof. by move=> f x ff sg t; rewrite im_singleton_pr; fprops.
Qed.
Lemma partial_fun1_function: forall f x, is_function f -> is_graph(source f) ->
is_function (partial_fun1 f x).
Proof.
rewrite/partial_fun1=> f x ff sg.
by apply bl_function; apply partial_fun1_axioms.
Qed.
Lemma partial_fun1_W: forall f x y, is_function f -> is_graph(source f) ->
inc (J x y) (source f) -> W y (partial_fun1 f x) = W (J x y) f.
Proof.
by rewrite/partial_fun1=> f x y ff gs Js; aw; apply partial_fun1_axioms.
Qed.
Lemma partial_fun2_axioms: forall f y, is_function f -> is_graph(source f) ->
transf_axioms (fun x=>W (J x y) f)(im_singleton (inverse_graph (source f)) y)
(target f).
Proof. by move=> f y ff gs v; rewrite im_singleton_pr; aw; fprops. Qed.
Lemma partial_fun2_function: forall f y, is_function f -> is_graph(source f) ->
is_function (partial_fun2 f y).
Proof.
rewrite/partial_fun2=> f y ff gs.
by apply bl_function; apply partial_fun2_axioms.
Qed.
Lemma partial_fun2_W: forall f x y, is_function f -> is_graph(source f) ->
inc (J x y) (source f) -> W x (partial_fun2 f y) = W (J x y) f.
Proof.
rewrite /partial_fun2=> f x y ff gs Js; aw; last by aw.
by apply partial_fun2_axioms.
Qed.
BL(fun x=> W (J x y) f) (im_singleton (inverse_graph (source f)) y) (target f).
Definition partial_fun1 f x :=
BL(fun y=> W (J x y) f)(im_singleton (source f) x) (target f).
Lemma partial_fun1_axioms: forall f x, is_function f -> is_graph(source f) ->
transf_axioms (fun y=> W (J x y) f)(im_singleton (source f) x) (target f).
Proof. by move=> f x ff sg t; rewrite im_singleton_pr; fprops.
Qed.
Lemma partial_fun1_function: forall f x, is_function f -> is_graph(source f) ->
is_function (partial_fun1 f x).
Proof.
rewrite/partial_fun1=> f x ff sg.
by apply bl_function; apply partial_fun1_axioms.
Qed.
Lemma partial_fun1_W: forall f x y, is_function f -> is_graph(source f) ->
inc (J x y) (source f) -> W y (partial_fun1 f x) = W (J x y) f.
Proof.
by rewrite/partial_fun1=> f x y ff gs Js; aw; apply partial_fun1_axioms.
Qed.
Lemma partial_fun2_axioms: forall f y, is_function f -> is_graph(source f) ->
transf_axioms (fun x=>W (J x y) f)(im_singleton (inverse_graph (source f)) y)
(target f).
Proof. by move=> f y ff gs v; rewrite im_singleton_pr; aw; fprops. Qed.
Lemma partial_fun2_function: forall f y, is_function f -> is_graph(source f) ->
is_function (partial_fun2 f y).
Proof.
rewrite/partial_fun2=> f y ff gs.
by apply bl_function; apply partial_fun2_axioms.
Qed.
Lemma partial_fun2_W: forall f x y, is_function f -> is_graph(source f) ->
inc (J x y) (source f) -> W x (partial_fun2 f y) = W (J x y) f.
Proof.
rewrite /partial_fun2=> f x y ff gs Js; aw; last by aw.
by apply partial_fun2_axioms.
Qed.
Product of two functions
Definition ext_to_prod u v :=
BL(fun z=> J (W (P z) u)(W (Q z) v))
(product (source u)(source v))
(product (target u)(target v)).
Lemma ext_to_prod_function: forall u v,
is_function u -> is_function v ->
is_function (ext_to_prod u v).
Proof.
rewrite /ext_to_prod=> u v fu fv; apply bl_function.
by move=> t;aw; intuition.
Qed.
Hint Resolve ext_to_prod_function: fprops.
Lemma ext_to_prod_W: forall u v a b,
is_function u -> is_function v-> inc a (source u) -> inc b (source v)->
W (J a b) (ext_to_prod u v) = J (W a u) (W b v).
Proof.
rewrite /ext_to_prod=> u v a b fu fv asu bsv.
aw; [by move=> t;aw; intuition | fprops].
Qed.
Lemma ext_to_prod_W2: forall u v c,
is_function u -> is_function v->
inc c (product (source u)(source v)) ->
W c (ext_to_prod u v) = J (W (P c) u) (W (Q c) v).
Proof.
move=> u v c fu fv; aw; move=> [aa [bb cc]].
have eq: (J (P c) (Q c) =c) by aw.
by rewrite -{1}eq ext_to_prod_W.
Qed.
Lemma ext_to_prod_range: forall u v,
is_function u -> is_function v->
range (graph (ext_to_prod u v)) =
product (range (graph u))(range (graph v)).
Proof.
move=> u v fu fv.
have fe: (is_function (ext_to_prod u v)) by fprops.
set_extens t; aw;dw;fprops.
move=> [p Jg]; move: (W_pr fe Jg)=>Wp.
have : (inc p (source (ext_to_prod u v))) by graph_tac.
rewrite /ext_to_prod bl_source=> ps.
move: Wp; rewrite ext_to_prod_W2 //; move=> <-.
move: ps; aw; move=> [_ [pp qp]].
intuition.
exists (P p); graph_tac.
exists (Q p); graph_tac.
move=> [p [ [x p1] [y p2]]].
exists (J x y); rewrite /ext_to_prod /BL/L; aw.
exists (J x y); split;aw; first by ee;graph_tac.
by rewrite (W_pr fu p1) (W_pr fv p2) p.
Qed.
Lemma ext_to_prod_propP: forall a a' (x: product a a'), inc (P (Ro x)) a.
Proof.
move=> a a' x; have: (inc (Ro x) (product a a')) by apply R_inc.
by aw; intuition.
Qed.
Lemma ext_to_prod_propQ: forall a a' (x: product a a'), inc (Q (Ro x)) a'.
Proof.
move=> a a' x; have: (inc (Ro x) (product a a')) by apply R_inc.
by aw; intuition.
Qed.
Lemma ext_to_prod_propJ: forall (b b':Set) (x:b)(x':b'),
inc (J (Ro x)(Ro x')) (product b b').
Proof. move=> b b' x x'; aw; intuition; apply R_inc. Qed.
Definition pr1C a b:= fun x:product a b => Bo(ext_to_prod_propP x).
Definition pr2C a b:= fun x:product a b => Bo(ext_to_prod_propQ x).
Definition pairC (a b:Set) := fun (x:a)(y:b) => Bo(ext_to_prod_propJ x y).
Definition ext_to_prodC (a b a' b':Set) (u:a->a')(v:b->b') :=
fun x => pairC (u (pr1C x)) (v (pr2C x)).
Lemma prC_prop: forall (a b:Set) (x:product a b),
Ro x = J (Ro (pr1C x)) (Ro (pr2C x)).
Proof.
move=> a b x.
have: (inc (Ro x) (product a b)) by apply R_inc.
aw; rewrite /pr1C/pr2C B_eq B_eq; intuition; aw.
Qed.
Lemma pr1C_prop: forall (a b:Set) (x:product a b),
Ro (pr1C x) = P (Ro x).
Proof. move=> a b x; rewrite (prC_prop x); aw. Qed.
Lemma pr2C_prop: forall (a b:Set) (x:product a b),
Ro (pr2C x) = Q (Ro x).
Proof. move=> a b x; rewrite (prC_prop x); aw. Qed.
Lemma prJ_prop: forall (a b:Set) (x:a)(y:b),
Ro(pairC x y) = J (Ro x) (Ro y).
Proof. by move=> a b x y; rewrite /pairC B_eq. Qed.
Lemma prJ_recov: forall (a b:Set) (x:product a b),
pairC (pr1C x) (pr2C x) = x.
Proof.
move=> a b c; apply R_inj; rewrite prJ_prop pr1C_prop pr2C_prop.
have aux: (inc (Ro c) (product a b)) by apply R_inc.
by awi aux; move:aux=> [? ]; aw.
Qed.
Lemma ext_to_prod_prop:
forall (a b a' b':Set) (u:a->a')(v:b->b') (x:a)(x':b),
J(Ro (u x)) (Ro (v x')) = Ro(ext_to_prodC u v (pairC x x')).
Proof.
move=> a b a' b' u v x x'.
rewrite /ext_to_prodC prJ_prop.
have: (x = (pr1C (pairC x x'))).
by apply R_inj; rewrite pr1C_prop prJ_prop; aw.
have: (x' = (pr2C (pairC x x'))).
by apply R_inj; rewrite pr2C_prop prJ_prop; aw.
by move=> <- <-.
Qed.
BL(fun z=> J (W (P z) u)(W (Q z) v))
(product (source u)(source v))
(product (target u)(target v)).
Lemma ext_to_prod_function: forall u v,
is_function u -> is_function v ->
is_function (ext_to_prod u v).
Proof.
rewrite /ext_to_prod=> u v fu fv; apply bl_function.
by move=> t;aw; intuition.
Qed.
Hint Resolve ext_to_prod_function: fprops.
Lemma ext_to_prod_W: forall u v a b,
is_function u -> is_function v-> inc a (source u) -> inc b (source v)->
W (J a b) (ext_to_prod u v) = J (W a u) (W b v).
Proof.
rewrite /ext_to_prod=> u v a b fu fv asu bsv.
aw; [by move=> t;aw; intuition | fprops].
Qed.
Lemma ext_to_prod_W2: forall u v c,
is_function u -> is_function v->
inc c (product (source u)(source v)) ->
W c (ext_to_prod u v) = J (W (P c) u) (W (Q c) v).
Proof.
move=> u v c fu fv; aw; move=> [aa [bb cc]].
have eq: (J (P c) (Q c) =c) by aw.
by rewrite -{1}eq ext_to_prod_W.
Qed.
Lemma ext_to_prod_range: forall u v,
is_function u -> is_function v->
range (graph (ext_to_prod u v)) =
product (range (graph u))(range (graph v)).
Proof.
move=> u v fu fv.
have fe: (is_function (ext_to_prod u v)) by fprops.
set_extens t; aw;dw;fprops.
move=> [p Jg]; move: (W_pr fe Jg)=>Wp.
have : (inc p (source (ext_to_prod u v))) by graph_tac.
rewrite /ext_to_prod bl_source=> ps.
move: Wp; rewrite ext_to_prod_W2 //; move=> <-.
move: ps; aw; move=> [_ [pp qp]].
intuition.
exists (P p); graph_tac.
exists (Q p); graph_tac.
move=> [p [ [x p1] [y p2]]].
exists (J x y); rewrite /ext_to_prod /BL/L; aw.
exists (J x y); split;aw; first by ee;graph_tac.
by rewrite (W_pr fu p1) (W_pr fv p2) p.
Qed.
Lemma ext_to_prod_propP: forall a a' (x: product a a'), inc (P (Ro x)) a.
Proof.
move=> a a' x; have: (inc (Ro x) (product a a')) by apply R_inc.
by aw; intuition.
Qed.
Lemma ext_to_prod_propQ: forall a a' (x: product a a'), inc (Q (Ro x)) a'.
Proof.
move=> a a' x; have: (inc (Ro x) (product a a')) by apply R_inc.
by aw; intuition.
Qed.
Lemma ext_to_prod_propJ: forall (b b':Set) (x:b)(x':b'),
inc (J (Ro x)(Ro x')) (product b b').
Proof. move=> b b' x x'; aw; intuition; apply R_inc. Qed.
Definition pr1C a b:= fun x:product a b => Bo(ext_to_prod_propP x).
Definition pr2C a b:= fun x:product a b => Bo(ext_to_prod_propQ x).
Definition pairC (a b:Set) := fun (x:a)(y:b) => Bo(ext_to_prod_propJ x y).
Definition ext_to_prodC (a b a' b':Set) (u:a->a')(v:b->b') :=
fun x => pairC (u (pr1C x)) (v (pr2C x)).
Lemma prC_prop: forall (a b:Set) (x:product a b),
Ro x = J (Ro (pr1C x)) (Ro (pr2C x)).
Proof.
move=> a b x.
have: (inc (Ro x) (product a b)) by apply R_inc.
aw; rewrite /pr1C/pr2C B_eq B_eq; intuition; aw.
Qed.
Lemma pr1C_prop: forall (a b:Set) (x:product a b),
Ro (pr1C x) = P (Ro x).
Proof. move=> a b x; rewrite (prC_prop x); aw. Qed.
Lemma pr2C_prop: forall (a b:Set) (x:product a b),
Ro (pr2C x) = Q (Ro x).
Proof. move=> a b x; rewrite (prC_prop x); aw. Qed.
Lemma prJ_prop: forall (a b:Set) (x:a)(y:b),
Ro(pairC x y) = J (Ro x) (Ro y).
Proof. by move=> a b x y; rewrite /pairC B_eq. Qed.
Lemma prJ_recov: forall (a b:Set) (x:product a b),
pairC (pr1C x) (pr2C x) = x.
Proof.
move=> a b c; apply R_inj; rewrite prJ_prop pr1C_prop pr2C_prop.
have aux: (inc (Ro c) (product a b)) by apply R_inc.
by awi aux; move:aux=> [? ]; aw.
Qed.
Lemma ext_to_prod_prop:
forall (a b a' b':Set) (u:a->a')(v:b->b') (x:a)(x':b),
J(Ro (u x)) (Ro (v x')) = Ro(ext_to_prodC u v (pairC x x')).
Proof.
move=> a b a' b' u v x x'.
rewrite /ext_to_prodC prJ_prop.
have: (x = (pr1C (pairC x x'))).
by apply R_inj; rewrite pr1C_prop prJ_prop; aw.
have: (x' = (pr2C (pairC x x'))).
by apply R_inj; rewrite pr2C_prop prJ_prop; aw.
by move=> <- <-.
Qed.
If the two functions are injective, surjective, bijective,
so is the product. The inverse of the prodiuct is trivial
Lemma ext_to_prod_injective: forall u v,
injection u -> injection v -> injection (ext_to_prod u v).
Proof.
move=> u v [fu iu] [fv iv]; split; fprops.
rewrite /ext_to_prod; aw.
move => x y xs ys; rewrite ext_to_prod_W2 // ext_to_prod_W2 //.
move: xs ys; aw.
move => [px [pxs qxs]] [py [pys qys]] eq.
apply pair_exten =>//.
by apply iu=>//; apply (pr1_def eq).
by apply iv=>//; apply (pr2_def eq).
Qed.
Lemma ext_to_prod_surjective: forall u v,
surjection u -> surjection v -> surjection (ext_to_prod u v).
Proof.
move=> u v su sv.
have fu:is_function u by fct_tac.
have fv:is_function v by fct_tac.
apply surjective_pr6; first by fprops.
move=> y.
rewrite /ext_to_prod; aw; move=> [py [ptu qtv]].
move: (surjective_pr2 su ptu)=> [pv [prv prw]].
move: (surjective_pr2 sv qtv)=> [qv [qrv qrw]].
exists (J pv qv); split; fprops.
rewrite ext_to_prod_W //.
by apply pair_exten; fprops; aw.
Qed.
Lemma ext_to_prod_bijective: forall u v,
bijection u -> bijection v -> bijection (ext_to_prod u v).
Proof.
rewrite/bijective=> u v [p1 p2] [p3 p4].
split; first by apply ext_to_prod_injective.
by apply ext_to_prod_surjective.
Qed.
Lemma ext_to_prod_inverse: forall u v,
bijection u -> bijection v->
inverse_fun (ext_to_prod u v) =
ext_to_prod (inverse_fun u)(inverse_fun v).
Proof.
move=> u v bu bv.
have Ha:bijection (ext_to_prod u v) by apply ext_to_prod_bijective.
have Hb:is_function (inverse_fun u) by apply bijective_inv_function.
have Hc:is_function (inverse_fun v) by apply bijective_inv_function.
apply function_exten; fprops; try solve [rewrite /ext_to_prod; aw].
by apply bijective_inv_function.
move=> x xp.
rewrite /ext_to_prod in xp; awi xp; move:xp=>[xp [pxu qxv]].
rewrite ext_to_prod_W2=>//; last by aw.
have p1: (inc (W (P x) (inverse_fun u)) (source u)).
have : source u =(target (inverse_fun u)) by aw.
by move=>->; apply inc_W_target; aw.
have p2: (inc (W (Q x) (inverse_fun v)) (source v)).
have : source v =(target (inverse_fun v)) by aw.
by move=>->; apply inc_W_target; aw.
symmetry; apply W_inverse2=>//.
by rewrite /ext_to_prod; aw; split; fprops.
rewrite ext_to_prod_W=>//; try fct_tac.
have: (P x = W (W (P x) (inverse_fun u)) u) by apply W_inverse.
have: (Q x = W (W (Q x) (inverse_fun v)) v) by apply W_inverse.
by move => <- <-; aw.
Qed.
Composition of products
Lemma composable_ext_to_prod2: forall u v u' v',
u' \coP u -> v' \coP v -> (ext_to_prod u' v') \coP (ext_to_prod u v).
Proof.
move=> u v u' v' [fu' [fu seq]] [fv' [fv seq']].
hnf; intuition.
rewrite /ext_to_prod; aw; by rewrite seq seq'.
Qed.
Lemma compose_ext_to_prod2: forall u v u' v',
u' \coP u -> v' \coP v ->
(ext_to_prod u' v') \co (ext_to_prod u v) =
ext_to_prod (u' \co u)(v' \co v).
Proof.
move=> u v u' v' cuu cvv.
have cee: ((ext_to_prod u' v') \coP (ext_to_prod u v))
by apply composable_ext_to_prod2.
have fcu: (is_function (u' \co u)) by fct_tac.
have fcv: (is_function (v' \co v)) by fct_tac.
apply function_exten; try fct_tac; fprops; try solve [ rewrite/ext_to_prod;aw].
aw; move => x xs.
have xs1: inc x (product (source u) (source v))
by rewrite /ext_to_prod bl_source in xs.
have : inc x (product (source u) (source v)) by [].
rewrite product_inc_rw; move=> [xp [pxs qxs]].
have res1: inc (W x (ext_to_prod u v)) (product (source u') (source v')).
have aux: (product (source u') (source v')= target(ext_to_prod u v)).
move:cuu => [_[_]]; move: cvv => [_[_]]; move=> -> ->.
by rewrite /ext_to_prod; aw.
by rewrite aux; apply inc_W_target=>//; fct_tac.
aw; rewrite ext_to_prod_W2=>//; try fct_tac.
rewrite ext_to_prod_W2=>//; try fct_tac.
by rewrite ext_to_prod_W2=>//; aw.
Qed.
Lemma injective_ext_to_prod2C: forall (a b a' b':Set) (u:a->a')(v:b->b'),
injectiveC u -> injectiveC v-> injectiveC (ext_to_prodC u v).
Proof.
move=> a b a' b' u v iu iv x x' eql.
move: (f_equal (@Ro (product a' b')) eql).
rewrite -(prJ_recov x) -(prJ_recov x').
rewrite - 2!ext_to_prod_prop; move=> eql'.
by rewrite (iu _ _ (R_inj (pr1_def eql'))) (iv _ _ (R_inj (pr2_def eql'))).
Qed.
Lemma surjective_ext_to_prod2C: forall (a b a' b':Set) (u:a->a')(v:b->b'),
surjectiveC u -> surjectiveC v-> surjectiveC (ext_to_prodC u v).
Proof.
move=> a b a' b' u v su sv x; rewrite -(prJ_recov x).
have pRx: is_pair (Ro x) by move: (R_inc x); aw; intuition.
move: (su (pr1C x)) => [y yp]; move: (sv (pr2C x)) => [y' y'p].
exists (pairC y y'); apply R_inj.
rewrite - ext_to_prod_prop yp y'p prJ_recov pr1C_prop pr2C_prop; aw.
Qed.
Lemma bijective_ext_to_prod2C: forall (a b a' b':Set) (u:a->a')(v:b->b'),
bijectiveC u -> bijectiveC v-> bijectiveC (ext_to_prodC u v).
Proof.
rewrite /bijectiveC=> a b a' b' u v [p1 p2][p3 P4].
by split ; [apply injective_ext_to_prod2C | apply surjective_ext_to_prod2C].
Qed.
Lemma compose_ext_to_prod2C: forall (a b c a' b' c':Set) (u:b-> c)(v:a->b)
(u':b'-> c')(v':a'->b'),
(ext_to_prodC u u') \o (ext_to_prodC v v') =1
ext_to_prodC (u \o v)(u' \o v').
Proof.
move => a b c a' b' c' u v u' v' x /=.
rewrite -(prJ_recov x).
move: (ext_to_prod_prop v v' (pr1C x) (pr2C x));rewrite -prJ_prop=> xx.
rewrite - (R_inj xx).
by apply R_inj; rewrite -2! ext_to_prod_prop.
Qed.
Lemma inverse_ext_to_prod2C: forall (a b a' b':Set) (u:a->a')(v:b->b')
(Hu: bijectiveC u)(Hv:bijectiveC v),
inverseC (bijective_ext_to_prod2C Hu Hv) =1
ext_to_prodC (inverseC Hu)(inverseC Hv).
Proof.
move => a b a' b' u v Hu Hv x.
have ww: x = ext_to_prodC u v (ext_to_prodC (inverseC Hu) (inverseC Hv) x).
move: ( compose_ext_to_prod2C u (inverseC Hu) v(inverseC Hv))=> eq.
move: (eq x) => /= ->.
rewrite - (prJ_recov x); apply R_inj.
by rewrite -ext_to_prod_prop /= inverseC_prb inverseC_prb prJ_prop.
by rewrite ww inverseC_pra -ww.
Qed.
u' \coP u -> v' \coP v -> (ext_to_prod u' v') \coP (ext_to_prod u v).
Proof.
move=> u v u' v' [fu' [fu seq]] [fv' [fv seq']].
hnf; intuition.
rewrite /ext_to_prod; aw; by rewrite seq seq'.
Qed.
Lemma compose_ext_to_prod2: forall u v u' v',
u' \coP u -> v' \coP v ->
(ext_to_prod u' v') \co (ext_to_prod u v) =
ext_to_prod (u' \co u)(v' \co v).
Proof.
move=> u v u' v' cuu cvv.
have cee: ((ext_to_prod u' v') \coP (ext_to_prod u v))
by apply composable_ext_to_prod2.
have fcu: (is_function (u' \co u)) by fct_tac.
have fcv: (is_function (v' \co v)) by fct_tac.
apply function_exten; try fct_tac; fprops; try solve [ rewrite/ext_to_prod;aw].
aw; move => x xs.
have xs1: inc x (product (source u) (source v))
by rewrite /ext_to_prod bl_source in xs.
have : inc x (product (source u) (source v)) by [].
rewrite product_inc_rw; move=> [xp [pxs qxs]].
have res1: inc (W x (ext_to_prod u v)) (product (source u') (source v')).
have aux: (product (source u') (source v')= target(ext_to_prod u v)).
move:cuu => [_[_]]; move: cvv => [_[_]]; move=> -> ->.
by rewrite /ext_to_prod; aw.
by rewrite aux; apply inc_W_target=>//; fct_tac.
aw; rewrite ext_to_prod_W2=>//; try fct_tac.
rewrite ext_to_prod_W2=>//; try fct_tac.
by rewrite ext_to_prod_W2=>//; aw.
Qed.
Lemma injective_ext_to_prod2C: forall (a b a' b':Set) (u:a->a')(v:b->b'),
injectiveC u -> injectiveC v-> injectiveC (ext_to_prodC u v).
Proof.
move=> a b a' b' u v iu iv x x' eql.
move: (f_equal (@Ro (product a' b')) eql).
rewrite -(prJ_recov x) -(prJ_recov x').
rewrite - 2!ext_to_prod_prop; move=> eql'.
by rewrite (iu _ _ (R_inj (pr1_def eql'))) (iv _ _ (R_inj (pr2_def eql'))).
Qed.
Lemma surjective_ext_to_prod2C: forall (a b a' b':Set) (u:a->a')(v:b->b'),
surjectiveC u -> surjectiveC v-> surjectiveC (ext_to_prodC u v).
Proof.
move=> a b a' b' u v su sv x; rewrite -(prJ_recov x).
have pRx: is_pair (Ro x) by move: (R_inc x); aw; intuition.
move: (su (pr1C x)) => [y yp]; move: (sv (pr2C x)) => [y' y'p].
exists (pairC y y'); apply R_inj.
rewrite - ext_to_prod_prop yp y'p prJ_recov pr1C_prop pr2C_prop; aw.
Qed.
Lemma bijective_ext_to_prod2C: forall (a b a' b':Set) (u:a->a')(v:b->b'),
bijectiveC u -> bijectiveC v-> bijectiveC (ext_to_prodC u v).
Proof.
rewrite /bijectiveC=> a b a' b' u v [p1 p2][p3 P4].
by split ; [apply injective_ext_to_prod2C | apply surjective_ext_to_prod2C].
Qed.
Lemma compose_ext_to_prod2C: forall (a b c a' b' c':Set) (u:b-> c)(v:a->b)
(u':b'-> c')(v':a'->b'),
(ext_to_prodC u u') \o (ext_to_prodC v v') =1
ext_to_prodC (u \o v)(u' \o v').
Proof.
move => a b c a' b' c' u v u' v' x /=.
rewrite -(prJ_recov x).
move: (ext_to_prod_prop v v' (pr1C x) (pr2C x));rewrite -prJ_prop=> xx.
rewrite - (R_inj xx).
by apply R_inj; rewrite -2! ext_to_prod_prop.
Qed.
Lemma inverse_ext_to_prod2C: forall (a b a' b':Set) (u:a->a')(v:b->b')
(Hu: bijectiveC u)(Hv:bijectiveC v),
inverseC (bijective_ext_to_prod2C Hu Hv) =1
ext_to_prodC (inverseC Hu)(inverseC Hv).
Proof.
move => a b a' b' u v Hu Hv x.
have ww: x = ext_to_prodC u v (ext_to_prodC (inverseC Hu) (inverseC Hv) x).
move: ( compose_ext_to_prod2C u (inverseC Hu) v(inverseC Hv))=> eq.
move: (eq x) => /= ->.
rewrite - (prJ_recov x); apply R_inj.
by rewrite -ext_to_prod_prop /= inverseC_prb inverseC_prb prJ_prop.
by rewrite ww inverseC_pra -ww.
Qed.
Canonical decomposition of a function
Lemma image_of_fun_range: forall f, is_function f ->
image_of_fun f = range (graph f).
Proof.
move=> f [_ [a b]]; rewrite /image_of_fun -image_by_graph_domain; fprops.
by rewrite b.
Qed.
Lemma canonical_decomposition1: forall f g i,
is_function f ->
g = restriction2 f (source f) (range (graph f)) ->
i = canonical_injection (range (graph f)) (target f) ->
(i \coP g & f = i \co g & injection i & surjection g &
(injection f -> bijection g )).
Proof.
move=> f g i ff gv iv.
have Ha:sub (range (graph f)) (target f) by move:ff=> [? _]; fprops.
have ra: (restriction2_axioms f (source f) (range (graph f))).
hnf; intuition; fprops.
by rewrite /image_by_fun; apply sub_image_by_graph.
have fg: (is_function g) by rewrite gv; fprops.
have fi: (is_function i) by rewrite iv; fprops.
have ii: injection i by rewrite iv;apply ci_injective.
have sfsg:source f = source g by rewrite gv /restriction2; aw.
have sg:surjection g.
by rewrite gv; apply restriction2_surjective=>//; apply image_of_fun_range.
have cig: (i \coP g).
hnf; intuition.
by rewrite gv iv /canonical_injection /restriction2; aw.
have fcig: f = i \co g.
apply function_exten=>//; try fct_tac; aw.
by rewrite iv /restriction2 /canonical_injection; aw.
move => x xs.
have xsg: inc x (source g) by rewrite -sfsg.
aw; rewrite gv restriction2_W // iv ci_W //.
by rewrite range_inc_rw; fprops; ex_tac.
have r: injection f -> bijection g
by split=>//; apply inj_right_compose with i=>//; rewrite -fcig.
intuition.
Qed.
Restriction to its image
Definition imageC (a b:Set) (f:a->b) := IM (fun u:a => Ro (f u)).
Lemma imageC_inc: forall (a b:Set) (f:a->b) (x:a), inc (Ro (f x)) (imageC f).
Proof.
by rewrite /imageC=> a b f x; apply IM_inc; exists x.
Qed.
Lemma imageC_exists: forall (a b:Set) (f:a->b) x,
inc x (imageC f) -> exists y:a, x = Ro (f y).
Proof.
by rewrite /imageC=> a b f x xi; move: (IM_exists xi)=> [y] <-; exists y.
Qed.
Lemma sub_image_targetC: forall (a b:Set) (f:a->b), sub (imageC f) b.
Proof.
by move=> a b f x xi; move: (imageC_exists xi)=> [y] ->; apply R_inc.
Qed.
Definition restriction_to_image (a b:Set) (f:a->b) :=
fun x:a => Bo (imageC_inc f x).
Lemma restriction_to_image_pr: forall (a b:Set) (f:a->b) (x:a),
Ro (restriction_to_image f x) = Ro (f x).
Proof. by move=> a b f x; rewrite /restriction_to_image B_eq. Qed.
Lemma canonical_decomposition1C: forall (a b:Set) (f:a->b)
(g:a-> imageC f)(i:imageC f ->b),
g = restriction_to_image f ->
i = inclusionC (sub_image_targetC (f:=f)) ->
(injectiveC i & surjectiveC g &
(injectiveC f -> bijectiveC g )).
Proof.
move=> a b f g i gv iv.
have sg: surjectiveC g.
move=> x; rewrite gv.
have aux: (inc (Ro x) (imageC f)) by apply R_inc.
move: (imageC_exists aux)=> [y]. exists y. apply R_inj.
by rewrite restriction_to_image_pr; symmetry.
split.
move=> x x' eq; move: (f_equal (@Ro b) eq).
by rewrite iv 2! inclusionC_pr; apply R_inj.
split=>//.
move=> fi; split=> //; move=> x y eq ; move: (f_equal (@Ro (imageC f)) eq).
rewrite gv 2!restriction_to_image_pr=> eqbis.
by apply fi; apply R_inj.
Qed.
End Bfunction.
Export Bfunction.