From d6d2ec505be3d2cbe4d0f9495381f91a8ae780f1 Mon Sep 17 00:00:00 2001
From: Regis Blanc <regwblanc@gmail.com>
Date: Mon, 29 Jun 2015 18:06:56 +0200
Subject: [PATCH] addition modulo 6
---
testcases/proof/proba/Dices.scala | 22 ++++++++++++++++++++++
1 file changed, 22 insertions(+)
diff --git a/testcases/proof/proba/Dices.scala b/testcases/proof/proba/Dices.scala
index 7932b982b..148e6d578 100644
--- a/testcases/proof/proba/Dices.scala
+++ b/testcases/proof/proba/Dices.scala
@@ -38,6 +38,18 @@ object Dices {
)
}
+ def sumMod(dice1: DiceDist, dice2: DiceDist): DiceDist = {
+ require(isDist(dice1) && isDist(dice2))
+ DiceDist(
+ dice1.p1*dice2.p6 + dice1.p2*dice2.p5 + dice1.p3*dice2.p4 + dice1.p4*dice2.p3 + dice1.p5*dice2.p2 + dice1.p6*dice2.p1, //1
+ dice1.p1*dice2.p1 + dice1.p2*dice2.p6 + dice1.p3*dice2.p5 + dice1.p4*dice2.p4 + dice1.p5*dice2.p3 + dice1.p6*dice2.p2, //2
+ dice1.p1*dice2.p2 + dice1.p2*dice2.p1 + dice1.p3*dice2.p6 + dice1.p4*dice2.p5 + dice1.p5*dice2.p4 + dice1.p6*dice2.p3, //3
+ dice1.p1*dice2.p3 + dice1.p2*dice2.p2 + dice1.p3*dice2.p1 + dice1.p4*dice2.p6 + dice1.p5*dice2.p5 + dice1.p6*dice2.p4, //4
+ dice1.p1*dice2.p4 + dice1.p2*dice2.p3 + dice1.p3*dice2.p2 + dice1.p4*dice2.p1 + dice1.p5*dice2.p6 + dice1.p6*dice2.p5, //5
+ dice1.p1*dice2.p5 + dice1.p2*dice2.p4 + dice1.p3*dice2.p3 + dice1.p4*dice2.p2 + dice1.p5*dice2.p1 + dice1.p6*dice2.p6 //6
+ )
+ }
+
def uniformSumProperties1(dice1: DiceDist, dice2: DiceDist): Boolean = {
require(isDist(dice1) && isDist(dice2) && isUniform(dice1) && isUniform(dice2))
val dist = sum(dice1, dice2)
@@ -59,5 +71,15 @@ object Dices {
dist.p7 > dist.p10 && dist.p7 > dist.p11 && dist.p7 > dist.p12
} holds
+ def sumModIsUniform1(dice1: DiceDist, dice2: DiceDist): Boolean = {
+ require(isDist(dice1) && isDist(dice2) && isUniform(dice1) && isUniform(dice2))
+ val dist = sumMod(dice1, dice2)
+ isUniform(dist)
+ } holds
+ def sumModIsUniform2(dice1: DiceDist, dice2: DiceDist): Boolean = {
+ require(isDist(dice1) && isDist(dice2) && isUniform(dice1))
+ val dist = sumMod(dice1, dice2)
+ isUniform(dist)
+ } holds
}
--
GitLab