Set Difference
==============

<!--
SPDX-FileCopyrightText: The authors of this work have dedicated it to the public domain.
For more information, please refer to <https://unlicense.org/>
SPDX-License-Identifier: Unlicense
-->

Some theorems about set difference.

These theorems, as usually stated, are based on an [Algebra of sets (Wikipedia)](https://en.wikipedia.org/wiki/Algebra_of_sets).
However, we will use Boolean algebra as their basis here.  (I'm given to
understand that these two theories are subtlely different, but I've concluded
that the difference, if there is one, is too subtle to matter for our purposes;
all the axioms and properties we care about are shared by the two,
and it is only a matter of adjusting the nomenclature.)

Requires [Boolean algebra](boolean-algebra.eqthy.md).

Definition of set difference.

    axiom (#diff)          diff(A, B) = and(A, not(B))

A theorem about set difference: difference distributes over union.

    theorem (#diff-union-distrib)
        or(diff(A, C), diff(B, C)) = diff(or(A, B), C)
    proof
        or(diff(A, C), diff(B, C)) = or(diff(A, C), diff(B, C))
        or(diff(A, C), diff(B, C)) = or(diff(A, C), and(B, not(C)))
        or(diff(A, C), diff(B, C)) = or(and(A, not(C)), and(B, not(C)))
        or(diff(A, C), diff(B, C)) = or(and(A, not(C)), and(not(C), B))
        or(diff(A, C), diff(B, C)) = or(and(not(C), A), and(not(C), B))
        or(diff(A, C), diff(B, C)) = and(not(C), or(A, B))
        or(diff(A, C), diff(B, C)) = and(or(A, B), not(C))
        or(diff(A, C), diff(B, C)) = diff(or(A, B), C)
    qed

Another theorem about set difference: the difference of A and B is the
same as the difference of A and the intersection of A and B.

    theorem (#diff-of-inter-is-diff)
        diff(A, B) = diff(A, and(A, B))
    proof
        diff(A, B) = diff(A, B)
        diff(A, B) = and(A, not(B))
        diff(A, B) = or(and(A, not(B)), 0)
        diff(A, B) = or(0, and(A, not(B)))
        diff(A, B) = or(and(A, not(A)), and(A, not(B)))
        diff(A, B) = and(A, or(not(A), not(B)))
        diff(A, B) = and(A, not(and(A, B)))
        diff(A, B) = diff(A, and(A, B))
    qed

Both of these theorems were adapted from
[this presentation by Mustafa Jarrar](http://www.jarrar.info/courses/DMath/Jarrar.LectureNotes.6.3%20Algebric%20Proofs.pdf).