(*** version of july 7 2003 ---Carlos Simpson ***) Set Implicit Arguments. Module Axioms. (************************ PARAMETERS AND AXIOMS ************************) (*** interpret types as being classical sets ***) Definition E := Type. (*** elements of a set are themselves sets ***) (***) Parameter R : (x:E)x -> E. (***) Axiom R_inj : (x:E; a,b:x)(R a) == (R b) -> a == b. Definition inc := [x,y:E](exT ? [a:y](R a) == x). Definition sub := [a,b:E](x:E)(inc x a) -> (inc x b). (*** a set is determined by its elements ****) (***) Axiom extensionality : (a,b:E)(sub a b) -> (sub b a) -> a == b. Inductive nonemptyT [t:Type] : Prop := nonemptyT_intro : t -> (nonemptyT t). (*** the axiom of choice on the type level ********************* WARNING: !!!!!!!!!!! this version of choice is contradictory with the impredicativity of Set; when using things like nat : Set, be careful not to invoke the impredicativity of Set !!!!!!!!!!!!!! *********) (***) Parameter chooseT :(t:Type; p: t-> Prop)(nonemptyT t) -> t. (***) Axiom chooseT_pr : (t:Type; p: t-> Prop; ne: (nonemptyT t)) (exT ? p)-> (p (chooseT p ne)). (*** the replacement axiom: images of a set are again sets *********) (***) Parameter IM : (x:E)(x -> E) -> E. (***) Axiom IM_exists : (x:E; f:x -> E; y:E)(inc y (IM f)) -> (exT ? [a:x](f a) == y). (***) Axiom IM_inc : (x:E; f:x -> E; y:E)(exT ? [a:x](f a) == y) -> (inc y (IM f)). (*** the following actually follow from the above as was shown in the standard library but we write them as axioms for brevity **************) (***) Axiom excluded_middle : (P:Prop)(not (not P)) -> P. (***) Axiom proof_irrelevance : (P:Prop; q,p:P)p==q. (*** the following axioms can be obtained from the Ensembles library but we include it here as an axiom; it is used for convenience, allowing us to replace iff by equality so as to be able to rewrite using equality of propositions **********************************) (***) Axiom iff_eq : (P,Q:Prop)(P -> Q) -> (Q -> P) -> P==Q. (********* END OF PARAMETERS AND AXIOMS *********************************************) End Axioms. Export Axioms. Module Constructions. Definition neq := [x,y:E]~(x == y). Lemma sub_trans : (a,b,c:E)(sub a b) -> (sub b c) -> (sub a c). Unfold sub. EAuto. Save. Lemma inc_nonempty : (x,y:E)(inc x y) -> (nonemptyT y). Intros. Unfold inc in H. NewInduction H. Apply nonemptyT_intro. Assumption. Save. Lemma R_inc : (x:E; a:x)(inc (R a) x). Intros. Unfold inc. EApply exT_intro with a. Trivial. Save. Definition B := [x,y:E; hyp : (inc x y)] (chooseT [a:y](R a) == x (inc_nonempty hyp)). Lemma B_eq : (x,y:E; hyp : (inc x y))(R (B hyp)) == x. Intros. Unfold B. Pose (chooseT_pr 2![a:y](R a) == x). Apply e. Assumption. Save. Definition empty := [x:E](y:E)~(inc y x). Lemma nonemptyT_not_empty : (x:E)(nonemptyT x) -> ~(empty x). Intros. NewInduction H. Unfold not. Unfold empty. Intros. Unfold not in H. Apply H with (R X). Apply R_inc. Save. Lemma not_empty_nonemptyT : (x:E)~(empty x) -> (nonemptyT x). Intros. Apply excluded_middle. Unfold not. Intros. Unfold not in H. Apply H. Unfold empty. Unfold not. Intros. Apply H0. Apply nonemptyT_intro. Exact (B H1). Save. Inductive nonempty [x: E] : Prop := nonempty_intro : (y:E)(inc y x) -> (nonempty x). Inductive emptyset : E := . Lemma emptyset_empty : (x:E)~(inc x emptyset). Unfold not. Intros. Pose (B H). Elim e. Save. Syntactic Definition E1 := E -> E. Syntactic Definition E2 := E -> E1. Syntactic Definition E3 := E -> E2. Syntactic Definition E4 := E -> E3. Syntactic Definition E5 := E -> E4. Syntactic Definition E6 := E -> E5. (** thus for example E3 = E -> E -> E -> E **) Syntactic Definition EP := E -> Prop. Syntactic Definition E2P := E -> EP. Syntactic Definition E3P := E -> E2P. Syntactic Definition E4P := E -> E3P. Definition A := and. Recursive Tactic Definition Deconj := Match Context With [|- (A ? ?)] -> Unfold A; Apply conj; [Deconj |Deconj] | [|- (and ? ?)] -> Apply conj; [Deconj |Deconj] | [|- ? /\ ?] -> Apply conj; [Deconj |Deconj] | [|- ?] -> Auto. Recursive Tactic Definition Expand := Match Context With [id1 : (A ?1 ?2) |- ?] -> (Unfold A in id1); NewInduction id1; Expand | [id1 : (and ?1 ?2) |- ?] -> NewInduction id1; Expand | [id1 : (?1 /\ ?2) |- ?] -> NewInduction id1; Expand | [|- ?] -> Deconj. (*** we write a tactic which is like Pose but which is anonymous ***) Tactic Definition Recall u := Pose recalx := u; Match Context With [recalx : ?1 |- ? ] -> (Assert ?1; [Exact recalx | Clear recalx]). Definition strict_sub := [a,b:E] (A (neq a b) (sub a b) ). Lemma strict_sub_trans1 : (a,b,c:E)(strict_sub a b) -> (sub b c) -> (strict_sub a c). Unfold strict_sub. Unfold neq. Unfold not. Intros. Expand. Intros. Apply H. Apply extensionality. Assumption. Rewrite H2. Assumption. Expand. Apply sub_trans with b; Auto. Save. Lemma strict_sub_trans2 : (a,b,c:E)(sub a b) -> (strict_sub b c) -> (strict_sub a c). Unfold strict_sub. Unfold neq. Unfold not. Intros. Expand. Intros. Apply H0. Apply extensionality. Assumption. Rewrite <- H2. Assumption. Expand. Apply sub_trans with b; Auto. Save. Inductive exists [p:E -> Prop]: Prop := exists_intro : (x:E)(p x) -> (exists p). Definition exists_unique := [p:E->Prop] (A (exists p) (x,y:E)(p x) -> (p y) -> x == y ). Lemma exT_exists : (p:E-> Prop)(exT ? [x:E](p x)) -> (exists p). Intros. NewInduction H. Pose exists_intro. EAuto. Save. Lemma p_or_not_p : (P:Prop)P \/ (not P). Intros. EApply excluded_middle. Unfold not. Intros. Assert P; Apply excluded_middle; Unfold not; Auto. Save. Definition choose : (E -> Prop) -> E. Intros. EApply chooseT. Assumption. EApply nonemptyT_intro. Exact Prop. Defined. Lemma choose_pr : (p:E -> Prop)(exists p) -> (p (choose p)). Intros. Unfold choose. EApply chooseT_pr. NewInduction H. Apply exT_intro with x. Assumption. Save. Definition rep := [x:E](choose [y:E](inc y x)). Lemma nonempty_rep : (x:E)(nonempty x) -> (inc (rep x) x). Intros. NewInduction H. Unfold rep. Apply choose_pr. Apply exists_intro with y. Assumption. Save. Definition by_cases_pr:= [T:Type; P:Prop; a:P -> T; b:(not P) -> T; x:T] (A (p:P)(a p) == x (q:(not P))(b q) == x ). Lemma by_cases_exists : (T:Type; P:Prop; a:P -> T; b:(not P) -> T) (exT ? [x:T](by_cases_pr a b x)). Intros. Assert (P \/ (not P)). Apply p_or_not_p. NewInduction H. EApply exT_intro with (a H). Unfold by_cases_pr. Expand. Intros. Assert H==p. Apply proof_irrelevance. Rewrite H0. Trivial. Intros. Pose (q H). Elim f. EApply exT_intro with (b H). Unfold by_cases_pr. Expand. Intros. Pose (H p). Elim f. Intros. Assert H == q. Apply proof_irrelevance. Rewrite H0. Trivial. Save. Lemma by_cases_nonempty : (T:Type; P:Prop; a:P -> T; b:(not P) -> T) (nonemptyT T). Intros. Intros. Assert (P \/ (not P)). Apply p_or_not_p. NewInduction H. EApply nonemptyT_intro. Exact (a H). EApply nonemptyT_intro. Exact (b H). Save. Definition by_cases := [T:Type; P:Prop; a:P -> T; b:(not P) -> T] (chooseT [x:T](by_cases_pr a b x) (by_cases_nonempty a b)). Lemma by_cases_property : (T:Type; P:Prop; a:P -> T; b:(not P) -> T) (by_cases_pr a b (by_cases a b)). Intros. Recall '(by_cases_exists a b). Recall '(by_cases_nonempty a b). Recall '(chooseT_pr H0 H). Unfold by_cases. Assert (by_cases_nonempty a b) == H0. Apply proof_irrelevance. Rewrite H2. Assumption. Save. Lemma by_cases_unique : (T:Type; P:Prop; a:P -> T; b:(not P) -> T; x:T) (by_cases_pr a b x) -> (by_cases a b) == x. Intros. Recall '(by_cases_property a b). Intros. Assert (P \/ (not P)). Apply p_or_not_p. NewInduction H1. Unfold by_cases_pr in H. Unfold by_cases_pr in H0. Expand. Transitivity (a H1). Symmetry. Auto. Auto. Unfold by_cases_pr in H. Unfold by_cases_pr in H0. Expand. Transitivity (b H1). Symmetry. Auto. Auto. Save. Lemma by_cases_if : (T:Type; P:Prop; a:P -> T; b:(not P) -> T; p:P) (by_cases a b) == (a p). Intros. EApply by_cases_unique. Unfold by_cases_pr. Expand. Intros. Assert p == p0. Apply proof_irrelevance. Rewrite H. Trivial. Intros. Recall '(q p). Elim H. Save. Lemma by_cases_if_not : (T:Type; P:Prop; a:P -> T; b:(not P) -> T; q : (not P)) (by_cases a b) == (b q). Intros. EApply by_cases_unique. Unfold by_cases_pr. Expand. Intros. Recall '(q p). Elim H. Intros. Assert q == q0. Apply proof_irrelevance. Rewrite H. Trivial. Save. Lemma exists_proof : (p:E->Prop)(not (x:E)(not (p x))) -> (exists p). Intros. Unfold not in H. EApply excluded_middle. Unfold not. Intros. Apply H. Intros. Apply H0. EApply exists_intro with x. Assumption. Save. Lemma not_exists_pr : (p:E-> Prop)(not (exists p)) <-> ((x:E)(not (p x))). Intros. Unfold iff. Apply conj. Intros. Unfold not. Unfold not in H. Intros. Apply H. Apply exists_intro with x. Assumption. Intros. Unfold not. Unfold not in H. Intros. NewInduction H0. Apply H with x. Assumption. Save. Definition Yy :(P:Prop; f:P-> E)E -> E. Intros P f x. Apply by_cases with P. Exact f. Intros. Exact x. Defined. Lemma Yy_if : (P:Prop; hyp : P; f:P-> E; x,z:E)(f hyp) == z -> (Yy f x) == z. Intros. Unfold Yy. Pose b := [p:~P]x. Rewrite <- H. Apply by_cases_if. Save. Lemma Yy_if_not : (P:Prop; hyp : ~P; f:P-> E; x,z:E)x == z -> (Yy f x) == z. Intros. Unfold Yy. Pose b := [p:~P]x. Transitivity (b hyp). Apply by_cases_if_not. Trivial. Save. Definition Y : Prop -> E -> E -> E. Intros P x y. EApply by_cases with P. Intros. Exact x. Intros. Exact y. Defined. Lemma Y_if : (P:Prop; hyp : P; x,y,z:E) x == z -> (Y P x y) == z. Intros. Unfold Y. Pose a:= [p:P]x. Pose b := [p:~P]y. Transitivity (a hyp). Apply by_cases_if. Transitivity x. Trivial. Assumption. Save. Lemma Y_if_not : (P:Prop; hyp : (not P); x,y,z:E) y == z -> (Y P x z) == y. Intros. Unfold Y. Pose a:= [p:P]x. Pose b := [p:~P]z. Transitivity (b hyp). Apply by_cases_if_not. Rewrite H. Trivial. Save. Record Rec [x:E; f:x -> E] : E := join { head : x; tail : (f head) }. Implicits join [1 2]. Definition Z : E -> (E -> Prop) -> E. Intros x p. Pose (Rec [a:x](p (R a))). Exact (IM [t:T](R (head t))). Defined. Lemma Z_inc : (x:E; p: E -> Prop; y:E)(inc y x) -> (p y) -> (inc y (Z x p)). Intros. Unfold Z. EApply IM_inc. Unfold inc in H. NewInduction H. Assert (p (R x0)). Rewrite H. Assumption. Pose (join 2![a:x](p (R a)) x0 H1). Apply exT_intro with r. Trivial. Save. Lemma Z_sub : (x:E; p: E -> Prop)(sub (Z x p) x). Intros. Unfold sub. Intros. Pose (IM_exists H). NewInduction e. Rewrite <- H0. Apply R_inc. Save. Lemma Z_pr : (x:E; p: E-> Prop; y:E)(inc y (Z x p)) -> (p y). Intros. Unfold inc in H. NewInduction H. Unfold Z in x0. Pose (R_inc x0). Pose (IM_exists i). NewInduction e. Pose (tail x1). Rewrite H0 in p0. Rewrite <- H. Assumption. Save. Lemma Z_all : (x:E; p: E-> Prop; y:E)(inc y (Z x p)) -> (A (inc y x) (p y)). Intros. Expand. Assert (sub (Z x p) x). Apply Z_sub. Apply H0; Assumption. Pose _:=(Z_pr H); Auto. Save. Tactic Definition Ztac := Match Context With [id1 : (inc ?1 (Z ? ?)) |- ? ] -> Pose (Z_all id1); Expand | [|- (inc ? (Z ? ?))] -> Apply Z_inc; Auto | _ -> Idtac. Definition X := [x:E; f: x -> E; y:E] (Yy [hyp : (inc y x)](f (B hyp)) emptyset). Lemma X_eq : (x:E; f: x -> E; y,z: E) (exT ? [a:x](A (R a) == y (f a) == z)) -> (X f y) == z. Intros. NewInduction H. Expand. Unfold X. Assert (inc y x). Rewrite <- H. Apply R_inc. Apply Yy_if with H1. Assert (B H1) == x0. Apply R_inj. Rewrite B_eq. Auto. Rewrite H2. Assumption. Save. Lemma X_rewrite : (x:E; f: x -> E; a:x) (X f (R a)) == (f a). Intros. Apply X_eq. Apply exT_intro with a. Expand. Save. Definition cut := [x:E; p: x -> Prop] (Z x [y:E](hyp : (inc y x))(p (B hyp))). Lemma cut_sub : (x:E; p: x -> Prop)(sub (cut p) x). Intros. Unfold cut. Apply Z_sub. Save. Definition cut_to := [x:E; p: x -> Prop; y: (cut p)] (B ((cut_sub 2!p) ? (R_inc y))). Lemma cut_to_R_eq : (x:E; p: x -> Prop; y: (cut p)) (R (cut_to y)) == (R y). Intros. Unfold cut_to. Rewrite B_eq. Trivial. Save. Lemma cut_pr : (x:E; p: x -> Prop; y:(cut p))(p (cut_to y)). Intros. Unfold cut_to. Unfold cut in y. LetTac k := [y:E](hyp:(inc y x))(p (B hyp)). Pose (R_inc y). Ztac. Save. Lemma cut_inc : (x:E; p: x -> Prop; y:x)(p y) -> (inc (R y) (cut p)). Intros. Unfold cut. Apply Z_inc. Apply R_inc. Intros. Assert (B hyp) == y. Apply R_inj. Apply B_eq. Rewrite H0. Assumption. Save. End Constructions. Export Constructions. Module Little. Inductive one_point : E := point : one_point. Definition singleton := [x:E](IM [p:one_point]x). Lemma singleton_inc : (x:E)(inc x (singleton x)). Intros. Unfold singleton. Apply IM_inc. Apply exT_intro with point. Trivial. Save. Lemma singleton_eq : (x,y:E)(inc y (singleton x)) -> y == x. Intros. Pose (IM_exists H). NewInduction e. Symmetry. Trivial. Save. Lemma singleton_inj : (x,y: E)(singleton x) == (singleton y) -> x == y. Intros. Assert (inc x (singleton y)). Rewrite <- H. Apply singleton_inc. Apply singleton_eq. Assumption. Save. Inductive two_points : E := first : two_points | second : two_points. Definition doubleton_map : (x,y:E)two_points -> E. Intros x y t. NewInduction t. Exact x. Exact y. Defined. Definition doubleton := [x,y:E](IM (doubleton_map x y)). Lemma doubleton_first : (x,y:E)(inc x (doubleton x y)). Intros. Unfold doubleton. Apply IM_inc. Apply exT_intro with first. Trivial. Save. Lemma doubleton_second : (x,y:E)(inc y (doubleton x y)). Intros. Unfold doubleton. Apply IM_inc. Apply exT_intro with second. Trivial. Save. Lemma doubleton_or : (x,y,z:E)(inc z (doubleton x y)) -> (z == x) \/ (z == y). Intros. Pose (IM_exists H). NewInduction e. NewInduction x0. Compute in H0. Intuition. Compute in H0. Intuition. Save. Lemma doubleton_inj : (x,y,z,w:E)(doubleton x y) == (doubleton z w) -> (A x == z y == w) \/ (A x == w y == z). Intros. Assert (inc x (doubleton z w)). Rewrite <- H. Apply doubleton_first. Pose (doubleton_or H0). Assert (inc y (doubleton z w)). Rewrite <- H. Apply doubleton_second. Pose (doubleton_or H1). NewInduction o. NewInduction o0. Assert (inc w (doubleton x y)). Rewrite H. Apply doubleton_second. Pose (doubleton_or H4). NewInduction o. Apply or_introl. Expand. Rewrite H5. Rewrite H2. Assumption. Apply or_introl. Expand. Apply or_introl. Expand. NewInduction o0. Apply or_intror. Expand. Assert (inc z (doubleton x y)). Rewrite H. Apply doubleton_first. Pose (doubleton_or H4). NewInduction o. Apply or_introl. Expand. Apply or_introl. Expand. Rewrite H5. Rewrite H3. Assumption. Save. End Little. Module Pair. Export Little. Definition pair := [x,y:E] (doubleton (singleton x) (doubleton emptyset (singleton y))). Definition is_pair := [u:E](exists [x:E](exists [y:E]u== (pair x y))). Lemma lem1 : (x,y,z,w:E)(pair x y) == (pair z w) -> x == z. Intros. Assert (inc (singleton x) (pair z w)). Rewrite <- H. Unfold pair. Apply doubleton_first. Unfold pair in H0. Pose (doubleton_or H0). NewInduction o. Apply singleton_inj. Assumption. Assert (inc emptyset (singleton x)). Rewrite H1. Apply doubleton_first. Assert (inc (singleton w) (singleton x)). Rewrite H1. Apply doubleton_second. Assert emptyset == x. Apply singleton_eq. Assumption. Assert (singleton w) == x. Apply singleton_eq. Assumption. Assert (inc w emptyset). Rewrite H4. Rewrite <- H5. Apply singleton_inc. Pose (emptyset_empty H6). Elim f. Save. Lemma lem2 : (x,y,z,w:E)(pair x y) == (pair z w) -> y == w. Intros. Assert (inc (doubleton emptyset (singleton y)) (pair z w)). Rewrite <- H. Unfold pair. Apply doubleton_second. Unfold pair in H0. Pose (doubleton_or H0). NewInduction o. Assert (inc emptyset (singleton z)). Rewrite <- H1. Apply doubleton_first. Assert (inc (singleton y) (singleton z)). Rewrite <- H1. Apply doubleton_second. Pose (singleton_eq H2). Pose (singleton_eq H3). Assert (inc y emptyset). Rewrite e. Rewrite <- e0. Apply singleton_inc. Pose (emptyset_empty H4). Elim f. Assert (inc (singleton y) (doubleton emptyset (singleton w))). Rewrite <- H1. Apply doubleton_second. Pose (doubleton_or H2). NewInduction o. Assert (inc y emptyset). Rewrite<- H3. Apply singleton_inc. Pose (emptyset_empty H4). Elim f. Apply singleton_inj. Assumption. Save. Definition pr1 := [u:E](choose [x:E](exists [y:E]u== (pair x y))). Definition pr2 := [u:E](choose [y:E](exists [x:E]u == (pair x y))). Syntactic Definition J := pair. Syntactic Definition P := pr1. Syntactic Definition Q := pr2. Definition pair_recovers := [u:E](pair (pr1 u) (pr2 u)) == u. Lemma pair_recov : (u:E)(is_pair u) -> (pair_recovers u). Intros. Unfold is_pair in H. Unfold pair_recovers. Pose (choose_pr H). Assert (exists [y:E](exists [x:E] (u == (pair x y)))). NewInduction e. Apply exists_intro with x. Apply exists_intro with (pr1 u). Assumption. Pose (choose_pr H0). NewInduction e. NewInduction e0. Assert u == (pair (pr1 u) x). Assumption. Assert u == (pair x0 (pr2 u)). Assumption. Assert (pair (pr1 u) x) == (pair x0 (pr2 u)). Rewrite <- H3. Assumption. Pose (lem1 H5). Rewrite e. Symmetry. Assumption. Save. Lemma pair_is_pair : (x,y:E)(is_pair (pair x y)). Intros. Unfold is_pair. Apply exists_intro with x. Apply exists_intro with y. Trivial. Save. Lemma pr1_pair : (x,y:E)(pr1 (pair x y)) == x. Intros. LetTac u := (pair x y). Assert (is_pair u). Unfold u. Apply pair_is_pair. Pose (pair_recov H). Unfold pair_recovers in (Type of p). Unfold u in (Type of p). Pose (lem1 p). Assumption. Save. Lemma pr2_pair : (x,y:E)(pr2 (pair x y)) == y. Intros. LetTac u := (pair x y). Assert (is_pair u). Unfold u. Apply pair_is_pair. Pose (pair_recov H). Unfold pair_recovers in (Type of p). Unfold u in (Type of p). Pose (lem2 p). Assumption. Save. Definition V := [x,f:E](choose [y:E](inc (pair x y) f)). Lemma V_inc : (x,z,f:E)(exists [y:E](inc (pair x y) f)) -> z == (V x f) -> (inc (pair x z) f). Intros. Pose (choose_pr H). Rewrite H0. Assumption. Save. End Pair. Export Pair. Module Image. Definition create := [x:E; f: E1](IM [a:x](f (R a))). Lemma incl : (x:E; f:E -> E; a:E)(inc a x) -> (inc (f a) (create x f)). Intros. Unfold create. Apply IM_inc. Apply exT_intro with (B H). Pose (B_eq H). Rewrite e. Trivial. Save. Lemma show_inc : (x:E; f:E -> E; z:E) (exists [a:E](A (inc a x) (f a) == z)) -> (inc z (create x f)). Intros. NewInduction H. Expand. Rewrite <- H0. Apply incl. Assumption. Save. Lemma ex : (x:E; f:E-> E; a:E)(inc a (create x f)) -> (exists [b:E](A (inc b x) (f b) == a)). Intros. Pose (IM_exists H). NewInduction e. Apply exists_intro with (R x0). Expand. Unfold inc. Apply exT_intro with x0. Trivial. Save. End Image. Module Powerset. Definition powerset := [x:E](IM [p:x-> Prop](cut p)). Lemma powerset_inc : (x,y:E)(sub x y) -> (inc x (powerset y)). Intros. Unfold powerset. Apply IM_inc. Apply exT_intro with [b:y](inc (R b) x). Apply extensionality. Unfold sub. Intros. Pose (B H0). Pose (B_eq H0). Pose (cut_pr c). Assert x0 == (R (cut_to c)). Transitivity (R c). Unfold c. Auto. Symmetry. Apply cut_to_R_eq. Rewrite H1. Assumption. Unfold sub. Intros. Pose (B H0). Pose (B_eq H0). Rewrite <- e. Unfold cut. Apply Z_inc. Apply H. Rewrite e. Assumption. Intros. Pose (B_eq hyp). Rewrite e0. Rewrite e. Assumption. Save. Lemma powerset_sub : (x,y:E)(inc x (powerset y)) -> (sub x y). Intros. Unfold powerset in H. Pose (IM_exists H). NewInduction e. Rewrite <- H0. Apply cut_sub. Save. End Powerset. Export Powerset. Module Union. Record Integral [x:E] : E := { param : x; elt : (R param) }. Definition union := [x:E](IM [i:(Integral x)](R (!elt x i))). Lemma union_inc : (x,y,a:E)(inc x y) -> (inc y a) -> (inc x (union a)). Intros. Pose (B H0). Assert (R a0) == y. Unfold a0. Apply B_eq. Assert (inc x (R a0)). Rewrite H1. Assumption. Pose (B H2). Pose (!Build_Integral a a0 r). Unfold union. Apply IM_inc. Apply exT_intro with i. Change (R r) == x. Unfold r. Apply B_eq. Save. Lemma union_exists : (x,a:E)(inc x (union a)) -> (exists [y:E](A (inc x y) (inc y a))). Intros. Unfold union in H. Pose (IM_exists H). NewInduction e. Apply exists_intro with (R (param x0)). Expand. Rewrite <- H0. Apply R_inc. Apply R_inc. Save. Definition union2 := [x,y:E](union (doubleton x y)). Lemma union2_or : (x,y,a:E)(inc a (union2 x y)) -> ((inc a x) \/ (inc a y)). Intros. Unfold union2 in H. Pose (union_exists H). NewInduction e. Expand. Pose (doubleton_or H1). NewInduction o. Rewrite H2 in H0. Intuition. Rewrite H2 in H0; Intuition. Save. Lemma union2_first : (x,y,a:E)(inc a x)-> (inc a (union2 x y)). Intros. Unfold union2. Apply union_inc with x. Assumption. Apply doubleton_first. Save. Lemma union2_second : (x,y,a:E)(inc a y)-> (inc a (union2 x y)). Intros. Unfold union2. Apply union_inc with y. Assumption. Apply doubleton_second. Save. End Union. Export Union. Module Intersection. Definition intersection := [x:E](Z (rep x) [y:E] (z:E)(inc z x) -> (inc y z)). Lemma intersection_inc : (x,a:E)(nonempty x) -> ((y:E)(inc y x) -> (inc a y)) -> (inc a (intersection x)). Intros. Unfold intersection. Apply Z_inc. Pose (nonempty_rep H). Apply H0. Assumption. Assumption. Save. Lemma intersection_forall : (x,a,y:E) (inc a (intersection x)) -> (inc y x) -> (inc a y). Intros. Unfold intersection in H. Ztac. Save. Lemma intersection_sub : (x,y:E) (inc y x) -> (sub (intersection x) y). Intros. Unfold sub. Intros. Apply intersection_forall with x; Auto. Save. Definition intersection2 : E -> E -> E := [x,y:E](intersection (doubleton x y)). Lemma intersection2_inc : (x,y,a:E)(inc a x) -> (inc a y) ->(inc a (intersection2 x y)). Intros. Unfold intersection2. Apply intersection_inc. Apply nonempty_intro with x. Apply doubleton_first. Intros. Recall '(doubleton_or H1). NewInduction H2. Rewrite H2. Assumption. Rewrite H2. Assumption. Save. Lemma intersection2_first : (x,y,a:E)(inc a (intersection2 x y)) -> (inc a x). Intros. Unfold intersection2 in H. EApply intersection_forall with (doubleton x y). Assumption. Apply doubleton_first. Save. Lemma intersection2_second : (x,y,a:E)(inc a (intersection2 x y)) -> (inc a y). Intros. Unfold intersection2 in H. EApply intersection_forall with (doubleton x y). Assumption. Apply doubleton_second. Save. End Intersection. Export Intersection. Module Transposition. Definition create := [i,j,a:E] (Y (a == i) j (Y (a == j) i a )). Lemma not_i_not_j : (i,j,a:E)(not a==i) -> (not a==j) -> (create i j a) == a. Intros. Unfold create. Apply (Y_if_not H). Symmetry. Apply (Y_if_not H0). Trivial. Save. Lemma i_j_j_i : (i,j,a:E)(create i j a) == (create j i a). Intros. Unfold create. Apply by_cases with a==i. Intros. Apply (Y_if H). Symmetry. Apply by_cases with a == j. Intros. Apply (Y_if H0). Rewrite <- H. Assumption. Intros. Apply (Y_if_not H0). Symmetry. Apply (Y_if H). Trivial. Intros. Apply (Y_if_not H). Apply by_cases with a== j. Intros. Apply (Y_if H0). Symmetry. Apply (Y_if H0). Trivial. Intros. Apply (Y_if_not H0). Apply (Y_if_not H0). Apply (Y_if_not H). Trivial. Save. Lemma i_j_i : (i,j : E)(create i j i) == j. Intros. Unfold create. Assert i==i; Trivial. Apply (Y_if H). Trivial. Save. Lemma i_j_j : (i,j : E)(create i j j) == i. Intros. Rewrite i_j_j_i. Apply i_j_i. Save. Lemma i_i_a : (i,a:E)(create i i a) == a. Intros. Apply by_cases with a == i. Intros. Rewrite H. Apply i_j_j. Intros. Unfold create. Apply (Y_if_not H). Symmetry. Apply (Y_if_not H). Trivial. Save. Lemma surj : (i,j,a:E)(exists [b:E](create i j b) == a). Intros. Apply by_cases with a==i. Intros. Apply exists_intro with j. Rewrite H. Apply i_j_j. Intros. Apply by_cases with a==j. Intros. Apply exists_intro with i. Rewrite H0. Apply i_j_i. Intros. Apply exists_intro with a. Apply not_i_not_j. Assumption. Assumption. Save. Lemma involutive : (i,j,a:E)(create i j (create i j a)) == a. Intros. Apply by_cases with a==i. Intros. Rewrite H. Rewrite i_j_i. Apply i_j_j. Apply by_cases with a==j. Intros. Rewrite H. Rewrite i_j_j. Apply i_j_i. Intros. Pose (not_i_not_j H0 H). Rewrite e. Assumption. Save. Lemma inj : (i,j,a,b:E)(create i j a) == (create i j b) -> a == b. Intros. Transitivity (create i j (create i j a)). Symmetry; Apply involutive. Rewrite H. Apply involutive. Save. End Transposition. Module Function. Definition axioms := [f:E] (A (x:E)(inc x f) -> (pair (pr1 x) (pr2 x)) == x (x,y:E)(inc x f) -> (inc y f) -> (pr1 x) == (pr1 y) -> x == y ). Definition domain [f:E] := (Image.create f pr1). Definition range [f:E] := (Image.create f pr2). Definition defined := [f,x:E] (A (axioms f) (inc x (domain f)) ). Lemma sub_axioms : (f,g:E)(axioms g) -> (sub f g) -> (axioms f). Intros. NewInduction H. Unfold sub in H0. Unfold axioms; Expand. Save. Lemma sub_domain : (f,g:E)(sub f g) -> (sub (domain f) (domain g)). Intros. Unfold sub. Unfold domain. Unfold sub in H. Intros. LetTac K := (Image.ex H0). NewInduction K. NewInduction H1. Rewrite <- H2. Apply Image.incl. Auto. Save. Lemma sub_range : (f,g:E)(sub f g) -> (sub (range f) (range g)). Intros. Unfold sub. Unfold range. Unfold sub in H. Intros. LetTac K:= (Image.ex H0). NewInduction K. NewInduction H1. Rewrite <- H2. Apply Image.incl. Auto. Save. Lemma range_inc : (f,z:E)(axioms f)-> (exists [y:E](A (inc y (domain f)) (V y f) == z)) -> (inc z (range f)). Intros. NewInduction H0. Expand. Unfold range. Apply Image.show_inc. Apply exists_intro with (pair x z). Expand. Apply V_inc. Unfold domain in H0. Pose (Image.ex H0). NewInduction e; Expand. Apply exists_intro with (pr2 x0). Rewrite <- H3. Unfold axioms in H. Expand. Rewrite H. Assumption. Assumption. Auto. Apply pr2_pair. Save. Lemma defined_lem : (f,x:E)(axioms f) -> (defined f x) -> (inc (pair x (V x f)) f). Intros. Unfold axioms in H. Unfold defined in H0. Expand. Unfold domain in H1. LetTac K := (Image.ex H1). NewInduction K. NewInduction H3. Assert (exists [y:E](inc (pair x y) f)). EApply exists_intro with (pr2 x0). Rewrite <- H4. Rewrite H. Assumption. Assumption. LetTac K := (choose_pr H5). Assumption. Save. Lemma lem1 : (f,x:E)(axioms f) -> (inc x f) -> x == (pair (pr1 x) (V (pr1 x) f)). Intros. Unfold axioms in H. Expand. LetTac z := (pr1 x). Assert (exists [y:E](inc (pair z y) f)). Apply exists_intro with (pr2 x). Unfold z. Rewrite H. Assumption. Assumption. LetTac K := (choose_pr H2). Assert (inc (pair z (V z f)) f). Assumption. Apply H1. Assumption. Assumption. Rewrite pr1_pair. Trivial. Save. Lemma lem2 : (f,x:E)(axioms f) -> (inc x f) -> (inc (pr1 x) (domain f)). Intros. Unfold domain. Apply Image.incl. Assumption. Save. Lemma pr2_V : (f,x:E)(axioms f) -> (inc x f) -> (pr2 x) == (V (pr1 x) f). Intros. Pose (lem1 H H0). LetTac a:=(pr1 x). Rewrite -> e. Rewrite -> pr2_pair. Trivial. Save. Lemma range_ex : (f,y:E)(axioms f) -> (inc y (range f)) -> (exists [x:E](A (inc x (domain f)) (V x f) == y)). Intros. Unfold range in H0. Pose (Image.ex H0); NewInduction e; Expand. Assert (axioms f). Assumption. Unfold axioms in H; Expand. Pose (H x H1). LetTac a := (pr1 x). LetTac b := (pr2 x). Apply exists_intro with a. Expand. Unfold a; Apply lem2; Auto. Assert x == (pair a (V a f)). Unfold a. Apply lem1; Auto. Rewrite <- H2. Unfold b. Rewrite H5. Symmetry; Apply pr2_pair. Save. Lemma function_sub : (f,g:E)(axioms f) -> (axioms g) -> ((x:E)(defined f x) -> (defined g x)) -> ((x:E)(defined f x) -> (V x f) == (V x g)) -> (sub f g). Intros. Unfold sub. Intros. LetTac K := (lem1 H H3). Assert (defined f (pr1 x)). Unfold defined; Expand. Unfold domain. Apply Image.incl. Assumption. Assert (V (pr1 x) f) == (V (pr1 x) g). Apply H2. Assumption. Rewrite K. Assert (defined g (pr1 x)). Apply H1. Assumption. Unfold defined in H6. Expand. Unfold domain in H7. LetTac K1 := (Image.ex H7). NewInduction K1. NewInduction H8. Unfold axioms in H0. LetTac K1 := (lem1 H6 H8). Rewrite H9 in K1. Rewrite H5. Rewrite <- K1. Assumption. Save. Lemma function_extensionality : (f,g:E)(axioms f) -> (axioms g) -> ((x:E)(defined f x) -> (defined g x)) -> ((x:E)(defined g x) -> (defined f x)) -> ((x:E)(defined f x) -> (V x f) == (V x g)) -> f == g. Intros. Apply extensionality. Apply function_sub; Auto. Apply function_sub; Auto. Intros. Symmetry. Apply H3. Apply H2. Assumption. Save. Definition inverse_image := [a,f:E] (Z (domain f) [x:E](inc (V x f) a)). Lemma inverse_image_sub : (a,f:E) (sub (inverse_image a f) (domain f)). Intros. Unfold inverse_image. Apply Z_sub. Save. Lemma inverse_image_inc : (a,f,x:E) (inc x (domain f)) -> (inc (V x f) a) -> (inc x (inverse_image a f)). Intros. Unfold inverse_image. Apply Z_inc. Assumption. Assumption. Save. Lemma inverse_image_pr : (a,f,x:E)(inc x (inverse_image a f)) -> (inc (V x f) a). Intros. Unfold inverse_image in H. Ztac. Save. Definition create := [x:E;p:E -> E] (Image.create x [y:E](pair y (p y))). Lemma elt_rewrite : (x:E; p: E -> E; y:E) (inc y (create x p)) -> y == (pair (pr1 y) (p (pr1 y))). Intros. Unfold create in H. Pose (Image.ex H). NewInduction e. Expand. Assert (pr1 y) == x0. Rewrite <- H1. Apply pr1_pair. Rewrite H2. Auto. Save. Lemma create_axioms : (p:E-> E; x:E)(axioms (create x p)). Intros. Unfold axioms; Expand. Intros. Apply pair_recov. Unfold create in H. Pose (Image.ex H). NewInduction e. Expand. Rewrite <- H1. Apply pair_is_pair. Intros. Unfold create in H. Unfold create in H0. Pose (Image.ex H). Pose (Image.ex H0). NewInduction e. NewInduction e0. Expand. Rewrite <- H5. Assert x1 == x2. Transitivity (pr1 x0). Rewrite <- H5. Symmetry; Apply pr1_pair. Rewrite H1. Rewrite <- H4. Apply pr1_pair. Rewrite H6; Assumption. Save. Lemma create_inc : (x,y:E; hyp : (inc y x); p: E -> E; z:E) (pair y (p y)) == z -> (inc z (create x p)). Intros. Unfold create. Apply Image.show_inc. Apply exists_intro with y; Expand. Save. Lemma create_domain : (x:E;p:E -> E)(domain (create x p)) == x. Intros. Unfold domain. Apply extensionality; Unfold sub; Intros. Pose (Image.ex H); NewInduction e; Expand. Unfold create in H0; Pose (Image.ex H0); NewInduction e; Expand. Rewrite <- H1. Assert (pr1 x1) == x2. Rewrite <- H3; Apply pr1_pair. Rewrite H4; Auto. Apply Image.show_inc. Apply exists_intro with (pair x0 (p x0)). Expand. Apply (create_inc H); Auto. Apply pr1_pair. Save. Lemma create_V_apply : (x:E; p: E-> E; y,z:E) (inc y x) -> (p y) == z -> (V y (create x p)) == z. Intros. Assert (inc (pair y (V y (create x p))) (create x p)). Apply V_inc. Apply exists_intro with (p y). Apply (create_inc H). Trivial. Trivial. Assert (axioms (create x p)). Apply create_axioms. Unfold axioms in H2; Expand. Assert (pair y (V y (create x p))) == (pair y z). Apply H3. Apply V_inc. Apply exists_intro with (p y). Apply (create_inc H). Trivial. Trivial. Apply (create_inc H). Rewrite H0; Trivial. Rewrite pr1_pair. Rewrite pr1_pair. Trivial. Transitivity (pr2 (pair y z)). Rewrite <- H4. Symmetry; Apply pr2_pair. Apply pr2_pair. Save. Lemma create_V_rewrite : (x:E; p: E -> E; y: E) (inc y x) -> (V y (create x p)) == (p y). Intros. Apply create_V_apply; Auto. Save. Lemma create_range : (p:E-> E; x:E)(range (create x p)) == (Image.create x p). Intros. Unfold range. Apply extensionality; Unfold sub; Intros. Pose (Image.ex H); NewInduction e; Expand. Apply Image.show_inc. Unfold create in H0. Pose (Image.ex H0); NewInduction e; Expand. Apply exists_intro with x2. Expand. Rewrite <- H1. Rewrite <- H3. Symmetry; Apply pr2_pair. Pose (Image.ex H); NewInduction e; Expand. Apply Image.show_inc. Apply exists_intro with (pair x1 x0). Expand. Apply (create_inc H0). Rewrite H1. Trivial. Apply pr2_pair. Save. Lemma create_recovers : (f:E)(axioms f) -> (create (domain f) [x:E](V x f)) == f. Intros. Apply function_extensionality. Apply create_axioms. Assumption. Intros. Unfold defined in H0. Expand. Unfold defined. Expand. Rewrite create_domain in H1. Assumption. Intros. Unfold defined in H0. Expand. Unfold defined; Expand. Apply create_axioms. Rewrite create_domain. Assumption. Intros. Unfold defined in H0; Expand. Rewrite create_domain in H1. Apply create_V_apply; Auto. Save. Lemma create_V_defined : (x:E; p: E -> E; y: E) (defined (create x p) y) -> (V y (create x p)) == (p y). Intros. Apply create_V_apply. Unfold defined in H. Expand. Rewrite create_domain in H0. Assumption. Trivial. Save. Lemma create_extensionality : (a,b:E; f,g:E1)a==b -> ((x:E)(inc x a) -> (inc x b) -> (f x) == (g x)) -> (create a f) == (create b g). Intros. Assert (axioms (create a f)). Apply create_axioms. Assert (axioms (create b g)). Apply create_axioms. Apply function_extensionality; Auto. Unfold defined; Intros. Expand. Rewrite -> create_domain. Rewrite <- H. Rewrite -> create_domain in H4. Assumption. Unfold defined. Intros; Expand. Rewrite -> create_domain. Rewrite -> create_domain in H4. Rewrite -> H. Assumption. Intros. Assert (inc x a). Unfold defined in H3. Expand. Rewrite -> create_domain in H4; Assumption. Repeat Rewrite -> create_V_rewrite. Apply H0. Assumption. Rewrite <- H. Assumption. Rewrite <- H. Assumption. Assumption. Save. Lemma create_create : (a:E; f:E1)(create a [x:E](V x (create a f))) == (create a f). Intros. Apply create_extensionality. Trivial. Intros. Apply create_V_rewrite. Assumption. Save. Definition composable := [f,g:E] (A (axioms f) (A (axioms g) (sub (range g) (domain f)) )). Definition compose := [f,g:E] (create (inverse_image (domain f) g) [y:E](V (V y g) f)). Lemma compose_axioms : (f,g:E)(axioms (compose f g)). Intros. Unfold compose. Apply create_axioms. Save. Lemma compose_domain : (f,g:E) (domain (compose f g)) == (inverse_image (domain f) g). Intros. Unfold compose. Rewrite create_domain. Trivial. Save. Lemma composable_domain : (f,g:E)(composable f g) -> (domain (compose f g)) == (domain g). Intros. Unfold compose. Rewrite create_domain. Apply extensionality. Apply inverse_image_sub. Unfold sub; Intros. Apply inverse_image_inc. Assumption. Unfold composable in H. Expand. Apply H2. Apply range_inc. Assumption. Apply exists_intro with x. Expand. Save. Lemma compose_ev : (x,f,g:E)(inc x (domain (compose f g))) -> (V x (compose f g)) == (V (V x g) f). Intros. Unfold compose. Unfold compose in H. Rewrite create_domain in H. Apply create_V_apply. Assumption. Trivial. Save. Definition identity [x:E] := (create x [y:E]y). Lemma identity_axioms : (x:E)(axioms (identity x)). Intros; Unfold identity; Apply create_axioms. Save. Lemma identity_domain : (x:E)(domain (identity x)) == x. Intros; Unfold identity; Rewrite create_domain; Trivial. Save. Lemma identity_ev : (x,a:E)(inc x a) -> (V x (identity a)) == x. Intros. Unfold identity. Apply create_V_apply; Auto. Save. End Function. Syntactic Definition L := Function.create. Module Transformation. Definition covers := [a,b:E; f:E -> E](x:E)(inc x b) -> (exists [y:E](A (inc y a) (f y) == x)). Definition injects := [a:E; f:E-> E](x,y:E)(inc x a) -> (inc y a) -> (f x) == (f y) -> x == y. Definition inverse := [a:E; f:E -> E;y:E](choose [x:E] (A (inc x a) (f x) == y)). Definition axioms := [a,b:E; f:E -> E](x:E)(inc x a) -> (inc (f x) b). Lemma compose_axioms : (a,b,c:E;f,g: E->E)(axioms b c f) -> (axioms a b g) -> (axioms a c [x:E](f (g x))). Intros. Unfold axioms. Intros. Unfold axioms in H. Unfold axioms in H0. Auto. Save. Lemma identity_axioms : (a:E)(axioms a a [x:E]x). Intros. Unfold axioms. Intros. Assumption. Save. Definition surjective := [a,b:E;f: E->E] (A (axioms a b f) (covers a b f) ). Lemma surjective_inverse_axioms : (a,b:E; f:E1)(surjective a b f) -> (axioms b a (inverse a f)). Intros. Unfold axioms. Intros. Unfold inverse. Unfold surjective in H; Expand. Unfold covers in H1; Expand. Pose (H1 x H0). Pose (choose_pr e). Expand. Save. Lemma surjective_inverse_right : (a,b:E; f:E1; x:E)(surjective a b f) -> (inc x b) -> (f (inverse a f x)) == x. Intros. Unfold inverse. Unfold surjective in H; Expand. Unfold covers in H1; Expand. Pose (H1 x H0). Pose (choose_pr e). Expand. Save. Definition injective := [a,b:E;f:E->E] (A (axioms a b f) (injects a f) ). Definition bijective := [a,b:E;f:E-> E] (A (axioms a b f) (A (surjective a b f) (injective a b f) )). Definition are_inverse := [a,b:E; f,g:E1] (A (axioms a b f) (A (axioms b a g) (A (x:E)(inc x a) -> (g (f x)) == x (y:E)(inc y b) -> (f (g y)) == y ))). Lemma bijective_inverse : (a,b:E; f:E1)(bijective a b f) -> (are_inverse a b f (inverse a f)). Intros. Unfold are_inverse; Expand. Unfold bijective in H; Expand. Apply surjective_inverse_axioms. Unfold bijective in H; Expand. Intros. Unfold bijective in H; Expand. Unfold injective in H2. Expand. Apply H3. Assert (axioms b a (inverse a f)). Apply surjective_inverse_axioms; Auto. Unfold axioms in H4. Apply H4. Apply H2. Assumption. Assumption. Pose surjective_inverse_right. Assert (inc (f x) b). Apply H2; Auto. Pose (e ? ? ? ? H1 H4). Assumption. Intros. Unfold bijective in H; Expand. Apply surjective_inverse_right with b. Assumption. Assumption. Save. Lemma inverse_bijective : (a,b:E; f,g:E1)(are_inverse a b f g) -> (bijective a b f). Intros. Unfold bijective. Unfold are_inverse in H. Expand. Unfold surjective; Expand. Unfold covers. Intros. Apply exists_intro with (g x). Expand. Unfold injective; Expand. Unfold injects; Intros. Rewrite <- H1. Rewrite <- H5. Rewrite -> H1; Auto. Assumption. Save. End Transformation. Module Map. Definition axioms := [a,b,f:E] (A (Function.axioms f) (A (Function.domain f) == a (sub (Function.range f) b) )). Lemma compose_axioms : (a,b,c,f,g: E)(axioms b c f) -> (axioms a b g) -> (axioms a c (Function.compose f g)). Intros. Unfold axioms in H H0; Expand. Assert (Function.composable f g). Unfold Function.composable. Expand. Rewrite H2; Assumption. Unfold axioms; Expand. Apply Function.compose_axioms. Rewrite Function.composable_domain; Auto. Unfold sub; Intros. Assert (Function.axioms (Function.compose f g)). Apply Function.compose_axioms. Pose (Function.range_ex H7 H6). NewInduction e; Expand. Pose (Function.compose_ev H8). Rewrite H9 in e. Rewrite e. Apply H4. Apply Function.range_inc. Assumption. Apply exists_intro with (V x0 g); Expand. Unfold Function.composable in H5; Expand. Apply H11. Apply Function.range_inc. Assumption. Apply exists_intro with x0; Expand. Assert (Function.domain (Function.compose f g)) == (Function.domain g). Apply Function.composable_domain. Unfold Function.composable; Expand. Rewrite <- H12. Assumption. Save. Lemma identity_axioms : (a:E)(axioms a a (Function.identity a)). Intros. Unfold axioms; Expand. Apply Function.identity_axioms. Apply Function.identity_domain. Unfold sub; Intros. Assert (Function.axioms (Function.identity a)). Apply Function.identity_axioms. Pose (Function.range_ex H0 H). NewInduction e; Expand. Rewrite Function.identity_domain in H1. Rewrite Function.identity_ev in H2. Rewrite <- H2; Assumption. Assumption. Save. Definition surjective := [a,b,f: E] (A (axioms a b f) (Transformation.covers a b [x:E](V x f)) ). Definition injective := [a,b,f:E] (A (axioms a b f) (Transformation.injects a [x:E](V x f)) ). Definition bijective := [a,b,f:E] (A (axioms a b f) (A (surjective a b f) (injective a b f) )). End Map. Module Bounded. Definition property := [p:EP; x:E](y:E) (A (p y) -> (inc y x) (inc y x) -> (p y)). Definition axioms := [p:E -> Prop](exists (property p)). Definition create := [p:E->Prop] (choose (property p)). Lemma criterion : (p:E -> Prop)(exists [x:E]((y:E)(p y) -> (inc y x))) -> (axioms p). Intros. NewInduction H. Unfold axioms. EApply exists_intro with (Z x p). Unfold property. Intros; Expand; Intros. Apply Z_inc. Apply H; Auto. Auto. Apply Z_pr with x. Assumption. Save. Lemma lem1 : (p:E-> Prop; y:E)(axioms p) -> (inc y (create p)) -> (p y). Intros. Unfold create in H0. Unfold axioms in H. Pose (choose_pr H). Unfold property in H0. Unfold property in (Type of p0). Pose (p0 y). Expand. Save. Lemma lem2 : (p:E -> Prop; y:E)(axioms p) -> (p y) -> (inc y (create p)). Intros. Unfold create. Unfold axioms in H. Pose (choose_pr H). LetTac K:= (choose (property p)). Unfold property in (Type of p0). Pose (p0 y); Expand. Save. End Bounded. Module Quotient. Definition is_part := [a:E; r: E -> E -> Prop; y:E] (A (sub y a) (A (x,z:E)(inc x y) -> (r x z) -> (inc z a) -> (inc z y) (x,z : E)(inc x y) -> (r z x) -> (inc z a) -> (inc z y) )). Definition is_class := [a:E; r: E -> E -> Prop; y:E] (A (is_part a r y) (A (nonempty y) (z:E)(is_part a r z) -> (nonempty (Intersection.intersection2 y z)) -> (sub y z) )). Lemma lem1 : (a:E; r: E -> E -> Prop)(is_part a r a). Intros. Unfold is_part; Expand. Unfold sub; Intros; Auto. Save. Definition parts_containing := [a:E; r:E -> E -> Prop; y:E] (Z (Powerset.powerset a) [z:E](A (is_part a r z) (inc y z))). Definition class_of := [a:E; r: E -> E -> Prop; y:E] (Intersection.intersection (parts_containing a r y)). Lemma inc_parts_containing : (a:E; r: E -> E -> Prop; y,z:E) (inc y z) -> (is_part a r z) -> (inc z (parts_containing a r y)). Intros. Unfold parts_containing. Apply Z_inc. Apply Powerset.powerset_inc. Unfold is_part in H0; Expand. Expand. Save. Lemma class_of_origin : (a:E; r: E-> E-> Prop; y:E) (inc y a) -> (inc y (class_of a r y)). Intros. Unfold class_of. Apply intersection_inc. Apply nonempty_intro with a. Apply inc_parts_containing. Assumption. Apply lem1. Intros. Unfold parts_containing in H0. Pose (Z_pr H0). Expand; Auto. Save. Lemma class_of_sub : (a:E; r: E -> E -> Prop; y,z:E) (inc y z) -> (is_part a r z) -> (sub (class_of a r y) z). Intros. Unfold class_of. Apply intersection_sub. Apply inc_parts_containing; Auto. Save. Lemma class_of_part : (a:E; r: E -> E -> Prop; y:E) (inc y a) -> (is_part a r (class_of a r y)). Intros. Unfold is_part; Expand; Intros. Unfold class_of. Apply Intersection.intersection_sub. Unfold parts_containing. Apply Z_inc. Apply Powerset.powerset_inc. Unfold sub; Intros; Auto. Expand. Apply lem1. Unfold class_of. Apply Intersection.intersection_inc. Apply nonempty_intro with a. Unfold parts_containing. Apply Z_inc. Apply Powerset.powerset_inc; Unfold sub; Intros; Auto. Expand. Apply lem1. Intros. Assert (is_part a r y0). Unfold parts_containing in H3. Pose _:=(Z_pr H3). Expand. Unfold is_part in H4; Expand. Apply H5 with x. Apply Intersection.intersection_forall with (parts_containing a r y). Exact H0. Assumption. Assumption. Assumption. Unfold class_of. Apply Intersection.intersection_inc. Apply nonempty_intro with a. Unfold parts_containing. Apply Z_inc. Apply Powerset.powerset_inc; Unfold sub; Intros; Auto. Expand. Apply lem1. Intros. Assert (is_part a r y0). Unfold parts_containing in H3. Pose _:=(Z_pr H3). Expand. Unfold is_part in H4; Expand. Apply H6 with x. Apply Intersection.intersection_forall with (parts_containing a r y). Exact H0. Assumption. Assumption. Assumption. Save. Lemma class_of_class : (a:E; r: E -> E -> Prop; y:E) (inc y a) -> (is_class a r (class_of a r y)). Intros. Unfold is_class; Expand; Intros. Apply class_of_part. Assumption. Apply nonempty_intro with y. Unfold class_of. Apply Intersection.intersection_inc. Apply nonempty_intro with a. Unfold parts_containing; Apply Z_inc; Expand. Apply Powerset.powerset_inc; Unfold sub; Intros; Auto. Apply lem1. Intros. Unfold parts_containing in H0. Pose _:=(Z_pr H0). Expand. Unfold class_of. Apply Intersection.intersection_sub. Unfold parts_containing. Apply Z_inc. Apply Powerset.powerset_inc. Unfold is_part in H0. Expand. Expand. NewInduction H1. Pose (Intersection.intersection2_first H1). Pose (Intersection.intersection2_second H1). Apply excluded_middle; Unfold not; Intros. Pose (Z (class_of a r y) [v:E](inc v z) -> False). Assert (is_part a r e). Unfold is_part. Expand. Apply sub_trans with (class_of a r y). Unfold e; Apply Z_sub. Unfold sub; Intros. Unfold class_of in H3. Apply Intersection.intersection_forall with (parts_containing a r y). Assumption. Unfold parts_containing. Apply Z_inc. Apply Powerset.powerset_inc; Unfold sub; Intros; Auto. Expand; Try Apply lem1; Auto. Intros. Unfold e; Ztac. Unfold class_of. Apply intersection_inc; Intros. Apply nonempty_intro with a. Unfold parts_containing; Ztac; Expand. Apply Powerset.powerset_inc; Unfold sub; Intros; Auto. Apply lem1. Unfold parts_containing in H6. Pose (Z_pr H6). Expand. Assert (inc x (class_of a r y)). Assert (sub e (class_of a r y)). Unfold e; Apply Z_sub. Apply H9. Assumption. Unfold class_of in H9. Assert (inc x y1). Apply intersection_forall with (parts_containing a r y). Assumption. Unfold parts_containing; Apply Z_inc. Apply powerset_inc. Unfold is_part in H7; Expand; Auto. Expand. Unfold is_part in H7; Expand. Apply H11 with x; Assumption. Intros. Assert (inc x z). Unfold is_part in H0; Expand. Apply H8 with z0; Auto. Assert (sub e a). Apply sub_trans with (class_of a r y). Unfold e; Apply Z_sub. Apply class_of_sub. Assumption. Apply lem1. Apply H9; Assumption. Unfold e in H3. Pose (Z_pr H3). Apply f; Assumption. Intros. Unfold e; Apply Z_inc. Assert (sub e (class_of a r y)). Unfold e; Apply Z_sub. Apply H6. Unfold e; Apply Z_inc. Assert (is_part a r (class_of a r y)). Apply class_of_part. Assumption. Unfold is_part in H7. Expand. Apply H9 with x. Apply H6. Assumption. Assumption. Assumption. Intros. Assert (inc x z). Unfold is_part in H0; Expand. Apply H8 with z0. Assumption. Assumption. Assert (sub e a). Apply sub_trans with (class_of a r y). Unfold e; Apply Z_sub. Apply class_of_sub. Assumption. Apply lem1. Apply H10; Assumption. Unfold e in H3. Pose (Z_pr H3). Apply f; Assumption. Intros. Assert (inc x z). Unfold is_part in H0; Expand. Apply H7 with z0; Auto. Assert (sub e a). Apply sub_trans with (class_of a r y). Unfold e; Apply Z_sub. Apply class_of_sub. Assumption. Apply lem1. Apply H9; Auto. Unfold e in H3. Pose (Z_pr H3). Apply f; Auto. Assert (sub (class_of a r y) e). Apply class_of_sub. Unfold e; Apply Z_inc. Apply class_of_origin; Auto. Assumption. Assumption. Assert (inc y0 e). Apply H4. Assumption. Unfold e in H5. Pose (Z_pr H5). Apply f; Auto. Save. Lemma class_rep_inc : (a:E; r: E -> E -> Prop;x:E)(is_class a r x) -> (inc (rep x) x). Intros. Unfold is_class in H. Expand. Unfold rep. Apply choose_pr. NewInduction H0. Apply exists_intro with y; Auto. Save. Lemma class_eq_class_of : (a:E; r: E -> E -> Prop;y:E) (is_class a r y) -> ((x:E)(inc x y) -> (class_of a r x) == y). Intros. Apply extensionality. Apply class_of_sub; Auto. Unfold is_class in H; Expand; Auto. Unfold is_class in H. Expand. Apply H2. Apply class_of_part. Unfold is_part in H; Expand. Apply nonempty_intro with x. Apply intersection2_inc; Auto. Apply class_of_origin. Unfold is_part in H; Expand. Save. Lemma intersecting_classes_eq : (a:E; r: E -> E -> Prop; x,y:E)(is_class a r x) -> (is_class a r y) -> (nonempty (intersection2 x y)) -> x == y. Intros. Pose (class_eq_class_of H). Pose (class_eq_class_of H0). NewInduction H1. Pose (intersection2_first H1). Pose (intersection2_second H1). Pose (e ? i). Pose (e0 ? i0). Rewrite <- e1. Rewrite <- e2. Trivial. Save. Lemma intersecting_classes_of_eq : (a:E; r: E -> E -> Prop; x,y:E) (inc x a) -> (inc y a) -> (nonempty (intersection2 (class_of a r x) (class_of a r y))) -> (class_of a r x) == (class_of a r y). Intros. Pose class_of_class. Apply intersecting_classes_eq with a r; Auto. Save. Definition quotient := [a:E; r : E -> E -> Prop] (Z (powerset a) [y:E](is_class a r y)). Lemma in_quotient_is_class : (a:E; r: E -> E -> Prop; x:E) (inc x (quotient a r)) -> (is_class a r x). Intros. Unfold quotient in H. Pose (Z_pr H); Auto. Save. Lemma is_class_in_quotient : (a:E; r: E -> E -> Prop; x:E) (is_class a r x) -> (inc x (quotient a r)). Intros. Unfold quotient; Apply Z_inc. Apply powerset_inc. Unfold is_class in H. Expand. Unfold is_part in H; Expand; Auto. Assumption. Save. Lemma class_of_in_quotient : (a:E; r: E -> E -> Prop; x:E) (inc x a) -> (inc (class_of a r x) (quotient a r)). Intros. Unfold quotient; Apply Z_inc. Apply powerset_inc. Apply class_of_sub; Auto. Apply lem1. Apply class_of_class; Auto. Save. Lemma inc_class_of : (a:E; r: E -> E -> Prop; x,y:E) (inc x a) -> (inc y a) -> (r x y) -> (inc x (class_of a r y)). Intros. Assert (is_part a r (class_of a r y)). Apply class_of_part. Assumption. Unfold is_part in H2. Expand. Pose _:=class_of_origin. Apply H4 with y; Auto. Save. Lemma related_classes_eq : (a:E; r: E -> E -> Prop; x,y:E) (inc x a) -> (inc y a) -> (r x y) -> (class_of a r x) == (class_of a r y). Intros. Apply intersecting_classes_of_eq; Auto. Apply nonempty_intro with x. Pose class_of_origin. Pose inc_class_of. Apply intersection2_inc; Auto. Save. Definition class_in := [q,x:E](choose [y:E](A (inc y q) (inc x y))). Lemma class_of_eq_class: (a:E; r: E -> E -> Prop; x:E) (inc x a) -> (class_of a r x) == (class_in (quotient a r) x). Intros. Apply class_eq_class_of. Assert (inc (class_in (quotient a r) x) (quotient a r)). Unfold class_in. Assert (exists [y:E](A (inc y (quotient a r)) (inc x y))). Apply exists_intro with (class_of a r x). Expand. Apply class_of_in_quotient; Auto. Apply class_of_origin; Auto. Pose (choose_pr H0). Expand. Unfold quotient in H0. Pose (Z_pr H0). Assumption. Assert (exists [y:E](A (inc y (quotient a r)) (inc x y))). Apply exists_intro with (class_of a r x). Expand. Apply class_of_in_quotient; Auto. Apply class_of_origin; Auto. Pose (choose_pr H0). Expand. Save. Lemma class_of_rep : (a:E; r: E -> E -> Prop; x:E) (inc x (quotient a r)) -> (class_of a r (rep x)) == x. Intros. Apply class_eq_class_of. Apply in_quotient_is_class; Auto. Assert (is_class a r x). Apply in_quotient_is_class; Auto. Unfold is_class in H0; Expand. Unfold rep. NewInduction H1. Apply choose_pr. Apply exists_intro with y. Assumption. Save. Definition is_eq_reln := [a:E; r:E -> E -> Prop] (A (x:E)(inc x a) -> (r x x) (A (x,y:E)(inc x a) -> (inc y a) -> (r x y) -> (r y x) (x,y,z:E)(inc x a) -> (inc y a) -> (inc z a) -> (r x y) -> (r y z) -> (r x z) )). Definition equivalent := [a:E; r:E -> E -> Prop; x,y:E] (A (inc x a) (A (inc y a) (class_of a r x) == (class_of a r y) )). Lemma equivalent_symm : (a:E; r: E -> E -> Prop; x,y:E)(equivalent a r x y) -> (equivalent a r y x). Intros. Unfold equivalent in H. Unfold equivalent. Expand. Save. Lemma equivalent_refl : (a:E; r: E -> E -> Prop; x:E)(inc x a) -> (equivalent a r x x). Intros; Unfold equivalent; Expand. Save. Lemma equivalent_trans : (a:E; r: E -> E -> Prop; x,y,z:E)(equivalent a r x y)-> (equivalent a r y z) -> (equivalent a r x z). Unfold equivalent; Intros; Expand. Transitivity (class_of a r y); Auto. Save. Lemma equivalent_is_eq_reln : (a:E; r: E -> E -> Prop)(is_eq_reln a (equivalent a r)). Intros. Unfold is_eq_reln; Expand; Intros. Apply equivalent_refl; Auto. Apply equivalent_symm; Auto. Apply equivalent_trans with y; Auto. Save. Lemma related_equivalent : (a:E; r: E -> E -> Prop; x,y:E)(inc x a) -> (inc y a) -> (r x y) -> (equivalent a r x y). Intros. Unfold equivalent; Expand. Apply intersecting_classes_of_eq; Auto. Apply nonempty_intro with x. Apply intersection2_inc. Apply class_of_origin; Auto. Apply inc_class_of; Auto. Save. Lemma equivalent_related : (a:E; r:E -> E -> Prop; x,y:E)(is_eq_reln a r) -> (equivalent a r x y) -> (r x y). Intros. Unfold is_eq_reln in H; Expand. Pose z:=(Z a [u:E](r x u)). Assert (inc y z). Unfold equivalent in H0; Expand. Assert (sub (class_of a r y) z). Rewrite <- H4. Apply class_of_sub. Unfold z; Ztac. Unfold is_part; Expand. Unfold z; Apply Z_sub. Intros. Unfold z; Ztac. Apply H2 with x0. Assumption. Assert (sub z a); [ Unfold z; Apply Z_sub | Apply H8; Auto ]. Auto. Unfold z in H5; Ztac. Assumption. Intros. Unfold z; Ztac. Apply H2 with x0; Auto. Assert (sub z a); [ Unfold z; Apply Z_sub | Apply H8; Auto ]. Unfold z in H5; Ztac. Apply H1; Auto. Assert (sub z a); [ Unfold z; Apply Z_sub | Apply H8; Auto ]. Apply H5. Apply class_of_origin. Assumption. Unfold z in H3; Ztac. Save. Lemma equivalent_to_rep : (a:E; r: E -> E -> Prop; x:E)(inc x a) -> (equivalent a r x (rep (class_of a r x))). Intros. Unfold equivalent; Expand. Assert (sub (class_of a r x) a). Apply class_of_sub; Auto. Apply lem1. Apply H0. Apply nonempty_rep. Apply nonempty_intro with x; Apply class_of_origin. Assumption. Apply intersecting_classes_of_eq. Assumption. Assert (sub (class_of a r x) a). Pose _:=lem1; Apply class_of_sub; Auto. Apply H0. Apply nonempty_rep. Apply nonempty_intro with x; Apply class_of_origin. Assumption. Apply nonempty_intro with (rep (class_of a r x)). Apply intersection2_inc. Apply nonempty_rep. Apply nonempty_intro with x; Apply class_of_origin. Assumption. Apply class_of_origin. Assert (sub (class_of a r x) a). Apply class_of_sub. Auto. Apply lem1. Apply H0. Apply nonempty_rep. Apply nonempty_intro with x. Apply class_of_origin. Assumption. Save. Lemma equivalent_universal : (a:E; r,s:E -> E -> Prop)(is_eq_reln a s) -> ((x,y:E)(inc x a) -> (inc y a) -> (r x y) -> (s x y)) -> ((x,y:E)(equivalent a r x y) -> (s x y)). Intros. Pose z:=(Z a [u:E](s x u)). Assert (sub z a). Unfold z; Apply Z_sub. Unfold sub in H2. Unfold equivalent in H1; Expand. Assert (sub (class_of a r y) z). Rewrite <- H4. Apply class_of_sub. Unfold z; Ztac. Unfold is_eq_reln in H; Expand. Unfold is_part; Expand. Intros. Unfold z; Ztac. Unfold is_eq_reln in H; Expand. Apply H9 with x0; Auto. Unfold z in H5; Ztac. Intros. Unfold z; Ztac. Unfold is_eq_reln in H; Expand. Apply H9 with x0; Auto. Unfold z in H5; Ztac. Assert (inc y z). Apply H5; Apply class_of_origin. Auto. Unfold z in H6; Ztac. Save. Definition quotient_endo := [q:E; endo : E -> E; x:E](class_in q (endo (rep x))). Definition endo_within := [a:E; endo : E -> E](x:E)(inc x a) -> (inc (endo x) a). Definition endo_compatible := [a:E; r: E -> E -> Prop; endo: E -> E] (x,y:E)(inc x a) -> (inc y a) -> (r x y) -> (r (endo x) (endo y)). Definition endo_passes_to_quotient := [q:E; endo : E -> E] (x,a:E)(inc x q) -> (inc a x) -> (class_in q (endo a)) == (quotient_endo q endo x). Lemma endo_compatible_passes : (a:E; r: E -> E -> Prop; endo : E -> E) (endo_within a endo) -> (endo_compatible a r endo) -> (endo_passes_to_quotient (quotient a r) endo). Intros. Unfold endo_passes_to_quotient. LetTac q:=(quotient a r). Intros. Assert (is_class a r x). Apply in_quotient_is_class. Assumption. Assert (class_of a r (rep x))==x. Apply class_of_rep. Assumption. Assert (class_of a r a0)==x. Apply class_eq_class_of. Assumption. Assumption. Pose z:=(Z a [u:E](class_in q (endo u))==(quotient_endo q endo x)). Assert (sub z a). Unfold z; Apply Z_sub. Assert (sub (class_of a r (rep x)) z). Apply class_of_sub. Unfold z; Ztac. Unfold is_class in H3. Expand. Unfold is_part in H3; Expand. Apply H3. Apply nonempty_rep. Assumption. Unfold is_part; Expand. Intros. Unfold z; Ztac. Transitivity (class_in q (endo x0)). Unfold q. Assert (inc x0 a). Apply H6; Auto. Rewrite <- class_of_eq_class. Rewrite <- class_of_eq_class. Symmetry. Apply related_classes_eq. Apply H. Assumption. Apply H; Assumption. Apply H0; Auto. Apply H. Auto. Apply H; Auto. Unfold z in H7; Ztac. Intros. Unfold z; Ztac. Transitivity (class_in q (endo x0)). Assert (inc x0 a). Apply H6; Auto. Unfold q. Rewrite <- class_of_eq_class. Rewrite <- class_of_eq_class. Apply related_classes_eq. Apply H; Auto. Apply H; Auto. Apply H0; Auto. Apply H; Auto. Apply H; Auto. Unfold z in H7; Ztac. Assert (inc a0 z). Apply H7. Rewrite -> H4; Auto. Unfold z in H8; Ztac. Save. Definition quotient_op := [q:E; op : E -> E -> E; x,y:E](class_in q (op (rep x) (rep y))). Definition op_within := [a:E; op : E -> E -> E](x,y:E)(inc x a) -> (inc y a) -> (inc (op x y) a). Definition op_left_compatible := [a:E; r: E -> E -> Prop; op : E -> E -> E] (x,y,z: E)(inc x a) -> (inc y a) -> (inc z a)-> (r x z) -> (r (op x y) (op z y)). Definition op_right_compatible := [a:E; r: E -> E -> Prop; op : E -> E -> E] (x,y,z: E)(inc x a) -> (inc y a) -> (inc z a)-> (r y z) -> (r (op x y) (op x z)). Definition op_passes_to_quotient := [q:E;op : E -> E -> E] (x,y,a,b,c,d:E)(inc x q) -> (inc y q) -> (inc a x) -> (inc b y) -> (class_in q (op a b)) == (quotient_op q op x y). Lemma op_left_very_compatible : (a:E; r: E -> E -> Prop; op : E -> E -> E)(op_within a op) -> (op_left_compatible a r op) -> ((x,b,c,d:E)(inc x (quotient a r)) -> (inc b x) -> (inc c x) -> (inc d a) -> (class_in (quotient a r) (op b d)) == (class_in (quotient a r) (op c d))). Intros. Pose f:=[u:E](op u d). Assert (endo_within a f). Unfold endo_within. Intros. Unfold f. Apply H; Auto. Assert (endo_compatible a r f). Unfold endo_compatible. Intros. Unfold f. Apply H0; Auto. Pose (endo_compatible_passes H5 H6). Unfold endo_passes_to_quotient in (Type of e). Unfold f in (Type of e). Transitivity (quotient_endo (quotient a r) [u:E](op u d) x). Apply e; Auto. Symmetry. Apply e; Auto. Save. Lemma op_right_very_compatible : (a:E; r: E -> E -> Prop; op : E -> E -> E)(op_within a op) -> (op_right_compatible a r op) -> ((x,b,c,d:E)(inc x (quotient a r)) -> (inc b a) -> (inc c x) -> (inc d x) -> (class_in (quotient a r) (op b c)) == (class_in (quotient a r) (op b d))). Intros. Pose f:=[u:E](op b u). Assert (endo_within a f). Unfold endo_within. Intros. Unfold f. Apply H; Auto. Assert (endo_compatible a r f). Unfold endo_compatible. Intros. Unfold f. Apply H0; Auto. Pose (endo_compatible_passes H5 H6). Unfold endo_passes_to_quotient in (Type of e). Unfold f in (Type of e). Transitivity (quotient_endo (quotient a r) [u:E](op b u) x). Apply e; Auto. Symmetry. Apply e; Auto. Save. Lemma op_compatible_passes : (a:E; r: E -> E -> Prop; op : E -> E -> E)(op_within a op) -> (op_left_compatible a r op) -> (op_right_compatible a r op) -> (op_passes_to_quotient (quotient a r) op). Intros. Unfold op_passes_to_quotient; Intros. Unfold quotient_op. Assert (inc (rep x) x). Apply nonempty_rep. Apply nonempty_intro with a0. Assumption. Assert (inc (rep y) y). Apply nonempty_rep; Apply nonempty_intro with b; Auto. Transitivity (class_in (quotient a r) (op a0 (rep y))). Apply op_right_very_compatible with y; Auto. Assert (inc x (powerset a)). Unfold quotient in H2; Ztac. Assert (sub x a). Apply powerset_sub. Assumption. Apply H9. Assumption. Apply op_left_very_compatible with x; Auto. Assert (sub y a). Apply powerset_sub. Unfold quotient in H3; Ztac. Apply H8; Auto. Save. End Quotient. Module Cartesian. Definition in_record := [a:E; f:E1; x:E] (A (is_pair x) (A (inc (pr1 x) a) (inc (pr2 x) (f (pr1 x))) )). Record recordRec [a:E; f:E1]:E := { first : a; second : (f (R first)) }. Definition recordMap := [a:E; f:E1; i:(recordRec a f)](pair (R (first i)) (R (second i))). Lemma in_record_ex : (a:E; f:E1; x:E)(in_record a f x) -> (exT ? [i:(recordRec a f)](recordMap i) == x). Intros. Unfold in_record in H; Expand. Pose u:=(B H0). Assert (R u)==(pr1 x). Unfold u. Apply B_eq. Assert (inc (pr2 x) (f (R u))). Rewrite -> H2; Assumption. Pose v:=(B H3). Pose (!Build_recordRec a f u v). Apply exT_intro with r. Transitivity (pair (R u) (R v)). Trivial. Assert (R v)==(pr2 x). Unfold v. Apply B_eq. Rewrite -> H4. Assert (R u)==(pr1 x); Auto. Rewrite -> H5. Apply pair_recov. Assumption. Save. Lemma in_record_bounded : (a:E; f:E1)(Bounded.axioms (in_record a f)). Intros. Apply Bounded.criterion. Apply exists_intro with (IM (!recordMap a f)). Intros. Apply IM_inc. Apply in_record_ex. Assumption. Save. Definition record := [a:E; f: E1](Bounded.create (in_record a f)). Lemma record_in : (a:E; f:E1; x:E)(inc x (record a f)) -> (in_record a f x). Intros. Unfold record in H. Pose (in_record_bounded a f). Pose (Bounded.lem1 a0 H). Assumption. Save. Lemma record_pr : (a:E; f:E1; x:E)(inc x (record a f)) -> (A (is_pair x) (A (inc (pr1 x) a) (inc (pr2 x) (f (pr1 x))) )). Intros. Pose (record_in H). Assumption. Save. Lemma record_inc : (a:E; f:E1; x:E)(in_record a f x) -> (inc x (record a f)). Intros. Unfold record. Apply Bounded.lem2. Apply in_record_bounded. Assumption. Save. Lemma record_pair_pr : (a:E; f: E1; x,y:E)(inc (pair x y) (record a f)) -> (A (inc x a) (inc y (f x))). Intros. Expand. Pose (record_in H). Unfold in_record in (Type of i); Expand. Rewrite -> pr1_pair in H1. Assumption. Pose (record_in H). Unfold in_record in (Type of i); Expand. Rewrite -> pr1_pair in H2. Rewrite -> pr2_pair in H2. Assumption. Save. Lemma record_pair_inc : (a:E; f:E1; x,y:E)(inc x a) -> (inc y (f x)) -> (inc (pair x y) (record a f)). Intros. Apply record_inc. Unfold in_record; Expand. Apply pair_is_pair. Rewrite -> pr1_pair; Assumption. Rewrite -> pr2_pair; Rewrite -> pr1_pair; Assumption. Save. Definition product := [a,b:E](record a [x:E]b). Lemma product_pr : (a,b,u:E)(inc u (product a b)) -> (A (is_pair u) (A (inc (pr1 u) a) (inc (pr2 u) b) )). Intros. Unfold product in H. Pose (record_pr H). Expand. Save. Lemma product_inc : (a,b,u:E)(is_pair u) -> (inc (pr1 u) a) -> (inc (pr2 u) b) -> (inc u (product a b)). Intros. Unfold product. Apply record_inc. Unfold in_record; Expand. Save. Lemma product_pair_pr : (a,b,x,y:E)(inc (pair x y) (product a b)) -> (A (inc x a) (inc y b)). Intros. Unfold product in H. Pose (record_pair_pr H). Assumption. Save. Lemma product_pair_inc : (a,b,x,y:E)(inc x a) -> (inc y b) -> (inc (pair x y) (product a b)). Intros. Unfold product. Apply record_pair_inc; Auto. Save. End Cartesian. Export Cartesian. Module Function_Set. Definition in_function_set := [a:E; f:E1; u:E] (A (Function.axioms u) (A (Function.domain u) == a (y:E)(inc y a) -> (inc (V y u) (f y)) )). Lemma in_fs_sub_record : (a:E; f:E1; u:E)(in_function_set a f u) -> (sub u (record a f)). Intros. Unfold in_function_set in H; Expand. Unfold sub; Intros. Pose (Function.pr2_V H H2). Assert (Function.axioms u). Assumption. Unfold Function.axioms in H3; Expand. Pose (H3 ? H2). Rewrite <- e0. Apply record_pair_inc. Rewrite <- H0. Apply Function.lem2; Auto. Rewrite -> e. Apply H1. Rewrite <- H0. Apply Function.lem2; Auto. Save. Lemma in_fs_eq_L : (a:E; f:E1; u:E)(in_function_set a f u) -> u == (L a [y:E](V y u)). Intros. Unfold in_function_set in H; Expand. Rewrite <- H0. Symmetry. Apply Function.create_recovers. Assumption. Save. Lemma in_fs_for_L : (a:E; f,v:E1)((y:E)(inc y a) -> (inc (v y) (f y))) -> (in_function_set a f (L a v)). Intros. Unfold in_function_set; Expand. Apply Function.create_axioms. Apply Function.create_domain. Intros. Rewrite -> Function.create_V_rewrite. Apply H; Auto. Assumption. Save. Lemma in_fs_bounded : (a:E; f:E1)(Bounded.axioms (in_function_set a f)). Intros. Apply Bounded.criterion. Apply exists_intro with (powerset (record a f)). Intros. Apply powerset_inc. Apply in_fs_sub_record; Auto. Save. Definition function_set := [a:E; f:E1](Bounded.create (in_function_set a f)). Lemma function_set_iff : (a:E; f:E1; u:E)(inc u (function_set a f)) <-> (in_function_set a f u). Intros. Unfold iff; Expand; Intros. Unfold function_set in H. Apply Bounded.lem1. Apply in_fs_bounded. Assumption. Unfold function_set. Apply Bounded.lem2. Apply in_fs_bounded. Assumption. Save. Lemma function_set_sub_powerset_record : (a:E; f:E1)(sub (function_set a f) (powerset (record a f))). Intros. Unfold sub; Intros. Pose (function_set_iff a f x). Unfold iff in (Type of i); Expand. Pose (H0 H). Apply powerset_inc. Apply in_fs_sub_record; Auto. Save. Lemma function_set_pr : (a:E; f:E1; u:E)(inc u (function_set a f)) -> (A (in_function_set a f u) (A (Function.axioms u) (A (Function.domain u) == a (y:E)(inc y a) -> (inc (V y u) (f y)) ))). Intros. Assert (in_function_set a f u). Pose (function_set_iff a f u). Unfold iff in (Type of i); Expand. Unfold in_function_set in H0; Expand. Unfold in_function_set; Expand. Save. Lemma function_set_inc : (a:E; f:E1; u:E)(Function.axioms u) -> (Function.domain u) == a -> ((y:E)(inc y a) -> (inc (V y u) (f y))) -> (inc u (function_set a f)). Intros. Pose (function_set_iff a f u). Unfold iff in (Type of i); Expand. Apply H3. Unfold in_function_set; Expand. Save. Lemma in_function_set_inc : (a:E; f:E1; u:E)(in_function_set a f u) ->(inc u (function_set a f)). Intros. Pose (function_set_iff a f u). Unfold iff in (Type of i); Expand. Save. End Function_Set. Module Notation. Inductive t : E := Underlying : t | OrderGraph : t | Objects : t | Morphisms : t | Source : t| Target : t| Mapping : t| Comp : t | Id : t | Plus : t | Times : t. Definition G := [i:t; x:E](V (R i) x). Definition create := [f:t -> E](L t (X f)). Lemma get_rewrite : (f:t-> E; i:t)(G i (create f)) == (f i). Intros. Unfold G. Unfold create. Apply Function.create_V_apply. Apply R_inc. Apply X_eq. Apply exT_intro with i; Expand. Save. Lemma get_back : (f:t-> E; i:t; x:E)(f i) == x -> (G i (create f)) == x. Intros. Rewrite -> get_rewrite. Assumption. Save. Lemma extens : (f,g:t-> E)((i:t)(f i) == (g i)) -> (create f) == (create g). Intros. Unfold create. Apply Function.create_extensionality. Trivial. Intros. Unfold X. Apply Yy_if with H0. Symmetry. Apply Yy_if with H0. Symmetry. Apply H. Save. Definition U := [x:E](G Underlying x). End Notation. Export Notation. Module Umorphism. Definition source := [a:E](G Source a). Definition target := [a:E](G Target a). Definition mapping := [a:E](G Mapping a). Definition ev := [a,x:E](V x (mapping a)). Definition create := [x,y:E; f: E1](Notation.create [i:Notation.t]Cases i of Source => x | Target => y | Mapping => (L (U x) f) | _ => emptyset end). Definition realizes := [x,y:E; f:E1; a:E] (A (source a) == x (A (target a) == y (z:E)(inc z (U x)) -> (ev a z) == (f z) )). Definition property := [x,y:E; f: E1] (Transformation.axioms (U x) (U y) f). Definition like := [a:E](create (source a) (target a) (ev a)) == a. Lemma create_like : (x,y:E; f:E1)(like (create x y f)). Intros. Unfold like. Unfold source. Unfold target. Unfold ev. Unfold mapping. Unfold create; Repeat Rewrite -> get_rewrite. Apply Notation.extens; Intros. NewInduction i; Auto. Apply Function.create_create. Save. Lemma source_create : (x,y:E; f:E1)(source (create x y f)) == x. Intros. Unfold source; Unfold create; Rewrite -> get_rewrite; Trivial. Save. Lemma target_create : (x,y:E; f:E1)(target (create x y f)) == y. Intros. Unfold target; Unfold create; Rewrite -> get_rewrite; Trivial. Save. Lemma ev_create : (x,y:E; f:E1; z:E)(inc z (U x)) -> (ev (create x y f) z) == (f z). Intros. Unfold ev; Unfold mapping; Unfold create; Rewrite -> get_rewrite. Apply Function.create_V_rewrite. Assumption. Save. Lemma create_realizes : (x,y:E; f:E1)(realizes x y f (create x y f)). Intros. Pose source_create. Pose target_create. Pose ev_create. Unfold realizes; Expand. Save. Lemma realizes_like_eq : (x,y:E; f:E1; a:E)(like a) -> (realizes x y f a) -> (create x y f) == a. Intros. Unfold like in H. Rewrite <- H. Unfold create; Apply Notation.extens. Intro i. NewInduction i; Auto. Symmetry. Unfold realizes in H0; Expand. Symmetry. Unfold realizes in H0; Expand. Apply Function.create_extensionality. Unfold realizes in H0; Expand. Rewrite -> H0; Trivial. Intros. Unfold realizes in H0; Expand. Symmetry; Apply H4. Assumption. Save. Definition axioms := [a:E](property (source a) (target a) (ev a)). Definition strong_axioms := [a:E](A (axioms a) (like a)). Lemma axioms_from_strong : (a:E)(strong_axioms a) -> (axioms a). Intros. Unfold strong_axioms in H; Expand. Save. Lemma create_strong_axioms : (x,y:E; f:E1)(property x y f) -> (strong_axioms (create x y f)). Intros. Unfold strong_axioms. Expand. Unfold axioms. Rewrite -> source_create. Rewrite -> target_create. Unfold property. Unfold Transformation.axioms. Intros. Rewrite -> ev_create. Unfold property in H. Unfold Transformation.axioms in H. Apply H. Assumption. Assumption. Apply create_like. Save. Lemma create_axioms: (x,y:E; f:E1)(property x y f) -> (axioms (create x y f)). Intros. Apply axioms_from_strong. Apply create_strong_axioms; Auto. Save. Definition identity := [x:E](create x x [y:E]y). Definition compose := [a,b:E](create (source b) (target a) [y:E](ev a (ev b y))). Lemma identity_strong_axioms : (x:E)(strong_axioms (identity x)). Intros. Unfold identity. Apply create_strong_axioms. Unfold property. Apply Transformation.identity_axioms. Save. Lemma identity_axioms : (x:E)(axioms (identity x)). Intros. Pose H:= (identity_strong_axioms x). Unfold strong_axioms in (Type of H); Expand. Save. Lemma left_identity : (a:E)(strong_axioms a) -> (compose (identity (target a)) a) == a. Intros. Unfold compose. Apply realizes_like_eq. Unfold strong_axioms in H; Expand. Unfold realizes. Expand. Unfold identity; Rewrite -> target_create. Trivial. Intros. Unfold identity. Rewrite -> ev_create. Trivial. Unfold strong_axioms in H. Expand. Save. Lemma right_identity : (a:E)(strong_axioms a) -> (compose a (identity (source a))) == a. Intros. Unfold compose. Apply realizes_like_eq. Unfold strong_axioms in H; Expand. Unfold realizes. Expand. Unfold identity; Rewrite -> source_create. Trivial. Intros. Unfold identity; Rewrite -> ev_create. Trivial. Unfold identity in H0; Rewrite -> source_create in H0. Assumption. Save. Lemma source_identity : (x:E)(source (identity x)) == x. Intros. Unfold identity; Rewrite -> source_create. Trivial. Save. Lemma target_identity : (x:E)(target (identity x)) == x. Intros. Unfold identity; Rewrite -> target_create. Trivial. Save. Lemma ev_identity : (x,y:E)(inc y (U x)) -> (ev (identity x) y) == y. Intros. Unfold identity; Rewrite -> ev_create; Auto. Save. Lemma source_compose : (a,b:E)(source (compose a b)) == (source b). Intros. Unfold compose; Rewrite source_create; Trivial. Save. Lemma target_compose : (a,b:E)(target (compose a b)) == (target a). Intros. Unfold compose; Rewrite target_create; Trivial. Save. Lemma ev_compose : (a,b,y:E)(inc y (U (source b))) -> (ev (compose a b) y) == (ev a (ev b y)). Intros. Unfold compose; Rewrite ev_create; Auto. Save. Definition composable := [a,b:E] (A (axioms a) (A (axioms b) (source a) == (target b) )). Lemma compose_strong_axioms : (a,b:E)(composable a b) -> (strong_axioms (compose a b)). Intros. Unfold strong_axioms. Expand. Unfold axioms. Rewrite -> source_compose. Rewrite -> target_compose. Unfold property. Unfold Transformation.axioms. Intros. Rewrite -> ev_compose. Unfold composable in H. Expand. Unfold axioms in H. Unfold property in H. Unfold Transformation.axioms in H. Apply H. Unfold axioms in H1. Unfold property in H1. Unfold Transformation.axioms in H1. Rewrite -> H2. Apply H1. Assumption. Assumption. Unfold compose. Apply create_like. Save. Lemma compose_axioms : (a,b:E)(composable a b) -> (axioms (compose a b)). Intros. Pose K:= (compose_strong_axioms H). Unfold strong_axioms in (Type of K); Expand. Save. Lemma extens : (a,b:E)(strong_axioms a) -> (strong_axioms b) -> (source a) == (source b) -> (target a) == (target b) -> ((x:E)(inc x (U (source a))) -> (inc x (U (source b))) -> (ev a x) == (ev b x)) -> a == b. Intros. Unfold strong_axioms in H H0. Expand. Unfold like in H5 H4. Rewrite <- H5. Apply realizes_like_eq; Auto. Unfold realizes. Expand. Intros. Symmetry; Apply H3. Assumption. Rewrite <- H1. Assumption. Save. Lemma associativity : (a,b,c:E)(composable a b) -> (composable b c) -> (compose (compose a b) c) == (compose a (compose b c)). Intros. Apply extens. Apply compose_strong_axioms. Unfold composable. Expand. Apply compose_axioms; Auto. Unfold composable in H0; Expand. Rewrite -> source_compose. Unfold composable in H0; Expand. Apply compose_strong_axioms. Unfold composable; Expand. Unfold composable in H; Expand. Apply compose_axioms. Assumption. Rewrite -> target_compose. Unfold composable in H; Expand. Repeat Rewrite -> source_compose. Trivial. Repeat Rewrite -> target_compose; Trivial. Intros. Repeat Rewrite -> ev_compose. Trivial. Repeat Rewrite -> source_compose in H1. Assumption. Rewrite -> source_compose in H2. Assumption. Repeat Rewrite -> source_compose in H1. Unfold composable in H0. Expand. Rewrite -> H4. Apply H3. Assumption. Repeat Rewrite -> source_compose in H1. Assumption. Save. Definition inclusion := [a,b:E](create a b [y:E]y). Lemma inclusion_strong_axioms : (a,b:E)(sub (U a) (U b)) -> (strong_axioms (inclusion a b)). Intros. Unfold inclusion. Apply create_strong_axioms. Unfold property. Unfold Transformation.axioms. Intros. Apply H; Auto. Save. Lemma inclusion_axioms : (a,b:E)(sub (U a) (U b)) -> (axioms (inclusion a b)). Intros. Apply axioms_from_strong. Apply inclusion_strong_axioms; Auto. Save. Definition injective := [u:E] (A (axioms u) (Transformation.injective (U (source u)) (U (target u)) (ev u)) ). Lemma injective_rewrite : (u:E)(axioms u) -> (injective u) == ((x,y:E)(inc x (U (source u))) -> (inc y (U (source u))) -> (ev u x) == (ev u y) -> x == y). Intros. Apply iff_eq; Intros. Unfold injective in H0. Expand. Unfold Transformation.injective in H4. Expand. Unfold injective; Expand. Unfold Transformation.injective; Expand. Save. Lemma injective_compose_with : (u,v,w:E)(strong_axioms u) -> (strong_axioms v) -> (injective w) -> (composable w u) -> (composable w v) -> (compose w u) == (compose w v) -> u == v. Intros. Apply extens; Auto. Transitivity (source (compose w u)). Rewrite -> source_compose; Auto. Rewrite -> H4. Rewrite -> source_compose; Auto. Unfold composable in H2 H3. Expand. Transitivity (source w); Auto. Intros. Unfold injective in H1. Expand. Unfold Transformation.injective in H7. Expand. Apply H8. Unfold strong_axioms in H. Expand. Unfold axioms in H. Unfold property in H. Unfold composable in H2. Expand. Rewrite -> H11. Apply H. Assumption. Unfold composable in H3; Expand. Rewrite -> H10. Unfold strong_axioms in v; Expand. Transitivity (ev (compose w u) x). Rewrite -> ev_compose; Auto. Rewrite -> H4. Rewrite -> ev_compose; Auto. Save. Definition surjective := [u:E] (A (axioms u) (Transformation.surjective (U (source u)) (U (target u)) (ev u)) ). Lemma surjective_rewrite : (u:E)(axioms u) -> (surjective u) == ((x:E)(inc x (U (target u))) -> (exists [y:E](A (inc y (U (source u))) (ev u y) == x))). Intros. Apply iff_eq; Intros. Unfold surjective in H0; Expand. Unfold Transformation.surjective in H2; Expand. Unfold surjective; Expand. Unfold Transformation.surjective; Expand. Save. Definition inverse := [u:E](create (target u) (source u) (Transformation.inverse (U (source u)) (ev u))). Lemma surjective_inverse_axioms : (u:E)(surjective u) -> (strong_axioms (inverse u)). Intros. Unfold strong_axioms; Expand. Unfold inverse. Apply create_axioms. Unfold property. Apply Transformation.surjective_inverse_axioms. Unfold surjective in H; Expand. Unfold inverse. Apply create_like. Save. Lemma surjective_composable_left : (u:E)(surjective u) -> (composable (inverse u) u). Intros. Unfold composable. Expand. Apply axioms_from_strong. Apply surjective_inverse_axioms; Auto. Unfold surjective in H; Expand. Unfold inverse. Rewrite -> source_create; Trivial. Save. Lemma surjective_composable_right : (u:E)(surjective u) -> (composable u (inverse u)). Intros. Unfold composable; Expand. Unfold surjective in H; Expand. Apply axioms_from_strong. Apply surjective_inverse_axioms; Auto. Unfold inverse; Rewrite -> target_create; Trivial. Save. Lemma surjective_inverse_right : (u:E)(surjective u) -> (compose u (inverse u)) == (identity (target u)). Intros. Assert (axioms u). Unfold surjective in H; Expand. Apply extens. Apply compose_strong_axioms. Apply surjective_composable_right. Assumption. Apply identity_strong_axioms. Rewrite -> source_compose. Rewrite -> source_identity. Unfold inverse; Rewrite -> source_create. Trivial. Rewrite -> target_compose. Rewrite -> target_identity; Trivial. Intros. Rewrite -> ev_compose. Rewrite -> ev_identity. Unfold inverse. Rewrite -> ev_create. Unfold surjective in H. Expand. Rewrite -> source_identity in H2. Pose (Transformation.surjective_inverse_right H3 H2). Apply e. Rewrite -> source_identity in H2; Assumption. Rewrite -> source_identity in H2; Assumption. Rewrite -> source_compose in H1; Assumption. Save. Definition bijective := [u:E] (A (injective u) (surjective u)). Lemma bijective_transformation_bijective : (u:E)(bijective u) -> (Transformation.bijective (U (source u)) (U (target u)) (ev u)). Intros. Unfold bijective in H; Expand. Unfold injective in H. Unfold surjective in H0. Expand. Unfold axioms in H. Unfold property in H. Unfold Transformation.bijective; Expand. Save. Lemma transformation_bijective_bijective : (u:E)(axioms u) -> (Transformation.bijective (U (source u)) (U (target u)) (ev u)) -> (bijective u). Intros. Unfold Transformation.bijective in H0. Unfold bijective. Expand. Unfold injective; Expand. Unfold surjective; Expand. Save. Definition are_inverse := [u,v:E] (A (composable u v) (A (composable v u) (A (compose u v) == (identity (source v)) (compose v u) == (identity (source u)) ))). Lemma inverse_symm : (u,v:E)(are_inverse u v) -> (are_inverse v u). Intros. Unfold are_inverse. Unfold are_inverse in H. Expand. Save. Lemma inverse_unique : (u,v,w:E)(strong_axioms v) -> (strong_axioms w) -> (are_inverse u v) -> (are_inverse u w) -> v == w. Intros. Transitivity (compose v (identity (source v))). Symmetry. Apply right_identity. Assumption. Unfold are_inverse in H1 H2; Expand. Assert (source v)==(target u). Unfold composable in H4; Expand. Assert (source v)==(source w). Rewrite -> H9. Unfold composable in H3; Expand. Rewrite -> H10. Rewrite <- H5. Rewrite <- associativity. Rewrite -> H8. Assert (source u)==(target w). Unfold composable in H2; Expand. Rewrite -> H11. Apply left_identity. Assumption. Assumption. Assumption. Save. Definition has_inverse := [u:E](exists [v:E](are_inverse u v)). Lemma are_inverse_transfo_inverse : (u,v:E)(are_inverse u v) -> (Transformation.are_inverse (U (source u)) (U (target u)) (ev u) (ev v)). Intros. Unfold Transformation.are_inverse. Unfold are_inverse in H. Expand. Unfold composable in H; Expand. Unfold composable in H H0; Expand. Rewrite <- H5. Rewrite -> H6. Assumption. Intros. Transitivity (ev (compose v u) x). Symmetry; Apply ev_compose. Assumption. Rewrite -> H2. Apply ev_identity. Assumption. Intros. Assert (inc y (U (source v))). Unfold composable in H0; Expand. Rewrite -> H5; Assumption. Transitivity (ev (compose u v) y). Rewrite -> ev_compose. Trivial. Assumption. Rewrite -> H1. Rewrite -> ev_identity. Trivial. Assumption. Save. Lemma inverse_bijective : (u,v:E)(are_inverse u v) -> (bijective u). Intros. Apply transformation_bijective_bijective. Unfold are_inverse in H; Expand. Unfold composable in H; Expand. Apply Transformation.inverse_bijective with (ev v). Apply are_inverse_transfo_inverse. Assumption. Save. Lemma bijective_inverse : (u:E)(bijective u) -> (are_inverse u (inverse u)). Intros. Unfold bijective in H; Expand. Pose (surjective_composable_left H0). Pose (surjective_composable_right H0). Pose (surjective_inverse_right H0). Unfold are_inverse; Expand. Unfold composable in (Type of c); Expand. Rewrite -> H3. Apply e. Apply injective_compose_with with u. Apply compose_strong_axioms; Auto. Apply identity_strong_axioms. Assumption. Unfold composable. Expand. Unfold injective in H; Expand. Apply compose_axioms; Auto. Rewrite -> target_compose. Unfold composable in (Type of c0); Expand. Unfold composable; Expand. Unfold injective in H; Expand. Apply identity_axioms. Rewrite -> target_identity; Trivial. Rewrite <- associativity. Rewrite -> e. Apply extens. Apply compose_strong_axioms. Unfold composable; Expand. Apply identity_axioms. Unfold injective in H; Expand. Rewrite -> source_identity. Trivial. Apply compose_strong_axioms. Unfold composable; Expand. Unfold injective in H; Expand. Apply identity_axioms. Rewrite -> target_identity; Trivial. Rewrite -> source_compose. Rewrite -> source_compose. Rewrite -> source_identity; Trivial. Repeat Rewrite -> target_compose. Rewrite -> target_identity. Trivial. Intros. Repeat Rewrite -> ev_compose. Repeat Rewrite -> ev_identity. Trivial. Rewrite -> source_compose in H2. Rewrite -> source_identity in H2; Assumption. Unfold injective in H; Expand. Unfold axioms in H. Unfold property in H; Expand. Apply H. Rewrite -> source_compose in H2. Rewrite -> source_identity in H2. Assumption. Rewrite -> source_compose in H2; Assumption. Rewrite -> source_compose in H2. Rewrite -> source_identity in H2. Assumption. Assumption. Assumption. Save. Lemma bijective_has_inverse : (u:E)(bijective u) -> (has_inverse u). Intros. Unfold has_inverse. Apply exists_intro with (inverse u). Apply bijective_inverse; Auto. Save. Lemma bijective_eq_has_inverse : (u:E)(bijective u) == (has_inverse u). Intros. Apply iff_eq; Intros. Unfold has_inverse. Apply exists_intro with (inverse u). Apply bijective_inverse; Auto. Unfold has_inverse in H. NewInduction H. Apply inverse_bijective with x; Auto. Save. Lemma bijective_eq_inverse : (u:E)(bijective u) == (are_inverse u (inverse u)). Intros. Apply iff_eq; Intros. Apply bijective_inverse. Assumption. Apply inverse_bijective with (inverse u); Assumption. Save. Lemma has_inverse_eq_inverse : (u:E)(has_inverse u) == (are_inverse u (inverse u)). Intros. Rewrite <- bijective_eq_inverse. Rewrite -> bijective_eq_has_inverse. Trivial. Save. End Umorphism. Module Order. Export Umorphism. Definition leq := [a,x,y:E](inc (pair x y) (G OrderGraph a)). Definition lt := [a,x,y:E](A (leq a x y) ~(x == y)). Definition create := [a:E; l : E -> E -> Prop](Notation.create [i:Notation.t] Cases i of Underlying => a | OrderGraph => (Z (Cartesian.product a a) [x:E](l (pr1 x) (pr2 x))) | _ => emptyset end). Lemma underlying_create : (a:E; l:E->E->Prop)(U (create a l)) == a. Intros. Unfold create. Unfold U. Apply get_back. Trivial. Save. Lemma leq_create_then : (a:E; l:E->E->Prop; x,y:E)(leq (create a l) x y) -> (A (inc x a) (A (inc y a) (l x y))). Intros. Unfold leq in H. Unfold create in H; Rewrite -> get_rewrite in H. Pose (Z_all H). Expand. Pose (Cartesian.product_pair_pr H0); Expand. Pose (Cartesian.product_pair_pr H0); Expand. Rewrite -> pr1_pair in H1; Rewrite -> pr2_pair in H1; Assumption. Save. Lemma leq_create_if : (a:E; l:E->E->Prop; x,y:E)(inc x a) -> (inc y a) ->(l x y) -> (leq (create a l) x y). Intros. Unfold leq. Unfold create; Rewrite -> get_rewrite. Ztac. Apply product_pair_inc; Auto. Rewrite -> pr1_pair. Rewrite -> pr2_pair. Assumption. Save. Lemma leq_create : (a:E; l:E->E->Prop; x,y:E)(inc x a) -> (inc y a) -> (leq (create a l) x y) == (l x y). Intros. Apply iff_eq; Intros. Pose _:=(leq_create_then H1). Expand. Apply leq_create_if; Auto. Save. Lemma leq_create_all : (a:E; l:E->E->Prop; x,y:E)(leq (create a l) x y) == (A (inc x a) (A (inc y a) (l x y))). Intros. Apply iff_eq; Intros. Pose _:=(leq_create_then H); Expand. Apply leq_create_if; Expand. Save. Definition like := [a:E](create (U a) (leq a)) == a. Lemma create_like : (a:E; l:E->E->Prop)(like (create a l)). Intros. Unfold like. Rewrite -> underlying_create. Unfold 1 3 create; Apply Notation.extens; Intro i; NewInduction i; Auto. Apply extensionality; Unfold sub; Intros. Ztac. Apply Z_inc; Auto. Pose (leq_create_then H1). Expand. Ztac. Apply Z_inc; Auto. Pose (product_pr H0). Expand. Apply leq_create_if; Auto. Save. Definition property := [a:E; l:E -> E -> Prop] (A (x:E)(inc x a) -> (l x x) (A (x,y:E)(inc x a) -> (inc y a) -> (l x y) -> (l y x) -> x == y (x,y,z:E)(inc x a) -> (inc y a) -> (inc z a) -> (l x y) -> (l y z) -> (l x z) )). Definition axioms := [a:E] (A (x:E)(inc x (U a)) -> (leq a x x) (A (x,y:E)(leq a x y) -> (inc x (U a)) (A (x,y:E)(leq a x y) -> (inc y (U a)) (A (x,y:E)(leq a x y) -> (leq a y x) -> x == y (x,y,z:E)(leq a x y) -> (leq a y z) -> (leq a x z) )))). Lemma create_axioms : (a:E; l: E-> E->Prop)(property a l) -> (axioms (create a l)). Intros. Unfold property in H; Expand. Unfold axioms; Expand; Intros; Expand. Rewrite -> underlying_create in H2. Apply leq_create_if; Auto. Rewrite -> underlying_create. Pose (leq_create_then H2); Expand. Rewrite -> underlying_create. Pose (leq_create_then H2); Expand. Pose (leq_create_then H2); Pose (leq_create_then H3); Expand. Pose (leq_create_then H2); Pose (leq_create_then H3); Expand. Apply leq_create_if; Auto. Apply H1 with y; Auto. Save. Definition strong_axioms := [a:E](A (axioms a) (like a)). Lemma axioms_from_strong : (a:E)(strong_axioms a) -> (axioms a). Intros. Unfold strong_axioms in H; Expand. Save. Lemma create_strong_axioms : (a:E; l: E-> E->Prop)(property a l) -> (strong_axioms (create a l)). Intros. Unfold strong_axioms; Expand. Apply create_axioms; Auto. Apply create_like. Save. Lemma extens : (a,b:E)(strong_axioms a) -> (strong_axioms b) -> (U a) == (U b) -> ((x,y:E)(leq a x y) -> (leq b x y)) ->((x,y:E)(leq b x y) -> (leq a x y)) -> a==b. Intros. Unfold strong_axioms in H H0. Expand. Unfold like in H5 H4. Rewrite <- H5. Rewrite <- H4. Unfold create; Apply Notation.extens; Intro i; NewInduction i; Auto. Apply extensionality; Unfold sub; Intros. Pose _:=(Z_all H6). Expand. Apply Z_inc. Rewrite <- H1. Assumption. Apply H2; Assumption. Pose _:=(Z_all H6); Expand. Apply Z_inc. Rewrite -> H1; Assumption. Apply H3; Assumption. Save. Lemma lt_leq_trans : (a,x,y,z:E)(axioms a) -> (lt a x y) -> (leq a y z) -> (lt a x z). Intros. Unfold lt; Unfold lt in H0; Expand. Unfold axioms in H; Expand. Apply H6 with y; Auto. Unfold not; Intros. Rewrite -> H3 in H0. Unfold axioms in H; Expand. Apply H2. Rewrite -> H3. Apply H6; Auto. Save. Lemma leq_lt_trans : (a,x,y,z:E)(axioms a) -> (leq a x y) -> (lt a y z) -> (lt a x z). Intros. Unfold lt; Unfold lt in H1; Expand. Unfold axioms in H; Expand. Apply H6 with y; Auto. Unfold not; Intros. Apply H2. Rewrite <- H3. Rewrite <- H3 in H1. Unfold axioms in H; Expand. Save. Definition mor_axioms := [u:E] (A (axioms (source u)) (A (axioms (target u)) (A (Umorphism.strong_axioms u) (x,y:E)(leq (source u) x y) -> (leq (target u) (ev u x) (ev u y)) ))). Lemma identity_axioms : (a:E)(axioms a) -> (mor_axioms (Umorphism.identity a)). Intros. Unfold mor_axioms. Expand. Rewrite -> source_identity; Auto. Rewrite -> target_identity; Auto. Apply Umorphism.identity_strong_axioms. Intros. Rewrite -> source_identity in H0. Rewrite -> target_identity. Rewrite -> ev_identity. Rewrite -> ev_identity. Unfold axioms in H; Expand. Unfold axioms in H; Expand. Apply H2 with x; Auto. Unfold axioms in H; Expand. Apply H1 with y; Auto. Save. Definition composable := [u,v:E] (A (mor_axioms u) (A (mor_axioms v) (source u) == (target v) )). Lemma compose_axioms : (u,v:E)(composable u v) -> (mor_axioms (Umorphism.compose u v)). Intros. Unfold composable in H; Expand. Unfold mor_axioms in H; Expand. Unfold mor_axioms in H0; Expand. Unfold mor_axioms; Expand. Rewrite -> source_compose; Auto. Rewrite -> target_compose; Auto. Apply Umorphism.compose_strong_axioms. Unfold Umorphism.composable; Expand. Apply Umorphism.axioms_from_strong; Assumption. Apply Umorphism.axioms_from_strong; Assumption. Intros. Rewrite -> target_compose. Rewrite -> ev_compose. Rewrite -> ev_compose. Rewrite -> source_compose in H8. Apply H4. Rewrite -> H1. Apply H7. Assumption. Unfold axioms in H0; Expand. Rewrite -> source_compose in H8. Apply H10 with x; Auto. Rewrite -> source_compose in H8. Unfold axioms in H0; Expand. Apply H9 with y; Auto. Save. Definition suborder := [b,a:E](create b (leq a)). Lemma suborder_strong_axioms : (a,b:E)(axioms a) -> (sub b (U a)) -> (strong_axioms (suborder b a)). Intros. Unfold suborder. Apply create_strong_axioms. Unfold property. Unfold axioms in H. Expand. Intros. Apply H4 with y; Auto. Save. Lemma underlying_suborder : (a,b:E)(U (suborder b a)) == b. Intros. Unfold suborder; Rewrite -> underlying_create; Trivial. Save. Lemma leq_suborder_if : (a,b,x,y:E)(inc x b) -> (inc y b) -> (sub b (U a)) -> (leq a x y) -> (leq (suborder b a) x y). Intros. Unfold suborder. Apply leq_create_if; Auto. Save. Lemma leq_suborder_then : (a,b,x,y:E)(axioms a) -> (sub b (U a)) -> (leq (suborder b a) x y) -> (A (inc x b) (A (inc y b) (leq a x y) )). Intros. Expand. Unfold suborder in H1. Pose (leq_create_then H1). Expand. Unfold suborder in H1. Pose (leq_create_then H1); Expand. Unfold suborder in H1. Pose (leq_create_then H1); Expand. Save. Lemma leq_suborder_all : (a,b,x,y:E)(axioms a) -> (sub b (U a)) -> (leq (suborder b a) x y) == (A (inc x b) (A (inc y b) (leq a x y) )). Intros. Apply iff_eq; Intros. Pose _:=(leq_suborder_then H H0 H1). Expand. Apply leq_suborder_if; Expand. Save. Lemma suborder_trans : (a,b,c:E)(axioms a) -> (sub b (U a)) -> (sub c b) -> (suborder c a) == (suborder c (suborder b a)). Intros. Apply extens. Apply suborder_strong_axioms. Assumption. Apply sub_trans with b; Auto. Apply suborder_strong_axioms. Apply axioms_from_strong. Apply suborder_strong_axioms. Assumption. Assumption. Rewrite -> underlying_suborder. Assumption. Repeat Rewrite -> underlying_suborder. Trivial. Intros. Assert (sub c (U a)). Apply sub_trans with b; Auto. Rewrite leq_suborder_all in H2; Auto. Expand. Apply leq_suborder_if; Auto. Rewrite -> underlying_suborder; Assumption. Apply leq_suborder_if; Auto. Intros. Rewrite -> leq_suborder_all in H2; Auto. Expand. Rewrite -> leq_suborder_all in H4; Auto. Expand. Apply leq_suborder_if; Auto. Apply sub_trans with b; Auto. Apply axioms_from_strong; Apply suborder_strong_axioms; Auto. Rewrite -> underlying_suborder; Assumption. Save. Definition suborder_inclusion := [b,a:E](Umorphism.inclusion (suborder b a) a). Lemma suborder_inclusion_mor_axioms : (a,b:E)(axioms a) -> (sub b (U a)) -> (mor_axioms (suborder_inclusion b a)). Intros. Unfold suborder_inclusion. Unfold mor_axioms; Expand. Unfold inclusion; Rewrite -> source_create. Apply axioms_from_strong; Apply suborder_strong_axioms; Auto. Unfold inclusion; Rewrite -> target_create. Assumption. Unfold inclusion. Apply Umorphism.create_strong_axioms. Unfold Umorphism.property. Unfold Transformation.axioms. Intros. Rewrite -> underlying_suborder in H1. Apply H0; Auto. Intros. Unfold inclusion. Rewrite -> target_create. Repeat Rewrite -> ev_create. Unfold inclusion in H1; Rewrite -> source_create in H1. Rewrite -> leq_suborder_all in H1. Expand. Assumption. Assumption. Unfold inclusion in H1; Rewrite -> source_create in H1. Rewrite -> leq_suborder_all in H1; Auto. Expand. Rewrite -> underlying_suborder; Assumption. Unfold inclusion in H1; Rewrite -> source_create in H1. Rewrite -> leq_suborder_all in H1; Auto. Expand. Rewrite -> underlying_suborder; Auto. Save. Definition is_linear := [a:E] (A (axioms a) (x,y:E)(inc x (U a)) -> (inc y (U a)) -> ((leq a x y) \/ (leq a y x)) ). Definition is_minimal := [a,b,x:E] (A (axioms a) (A (sub b (U a)) (A (inc x b) (y:E)(inc y b) -> (leq a y x) -> y == x ))). Definition is_maximal := [a,b,x:E] (A (axioms a) (A (sub b (U a)) (A (inc x b) (y:E)(inc y b) -> (leq a x y) -> x == y ))). Definition is_upper_bound := [a,b,x:E] (A (axioms a) (A (sub b (U a)) (A (inc x (U a)) (y:E)(inc y b) -> (leq a y x) ))). Definition is_lower_bound := [a,b,x:E] (A (axioms a) (A (sub b (U a)) (A (inc x (U a)) (y:E)(inc y b) -> (leq a x y) ))). Definition is_bottom_element := [a,b,x:E] (A (is_lower_bound a b x) (inc x b) ). Definition is_top_element := [a,b,x:E] (A (is_upper_bound a b x) (inc x b) ). Lemma top_element_maximal : (a,b,x:E)(is_top_element a b x) -> (is_maximal a b x). Intros. Unfold is_top_element in H. Expand. Unfold is_upper_bound in H; Expand. Unfold is_maximal; Expand. Intros. Unfold axioms in H; Expand. Save. Lemma bottom_element_minimal : (a,b,x:E)(is_bottom_element a b x) -> (is_minimal a b x). Intros. Unfold is_bottom_element in H. Expand. Unfold is_lower_bound in H; Expand. Unfold is_minimal; Expand. Intros. Unfold axioms in H; Expand. Save. Lemma top_element_unique : (a,b,x,y:E)(is_top_element a b x) -> (is_top_element a b y) -> x == y. Intros. Unfold is_top_element in H H0; Expand. Unfold is_upper_bound in H H0; Expand. Unfold axioms in H; Expand. Save. Lemma bottom_element_unique : (a,b,x,y:E)(is_bottom_element a b x) -> (is_bottom_element a b y) -> x == y. Intros. Unfold is_bottom_element in H H0; Expand. Unfold is_lower_bound in H H0; Expand. Unfold axioms in H; Expand. Save. Lemma linear_maximal_top_element : (a,b,x:E)(is_linear a) -> (is_maximal a b x) -> (is_top_element a b x). Intros. Unfold is_linear in H. Unfold is_maximal in H0. Unfold is_top_element. Unfold is_upper_bound. Expand. Intros. Assert (inc x (U a)). Apply H1; Auto. Assert (inc y (U a)). Apply H1; Auto. Pose (H2 ? ? H6 H7). NewInduction o. Unfold axioms in H; Expand. Assert x == y. Apply H4; Auto. Rewrite H13. Auto. Assumption. Save. Lemma linear_minimal_bottom_element : (a,b,x:E)(is_linear a) -> (is_minimal a b x) -> (is_bottom_element a b x). Intros. Unfold is_linear in H. Unfold is_minimal in H0. Unfold is_bottom_element. Unfold is_lower_bound. Expand. Intros. Assert (inc x (U a)). Apply H1; Auto. Assert (inc y (U a)). Apply H1; Auto. Pose (H2 ? ? H6 H7). NewInduction o. Unfold axioms in H; Expand. Assert y == x. Apply H4; Auto. Rewrite H9. Unfold axioms in H; Expand. Save. Definition downward_subset := [a,x:E] (Z (U a) [y:E](leq a y x)). Definition punctured_downward_subset := [a,x:E] (Z (U a) [y:E](lt a y x)). Definition downward_suborder := [a,x:E](suborder (downward_subset a x) a). Definition punctured_downward_suborder := [a,x:E](suborder (punctured_downward_subset a x) a). Definition is_well_ordered := [a:E] (A (is_linear a) (b:E)(sub b (U a)) -> (nonempty b) -> (exists [x:E](is_bottom_element a b x)) ). End Order.