Remove sampleSpace variables (#112)

By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).
dafny-lang · Nov 6, 2023 · b21286d · b21286d
1 parent 9568c0e
commit b21286d
Show file tree

Hide file tree

Showing 7 changed files with 50 additions and 75 deletions.
diff --git a/audit.log b/audit.log
@@ -8,8 +8,8 @@ src/Math/Exponential.dfy(11,17): EvalOne: Declaration has explicit `{:axiom}` at
 src/Math/Exponential.dfy(2,26): Exp: Declaration has explicit `{:axiom}` attribute. 
 src/Math/Exponential.dfy(4,17): FunctionalEquation: Declaration has explicit `{:axiom}` attribute. 
 src/Math/Exponential.dfy(7,17): Increasing: Declaration has explicit `{:axiom}` attribute. 
-src/Math/Measures.dfy(169,17): CountableSumOfZeroesIsZero: Declaration has explicit `{:axiom}` attribute. 
-src/Math/Measures.dfy(25,4): CountableSum: Definition has `assume {:axiom}` statement in body. 
+src/Math/Measures.dfy(157,17): CountableSumOfZeroesIsZero: Declaration has explicit `{:axiom}` attribute. 
+src/Math/Measures.dfy(37,4): CountableSum: Definition has `assume {:axiom}` statement in body. 
 src/ProbabilisticProgramming/Independence.dfy(28,27): IsIndep: Declaration has explicit `{:axiom}` attribute. 
 src/ProbabilisticProgramming/Independence.dfy(34,17): IsIndepImpliesMeasurableBool: Declaration has explicit `{:axiom}` attribute. 
 src/ProbabilisticProgramming/Independence.dfy(38,17): IsIndepImpliesMeasurableNat: Declaration has explicit `{:axiom}` attribute. 
@@ -21,7 +21,7 @@ src/ProbabilisticProgramming/Loops.dfy(311,17): EnsureWhileTerminates: Declarati
 src/ProbabilisticProgramming/Loops.dfy(317,17): UntilProbabilityFraction: Declaration has explicit `{:axiom}` attribute. 
 src/ProbabilisticProgramming/Loops.dfy(349,4): EnsureUntilTerminatesAndForAll: Definition has `assume {:axiom}` statement in body. 
 src/ProbabilisticProgramming/Loops.dfy(372,4): WhileIsIndep: Definition has `assume {:axiom}` statement in body. 
