From 24688442f554582583a3a9833f13759c5d534b6b Mon Sep 17 00:00:00 2001
From: Sandro Stucki <sandro.stucki@gmail.com>
Date: Wed, 19 Aug 2015 09:06:56 +0200
Subject: [PATCH] Adds DSL for proofs.
---
library/proof/Internal.scala | 61 ++++++++++++++++++++++++++++++++++++
library/proof/package.scala | 59 ++++++++++++++++++++++++++++++++++
2 files changed, 120 insertions(+)
create mode 100644 library/proof/Internal.scala
create mode 100644 library/proof/package.scala
diff --git a/library/proof/Internal.scala b/library/proof/Internal.scala
new file mode 100644
index 000000000..3ac290310
--- /dev/null
+++ b/library/proof/Internal.scala
@@ -0,0 +1,61 @@
+/* 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))
+ }
+ }
+}
diff --git a/library/proof/package.scala b/library/proof/package.scala
new file mode 100644
index 000000000..fd07a8128
--- /dev/null
+++ b/library/proof/package.scala
@@ -0,0 +1,59 @@
+/* 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)
+
+}
+
--
GitLab