``` ```

# Fundamental set theory

Original file by Carlos Simpson (CNRS/UNSA)

Copyright INRIA (2009) Apics Team (Jose Grimm).
``` Set Implicit Arguments. Require Export Arith. ```

## Axioms

``` Module Axioms. ```
Realisation: if `x` is a set, `Ro` maps an object of type `x` to a set
``` Parameter Ro : forall x : Set, x -> Set. ```
Injectivity of `Ro`
``` Axiom R_inj : forall (x : Set) (a b : x), Ro a = Ro b -> a = b. ```
Defines `inc` as "is element of" and `sub` as "is subset of"
``` Definition inc (x y : Set) := exists a : y, Ro a = x. Definition sub (a b : Set) := forall x : Set, inc x a -> inc x b. ```
Extensionality for sets
``` Axiom extensionality : forall a b : Set, sub a b -> sub b a -> a = b. ```
Extensionality for products
``` Axiom prod_extensionality :   forall (x : Type) (y : x -> Type) (u v : forall a : x, y a),     (forall a : x, u a = v a) -> u = v. Lemma arrow_extensionality :   forall (x y : Type) (u v : x -> y), (forall a : x, u a = v a) -> u = v. Proof. intros x y.   change (forall u v : forall a : x, (fun _ : x => y) a,       (forall a : x, u a = v a) -> u = v).   intros. apply prod_extensionality; assumption. Qed. ```
`nonempty`: type is populated, or set has an element.
``` Inductive nonemptyT (t : Type) : Prop :=     nonemptyT_intro : t -> nonemptyT t. Inductive nonempty (x : Set) : Prop :=     nonempty_intro : forall y : Set, inc y x -> nonempty x. ```
Axiom of choice: let `t` be a nonempty type, `p` a predicate on `t`. If `p` is true for some object it is for `(chooseT p ne)`.
``` Parameter chooseT : forall (t : Type) (p : t -> Prop)(q:nonemptyT t), t. Axiom chooseT_pr :   forall (t : Type) (p : t -> Prop) (q : nonemptyT t),     ex p -> p (chooseT p q). ```
Image: if `f:x->Set` is an abstraction, then `IM f` is a set, it contains `y` if and only if `y` is `(f z)` for some `z:x`.
``` Parameter IM : forall x : Set, (x -> Set) -> Set. Axiom IM_exists :           forall (x : Set) (f : x -> Set) (y : Set),           inc y (IM f) -> exists a : x, f a = y. Axiom IM_inc :           forall (x : Set) (f : x -> Set) (y : Set),           (exists a : x, f a = y) -> inc y (IM f). ```
Excluded middle and consequences.
``` Axiom excluded_middle : forall P : Prop, ~ ~ P -> P. Axiom iff_eq : forall P Q : Prop, (P -> Q) -> (Q -> P) -> P = Q. Lemma p_or_not_p : forall P : Prop, P \/ ~ P. Proof. intros. apply excluded_middle. intro. intuition. Qed. Lemma equal_or_not: forall x y:Set, x= y \/ x<> y. Proof. intros. apply p_or_not_p. Qed. Lemma inc_or_not: forall x y:Set, inc x y \/ ~ (inc x y). Proof. intros. apply p_or_not_p. Qed. End Axioms. Export Axioms. ```

## Tactics

``` Module Tactics1. ```
Shorthands, for instance `EEE = Set -> Set -> Set`.
``` Notation EE := (Set -> Set). Notation EEE := (Set -> EE). Notation EP := (Set -> Prop). Notation EEP := (Set -> EP). Infix "&":= and (right associativity, at level 100). Lemma seq_deconj : forall P Q : Prop, P -> (P -> Q) -> (P & Q).   intros P Q p H. split ; [idtac | apply H]; assumption. Qed. Lemma uneq : forall (f:EE) x y,   x = y -> f x = f y. Proof. intros f x y H. rewrite H. trivial. Qed. Lemma uneq2 : forall (f:EEE) x y x' y',   x = y -> x' = y' -> f x x' = f y y'. Proof. intros f x y x' y' H H'. rewrite H. rewrite H'. trivial. Qed. Ltac ir := intros. Ltac rw u := rewrite u. Ltac rwi u h := rewrite u in h. Ltac wr u := rewrite <- u. Ltac wri u h := rewrite <- u in h. Ltac ap h := apply h. Ltac am := assumption. Ltac tv := trivial. Ltac eau := eauto. Ltac sy := symmetry. Ltac uf u := unfold u. Ltac ufi u h := unfold u in h. Ltac nin h := induction h. Ltac int := intuition. Ltac app u := ap u; tv. Ltac apw u v := apply u with v ; tv. Ltac rww u := rw u; tv. Ltac rwii u h:= rwi u h; tv. Ltac wrii u h:= wri u h; tv. Ltac wrr u := wr u; tv. Ltac dneg := match goal with   H : ~ _ |- ~ _ => red; ir; elim H end. Ltac ex_middle := match goal with   | |- inc ?a ?b => nin (inc_or_not a b) ; tv   | |- ?a = ?b => nin (equal_or_not a b) ; tv end. ```
Tatics like `aw` use autorewite on the goal and try to solve; tactics like `awi` just rewrite in an assumption, tatics like `fprop` use auto
``` Ltac aw := autorewrite with aw; tv. Ltac awi u:= autorewrite with aw in u. Ltac awii u:= autorewrite with aw in u; tv. Ltac bw := autorewrite with bw; tv. Ltac bwi u:= autorewrite with bw in u. Ltac srw:= autorewrite with sw; tv. Ltac srwi u:= autorewrite with sw in u. Ltac fprops := auto with fprops. Ltac gprops := auto with gprops. Ltac au := first [ solve [am] | auto ]. Ltac set_extens:= app extensionality; unfold sub; intros. Ltac EasyDeconj :=   match goal with   | |- (_ & _) => ap conj; [ EasyDeconj | EasyDeconj ]   | |- _ => idtac   end. Ltac EasyExpand :=   match goal with   | id1:(?X1 /\ ?X2) |- _ => nin id1; EasyExpand   | |- _ => EasyDeconj   end. Ltac ee := EasyExpand. Ltac Remind u :=   set (recalx := u);    match goal with    | recalx:?X1 |- _ => assert X1; [ exact recalx | clear recalx ]    end. Ltac cp := Remind. Ltac Use_eq :=   match goal with     | H:?a = ?b |- ?f ?a = ?f ?b => rww H     | H:?a = ?b |- ?f ?a _ = ?f ?b _ => rww H     | H:?a = ?b |- ?f _ ?a = ?f _ ?b => rww H     | H:?a = ?b |- ?f ?a _ _ = ?f ?b _ _ => rww H     | H:?a = ?b |- ?f _ ?a _ = ?f _ ?b _ => rww H     | H:?a = ?b |- ?f _ _ ?a = ?f _ _ ?b => rww H     | H:?a = ?b |- _ => solve [ rww H ; fprops | wrr H ; fprops]     | Ha : ?a = ?c, Hb : ?b = ?c |- ?a = ?b => wr Ha ; wr Hb; tv     | H:?b = _ |- _ ?b => rww H     | H:?b = _ |- _ _ ?b => rww H     | H:?b = _ |- _ ?b _ => rww H     | H:?b = _ |- _ _ ?b _ => rww H     | H:?b = _ |- _ ?b _ _ => rww H     | H:?b = _ |- _ _ _ ?b => rww H end. Ltac ue := Use_eq. Ltac eee := ee ; tv; try ue; fprops. End Tactics1. Export Tactics1. ```

## Constructions

