typelevel / algebra
 1 ```package algebra.laws ``` 2 3 ```import algebra._ ``` 4 ```import algebra.lattice.{Heyting, Bool, GenBool} ``` 5 6 ```import org.scalacheck.{Arbitrary, Prop} ``` 7 ```import org.scalacheck.Prop._ ``` 8 9 ```object LogicLaws { ``` 10 3 ``` def apply[A: Eq: Arbitrary] = new LogicLaws[A] { ``` 11 3 ``` def Equ = Eq[A] ``` 12 3 ``` def Arb = implicitly[Arbitrary[A]] ``` 13 ``` } ``` 14 ```} ``` 15 16 ```trait LogicLaws[A] extends LatticeLaws[A] { ``` 17 18 3 ``` def heyting(implicit A: Heyting[A]) = new LogicProperties( ``` 19 3 ``` name = "heyting", ``` 20 3 ``` parents = Seq(), ``` 21 3 ``` ll = boundedDistributiveLattice, ``` 22 23 3 ``` Rules.distributive(A.or)(A.and), ``` 24 25 3 ``` "consistent" -> forAll { (x: A) => A.and(x, A.complement(x)) ?== A.zero }, ``` 26 3 ``` "¬x = (x → 0)" -> forAll { (x: A) => A.complement(x) ?== A.imp(x, A.zero) }, ``` 27 3 ``` "x → x = 1" -> forAll { (x: A) => A.imp(x, x) ?== A.one }, ``` 28 29 3 ``` "if x → y and y → x then x=y" -> forAll { (x: A, y: A) => ``` 30 3 ``` (A.imp(x, y) ?!= A.one) || (A.imp(y, x) ?!= A.one) || (x ?== y) ``` 31 ``` }, ``` 32 33 3 ``` "if (1 → x)=1 then x=1" -> forAll { (x: A) => ``` 34 3 ``` (A.imp(A.one, x) ?!= A.one) || (x ?== A.one) ``` 35 ``` }, ``` 36 37 3 ``` "x → (y → x) = 1" -> forAll { (x: A, y: A) => A.imp(x, A.imp(y, x)) ?== A.one }, ``` 38 39 3 ``` "(x→(y→z)) → ((x→y)→(x→z)) = 1" -> forAll { (x: A, y: A, z: A) => ``` 40 3 ``` A.imp(A.imp(x, A.imp(y, z)), A.imp(A.imp(x, y), A.imp(x, z))) ?== A.one ``` 41 ``` }, ``` 42 43 3 ``` "x∧y → x = 1" -> forAll { (x: A, y: A) => A.imp(A.and(x, y), x) ?== A.one }, ``` 44 3 ``` "x∧y → y = 1" -> forAll { (x: A, y: A) => A.imp(A.and(x, y), y) ?== A.one }, ``` 45 3 ``` "x → y → (x∧y) = 1" -> forAll { (x: A, y: A) => A.imp(x, A.imp(y, A.and(x, y))) ?== A.one }, ``` 46 47 3 ``` "x → x∨y" -> forAll { (x: A, y: A) => A.imp(x, A.or(x, y)) ?== A.one }, ``` 48 3 ``` "y → x∨y" -> forAll { (x: A, y: A) => A.imp(y, A.or(x, y)) ?== A.one }, ``` 49 50 3 ``` "(x → z) → ((y → z) → ((x | y) → z)) = 1" -> forAll { (x: A, y: A, z: A) => ``` 51 3 ``` A.imp(A.imp(x, z), A.imp(A.imp(y, z), A.imp(A.or(x, y), z))) ?== A.one ``` 52 ``` }, ``` 53 54 3 ``` "(0 → x) = 1" -> forAll { (x: A) => A.imp(A.zero, x) ?== A.one } ``` 55 ``` ) ``` 56 57 3 ``` def generalizedBool(implicit A: GenBool[A]) = new LogicProperties( ``` 58 3 ``` name = "generalized bool", ``` 59 3 ``` parents = Seq(), ``` 60 3 ``` ll = new LatticeProperties( ``` 61 3 ``` name = "lowerBoundedDistributiveLattice", ``` 62 3 ``` parents = Seq(boundedJoinSemilattice, distributiveLattice), ``` 63 3 ``` join = Some(boundedSemilattice(A.joinSemilattice)), ``` 64 3 ``` meet = Some(semilattice(A.meetSemilattice)) ``` 65 ``` ), ``` 66 67 3 ``` """x\y ∧ y = 0""" -> forAll { (x: A, y: A) => ``` 68 3 ``` A.and(A.without(x, y), y) ?== A.zero }, ``` 69 70 3 ``` """x\y ∨ y = x ∨ y""" -> forAll { (x: A, y: A) => ``` 71 3 ``` A.or(A.without(x, y), y) ?== A.or(x, y) } ``` 72 ``` ) ``` 73 74 3 ``` def bool(implicit A: Bool[A]) = new LogicProperties( ``` 75 3 ``` name = "bool", ``` 76 3 ``` parents = Seq(heyting, generalizedBool), ``` 77 3 ``` ll = boundedDistributiveLattice, ``` 78 79 3 ``` "excluded middle" -> forAll { (x: A) => A.or(x, A.complement(x)) ?== A.one } ``` 80 ``` ) ``` 81 82 ``` class LogicProperties( ``` 83 ``` val name: String, ``` 84 ``` val parents: Seq[LogicProperties], ``` 85 ``` val ll: LatticeProperties, ``` 86 ``` val props: (String, Prop)* ``` 87 ``` ) extends RuleSet { ``` 88 3 ``` val bases = Seq("lattice" -> ll) ``` 89 ``` } ``` 90 91 ```} ```

Read our documentation on viewing source code .