From 9bff2987772443f0d5e450b2978fe8c93a0209a3 Mon Sep 17 00:00:00 2001
From: Regis Blanc <regwblanc@gmail.com>
Date: Wed, 8 Jul 2015 14:36:31 +0200
Subject: [PATCH] indepence of coins
---
testcases/proof/proba/Coins.scala | 57 +++++++++++++++++++++++++++----
1 file changed, 50 insertions(+), 7 deletions(-)
diff --git a/testcases/proof/proba/Coins.scala b/testcases/proof/proba/Coins.scala
index bc18f650e..a24211154 100644
--- a/testcases/proof/proba/Coins.scala
+++ b/testcases/proof/proba/Coins.scala
@@ -8,6 +8,7 @@ object Coins {
*/
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))
@@ -17,6 +18,26 @@ object Coins {
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
+
//sum modulo: face is 0, tail is 1
def sum(coin1: CoinDist, coin2: CoinDist): CoinDist = {
require(isDist(coin1) && isDist(coin2))
@@ -26,6 +47,14 @@ object Coins {
)
}
+ def sum(dist: CoinsJoinDist): CoinDist = {
+ require(isDist(dist))
+ CoinDist(
+ dist.hh + dist.tt,
+ dist.ht + dist.th
+ )
+ }
+
def sumIsUniform1(coin1: CoinDist, coin2: CoinDist): Boolean = {
require(isDist(coin1) && isDist(coin2) && isUniform(coin1) && isUniform(coin2))
val dist = sum(coin1, coin2)
@@ -38,6 +67,26 @@ object Coins {
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))
@@ -52,12 +101,6 @@ object Coins {
} //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 sumIsCommutative(coin1: CoinDist, coin2: CoinDist, coin3: CoinDist): Boolean = {
require(isDist(coin1) && isDist(coin2))
sum(coin1, coin2) == sum(coin2, coin1)
@@ -66,6 +109,6 @@ object Coins {
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
+ } //holds
}
--
GitLab