Remove almost all axioms (#163)

Depends on #161 and
#162

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).

audit.log

@@ -1,7 +1,2 @@
-src/Distributions/Uniform/Correctness.dfy(31,17): UniformFullCorrectness: Declaration has explicit `{:axiom}` attribute. 
-src/Distributions/Uniform/Model.dfy(19,33): Sample: Declaration has explicit `{:axiom}` attribute. 
-src/Distributions/Uniform/Model.dfy(46,17): IntervalSampleIsMeasurePreserving: Declaration has explicit `{:axiom}` attribute. 
-src/ProbabilisticProgramming/Independence.dfy(30,27): IsIndep: Declaration has explicit `{:axiom}` attribute. 
-src/ProbabilisticProgramming/Independence.dfy(70,17): IsIndepImpliesIsIndepFunction: Declaration has explicit `{:axiom}` attribute. 
-src/ProbabilisticProgramming/Independence.dfy(74,17): MapIsIndep: Declaration has explicit `{:axiom}` attribute. 
+src/Distributions/Uniform/Model.dfy(19,26): Sample: Declaration has explicit `{:axiom}` attribute. 
 src/ProbabilisticProgramming/RandomSource.dfy(50,17): ProbIsProbabilityMeasure: Declaration has explicit `{:axiom}` attribute. 

src/Distributions/Uniform/Correctness.dfy

