(** * 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 proof_irrelevance : forall (P : Prop) (q p : P), p = q. *) 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. (* EOF*)