Add subset type back

dafny-lang · Oct 13, 2023 · a7682c9 · a7682c9
1 parent 5efab50
commit a7682c9
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 1 deletion.
diff --git a/src/ProbabilisticProgramming/Monad.dfy b/src/ProbabilisticProgramming/Monad.dfy
@@ -15,6 +15,7 @@ module Monad {
 
   // Equation (2.38)
   function Tail(s: Random.Bitstream): (s': Random.Bitstream) {
+    TailIsBitstream(s);
     (n: nat) => s(n+1)
   }
 
@@ -130,6 +131,9 @@ module Monad {
     }
   }
 
+  lemma {:axiom} TailIsBitstream(s: Random.Bitstream)
+    ensures Random.IsBitstream((n: nat) => s(n+1))
+
   // Equation (2.68) && (2.77)
   lemma {:axiom} CoinHasProbOneHalf(b: bool)
     ensures

diff --git a/src/ProbabilisticProgramming/RandomSource.dfy b/src/ProbabilisticProgramming/RandomSource.dfy
@@ -10,7 +10,9 @@ module Random {
    Definitions
   ************/
 
-  type Bitstream = nat -> bool
+  type Bitstream = s: nat -> bool | IsBitstream(s) witness *
+
+  ghost predicate IsBitstream(stream: nat -> bool)
 
   ghost const sampleSpace: iset<Bitstream> := iset s: Bitstream