algebra.scala

// a ∨ (b ∨ c) = (a ∨ b) ∨ c, a ∧ (b ∧ c) = (a ∧ b) ∧ c                associativity
// a ∨ b = b ∨ a, a ∧ b = b ∧ a                                        commutativity
// a ∨ (a ∧ b) = a, a ∧ (a ∨ b) = a                                    absorption
// a ∨ 0 = a, a ∧ 1 = a                                                identity
// a ∨ (b ∧ c) = (a ∨ b) ∧ (a ∨ c), a ∧ (b ∨ c) = (a ∧ b) ∨ (a ∧ c)    distributivity
// a ∨ ¬a = 1, a ∧ ¬a = 0                                              complements
class AlgebraPoliceman[A : BooleanAlgebra : Arbitrary : Eq]() extends Properties("BooleanAlgebra") {
  def zero = implicitly[BooleanAlgebra[A]].zero
  def one  = implicitly[BooleanAlgebra[A]].one

  property("associative law (||)")  = forAll((a: A, b: A, c: A) => (a || (b || c)) === ((a || b) || c))
  property("associative law (&&)")  = forAll((a: A, b: A, c: A) => (a && (b && c)) === ((a && b) && c))
  property("distributive law (||)") = forAll((a: A, b: A, c: A) => (a || (b && c)) === ((a || b) && (a || c)))
  property("distributive law (&&)") = forAll((a: A, b: A, c: A) => (a && (b || c)) === ((a && b) || (a && c)))
  property("commutative law")       = forAll((a: A, b: A) => ((a || b) === (b || a)) && ((a && b) === (b && a)))
  property("absorption law")        = forAll((a: A, b: A) => ((a || (a && b)) === a) && (a && (a || b)) === a)
  property("identity law")          = forAll((a: A) => ((a || zero) === a) && ((a && one) === a))
  property("complement law")        = forAll((a: A) => ((a || !a) === one) && ((a && !a) === zero))
}