Library ZFrelations


Require Import ZFpairs.
Import IZF.


Definition is_relation x :=
  forall p, p \in x -> p == couple (fst p) (snd p).

Definition rel_app r x y := couple x y \in r.

Instance rel_app_morph :
  Proper (eq_set ==> eq_set ==> eq_set ==> iff) rel_app.
Qed.

Definition rel_domain r :=
  subset (union (union r)) (fun x => exists y, rel_app r x y).

Definition rel_image r :=
  subset (union (union r)) (fun y => exists x, rel_app r x y).

Instance rel_image_morph : morph1 rel_image.


Qed.

Lemma rel_image_ex : forall r x, x \in rel_domain r -> exists y, rel_app r x y.

Lemma rel_domain_intro : forall r x y, rel_app r x y -> x \in rel_domain r.

Lemma rel_image_intro : forall r x y, rel_app r x y -> y \in rel_image r.

Definition rel_comp f g :=
  subset (prodcart (rel_domain g) (rel_image f))
    (fun p => exists2 y, rel_app g (fst p) y & rel_app f y (snd p)).

Lemma rel_comp_intro : forall f g x y z,
  rel_app g x y -> rel_app f y z -> rel_app (rel_comp f g) x z.


Definition rel A B := power (prodcart A B).

Lemma rel_mono :
  Proper (incl_set ==> incl_set ==> incl_set) rel.

Instance rel_morph : morph2 rel.

Lemma app_typ1 : forall r x y A B, r \in rel A B -> rel_app r x y -> x \in A.

Lemma app_typ2 : forall r x y A B, r \in rel A B -> rel_app r x y -> y \in B.

Lemma rel_is_relation : forall f A B, f \in rel A B -> is_relation f.

Lemma rel_domain_incl : forall r A B, r \in rel A B -> rel_domain r \incl A.

Lemma rel_image_incl : forall r A B, r \in rel A B -> rel_image r \incl B.

Lemma relation_is_rel :
  forall r A B,
  is_relation r ->
  rel_domain r \incl A ->
  rel_image r \incl B ->
  r \in rel A B.

Definition inject_rel R A B :=
  subset (prodcart A B) (fun p => R (fst p) (snd p)).

Lemma inject_rel_is_rel : forall (R:set->set->Prop) A B,
  inject_rel R A B \in rel A B.

Lemma inject_rel_intro :
  forall (R:set->set->Prop) A B x y,
  ext_rel A R ->
  x \in A ->
  y \in B ->
  R x y ->
  rel_app (inject_rel R A B) x y.

Lemma inject_rel_elim :
  forall (R:set->set->Prop) A B x y,
  ext_rel A R ->
  rel_app (inject_rel R A B) x y ->
  x \in A /\ y \in B /\ R x y.


Definition is_function f :=
  is_relation f /\
  forall x y y', rel_app f x y -> rel_app f x y' -> y == y'.

Definition app f x :=
  union (subset (rel_image f) (fun y => rel_app f x y)).

Instance app_morph : morph2 app.


Lemma app_defined : forall f x y,
  is_function f -> rel_app f x y -> app f x == y.

Lemma app_elim : forall f x,
  is_function f -> x \in rel_domain f -> rel_app f x (app f x).


Definition func A B :=
  subset (rel A B)
    (fun r =>
       (forall x, x \in A -> exists2 y, y \in B & rel_app r x y) /\
       (forall x y y', rel_app r x y -> rel_app r x y' -> y == y')).

Instance func_mono :
  Proper (eq_set ==> incl_set ==> incl_set) func.


Qed.

Instance func_morph : morph2 func.

Lemma func_rel_incl : forall A B, func A B \incl rel A B.

Lemma func_is_function : forall f A B, f \in func A B -> is_function f.

Lemma fun_domain_func : forall f A B, f \in func A B -> rel_domain f == A.

Lemma app_typ :
  forall f x A B, f \in func A B -> x \in A -> app f x \in B.

Lemma func_narrow : forall f A B B',
  f \in func A B ->
  (forall x, x \in A -> app f x \in B') ->
  f \in func A B'.

Definition lam_rel (F:set->set) A B := inject_rel (fun x y => F x == y) A B.

Lemma lam_rel_is_func : forall A B f,
  ext_fun A f ->
  (forall x, x \in A -> f x \in B) ->
  lam_rel f A B \in func A B.

Lemma beta_rel_eq : forall f x A B,
  ext_fun A f ->
  x \in A -> (forall x, x \in A -> f x \in B) -> app (lam_rel f A B) x == f x.

Definition lam A F := replf A (fun x => couple x (F x)).

Lemma fun_elt_is_ext : forall A f,
  ext_fun A f ->
  ext_fun A (fun x => couple x (f x)).
Hint Resolve fun_elt_is_ext.

Lemma lam_is_function : forall A f, ext_fun A f -> is_function (lam A f).

Lemma lam_is_func : forall A B f,
  ext_fun A f ->
  (forall x, x \in A -> f x \in B) ->
  lam A f \in func A B.

Lemma beta_eq : forall f x A,
  ext_fun A f -> x \in A -> app (lam A f) x == f x.

Definition dep_image (A:set) (B:set->set) := replf A B.

Lemma dep_image_ext :
  forall x1 x2 f1 f2,
  x1 == x2 ->
  eq_fun x1 f1 f2 ->
  dep_image x1 f1 == dep_image x2 f2.

Definition dep_func (A:set) (B:set->set) :=
  subset (func A (union (dep_image A B)))
    (fun f => forall x, x \in A -> app f x \in B x).

Lemma dep_func_ext :
  forall x1 x2 f1 f2,
  x1 == x2 ->
  eq_fun x1 f1 f2 ->
  dep_func x1 f1 == dep_func x2 f2.

Lemma dep_func_intro : forall f dom F,
  ext_fun dom f ->
  ext_fun dom F ->
  (forall x, x \in dom -> f x \in F x) ->
  lam dom f \in dep_func dom F.

Lemma func_eta : forall f A B,
  f \in func A B ->
  f == lam A (fun x => app f x).

Lemma dep_func_eta : forall f dom F,
  f \in dep_func dom F ->
  f == lam dom (fun x => app f x).

Lemma dep_func_incl_func : forall A B,
  dep_func A B \incl func A (union (dep_image A B)).

Lemma dep_func_elim :
  forall f x A B, f \in dep_func A B -> x \in A -> app f x \in B x.