Grace/Cumulus/Combinatorics/InclusionExclusion.g17

Open in Workbench Download source

Imports

Basics

Declarations

Source

1-- Inclusion–exclusion for finite sets: differences, unions of two and three2-- sets, the subtraction forms, and the symmetric difference3-- 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.Combinatorics.InclusionExclusion9import Basics1011theorem Finite.intersection_left (A B : Set)12  requires finite : Finite(A)13  shows Finite(A ∩ B)14proof15  exact Finite.subset with finite, (intersection.subset_left at A, B)1617theorem Finite.intersection_right (A B : Set)18  requires finite : Finite(B)19  shows Finite(A ∩ B)20proof21  exact Finite.subset with finite, (intersection.subset_right at A, B)2223theorem Finite.symmetricDifference (A B : Set)24  requires finiteA : Finite(A)25  requires finiteB : Finite(B)26  shows Finite(A △ B)27proof28  unfold symmetricDifference29  exact Finite.union with (Finite.difference at A, B with finiteA),30    (Finite.difference at B, A with finiteB)3132-- A finite set splits into the part inside B and the part outside B.33theorem cardinality.difference_add_intersection (A B : Set)34  requires finite : Finite(A)35  shows cardinality(A ∖ B) + cardinality(A ∩ B) = cardinality(A)36proof37  have finiteRest := Finite.difference at A, B with finite38  have finiteMeet := Finite.intersection_left at A, B with finite39  have disjoint : Disjoint(A ∖ B, A ∩ B)40    unfold Disjoint41    ext x42    simp43  have split : (A ∖ B) ∪ (A ∩ B) = A44    ext x45    simp46  have count := cardinality.union_disjoint with finiteRest, finiteMeet, disjoint47  rw split at count48  symm49  exact count5051theorem cardinality.difference_count (A B : Set)52  requires finite : Finite(A)53  shows cardinality(A ∖ B) = cardinality(A) - cardinality(A ∩ B)54proof55  have split := cardinality.difference_add_intersection at A, B with finite56  have natRest := cardinality.nat with (Finite.difference at A, B with finite)57  have natMeet := cardinality.nat with (Finite.intersection_left at A, B with58    finite)59  rw ← split60  symm61  exact sub.add_right at cardinality(A ∖ B), cardinality(A ∩ B)6263theorem cardinality.intersection_le_left (A B : Set)64  requires finite : Finite(A)65  shows cardinality(A ∩ B) ≤ cardinality(A)66proof67  exact cardinality.monotone with finite, (intersection.subset_left at A, B)6869theorem cardinality.intersection_le_right (A B : Set)70  requires finite : Finite(B)71  shows cardinality(A ∩ B) ≤ cardinality(B)72proof73  exact cardinality.monotone with finite, (intersection.subset_right at A, B)7475theorem cardinality.difference_le (A B : Set)76  requires finite : Finite(A)77  shows cardinality(A ∖ B) ≤ cardinality(A)78proof79  exact cardinality.monotone with finite, (difference.subset_left at A, B)8081theorem cardinality.difference_add_of_subset (A B : Set)82  requires finite : Finite(A)83  requires subset : B ⊆ A84  shows cardinality(A ∖ B) + cardinality(B) = cardinality(A)85proof86  have split := cardinality.difference_add_intersection at A, B with finite87  have meet : A ∩ B = B88    ext x89    simp90  rw meet at split91  exact split9293theorem cardinality.difference_of_subset (A B : Set)94  requires finite : Finite(A)95  requires subset : B ⊆ A96  shows cardinality(A ∖ B) = cardinality(A) - cardinality(B)97proof98  have split := cardinality.difference_add_of_subset with finite, subset99  have natRest := cardinality.nat with (Finite.difference at A, B with finite)100  have natB := cardinality.nat with (Finite.subset with finite, subset)101  rw ← split102  symm103  exact sub.add_right at cardinality(A ∖ B), cardinality(B)104105theorem cardinality.union_sub (A B : Set)106  requires finiteA : Finite(A)107  requires finiteB : Finite(B)108  shows109    cardinality(A ∪ B) = cardinality(A) + cardinality(B) - cardinality(A ∩ B)110proof111  have both := cardinality.inclusion_exclusion with finiteA, finiteB112  have natUnion := cardinality.nat with (Finite.union with finiteA, finiteB)113  have natMeet := cardinality.nat with (Finite.intersection_left at A, B with114    finiteA)115  rw ← both116  symm117  exact sub.add_right at cardinality(A ∪ B), cardinality(A ∩ B)118119theorem cardinality.union_le (A B : Set)120  requires finiteA : Finite(A)121  requires finiteB : Finite(B)122  shows cardinality(A ∪ B) ≤ cardinality(A) + cardinality(B)123proof124  have both := cardinality.inclusion_exclusion with finiteA, finiteB125  have natUnion := cardinality.nat with (Finite.union with finiteA, finiteB)126  have natMeet := cardinality.nat with (Finite.intersection_left at A, B with127    finiteA)128  have natA := cardinality.nat with finiteA129  have natB := cardinality.nat with finiteB130  arith131132theorem cardinality.union_ge_left (A B : Set)133  requires finiteA : Finite(A)134  requires finiteB : Finite(B)135  shows cardinality(A) ≤ cardinality(A ∪ B)136proof137  have finiteUnion := Finite.union with finiteA, finiteB138  exact cardinality.monotone with finiteUnion, (union2.subset_left at A, B)139140theorem cardinality.union_ge_right (A B : Set)141  requires finiteA : Finite(A)142  requires finiteB : Finite(B)143  shows cardinality(B) ≤ cardinality(A ∪ B)144proof145  have finiteUnion := Finite.union with finiteA, finiteB146  exact cardinality.monotone with finiteUnion, (union2.subset_right at A, B)147148theorem cardinality.le_add_of_cover (S A B : Set)149  requires finiteA : Finite(A)150  requires finiteB : Finite(B)151  requires cover : S ⊆ A ∪ B152  shows cardinality(S) ≤ cardinality(A) + cardinality(B)153proof154  have finiteUnion := Finite.union with finiteA, finiteB155  have inside := cardinality.monotone with finiteUnion, cover156  have bound := cardinality.union_le with finiteA, finiteB157  have natS := cardinality.nat with (Finite.subset with finiteUnion, cover)158  have natUnion := cardinality.nat with finiteUnion159  have natA := cardinality.nat with finiteA160  have natB := cardinality.nat with finiteB161  exact LessEqual.transitive with inside, bound162163-- The union has the full count exactly when the sets are disjoint.164theorem cardinality.union_eq_add_iff_disjoint (A B : Set)165  requires finiteA : Finite(A)166  requires finiteB : Finite(B)167  shows cardinality(A ∪ B) = cardinality(A) + cardinality(B) ↔ Disjoint(A, B)168proof169  constructor170  . intro full171    have both := cardinality.inclusion_exclusion with finiteA, finiteB172    rw full at both173    have finiteMeet := Finite.intersection_left at A, B with finiteA174    have natMeet := cardinality.nat with finiteMeet175    have natA := cardinality.nat with finiteA176    have natB := cardinality.nat with finiteB177    have zero : cardinality(A ∩ B) = 0178      have le : cardinality(A ∩ B) ≤ 0 by arith179      have ge : 0 ≤ cardinality(A ∩ B) by arith180      exact LessEqual.antisymmetric with le, ge181    have iff := cardinality.eq_zero_iff with finiteMeet182    unfold Disjoint183    exact iff.forward with zero184  . intro disjoint185    exact cardinality.union_disjoint with finiteA, finiteB, disjoint186187-- Inclusion–exclusion for three sets.188theorem cardinality.union_three (A B C : Set)189  requires finiteA : Finite(A)190  requires finiteB : Finite(B)191  requires finiteC : Finite(C)192  shows cardinality(A ∪ B ∪ C) + cardinality(A ∩ B) + cardinality(A ∩ C) +193      cardinality(B ∩ C) =194    cardinality(A) + cardinality(B) + cardinality(C) + cardinality(A ∩ B ∩ C)195proof196  have finiteAB := Finite.union with finiteA, finiteB197  have finiteAC := Finite.intersection_left at A, C with finiteA198  have finiteBC := Finite.intersection_left at B, C with finiteB199  have outer := cardinality.inclusion_exclusion with finiteAB, finiteC200  have inner := cardinality.inclusion_exclusion with finiteA, finiteB201  have meetSplit : (A ∪ B) ∩ C = (A ∩ C) ∪ (B ∩ C)202    ext x203    simp204  have meetMeet : (A ∩ C) ∩ (B ∩ C) = A ∩ B ∩ C205    ext x206    simp207  have meets := cardinality.inclusion_exclusion with finiteAC, finiteBC208  rw meetSplit at outer209  rw meetMeet at meets210  have natUnion := cardinality.nat with (Finite.union with finiteAB, finiteC)211  have natAB := cardinality.nat with finiteAB212  have natMeetAB := cardinality.nat with (Finite.intersection_left at A, B with213    finiteA)214  have natAC := cardinality.nat with finiteAC215  have natBC := cardinality.nat with finiteBC216  have natACBC := cardinality.nat with (Finite.union with finiteAC, finiteBC)217  have natABC := cardinality.nat with (Finite.intersection_left at A ∩ B, C with (Finite.intersection_left at A, B with finiteA))218  have natA := cardinality.nat with finiteA219  have natB := cardinality.nat with finiteB220  have natC := cardinality.nat with finiteC221  have le : cardinality(A ∪ B ∪ C) + cardinality(A ∩ B) + cardinality(A ∩ C) + cardinality(B ∩ C) ≤ cardinality(A) + cardinality(B) + cardinality(C) + cardinality(A ∩ B ∩ C) by arith222  have ge : cardinality(A) + cardinality(B) + cardinality(C) + cardinality(A ∩ B ∩ C) ≤ cardinality(A ∪ B ∪ C) + cardinality(A ∩ B) + cardinality(A ∩ C) + cardinality(B ∩ C) by arith223  exact LessEqual.antisymmetric with le, ge224225theorem cardinality.union_three_le (A B C : Set)226  requires finiteA : Finite(A)227  requires finiteB : Finite(B)228  requires finiteC : Finite(C)229  shows230    cardinality(A ∪ B ∪ C) ≤ cardinality(A) + cardinality(B) + cardinality(C)231proof232  have finiteAB := Finite.union with finiteA, finiteB233  have first := cardinality.union_le with finiteAB, finiteC234  have second := cardinality.union_le with finiteA, finiteB235  have natABC := cardinality.nat with (Finite.union with finiteAB, finiteC)236  have natAB := cardinality.nat with finiteAB237  have natA := cardinality.nat with finiteA238  have natB := cardinality.nat with finiteB239  have natC := cardinality.nat with finiteC240  arith241242theorem cardinality.union_three_disjoint (A B C : Set)243  requires finiteA : Finite(A)244  requires finiteB : Finite(B)245  requires finiteC : Finite(C)246  requires disjointAB : Disjoint(A, B)247  requires disjointAC : Disjoint(A, C)248  requires disjointBC : Disjoint(B, C)249  shows250    cardinality(A ∪ B ∪ C) = cardinality(A) + cardinality(B) + cardinality(C)251proof252  have finiteAB := Finite.union with finiteA, finiteB253  have disjoint : Disjoint(A ∪ B, C)254    have leftFree := Disjoint.iff.forward with disjointAC255    have rightFree := Disjoint.iff.forward with disjointBC256    apply Disjoint.iff.backward257    intros x hx258    have split := union2.membership.forward with hx259    cases split with inA | inB260    . exact leftFree with x, inA261    . exact rightFree with x, inB262  have outer := cardinality.union_disjoint with finiteAB, finiteC, disjoint263  have inner := cardinality.union_disjoint with finiteA, finiteB, disjointAB264  rw [outer, inner]265  rfl266267-- The symmetric difference counts each set once and the overlap twice less.268theorem cardinality.symmetricDifference_add (A B : Set)269  requires finiteA : Finite(A)270  requires finiteB : Finite(B)271  shows cardinality(A △ B) + 2 * cardinality(A ∩ B) =272    cardinality(A) + cardinality(B)273proof274  have finiteAB := Finite.difference at A, B with finiteA275  have finiteBA := Finite.difference at B, A with finiteB276  have disjoint : Disjoint(A ∖ B, B ∖ A)277    unfold Disjoint278    ext x279    simp280  have split := cardinality.union_disjoint with finiteAB, finiteBA, disjoint281  have left := cardinality.difference_add_intersection at A, B with finiteA282  have right := cardinality.difference_add_intersection at B, A with finiteB283  have commute := intersection.commutative at B, A284  rw commute at right285  have natAB := cardinality.nat with finiteAB286  have natBA := cardinality.nat with finiteBA287  have natMeet := cardinality.nat with (Finite.intersection_left at A, B with288    finiteA)289  have natA := cardinality.nat with finiteA290  have natB := cardinality.nat with finiteB291  unfold symmetricDifference292  rw split293  have le : cardinality(A ∖ B) + cardinality(B ∖ A) + 2 * cardinality(A ∩ B) ≤ cardinality(A) + cardinality(B) by arith294  have ge : cardinality(A) + cardinality(B) ≤ cardinality(A ∖ B) + cardinality(B ∖ A) + 2 * cardinality(A ∩ B) by arith295  exact LessEqual.antisymmetric with le, ge296297theorem cardinality.symmetricDifference_sub (A B : Set)298  requires finiteA : Finite(A)299  requires finiteB : Finite(B)300  shows cardinality(A △ B) =301    cardinality(A) + cardinality(B) - 2 * cardinality(A ∩ B)302proof303  have split := cardinality.symmetricDifference_add with finiteA, finiteB304  have natSym := cardinality.nat with (Finite.symmetricDifference with305    finiteA, finiteB)306  have natMeet := cardinality.nat with (Finite.intersection_left at A, B with307    finiteA)308  rw ← split309  symm310  exact sub.add_right at cardinality(A △ B), 2 * cardinality(A ∩ B)311312theorem cardinality.symmetricDifference_le (A B : Set)313  requires finiteA : Finite(A)314  requires finiteB : Finite(B)315  shows cardinality(A △ B) ≤ cardinality(A) + cardinality(B)316proof317  have split := cardinality.symmetricDifference_add with finiteA, finiteB318  have natSym := cardinality.nat with (Finite.symmetricDifference with319    finiteA, finiteB)320  have natMeet := cardinality.nat with (Finite.intersection_left at A, B with321    finiteA)322  have natA := cardinality.nat with finiteA323  have natB := cardinality.nat with finiteB324  arith325326theorem cardinality.symmetricDifference_of_disjoint (A B : Set)327  requires finiteA : Finite(A)328  requires finiteB : Finite(B)329  requires disjoint : Disjoint(A, B)330  shows cardinality(A △ B) = cardinality(A) + cardinality(B)331proof332  have split := cardinality.symmetricDifference_add with finiteA, finiteB333  unfold Disjoint at disjoint334  rw [disjoint, cardinality.empty] at split335  have natSym := cardinality.nat with (Finite.symmetricDifference with336    finiteA, finiteB)337  have zero : 2 * 0 = 0 by compute338  rw zero at split339  have natA := cardinality.nat with finiteA340  have natB := cardinality.nat with finiteB341  have shape : cardinality(A △ B) + 0 = cardinality(A △ B) by ring342  rw shape at split343  exact split344345-- Removing a subset of known size.346theorem cardinality.difference_lt_of_member (A B b : Set)347  requires finite : Finite(A)348  requires inA : b ∈ A349  requires inB : b ∈ B350  shows cardinality(A ∖ B) < cardinality(A)351proof352  have absent : ¬b ∈ A ∖ B353    intro h354    have parts := difference.membership.forward with h355    exact parts.right with inB356  exact cardinality.strict with finite, (difference.subset_left at A, B), inA, absent357358theorem cardinality.difference_eq_iff_disjoint (A B : Set)359  requires finite : Finite(A)360  shows cardinality(A ∖ B) = cardinality(A) ↔ Disjoint(A, B)361proof362  constructor363  . intro same364    have equal := cardinality.eq_subset with finite,365      (difference.subset_left at A, B), same366    apply Disjoint.iff.backward367    intros x hx inB368    rw ← equal at hx369    have parts := difference.membership.forward with hx370    exact parts.right with inB371  . intro disjoint372    have same : A ∖ B = A373      have free := Disjoint.iff.forward with disjoint374      ext x375      constructor376      . intro hx377        exact difference.subset_left at A, B with x, hx378      . intro hx379        apply difference.membership.backward380        exact ⟨hx, (free with x, hx)⟩381    rw same382    rfl383