``` Module Constructions. ```
`exists_unique p` says there a unique `x` such that `(p x)`
``` Definition exists_unique t (p : t->Prop) :=   (ex p) & (forall x y : t, p x -> p y -> x = y). ```
Defines `strict_sub` as strict subset
``` Definition strict_sub (a b : Set) := (a <> b) & (sub a b). Lemma sub_trans : forall a b c, sub a b -> sub b c -> sub a c. Proof. uf sub; auto. Qed. Lemma sub_refl : forall x, sub x x. Proof. unfold sub; auto. Qed. Lemma strict_sub_trans1 :   forall a b c, strict_sub a b -> sub b c -> strict_sub a c. Proof. uf strict_sub. ir. nin H.   split. dneg. wri H2 H0. app extensionality. apw sub_trans b. Qed. Lemma strict_sub_trans2 :  forall a b c, sub a b -> strict_sub b c -> strict_sub a c. Proof. unfold strict_sub. ir. nin H0. split. dneg.   rwi H2 H. app extensionality. apw sub_trans b. Qed. ```
`emptyset` is a type without constructor; `empty` is classical.
``` Definition empty (x : Set) := forall y : Set, ~ inc y x. Inductive emptyset : Set :=. ```
Basic property of `Ro`.
``` Lemma R_inc : forall (x : Set) (a : x), inc (Ro a) x. Proof. ir. exists a; tv. Qed. ```
Equivalence between `nonempty` and `~ empty`.
``` Lemma inc_nonempty : forall x y, inc x y -> nonemptyT y. Proof. uf inc; ir; nin H; app nonemptyT_intro. Qed. Lemma nonemptyT_not_empty : forall x:Set, nonemptyT x -> ~ empty x. Proof. uf not. ir. nin H. ap (H0 (Ro H)(R_inc H)). Qed. Lemma nonemptyT_not_empty0 : forall x:Set, nonemptyT x = nonempty x. Proof. ir. ap iff_eq; ir; nin H. exists (Ro H). exists H. tv.   ap (inc_nonempty H). Qed. Lemma emptyset_pr: forall x, ~ inc x emptyset. Proof. ir. red. ir. nin H. elim x0. Qed. Lemma is_emptyset: forall x, (forall y, ~ (inc y x)) -> x = emptyset. Proof. ir. set_extens. elim (H x0). am. elim (emptyset_pr H0). Qed. Ltac empty_tac :=   match goal with   | |- _ = emptyset => ap is_emptyset; red;ir; idtac   | H:inc _ emptyset |- _ => elim (emptyset_pr H)   | _ => idtac   end. Ltac empty_tac1 u := elim (emptyset_pr (x:= u));   match goal with H: ?x = emptyset |- _ => wr H     | H: emptyset = ?x |- _ => rw H end ; fprops. Lemma emptyset_sub_any:   forall x, sub emptyset x. Proof. ir. red. ir. empty_tac. Qed. ```
Axiom of choice applied to `(inc x y)`, and the property `(P a)` that says realisation of `a` is `x`. This gives a partial inverse of `Ro` and more properties of the emptyset.
``` Definition Bo (x y : Set) (hyp : inc x y) :=   chooseT (fun a : y => Ro a = x) (inc_nonempty hyp). Lemma B_eq : forall x y (hyp : inc x y), Ro (Bo hyp) = x. Proof. uf inc; uf Bo. ir. app chooseT_pr. Qed. Lemma B_back : forall (x:Set) (y:x) (hyp : inc (Ro y) x), Bo hyp = y. Proof. ir. ap R_inj. ap B_eq. Qed. Lemma not_empty_nonemptyT : forall x , ~ empty x -> nonemptyT x. Proof. ir. nin (p_or_not_p (nonemptyT x)). am. elim H.   red. ir. dneg. ap (nonemptyT_intro (Bo H1)). Qed. Lemma emptyset_dichot : forall x, (x = emptyset \/ nonempty x). Proof. ir. nin (p_or_not_p (nonempty x)). au. left. empty_tac.   elim H. exists y. am. Qed. ```
Let `T` be a type, `P` a proposition, `a` a function that maps a proof of `P` into `T` and `b` a function that maps a proof of `~P` into `T`. Let `q x` the property that `a p =x` and `b q = x`. We show that there exists `x` with this property
``` Lemma by_cases_nonempty :  forall (T : Type) (P : Prop) (a : P -> T) (b : ~ P -> T), nonemptyT T. Proof. ir. nin (p_or_not_p P); ap nonemptyT_intro; [ app a | app b]. Qed. ```
We can apply the axiom of choice. We have 4 lemmas: fundamental property, uniqueness, case where P is true, case where P is false.
``` Definition by_cases (T : Type) (P : Prop) (a : P -> T) (b : ~ P -> T) :=   chooseT (fun x : T => (forall p : P, a p = x)                        & (forall q : ~ P, b q = x))     (by_cases_nonempty a b). Lemma by_cases_if :   forall (T : Type) (P : Prop) (a : P -> T) (b : ~ P -> T) (p : P),     (forall p1 p2: P, a p1 = a p2) ->     by_cases a b = a p. Proof. ir.   assert ((forall p , a p = (by_cases a b))     & (forall q, b q = (by_cases a b))).   uf by_cases. app chooseT_pr. exists (a p). split. ir. app H.   ir. contradiction. nin H0. sy. app H0. Qed. Lemma by_cases_if_not :   forall (T : Type) (P : Prop) (a : P -> T) (b : ~ P -> T) (q : ~ P),     (forall p1 p2: ~P, b p1 = b p2) ->     by_cases a b = b q. Proof. ir. assert ((forall p : P, a p = (by_cases a b))   & (forall q : ~ P, b q = (by_cases a b))). uf by_cases.   app chooseT_pr. exists (b q). split. ir. contradiction.   ir. app H. nin H0. sy. app H1. Qed. ```
Genereralised axiom of choice. `choose p` is satisfied by `p` if somebody satisfies `p`, is the emptyset otherwise
``` Definition choose (p:EP) :=   chooseT (fun x => (ex p -> p x) & ~ ex p -> x = emptyset)   (nonemptyT_intro emptyset). Lemma choose_pr : forall p, ex p -> p (choose p). Proof. ir. unfold choose. assert (H0:=H).   set (q:= fun x => ex p -> p x & ~ ex p -> x = emptyset).   assert (q (chooseT q (nonemptyT_intro emptyset))). app chooseT_pr.   nin H. exists x. uf q. split;ir. am. contradiction. nin H1. app H1. Qed. Lemma choose_not : forall p, ~(ex p) -> choose p = emptyset. Proof. ir. unfold choose. cp H.   set (q:= fun x => ex p -> p x & ~ ex p -> x = emptyset).   assert (q (chooseT q (nonemptyT_intro emptyset))). app chooseT_pr.   exists emptyset. uf q. split;ir. contradiction. tv. nin H1. app H2. Qed. Lemma arrow_EP_exten: forall (p q: EP),   (forall x, p x <-> q x) -> p = q. Proof. ir. app arrow_extensionality. ir. nin (H a). app iff_eq. Qed. Lemma choose_equiv: forall (p q: EP),   (forall x, p x <-> q x) -> choose p = choose q. Proof. ir. rww (arrow_EP_exten _ _ H). Qed. Definition choosenat p :=   chooseT (fun u => (ex p -> p u) & ~ ex p -> u = 0) (nonemptyT_intro 0). Lemma choosenat_pr : forall p, (ex p) -> p (choosenat p). Proof. ir. unfold choosenat.   set(q:= fun u : nat => ex p -> p u & ~ ex p -> u = 0).   assert (q (chooseT q (nonemptyT_intro 0))). app chooseT_pr.   cp H. nin H. exists x. uf q. split. auto. ir. contradiction. red in H0.   ee. app H0. Qed. ```
Axiom of choice applied to `inc`. If `x` not empty, `rep x` is in `x`.
``` Definition rep (x : Set) := choose (fun y : Set => inc y x). Lemma nonempty_rep : forall x, nonempty x -> inc (rep x) x. Proof. ir. unfold rep. nin H. ap choose_pr. exists y. am. Qed. ```
The negation of `forall x`, `~ (p x)` is the existence of `x` with `(p x)`.
``` Lemma exists_proof : forall p : EP, ~ (forall x : Set, ~ p x) -> ex p. Proof. ir. nin (p_or_not_p (ex p)). am. elim H. ir. dneg. exists x. am. Qed. Lemma not_exists_pr : forall p : EP, (~ ex p) = (forall x : Set, ~ p x). Proof. ir. ap iff_eq; ir; intro H1. elim H. exists x; am.   nin H1. apw H x. Qed. ```
Defines `Y P x y` to `x` if P is true and `y` otherwise
``` Definition Yo : Prop -> EEE :=   fun P x y => by_cases (fun _ : P => x) (fun _ : ~ P => y). Lemma Y_if : forall (P : Prop) (hyp : P) x y z, x = z -> Yo P x y = z. Proof. ir. unfold Yo. wr H. set (a := fun _:P => x).   change (by_cases a (fun _ : ~ P => y) = a hyp). app by_cases_if. Qed. Lemma Y_if_not :   forall (P : Prop) (hyp : ~ P) x y z, y = z -> Yo P x z = y. Proof. ir. unfold Yo. set (b := fun _: ~ P => z). rw H.   change (by_cases (fun _ : P => x) b = b hyp). app by_cases_if_not. Qed. Lemma Y_if_rw : forall (P:Prop) (hyp :P) x y, Yo P x y = x. Proof. intros. app Y_if. Qed. Lemma Y_if_not_rw : forall (P:Prop) (hyp : ~P) x y, Yo P x y = y. Proof. intros. app Y_if_not. Qed. Definition Yt (A:Type): Prop -> (A->A->A):=   fun P x y => by_cases (fun _ : P => x) (fun _ : ~ P => y). Lemma Yt_if_rw : forall (A:Type)(P : Prop) (hyp : P) (x:A) y,   Yt P x y = x. Proof. ir. unfold Yt. set (a := fun _:P => x).   change (by_cases a (fun _ : ~ P => y) = a hyp). app by_cases_if. Qed. Lemma Yt_if_not_rw : forall (A:Type) (P : Prop) (hyp : ~ P) x (y:A),   Yt P x y = y. Proof. ir. unfold Yt. set (b := fun _: ~ P => y).   change (by_cases (fun _ : P => x) b = b hyp). app by_cases_if_not. Qed. ```
Given a function f, `Zorec` remembers a and f(a)
``` Inductive Zorec (x : Set) (f : x -> Prop) : Set :=   Zorec_c :forall (a: x), f a -> Zorec f. ```
`Zo x p` is the image of some function `g`; this means that `inc y (Zo x p)` if and only if `y = (g t)` for some `t`; `t` is a record, say it remembers `a` of type `x`, and `p (Ro a)` holds; `g(t)` is `Ro a`. Thus `inc y x` and `p y`. The converse is true.
``` Definition Zo (x:Set) (p:EP) :=   IM (fun (z : Zorec (fun (a : x) => p (Ro a))) => let (a, _) := z in Ro a). Lemma Z_inc : forall x (p: EP) y, inc y x -> p y -> inc y (Zo x p). Proof. ir. unfold Zo. ap IM_inc. nin H. wri H H0.   exists (Zorec_c (fun a : x => p (Ro a)) x0 H0). tv. Qed. Lemma Z_sub : forall x p, sub (Zo x p) x. Proof. ir. red. ir. nin (IM_exists H). wr H0. nin x1. apply R_inc. Qed. Lemma Z_all : forall x p y, inc y (Zo x p) -> (inc y x & p y). Proof. ir. nin (IM_exists H). wr H0. nin x0. split. ap R_inc. am. Qed. Ltac Ztac :=   match goal with     | id1:(inc _ (Zo _ _)) |- inc _ (Zo _ _ )       => nin (Z_all id1) ; ap Z_inc; auto     | id1:(inc _ (Zo _ _)) |- _ => nin (Z_all id1)     | |- (inc _ (Zo _ _)) => ap Z_inc; auto     | _ => idtac   end. Definition Yy : forall P : Prop, (P -> Set) -> EE :=   fun P f x => by_cases f (fun _ : ~ P => x). Lemma Yy_if :  forall (P : Prop) (hyp : P) (f : P -> Set) x z,    (forall p1 p2: P, f p1 = f p2) ->    f hyp = z -> Yy f x = z. Proof. ir. unfold Yy. wr H0. app by_cases_if. Qed. Lemma Yy_if_not :   forall (P : Prop) (hyp : ~ P) (f : P -> Set) (x z : Set), x = z -> Yy f x = z. Proof. ir. unfold Yy. set (b := fun _: ~ P => x). wr H.   change (by_cases f b = b hyp). app by_cases_if_not. Qed. ```
Defines `Xo f y`, where `f` is defined for objects of type `x` as: `(f z)` if `inc y x`, and `z` expresses this, the emptyset otherwise.
``` Definition Xo (x : Set) (f : x -> Set) (y : Set) :=   Yy (fun hyp : inc y x => f (Bo hyp)) emptyset. Lemma X_eq :   forall (x : Set) (f : x -> Set) (y z : Set),     (exists a : x, (Ro a = y) & (f a = z)) -> Xo f y = z. Proof. ir. induction H. unfold Xo. nin H. symmetry in H.   assert (inc y x). rw H. apply R_inc.   apply Yy_if with H1. ir.   assert (Bo p1 = x0). apply R_inj. rww B_eq. rw H2.   assert (Bo p2 = x0). apply R_inj. rww B_eq. sy;ue.   assert (Bo H1 = x0). apply R_inj. rww B_eq. rww H2. Qed. Lemma X_rewrite : forall (x : Set) (f : x -> Set) (a : x), Xo f (Ro a) = f a. Proof. ir. apply X_eq. exists a. auto. Qed. ```
Set of all elements of `x` satisfying `p`
``` Definition cut (x : Set) (p : x -> Prop) :=   Zo x (fun y : Set => forall hyp : inc y x, p (Bo hyp)). Lemma cut_sub : forall (x : Set) (p : x -> Prop), sub (cut p) x. Proof. ir. unfold cut. apply Z_sub. Qed. Definition cut_to (x : Set) (p : x -> Prop) (y : cut p) :=   Bo (cut_sub (p:=p) (R_inc y)). Lemma cut_to_R_eq :  forall (x : Set) (p : x -> Prop) (y : cut p), Ro (cut_to y) = Ro y. Proof. ir. unfold cut_to. rww B_eq. Qed. Lemma cut_pr : forall (x : Set) (p : x -> Prop) (y : cut p), p (cut_to y). Proof. ir. unfold cut_to. ufi cut y.   set (R_inc y). Ztac. ap H0. Qed. Lemma cut_inc :  forall (x : Set) (p : x -> Prop) (y : x), p y -> inc (Ro y) (cut p). Proof. ir. unfold cut. Ztac. ap R_inc.   ir. assert (Bo hyp = y). ap R_inj. ap B_eq. ue. Qed. End Constructions. Export Constructions. ```

