Prove independence of BernoulliExpNeg.SampleLe1 (#139)

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

Author: fzaiser

audit.log

@@ -1,16 +1,15 @@
 src/DafnyVMC.dfy(23,6): UniformPowerOfTwoSample: Definition has `assume {:axiom}` statement in body. 
 src/Distributions/Bernoulli/Correctness.dfy(59,17): BernoulliCorrectnessCaseFalse: Declaration has explicit `{:axiom}` attribute. 
 src/Distributions/BernoulliExpNeg/Correctness.dfy(228,6): CorrectnessLe1: Definition has `assume {:axiom}` statement in body. 
-src/Distributions/BernoulliExpNeg/Correctness.dfy(251,17): SampleLe1IsIndep: Declaration has explicit `{:axiom}` attribute. 
-src/Distributions/BernoulliExpNeg/Correctness.dfy(303,17): Le1SeriesConvergesToExpNeg: Declaration has explicit `{:axiom}` attribute. 
-src/Distributions/BernoulliExpNeg/Correctness.dfy(368,6): Le1LoopCutDecomposeProb: Definition has `assume {:axiom}` statement in body. 
-src/Distributions/BernoulliExpNeg/Correctness.dfy(369,6): Le1LoopCutDecomposeProb: Definition has `assume {:axiom}` statement in body. 
-src/Distributions/BernoulliExpNeg/Correctness.dfy(376,6): Le1LoopCutDecomposeProb: Definition has `assume {:axiom}` statement in body. 
-src/Distributions/BernoulliExpNeg/Correctness.dfy(377,6): Le1LoopCutDecomposeProb: Definition has `assume {:axiom}` statement in body. 
-src/Distributions/BernoulliExpNeg/Correctness.dfy(381,6): Le1LoopCutDecomposeProb: Definition has `assume {:axiom}` statement in body. 
-src/Distributions/BernoulliExpNeg/Correctness.dfy(382,6): Le1LoopCutDecomposeProb: Definition has `assume {:axiom}` statement in body. 
-src/Distributions/BernoulliExpNeg/Correctness.dfy(572,8): Le1LoopCorrectnessEq: Definition has `assume {:axiom}` statement in body. 
-src/Distributions/BernoulliExpNeg/Correctness.dfy(573,8): Le1LoopCorrectnessEq: Definition has `assume {:axiom}` statement in body. 
+src/Distributions/BernoulliExpNeg/Correctness.dfy(336,17): Le1SeriesConvergesToExpNeg: Declaration has explicit `{:axiom}` attribute. 
+src/Distributions/BernoulliExpNeg/Correctness.dfy(401,6): Le1LoopCutDecomposeProb: Definition has `assume {:axiom}` statement in body. 
+src/Distributions/BernoulliExpNeg/Correctness.dfy(402,6): Le1LoopCutDecomposeProb: Definition has `assume {:axiom}` statement in body. 
+src/Distributions/BernoulliExpNeg/Correctness.dfy(409,6): Le1LoopCutDecomposeProb: Definition has `assume {:axiom}` statement in body. 
+src/Distributions/BernoulliExpNeg/Correctness.dfy(410,6): Le1LoopCutDecomposeProb: Definition has `assume {:axiom}` statement in body. 
+src/Distributions/BernoulliExpNeg/Correctness.dfy(414,6): Le1LoopCutDecomposeProb: Definition has `assume {:axiom}` statement in body. 
+src/Distributions/BernoulliExpNeg/Correctness.dfy(415,6): Le1LoopCutDecomposeProb: Definition has `assume {:axiom}` statement in body. 
+src/Distributions/BernoulliExpNeg/Correctness.dfy(605,8): Le1LoopCorrectnessEq: Definition has `assume {:axiom}` statement in body. 
+src/Distributions/BernoulliExpNeg/Correctness.dfy(606,8): Le1LoopCorrectnessEq: Definition has `assume {:axiom}` statement in body. 
 src/Distributions/BernoulliExpNeg/Model.dfy(112,10): Le1LoopTerminatesAlmostSurely: Definition has `assume {:axiom}` statement in body. 
 src/Distributions/BernoulliExpNeg/Model.dfy(148,4): Le1LoopDivergenceProbabilityBound: Definition has `assume {:axiom}` statement in body. 
 src/Distributions/BernoulliExpNeg/Model.dfy(161,8): Le1LoopDivergenceProbabilityBound: Definition has `assume {:axiom}` statement in body. 

src/Distributions/BernoulliExpNeg/Correctness.dfy

@@ -248,10 +248,43 @@ module BernoulliExpNeg.Correctness {
     }
   }
 
-  lemma {:axiom} SampleLe1IsIndep(gamma: Rationals.Rational)
+  lemma SampleLe1IsIndep(gamma: Rationals.Rational)
     requires 0 <= gamma.numer <= gamma.denom
     ensures Independence.IsIndep(Model.SampleLe1(gamma))
+  {
+    Le1LoopIsIndep(gamma);
+    Independence.MapIsIndep(Model.Le1Loop(gamma)((true, 0)), (ak: (bool, nat)) => ak.1 % 2 == 1);
+  }
 
+  lemma Le1LoopIsIndep(gamma: Rationals.Rational)
+    requires 0 <= gamma.numer <= gamma.denom
+    ensures Independence.IsIndep(Model.Le1Loop(gamma)((true, 0)))
+  {
+    Model.Le1LoopTerminatesAlmostSurely(gamma);
+    forall ak: (bool, nat) ensures Independence.IsIndep(Model.Le1LoopIter(gamma)(ak)) {
+      Le1LoopIterIsIndep(gamma, ak);
+    }
+    Loops.WhileIsIndep(
+      Model.Le1LoopCondition,
+      Model.Le1LoopIter(gamma),
+      (true, 0)
+    );
+    assert Independence.IsIndep(Model.Le1Loop(gamma)((true, 0))) by {
+      reveal Model.Le1Loop();
+    }
+  }
+
+  lemma Le1LoopIterIsIndep(gamma: Rationals.Rational, ak: (bool, nat))
+    requires 0 <= gamma.numer <= gamma.denom
+    ensures Independence.IsIndep(Model.Le1LoopIter(gamma)(ak))
+  {
+    var k': nat := ak.1 + 1;
+    Bernoulli.Correctness.SampleIsIndep(gamma.numer, k' * gamma.denom);
+    Independence.MapIsIndep(
+      Bernoulli.Model.Sample(gamma.numer, k' * gamma.denom),
+      a => (a, k')
+    );
+  }
 
   // Proves the correctness of `Model.Le1LoopIter`.
   // Correctness means that when run on an initial value of `(true, k)` it produces