theorem prover.md

Here’s more detail on what I want to be able to do. I want to be able to write class hierarchies and reason about what properties are possible for objects which have particular classes. I have no idea whether something like this exists.

abstract class Animal {
  def makeNoise(): String
  
  def numberOfLegs: Int
}

abstract class Insect extends Animal {
  def numberOfLegs = 6
}

class Bee extends Animal {
  def makeNoise() = "Buzz!"
}

class Dog extends Animal {
  def makeNoise() = "Woof!"
  def numberOfLegs = 4
}

object Reasoner {
  def main(args: Array[String]) {
    // Do animals all make the noise "Woof!"?
    println(TheoremProver.check(
      ForAll[Animal]((animal) => animal.makeNoise() == "Woof!")
    ))
    // #=> No, there are animals which don't, eg bees.
    
    // Do any animals make the noise "Woof!"?
    println(TheoremProver.check(
      ThereExists[Animal]((animal) => animal.makeNoise() == "Woof!")
    ))
    // #=> Yes, dogs do.
    
    // Do any animals make the noise "Meow"?
    println(TheoremProver.check(
      ThereExists[Animal]((animal) => animal.makeNoise() == "Meow")
    ))
    // #=> I don't know. No animals that I'm aware of do that, but
    // for all I know some other animal exists. (The class Animal
    // was not defined as "sealed", so other implementations could
    // exist.)
    
    // Do all insects have six legs?
    println(TheoremProver.check(
      ForAll[Insect]((insect) => insect.numberOfLegs() == 6)
    ))
    // # => Yes!
    // Note that this is not actually true in Scala, because I can
    // override definitions.
  }
}