## Little

``` Module Little. ```
`singleton`: image of a set with one point
``` Inductive one_point : Set :=     one_point_intro. Definition singleton (x : Set) := IM (fun p : one_point => x). Lemma singleton_inc : forall x, inc x (singleton x). Proof. ir. uf singleton. ap IM_inc. exists one_point_intro. tv. Qed. Hint Resolve sub_refl singleton_inc: fprops. Lemma singleton_eq : forall x y, inc y (singleton x) -> y = x. Proof. ir. sy. nin (IM_exists H). am. Qed. Lemma singleton_rw: forall x y, inc y (singleton x) = (y = x). Proof. ir. ap iff_eq. ir. ap (singleton_eq H). ir. rw H. fprops. Qed. Hint Rewrite singleton_rw: aw. Lemma singleton_inj : forall x y, singleton x = singleton y -> x = y. Proof. ir. assert (inc x (singleton y)). wr H. fprops. app singleton_eq. Qed. Lemma nonempty_singleton: forall x, nonempty (singleton x). Proof. ir. exists x. fprops. Qed. Lemma sub_singleton: forall x y,   inc x y -> sub (singleton x) y. Proof. ir. red. ir. rww (singleton_eq H0). Qed. ```
doubleton: image of a set with two points
``` Inductive two_points : Set :=   | two_points_a | two_points_b. Definition TPa := Ro two_points_a. Definition TPb := Ro two_points_b. Lemma two_points_pr: forall x,   inc x two_points = (x= TPa \/ x = TPb). Proof. ir. uf TPa; uf TPb. ap iff_eq.   ir. nin H; wr H. elim x0; auto.   ir. nin H; rw H;app R_inc. Qed. Lemma two_points_distinct: TPa <> TPb. Proof. red. ir. set (R_inj H). discriminate e. Qed. Lemma two_points_distinctb: TPb <> TPa. Proof. red. ir. set (R_inj H). discriminate e. Qed. Lemma inc_TPa_two_points: inc TPa two_points. Proof. uf TPa. app R_inc. Qed. Lemma inc_TPb_two_points: inc TPb two_points. Proof. uf TPb. app R_inc. Qed. Definition doubleton (x y : Set) :=   IM (fun t => two_points_rect (fun _ : two_points => Set) x y t). Lemma doubleton_first : forall x y, inc x (doubleton x y). Proof. ir. uf doubleton. ap IM_inc. exists two_points_a. tv. Qed. Lemma doubleton_second : forall x y : Set, inc y (doubleton x y). Proof. ir. uf doubleton. ap IM_inc. exists two_points_b. tv. Qed. Lemma doubleton_or :  forall x y z : Set, inc z (doubleton x y) -> z = x \/ z = y. Proof. ir. nin (IM_exists H). nin x0; intuition. Qed. Hint Resolve doubleton_first doubleton_second inc_TPa_two_points inc_TPb_two_points: fprops. Ltac db_tac :=  match goal with     | H: inc _ (doubleton _ _ ) |- _ => nin (doubleton_or H); ue     | H: inc _ (singleton _ ) |- _ => rwi singleton_rw H; ue end. Lemma doubleton_rw : forall x y z : Set,   inc z (doubleton x y) = (z = x \/ z = y). Proof. ir. ap iff_eq. app doubleton_or. ir. nin H; rw H; fprops. Qed. Lemma two_points_pr2: doubleton TPa TPb = two_points. Proof. set_extens. rw two_points_pr. app doubleton_or.   rwi two_points_pr H. nin H; rw H; fprops. Qed. Lemma doubleton_inj : forall x y z w,   doubleton x y = doubleton z w -> (x = z & y = w) \/ (x = w & y = z). Proof. ir.   assert (inc x (doubleton z w)). wr H; fprops.   assert (inc y (doubleton z w)). wr H; fprops.   assert (inc w (doubleton x y)). rw H; fprops.   assert (inc z (doubleton x y)). rw H; fprops.   nin (doubleton_or H0). left. split. am.   nin (doubleton_or H2). nin (doubleton_or H1). rw H5; rw H4; am. am. auto.   right. split. am. nin (doubleton_or H1). am. sy.   wri H4 H5. nin (doubleton_or H3). rww H5. am. Qed. Lemma doubleton_singleton : forall x, doubleton x x = singleton x. Proof. ir. set_extens; db_tac. Qed. Lemma nonempty_doubleton: forall x y, nonempty (doubleton x y). Proof. ir. exists x. fprops. Qed. Lemma sub_doubleton: forall x y z,   inc x z -> inc y z -> sub (doubleton x y) z. Proof. ir. red. ir. db_tac. Qed. Lemma doubleton_symm: forall a b,   doubleton a b = doubleton b a. Proof. ir. set_extens; db_tac. Qed. End Little. Export Little. ```

## Complement

