diff --git a/testcases/proof/proba/Coins.scala b/testcases/proof/proba/Coins.scala
index ff8bf91222b6493591be4e279a6069218c781d2f..0a84cb072700fe9a4070ec0ed4003b4596bb03d7 100644
--- a/testcases/proof/proba/Coins.scala
+++ b/testcases/proof/proba/Coins.scala
@@ -3,24 +3,29 @@ import leon.lang._
object Coins {
- /*
- * number of outcomes for each face
- */
- case class CoinDist(pHead: BigInt, pTail: BigInt)
+ case class CoinDist(pHead: Rational) {
+ def pTail: Rational = Rational(1) - pHead
+ }
+
+ def isDist(dist: CoinDist): Boolean =
+ dist.pHead.isRational && dist.pHead >= Rational(0) && dist.pHead <= Rational(1)
+
+
+ case class CoinsJoinDist(hh: Rational, ht: Rational, th: Rational, tt: Rational)
+
+ def isDist(dist: CoinsJoinDist): Boolean =
+ dist.hh.isRational && dist.hh >= Rational(0) && dist.hh <= Rational(1) &&
+ dist.ht.isRational && dist.ht >= Rational(0) && dist.ht <= Rational(1) &&
+ dist.th.isRational && dist.th >= Rational(0) && dist.th <= Rational(1) &&
+ dist.tt.isRational && dist.tt >= Rational(0) && dist.tt <= Rational(1) &&
+ (dist.hh + dist.ht + dist.th + dist.tt) ~ Rational(1)
- case class CoinsJoinDist(hh: BigInt, ht: BigInt, th: BigInt, tt: BigInt)
def isUniform(dist: CoinDist): Boolean = {
require(isDist(dist))
- dist.pHead == dist.pTail
+ dist.pHead ~ Rational(1, 2)
}
- def isDist(dist: CoinDist): Boolean =
- dist.pHead >= 0 && dist.pTail >= 0 && (dist.pHead > 0 || dist.pTail > 0)
-
- def isDist(dist: CoinsJoinDist): Boolean =
- dist.hh >= 0 && dist.ht >= 0 && dist.th >= 0 && dist.tt >= 0 &&
- (dist.hh > 0 || dist.ht > 0 || dist.th > 0 || dist.tt > 0)
def join(c1: CoinDist, c2: CoinDist): CoinsJoinDist =
CoinsJoinDist(
@@ -29,82 +34,76 @@ object Coins {
c1.pTail*c2.pHead,
c1.pTail*c2.pTail)
- def firstCoin(dist: CoinsJoinDist): CoinDist =
- CoinDist(dist.hh + dist.ht, dist.th + dist.tt)
+ def firstCoin(dist: CoinsJoinDist): CoinDist = {
+ CoinDist(dist.hh + dist.ht)
+ } ensuring(res => res.pTail ~ (dist.th + dist.tt))
- def secondCoin(dist: CoinsJoinDist): CoinDist =
- CoinDist(dist.hh + dist.th, dist.ht + dist.tt)
+ def secondCoin(dist: CoinsJoinDist): CoinDist = {
+ CoinDist(dist.hh + dist.th)
+ } ensuring(res => res.pTail ~ (dist.ht + dist.tt))
def isIndependent(dist: CoinsJoinDist): Boolean =
join(firstCoin(dist), secondCoin(dist)) == dist
def isEquivalent(dist1: CoinsJoinDist, dist2: CoinsJoinDist): Boolean = {
- require(isDist(dist1) && dist1.hh > 0 && isDist(dist2) && dist2.hh > 0)
+ require(isDist(dist1) && isDist(dist2))
- dist1.hh*dist2.hh == dist2.hh*dist1.hh &&
- dist1.ht*dist2.hh == dist2.ht*dist1.hh &&
- dist1.th*dist2.hh == dist2.th*dist1.hh &&
- dist1.tt*dist2.hh == dist2.tt*dist1.hh
+ (dist1.hh ~ dist2.hh) &&
+ (dist1.ht ~ dist2.ht) &&
+ (dist1.th ~ dist2.th) &&
+ (dist1.tt ~ dist2.tt)
}
- case class CoinCondDist(ifHead: CoinDist, ifTail: CoinDist)
+ //case class CoinCondDist(ifHead: CoinDist, ifTail: CoinDist)
- def condByFirstCoin(dist: CoinsJoinDist): CoinCondDist = {
- CoinCondDist(
- CoinDist(
- dist.hh*(dist.th + dist.tt), //probability of head if head
- dist.ht*(dist.th + dist.tt) //probability of tail if head
- ),
- CoinDist(
- dist.th*(dist.hh + dist.ht), //probability of head if tail
- dist.tt*(dist.hh + dist.ht) //probability of tail if tail
- )
- )
- }
+ //def condByFirstCoin(dist: CoinsJoinDist): CoinCondDist = {
+ // CoinCondDist(
+ // CoinDist(
+ // dist.hh*(dist.th + dist.tt), //probability of head if head
+ // dist.ht*(dist.th + dist.tt) //probability of tail if head
+ // ),
+ // CoinDist(
+ // dist.th*(dist.hh + dist.ht), //probability of head if tail
+ // dist.tt*(dist.hh + dist.ht) //probability of tail if tail
+ // )
+ // )
+ //}
- def combine(cond: CoinCondDist, dist: CoinDist): CoinsJoinDist = {
- require(isDist(dist) && dist.pHead > 0 && dist.pTail > 0)
+ //def combine(cond: CoinCondDist, dist: CoinDist): CoinsJoinDist = {
+ // require(isDist(dist) && dist.pHead > 0 && dist.pTail > 0)
- val hh = cond.ifHead.pHead * dist.pHead
- val ht = cond.ifHead.pTail * dist.pHead
- val th = cond.ifTail.pHead * dist.pTail
- val tt = cond.ifTail.pTail * dist.pTail
- CoinsJoinDist(hh, ht, th, tt)
- }
-
- def condIsSound(dist: CoinsJoinDist): Boolean = {
- require(isDist(dist) && dist.hh > 0 && dist.ht > 0 && dist.th > 0 && dist.tt > 0)
+ // val hh = cond.ifHead.pHead * dist.pHead
+ // val ht = cond.ifHead.pTail * dist.pHead
+ // val th = cond.ifTail.pHead * dist.pTail
+ // val tt = cond.ifTail.pTail * dist.pTail
+ // CoinsJoinDist(hh, ht, th, tt)
+ //}
+ //
+ //def condIsSound(dist: CoinsJoinDist): Boolean = {
+ // require(isDist(dist) && dist.hh > 0 && dist.ht > 0 && dist.th > 0 && dist.tt > 0)
- val computedDist = combine(condByFirstCoin(dist), firstCoin(dist))
- isEquivalent(dist, computedDist)
- } holds
+ // val computedDist = combine(condByFirstCoin(dist), firstCoin(dist))
+ // isEquivalent(dist, computedDist)
+ //} holds
//should be INVALID
def anyDistributionsNotEquivalent(dist1: CoinsJoinDist, dist2: CoinsJoinDist): Boolean = {
- require(isDist(dist1) && isDist(dist2) && dist1.hh > 0 && dist2.hh > 0)
+ require(isDist(dist1) && isDist(dist2))
isEquivalent(dist1, dist2)
} holds
//sum modulo: face is 0, tail is 1
def sum(coin1: CoinDist, coin2: CoinDist): CoinDist = {
require(isDist(coin1) && isDist(coin2))
- CoinDist(
- coin1.pHead*coin2.pHead + coin1.pTail*coin2.pTail,
- coin1.pHead*coin2.pTail + coin1.pTail*coin2.pHead
- )
- }
+ CoinDist(coin1.pHead*coin2.pHead + coin1.pTail*coin2.pTail)
+ } ensuring(res => res.pTail ~ (coin1.pHead*coin2.pTail + coin1.pTail*coin2.pHead))
def sum(dist: CoinsJoinDist): CoinDist = {
require(isDist(dist))
- CoinDist(
- dist.hh + dist.tt,
- dist.ht + dist.th
- )
- }
-
-
+ CoinDist(dist.hh + dist.tt)
+ } ensuring(res => res.pTail ~ (dist.ht + dist.th))
@@ -113,73 +112,73 @@ object Coins {
* properties of sum operation *
***************************************************/
- def sumIsUniform1(coin1: CoinDist, coin2: CoinDist): Boolean = {
- require(isDist(coin1) && isDist(coin2) && isUniform(coin1) && isUniform(coin2))
- val dist = sum(coin1, coin2)
- isUniform(dist)
- } holds
-
- def sumIsUniform2(coin1: CoinDist, coin2: CoinDist): Boolean = {
- require(isDist(coin1) && isDist(coin2) && isUniform(coin1))
- val dist = sum(coin1, coin2)
- isUniform(dist)
- } holds
-
- def sumUniform3(coin1: CoinDist, coin2: CoinDist, coin3: CoinDist): Boolean = {
- require(isDist(coin1) && isDist(coin2) && isDist(coin3) && isUniform(coin1))
- val dist = sum(sum(coin1, coin2), coin3)
- isUniform(dist)
- } holds
-
- def sumUniformWithIndependence(dist: CoinsJoinDist): Boolean = {
- require(isDist(dist) && isIndependent(dist) && (isUniform(firstCoin(dist)) || isUniform(secondCoin(dist))))
- val res = sum(dist)
- isUniform(res)
- } holds
-
- //should find counterexample, indepenence is required
- def sumUniformWithoutIndependence(dist: CoinsJoinDist): Boolean = {
- require(isDist(dist) && (isUniform(firstCoin(dist)) || isUniform(secondCoin(dist))))
- val res = sum(dist)
- isUniform(res)
- } holds
-
-
- //sum of two non-uniform dices is potentially uniform (no result)
- def sumNonUniform1(coin1: CoinDist, coin2: CoinDist): Boolean = {
- require(isDist(coin1) && isDist(coin2) && !isUniform(coin1) && !isUniform(coin2))
- val dist = sum(coin1, coin2)
- !isUniform(dist)
- } holds
-
- def sumNonUniform2(coin1: CoinDist, coin2: CoinDist, coin3: CoinDist): Boolean = {
- require(isDist(coin1) && isDist(coin2) && isDist(coin3) && !isUniform(coin1) && !isUniform(coin2) && !isUniform(coin3))
- val dist = sum(sum(coin1, coin2), coin3)
- !isUniform(dist)
- } //holds
-
- def sumNonUniformWithIndependence(dist: CoinsJoinDist): Boolean = {
- require(isDist(dist) && isIndependent(dist) && !isUniform(firstCoin(dist)) && !isUniform(secondCoin(dist)))
- val res = sum(dist)
- !isUniform(res)
- } holds
-
- //independence is required
- def sumNonUniformWithoutIndependence(dist: CoinsJoinDist): Boolean = {
- require(isDist(dist) && !isUniform(firstCoin(dist)) && !isUniform(secondCoin(dist)))
- val res = sum(dist)
- !isUniform(res)
- } holds
-
-
- def sumIsCommutative(coin1: CoinDist, coin2: CoinDist, coin3: CoinDist): Boolean = {
- require(isDist(coin1) && isDist(coin2))
- sum(coin1, coin2) == sum(coin2, coin1)
- } holds
-
- def sumIsAssociative(coin1: CoinDist, coin2: CoinDist, coin3: CoinDist): Boolean = {
- require(isDist(coin1) && isDist(coin2) && isDist(coin3))
- sum(sum(coin1, coin2), coin3) == sum(coin1, sum(coin2, coin3))
- } //holds
+ //def sumIsUniform1(coin1: CoinDist, coin2: CoinDist): Boolean = {
+ // require(isDist(coin1) && isDist(coin2) && isUniform(coin1) && isUniform(coin2))
+ // val dist = sum(coin1, coin2)
+ // isUniform(dist)
+ //} holds
+
+ //def sumIsUniform2(coin1: CoinDist, coin2: CoinDist): Boolean = {
+ // require(isDist(coin1) && isDist(coin2) && isUniform(coin1))
+ // val dist = sum(coin1, coin2)
+ // isUniform(dist)
+ //} holds
+
+ //def sumUniform3(coin1: CoinDist, coin2: CoinDist, coin3: CoinDist): Boolean = {
+ // require(isDist(coin1) && isDist(coin2) && isDist(coin3) && isUniform(coin1))
+ // val dist = sum(sum(coin1, coin2), coin3)
+ // isUniform(dist)
+ //} holds
+
+ //def sumUniformWithIndependence(dist: CoinsJoinDist): Boolean = {
+ // require(isDist(dist) && isIndependent(dist) && (isUniform(firstCoin(dist)) || isUniform(secondCoin(dist))))
+ // val res = sum(dist)
+ // isUniform(res)
+ //} holds
+
+ ////should find counterexample, indepenence is required
+ //def sumUniformWithoutIndependence(dist: CoinsJoinDist): Boolean = {
+ // require(isDist(dist) && (isUniform(firstCoin(dist)) || isUniform(secondCoin(dist))))
+ // val res = sum(dist)
+ // isUniform(res)
+ //} holds
+
+
+ ////sum of two non-uniform dices is potentially uniform (no result)
+ //def sumNonUniform1(coin1: CoinDist, coin2: CoinDist): Boolean = {
+ // require(isDist(coin1) && isDist(coin2) && !isUniform(coin1) && !isUniform(coin2))
+ // val dist = sum(coin1, coin2)
+ // !isUniform(dist)
+ //} holds
+
+ //def sumNonUniform2(coin1: CoinDist, coin2: CoinDist, coin3: CoinDist): Boolean = {
+ // require(isDist(coin1) && isDist(coin2) && isDist(coin3) && !isUniform(coin1) && !isUniform(coin2) && !isUniform(coin3))
+ // val dist = sum(sum(coin1, coin2), coin3)
+ // !isUniform(dist)
+ //} //holds
+
+ //def sumNonUniformWithIndependence(dist: CoinsJoinDist): Boolean = {
+ // require(isDist(dist) && isIndependent(dist) && !isUniform(firstCoin(dist)) && !isUniform(secondCoin(dist)))
+ // val res = sum(dist)
+ // !isUniform(res)
+ //} holds
+
+ ////independence is required
+ //def sumNonUniformWithoutIndependence(dist: CoinsJoinDist): Boolean = {
+ // require(isDist(dist) && !isUniform(firstCoin(dist)) && !isUniform(secondCoin(dist)))
+ // val res = sum(dist)
+ // !isUniform(res)
+ //} holds
+
+
+ //def sumIsCommutative(coin1: CoinDist, coin2: CoinDist, coin3: CoinDist): Boolean = {
+ // require(isDist(coin1) && isDist(coin2))
+ // sum(coin1, coin2) == sum(coin2, coin1)
+ //} holds
+
+ //def sumIsAssociative(coin1: CoinDist, coin2: CoinDist, coin3: CoinDist): Boolean = {
+ // require(isDist(coin1) && isDist(coin2) && isDist(coin3))
+ // sum(sum(coin1, coin2), coin3) == sum(coin1, sum(coin2, coin3))
+ //} //holds
}
diff --git a/testcases/proof/proba/ints/Coins.scala b/testcases/proof/proba/ints/Coins.scala
new file mode 100644
index 0000000000000000000000000000000000000000..ff8bf91222b6493591be4e279a6069218c781d2f
--- /dev/null
+++ b/testcases/proof/proba/ints/Coins.scala
@@ -0,0 +1,185 @@
+import leon.annotation._
+import leon.lang._
+
+object Coins {
+
+ /*
+ * number of outcomes for each face
+ */
+ case class CoinDist(pHead: BigInt, pTail: BigInt)
+
+ case class CoinsJoinDist(hh: BigInt, ht: BigInt, th: BigInt, tt: BigInt)
+
+ def isUniform(dist: CoinDist): Boolean = {
+ require(isDist(dist))
+ dist.pHead == dist.pTail
+ }
+
+ def isDist(dist: CoinDist): Boolean =
+ dist.pHead >= 0 && dist.pTail >= 0 && (dist.pHead > 0 || dist.pTail > 0)
+
+ def isDist(dist: CoinsJoinDist): Boolean =
+ dist.hh >= 0 && dist.ht >= 0 && dist.th >= 0 && dist.tt >= 0 &&
+ (dist.hh > 0 || dist.ht > 0 || dist.th > 0 || dist.tt > 0)
+
+ def join(c1: CoinDist, c2: CoinDist): CoinsJoinDist =
+ CoinsJoinDist(
+ c1.pHead*c2.pHead,
+ c1.pHead*c2.pTail,
+ c1.pTail*c2.pHead,
+ c1.pTail*c2.pTail)
+
+ def firstCoin(dist: CoinsJoinDist): CoinDist =
+ CoinDist(dist.hh + dist.ht, dist.th + dist.tt)
+
+ def secondCoin(dist: CoinsJoinDist): CoinDist =
+ CoinDist(dist.hh + dist.th, dist.ht + dist.tt)
+
+ def isIndependent(dist: CoinsJoinDist): Boolean =
+ join(firstCoin(dist), secondCoin(dist)) == dist
+
+ def isEquivalent(dist1: CoinsJoinDist, dist2: CoinsJoinDist): Boolean = {
+ require(isDist(dist1) && dist1.hh > 0 && isDist(dist2) && dist2.hh > 0)
+
+ dist1.hh*dist2.hh == dist2.hh*dist1.hh &&
+ dist1.ht*dist2.hh == dist2.ht*dist1.hh &&
+ dist1.th*dist2.hh == dist2.th*dist1.hh &&
+ dist1.tt*dist2.hh == dist2.tt*dist1.hh
+ }
+
+
+ case class CoinCondDist(ifHead: CoinDist, ifTail: CoinDist)
+
+ def condByFirstCoin(dist: CoinsJoinDist): CoinCondDist = {
+ CoinCondDist(
+ CoinDist(
+ dist.hh*(dist.th + dist.tt), //probability of head if head
+ dist.ht*(dist.th + dist.tt) //probability of tail if head
+ ),
+ CoinDist(
+ dist.th*(dist.hh + dist.ht), //probability of head if tail
+ dist.tt*(dist.hh + dist.ht) //probability of tail if tail
+ )
+ )
+ }
+
+ def combine(cond: CoinCondDist, dist: CoinDist): CoinsJoinDist = {
+ require(isDist(dist) && dist.pHead > 0 && dist.pTail > 0)
+
+ val hh = cond.ifHead.pHead * dist.pHead
+ val ht = cond.ifHead.pTail * dist.pHead
+ val th = cond.ifTail.pHead * dist.pTail
+ val tt = cond.ifTail.pTail * dist.pTail
+ CoinsJoinDist(hh, ht, th, tt)
+ }
+
+ def condIsSound(dist: CoinsJoinDist): Boolean = {
+ require(isDist(dist) && dist.hh > 0 && dist.ht > 0 && dist.th > 0 && dist.tt > 0)
+
+ val computedDist = combine(condByFirstCoin(dist), firstCoin(dist))
+ isEquivalent(dist, computedDist)
+ } holds
+
+
+ //should be INVALID
+ def anyDistributionsNotEquivalent(dist1: CoinsJoinDist, dist2: CoinsJoinDist): Boolean = {
+ require(isDist(dist1) && isDist(dist2) && dist1.hh > 0 && dist2.hh > 0)
+ isEquivalent(dist1, dist2)
+ } holds
+
+ //sum modulo: face is 0, tail is 1
+ def sum(coin1: CoinDist, coin2: CoinDist): CoinDist = {
+ require(isDist(coin1) && isDist(coin2))
+ CoinDist(
+ coin1.pHead*coin2.pHead + coin1.pTail*coin2.pTail,
+ coin1.pHead*coin2.pTail + coin1.pTail*coin2.pHead
+ )
+ }
+
+ def sum(dist: CoinsJoinDist): CoinDist = {
+ require(isDist(dist))
+ CoinDist(
+ dist.hh + dist.tt,
+ dist.ht + dist.th
+ )
+ }
+
+
+
+
+
+
+ /***************************************************
+ * properties of sum operation *
+ ***************************************************/
+
+ def sumIsUniform1(coin1: CoinDist, coin2: CoinDist): Boolean = {
+ require(isDist(coin1) && isDist(coin2) && isUniform(coin1) && isUniform(coin2))
+ val dist = sum(coin1, coin2)
+ isUniform(dist)
+ } holds
+
+ def sumIsUniform2(coin1: CoinDist, coin2: CoinDist): Boolean = {
+ require(isDist(coin1) && isDist(coin2) && isUniform(coin1))
+ val dist = sum(coin1, coin2)
+ isUniform(dist)
+ } holds
+
+ def sumUniform3(coin1: CoinDist, coin2: CoinDist, coin3: CoinDist): Boolean = {
+ require(isDist(coin1) && isDist(coin2) && isDist(coin3) && isUniform(coin1))
+ val dist = sum(sum(coin1, coin2), coin3)
+ isUniform(dist)
+ } holds
+
+ def sumUniformWithIndependence(dist: CoinsJoinDist): Boolean = {
+ require(isDist(dist) && isIndependent(dist) && (isUniform(firstCoin(dist)) || isUniform(secondCoin(dist))))
+ val res = sum(dist)
+ isUniform(res)
+ } holds
+
+ //should find counterexample, indepenence is required
+ def sumUniformWithoutIndependence(dist: CoinsJoinDist): Boolean = {
+ require(isDist(dist) && (isUniform(firstCoin(dist)) || isUniform(secondCoin(dist))))
+ val res = sum(dist)
+ isUniform(res)
+ } holds
+
+
+ //sum of two non-uniform dices is potentially uniform (no result)
+ def sumNonUniform1(coin1: CoinDist, coin2: CoinDist): Boolean = {
+ require(isDist(coin1) && isDist(coin2) && !isUniform(coin1) && !isUniform(coin2))
+ val dist = sum(coin1, coin2)
+ !isUniform(dist)
+ } holds
+
+ def sumNonUniform2(coin1: CoinDist, coin2: CoinDist, coin3: CoinDist): Boolean = {
+ require(isDist(coin1) && isDist(coin2) && isDist(coin3) && !isUniform(coin1) && !isUniform(coin2) && !isUniform(coin3))
+ val dist = sum(sum(coin1, coin2), coin3)
+ !isUniform(dist)
+ } //holds
+
+ def sumNonUniformWithIndependence(dist: CoinsJoinDist): Boolean = {
+ require(isDist(dist) && isIndependent(dist) && !isUniform(firstCoin(dist)) && !isUniform(secondCoin(dist)))
+ val res = sum(dist)
+ !isUniform(res)
+ } holds
+
+ //independence is required
+ def sumNonUniformWithoutIndependence(dist: CoinsJoinDist): Boolean = {
+ require(isDist(dist) && !isUniform(firstCoin(dist)) && !isUniform(secondCoin(dist)))
+ val res = sum(dist)
+ !isUniform(res)
+ } holds
+
+
+ def sumIsCommutative(coin1: CoinDist, coin2: CoinDist, coin3: CoinDist): Boolean = {
+ require(isDist(coin1) && isDist(coin2))
+ sum(coin1, coin2) == sum(coin2, coin1)
+ } holds
+
+ def sumIsAssociative(coin1: CoinDist, coin2: CoinDist, coin3: CoinDist): Boolean = {
+ require(isDist(coin1) && isDist(coin2) && isDist(coin3))
+ sum(sum(coin1, coin2), coin3) == sum(coin1, sum(coin2, coin3))
+ } //holds
+
+}
diff --git a/testcases/proof/proba/Dices.scala b/testcases/proof/proba/ints/Dices.scala
similarity index 100%
rename from testcases/proof/proba/Dices.scala
rename to testcases/proof/proba/ints/Dices.scala
diff --git a/testcases/proof/proba/FiniteDistributions.scala b/testcases/proof/proba/ints/FiniteDistributions.scala
similarity index 100%
rename from testcases/proof/proba/FiniteDistributions.scala
rename to testcases/proof/proba/ints/FiniteDistributions.scala
diff --git a/testcases/proof/proba/RandomVariables.scala b/testcases/proof/proba/ints/RandomVariables.scala
similarity index 100%
rename from testcases/proof/proba/RandomVariables.scala
rename to testcases/proof/proba/ints/RandomVariables.scala