Grace/Cumulus/Set/Algebra.g17

Open in Workbench Download source

Imports

Core

Declarations

• symmetricDifference def
• symmetricDifference.membership theorem derivation
• Subset.of_eq theorem derivation
• Subset.empty_iff theorem derivation
• Subset.union2_iff theorem derivation
• Subset.intersection_iff theorem derivation
• union2.left_empty theorem derivation
• union2.right_empty theorem derivation
• union2.monotone theorem derivation
• union2.monotone_left theorem derivation
• union2.monotone_right theorem derivation
• union2.eq_right_of_subset theorem derivation
• union2.eq_left_of_subset theorem derivation
• union2.subset_iff_eq theorem derivation
• union2.left_commutative theorem derivation
• union2.subset_of_subset_left theorem derivation
• union2.subset_of_subset_right theorem derivation
• union2.eq_empty_iff theorem derivation
• intersection.left_empty theorem derivation
• intersection.right_empty theorem derivation
• intersection.associative theorem derivation
• intersection.left_commutative theorem derivation
• intersection.monotone theorem derivation
• intersection.monotone_left theorem derivation
• intersection.monotone_right theorem derivation
• intersection.eq_left_of_subset theorem derivation
• intersection.eq_right_of_subset theorem derivation
• intersection.subset_iff_eq theorem derivation
• intersection.subset_union2 theorem derivation
• intersection.union2_distrib theorem derivation
• union2.intersection_distrib theorem derivation
• intersection.union2_distrib_right theorem derivation
• union2.intersection_distrib_right theorem derivation
• union2.absorb theorem derivation
• intersection.absorb theorem derivation
• difference.self theorem derivation
• difference.empty theorem derivation
• difference.left_empty theorem derivation
• difference.eq_empty_iff theorem derivation
• difference.eq_self_iff_disjoint theorem derivation
• difference.subset_of_subset theorem derivation
• difference.antitone theorem derivation
• difference.monotone theorem derivation
• difference.union2_of_subset theorem derivation
• difference.union2_self theorem derivation
• difference.difference theorem derivation
• difference.difference_right theorem derivation
• difference.union2 theorem derivation
• difference.intersection theorem derivation
• difference.union2_left theorem derivation
• difference.intersection_left theorem derivation
• difference.intersection_right theorem derivation
• difference.of_intersection theorem derivation
• difference.intersection_eq theorem derivation
• difference.disjoint theorem derivation
• difference.union2_intersection theorem derivation
• difference.of_union2 theorem derivation
• difference.subset_iff theorem derivation
• Disjoint.iff theorem derivation
• Disjoint.empty_left theorem derivation
• Disjoint.empty_right theorem derivation
• Disjoint.of_subset_left theorem derivation
• Disjoint.of_subset_right theorem derivation
• Disjoint.union2_iff theorem derivation
• Disjoint.difference_left theorem derivation
• Disjoint.difference_right theorem derivation
• Disjoint.subset_difference theorem derivation
• symmetricDifference.commutative theorem derivation
• symmetricDifference.self theorem derivation
• symmetricDifference.empty theorem derivation
• symmetricDifference.left_empty theorem derivation
• symmetricDifference.eq_difference theorem derivation
• symmetricDifference.associative theorem derivation
• symmetricDifference.union2 theorem derivation
• symmetricDifference.intersection_distrib theorem derivation
• symmetricDifference.intersection_distrib_right theorem derivation
• symmetricDifference.eq_empty_iff theorem derivation
• symmetricDifference.subset theorem derivation

Source

