sbv-8.7: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.

Documentation.SBV.Examples.Misc.SetAlgebra

Description

Proves various algebraic properties of sets using SBV. The properties we prove all come from http://en.wikipedia.org/wiki/Algebra_of_sets.

Synopsis

# Documentation

>>> -- For doctest purposes only:
>>> import Data.SBV hiding (complement)
>>> import Data.SBV.Set
>>> :set -XScopedTypeVariables


type SI = SSet Integer Source #

Abbreviation for set of integers. For convenience only in monomorphising the properties.

# Commutativity

$$A\cup B=B\cup A$$

>>> prove $$$a :: SI) -> a union empty .== a Q.E.D.  \(A\cap U = A$$ >>> prove$ $$a :: SI) -> a intersection full .== a Q.E.D.  # Complement properties \( A\cup A^{C}=U$$

>>> prove $$$a :: SI) -> a union complement a .== full Q.E.D.  \( A\cap A^{C}=\varnothing$$ >>> prove$ $$a :: SI) -> a intersection complement a .== empty Q.E.D.  \({(A^{C})}^{C}=A$$

>>> prove $$$a :: SI) -> complement (complement a) .== a Q.E.D.  \(\varnothing ^{C}=U$$ >>> prove$ complement (empty :: SI) .== full
Q.E.D.


$$U^{C}=\varnothing$$

>>> prove $$$a :: SI) b -> a isSubsetOf b .&& b isSubsetOf a .<=> a .== b Q.E.D.  \( A\subseteq B \land B\subseteq C \Rightarrow A \subseteq C$$ >>> prove$ $$a :: SI) b c -> a isSubsetOf b .&& b isSubsetOf c .=> a isSubsetOf c Q.E.D.  # Joins and meets \( A\subseteq A\cup B$$

>>> prove $$$a :: SI) b -> a isSubsetOf (a union b) Q.E.D.  \( A\subseteq C \land B\subseteq C \Rightarrow (A \cup B) \subseteq C$$ >>> prove$ $$a :: SI) b c -> a isSubsetOf c .&& b isSubsetOf c .=> (a union b) isSubsetOf c Q.E.D.  \( A\cap B\subseteq A$$

>>> prove $$$a :: SI) b -> (a intersection b) isSubsetOf a Q.E.D.  \( A\cap B\subseteq B$$ >>> prove$ $$a :: SI) b -> (a intersection b) isSubsetOf b Q.E.D.  \( C\subseteq A \land C\subseteq B \Rightarrow C \subseteq (A \cap B)$$

>>> prove $$$a :: SI) b c -> c isSubsetOf a .&& c isSubsetOf b .=> c isSubsetOf (a intersection b) Q.E.D.  # Subset characterization There are multiple equivalent ways of characterizing the subset relationship: \( A\subseteq B \iff A \cap B = A$$ >>> prove$ $$a :: SI) b -> a isSubsetOf b .<=> a intersection b .== a Q.E.D.  \( A\subseteq B \iff A \cup B = B$$

>>> prove $$$a :: SI) b -> a isSubsetOf b .<=> a union b .== b Q.E.D.  \( A\subseteq B \iff A \setminus B = \varnothing$$ >>> prove$ $$a :: SI) b -> a isSubsetOf b .<=> a difference b .== empty Q.E.D.  \( A\subseteq B \iff B^{C} \subseteq A^{C}$$

>>> prove $$$a :: SI) b -> a isSubsetOf b .<=> complement b isSubsetOf complement a Q.E.D.  # Relative complements \( C\setminus (A\cap B)=(C\setminus A)\cup (C\setminus B)$$ >>> prove$ $$a :: SI) b c -> c \\ (a intersection b) .== (c \\ a) union (c \\ b) Q.E.D.  \( C\setminus (A\cup B)=(C\setminus A)\cap (C\setminus B)$$

>>> prove $$$a :: SI) b c -> c \\ (a union b) .== (c \\ a) intersection (c \\ b) Q.E.D.  \( \displaystyle C\setminus (B\setminus A)=(A\cap C)\cup (C\setminus B)$$ >>> prove$ $$a :: SI) b c -> c \\ (b \\ a) .== (a intersection c) union (c \\ b) Q.E.D.  \( (B\setminus A)\cap C = (B\cap C)\setminus A$$

>>> prove $$$a :: SI) b c -> (b \\ a) intersection c .== (b intersection c) \\ a Q.E.D.  \( (B\setminus A)\cap C= B\cap (C\setminus A)$$ >>> prove$ $$a :: SI) b c -> (b \\ a) intersection c .== b intersection (c \\ a) Q.E.D.  \( (B\setminus A)\cup C=(B\cup C)\setminus (A\setminus C)$$

>>> prove $$$a :: SI) b c -> (b \\ a) union c .== (b union c) \\ (a \\ c) Q.E.D.  \( A \setminus A = \varnothing$$ >>> prove$ $$a :: SI) -> a \\ a .== empty Q.E.D.  \( \varnothing \setminus A = \varnothing$$

>>> prove $$$a :: SI) -> empty \\ a .== empty Q.E.D.  \( A \setminus \varnothing = A$$ >>> prove$ $$a :: SI) -> a \\ empty .== a Q.E.D.  \( B \setminus A = A^{C} \cap B$$

>>> prove $$$a :: SI) b -> b \\ a .== complement a intersection b Q.E.D.  \( {(B \setminus A)}^{C} = A \cup B^{C}$$ >>> prove$ $$a :: SI) b -> complement (b \\ a) .== a union complement b Q.E.D.  \( U \setminus A = A^{C}$$

>>> prove $$$a :: SI) -> full \\ a .== complement a Q.E.D.  \( A \setminus U = \varnothing$$ >>> prove$ $$a :: SI) -> a \\ full .== empty Q.E.D.  # Distributing subset relation A common mistake newcomers to set theory make is to distribute the subset relationship over intersection and unions, which is only true as described above. Here, we use SBV to show two incorrect cases: Subset relation does not distribute over union on the left: \(A \subseteq (B \cup C) \nRightarrow A \subseteq B \land A \subseteq C$$

>>> prove $$$a :: SI) b c -> a isSubsetOf (b union c) .=> a isSubsetOf b .&& a isSubsetOf c Falsifiable. Counter-example: s0 = {0} :: {Integer} s1 = U :: {Integer} s2 = U - {0} :: {Integer}  Similarly, subset relation does not distribute over intersection on the right: \( (B \cap C) \subseteq A \nRightarrow B \subseteq A \land C \subseteq A$$ >>> prove$ \(a :: SI) b c -> (b intersection c) isSubsetOf a .=> b isSubsetOf a .&& c isSubsetOf a
Falsifiable. Counter-example:
s0 = U - {0} :: {Integer}
s1 =      {} :: {Integer}
s2 =     {0} :: {Integer}