diff options
Diffstat (limited to 'megalodon/library/set.mg')
| -rw-r--r-- | megalodon/library/set.mg | 293 |
1 files changed, 293 insertions, 0 deletions
diff --git a/megalodon/library/set.mg b/megalodon/library/set.mg new file mode 100644 index 0000000..3606b4e --- /dev/null +++ b/megalodon/library/set.mg @@ -0,0 +1,293 @@ +Let emptyset : set := Empty. +Let elem : set->set->prop := In. +Let notelem : set->set->prop := fun a A => ~(In a A). +Let pow : set->set := Power. +Let unions : set->set := Union. +Let union : set->set->set := binunion. +Let cons : set -> set -> set := fun x X => binunion {x} X. +Let xor : prop -> prop -> prop := fun p q => (p \/ q) /\ ~(p /\ q). +Let pair : set -> set -> set := fun a b => {{a}, {a, b}}. +Let fst : set -> set := fun p => Eps_i (fun a => exists b, p = pair a b). +Let snd : set -> set := fun p => Eps_i (fun b => exists a, p = pair a b). +Let nor : prop -> prop -> prop := fun p q => ~(p \/ q) . +Definition ni := fun x0 x1 : set => (elem x1 x0). +Fact setext : (forall A B,(((forall a,(((elem a A)<->(elem a B))))->(A = B)))). +Admitted. +Theorem neq_witness : (forall A B,(((A <> B)->(exists c,((xor((elem c A)/\~((elem c B))) (~((elem c A))/\(elem c B)))))))). +Admitted. +Definition subseteq := fun A B: set => (forall a,(((elem a A)->(elem a B)))). +Definition is_subset := fun x0 x1 : set => (subseteq x0 x1). +Definition supseteq := fun x0 x1 : set => (subseteq x1 x0). +Theorem subseteq_refl : (forall A,((subseteq A A))). +Admitted. +Theorem subseteq_antisymmetric : (forall A B,((((subseteq A B)/\(subseteq B A))->(A = B)))). +Admitted. +Theorem elem_subseteq : (forall a A B,((((elem a A)/\(subseteq A B))->(elem a B)))). +Admitted. +Theorem not_in_subseteq : (forall A B c,((((subseteq A B)/\(notelem c B))->(notelem c A)))). +Admitted. +Theorem subseteq_transitive : (forall A B C,((((subseteq A B)/\(subseteq B C))->(subseteq A C)))). +Admitted. +Definition subset := fun A B: set => ((subseteq A B)/\(A <> B)). +Theorem subset_irrefl : (forall A,(~((subset A A)))). +Admitted. +Theorem subset_transitive : (forall A B C,((((subseteq A B)/\(subseteq B C))->(subseteq A C)))). +Admitted. +Theorem subset_witness : (forall A B,(((subset A B)->(exists b,(((elem b B)/\(notelem b A))))))). +Admitted. +Definition family_of_subsets := fun x0 x1 : set => (forall A,(((elem A x0)->(subseteq A x1)))). +Fact notin_emptyset : (forall a,((notelem a (emptyset)))). +Admitted. +Definition inhabited := fun A: set => (exists a,((elem a A))). +Definition empty := fun x0 : set => ~((inhabited x0)). +Theorem empty_eq : (forall x y,((((empty x)/\(empty y))->(x = y)))). +Admitted. +Theorem emptyset_subseteq : (forall a,((subseteq (emptyset) a))). +Admitted. +Theorem subseteq_emptyset_iff : (forall A,(((subseteq A (emptyset))<->(A = (emptyset))))). +Admitted. +Definition disjoint := fun A B: set => ~((exists a,(((elem a A)/\(elem a B))))). +Definition notmeets := fun x0 x1 : set => (disjoint x0 x1). +Definition meets := fun x0 x1 : set => ~((disjoint x0 x1)). +Theorem disjoint_symmetric : (forall A B,(((disjoint A B)->(disjoint B A)))). +Admitted. +Fact in_cons : (forall x y X,(((elem x (cons y X))<->((x = y)\/(elem x X))))). +Admitted. +Theorem in_cons_left : (forall x X,((elem x (cons x X)))). +Admitted. +Theorem in_cons_right : (forall y X x,(((elem y X)->(elem y (cons x X))))). +Admitted. +Theorem upair_intro_left : (forall a b,((elem a (cons a (cons b (emptyset)))))). +Admitted. +Theorem upair_intro_right : (forall b a,((elem b (cons a (cons b (emptyset)))))). +Admitted. +Theorem upair_elim : (forall c a b,(((elem c (cons a (cons b (emptyset))))->((a = c)\/(b = c))))). +Admitted. +Theorem upair_iff : (forall c a b,(((elem c (cons a (cons b (emptyset))))<->((a = c)\/(b = c))))). +Admitted. +Theorem singleton_intro : (forall a,((elem a (cons a (emptyset))))). +Admitted. +Theorem singleton_elim : (forall a b,(((elem a (cons b (emptyset)))->(a = b)))). +Admitted. +Theorem singleton_iff : (forall a b,(((elem a (cons b (emptyset)))<->(a = b)))). +Admitted. +Definition subsingleton := fun x0 : set => (forall a b,((((elem a x0)/\(elem b x0))->(a = b)))). +Theorem singleton_inhabited : (forall a,((inhabited (cons a (emptyset))))). +Admitted. +Theorem singleton_iff_inhabited_subsingleton : (forall A a,((((subsingleton A)/\(elem a A))->(A = (cons a (emptyset)))))). +Admitted. +Theorem singleton_subset_intro : (forall a C,(((elem a C)->(subseteq (cons a (emptyset)) C)))). +Admitted. +Theorem singleton_subset_elim : (forall a C,(((subseteq (cons a (emptyset)) C)->(elem a C)))). +Admitted. +Fact unions_iff_exists : (forall z X,(((elem z (unions X))<->(exists Y,(((elem Y X)/\(elem z Y))))))). +Admitted. +Theorem unions_intro : (forall A B C,((((elem A B)/\(elem B C))->(elem A (unions C))))). +Admitted. +Theorem unions_emptyset : ((unions (emptyset)) = (emptyset)). +Admitted. +Theorem unions_family : (forall F X,(((family_of_subsets F X)->(subseteq (unions F) X)))). +Admitted. +Definition closedunderunions := fun x0 : set => (forall M,(((is_subset M x0)->(elem (unions M) x0)))). +Definition inters := fun A : set => {x :e ((unions A))|(forall a,(((elem a A)->(elem x a))))}. +Theorem inters_iff_forall : (forall z X,(((elem z (inters X))<->((inhabited X)/\(forall Y,(((elem Y X)->(elem z Y)))))))). +Admitted. +Theorem inters_intro : (forall C A,((((inhabited C)/\(forall B,(((elem B C)->(elem A B)))))->(elem A (inters C))))). +Admitted. +Theorem inters_destr : (forall A C B,((((elem A (inters C))/\(elem B C))->(elem A B)))). +Admitted. +Theorem inters_greatest : (forall A C,((((inhabited A)/\(forall a,(((elem a A)->(subseteq C a)))))->(subseteq C (inters A))))). +Admitted. +Theorem subseteq_inters_iff : (forall A C,(((inhabited A)->((subseteq C (inters A))<->(forall a,(((elem a A)->(subseteq C a)))))))). +Admitted. +Theorem inters_subseteq_elem : (forall B A,(((elem B A)->(subseteq (inters A) B)))). +Admitted. +Theorem inters_singleton : (forall a,(((inters (cons a (emptyset))) = a))). +Admitted. +Theorem inters_emptyset : ((inters (cons (emptyset) (emptyset))) = (emptyset)). +Admitted. +Fact union_iff : (forall a A B,(((elem a (union A B))<->((elem a A)\/(elem a B))))). +Admitted. +Theorem union_intro_left : (forall c A B,(((elem c A)->(elem c (union A B))))). +Admitted. +Theorem union_intro_right : (forall c B A,(((elem c B)->(elem c (union A B))))). +Admitted. +Theorem union_comm : (forall A B,(((union A B) = (union B A)))). +Admitted. +Theorem union_assoc : (forall A B C,(((union (union A B) C) = (union A (union B C))))). +Admitted. +Theorem union_idempotent : (forall A,(((union A A) = A))). +Admitted. +Theorem subseteq_union_iff : (forall A B C,(((subseteq (union A B) C)<->((subseteq A C)/\(subseteq B C))))). +Admitted. +Theorem union_upper_left : (forall A B,((subseteq A (union A B)))). +Admitted. +Theorem union_upper_right : (forall B A,((subseteq B (union A B)))). +Admitted. +Theorem union_subseteq_union : (forall A C B D,((((subseteq A C)/\(subseteq B D))->(subseteq (union A B) (union C D))))). +Admitted. +Theorem union_emptyset : (forall A,(((union A (emptyset)) = A))). +Admitted. +Theorem union_emptyset_intro : (forall A B,((((A = (emptyset))/\(B = (emptyset)))->((union A B) = (emptyset))))). +Admitted. +Theorem union_emptyset_elim_left : (forall A B,((((union A B) = (emptyset))->(A = (emptyset))))). +Admitted. +Theorem union_emptyset_elim_right : (forall A B,((((union A B) = (emptyset))->(B = (emptyset))))). +Admitted. +Theorem union_absorb_subseteq_left : (forall A B,(((subseteq A B)->((union A B) = B)))). +Admitted. +Theorem union_absorb_subseteq_right : (forall A B,(((subseteq A B)->((union B A) = B)))). +Admitted. +Theorem union_eq_self_implies_subseteq : (forall A B,((((union A B) = B)->(subseteq A B)))). +Admitted. +Theorem unions_cons : (forall b A,(((unions (cons b A)) = (union b (unions A))))). +Admitted. +Theorem union_cons : (forall b A C,(((union (cons b A) C) = (cons b (union A C))))). +Admitted. +Theorem union_absorb_left : (forall A B,(((union A (union A B)) = (union A B)))). +Admitted. +Theorem union_absorb_right : (forall A B,(((union (union A B) B) = (union A B)))). +Admitted. +Theorem union_comm_left : (forall A B C,(((union A (union B C)) = (union B (union A C))))). +Admitted. +Definition closedunderunion := fun x0 : set => (forall U V,((((elem U x0)/\(elem V x0))->(elem (union U V) x0)))). +Definition inter := fun A B : set => {a :e (A)|(elem a B)}. +Theorem inter_intro : (forall c A B,((((elem c A)/\(elem c B))->(elem c (inter A B))))). +Admitted. +Theorem inter_elim_left : (forall c A B,(((elem c (inter A B))->(elem c A)))). +Admitted. +Theorem inter_elim_right : (forall c A B,(((elem c (inter A B))->(elem c B)))). +Admitted. +Theorem inter_as_inters : (forall A B,(((inters (cons A (cons B (emptyset)))) = (inter A B)))). +Admitted. +Theorem inter_comm : (forall A B,(((inter A B) = (inter B A)))). +Admitted. +Theorem inter_assoc : (forall A B C,(((inter (inter A B) C) = (inter A (inter B C))))). +Admitted. +Theorem inter_idempotent : (forall A,(((inter A A) = A))). +Admitted. +Theorem inter_subseteq : (forall A B,((subseteq (inter A B) A))). +Admitted. +Theorem inter_emptyset : (forall A,(((inter A (emptyset)) = (emptyset)))). +Admitted. +Theorem inter_absorb_supseteq_right : (forall A B,(((subseteq A B)->((inter A B) = A)))). +Admitted. +Theorem inter_absorb_supseteq_left : (forall A B,(((subseteq A B)->((inter B A) = A)))). +Admitted. +Theorem inter_eq_left_implies_subseteq : (forall A B,((((inter A B) = A)->(subseteq A B)))). +Admitted. +Theorem subseteq_inter_iff : (forall C A B,(((subseteq C (inter A B))<->((subseteq C A)/\(subseteq C B))))). +Admitted. +Theorem inter_lower_left : (forall A B,((subseteq (inter A B) A))). +Admitted. +Theorem inter_lower_right : (forall A B,((subseteq (inter A B) B))). +Admitted. +Theorem inter_absorb_left : (forall A B,(((inter A (inter A B)) = (inter A B)))). +Admitted. +Theorem inter_absorb_right : (forall A B,(((inter (inter A B) B) = (inter A B)))). +Admitted. +Theorem inter_comm_left : (forall A B C,(((inter A (inter B C)) = (inter B (inter A C))))). +Admitted. +Definition closedunderinter := fun x0 : set => (forall U V,((((elem U x0)/\(elem V x0))->(elem (inter U V) x0)))). +Theorem inter_distrib_union : (forall x y z,(((inter x (union y z)) = (union (inter x y) (inter x z))))). +Admitted. +Theorem union_distrib_inter : (forall x y z,(((union x (inter y z)) = (inter (union x y) (union x z))))). +Admitted. +Theorem union_inter_assoc_intro : (forall C A B,(((subseteq C A)->((union (inter A B) C) = (inter A (union B C)))))). +Admitted. +Theorem union_inter_assoc_elim : (forall A B C,((((union (inter A B) C) = (inter A (union B C)))->(subseteq C A)))). +Admitted. +Theorem union_inter_crazy : (forall A B C,(((union (union (inter A B) (inter B C)) (inter C A)) = (inter (inter (union A B) (union B C)) (union C A))))). +Admitted. +Theorem inters_distrib_union : (forall A B,((((inhabited A)/\(inhabited B))->((inters (union A B)) = (inter (inters A) (inters B)))))). +Admitted. +Definition setminus := fun A B : set => {a :e (A)|~((elem a B))}. +Theorem setminus_intro : (forall a A B,((((elem a A)/\(notelem a B))->(elem a (setminus A B))))). +Admitted. +Theorem setminus_elim_left : (forall a A B,(((elem a (setminus A B))->(elem a A)))). +Admitted. +Theorem setminus_elim_right : (forall a A B,(((elem a (setminus A B))->(notelem a B)))). +Admitted. +Theorem setminus_emptyset : (forall x,(((setminus x (emptyset)) = x))). +Admitted. +Theorem emptyset_setminus : (forall x,(((setminus (emptyset) x) = (emptyset)))). +Admitted. +Theorem setminus_self : (forall x,(((setminus x x) = (emptyset)))). +Admitted. +Theorem setminus_setminus : (forall x y,(((setminus x (setminus x y)) = (inter x y)))). +Admitted. +Theorem double_relative_complement : (forall y x,(((subseteq y x)->((setminus x (setminus x y)) = y)))). +Admitted. +Theorem setminus_inter : (forall x y z,(((setminus x (inter y z)) = (union (setminus x y) (setminus x z))))). +Admitted. +Theorem setminus_union : (forall x y z,(((setminus x (union y z)) = (inter (setminus x y) (setminus x z))))). +Admitted. +Theorem inter_setminus : (forall x y z,(((inter x (setminus y z)) = (setminus (inter x y) (inter x z))))). +Admitted. +Theorem difference_with_proper_subset_is_inhabited : (forall A B,(((subset A B)->(inhabited (setminus B A))))). +Admitted. +Theorem setminus_subseteq : (forall B A,((subseteq (setminus B A) B))). +Admitted. +Theorem subseteq_setminus : (forall C A B,((((subseteq C A)/\((inter C B) = (emptyset)))->(subseteq C (setminus A B))))). +Admitted. +Theorem subseteq_implies_setminus_supseteq : (forall A B C,(((subseteq A B)->(supseteq (setminus C A) (setminus C B))))). +Admitted. +Theorem setminus_absorb_right : (forall A B,((((inter A B) = (emptyset))->((setminus A B) = A)))). +Admitted. +Theorem setminus_eq_emptyset_iff_subseteq : (forall A B,((((setminus A B) = (emptyset))<->(subseteq A B)))). +Admitted. +Theorem subseteq_setminus_cons_intro : (forall B A C c,((((subseteq B (setminus A C))/\(notelem c B))->(subseteq B (setminus A (cons c C)))))). +Admitted. +Theorem subseteq_setminus_cons_elim : (forall B A c C,(((subseteq B (setminus A (cons c C)))->((subseteq B (setminus A C))/\(notelem c B))))). +Admitted. +Theorem setminus_cons : (forall A a B,(((setminus A (cons a B)) = (setminus (setminus A (cons a (emptyset))) B)))). +Admitted. +Theorem setminus_cons_flip : (forall A a B,(((setminus A (cons a B)) = (setminus (setminus A B) (cons a (emptyset)))))). +Admitted. +Theorem setminus_disjoint : (forall A B,(((inter A (setminus B A)) = (emptyset)))). +Admitted. +Theorem setminus_partition : (forall A B,(((subseteq A B)->((union A (setminus B A)) = B)))). +Admitted. +Theorem subseteq_union_setminus : (forall A B,((subseteq A (union B (setminus A B))))). +Admitted. +Theorem double_complement : (forall A B C,((((subseteq A B)/\(subseteq B C))->((setminus B (setminus C A)) = A)))). +Admitted. +Theorem double_complement_union : (forall A B,(((setminus (union A B) (setminus B A)) = A))). +Admitted. +Theorem setminus_eq_inter_complement : (forall A C B,((((subseteq A C)/\(subseteq B C))->((setminus A B) = (inter A (setminus C B)))))). +Admitted. +Fact pair_eq_iff : (forall a b aprime bprime,((((pair a b) = (pair aprime bprime))<->((a = aprime)/\(b = bprime))))). +Admitted. +Fact pair_neq_emptyset : (forall a b,(((pair a b) <> (emptyset)))). +Admitted. +Fact pair_neq_fst : (forall a b,(((pair a b) <> a))). +Admitted. +Fact pair_neq_snd : (forall a b,(((pair a b) <> b))). +Admitted. +Theorem triple_eq_iff : (forall a b c aprime bprime cprime,((((pair a (pair b c)) = (pair aprime (pair bprime cprime)))<->(((a = aprime)/\(b = bprime))/\(c = cprime))))). +Admitted. +Fact fst_eq : (forall a b,(((fst (pair a b)) = a))). +Admitted. +Fact snd_eq : (forall a b,(((snd (pair a b)) = b))). +Admitted. +Theorem pair_eq_pair_of_proj : (forall a b,(((pair a b) = (pair (fst (pair a b)) (snd (pair a b)))))). +Admitted. +Definition times := fun A B : set => ReplSep2 (A)(fun dummyVar => B)(fun a b => True)(fun a b => (pair a b)). +Theorem times_tuple_elim : (forall x y X Y,(((elem (pair x y) (times X Y))->((elem x X)/\(elem y Y))))). +Admitted. +Theorem times_tuple_intro : (forall x X y Y,((((elem x X)/\(elem y Y))->(elem (pair x y) (times X Y))))). +Admitted. +Theorem times_empty_left : (forall Y,(((times (emptyset) Y) = (emptyset)))). +Admitted. +Theorem times_empty_right : (forall X,(((times X (emptyset)) = (emptyset)))). +Admitted. +Theorem times_empty_iff : (forall X Y,(((empty (times X Y))<->((empty X)\/(empty Y))))). +Admitted. +Theorem fst_type : (forall c A B,(((elem c (times A B))->(elem (fst c) A)))). +Admitted. +Theorem snd_type : (forall c A B,(((elem c (times A B))->(elem (snd c) B)))). +Admitted. +Theorem times_elem_is_tuple : (forall p X Y,(((elem p (times X Y))->(exists x y,(((elem x X)/\((elem y Y)/\(p = (pair x y))))))))). +Admitted. +Theorem times_proj_elim : (forall p X Y,(((elem p (times X Y))->((elem (fst p) X)/\(elem (snd p) Y))))). +Admitted. |