@@ -16,6 +16,17 @@ module Uniform.Correctness {
    Definitions
   ************/
 
+  function IntervalSampleIsIndepFunctionHelper(a: int, x: int): nat
+    requires x-a >= 0
+  {
+    x-a
+  }
+
+  ghost function IntervalSampleIsIndepFunctionHelperLifted(a: int, A: iset<int>): iset<nat>
+  {
+    iset x: int | x in A && x-a >= 0 :: IntervalSampleIsIndepFunctionHelper(a, x)
+  }
+
   ghost function SampleEquals(n: nat, i: nat): iset<Rand.Bitstream>
     requires 0 <= i < n
   {
@@ -28,10 +39,13 @@ module Uniform.Correctness {
 
   // Correctness theorem for Model.Sample
   // Equation (4.12) / PROB_BERN_UNIFORM
-  lemma {:axiom} UniformFullCorrectness(n: nat, i: nat)
+  lemma UniformFullCorrectness(n: nat, i: nat)
     requires 0 <= i < n
-    ensures SampleEquals(n, i) in Rand.eventSpace
-    ensures Rand.prob(SampleEquals(n, i)) == 1.0 / (n as real)
+    ensures
+      var e := iset s | Model.Sample(n)(s).Equals(i);
+      e in Rand.eventSpace &&
+      Rand.prob(e) == 1.0 / (n as real)
+  {}
 
   // Correctness theorem for Model.IntervalSample
   lemma UniformFullIntervalCorrectness(a: int, b: int, i: int)
@@ -55,17 +69,96 @@ module Uniform.Correctness {
     }
   }
 
-  // Equation (4.10)
-  lemma SampleIsIndep(n: nat)
+  lemma SampleIsIndepFunction(n: nat)
+    requires n > 0
+    ensures Independence.IsIndepFunction(Model.Sample(n))
+  {}
+
+  lemma IntervalSampleIsIndepFunction(a: int, b: int)
+    requires a < b
+    ensures Independence.IsIndepFunction(Model.IntervalSample(a, b))
+  {
+    forall A: iset<int>, E: iset<Rand.Bitstream> | E in Rand.eventSpace ensures Independence.IsIndepFunctionCondition(Model.IntervalSample(a, b), A, E) {
+      var A': iset<nat> := IntervalSampleIsIndepFunctionHelperLifted(a, A);
+      assert Measures.AreIndepEvents(Rand.eventSpace, Rand.prob, Monad.BitstreamsWithValueIn(Model.IntervalSample(a, b), A), Monad.BitstreamsWithRestIn(Model.IntervalSample(a, b), E)) by {
+        assert Monad.BitstreamsWithValueIn(Model.IntervalSample(a, b), A) == Monad.BitstreamsWithValueIn(Model.Sample(b - a), A') by {
+          forall s ensures s in Monad.BitstreamsWithValueIn(Model.IntervalSample(a, b), A) <==> s in Monad.BitstreamsWithValueIn(Model.Sample(b - a), A') {
+            calc {
+              s in Monad.BitstreamsWithValueIn(Model.IntervalSample(a, b), A);
+              Monad.Map(Model.Sample(b - a), x => a + x)(s).value in A;
+              Monad.Bind(Model.Sample(b - a), x => Monad.Return(a+x))(s).value in A;
+              Model.Sample(b - a)(s).value + a in A;
+              Model.Sample(b - a)(s).value in A';
+              s in Monad.BitstreamsWithValueIn(Model.Sample(b - a), A');
+            }
+          }
+        }
+        assert Monad.BitstreamsWithRestIn(Model.IntervalSample(a, b), E) == Monad.BitstreamsWithRestIn(Model.Sample(b-a), E) by {
+          forall s ensures s in Monad.BitstreamsWithRestIn(Model.IntervalSample(a, b), E) <==> s in Monad.BitstreamsWithRestIn(Model.Sample(b-a), E) {
+            calc {
+              s in Monad.BitstreamsWithRestIn(Model.IntervalSample(a, b), E);
+              Monad.Map(Model.Sample(b - a), x => a + x)(s).rest in E;
+              Monad.Bind(Model.Sample(b - a), x => Monad.Return(a+x))(s).rest in E;
+              Model.Sample(b-a)(s).rest in E;
+              s in Monad.BitstreamsWithRestIn(Model.Sample(b-a), E);
+            }
+          }
+        }
+        assert Independence.IsIndepFunctionCondition(Model.Sample(b - a), A', E) by {
+          SampleIsIndepFunction(b-a);
+        }
+      }
+    }
+  }
+
+  lemma SampleBound(n: nat, s: Rand.Bitstream)
     requires n > 0
-    ensures Independence.IsIndep(Model.Sample(n))
+    ensures 0 <= Model.Sample(n)(s).value < n
   {}
 
-  lemma IntervalSampleIsIndep(a: int, b: int)
+  lemma IntervalSampleBound(a: int, b: int, s: Rand.Bitstream)
     requires a < b
-    ensures Independence.IsIndep(Model.IntervalSample(a, b))
+    ensures a <= Model.IntervalSample(a, b)(s).value < b
   {
-    SampleIsIndep(b-a);
-    Independence.MapIsIndep(Model.Sample(b-a), x => a + x);
+    SampleBound(b-a, s);
+  }
+
+  lemma SampleIsMeasurePreserving(n: nat)
+    requires n > 0
+    ensures forall n | n > 0 :: Measures.IsMeasurePreserving(Rand.eventSpace, Rand.prob, Rand.eventSpace, Rand.prob, s => Model.Sample(n)(s).rest)
+  {}
+
+  lemma IntervalSampleIsMeasurePreserving(a: int, b: int)
+    requires a < b
+    ensures Measures.IsMeasurePreserving(Rand.eventSpace, Rand.prob, Rand.eventSpace, Rand.prob, s => Model.IntervalSample(a, b)(s).rest)
+  {
+    var f := s => Model.IntervalSample(a, b)(s).rest;
+    var f' := s => Model.Sample(b-a)(s).rest;
+
+    forall e: iset<Rand.Bitstream> | e in Rand.eventSpace ensures Measures.PreImage(f, e) == Measures.PreImage(f', e) {
+      forall s ensures s in Measures.PreImage(f, e) <==> s in Measures.PreImage(f', e) {
+        calc {
+          s in Measures.PreImage(f, e);
+          f(s) in e;
+          Model.IntervalSample(a, b)(s).rest in e;
+          Model.Sample(b-a)(s).rest in e;
+          f'(s) in e;
+          s in Measures.PreImage(f', e);
+        }
+      }
+    }
+
+    assert Measures.IsMeasurable(Rand.eventSpace, Rand.eventSpace, f) by {
+      forall e: iset<Rand.Bitstream> | e in Rand.eventSpace ensures Measures.PreImage(f, e) in Rand.eventSpace {
+        assert Measures.PreImage(f, e) == Measures.PreImage(f', e);
+        SampleIsMeasurePreserving(b-a);
+      }
+    }
+
+    forall e | e in Rand.eventSpace ensures Rand.prob(Measures.PreImage(f, e)) == Rand.prob(e) {
+      assert Measures.PreImage(f, e) == Measures.PreImage(f', e);
+      SampleIsMeasurePreserving(b-a);
+    }
+
   }
 }

src/Distributions/Uniform/Model.dfy

@@ -16,35 +16,20 @@ module Uniform.Model {
   ************/
 
   // Definition 49
-  opaque ghost function {:axiom} Sample(n: nat): (h: Monad.Hurd<nat>)
+  ghost function {:axiom} Sample(n: nat): (h: Monad.Hurd<nat>)
     requires n > 0
-    ensures Independence.IsIndep(h)
+    ensures Independence.IsIndepFunction(h)
+    ensures Measures.IsMeasurePreserving(Rand.eventSpace, Rand.prob, Rand.eventSpace, Rand.prob, s => h(s).rest)
     ensures forall s :: 0 <= h(s).value < n
+    ensures forall i | 0 <= i < n ::
+              var e := iset s | h(s).Equals(i);
+              && e in Rand.eventSpace
+              && Rand.prob(e) == 1.0 / (n as real)
 
   ghost function IntervalSample(a: int, b: int): (f: Monad.Hurd<int>)
     requires a < b
   {
     Monad.Map(Sample(b - a), x => a + x)
   }
 
-  /*******
-   Lemmas
-  *******/
-
-  lemma SampleBound(n: nat, s: Rand.Bitstream)
-    requires n > 0
-    ensures 0 <= Sample(n)(s).value < n
-  {}
-
-  lemma IntervalSampleBound(a: int, b: int, s: Rand.Bitstream)
-    requires a < b
-    ensures a <= IntervalSample(a, b)(s).value < b
-  {
-    SampleBound(b-a, s);
-  }
-
-  lemma {:axiom} IntervalSampleIsMeasurePreserving(a: int, b: int)
-    requires a < b
-    ensures Measures.IsMeasurePreserving(Rand.eventSpace, Rand.prob, Rand.eventSpace, Rand.prob, s => IntervalSample(a, b)(s).rest)
-
 }

src/Math/RealArith.dfy

@@ -178,4 +178,10 @@ module RealArith {
   lemma AsRealOfMultiplication(a: nat, b: nat)
     ensures (a as real) * (b as real) == (a * b) as real
   {}
+
+  lemma MultiplicationInvariance(a: real, b1: real, b2: real)
+    requires b1 == b2
+    ensures a * b1 == a * b2
+    ensures b1 * a == b2 * a
+  {}
 }

src/ProbabilisticProgramming/Independence.dfy

@@ -26,9 +26,6 @@ module Independence {
     forall A: iset<A>, E: iset<Rand.Bitstream> | E in Rand.eventSpace :: IsIndepFunctionCondition(f, A, E)
   }
 
-  // Definition 35: (strong) independence
-  ghost predicate {:axiom} IsIndep<A(!new)>(f: Monad.Hurd<A>)
-
   /*******
    Lemmas
   *******/
@@ -66,15 +63,6 @@ module Independence {
     }
   }
 
-  // Equation (3.14)
-  lemma {:axiom} IsIndepImpliesIsIndepFunction<A(!new)>(f: Monad.Hurd<A>)
-    requires IsIndep(f)
-    ensures IsIndepFunction(f)
-
-  lemma {:axiom} MapIsIndep<A, B(!new)>(f: Monad.Hurd<A>, g: A -> B)
-    requires IsIndep(f)
-    ensures IsIndep(Monad.Map(f, g))
-
   lemma AreIndepEventsConjunctElimination(e1: iset<Rand.Bitstream>, e2: iset<Rand.Bitstream>)
     requires Measures.AreIndepEvents(Rand.eventSpace, Rand.prob, e1, e2)
     ensures Rand.prob(e1 * e2) == Rand.prob(e1) * Rand.prob(e2)