Remove Coin (#162)

Depends on #161 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). --------- Co-authored-by: John Tristan <[email protected]>
dafny-lang · Mar 6, 2024 · fdc7a86 · fdc7a86
1 parent 2697703
commit fdc7a86
Show file tree

Hide file tree

Showing 5 changed files with 0 additions and 63 deletions.
diff --git a/audit.log b/audit.log
@@ -1,5 +1,4 @@
 src/Distributions/Uniform/Correctness.dfy(31,17): UniformFullCorrectness: Declaration has explicit `{:axiom}` attribute. 
-src/Distributions/Uniform/Correctness.dfy(36,17): SampleCoin: 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. 

diff --git a/src/Distributions/Coin/Implementation.dfy b/src/Distributions/Coin/Implementation.dfy
diff --git a/src/Distributions/Coin/Interface.dfy b/src/Distributions/Coin/Interface.dfy
diff --git a/src/Distributions/Coin/Model.dfy b/src/Distributions/Coin/Model.dfy
diff --git a/src/Distributions/Uniform/Correctness.dfy b/src/Distributions/Uniform/Correctness.dfy
@@ -33,9 +33,6 @@ module Uniform.Correctness {
     ensures SampleEquals(n, i) in Rand.eventSpace
     ensures Rand.prob(SampleEquals(n, i)) == 1.0 / (n as real)
 
-  lemma {:axiom} SampleCoin(s: Rand.Bitstream)
-    ensures Model.Sample(2)(s)== Monad.Coin(s).Map(b => if b then 1 else 0)
-
   // Correctness theorem for Model.IntervalSample
   lemma UniformFullIntervalCorrectness(a: int, b: int, i: int)
     requires a <= i < b