conditional probabilities

testcases/proof/proba/Coins.scala

@@ -38,6 +38,55 @@ object Coins {
   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))
@@ -55,6 +104,15 @@ 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)