``` Module Complement. ```
Set of all elements in a not in b
``` Definition complement (a b : Set) := Zo a (fun x : Set => ~ inc x b). Lemma inc_complement :   forall a b x, inc x (complement a b) = (inc x a & ~ inc x b). Proof. ir. uf complement. ap iff_eq; ir. Ztac. au. ee. Ztac. Qed. Hint Rewrite inc_complement: sw. Lemma use_complement :   forall a b x, inc x a -> ~ inc x (complement a b) -> inc x b. Proof. ir. ex_middle. elim H0. srw. auto. Qed. Lemma sub_complement: forall a b, sub (complement a b) a. Proof. ir. uf sub; ir. srwi H; eee. Qed. Lemma empty_complement: forall a b,   complement a b = emptyset -> sub a b. Proof. ir. red. ir. app (@use_complement a b x). rw H. app emptyset_pr. Qed. Lemma strict_sub_nonempty_complement : forall x y,   strict_sub x y -> nonempty (complement y x). Proof. ir. nin H. nin (emptyset_dichot (complement y x)).   elim H. app extensionality. app empty_complement. am. Qed. Lemma double_complement: forall a x,   sub a x -> complement x (complement x a) = a. Proof. ir. set_extens. srwi H0. ee. ex_middle. elim H1.   auto. srw. ee. app H. red. ir. ee. app H2. Qed. Hint Rewrite double_complement: sw. Lemma complement_itself : forall x,   complement x x = emptyset. Proof. ir. empty_tac. srwi H. intuition. Qed. Lemma complement_emptyset : forall x,   complement x emptyset = x. Proof. ir. set_extens. srwi H. intuition. srw. split. am. ap emptyset_pr. Qed. Lemma not_inc_complement_singleton: forall a b,   ~ (inc b (complement a (singleton b))). Proof. ir. red. ir. srwi H. nin H. elim H0. fprops. Qed. Lemma complement_monotone : forall a b x,   sub a x -> sub b x -> (sub a b = sub (complement x b) (complement x a)). Proof. ir. ap iff_eq. ir. red. ir. srw. srwi H2.   ee. am. dneg. app H1.   ir. red. ir. nin (inc_or_not x0 (complement x b)).   cp (H1 _ H3). srwi H4. ee. intuition.   cp (H _ H2). app (use_complement H4 H3). Qed. End Complement. Export Complement. ```

## Image

``` Module Image. ```
Image of a set by a function
``` Definition fun_image (x : Set) (f : EE) := IM (fun a : x => f (Ro a)). Lemma inc_fun_image : forall x f a, inc a x -> inc (f a) (fun_image x f). Proof. ir. uf fun_image. ap IM_inc. exists (Bo H). rww (B_eq H). Qed. Lemma fun_image_rw : forall f x y,   inc y (fun_image x f) = exists z, (inc z x & f z = y). Proof. ir. ap iff_eq; intros.   nin (IM_exists H). exists (Ro x0). split. app R_inc. tv.   induction H. induction H. wr H0. app inc_fun_image. Qed. Hint Rewrite fun_image_rw : aw. End Image. Export Image. ```

## Powerset

``` Module Powerset. ```
This is the set of all cuts, but in fact is the set of all subsets
``` Definition powerset (x : Set) :=   IM (fun p : x -> two_points =>     Zo x (fun y : Set => forall hyp : inc y x, p (Bo hyp) = two_points_a)). Lemma powerset_inc : forall x y, sub x y -> inc x (powerset y). Proof. ir. uf powerset. ap IM_inc.   exists (fun b:y =>by_cases (fun _:inc (Ro b) x => two_points_a)     (fun _:~inc (Ro b) x => two_points_b)).   set_extens. Ztac. set (H2 H1). ex_middle.   rwi by_cases_if_not e. discriminate e. rww B_eq. ir. tv.   Ztac. ir. rww by_cases_if. rww B_eq. Qed. Lemma powerset_sub : forall x y, inc x (powerset y) -> sub x y. Proof. ir. ufi powerset H. nin (IM_exists H). wr H0. app Z_sub. Qed. Lemma powerset_inc_rw : forall x y, inc x (powerset y) = sub x y. Proof. ir. apply iff_eq; ir. app powerset_sub. app powerset_inc. Qed. Hint Rewrite powerset_inc_rw : aw. Lemma inc_x_powerset_x: forall x, inc x (powerset x). Proof. ir. aw. red; tv. Qed. End Powerset. Export Powerset. ```

## Union

``` Module Union. ```
Integral: records `p` and `e`. Pose `q = Ro p`. By definition, `inc q x`.
``` Record Union_integral (x : Set) : Set :=   {Union_param : x; Union_elt : Ro Union_param}. ```
Union: `y` is in the union if `y= Ro e` for some `e`, this is `inc y q`, q defined above
``` Definition union (x : Set) :=   IM (fun i : Union_integral x => Ro (Union_elt i)). Lemma union_inc : forall x y a, inc x y -> inc y a -> inc x (union a). Proof. ir. set (w:= Bo H0). assert (Ro w = y). uf w; ap B_eq.   assert (inc x (Ro w)). rww H1. uf union. ap IM_inc.   exists (Build_Union_integral (Bo H2)). simpl. apply B_eq. Qed. Lemma union_exists : forall x a,     inc x (union a) -> exists y, inc x y & inc y a. Proof. ir. ufi union H. nin (IM_exists H).   exists (Ro (Union_param x0)). wr H0. split. ap R_inc. ap R_inc. Qed. Lemma union_sub: forall x y, inc x y -> sub x (union y). Proof. ir. red. ir. apply union_inc with x. am. am. Qed. ```
Union of two sets
``` Definition union2 (x y : Set) := union (doubleton x y). Lemma union2_or : forall x y a, inc a (union2 x y) -> inc a x \/ inc a y. Proof. ir. ufi union2 H. nin (union_exists H). nin H0.   nin (doubleton_or H1) ; [ left | right ] ; wrr H2. Qed. Lemma union2_first : forall x y a, inc a x -> inc a (union2 x y). Proof. ir. uf union2. apw union_inc x. fprops. Qed. Lemma union2_second : forall x y a, inc a y -> inc a (union2 x y). Proof. ir. uf union2. apw union_inc y. fprops. Qed. Lemma inc_union2_rw : forall a b x,   inc x (union2 a b) = (inc x a \/ inc x b). Proof. ir. apply iff_eq; ir. app union2_or.   induction H; [app union2_first | app union2_second]. Qed. Lemma union2sub_first: forall a b, sub a (union2 a b). Proof. red. ir. app union2_first. Qed. Lemma union2sub_second: forall a b, sub b (union2 a b). Proof. red. ir. app union2_second. Qed. ```
Union of `x` and a single element
``` Definition tack_on x y := union2 x (singleton y). Lemma tack_on_or : forall x y z, inc z (tack_on x y) ->   (inc z x \/ z = y). Proof. ir. ufi tack_on H. set (H1:= union2_or H).   induction H1; [ left | right; awi H0]; assumption. Qed. Lemma tack_on_inc: forall x y z,   (inc z (tack_on x y) ) = (inc z x \/ z = y). Proof. ir. ap iff_eq. ap tack_on_or. ir.   uf tack_on. induction H. app union2_first.   ap union2_second. wr H. fprops. Qed. Hint Rewrite tack_on_inc : aw. Lemma inc_tack_on_x: forall a b, inc a (tack_on b a). Proof. ir. aw. au. Qed. Lemma inc_tack_on_sub: forall a b, sub b (tack_on b a). Proof. ir. red. ir. aw. au. Qed. Lemma inc_tack_on_y: forall a b y, inc y b -> inc y (tack_on b a). Proof. ir. aw. au. Qed. Hint Resolve inc_tack_on_x inc_tack_on_y inc_tack_on_sub: fprops. Lemma tack_on_when_inc: forall x y, inc y x -> tack_on x y = x. Proof. ir. set_extens. awi H0. nin H0. am. ue. fprops. Qed. Lemma tack_on_sub: forall x y z, sub x z -> inc y z -> sub (tack_on x y) z. Proof. ir. red. ir. awi H1. nin H1. app H. ue. Qed. Lemma tack_on_complement: forall x y, inc y x ->   x = tack_on (complement x (singleton y)) y. Proof. ir. set_extens. nin (equal_or_not x0 y). rw H1. fprops. aw. left. srw.   split. am. dneg. awi H2. am.   awi H0. nin H0. srwi H0. nin H0. am. ue. Qed. Lemma sub_union : forall x z,   (forall y, inc y z -> sub y x) -> sub (union z) x. Proof. ir. red; ir. nin (union_exists H0). ee. app (H _ H2). Qed. Lemma union2idem: forall x, union2 x x = x. Proof. ir. set_extens. nin (union2_or H). am. am. app union2_first. Qed. Lemma union2comm: forall x y, union2 x y = union2 y x. Proof. ir. set_extens ;   (nin (union2_or H); [app union2_second | app union2_first]). Qed. Lemma union2_sub: forall x y,   sub x y = (union2 x y = y). Proof. ir. app iff_eq. ir. set_extens. nin (union2_or H0). app H. am.   app union2_second. ir. red. ir. wr H. app union2_first. Qed. End Union. Export Union. ```

## Intersection

