(** * Fundamental set theory Original file by Carlos Simpson Changes: R and Z renamed to Re and Zo E renamed to Bset B Y X renamed to Bo Yo Xo Defines following one letter symbols: J P Q L V W *) Set Implicit Arguments. Require Export Arith. (** ** Axioms *) Module Axioms. Definition Bset:=Type. (** Realisation: if x is a set, maps an object of type x to a set *) Unset Strict Implicit. Parameter Ro : forall x : Bset, x -> Bset. Set Strict Implicit. (** Injectivity of [Ro] *) Axiom R_inj : forall (x : Bset) (a b : x), Ro a = Ro b -> a = b. (** Defines is_element_of and is_subset_of *) Definition inc (x y : Bset) := exists a : y, Ro a = x. Definition sub (a b : Bset) := forall x : Bset, inc x a -> inc x b. (** extensionality for sets *) Axiom extensionality : forall a b : Bset, 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 : Bset) : Prop := nonempty_intro : forall y : Bset, inc y x -> nonempty x. (** Axiom of choice: let [t] be a nonempty type, [p] a predicated 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) (ne : nonemptyT t), ex p -> p (chooseT p ne). (** Image: if [f:x->Bset] is an abstraction, the [IM f] is a set, it contains [y] if and only if [y] is [f z] for some [z:x] *) Parameter IM : forall x : Bset, (x -> Bset) -> Bset. Axiom IM_exists : forall (x : Bset) (f : x -> Bset) (y : Bset), inc y (IM f) -> exists a : x, f a = y. Axiom IM_inc : forall (x : Bset) (f : x -> Bset) (y : Bset), (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 excluded_middle':forall A B:Prop, (~ B->A)->(~A->B). intros a b H c. apply excluded_middle. auto. Qed. Lemma p_or_not_p : forall P : Prop, P \/ ~ P. Proof. intros. apply excluded_middle. intro. apply H. assert P. apply excluded_middle. unfold not. intros. apply H. right; assumption. left ; assumption. Qed. (** Roalisation of nat as ordinals *) Axiom nat_realization_O : forall x : Bset, ~ inc x (Ro 0). Axiom nat_realization_S : forall (n : nat) (x : Bset), inc x (Ro (S n)) = (inc x (Ro n) \/ x = Ro n). (** Roalisation of Prop and True *) Axiom prop_realization : forall x : Prop, Ro x = x. Axiom true_proof_realization_empty : forall t : True, Ro t = Ro 0. End Axioms. Export Axioms. (** ** Tactics *) Module Tactics1. (** Shorthands, for instance [E3 = E -> E -> E -> E] *) Notation EE := (Bset -> Bset). Notation EEE := (Bset -> EE). Notation EP := (Bset -> Prop). Notation EEP := (Bset -> EP). Infix "&":= and (right associativity, at level 100). Definition type_of (T : Type) (t : T) := T. 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 forup : forall A B (f g:A -> B) (a b : A), f = g -> a = b -> f a = g b. Proof. intros T1 T2 f g a b H1 H2. rewrite H2; rewrite H1; 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 om := omega. 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 uh a := red in a. Ltac app u := (ap u; try tv; try am). Ltac rww u := (rw u; try tv; try am). Ltac rwii u h:= (rwi u h; try tv; try am). Ltac wrr u := (wr u; try tv; try am). Ltac aw := autorewrite with aw; try tv; try am. Ltac au := first [ solve [am] | auto ]. Ltac set_extens:= app extensionality; unfold sub; intros. Ltac EasyDeconj := match goal with | |- (_ & _) => ap conj; [ EasyDeconj | EasyDeconj ] | |- (and _ _) => ap conj; [ EasyDeconj | EasyDeconj ] | |- (_ /\ _) => 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. End Tactics1. Export Tactics1. (** ** Constructions *) Module Constructions. (** This definition is rarely used *) Definition exists_unique t (p : t->Prop) := (ex p) & (forall x y : t, p x -> p y -> x = y). (** Defines [neq] as different, and [strict_sub] as strict subset *) Definition neq (x y : Bset) := x <> y. Definition strict_sub (a b : Bset) := (neq a b) & (sub a b). Definition elt x y := inc y x. Lemma sub_trans : forall a b c, sub a b -> sub b c -> sub a c. Proof. unfold 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. unfold strict_sub; unfold neq. ir. nin H. split. red. ir. ap H. wri H2 H0. app extensionality. apply sub_trans with b; am. Qed. Lemma strict_sub_trans2 : forall a b c, sub a b -> strict_sub b c -> strict_sub a c. Proof. unfold strict_sub; unfold neq. ir. nin H0. split. red. ir. ap H0. rwi H2 H. app extensionality. apply sub_trans with b; am. Qed. (** Emptyset is a type without constructor; empty is classical *) Definition empty (x : Bset) := forall y : Bset, ~ inc y x. Inductive emptyset : Bset :=. (** Basic property of Ro*) Lemma R_inc : forall (x : Bset) (a : x), inc (Ro a) x. Proof. ir. uf inc. exists a; tv. Qed. (** Equivalence between [nonempty] and [~ empty] *) Lemma inc_nonempty : forall x y, inc x y -> nonemptyT y. Proof. uf inc. ir. destruct H as [H _]. app nonemptyT_intro. Qed. Lemma nonemptyT_not_empty : forall x, nonemptyT x -> ~ empty x. Proof. ir. nin H. unfold not. ir. unfold empty in H. apply H with (Ro X). apply R_inc. 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 : Bset) (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. unfold inc; unfold Bo. ir. app chooseT_pr. Qed. Lemma B_back : forall (x:Bset) (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. intro. ap excluded_middle'. ir. red. intros y H0. ap H. ap nonemptyT_intro. exact (Bo H0). Qed. Lemma emptyset_empty : forall x, ~ inc x emptyset. Proof. intros x H. assert (e:= Bo H). elim e. Qed. Lemma exT_exists : forall p : EP, (exists x : Bset, p x) -> ex p. Proof. ir. nin H. exists x; 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 *) Definition by_cases_pr (T : Type) (P : Prop) (a : P -> T) (b : ~ P -> T) (x : T) := (forall p : P, a p = x) & (forall q : ~ P, b q = x). Lemma by_cases_exists : forall (T : Type) (P : Prop) (a : P -> T) (b : ~ P -> T), exists x : T, by_cases_pr a b x. Proof. ir. assert (H: P \/ ~ P). app p_or_not_p. nin H. exists (a H). red. split. ir. assert (p=H). ap proof_irrelevance. rww H0. ir. assert (e:=q H); elim e. exists (b H). red. split. ir. assert (e:= H p); elim e. ir. assert (H = q). ap proof_irrelevance. rww H0. Qed. Lemma by_cases_nonempty : forall (T : Type) (P : Prop) (a : P -> T) (b : ~ P -> T), nonemptyT T. Proof. ir. assert (P \/ ~ P). ap p_or_not_p. nin H; 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 => by_cases_pr a b x) (by_cases_nonempty a b). Lemma by_cases_property : forall (T : Type) (P : Prop) (a : P -> T) (b : ~ P -> T), by_cases_pr a b (by_cases a b). Proof. ir. set (H:= (by_cases_exists a b)). set (H1:=(by_cases_nonempty a b)). set (H2:=(chooseT_pr H1 H)). unfold by_cases. assert (by_cases_nonempty a b = H1). apply proof_irrelevance. rewrite H0. apply H2. Qed. Lemma by_cases_unique : forall (T : Type) (P : Prop) (a : P -> T) (b : ~ P -> T) (x : T), by_cases_pr a b x -> by_cases a b = x. Proof. ir. red in H. destruct H as [PT PF]. set (H1:= (by_cases_property a b)). unfold by_cases_pr in H1. destruct H1 as [APT APF]. assert (P \/ ~ P). apply p_or_not_p. induction H. rewrite <- APT with H; auto. rewrite <- APF with H; auto. Qed. Lemma by_cases_if : forall (T : Type) (P : Prop) (a : P -> T) (b : ~ P -> T) (p : P), by_cases a b = a p. Proof. ir. ap by_cases_unique. red. split. ir. assert (p0=p). apply proof_irrelevance. rww H. ir; elim q; tv. Qed. Lemma by_cases_if_not : forall (T : Type) (P : Prop) (a : P -> T) (b : ~ P -> T) (q : ~ P), by_cases a b = b q. Proof. ir. ap by_cases_unique. red. split. intro p; elim q; auto. ir. assert (q0=q). ap proof_irrelevance. rww H. Qed. (** Constructs q from p, such that, if p is true for some value, then q is p, otherwise, [q x] is [x=emptyset]. Two lemmas that restate this, and another that says taht theres exists at least one x with [q x] *) Definition refined_pr (p:EP) (x:Bset) := (ex p -> p x) & ~(ex p) -> x = emptyset. Lemma refined_pr_if : forall p x, ex p -> refined_pr p x = p x. Proof. ir. unfold refined_pr. ap iff_eq; ir. destruct H0. auto. split; [idtac | intro; destruct H1]; auto. Qed. Lemma refined_pr_not : forall p x, ~(ex p) -> refined_pr p x = (x = emptyset). Proof. ir. unfold refined_pr. ap iff_eq; ir. destruct H0; auto. split; [intro; destruct H | idtac]; auto. Qed. Lemma exists_refined_pr : forall p, ex (refined_pr p). Proof. ir. apply by_cases with (ex p); ir. elim H; intros x Hx. exists x. rww refined_pr_if. exists emptyset. rww refined_pr_not. Qed. (** Genereralised axiom of choice. [choose p] is satisfied by [p] if somebody satisfies p, is the emptyset otherwise *) Definition choose' : EP -> Bset := fun X:EP => chooseT X (nonemptyT_intro Prop). Lemma choose'_pr : forall p : EP, ex p -> p (choose' p). Proof. ir. unfold choose'. app chooseT_pr. Qed. Definition choose (p:EP) := choose' (refined_pr p). Lemma choose_pr : forall p, ex p -> p (choose p). Proof. ir. unfold choose. set (H1:=exists_refined_pr p). assert (refined_pr p (choose' (refined_pr p))). app choose'_pr. destruct H0 as [HT HF]. app HT. Qed. Lemma choose_not : forall p, ~(ex p) -> choose p = emptyset. Proof. ir. unfold choose. assert (W:=(exists_refined_pr p)). assert (refined_pr p (choose' (refined_pr p))). app choose'_pr. destruct H0 as [HT HF]. app HF. Qed. (** Axiom of choice applied to [inc]. If [x] not empty, [rep x] is in [x] *) Definition rep (x : Bset) := choose (fun y : Bset => inc y x). Lemma nonempty_rep : forall x, nonempty x -> inc (rep x) x. Proof. ir. unfold rep. ap choose_pr. induction H. exists y. am. Qed. (** compares: forall x, p(x) false, and the existence of p(x) *) Lemma exists_proof : forall p : EP, ~ (forall x : Bset, ~ p x) -> ex p. Proof. intro. ap excluded_middle'. intros H x H0. apply H. exists x. assumption. Qed. Lemma not_exists_pr : forall p : EP, ~ ex p <-> (forall x : Bset, ~ p x). Proof. ir. split; ir; intro H1. apply H. exists x; am. induction H1. apply H with x; am. Qed. (** Defines [Y P x y] to b 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. set (a := fun p:P => x); set (b := fun p: ~ P => y). assert (z= a hyp). auto. rewrite H0. ap 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 (a := fun p:P => x); set (b := fun p : ~ P => z). assert (y = b hyp); auto. rewrite H0. apply by_cases_if_not. Qed. Lemma Y_if_rw : forall (P:Prop) (hyp :P) x y, Yo P x y = x. Proof. intros. apply Y_if; auto. Qed. Lemma Y_if_not_rw : forall (P:Prop) (hyp : ~P) x y, Yo P x y = y. Proof. intros. apply Y_if_not; auto. Qed. (** Given a function f, [Zorec] remembers a and f(a) *) Record Zorec (x : Bset) (f : x -> Bset) : Bset := {Zohead : x; Zotail : f Zohead}. (** [Zo x p] is the image of some function [g]; this means that [inc y (Zo x p)] if and anly if [y = g t] for some [t]; [t] is a record, say it remembers [a], of type [x], and [p (Ro a)]; [g(t)] is [Ro a]. Thus [inc y x] and [p y]; The converse is true. *) Definition Zo := fun (x:Bset) (p:EP) => let P := Zorec (fun a : x => p (Ro a)) in IM (fun t : P => Ro (Zohead t)). Lemma Z_inc : forall (x : Bset) (p : EP) (y : Bset), inc y x -> p y -> inc y (Zo x p). Proof. ir. unfold Zo. ap IM_inc. ufi inc H. induction H. assert (p (Ro x0)). rww H. pose (Build_Zorec (fun a : x => p (Ro a)) x0 H1). exists z. trivial. Qed. Lemma Z_sub : forall x p, sub (Zo x p) x. Proof. unfold sub. ir. pose (IM_exists H). nin e. wr H0. apply R_inc. Qed. Lemma Z_pr : forall x p y, inc y (Zo x p) -> p y. Proof. unfold inc; unfold Zo. ir. induction H. pose (R_inc x0). pose (IM_exists i). induction e. pose (Zotail x1). rwi H0 p0. rwi H0 p0. wrr H. Qed. Lemma Z_all : forall x p y, inc y (Zo x p) -> (inc y x & p y). Proof. ir. assert (sub (Zo x p) x). ap Z_sub. split. app H0. set (Z_pr H); auto. Qed. Ltac Ztac := match goal with | id1:(inc ?X1 (Zo _ _)) |- _ => pose (Z_all id1); ee | |- (inc _ (Zo _ _)) => ap Z_inc; au | _ => idtac end. Definition Yy : forall P : Prop, (P -> Bset) -> EE := fun P f x => by_cases f (fun _ : ~ P => x). Lemma Yy_if : forall (P : Prop) (hyp : P) (f : P -> Bset) x z, f hyp = z -> Yy f x = z. Proof. ir. unfold Yy. set (b := fun _ : ~ P => x). rewrite <- H. apply by_cases_if. Qed. Lemma Yy_if_not : forall (P : Prop) (hyp : ~ P) (f : P -> Bset) (x z : Bset), x = z -> Yy f x = z. Proof. ir. unfold Yy. set (b := fun _ : ~ P => x). assert (z= b hyp). unfold b. auto. rw H0. ap by_cases_if_not. Qed. (** Defines [X 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 : Bset) (f : x -> Bset) (y : Bset) := Yy (fun hyp : inc y x => f (Bo hyp)) emptyset. Lemma X_eq : forall (x : Bset) (f : x -> Bset) (y z : Bset), (exists a : x, (Ro a = y) & (f a = z)) -> Xo f y = z. Proof. ir. induction H. unfold Xo. destruct H. symmetry in H. assert (inc y x). rw H. apply R_inc. apply Yy_if with H1. assert (Bo H1 = x0). apply R_inj. rww B_eq. rww H2. Qed. Lemma X_rewrite : forall (x : Bset) (f : x -> Bset) (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 : Bset) (p : x -> Prop) := Zo x (fun y : Bset => forall hyp : inc y x, p (Bo hyp)). Lemma cut_sub : forall (x : Bset) (p : x -> Prop), sub (cut p) x. Proof. ir. unfold cut. apply Z_sub. Qed. Definition cut_to (x : Bset) (p : x -> Prop) (y : cut p) := Bo (cut_sub (p:=p) (R_inc y)). Lemma cut_to_R_eq : forall (x : Bset) (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 : Bset) (p : x -> Prop) (y : cut p), p (cut_to y). Proof. ir. unfold cut_to. ufi cut y. set (k := fun y : Bset => forall hyp : inc y x, p (Bo hyp)) in y. pose (R_inc y). pose (Z_all i). induction a. apply H0. Qed. Lemma cut_inc : forall (x : Bset) (p : x -> Prop) (y : x), p y -> inc (Ro y) (cut p). Proof. ir. unfold cut. ap Z_inc. ap R_inc. ir. assert (Bo hyp = y). ap R_inj. ap B_eq. rww H0. Qed. (** If x is in the image of f, chooses y with f(y)=x *) Definition IM_lift : forall (a : Bset) (f : a -> Bset), IM f -> a. ir. assert (exists x : a, f x = Ro X). ap IM_exists. ap R_inc. assert (nonemptyT a). induction H. app nonemptyT_intro. exact (chooseT (fun x : a => f x = Ro X) H0). Defined. Lemma IM_lift_pr : forall (a : Bset) (f : a -> Bset) (x : IM f), f (IM_lift x) = Ro x. Proof. ir. assert (exists y : a, f y = Ro x). ap IM_exists. ap R_inc. unfold IM_lift. set (K := ex_ind (fun (x0 : a) (_ : (fun u : a => f u = Ro x) x0) => nonemptyT_intro x0) (IM_exists (R_inc x))). pose (chooseT_pr K H). assumption. Qed. End Constructions. Export Constructions. (** ** Little*) Module Little. (** singleton: image of a set with one point *) Inductive one_point : Bset := one_point_intro : one_point. Definition singleton (x : Bset) := IM (fun p : one_point => x). Lemma singleton_inc : forall x, inc x (singleton x). Proof. ir. unfold singleton. ap IM_inc. exists one_point_intro. tv. Qed. Hint Resolve sub_refl singleton_inc: fprops. Ltac fprops := auto with fprops. Lemma singleton_eq : forall x y, inc y (singleton x) -> y = x. Proof. ir. pose (IM_exists H). elim e. sy. tv. Qed. 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. (** doubleton: image of a set with two points *) Inductive two_points : Bset := | two_points_a | two_points_b. Lemma two_points_pr: forall x, inc x two_points = (x= Ro two_points_a \/ x = Ro two_points_b). Proof. ir. app iff_eq. ir. nin H. wr H. elim x0. left. tv. right. tv. ir. nin H. rw H. app R_inc. rw H. app R_inc. Qed. Lemma two_points_distinct: Ro two_points_a <> Ro two_points_b. Proof. red. ir. cp (R_inj H). discriminate H0. Qed. Lemma two_points_distinctb: Ro two_points_b <> Ro two_points_a. Proof. red. ir. cp (R_inj H). discriminate H0. Qed. Definition doubleton_map : forall x y : Bset, two_points -> Bset. intros x y t. induction t. exact x. exact y. Defined. Definition doubleton (x y : Bset) := IM (doubleton_map x y). Lemma doubleton_first : forall x y, inc x (doubleton x y). Proof. ir. unfold doubleton. ap IM_inc. exists two_points_a. tv. Qed. Lemma doubleton_second : forall x y : Bset, inc y (doubleton x y). Proof. ir. unfold doubleton. ap IM_inc. exists two_points_b. tv. Qed. Lemma doubleton_or : forall x y z : Bset, inc z (doubleton x y) -> z = x \/ z = y. Proof. ir. pose (IM_exists H). elim e. intro x0. induction x0. simpl. intuition. simpl. intuition. Qed. Hint Resolve doubleton_first doubleton_second: fprops. 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. pose (doubleton_or H0). pose (doubleton_or H1). induction o. pose (doubleton_or H2). induction o. left. split. am. induction o0. rw H5; rw H4; am. am. left. auto. right. split. am. induction o0. am. pose (doubleton_or H3). sy. wri H4 H5. induction o. rww H5. am. Qed. Lemma doubleton_singleton : forall x, doubleton x x = singleton x. Proof. ir. ap extensionality; unfold sub; ir. assert (e:=doubleton_or H). induction e. rw H0. fprops. rw H0; fprops. assert (H0:=singleton_eq H). rw H0. fprops. 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. nin (doubleton_or H1). rw H2. fprops. rw H2. fprops. Qed. End Little. Export Little. (** ** Basic Realisations *) Module Basic_Realizations. Lemma nat_zero_emptyset : Ro 0 = emptyset. Proof. set_extens. assert (H0:=nat_realization_O H). auto; elim H0. induction (Bo H). Qed. Lemma false_emptyset : emptyset = False. Proof. set_extens. induction (Bo H). elim (Bo H). Qed. Lemma R_false_emptyset : Ro False = emptyset. Proof. rw false_emptyset. ap prop_realization. Qed. Lemma true_proof_emptyset : forall t : True, Ro t = emptyset. Proof. ir. assert (H:=true_proof_realization_empty t). rw H. apply nat_zero_emptyset. Qed. Lemma true_singleton_emptyset : singleton emptyset = True. Proof. set_extens. assert (p:=singleton_eq H). unfold inc. exists I. sy. rww true_proof_emptyset. ufi inc H. induction H. assert (Ro x0 = emptyset). ap true_proof_emptyset. wr H0. rw H. ap singleton_inc. Qed. Lemma R_true_singleton_emptyset : Ro True = singleton emptyset. Proof. rw prop_realization. sy. ap true_singleton_emptyset. Qed. Lemma R_one_singleton_emptyset : Ro 1 = singleton emptyset. Proof. set_extens. rwi nat_realization_S H; rwi nat_zero_emptyset H. induction H. pose emptyset_empty. elim (n x H). rw H. ap singleton_inc. rw nat_realization_S; rw nat_zero_emptyset. right. app singleton_eq. Qed. Lemma R_two_prop : Ro 2 = Prop. Proof. set_extens. rwi nat_realization_S H; rwi R_one_singleton_emptyset H. unfold inc. induction H. set (H0:=(singleton_eq H)). rw H0. exists False. ap R_false_emptyset. rwi true_singleton_emptyset H. rw H. exists True. ap prop_realization. rw nat_realization_S. rw R_one_singleton_emptyset. apply by_cases with (Bo H). ir. right. wrr R_true_singleton_emptyset. assert (Bo H = True). ap iff_eq; ir; tv. wr H1. rww B_eq. ir. left. wr R_false_emptyset. assert (Bo H = False). ap iff_eq. am. ir. elim H1. assert (x = Ro (Bo H)). rww B_eq. rwi H1 H2. rw H2. ap singleton_inc. Qed. Lemma emptyset_dichot : forall x, (x = emptyset \/ nonempty x). Proof. ir. ap excluded_middle. red. intro. cut (x = emptyset & nonempty x); intuition. apply excluded_middle; red; intros. apply H1. apply excluded_middle; red; intros. apply H. apply extensionality; red; intros. assert False. apply H2. apply nonempty_intro with x0. assumption. elim H4. assert (~ inc x0 emptyset). apply emptyset_empty. intuition. (* Second case*) apply excluded_middle; red; intros. apply H0. apply extensionality; red; intros. assert False. apply H1. apply nonempty_intro with x0. assumption. elim H3. assert (~ inc x0 emptyset). apply emptyset_empty. intuition. Qed. End Basic_Realizations. Export Basic_Realizations. (** ** Complement *) Module Complement. (** Set of all elements in a not in b *) Definition complement (a b : Bset) := Zo a (fun x : Bset => ~ inc x b). Lemma inc_complement : forall a b x, inc x (complement a b) = (inc x a & ~ inc x b). Proof. ir. unfold complement. apply iff_eq; ir. pose (Z_all H). apply a0. destruct H. app Z_inc. Qed. Lemma use_complement : forall a b x, inc x a -> ~ inc x (complement a b) -> inc x b. Proof. ir. ap excluded_middle; unfold not; ir. ap H0. unfold complement. app Z_inc. Qed. Lemma non_nonempty_comp_sub: forall a b, ~ nonempty (complement a b) -> sub a b. Proof. ir. uf sub. ir. apply use_complement with a. am. red. ir. app H. exists x. am. Qed. Lemma show_sub_or_aux: forall b c, ~ (sub b c \/ sub c b) -> nonempty (complement c b). Proof. ir. app excluded_middle. red. ir. app H. right. app non_nonempty_comp_sub. Qed. Lemma show_sub_or : forall b c , (nonempty (complement b c) -> nonempty (complement c b) -> False) -> sub b c \/ sub c b. Proof. ir. app excluded_middle. red. ir. ap H. assert (~ (sub c b \/ sub b c)). red. ir. app H0. induction H1. right. am. left. am. app show_sub_or_aux. app show_sub_or_aux. Qed. Lemma sub_complement: forall a b, sub (complement a b) a. Proof. ir. uf sub; ir. rwi inc_complement H; ee; am. Qed. Lemma strict_sub_nonempty_complement : forall x y, strict_sub x y -> nonempty (complement y x). Proof. ir. assert (nonemptyT (complement y x)). ap not_empty_nonemptyT. red; ir. uh H; ee. ap H. set_extens. ap excluded_middle. red; ir. assert (inc x0 (complement y x)). rw inc_complement. split;am. uh H0. ufi not H0. apply H0 with x0. am. nin H0. cp (R_inc X). exists (Ro X). am. Qed. End Complement. Export Complement. (** ** Pair *) Module Pair. Export Little. (** One way of defining an ordered set *) Definition pair_first (x y:Bset):= singleton x. Definition pair_second (x y:Bset):= doubleton emptyset (singleton y). Definition pair (x y : Bset) := doubleton (pair_first x y) (pair_second x y). Definition is_pair (u : Bset) := exists x, exists y, u = pair x y. Lemma inc_pair1: forall x y, inc (pair_first x y) (pair x y). Proof. ir. uf pair. fprops. Qed. Lemma inc_pair2: forall x y, inc (pair_second x y) (pair x y). Proof. ir. uf pair. fprops. Qed. Lemma pair_extensionalitya: forall x y u, inc u (pair x y) -> u = pair_first x y \/ u = pair_second x y. Proof. ir. uf pair. app doubleton_or. Qed. Lemma pair_distincta:forall x y z w, (pair_first x y = pair_second z w)-> False. Proof. ir. ufi pair_first H; ufi pair_second H. assert (inc emptyset (singleton x)). rw H. fprops. cp (singleton_eq H0). assert (inc (singleton w) (singleton x)). rw H. fprops. cp (singleton_eq H2). assert (inc w emptyset). rw H1; wr H3. fprops. nin H4. elim x0. 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 pair_extensionality_first : forall x y z w : Bset, pair x y = pair z w -> x = z. Proof. ir. assert (pair_first x y = pair_first z w). assert (inc (pair_first x y) (pair z w)). wr H. app inc_pair1. cp (pair_extensionalitya H0). nin H1. am. elim (pair_distincta H1). ufi pair_first H0. app singleton_inj. Qed. Lemma pair_extensionality_second : forall x y z w, pair x y = pair z w -> y = w. Proof. ir. assert (pair_second x y = pair_second z w). assert (inc (pair_second x y) (pair z w)). wr H. app inc_pair2. cp (pair_extensionalitya H0). nin H1. symmetry in H1. elim (pair_distincta H1). am. ufi pair_second H0. assert (inc (singleton y) (doubleton emptyset (singleton w))). wrr H0. fprops. pose (doubleton_or H1). induction o. assert (inc y emptyset). wr H2. fprops. nin H3. elim x0. app singleton_inj. Qed. (** First and second projections *) Definition pr1 (u : Bset) := choose (fun x : Bset => ex (fun y : Bset => u = pair x y)). Definition pr2 (u : Bset) := choose (fun y : Bset => ex (fun x : Bset => u = pair x y)). Notation J := pair. Notation P := pr1. Notation Q := pr2. Definition pair_recovers (u : Bset) := J (P u) (Q u) = u. Lemma pair_recov : forall u, is_pair u -> pair_recovers u. Proof. unfold is_pair. unfold pair_recovers. ir. pose (choose_pr H). induction e. assert (exists y : Bset, exists x : Bset, u = J x y). exists x. exists (P u). am. pose (choose_pr H1). induction e. assert (u = J (P u) x). am. assert (u = J x0 (Q u)). am. assert (J (pr1 u) x = J x0 (pr2 u)). wrr H3. pose (pair_extensionality_first H5). rw e. sy. am. Qed. Lemma pair_is_pair : forall x y : Bset, is_pair (J x y). Proof. unfold is_pair. intros. exists x. exists y. trivial. Qed. Hint Resolve pair_is_pair: fprops. Lemma is_pair_rw : forall x, is_pair x = (x = J (P x) (Q x)). Proof. ir. ap iff_eq;ir. set (H0:=pair_recov H). red in (type of H0). sy; am. rw H. fprops. Qed. Lemma pr1_pair : forall x y, P (J x y) = x. Proof. ir. set (u := J x y). assert (is_pair u). unfold u. ap pair_is_pair. assert(p:=pair_recov H). ufi pair_recovers p. ufi u p. pose (pair_extensionality_first p). am. Qed. Lemma pr2_pair : forall x y, Q (J x y) = y. Proof. ir. set (u := J x y). assert (is_pair u). unfold u. fprops. assert (p:=pair_recov H). ufi pair_recovers p. ufi u p. pose (pair_extensionality_second p). am. Qed. Hint Rewrite pr1_pair pr2_pair : aw. Ltac awi u:= autorewrite with aw in u. 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)). assert (pair_recovers a). app pair_recov. sy. ap H3. assert (pair_recovers b). app pair_recov. rw H1. rw H2. am. Qed. Lemma pr1_injective: forall a b c d, J a b = J c d -> a = c. Proof. ir. assert (P (J a b) = P (J c d)). rww H. awi H0. am. Qed. Lemma pr2_injective: forall a b c d, J a b = J c d -> b = d. Proof. ir. assert (Q (J a b) = Q (J c d)). rww H. awi H0. am. Qed. Lemma uneq2 : forall (f:Bset-> Bset-> Bset) (a b c d:Bset), a=c -> b = d -> f a b = f c d. Proof. ir. rw H. rw H0. tv. 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, that V chooses one, otherwise it is the empty set. *) Definition V (x f : Bset) := choose (fun y : Bset => inc (pair 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. pose (choose_pr H). am. 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. apply by_cases with (ex (fun y=> inc (pair x y) f)); ir. left. app V_inc. right. split. ir. unfold not; intro; apply H. exists z. am. unfold V. app choose_not. Qed. End Pair. Export Pair. (** ** Image *) Module Image. (** Image of a set by a function *) Definition fun_image (x : Bset) (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. pose (IM_exists H). induction e. exists (Ro x0). split. app R_inc. tv. induction H. induction H. wr H0. app inc_fun_image. Qed. 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 : Bset) := IM (fun p : x -> Prop => cut p). Lemma powerset_inc : forall x y, sub x y -> inc x (powerset y). Proof. ir. uf powerset. ap IM_inc. exists (fun b:y=> inc (Ro b) x). set_extens. set (c:= (Bo H0)). assert (x0 = Ro c). pose (B_eq H0); sy; am. assert (Ro c = Ro (cut_to c)). sy. ap cut_to_R_eq. rw H1; rw H2. apply (cut_pr c). set (x1:= Bo H0). set (e:=B_eq H0). wr e. unfold cut. ap Z_inc. ap H. rww e. ir. set (w:= B_eq hyp). rw w; rw e. am. Qed. Lemma powerset_sub : forall x y, inc x (powerset y) -> sub x y. Proof. ir. ufi powerset H. set (e:= IM_exists H). induction e. wr H0. ap cut_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. Lemma inc_x_powerset_x: forall x, inc x (powerset x). Proof. ir. app powerset_inc. 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 : Bset) : Bset := {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 : Bset) := IM (fun i : Union_integral x => Ro (Union_elt (x:=x) 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. pose (Bo H2). pose (Build_Union_integral (x:=a) (Union_param:=w) r). uf union. ap IM_inc. exists u. simpl. uf r. 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. set (e:= IM_exists H). induction e. 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 : Bset) := 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. pose (union_exists H). induction e. induction H0. nin (doubleton_or H1). left; wrr H2. right; wrr H2. Qed. Lemma union2_first : forall x y a, inc a x -> inc a (union2 x y). Proof. ir. uf union2. apply union_inc with x. am. fprops. Qed. Lemma union2_second : forall x y a, inc a y -> inc a (union2 x y). Proof. ir. uf union2. apply union_inc with y. am. 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 union2_idempotent: forall u, union2 u u= u. Proof. ir. set_extens. rwi inc_union2_rw H. nin H. am. am. rw inc_union2_rw. left. am. 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; ap singleton_eq]; 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. ap singleton_inc. Qed. (** Like tack, argumenrs reversed *) Definition tack x y := tack_on y x. Lemma tack_or : forall x y z, inc z (tack y x) -> (inc z x \/ z = y). Proof. ir. ufi tack H. app tack_on_or. Qed. Lemma tack_inc : forall x y z, (inc z (tack y x) ) = (inc z x \/ z = y). Proof. ir. uf tack. ap tack_on_inc. Qed. Lemma sub_union : forall x z, (forall y, inc y z -> sub y x) -> sub (union z) x. Proof. ir. red; ir. pose (union_exists H0). nin e. ee. assert (sub x1 x). app H. app H3. Qed. End Union. Export Union. (** ** Intersection *) Module Intersection. (** Intersection: set of of all z in w, that are in all elements of x; w is some element of x, the value is irrelevant. Sometimes x must be assumed nonempty *) Definition intersection (x : Bset) := Zo (rep x) (fun y : Bset => forall z : Bset, 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. pose (nonempty_rep H). 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. pose (Z_all H). induction a0. app H2. Qed. Lemma intersection_sub : forall x y, inc y x -> sub (intersection x) y. Proof. ir. uf sub. ir. apply intersection_forall with x. am. am. 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. apply intersection_forall with (doubleton x y). am. fprops. Qed. Lemma intersection2_second : forall x y a, inc a (intersection2 x y) -> inc a y. Proof. ir. ufi intersection2 H. apply intersection_forall with (doubleton x y). am. fprops. Qed. Lemma intersection_use_inc : forall x y, inc y (intersection x) -> forall z, inc z x -> inc y z. Proof. ir. apply intersection_forall with x; am. Qed. End Intersection. Export Intersection. (** ** Transposition *) Module Transposition. (** Evaluates to j or i if a is i or j; to a otherwise *) Definition create (i j a : Bset) := Yo (a = i) j (Yo (a = j) i a). Lemma not_i_not_j : forall i j a, a <> i -> a <> j -> create i j a = a. Proof. ir. uf create. ap (Y_if_not H). sy. apply (Y_if_not H0). tv. Qed. Lemma i_j_j_i : forall i j a, create i j a = create j i a. Proof. ir. uf create. apply by_cases with (a = i). ir. ap (Y_if H). sy. apply by_cases with (a = j). ir. ap (Y_if H0). wrr H. ir. ap (Y_if_not H0). sy. app (Y_if H). ir. ap (Y_if_not H). apply by_cases with (a = j). ir. ap (Y_if H0). sy. app (Y_if H0). ir. ap (Y_if_not H0). ap (Y_if_not H0). app (Y_if_not H). Qed. Lemma i_j_i : forall i j, create i j i = j. Proof. ir. uf create. assert (i = i); trivial. app (Y_if H). Qed. Lemma i_j_j : forall i j, create i j j = i. Proof. ir. rw i_j_j_i. ap i_j_i. Qed. Lemma i_i_a : forall i a, create i i a = a. Proof. ir. apply by_cases with (a = i). ir. rw H. ap i_j_j. ir. uf create. ap (Y_if_not H). sy. app (Y_if_not H). Qed. Lemma surj : forall i j a, exists b, create i j b = a. Proof. ir. apply by_cases with (a = i). ir. exists j. rw H. ap i_j_j. ir. apply by_cases with (a = j). ir. exists i. rw H0. ap i_j_i. ir. exists a. app not_i_not_j. Qed. Lemma involutive : forall i j a, create i j (create i j a) = a. Proof. ir. apply by_cases with (a = i). ir. rw H. rw i_j_i. ap i_j_j. apply by_cases with (a = j). ir. rw H. rw i_j_j. app i_j_i. ir. pose (not_i_not_j H0 H). rww e. Qed. Lemma inj : forall i j a b, create i j a = create i j b -> a = b. Proof. ir. transitivity (create i j (create i j a)). sy; ap involutive. rw H. ap involutive. Qed. End Transposition. (** ** Module Bounded A property p is "collectivisante" if there exists a set x such that [p y] if and only if [inc y x]. Such a set is unique. It exists if p has the form [y = f z], where f is defined on a set or a type. *) Module Bounded. Definition property (p : EP) (x : Bset) := forall y : Bset, (p y -> inc y x & inc y x -> p y). Definition axioms (p : EP) := ex (property p). Definition create (p : EP) := choose (property p). Lemma criterion : forall p : EP, ex (fun x : Bset => forall y : Bset, p y -> inc y x) -> axioms p. Proof. intros p (x) H. red. exists (Zo x p). red. ir. split. ir. apply (Z_inc _ (H _ H0) H0). ir. apply (Z_pr H0). Qed. Lemma lem1 : forall (p : EP) (y : Bset), axioms p -> inc y (create p) -> p y. Proof. ir. red in H. ufi create H0. pose (choose_pr H). ufi property H0. ufi property p0. pose (p0 y). induction a. app H2. Qed. Lemma lem2 : forall (p : EP) (y : Bset), axioms p -> p y -> inc y (create p). Proof. ir. uf create. ufi axioms H. pose (choose_pr H). set (K := choose (property p)). ufi property p0. pose (p0 y). induction a. app H1. Qed. Lemma inc_create : forall (p : EP) y, axioms p -> inc y (create p) = p y. Proof. ir. app iff_eq. ir. app lem1. ir. app lem2. Qed. Lemma trans_criterion : forall (p : EP) (f : EE) (x : Bset), (forall y : Bset, p y -> ex (fun z : Bset => (inc z x &f z = y))) -> axioms p. Proof. ir. app criterion. exists (fun_image x f). ir. rw fun_image_rw. app H. Qed. Lemma little_criterion : forall (p : EP) (x : Bset) (f : x -> Bset), (forall y : Bset, p y -> exists a : x, f a = y) -> axioms p. Proof. ir. ap criterion. exists (IM f). ir. ap IM_inc. app H. Qed. End Bounded. (** ** Cartesian products of two sets *) Module Cartesian. (** Rolation [in_record] is collectivisante, hence we can define a record *) Definition in_record (a : Bset) (f : EE) (x : Bset) := is_pair x & inc (P x) a & inc (Q x) (f (P x)). Record Cartesian_record (a : Bset) (f : EE) : Bset := {Cartesian_first : a; Cartesian_second : f (Ro Cartesian_first)}. Definition recordMap (a : Bset) (f : EE) (i : Cartesian_record a f) := J (Ro (Cartesian_first i)) (Ro (Cartesian_second i)). Lemma in_record_ex : forall (a : Bset) (f : EE) (x : Bset), in_record a f x -> exists i : Cartesian_record a f, recordMap i = x. Proof. ir. red in H. ee. set (u := Bo H0). assert (Ro u = pr1 x). uf u. apply B_eq. assert (inc (pr2 x) (f (Ro u))). rww H2. set (v := Bo H3). pose (Build_Cartesian_record f u v). exists c. transitivity (pair (Ro u) (Ro v)). trivial. assert (Ro v = pr2 x). uf v. app B_eq. rw H4. assert (Ro u = pr1 x); auto. rw H5. app pair_recov. Qed. Lemma in_record_bounded : forall (a : Bset) (f : EE), Bounded.axioms (in_record a f). Proof. ir. apply Bounded.criterion. exists (IM (recordMap (a:=a) (f:=f))). ir. ap IM_inc. app in_record_ex. Qed. Definition record (a : Bset) (f : EE) := Bounded.create (in_record a f). Lemma record_in : forall a f x, inc x (record a f) -> in_record a f x. Proof. ir. ufi record H. pose (in_record_bounded a f). pose (Bounded.lem1 a0 H). assumption. Qed. Lemma record_pr : forall a f x, inc x (record a f) -> (is_pair x & inc (P x) a & inc (Q x) (f (P x))). Proof. intros. pose (record_in H). assumption. Qed. Lemma record_inc : forall a f x, in_record a f x -> inc x (record a f). Proof. ir. uf record. app Bounded.lem2. ap in_record_bounded. Qed. Lemma record_pair_pr : forall a f x y, inc (J x y) (record a f) -> (inc x a & inc y (f x)). Proof. ir. split. pose (record_in H). ufi in_record i. induction i. induction H1. awi H1. am. pose (record_in H). ufi in_record i. ee. awi H2. am. Qed. Lemma record_pair_inc : forall a f x y, inc x a -> inc y (f x) -> inc (pair x y) (record a f). Proof. ir. ap record_inc. red. ee. fprops. aw. aw. Qed. (** A product is just a record where the function is constant *) Definition product (a b : Bset) := record a (fun x : Bset => b). Lemma product_pr : forall a b u, inc u (product a b) -> (is_pair u & inc (P u) a & inc (Q u) b). Proof. uf product; ir. pose (record_pr H). intuition. 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. uf product. ap record_inc. uf in_record. intuition. Qed. Lemma product_pair_pr : forall a b x y : Bset, inc (J x y) (product a b) -> (inc x a & inc y b). Proof. ir. ufi product H. pose (record_pair_pr H). assumption. 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. uf product. app record_pair_inc. Qed. Lemma inc_product : forall x y z, inc x (product y z) = (is_pair x & inc (P x) y & inc (Q x) z). Proof. ir. ap iff_eq; ir. cp (product_pr H). am. ap product_inc; ee; am. Qed. (** A product is empty if and only one factor is empty *) Lemma empty_product1: forall y, product emptyset y = emptyset. Proof. ir. set_extens. rwi inc_product H. ee. nin H0. elim x0. nin H. elim x0. Qed. Lemma empty_product2: forall x, product x emptyset = emptyset. Proof. ir. set_extens. rwi inc_product H. ee. nin H1. elim x1. nin H. elim x1. Qed. Lemma empty_product_pr: forall x y, product x y = emptyset -> (x = emptyset \/ y= emptyset). Proof. ir. pose (emptyset_dichot x). nin o. left. am. ir. right. nin H0. set_extens. assert (inc (J y0 x0) (product x y)). app product_pair_inc. rwi H H2. nin H2. elim x1. nin H1. elim x1. Qed. (** 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. rwi inc_product H0. ee. rw inc_product. 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. rwi inc_product H0. ee. rw inc_product. ee. am. am. app H. 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. rw inc_product. ee. fprops. aw. aw. rwi inc_product H2. ee. awi H3. 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. rw inc_product. ee. fprops. aw. aw. rwi inc_product H2. ee. awi H4. am. Qed. End Cartesian. Export Cartesian. (** ** Back *) Module Sback. (** Defines [Bdefault] as a version of [B] where a default value is given and thus no hypothesis of inclusion is required; applies this to get [Bnat] sending a set back to a natural with default value [0]. *) Definition RBdefault x z (d:z) := Yo (inc x z) x (Ro d). Lemma RBdefault_in : forall x z (d:z), inc x z -> RBdefault x d = x. Proof. ir. uf RBdefault. rww Y_if_rw. Qed. Lemma RBdefault_out : forall x z (d:z), ~(inc x z) -> RBdefault x d = (Ro d). Proof. ir. uf RBdefault. rww Y_if_not_rw. Qed. Lemma inc_RBdefault : forall x z (d:z), inc (RBdefault x d) z. Proof. ir. apply by_cases with (inc x z); ir. rww RBdefault_in. rww RBdefault_out. app R_inc. Qed. Definition Bdefault x z (d:z) : z := Bo (inc_RBdefault x d). Lemma R_Bdefault_in : forall x z (d:z), inc x z -> Ro (Bdefault x d) = x. Proof. ir. uf Bdefault. rw B_eq. rww RBdefault_in. Qed. Lemma Bdefault_out : forall x z (d:z), ~(inc x z) -> (Bdefault x d) = d. Proof. ir. uf Bdefault. ap R_inj. rw B_eq. rww RBdefault_out. Qed. Lemma Bdefault_R : forall z (y d:z), Bdefault (Ro y) d = y. Proof. ir. ap R_inj. rww R_Bdefault_in. ap R_inc. Qed. Definition Bnat x := Bdefault x (z:=nat) 0. Lemma R_Bnat : forall x, inc x nat -> Ro (Bnat x) = x. Proof. ir. uf Bnat. rww R_Bdefault_in. Qed. Lemma Bnat_out : forall x, ~(inc x nat) -> Bnat x = 0. Proof. ir. uf Bnat. rww Bdefault_out. Qed. Lemma Bnat_R : forall (i:nat), Bnat (Ro i) = i. Proof. ir. ap R_inj. rww R_Bnat. ap R_inc. Qed. End Sback.