-src/ProbabilisticProgramming/RandomSource.dfy(52,17): ProbIsProbabilityMeasure: Declaration has explicit `{:axiom}` attribute. 
-src/ProbabilisticProgramming/RandomSource.dfy(56,17): CoinHasProbOneHalf: Declaration has explicit `{:axiom}` attribute. 
-src/ProbabilisticProgramming/RandomSource.dfy(63,17): MeasureHeadDrop: Declaration has explicit `{:axiom}` attribute. 
-src/ProbabilisticProgramming/RandomSource.dfy(69,17): TailIsMeasurePreserving: Declaration has explicit `{:axiom}` attribute. 
+src/ProbabilisticProgramming/RandomSource.dfy(50,17): ProbIsProbabilityMeasure: Declaration has explicit `{:axiom}` attribute. 
+src/ProbabilisticProgramming/RandomSource.dfy(54,17): CoinHasProbOneHalf: Declaration has explicit `{:axiom}` attribute. 
+src/ProbabilisticProgramming/RandomSource.dfy(61,17): MeasureHeadDrop: Declaration has explicit `{:axiom}` attribute. 
+src/ProbabilisticProgramming/RandomSource.dfy(67,17): TailIsMeasurePreserving: Declaration has explicit `{:axiom}` attribute. 
diff --git a/src/Distributions/Bernoulli/Correctness.dfy b/src/Distributions/Bernoulli/Correctness.dfy
@@ -59,7 +59,7 @@ module Bernoulli.Correctness {
 
       assert e in Rand.eventSpace && Rand.prob(e) == 0.0 by {
         Rand.ProbIsProbabilityMeasure();
-        assert Measures.IsSigmaAlgebra(Rand.eventSpace, Rand.sampleSpace);
+        assert Measures.IsSigmaAlgebra(Rand.eventSpace);
         assert Measures.IsPositive(Rand.eventSpace, Rand.prob);
       }
     } else {
@@ -96,7 +96,7 @@ module Bernoulli.Correctness {
       calc {
         Rand.prob(e);
         Rand.prob(e1 + e2);
-        { reveal A1; reveal A2; assert e1 * e2 == iset{}; Rand.ProbIsProbabilityMeasure(); Measures.PosCountAddImpliesAdd(Rand.eventSpace, Rand.sampleSpace, Rand.prob); assert Measures.IsAdditive(Rand.eventSpace, Rand.prob); }
+        { reveal A1; reveal A2; assert e1 * e2 == iset{}; Rand.ProbIsProbabilityMeasure(); Measures.PosCountAddImpliesAdd(Rand.eventSpace, Rand.prob); assert Measures.IsAdditive(Rand.eventSpace, Rand.prob); }
         Rand.prob(e1) + Rand.prob(e2);
         { reveal A1; reveal A2; }
         (1.0 / n as real) + ((m - 1) as real / n as real);
@@ -108,7 +108,7 @@ module Bernoulli.Correctness {
         Rand.ProbIsProbabilityMeasure();
         reveal A1;
         reveal A2;
-        Measures.BinaryUnion(Rand.eventSpace, Rand.sampleSpace, e1, e2);
+        Measures.BinaryUnion(Rand.eventSpace, e1, e2);
       }
     }
   }

diff --git a/src/Distributions/BernoulliExpNeg/Implementation.dfy b/src/Distributions/BernoulliExpNeg/Implementation.dfy
@@ -29,8 +29,11 @@ module BernoulliExpNeg.Implementation {
         invariant gamma'.numer >= 0
         invariant Model.GammaReductionLoop((true, gamma))(old(s)) == Model.GammaReductionLoop((b, gamma'))(s)
       {
+        var prevGamma := gamma';
+        var prevS := s;
         b := BernoulliExpNegSampleCaseLe1(Rationals.Int(1));
         gamma' := Rationals.Rational(gamma'.numer - gamma'.denom, gamma'.denom);
+        assert Model.GammaReductionLoop((true, prevGamma))(prevS) == Model.GammaReductionLoop((b, gamma'))(s);
       }
       if b {
         c:= BernoulliExpNegSampleCaseLe1(gamma');

diff --git a/src/Distributions/UniformPowerOfTwo/Correctness.dfy b/src/Distributions/UniformPowerOfTwo/Correctness.dfy
@@ -89,13 +89,13 @@ module UniformPowerOfTwo.Correctness {
       assert e in Rand.eventSpace by {
         assert e == e1 + e2;
         Rand.ProbIsProbabilityMeasure();
-        Measures.BinaryUnion(Rand.eventSpace, Rand.sampleSpace, e1, e2);
+        Measures.BinaryUnion(Rand.eventSpace, e1, e2);
       }
       calc {
         Rand.prob(e);
         { assert e == e1 + e2; }
         Rand.prob(e1 + e2);
-        { assert e1 * e2 == iset{}; Rand.ProbIsProbabilityMeasure(); Measures.PosCountAddImpliesAdd(Rand.eventSpace, Rand.sampleSpace, Rand.prob); assert Measures.IsAdditive(Rand.eventSpace, Rand.prob); }
+        { assert e1 * e2 == iset{}; Rand.ProbIsProbabilityMeasure(); Measures.PosCountAddImpliesAdd(Rand.eventSpace, Rand.prob); assert Measures.IsAdditive(Rand.eventSpace, Rand.prob); }
         Rand.prob(e1) + Rand.prob(e2);
         { UnifCorrectness2(n, m-1); UnifCorrectness2Inequality(n, m-1); }
         (1.0 / (Helper.Power(2, Helper.Log2Floor(n)) as real)) + (((m-1) as real) / (Helper.Power(2, Helper.Log2Floor(n)) as real));
@@ -119,7 +119,7 @@ module UniformPowerOfTwo.Correctness {
       if k == 0 {
         reveal Model.Sample();
         if m == 0 {
-          assert (iset s | Model.Sample(1)(s).value == m) == (iset s);
+          assert (iset s | Model.Sample(1)(s).value == m) == Measures.SampleSpace();
         } else {
           assert (iset s | Model.Sample(1)(s).value == m) == iset{};
         }

diff --git a/src/Math/Measures.dfy b/src/Math/Measures.dfy
@@ -10,13 +10,25 @@ module Measures {
 
   type Probability = x: real | 0.0 <= x <= 1.0
 
-  ghost predicate IsSigmaAlgebra<T(!new)>(eventSpace: iset<iset<T>>, sampleSpace: iset<T>) {
-    && (forall e | e in eventSpace :: e <= sampleSpace)
+  // States that given collection of sets is σ-algebra on the set of values of type `T`.
+  // In other words, the sample space is `SampleSpace<T>()`, i.e. the set of all values of type `T`,
+  // and `eventSpace` is the collection of measurable subsets.
+  ghost predicate IsSigmaAlgebra<T(!new)>(eventSpace: iset<iset<T>>) {
     && (iset{}) in eventSpace
-    && (forall e | e in eventSpace :: (sampleSpace - e) in eventSpace)
+    && (forall e | e in eventSpace :: Complement(e) in eventSpace)
     && (forall f: nat -> iset<T> | (forall n :: f(n) in eventSpace) :: (CountableUnion(f) in eventSpace))
   }
 
+  // The set of all values of type `T` that are not in the given set.
+  ghost function Complement<T(!new)>(event: iset<T>): iset<T> {
+    iset x: T | x !in event
+  }
+
+  // The set of all values of type `T`.
+  ghost function SampleSpace<T(!new)>(): iset<T> {
+    Complement(iset{})
+  }
+
   ghost function CountableUnion<T(!new)>(f: nat -> iset<T>, i: nat := 0): iset<T> {
     iset n: nat | n >= i, x <- f(n) :: x
   }
@@ -26,20 +38,13 @@ module Measures {
     f(i) + CountableSum(f, i+1)
   }
 
-  ghost function Powerset<A(!new)>(): iset<A> {
-    iset _: A
-  }
-
+  // The σ-algebra that contains all subsets.
   ghost function DiscreteSigmaAlgebra<A(!new)>(): iset<iset<A>> {
     iset _: iset<A>
   }
 
-  ghost const boolSampleSpace: iset<bool> := Powerset<bool>()
-
   ghost const boolEventSpace: iset<iset<bool>> := DiscreteSigmaAlgebra<bool>()
 
-  ghost const natSampleSpace: iset<nat> := Powerset<nat>()
-
   // The sigma algebra on the natural numbers is just the power set
   ghost const natEventSpace: iset<iset<nat>> := DiscreteSigmaAlgebra<nat>()
 
@@ -60,8 +65,8 @@ module Measures {
   }
 
   // Definition 6
-  ghost predicate IsMeasure<T(!new)>(eventSpace: iset<iset<T>>, sampleSpace: iset<T>, Prob: iset<T> -> real) {
-    && IsSigmaAlgebra(eventSpace, sampleSpace)
+  ghost predicate IsMeasure<T(!new)>(eventSpace: iset<iset<T>>, Prob: iset<T> -> real) {
+    && IsSigmaAlgebra(eventSpace)
     && IsPositive(eventSpace, Prob)
     && IsCountablyAdditive(eventSpace, Prob)
   }
@@ -82,9 +87,9 @@ module Measures {
   }
 
   // Definition 12
-  ghost predicate IsProbability<T(!new)>(eventSpace: iset<iset<T>>, sampleSpace: iset<T>, Prob: iset<T> -> real) {
-    && IsMeasure(eventSpace, sampleSpace, Prob)
-    && Prob(sampleSpace) == 1.0
+  ghost predicate IsProbability<T(!new)>(eventSpace: iset<iset<T>>, Prob: iset<T> -> real) {
+    && IsMeasure(eventSpace, Prob)
+    && Prob(SampleSpace()) == 1.0
   }
 
   // Definition 13
@@ -99,17 +104,11 @@ module Measures {
   *******/
 
   lemma boolsHaveSigmaAlgebra()
-    ensures IsSigmaAlgebra(boolEventSpace, boolSampleSpace)
-  {
-    forall e | e in boolEventSpace ensures e <= boolSampleSpace {
-      assert e <= boolSampleSpace by {
-        forall x: bool ensures x in e ==> x in boolSampleSpace {}
-      }
-    }
-  }
+    ensures IsSigmaAlgebra(boolEventSpace)
+  {}
 
   lemma natsHaveSigmaAlgebra()
-    ensures IsSigmaAlgebra(natEventSpace, natSampleSpace)
+    ensures IsSigmaAlgebra(natEventSpace)
   {}
 
   lemma PreImageIdentity<S(!new)>(f: S -> S, e: iset<S>)
@@ -122,20 +121,9 @@ module Measures {
     ensures PreImage(f, e) == PreImage(f', e')
   {}
 
-  lemma SampleSpaceInEventSpace<T>(sampleSpace: iset<T>, eventSpace: iset<iset<T>>)
-    requires IsSigmaAlgebra(eventSpace, sampleSpace)
-    ensures sampleSpace in eventSpace
-  {
-    var empty := iset{};
-    assert empty in eventSpace;
-    var compl := sampleSpace - empty;
-    assert compl == sampleSpace;
-    assert compl in eventSpace;
-  }
-
   // Equation (2.18)
-  lemma PosCountAddImpliesAdd<T(!new)>(eventSpace: iset<iset<T>>, sampleSpace: iset<T>, Prob: iset<T> -> real)
-    requires IsSigmaAlgebra(eventSpace, sampleSpace)
+  lemma PosCountAddImpliesAdd<T(!new)>(eventSpace: iset<iset<T>>, Prob: iset<T> -> real)
+    requires IsSigmaAlgebra(eventSpace)
     requires IsPositive(eventSpace, Prob)
     requires IsCountablyAdditive(eventSpace, Prob)
     ensures IsAdditive(eventSpace, Prob)
@@ -174,8 +162,8 @@ module Measures {
     ensures CountableUnion(f, i) == f(i) + CountableUnion(f, i + 1)
   {}
 
-  lemma BinaryUnion<T(!new)>(eventSpace: iset<iset<T>>, sampleSpace: iset<T>, e1: iset<T>, e2: iset<T>)
-    requires IsSigmaAlgebra(eventSpace, sampleSpace)
+  lemma BinaryUnion<T(!new)>(eventSpace: iset<iset<T>>, e1: iset<T>, e2: iset<T>)
+    requires IsSigmaAlgebra(eventSpace)
     requires e1 in eventSpace
     requires e2 in eventSpace
     ensures e1 + e2 in eventSpace

diff --git a/src/ProbabilisticProgramming/Monad.dfy b/src/ProbabilisticProgramming/Monad.dfy
@@ -59,10 +59,6 @@ module Monad {
     }
   }
 
-  ghost function ResultSampleSpace<A(!new)>(sampleSpace: iset<A>): iset<Result<A>> {
-    iset r: Result<A> | r.Diverging? || (r.value in sampleSpace && r.rest in Rand.sampleSpace)
-  }
-
   ghost function Values<A>(results: iset<Result<A>>): iset<A> {
     iset r <- results | r.Result? :: r.value
   }
@@ -75,12 +71,8 @@ module Monad {
     iset e: iset<Result<A>> | Values(e) in eventSpace && Rests(e) in Rand.eventSpace
   }
 
-  ghost const boolResultSampleSpace: iset<Result<bool>> := ResultSampleSpace(Measures.boolSampleSpace)
-
   ghost const boolResultEventSpace: iset<iset<Result<bool>>> := ResultEventSpace(Measures.boolEventSpace)
 
-  ghost const natResultSampleSpace: iset<Result<nat>> := ResultSampleSpace(Measures.natSampleSpace)
-
   ghost const natResultEventSpace: iset<iset<Result<nat>>> := ResultEventSpace(Measures.natEventSpace)
 
   ghost function ResultsWithValueIn<A(!new)>(values: iset<A>): iset<Result<A>> {
@@ -145,12 +137,9 @@ module Monad {
     ensures ResultsWithValueIn(event) in ResultEventSpace(eventSpace)
   {
     var results := ResultsWithValueIn(event);
-    assert Measures.IsSigmaAlgebra(Rand.eventSpace, Rand.sampleSpace) by {
+    assert Measures.IsSigmaAlgebra(Rand.eventSpace) by {
       Rand.ProbIsProbabilityMeasure();
     }
-    assert Rand.sampleSpace in Rand.eventSpace by {
-      Measures.SampleSpaceInEventSpace(Rand.sampleSpace, Rand.eventSpace);
-    }
     assert Values(results) == event by {
       forall v: A ensures v in event <==> v in Values(results) {
         var s: Rand.Bitstream :| true;
@@ -159,8 +148,8 @@ module Monad {
     }
     assert Rests(results) in Rand.eventSpace by {
       if v :| v in event {
-        assert Rests(results) == Rand.sampleSpace by {
-          forall s: Rand.Bitstream ensures s in Rests(results) <==> s in Rand.sampleSpace {
+        assert Rests(results) == Measures.SampleSpace() by {
+          forall s: Rand.Bitstream ensures s in Rests(results) <==> s in Measures.SampleSpace() {
             calc {
               s in Rests(results);
               Result(v, s) in results;
@@ -177,19 +166,16 @@ module Monad {
   lemma LiftRestInEventSpaceToResultEventSpace<A(!new)>(rests: iset<Rand.Bitstream>, eventSpace: iset<iset<A>>)
     requires rests in Rand.eventSpace
     requires iset{} in eventSpace
-    requires Measures.Powerset<A>() in eventSpace
+    requires Measures.SampleSpace() in eventSpace
     ensures ResultsWithRestIn(rests) in ResultEventSpace(eventSpace)
   {
     var results := ResultsWithRestIn(rests);
-    assert Measures.IsSigmaAlgebra(Rand.eventSpace, Rand.sampleSpace) by {
+    assert Measures.IsSigmaAlgebra(Rand.eventSpace) by {
       Rand.ProbIsProbabilityMeasure();
     }
-    assert Rand.sampleSpace in Rand.eventSpace by {
-      Measures.SampleSpaceInEventSpace(Rand.sampleSpace, Rand.eventSpace);
-    }
     assert Values(results) in eventSpace by {
       if rest :| rest in rests {
-        assert Values(results) == Measures.Powerset<A>() by {
+        assert Values(results) == Measures.SampleSpace() by {
           forall v: A ensures v in Values(results) {
             assert Result(v, rest) in results;
           }

diff --git a/src/ProbabilisticProgramming/RandomSource.dfy b/src/ProbabilisticProgramming/RandomSource.dfy
@@ -12,8 +12,6 @@ module Rand {
 
   type Bitstream = nat -> bool
 
-  ghost const sampleSpace: iset<Bitstream> := iset s: Bitstream
-
   ghost const eventSpace: iset<iset<Bitstream>>
 
   ghost const prob: iset<Bitstream> -> real
@@ -50,7 +48,7 @@ module Rand {
   *******/
 
   lemma {:axiom} ProbIsProbabilityMeasure()
-    ensures Measures.IsProbability(eventSpace, sampleSpace, prob)
+    ensures Measures.IsProbability(eventSpace, prob)
 
   // Equation (2.68) && (2.77)
   lemma {:axiom} CoinHasProbOneHalf(b: bool)