``` Module Intersection. ```
Intersection: set of all `z` in `rep x`, that are in all elements of `x`; `rep x` is some element of `x`, its value is irrelevant, it exists if `x` nonempty
``` Definition intersection (x : Set) :=   Zo (union x) (fun y : Set => forall z : Set, inc z x -> inc y z). Lemma intersection_inc : forall x a,   nonempty x -> (forall y, inc y x -> inc a y) -> inc a (intersection x). Proof. ir. uf intersection. app Z_inc. nin H. apw union_inc y. app H0. Qed. Lemma intersection_forall :  forall x a y, inc a (intersection x) -> inc y x -> inc a y. Proof. ir. ufi intersection H. Ztac. app H2. Qed. Lemma intersection_sub : forall x y, inc y x -> sub (intersection x) y. Proof. ir. uf sub. ir. apw intersection_forall x. Qed. ```
Intersection of two sets
``` Definition intersection2 x y := intersection (doubleton x y). Lemma intersection2_inc :  forall x y a, inc a x -> inc a y -> inc a (intersection2 x y). Proof. ir. uf intersection2. ap intersection_inc. app nonempty_doubleton.   ir. set (H4:=doubleton_or H1). destruct H4 as [H5 | H6]; [rww H5|rww H6]. Qed. Lemma intersection2_first :  forall x y a, inc a (intersection2 x y) -> inc a x. Proof. ir. ufi intersection2 H.   apw intersection_forall (doubleton x y). fprops. Qed. Lemma intersection2_second :  forall x y a, inc a (intersection2 x y) -> inc a y. Proof. ir. ufi intersection2 H.   apw intersection_forall (doubleton x y). fprops. Qed. Lemma intersection2_both: forall x y a,   inc a (intersection2 x y) -> (inc a x & inc a y). Proof. ir. split. app (intersection2_first H). app (intersection2_second H). Qed. Lemma intersection2sub_first: forall a b, sub (intersection2 a b) a. Proof. red. ir. app (intersection2_first H). Qed. Lemma intersection2sub_second: forall a b, sub (intersection2 a b) b. Proof. red. ir. app (intersection2_second H). Qed. Lemma intersection2idem: forall x, intersection2 x x = x. Proof. ir. set_extens. app (intersection2_first H). app intersection2_inc. Qed. Lemma intersection2comm: forall x y, intersection2 x y = intersection2 y x. Proof. ir. set_extens ;   (app intersection2_inc; [app (intersection2_second H) | app (intersection2_first H)]). Qed. Lemma intersection2_sub: forall x y,   sub x y = (intersection2 x y = x). Proof. ir. app iff_eq. ir. set_extens. app (intersection2_first H0).   app intersection2_inc. ir. app H. red. ir. wri H H0.   app (intersection2_second H0). Qed. End Intersection. Export Intersection. ```

## Pair

``` Module Pair. ```
The object `(J x y)` is a set from which `x` and `y` can be recovered. Bourbaki (English edition) uses an axiom; he uses a doubleton in the French version; we use here another doubleton.
``` Definition kpair x y := doubleton (singleton x) (doubleton x y). Definition kpr1 x := union (intersection x). Definition kpr2 x := let a := complement (union x) (intersection x) in  Yo (a = emptyset) (kpr1 x) (union a). Lemma kpr0_pair:forall x y, intersection (kpair x y) = singleton x. Proof. ir. uf kpr1. assert (inc (singleton x) (kpair x y)). uf kpair.   fprops. set_extens. ap (intersection_forall H0 H).   app intersection_inc. exists (singleton x). am. ir. ufi kpair H1.   nin (doubleton_or H1). ue. awi H0. rw H0. ue. Qed. Lemma kpr1_pair: forall x y, kpr1 (kpair x y) = x. Proof. ir. uf kpr1. rw kpr0_pair. wr doubleton_singleton. ap (union2idem x). Qed. Lemma kpr2_pair: forall x y, kpr2 (kpair x y) = y. Proof. ir. uf kpr2. rw kpr0_pair.   assert (union (kpair x y) = doubleton x y). uf kpair. set_extens.   nin (union_exists H). nin H0. nin (doubleton_or H1). rwi H2 H0. awi H0. ue.   rwi H2 H0. am. apw union_inc (doubleton x y). fprops. rw H.   nin (equal_or_not x y). wr H0. rw doubleton_singleton. rw Y_if_rw.   app kpr1_pair. rww complement_itself.   assert (complement (doubleton x y) (singleton x) = singleton y). set_extens.   srwi H1. nin H1. nin (doubleton_or H1). awi H2. contradiction. ue.   srw. awi H1. rw H1. split. fprops. aw. int. rw H1.   rw Y_if_not_rw. wr doubleton_singleton. ap (union2idem y). red. ir.   empty_tac1 (y). Qed. Lemma kpr1_def : forall a b c d, kpair a b = kpair c d -> a = c. Proof. ir. transitivity (kpr1 (kpair a b)). rww kpr1_pair. rw H. rww kpr1_pair. Qed. Lemma kpr2_def : forall a b c d, kpair a b = kpair c d -> b = d. Proof. ir. transitivity (kpr2 (kpair a b)). rww kpr2_pair. rw H. rww kpr2_pair. Qed. Definition is_kpair (u : Set) := exists x, exists y, u = kpair x y. Lemma kpair_recov : forall u, is_kpair u -> kpair (kpr1 u) (kpr2 u) = u. Proof. uf is_kpair. ir. nin H. nin H. rw H. rww kpr1_pair. rww kpr2_pair. Qed. Lemma pair_is_kpair : forall x y : Set, is_kpair (kpair x y). Proof. uf is_kpair. ir. exists x. exists y. tv. Qed. Parameter pair_constructor : Set -> Set -> Set. Notation J := pair_constructor. Axiom axiom_of_pair : forall x y x' y' : Set,   (J x y = J x' y') -> (x = x' & y = y'). Definition is_pair (u : Set) := exists x, exists y, u = J x y. Definition pair_first (x y:Set):= singleton x. Definition pair_second (x y:Set):= doubleton emptyset (singleton y). Definition bpair_x (x y : Set) :=   doubleton (pair_first x y) (pair_second x y). Lemma pair_distincta:forall x y z w,   pair_first x y <> pair_second z w. Proof. ir. uf pair_first ; uf pair_second. red. ir.   assert (inc emptyset (singleton x)). rw H. fprops. awi H0.   assert (inc (singleton w) (singleton x)). rw H. fprops. awi H1.   empty_tac1 w. wr H1. fprops. Qed. Lemma pair_distinct:forall x y,   pair_second x y <> pair_first x y. Proof. ir. red. ir. symmetry in H. app (pair_distincta H). Qed. Lemma pr1_injective_x : forall x y z w : Set,   bpair_x x y = bpair_x z w -> x = z. Proof. ir. assert (pair_first x y = pair_first z w).   assert (inc (pair_first x y) (bpair_x z w)). wr H. uf bpair_x. fprops.   ufi bpair_x H0. db_tac. elim (pair_distincta H1).   ufi pair_first H0. app singleton_inj. Qed. Lemma pr2_injective_x : forall x y z w,   bpair_x x y = bpair_x z w -> y = w. Proof. ir. assert (pair_second x y = pair_second z w).   assert (inc (pair_second x y) (bpair_x z w)). wr H. uf bpair_x. fprops.   ufi bpair_x H0. db_tac.   symmetry in H1. elim (pair_distincta H1). ufi pair_second H0.   assert (inc (singleton y) (doubleton emptyset (singleton w))). wrr H0.   fprops. nin (doubleton_or H1).   assert (inc y emptyset). wr H2. fprops. nin H3. elim x0. app singleton_inj. Qed. Lemma pr1_def : forall x y z w : Set,   J x y = J z w -> x = z. Proof. ir. nin (axiom_of_pair H). am. Qed. Lemma pr2_def : forall x y z w,   J x y = J z w -> y = w. Proof. ir. nin (axiom_of_pair H). am. Qed. ```
First and second projections, `pr1` and `pr2`, denoted `P` and `Q`
``` Definition P (u : Set) :=   choose (fun x : Set => exists y : Set, u = J x y). Definition Q (u : Set) :=   choose (fun y : Set => exists x : Set, u = J x y). Lemma pair_recov : forall u, is_pair u -> J (P u) (Q u) = u. Proof. uf is_pair. ir.   assert (exists y : Set, exists x : Set, u = J x y). nin H; nin H.   exists x0. exists x. am. nin (choose_pr H). nin (choose_pr H0).   assert (u = J (P u) x). am. assert (u = J x0 (Q u)). am.   assert (J (P u) x = J x0 (Q u)). wrr H3. rw (pr1_def H5). sy; am. Qed. Lemma pair_is_pair : forall x y : Set, is_pair (J x y). Proof. uf is_pair. ir. exists x. exists y. tv. Qed. Hint Resolve pair_is_pair: fprops. Hint Rewrite pair_recov : aw. Lemma is_pair_rw : forall x, is_pair x = (x = J (P x) (Q x)). Proof. ir. ap iff_eq;ir. sy. aw. rw H. fprops. Qed. Lemma pr1_pair : forall x y, P (J x y) = x. Proof. ir. cp (pair_is_pair x y). rwi is_pair_rw H. sy. ap (pr1_def H). Qed. Lemma pr2_pair : forall x y, Q (J x y) = y. Proof. ir. cp (pair_is_pair x y). rwi is_pair_rw H. sy. ap (pr2_def H). Qed. Hint Rewrite pr1_pair pr2_pair : aw. Lemma pair_extensionality : forall a b,   is_pair a -> is_pair b -> P a = P b -> Q a = Q b -> a = b. Proof. ir. transitivity (J (P a) (Q a)). sy. aw. rw H1. rw H2. aw. Qed. ```
`V x f` is the value of `x` by a graph `f`; if there is a `z` such that `J x z` is in `f`, then `V` chooses one, otherwise it is the empty set.
``` Definition V (x f : Set) := choose (fun y : Set => inc (J x y) f). Lemma V_inc : forall x z f,   (exists y, inc (J x y) f) -> z = V x f -> inc (J x z) f. Proof. ir. rw H0. ap (choose_pr H). Qed. Lemma V_or : forall x f,   (inc (J x (V x f)) f) \/   ((forall z, ~(inc (J x z) f)) & (V x f = emptyset)). Proof. ir. nin (p_or_not_p (ex (fun y=> inc (J x y) f))).   left. app V_inc. right. split. ir. dneg. exists z. am.   unfold V. app choose_not. Qed. End Pair. Export Pair. Ltac inter2tac :=   match goal with     | H:inc ?X1 (intersection2 ?X2 _ ) |- inc ?X1 ?X2       => ap (intersection2_first H)     | H:inc ?X1 (intersection2 _ ?X2 ) |- inc ?X1 ?X2       => ap (intersection2_second H)     | H:inc ?X1 ?X2 |- inc ?X1 (union2 ?X2 _)       => app union2_first     | H:inc ?X1 ?X2 |- inc ?X1 (union2 _ ?X2)       => app union2_second     | |- inc _ (intersection2 _ _ )      => app intersection2_inc     | H:J _ _ = J _ _ |- _       => solve [ rww (pr1_def H);fprops | rww (pr2_def H) ; fprops]     | H1: is_pair ?x, H2: is_pair ?y |- ?x = ?y => app pair_extensionality    end. ```

