Adds DSL for proofs.

library/proof/Internal.scala

+/* Copyright 2009-2014 EPFL, Lausanne */
+package leon.proof
+
+import leon.lang._
+
+/** Internal helper classes and methods for the 'proof' package. */
+object Internal {
+
+  /*** Helper classes for relational reasoning ***/
+
+  case class WithRel[A, B](x: A, r: (A, B) => Boolean, prop: Boolean) {
+
+    /** Continue with the next relation. */
+    def ^^(y: B): RelReasoning[B] = {
+      require(prop ==> r(x, y))
+      RelReasoning(y, prop && r(x, y))
+    }
+
+    /** Add a proof. */
+    def ^^|(proof: Boolean): WithProof[A, B] = {
+      require(proof)
+      WithProof(x, r, proof, prop)
+    }
+
+    /** Short-hand for equational reasoning. */
+    def ==|(proof: Boolean): WithProof[A, A] = {
+      require(proof)
+      WithProof(x, _ == _, proof, prop)
+    }
+
+    def qed: Boolean = prop
+  }
+
+  case class WithProof[A, B](
+    x: A, r: (A, B) => Boolean, proof: Boolean, prop: Boolean) {
+
+    /** Close a proof. */
+    def |[C](that: WithProof[B, C]): WithProof[B, C] = {
+      require(this.prop && this.proof ==> this.r(this.x, that.x))
+      WithProof(
+        that.x, that.r, that.proof,
+        this.prop && this.proof && this.r(this.x, that.x))
+    }
+
+    /** Close a proof. */
+    def |[C](that: WithRel[B, C]): WithRel[B, C] = {
+      require(this.prop && this.proof ==> this.r(this.x, that.x))
+      WithRel(
+        that.x, that.r,
+        this.prop && this.proof && this.r(this.x, that.x))
+    }
+
+    /** Close a proof. */
+    def |(that: RelReasoning[B]): RelReasoning[B] = {
+      require(this.prop && this.proof ==> this.r(this.x, that.x))
+      RelReasoning(
+        that.x,
+        this.prop && this.proof && this.r(this.x, that.x))
+    }
+  }
+}

library/proof/package.scala

+/* Copyright 2009-2014 EPFL, Lausanne */
+package leon
+
+import leon.annotation._
+import leon.lang._
+import scala.language.implicitConversions
+
+import leon.proof.Internal._
+
+package object proof {
+
+  case class ProofOps(prop: Boolean) {
+    def because(proof: Boolean): Boolean = proof && prop
+    def neverHolds: Boolean = {
+      require(!prop)
+      !prop
+    }
+  }
+
+  implicit def boolean2ProofOps(prop: Boolean): ProofOps = ProofOps(prop)
+
+  def trivial: Boolean = true
+
+  def by(proof: Boolean)(prop: Boolean): Boolean =
+    proof && prop
+
+  def check(prop: Boolean): Boolean = {
+    require(prop)
+    prop
+  }
+
+  /**
+   * Relational reasoning.
+   *
+   *         {
+   *           ((y :: ys) :+ x).last   ^^ _ == _ ^^| trivial         |
+   *           (y :: (ys :+ x)).last   ==| trivial         |
+   *           (ys :+ x).last          ==| snocLast(ys, x) |
+   *           x
+   *         }.qed
+   */
+  case class RelReasoning[A](x: A, prop: Boolean) {
+
+    def ^^[B](r: (A, B) => Boolean): WithRel[A, B] = WithRel(x, r, prop)
+
+    /** Short-hand for equational reasoning. */
+    def ==|(proof: Boolean): WithProof[A, A] = {
+      require(proof)
+      WithProof(x, _ == _, proof, prop)
+    }
+
+    def qed: Boolean = prop
+  }
+
+  implicit def any2RelReasoning[A](x: A): RelReasoning[A] =
+    RelReasoning(x, true)
+
+}
+