1-- The Boolean algebra of sets: union, intersection, difference, and2-- symmetric difference under inclusion3-- Part of Cumulus, the Grace17 mathematics library.4-- Copyright (c) 2026 Grant Passmore.5-- Released under the Apache License 2.0. See LICENSE in the repository root.6-- Authors: Grant Passmore78module Grace.Cumulus.Set.Algebra9import Core1011def symmetricDifference (A B : Set) : Set := (A ∖ B) ∪ (B ∖ A)12notation infixl 60 "△" => symmetricDifference1314theorem symmetricDifference.membership (x A B : Set)15  shows x ∈ A △ B ↔ ¬(x ∈ A ↔ x ∈ B)16proof17  simp [symmetricDifference]1819-- Inclusion2021theorem Subset.of_eq (A B : Set)22  requires h : A = B23  shows A ⊆ B24proof25  rw h26  simp2728theorem Subset.empty_iff (A : Set)29  shows A ⊆ ∅ ↔ A = ∅30proof31  constructor32  . intro h33    ext y34    simp35  . intro h36    rw h37    simp3839theorem Subset.union2_iff (A B C : Set)40  shows A ∪ B ⊆ C ↔ A ⊆ C ∧ B ⊆ C41proof42  constructor43  . intro h44    constructor45    . simp46    . simp47  . intro h48    simp4950theorem Subset.intersection_iff (A B C : Set)51  shows A ⊆ B ∩ C ↔ A ⊆ B ∧ A ⊆ C52proof53  constructor54  . intro h55    constructor56    . simp57    . simp58  . intro h59    simp6061-- Union6263theorem union2.left_empty (A : Set)64  shows ∅ ∪ A = A65proof66  ext y67  simp6869theorem union2.right_empty (A : Set)70  shows A ∪ ∅ = A71proof72  ext y73  simp7475theorem union2.monotone (A B C D : Set)76  requires hAC : A ⊆ C77  requires hBD : B ⊆ D78  shows A ∪ B ⊆ C ∪ D79proof80  simp8182theorem union2.monotone_left (A B C : Set)83  requires h : A ⊆ B84  shows A ∪ C ⊆ B ∪ C85proof86  simp8788theorem union2.monotone_right (A B C : Set)89  requires h : A ⊆ B90  shows C ∪ A ⊆ C ∪ B91proof92  simp9394theorem union2.eq_right_of_subset (A B : Set)95  requires h : A ⊆ B96  shows A ∪ B = B97proof98  ext y99  simp100101theorem union2.eq_left_of_subset (A B : Set)102  requires h : B ⊆ A103  shows A ∪ B = A104proof105  ext y106  simp107108theorem union2.subset_iff_eq (A B : Set)109  shows A ⊆ B ↔ A ∪ B = B110proof111  constructor112  . intro h113    ext y114    simp115  . intros h x hx116    have member : x ∈ A ∪ B by simp [hx]117    rwa h at member118119theorem union2.left_commutative (A B C : Set)120  shows A ∪ (B ∪ C) = B ∪ (A ∪ C)121proof122  ext y123  simp124125theorem union2.subset_of_subset_left (A B C : Set)126  requires h : A ⊆ B127  shows A ⊆ B ∪ C128proof129  simp130131theorem union2.subset_of_subset_right (A B C : Set)132  requires h : A ⊆ C133  shows A ⊆ B ∪ C134proof135  simp136137theorem union2.eq_empty_iff (A B : Set)138  shows A ∪ B = ∅ ↔ A = ∅ ∧ B = ∅139proof140  constructor141  . intro h142    constructor143    . ext y144      constructor145      . intro hy146        have member : y ∈ A ∪ B by simp [hy]147        rwa h at member148      . intro hy149        exact empty.subset at A with y, hy150    . ext y151      constructor152      . intro hy153        have member : y ∈ A ∪ B by simp [hy]154        rwa h at member155      . intro hy156        exact empty.subset at B with y, hy157  . intro h158    rw [h.left, h.right]159    exact union2.left_empty160161-- Intersection162163theorem intersection.left_empty (A : Set)164  shows ∅ ∩ A = ∅165proof166  ext y167  simp168169theorem intersection.right_empty (A : Set)170  shows A ∩ ∅ = ∅171proof172  ext y173  simp174175theorem intersection.associative (A B C : Set)176  shows (A ∩ B) ∩ C = A ∩ (B ∩ C)177proof178  ext y179  simp180181theorem intersection.left_commutative (A B C : Set)182  shows A ∩ (B ∩ C) = B ∩ (A ∩ C)183proof184  ext y185  simp186187theorem intersection.monotone (A B C D : Set)188  requires hAC : A ⊆ C189  requires hBD : B ⊆ D190  shows A ∩ B ⊆ C ∩ D191proof192  simp193194theorem intersection.monotone_left (A B C : Set)195  requires h : A ⊆ B196  shows A ∩ C ⊆ B ∩ C197proof198  simp199200theorem intersection.monotone_right (A B C : Set)201  requires h : A ⊆ B202  shows C ∩ A ⊆ C ∩ B203proof204  simp205206theorem intersection.eq_left_of_subset (A B : Set)207  requires h : A ⊆ B208  shows A ∩ B = A209proof210  ext y211  simp212213theorem intersection.eq_right_of_subset (A B : Set)214  requires h : B ⊆ A215  shows A ∩ B = B216proof217  ext y218  simp219220theorem intersection.subset_iff_eq (A B : Set)221  shows A ⊆ B ↔ A ∩ B = A222proof223  constructor224  . intro h225    ext y226    simp227  . intros h x hx228    rw ← h at hx229    exact intersection.subset_right at A, B with x, hx230231theorem intersection.subset_union2 (A B : Set)232  shows A ∩ B ⊆ A ∪ B233proof234  simp235236-- Distributivity and absorption237238theorem intersection.union2_distrib (A B C : Set)239  shows A ∩ (B ∪ C) = (A ∩ B) ∪ (A ∩ C)240proof241  ext y242  simp243244theorem union2.intersection_distrib (A B C : Set)245  shows A ∪ (B ∩ C) = (A ∪ B) ∩ (A ∪ C)246proof247  ext y248  simp249250theorem intersection.union2_distrib_right (A B C : Set)251  shows (A ∪ B) ∩ C = (A ∩ C) ∪ (B ∩ C)252proof253  ext y254  simp255256theorem union2.intersection_distrib_right (A B C : Set)257  shows (A ∩ B) ∪ C = (A ∪ C) ∩ (B ∪ C)258proof259  ext y260  simp261262theorem union2.absorb (A B : Set)263  shows A ∪ (A ∩ B) = A264proof265  ext y266  simp267268theorem intersection.absorb (A B : Set)269  shows A ∩ (A ∪ B) = A270proof271  ext y272  simp273274-- Difference275276theorem difference.self (A : Set)277  shows A ∖ A = ∅278proof279  ext y280  simp281282theorem difference.empty (A : Set)283  shows A ∖ ∅ = A284proof285  ext y286  simp287288theorem difference.left_empty (A : Set)289  shows ∅ ∖ A = ∅290proof291  ext y292  simp293294theorem difference.eq_empty_iff (A B : Set)295  shows A ∖ B = ∅ ↔ A ⊆ B296proof297  constructor298  . intros h x hx299    by_contra absent300    have member : x ∈ A ∖ B by simp [hx, absent]301    rw h at member302    simpa using member303  . intro h304    ext y305    simp306307theorem difference.eq_self_iff_disjoint (A B : Set)308  shows A ∖ B = A ↔ A ∩ B = ∅309proof310  constructor311  . intro h312    ext y313    constructor314    . intro hy315      simp [intersection.membership] at hy316      have inA := hy.left317      rw ← h at inA318      simp [difference.membership] at inA319      exfalso320      exact inA.right with hy.right321    . intro hy322      exact empty.subset at A ∩ B with y, hy323  . intro h324    ext y325    constructor326    . intro hy327      simp [difference.membership] at hy328      exact hy.left329    . intro hy330      simp [difference.membership]331      constructor332      . exact hy333      . intro hB334        have member : y ∈ A ∩ B by simp [hy, hB]335        rw h at member336        simpa using member337338theorem difference.subset_of_subset (A B C : Set)339  requires h : A ⊆ B340  shows A ∖ C ⊆ B ∖ C341proof342  simp343344theorem difference.antitone (A B C : Set)345  requires h : B ⊆ C346  shows A ∖ C ⊆ A ∖ B347proof348  simp349350theorem difference.monotone (A B C D : Set)351  requires hAC : A ⊆ C352  requires hDB : D ⊆ B353  shows A ∖ B ⊆ C ∖ D354proof355  simp356357theorem difference.union2_of_subset (A B : Set)358  requires h : A ⊆ B359  shows A ∪ (B ∖ A) = B360proof361  ext y362  simp363364theorem difference.union2_self (A B : Set)365  shows A ∪ (B ∖ A) = A ∪ B366proof367  ext y368  simp369370theorem difference.difference (A B : Set)371  shows A ∖ (A ∖ B) = A ∩ B372proof373  ext y374  simp375376theorem difference.difference_right (A B C : Set)377  shows (A ∖ B) ∖ C = A ∖ (B ∪ C)378proof379  ext y380  simp381382theorem difference.union2 (A B C : Set)383  shows A ∖ (B ∪ C) = (A ∖ B) ∩ (A ∖ C)384proof385  ext y386  simp387388theorem difference.intersection (A B C : Set)389  shows A ∖ (B ∩ C) = (A ∖ B) ∪ (A ∖ C)390proof391  ext y392  simp393394theorem difference.union2_left (A B C : Set)395  shows (A ∪ B) ∖ C = (A ∖ C) ∪ (B ∖ C)396proof397  ext y398  simp399400theorem difference.intersection_left (A B C : Set)401  shows (A ∩ B) ∖ C = (A ∖ C) ∩ (B ∖ C)402proof403  ext y404  simp405406theorem difference.intersection_right (A B C : Set)407  shows A ∖ (B ∖ C) = (A ∖ B) ∪ (A ∩ C)408proof409  ext y410  simp411412theorem difference.of_intersection (A B : Set)413  shows A ∖ (A ∩ B) = A ∖ B414proof415  ext y416  simp417418theorem difference.intersection_eq (A B : Set)419  shows (A ∖ B) ∩ B = ∅420proof421  ext y422  simp423424theorem difference.disjoint (A B : Set)425  shows Disjoint(A ∖ B, B)426proof427  simp [Disjoint, difference.intersection_eq]428429theorem difference.union2_intersection (A B : Set)430  shows (A ∖ B) ∪ (A ∩ B) = A431proof432  ext y433  simp434435theorem difference.of_union2 (A B : Set)436  shows (A ∪ B) ∖ B = A ∖ B437proof438  ext y439  simp440441theorem difference.subset_iff (A B C : Set)442  shows A ∖ B ⊆ C ↔ A ⊆ B ∪ C443proof444  constructor445  . intro h446    simp447  . intros h x hx448    simp [difference.membership] at hx449    have inUnion : x ∈ B ∪ C := h with x, hx.left450    simp [union2.membership] at inUnion451    cases inUnion with inB | inC452    . exfalso453      exact hx.right with inB454    . exact inC455456-- Disjointness457458theorem Disjoint.iff (A B : Set)459  shows Disjoint(A, B) ↔ ∀ x ∈ A, ¬(x ∈ B)460proof461  constructor462  . intros h x hx hB463    have member : x ∈ A ∩ B by simp [hx, hB]464    simp [Disjoint] at h465    rw h at member466    simpa using member467  . intro h468    simp [Disjoint]469    ext y470    constructor471    . intro hy472      simp [intersection.membership] at hy473      exfalso474      exact h with y, hy.left, hy.right475    . intro hy476      exact empty.subset at A ∩ B with y, hy477478theorem Disjoint.empty_left (A : Set)479  shows Disjoint(∅, A)480proof481  simp [Disjoint, intersection.left_empty]482483theorem Disjoint.empty_right (A : Set)484  shows Disjoint(A, ∅)485proof486  simp [Disjoint, intersection.right_empty]487488theorem Disjoint.of_subset_left (A B C : Set)489  requires h : Disjoint(B, C)490  requires hAB : A ⊆ B491  shows Disjoint(A, C)492proof493  have absent := Disjoint.iff.forward with h494  apply Disjoint.iff.backward495  intros x hx496  exact absent with x, (hAB with x, hx)497498theorem Disjoint.of_subset_right (A B C : Set)499  requires h : Disjoint(A, C)500  requires hBC : B ⊆ C501  shows Disjoint(A, B)502proof503  have absent := Disjoint.iff.forward with h504  apply Disjoint.iff.backward505  intros x hx hB506  exact absent with x, hx, (hBC with x, hB)507508theorem Disjoint.union2_iff (A B C : Set)509  shows Disjoint(A ∪ B, C) ↔ Disjoint(A, C) ∧ Disjoint(B, C)510proof511  constructor512  . intro h513    have absent := Disjoint.iff.forward with h514    constructor515    . apply Disjoint.iff.backward516      intros x hx517      exact absent with x, (union2.subset_left at A, B with x, hx)518    . apply Disjoint.iff.backward519      intros x hx520      exact absent with x, (union2.subset_right at A, B with x, hx)521  . intro h522    have absentA := Disjoint.iff.forward with h.left523    have absentB := Disjoint.iff.forward with h.right524    apply Disjoint.iff.backward525    intros x hx526    simp [union2.membership] at hx527    cases hx with inA | inB528    . exact absentA with x, inA529    . exact absentB with x, inB530531theorem Disjoint.difference_left (A B : Set)532  shows Disjoint(A ∖ B, B)533proof534  exact difference.disjoint535536theorem Disjoint.difference_right (A B : Set)537  shows Disjoint(B, A ∖ B)538proof539  apply Disjoint.symmetric540  exact difference.disjoint541542theorem Disjoint.subset_difference (A B : Set)543  requires h : Disjoint(A, B)544  shows A ⊆ A ∖ B545proof546  have absent := Disjoint.iff.forward with h547  intros x hx548  simp [difference.membership]549550-- Symmetric difference551552theorem symmetricDifference.commutative (A B : Set)553  shows A △ B = B △ A554proof555  ext y556  simp [symmetricDifference]557558theorem symmetricDifference.self (A : Set)559  shows A △ A = ∅560proof561  ext y562  simp [symmetricDifference]563564theorem symmetricDifference.empty (A : Set)565  shows A △ ∅ = A566proof567  ext y568  simp [symmetricDifference]569570theorem symmetricDifference.left_empty (A : Set)571  shows ∅ △ A = A572proof573  ext y574  simp [symmetricDifference]575576theorem symmetricDifference.eq_difference (A B : Set)577  shows A △ B = (A ∪ B) ∖ (A ∩ B)578proof579  ext y580  simp [symmetricDifference]581582theorem symmetricDifference.associative (A B C : Set)583  shows (A △ B) △ C = A △ (B △ C)584proof585  ext y586  simp [symmetricDifference]587588theorem symmetricDifference.union2 (A B : Set)589  shows A ∪ B = (A △ B) ∪ (A ∩ B)590proof591  ext y592  simp [symmetricDifference]593594theorem symmetricDifference.intersection_distrib (A B C : Set)595  shows A ∩ (B △ C) = (A ∩ B) △ (A ∩ C)596proof597  ext y598  simp [symmetricDifference]599600-- Intersection distributes over △ on the right as well.601theorem symmetricDifference.intersection_distrib_right (A B C : Set)602  shows (A △ B) ∩ C = (A ∩ C) △ (B ∩ C)603proof604  ext y605  simp [symmetricDifference]606607theorem symmetricDifference.eq_empty_iff (A B : Set)608  shows A △ B = ∅ ↔ A = B609proof610  constructor611  . intro h612    ext y613    by_contra different614    have member : y ∈ A △ B by simp [symmetricDifference.membership]615    rw h at member616    simpa using member617  . intro h618    rw h619    exact symmetricDifference.self620621theorem symmetricDifference.subset (A B C : Set)622  requires first : A ⊆ C623  requires second : B ⊆ C624  shows A △ B ⊆ C625proof626  have left : A ∖ B ⊆ C :=627    Subset.transitive with (difference.subset_left at A, B), first628  have right : B ∖ A ⊆ C :=629    Subset.transitive with (difference.subset_left at B, A), second630  unfold symmetricDifference631  exact union2.subset with left, right632