## Cartesian products of two sets

``` ```
This is the set of all pairs `J x y` with x in A, y in B
``` Module Cartesian. Definition product (A B : Set) :=   union (fun_image A (fun x => (fun_image B (fun y => J x y)))). Lemma product_inc_rw : forall x y z,   inc x (product y z) = (is_pair x & inc (P x) y & inc (Q x) z). Proof. ir. uf product. app iff_eq. ir. nin (union_exists H). nin H0.   awi H1. nin H1. nin H1. wri H2 H0. awi H0. nin H0. nin H0.   wr H3. ee. fprops. aw. aw.   ir. ee. apply union_inc with (fun_image z (fun y : Set => J (P x) y)).   aw. exists (Q x). split. am. aw. aw. exists (P x). eee. Qed. Hint Rewrite product_inc_rw : aw. Lemma product_pr :forall a b u,   inc u (product a b) -> (is_pair u & inc (P u) a & inc (Q u) b). Proof. ir. wrr product_inc_rw. Qed. Lemma product_inc : forall a b u,   is_pair u -> inc (P u) a -> inc (Q u) b -> inc u (product a b). Proof. ir. aw. au. Qed. Lemma product_pair_pr :  forall a b x y : Set, inc (J x y) (product a b) -> (inc x a & inc y b). Proof. ir. awi H. intuition. Qed. Lemma product_pair_inc :   forall a b x y, inc x a -> inc y b -> inc (J x y) (product a b). Proof. ir. aw. eee. Qed. Lemma pair_in_product: forall a b c, inc a (product b c) -> is_pair a. Proof. ir. awi H. nin H. am. Qed. Hint Resolve product_pair_inc: fprops. ```
A product is empty if and only one factor is empty
``` Lemma empty_product1: forall y,   product emptyset y = emptyset. Proof. ir. empty_tac. awi H. ee. app (emptyset_pr H0). Qed. Lemma empty_product2: forall x,   product x emptyset = emptyset. Proof. ir. empty_tac. awi H. ee. app (emptyset_pr H1). Qed. Lemma empty_product_pr: forall x y,    product x y = emptyset -> (x = emptyset \/ y= emptyset). Proof. ir. nin (emptyset_dichot x). left. am. right. nin H0.   empty_tac. assert (inc (J y0 y1) (product x y)). fprops.   rwi H H2. elim (emptyset_pr H2). Qed. Hint Rewrite empty_product2 empty_product1 : sw. ```
The product A*B is increasing in A and B, strictly if the other argument is non empty.
``` Lemma product_monotone_left: forall x x' y,   sub x x' -> sub (product x y) (product x' y). Proof. ir. red. ir. awi H0. ee. aw. ee. am. app H. am. Qed. Lemma product_monotone_right: forall x y y',   sub y y' -> sub (product x y) (product x y'). Proof. ir. red. ir. awi H0. ee. aw. eee. Qed. Lemma product_monotone: forall x x' y y',   sub x x' -> sub y y' -> sub (product x y) (product x' y'). Proof. ir. apply sub_trans with (product x' y). app product_monotone_left.    app product_monotone_right. Qed. Lemma product_monotone_left2: forall x x' y, nonempty y ->   sub (product x y) (product x' y) -> sub x x'. Proof. ir. red. ir. nin H. assert (inc (J x0 y0) (product x' y)). app H0.   fprops. awi H2. ee. am. Qed. Lemma product_monotone_right2: forall x y y', nonempty x ->   sub (product x y) (product x y') -> sub y y'. Proof. ir. red. ir. nin H. assert (inc (J y0 x0) (product x y')). app H0.   fprops. awi H2. ee. am. Qed. End Cartesian. Export Cartesian. Module Function. ```
A graph is a set of pair; the set of first projections is the domain, the set of second projections is the range
``` Definition is_graph r := forall y, inc y r -> is_pair y. Definition domain f := fun_image f P. Definition range f := fun_image f Q. ```
A functional graph is one for which `P` is injective
``` Definition fgraph f :=   is_graph f & (forall x y, inc x f -> inc y f -> P x = P y -> x = y). Lemma fgraph_is_graph : forall f, fgraph f -> is_graph f. Proof. ir. nin H. am. Qed. Lemma fgraph_pr: forall f x y y',   fgraph f -> inc (J x y) f -> inc (J x y') f -> y = y'. Proof. ir. nin H. assert (P (J x y) = P (J x y')). aw.   cp (H2 _ _ H0 H1 H3). inter2tac. Qed. Hint Resolve fgraph_is_graph : fprops. ```
We give here some properties of the domain and range
``` Lemma inc_pr1_domain : forall f x,   inc x f -> inc (P x) (domain f). Proof. ir. uf domain. app inc_fun_image. Qed. Lemma inc_pr2_range : forall f x,   inc x f -> inc (Q x) (range f). Proof. ir. uf range. app inc_fun_image. Qed. Lemma domain_rw: forall r x,   is_graph r ->   inc x (domain r) = (exists y, inc (J x y) r). Proof. ir. uf domain. aw. app iff_eq. ir.   nin H0. ee. exists (Q x0). wr H1. aw. app H.   ir. nin H0. exists (J x x0). ee. am. aw. Qed. Lemma range_rw: forall r y,   is_graph r -> inc y (range r) = (exists x, inc (J x y) r). Proof. ir. uf range. aw. app iff_eq. ir.   nin H0. ee. exists (P x). wr H1. aw. app H.   ir. nin H0. exists (J x y). ee. am. aw. Qed. Ltac ex_tac:=   match goal with    | H:inc (J ?x ?y) ?z |- exists x, inc (J x ?y) ?z      => exists x ; am    | H:inc (J ?x ?y) ?z |- exists y, inc (J ?x y) ?z      => exists y ; am    | H:inc (J ?x ?y) ?z |- exists x, _ & inc (J x ?y) ?z      => exists x ; split; tv    | H:inc (J ?x ?y) ?z |- exists y, _ & inc (J ?x y) ?z      => exists y ; split; tv    | H:inc (J ?x ?y) ?z |- exists x, inc (J x ?y) ?z & _      => exists x ; split; tv    | H:inc (J ?x ?y) ?z |- exists y, inc (J ?x y) ?z & _      => exists y ; split; tv    | H:inc ?x ?y |- exists x, inc x ?y & _      => exists x ; split; tv     | |- exists x, inc x (singleton ?y) & _      => exists y ; split; fprops     | H : inc (J ?x ?y) ?g |- inc ?x (domain ?g)        => rww domain_rw; exists y ;am     | H : inc (J ?x ?y) ?g |- inc ?y (range ?g)        => rww range_rw; exists x;am     | H : inc ?x ?y |- nonempty ?y        => exists x;am    | |- exists y, inc (J (P ?x) y) _      => exists (Q x) ; aw    | |- exists y, inc (J y (Q ?x)) _      => exists (P x) ; aw end. Hint Rewrite range_rw domain_rw : aw. ```
The function `V` is well-defined for function graphs. Here are some properties
``` Lemma fdomain_pr1 : forall f x,   fgraph f -> inc x (domain f) -> inc (J x (V x f)) f. Proof. ir. awi H0. ap (choose_pr H0). fprops. Qed. Lemma in_graph_V : forall f x,   fgraph f -> inc x f -> x = J (P x) (V (P x) f). Proof. ir. ee. set H. nin f0. app H2. app fdomain_pr1.   app inc_pr1_domain. aw. Qed. Lemma pr2_V : forall f x,   fgraph f -> inc x f -> Q x = V (P x) f. Proof. ir. rw (in_graph_V H H0). aw. Qed. Lemma frange_inc_rw : forall f y,   fgraph f -> inc y (range f) = (exists x, inc x (domain f) & y = V x f). Proof. ir. set (fgraph_is_graph H). aw. ap iff_eq; ir; nin H0; exists x.   split. ex_tac. set (in_graph_V H H0). awi e. inter2tac.   nin H0. set (fdomain_pr1 H H0). ue. Qed. Hint Rewrite frange_inc_rw : sw. Lemma inc_V_range: forall f x,   fgraph f -> inc x (domain f) -> inc (V x f) (range f). Proof. ir. srw. exists x. eee. Qed. ```
Case of a subgraph
``` Lemma sub_graph_fgraph : forall f g, fgraph g -> sub f g -> fgraph f. Proof. ir. split. red. ir. nin H. app H. app H0.   ir. nin H. app H4; app H0. Qed. Lemma sub_graph_domain : forall f g, sub f g -> sub (domain f) (domain g). Proof. ir. uf domain. red. ir. awi H0. aw.   nin H0. nin H0. exists x0. split. ap H. am. am. Qed. Lemma sub_graph_range : forall f g, sub f g -> sub (range f) (range g). Proof. ir. uf range. red. ir. awi H0. aw.   nin H0. nin H0. set (H _ H0). ex_tac. Qed. Lemma sub_graph_ev: forall f g x,   fgraph g -> sub f g -> inc x (domain f) -> V x f = V x g. Proof. ir. set (sub_graph_fgraph H H0).   set (sub_graph_domain H0). set (s _ H1).   set (fdomain_pr1 f0 H1). set (H0 _ i0). set (in_graph_V H i1).   awi e. inter2tac. Qed. Lemma fgraph_sub : forall f g,   fgraph f -> fgraph g -> sub (domain f) (domain g) ->   (forall x, inc x (domain f) -> V x f = V x g) -> sub f g. Proof. ir. red. ir. rw (in_graph_V H H3). set (inc_pr1_domain H3).   rww H2. app fdomain_pr1. app H1. Qed. ```
Two functional graphs are equal if they have the same domain and evaluation
``` Lemma fgraph_exten: forall f g,   fgraph f -> fgraph g -> domain f = domain g ->   (forall x, inc x (domain f) -> V x f = V x g) -> f = g. Proof. ir. app extensionality; app fgraph_sub. ue. ue.   wr H1. ir. sy. app H2. Qed. Lemma range_union2: forall a b, range (union2 a b) = union2 (range a) (range b). Proof. ir. uf range. set_extens. awi H. nin H. nin H. nin (union2_or H).   app union2_first. aw. ex_tac. app union2_second. aw. ex_tac.   aw. nin (union2_or H); awi H0; nin H0; nin H0; exists x0; split.   app union2_first. am. app union2_second. am. Qed. Lemma domain_union2: forall a b,   domain (union2 a b) = union2 (domain a) (domain b). Proof. ir. uf domain. set_extens. awi H. nin H. nin H. nin (union2_or H).   app union2_first. aw. ex_tac. app union2_second. aw. ex_tac.   aw. nin (union2_or H); awi H0; nin H0; nin H0; exists x0; split.   app union2_first. am. app union2_second. am. Qed. Lemma fgraph_union2: forall a b, fgraph a -> fgraph b ->   intersection2 (domain a) (domain b) = emptyset ->   fgraph (union2 a b). Proof. ir. red. nin H; nin H0. split. red. ir. nin (union2_or H4). app H.   app H0. ir. nin (union2_or H4). nin (union2_or H5). app H2.   assert (inc (P x) (domain a)). uf domain. aw. ex_tac.   assert (inc (P y) (domain b)). uf domain. aw. ex_tac. rwi H6 H9.   empty_tac1 (P y). app intersection2_inc.   nin (union2_or H5).   assert (inc (P x) (domain b)). uf domain. aw. ex_tac.   assert (inc (P y) (domain a)). uf domain. aw. ex_tac. rwi H6 H9.   empty_tac1 (P y). app intersection2_inc. app H3. Qed. ```
Inverse image of a set by a graph
``` Definition inverse_image (a f : Set) :=   Zo (domain f) (fun x => inc (V x f) a). Lemma inverse_image_sub :   forall a f, sub (inverse_image a f) (domain f). Proof. uf inverse_image. ir. apply Z_sub. Qed. Lemma inverse_image_inc : forall a f x,   inc x (domain f) -> inc (V x f) a -> inc x (inverse_image a f). Proof. ir. uf inverse_image. Ztac. Qed. Lemma inverse_image_pr :   forall a f x, inc x (inverse_image a f) -> inc (V x f) a. Proof. ir. ufi inverse_image H. Ztac. am. Qed. ```
Graph associated to a function restricted to some set as domain.
``` Definition graph_constructor (x : Set) (p : EE) :=   fun_image x (fun y => J y (p y)). Notation L := graph_constructor. Lemma L_fgraph : forall p x, fgraph (L x p). Proof. ir. uf fgraph. uf L. split; ir. red. ir. awi H. nin H. nin H. wr H0.   fprops. awi H. awi H0. nin H. nin H0. ee. wri H3 H1; wri H2 H1. awi H1.   wr H2; wr H3; wrr H1. Qed. Lemma L_domain : forall x p, domain (L x p) = x. Proof. ir. uf domain. set_extens. awi H. nin H; ee.   ufi L H; awi H; nin H; ee. wr H0; wr H1; aw.   aw. exists (J x0 (p x0)). uf L. aw. split. ex_tac. tv. Qed. Hint Rewrite L_domain : bw. Hint Resolve L_fgraph: gprops. Lemma L_V_rewrite : forall x p y, inc y x -> V y (L x p) = p y. Proof. ir. set (f := L x p).   assert (inc (J y (p y)) f). uf f. uf L. aw. ex_tac.   assert (inc (J y (V y f)) f). app V_inc. ex_tac.   assert (fgraph f). uf f. gprops. app (fgraph_pr H2 H1 H0). Qed. Hint Rewrite L_V_rewrite : bw. Lemma L_range : forall p x,   range (L x p) = fun_image x p. Proof. ir. uf range. uf L. set_extens; awi H; nin H; ee.   awi H; nin H; ee. aw. ex_tac. wr H0. wr H1. aw.   aw. exists (J x1 x0). split. aw. ex_tac. ue. aw. Qed. Lemma L_recovers : forall f,   fgraph f -> L (domain f) (fun x => V x f) = f. Proof. ir. app fgraph_exten. gprops. bw. bw. ir. bw. Qed. ```
Two fgraphs are equal if their domain and function are the same.
``` Lemma L_exten1 : forall a b f g,   a = b -> (forall x, inc x a -> f x = g x) ->   L a f = L b g. Proof. ir. app fgraph_exten. gprops. gprops. bw. bw. ir. bw. app H0. ue. Qed. Lemma L_create : forall a f,   L a (fun x => V x (L a f)) = L a f. Proof. ir. app L_exten1. ir. bw. Qed. Lemma L_range_rw: forall sf f a,   inc a (range (L sf f)) = exists b, inc b sf & f b = a. Proof. ir. rw L_range. app iff_eq. ir. awi H. am. ir. aw. Qed. Hint Rewrite L_range_rw : bw. Lemma L_V_out : forall x f y,   ~inc y x -> V y (L x f) = emptyset. Proof. ir. nin (V_or y (L x f)).   set (inc_pr1_domain H0). rwi pr1_pair i. bwi i. contradiction. intuition. Qed. ```
Composition of two graphs. If the graphs are composable, we can simplify the definition
``` Definition fcomposable (f g : Set) :=   fgraph f & fgraph g & sub (range g) (domain f). Definition fcompose (f g : Set) :=   L (inverse_image (domain f) g) (fun y => V (V y g) f). Definition gcompose g f := L (domain f) (fun y => V (V y f) g). Lemma fcompose_fgraph : forall f g, fgraph (fcompose f g). Proof. ir. uf fcompose. gprops. Qed. Lemma fcompose_domain :   forall f g, domain (fcompose f g) = inverse_image (domain f) g. Proof. ir. uf fcompose. bw. Qed. Lemma fcompose_range: forall f g, fgraph f ->   sub (range (fcompose f g)) (range f). Proof. ir. red. ir. uf range. aw. ufi fcompose H0. bwi H0.   nin H0. nin H0. awi H0. set (inverse_image_pr H0). awi i. nin i.   ex_tac. rw (pr2_V H H2). aw. fprops. Qed. Lemma fcomposable_domain :   forall f g, fcomposable f g -> domain (fcompose f g) = domain g. Proof. ir. uf fcompose. bw. ap extensionality.   ap inverse_image_sub. uf sub; ir. app inverse_image_inc.   red in H. ee. app H2. app inc_V_range. Qed. Lemma fcompose_ev : forall x f g,   inc x (domain (fcompose f g)) -> V x (fcompose f g) = V (V x g) f. Proof. uf fcompose. ir. bwi H. bw. Qed. Lemma fcompose_ev1 : forall x f g, fcomposable f g ->   inc x (domain g) -> V x (fcompose f g) = V (V x g) f. Proof. ir. app fcompose_ev. rw fcomposable_domain. am. am. Qed. Hint Rewrite fcompose_ev1 : bw. Lemma alternate_compose: forall g f,   fcomposable g f -> gcompose g f = fcompose g f. Proof. ir. uf gcompose. app fgraph_exten. gprops.   app fcompose_fgraph. bw. rww fcomposable_domain. bw. ir. bw. Qed. ```
Graph of the identity function.
``` Definition identity_g (x : Set) := L x (fun y => y). Lemma identity_fgraph : forall x, fgraph (identity_g x). Proof. ir. uf identity_g. gprops. Qed. Lemma identity_domain : forall x, domain (identity_g x) = x. Proof. ir. uf identity_g. bw. Qed. Lemma identity_ev : forall x a, inc x a -> V x (identity_g a) = x. Proof. ir. uf identity_g. bw. Qed. ```
restriction of a graph to a set
``` Definition restr f x :=   Zo f (fun y=> inc (P y) x). Lemma restr_inc_rw : forall f x y,   inc y (restr f x) = (inc y f & inc (P y) x). Proof. ir. uf restr. ap iff_eq; ir; ee; Ztac; tv. Qed. Hint Rewrite restr_inc_rw : aw. Lemma restr_sub : forall f x, sub (restr f x) f. Proof. ir. uf sub. ir. awi H. intuition. Qed. Lemma restr_fgraph : forall f x,   fgraph f -> fgraph (restr f x). Proof. ir. eapply sub_graph_fgraph. eexact H. app restr_sub. Qed. Lemma restr_graph: forall x r,   is_graph r -> is_graph (restr r x). Proof. ir. red. ir. awi H0. nin H0. app H. Qed. Hint Resolve restr_graph restr_fgraph : fprops. Lemma restr_domain : forall f x, fgraph f ->     domain (restr f x) = intersection2 (domain f) x. Proof. ir. uf domain. uf restr. set_extens. awi H0. nin H0; ee. Ztac.   wr H1. app intersection2_inc. aw. ex_tac.   nin (intersection2_both H0). aw. awi H1. nin H1. nin H1.   exists x1. split. Ztac. ue. am. Qed. Lemma restr_domain1 : forall f x,   fgraph f -> sub x (domain f) ->   domain (restr f x) = x. Proof. ir. rww restr_domain. set_extens. inter2tac. app intersection2_inc.   app H0. Qed. Lemma fgraph_sub_eq : forall r s,   fgraph r -> fgraph s -> sub r s ->     sub (domain s) (domain r) -> r = s. Proof. ir. app extensionality. uf sub. ir.   rewrite (in_graph_V H0 H3) in H3 |- *.   set (inc_pr1_domain H3). rwi pr1_pair i. set (H2 _ i).   assert (inc (J (P x) (V (P x) r)) r). app fdomain_pr1.   red in H0. ee. rww (H5 _ _ H3 (H1 _ H4)). aw. Qed. Lemma restr_to_domain : forall f g,   fgraph f -> fgraph g -> sub f g ->     restr g (domain f) = f. Proof. ir. sy. app fgraph_sub_eq. fprops.   unfold sub. ir. uf restr; app Z_inc. app H1. app inc_pr1_domain.   rww restr_domain. uf sub;ir. inter2tac. Qed. Lemma restr_ev : forall f u x,   fgraph f -> sub u (domain f) -> inc x u ->     V x (restr f u) = V x f. Proof. ir. assert (inc (J x (V x f)) f). app fdomain_pr1. app H0.   assert (inc (J x (V x f)) (restr f u)).   uf restr; Ztac. aw.   assert (fgraph (restr f u)). fprops. set (pr2_V H4 H3).   awi e. sy. am. Qed. Lemma restr_ev1 : forall f u x,   fgraph f -> inc x (domain f) -> inc x u ->     V x (restr f u) = V x f. Proof. ir. assert (inc (J x (V x f)) f). app fdomain_pr1.   assert (inc (J x (V x f)) (restr f u)).   uf restr; Ztac. aw.   assert (fgraph (restr f u)). fprops. set (pr2_V H4 H3).   awi e. sy. am. Qed. Hint Rewrite restr_ev : bw. Lemma restr_to_domain2 : forall x f,   fgraph f -> sub x (domain f) ->   L x (fun i => V i f) = restr f x. Proof. ir. app fgraph_exten. gprops. fprops. bw. rww restr_domain1. bw.   ir. bw. Qed. Lemma double_restr: forall f a b, fgraph f ->   sub a b -> sub b (domain f) ->   (restr (restr f b) a) = (restr f a). Proof. ir. uf restr. set_extens. Ztac. clear H2. Ztac. am.   Ztac. clear H2. Ztac. Qed. ```
Other properties of graphs
``` Lemma fgraph_sub_V : forall f g x,   fgraph g -> inc x (domain f) -> sub f g -> V x f = V x g. Proof. ir. set (sub_graph_fgraph H H1).   set (H1 _ (fdomain_pr1 f0 H0)). set (in_graph_V H i). awi e.   inter2tac. Qed. ```
Restrictions
``` Definition is_restriction (f g :Set) :=   fgraph g & exists x, f = restr g x. Lemma is_restriction_pr: forall f g,   is_restriction f g =   (fgraph f & fgraph g & sub f g). Proof. ir. uf is_restriction. app iff_eq. ir. ee.   nin H0. rw H0. fprops. am. nin H0. rw H0. uf restr. app Z_sub.   ir. ee. am. set (sub_graph_domain H1). exists (domain f). app fgraph_exten.   fprops. rww restr_domain1. ir. bw. app sub_graph_ev. Qed. ```
Union of graphs
``` Lemma domain_union : forall z, domain (union z) =   union (fun_image z domain). Proof. ir. uf domain. set_extens. awi H. nin H. ee.   nin (union_exists H). ee. apw union_inc (domain x1).   uf domain. aw. ex_tac.   aw. ex_tac.   nin (union_exists H). nin H0. awi H1. nin H1; ee.   aw. wri H2 H0. awi H0. nin H0. nin H0. exists x2. ee. apw union_inc x1. am. Qed. Lemma tack_on_domain : forall f x y,   domain (tack_on f (J x y)) = tack_on (domain f) x. Proof. ir. uf domain. set_extens. awi H. nin H; ee.   rwi tack_on_inc H. rw tack_on_inc; aw. nin H. left. exists x1. split; am.   right. wr H0; rw H. aw.   aw. rwi tack_on_inc H; nin H. awi H. nin H;ee.   exists x1. split. rw tack_on_inc. left; am. am.   exists (J x y). split. rw tack_on_inc; right; tv. aw. sy; am. Qed. Lemma range_union : forall z, range (union z) =   union (fun_image z range). Proof. ir. set_extens.   ufi range H. awi H. nin H. nin H. induction (union_exists H). nin H1.   apw union_inc (range x1). uf range. aw.   exists x0; split; am. aw. exists x1. split. am. tv.   induction (union_exists H). ee. awi H1. nin H1. nin H1.   wri H2 H0. ufi range H0. awi H0. nin H0. ee. uf range. aw. exists x2. split.   apw union_inc x1. am. Qed. Lemma tack_on_range : forall f x y,   range (tack_on f (J x y)) = tack_on (range f) y. Proof. uf range. ir. set_extens. awi H; nin H. ee.   rw tack_on_inc. rwi tack_on_inc H; nin H.   left; aw; exists x1; eee. right; wr H0; rw H;rw pr2_pair; tv.   awi H. nin H. nin H. nin H.   aw. exists x1. eee.   aw. exists (J x y). aw. symmetry in H. au. Qed. Lemma tack_on_fgraph : forall f x y,   fgraph f -> ~ inc x (domain f) ->   fgraph (tack_on f (J x y)). Proof. ir. uf fgraph. ufi fgraph H. ee.   red. ir. rwi tack_on_inc H2. nin H2. app H. ue.   ir. awi H2. awi H3. nin H2; nin H3. app H1.   rwi H3 H4. awi H4. elim H0. wr H4. apply (inc_pr1_domain H2).   elim H0. rwi H2 H4. awi H4. rw H4. apply (inc_pr1_domain H3). ue. Qed. ```
We create a function given a set `x` and a map `f : x->Set`
``` Definition tcreate (x:Set) (f:x->Set) :=   L x (fun y => (Yy (fun (hyp : inc y x) => f (Bo hyp)) emptyset)). Lemma tcreate_value_type : forall (x:Set) (f:x->Set) y,   V (Ro y) (tcreate f) = f y. Proof. ir. assert (inc (Ro y) x). app R_inc. uf tcreate. bw.   apply Yy_if with H. ir. rw B_back. rww B_back. rww B_back. Qed. Lemma tcreate_value_inc : forall (x:Set) (f:x->Set) y (hyp : inc y x),   V y (tcreate f) = f (Bo hyp). Proof. ir. assert (y = Ro (Bo hyp)). rw B_eq. tv.   transitivity (V (Ro (Bo hyp)) (tcreate f)). wr H; tv. ap tcreate_value_type. Qed. Lemma tcreate_domain : forall (x:Set) (f:x->Set), domain (tcreate f) = x. Proof. ir. uf tcreate. bw. Qed. End Function. Export Function. ```