diff --git a/audit.log b/audit.log index 373a2aa0..48ac1963 100644 --- a/audit.log +++ b/audit.log @@ -1,23 +1,9 @@ src/DafnyVMC.dfy(28,6): UniformPowerOfTwoSample: Definition has `assume {:axiom}` statement in body. -src/Distributions/Uniform/Correctness.dfy(34,17): UniformFullCorrectness: Declaration has explicit `{:axiom}` attribute. -src/Distributions/Uniform/Model.dfy(21,33): Sample: Declaration has explicit `{:axiom}` attribute. -src/Math/Analysis/Limits.dfy(126,17): Sandwich: Declaration has explicit `{:axiom}` attribute. -src/Math/Analysis/Reals.dfy(35,17): LeastUpperBoundProperty: Declaration has explicit `{:axiom}` attribute. -src/Math/Measures.dfy(125,17): ProbabilityLe1: Declaration has explicit `{:axiom}` attribute. -src/Math/Measures.dfy(130,17): IsMonotonic: Declaration has explicit `{:axiom}` attribute. -src/ProbabilisticProgramming/Independence.dfy(105,17): BindIsIndep: Declaration has explicit `{:axiom}` attribute. +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/UniformPowerOfTwo/Model.dfy(19,20): Sample: Declaration has explicit `{:axiom}` attribute. src/ProbabilisticProgramming/Independence.dfy(30,27): IsIndep: Declaration has explicit `{:axiom}` attribute. src/ProbabilisticProgramming/Independence.dfy(55,6): ResultsIndependent: Definition has `assume {:axiom}` statement in body. -src/ProbabilisticProgramming/Independence.dfy(59,17): IsIndepImpliesMeasurableBool: Declaration has explicit `{:axiom}` attribute. -src/ProbabilisticProgramming/Independence.dfy(77,17): IsIndepImpliesMeasurableNat: Declaration has explicit `{:axiom}` attribute. -src/ProbabilisticProgramming/Independence.dfy(82,17): IsIndepImpliesIsIndepFunction: Declaration has explicit `{:axiom}` attribute. -src/ProbabilisticProgramming/Independence.dfy(87,17): CoinIsIndep: Declaration has explicit `{:axiom}` attribute. -src/ProbabilisticProgramming/Independence.dfy(91,17): ReturnIsIndep: Declaration has explicit `{:axiom}` attribute. -src/ProbabilisticProgramming/Loops.dfy(361,17): EnsureWhileTerminates: Declaration has explicit `{:axiom}` attribute. -src/ProbabilisticProgramming/Loops.dfy(371,17): UntilProbabilityFraction: Declaration has explicit `{:axiom}` attribute. -src/ProbabilisticProgramming/Loops.dfy(404,4): EnsureUntilTerminatesAndForAll: Definition has `assume {:axiom}` statement in body. -src/ProbabilisticProgramming/Loops.dfy(427,4): WhileIsIndep: Definition has `assume {:axiom}` statement in body. +src/ProbabilisticProgramming/Independence.dfy(60,17): IsIndepImpliesIsIndepFunction: Declaration has explicit `{:axiom}` attribute. +src/ProbabilisticProgramming/Independence.dfy(64,17): MapIsIndep: 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/DafnyVMC.dfy b/src/DafnyVMC.dfy index 7c076e86..0dc45366 100644 --- a/src/DafnyVMC.dfy +++ b/src/DafnyVMC.dfy @@ -21,7 +21,7 @@ module {:extern "DafnyVMCPart"} DafnyVMC { method UniformPowerOfTwoSample(n: nat) returns (u: nat) requires n >= 1 - modifies this + modifies `s ensures UniformPowerOfTwo.Model.Sample(n)(old(s)) == Monad.Result(u, s) { u := DafnyVMCPartMaterial.Random.ExternUniformPowerOfTwoSample(n); diff --git a/src/DafnyVMCTrait.dfy b/src/DafnyVMCTrait.dfy index ad0ec7a3..e9b560f5 100644 --- a/src/DafnyVMCTrait.dfy +++ b/src/DafnyVMCTrait.dfy @@ -7,7 +7,7 @@ module DafnyVMCTrait { import opened Pos - trait {:termination false} RandomTrait extends UniformPowerOfTwo.Implementation.Trait, FisherYates.Implementation.Trait { + trait {:termination false} RandomTrait extends UniformPowerOfTwo.Interface.Trait, FisherYates.Implementation.Trait { method {:verify false} UniformSample (n: pos) returns (o: nat) diff --git a/src/Distributions/Bitstream/Interface.dfy b/src/Distributions/Bitstream/Interface.dfy new file mode 100644 index 00000000..5ebc77bb --- /dev/null +++ b/src/Distributions/Bitstream/Interface.dfy @@ -0,0 +1,12 @@ +/******************************************************************************* + * Copyright by the contributors to the Dafny Project + * SPDX-License-Identifier: MIT + *******************************************************************************/ + +module Bitstream.Interface { + import Rand + + trait {:termination false} Trait { + ghost var s: Rand.Bitstream + } +} diff --git a/src/Distributions/Coin/Implementation.dfy b/src/Distributions/Coin/Implementation.dfy index 3bec2089..6a4f6072 100644 --- a/src/Distributions/Coin/Implementation.dfy +++ b/src/Distributions/Coin/Implementation.dfy @@ -17,9 +17,8 @@ module Coin.Implementation { { var x := UniformPowerOfTwoSample(2); b := if x == 1 then true else false; - reveal UniformPowerOfTwo.Model.Sample(); } } -} +} \ No newline at end of file diff --git a/src/Distributions/Coin/Interface.dfy b/src/Distributions/Coin/Interface.dfy index c506c519..ae0b7847 100644 --- a/src/Distributions/Coin/Interface.dfy +++ b/src/Distributions/Coin/Interface.dfy @@ -16,4 +16,4 @@ module Coin.Interface { ensures Model.Sample(old(s)) == Monad.Result(b, s) } -} +} \ No newline at end of file diff --git a/src/Distributions/Uniform/Correctness.dfy b/src/Distributions/Uniform/Correctness.dfy index 43d11af8..ca2dc0c7 100644 --- a/src/Distributions/Uniform/Correctness.dfy +++ b/src/Distributions/Uniform/Correctness.dfy @@ -9,10 +9,7 @@ module Uniform.Correctness { import Monad import Independence import Rand - import Quantifier - import Loops import Measures - import UniformPowerOfTwo import Model /************ diff --git a/src/Distributions/Uniform/Interface.dfy b/src/Distributions/Uniform/Interface.dfy index af2306a0..2cb1d4d4 100644 --- a/src/Distributions/Uniform/Interface.dfy +++ b/src/Distributions/Uniform/Interface.dfy @@ -5,12 +5,11 @@ module Uniform.Interface { import Monad - import Coin import Model - import UniformPowerOfTwo import Pos + import Bitstream - trait {:termination false} Trait extends UniformPowerOfTwo.Interface.Trait { + trait {:termination false} Trait extends Bitstream.Interface.Trait { method UniformSample(n: Pos.pos) returns (u: nat) modifies `s diff --git a/src/Distributions/Uniform/Model.dfy b/src/Distributions/Uniform/Model.dfy index 6cf5d5c1..0548490d 100644 --- a/src/Distributions/Uniform/Model.dfy +++ b/src/Distributions/Uniform/Model.dfy @@ -7,10 +7,8 @@ module Uniform.Model { import Measures import NatArith import Rand - import Quantifier import Monad import Independence - import Loops import UniformPowerOfTwo /************ diff --git a/src/Distributions/UniformPowerOfTwo/Correctness.dfy b/src/Distributions/UniformPowerOfTwo/Correctness.dfy deleted file mode 100644 index 6b15d7cd..00000000 --- a/src/Distributions/UniformPowerOfTwo/Correctness.dfy +++ /dev/null @@ -1,414 +0,0 @@ -/******************************************************************************* - * Copyright by the contributors to the Dafny Project - * SPDX-License-Identifier: MIT - *******************************************************************************/ - -module UniformPowerOfTwo.Correctness { - import Helper - import NatArith - import RealArith - import Monad - import Independence - import Rand - import Quantifier - import Loops - import Measures - import Model - - /************ - Definitions - ************/ - - ghost predicate UnifIsCorrect(n: nat, k: nat, m: nat) - requires NatArith.Power(2, k) <= n < NatArith.Power(2, k + 1) - { - Rand.prob(iset s | Model.Sample(n)(s).value == m) == if m < NatArith.Power(2, k) then 1.0 / (NatArith.Power(2, k) as real) else 0.0 - } - - function SampleRest(n: nat): Rand.Bitstream -> Rand.Bitstream - requires n >= 1 - { - (s: Rand.Bitstream) => Model.Sample(n)(s).rest - } - - /******* - Lemmas - *******/ - - // Correctness Theorem for Model.Sample. - // In contrast to UnifCorrectness, this lemma does not follow - // the thesis, but models PROB_BERN_UNIF of the HOL implementation. - lemma UnifCorrectness2(n: nat, m: nat) - requires n >= 1 - ensures - var e := iset s | Model.Sample(n)(s).value == m; - && e in Rand.eventSpace - && Rand.prob(e) == if m < NatArith.Power(2, NatArith.Log2Floor(n)) then 1.0 / (NatArith.Power(2, NatArith.Log2Floor(n)) as real) else 0.0 - { - var e := iset s | Model.Sample(n)(s).value == m; - var k := NatArith.Log2Floor(n); - - assert e in Rand.eventSpace by { - var resultsWithValueM := Monad.ResultsWithValueIn(iset{m}); - assert resultsWithValueM in Monad.natResultEventSpace by { - Monad.LiftInEventSpaceToResultEventSpace(iset{m}, Measures.natEventSpace); - } - var preimage := Measures.PreImage(Model.Sample(n), resultsWithValueM); - assert Measures.IsMeasurable(Rand.eventSpace, Monad.natResultEventSpace, Model.Sample(n)) by { - SampleIsIndep(n); - Independence.IsIndepImpliesMeasurableNat(Model.Sample(n)); - } - assert e == preimage; - } - NatArith.Power2OfLog2Floor(n); - UnifCorrectness(n, k); - assert UnifIsCorrect(n, k, m); - } - - // See PROB_BERN_UNIF_LT in HOL implementation. - lemma UnifCorrectness2Inequality(n: nat, m: nat) - requires n >= 1 - requires m <= NatArith.Power(2, NatArith.Log2Floor(n)) - ensures - var e := iset s | Model.Sample(n)(s).value < m; - && e in Rand.eventSpace - && Rand.prob(e) == (m as real) / (NatArith.Power(2, NatArith.Log2Floor(n)) as real) - { - var e := iset s | Model.Sample(n)(s).value < m; - - if m == 0 { - assert e == iset{}; - Rand.ProbIsProbabilityMeasure(); - } else { - var e1 := iset s | Model.Sample(n)(s).value < m-1; - var e2 := iset s | Model.Sample(n)(s).value == m-1; - assert e1 in Rand.eventSpace by { - UnifCorrectness2Inequality(n, m-1); - } - assert e2 in Rand.eventSpace by { - UnifCorrectness2(n, m-1); - } - assert e in Rand.eventSpace by { - assert e == e1 + e2; - Rand.ProbIsProbabilityMeasure(); - Measures.BinaryUnionIsMeasurable(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.prob); assert Measures.IsAdditive(Rand.eventSpace, Rand.prob); } - Rand.prob(e1) + Rand.prob(e2); - { UnifCorrectness2(n, m-1); UnifCorrectness2Inequality(n, m-1); } - (1.0 / (NatArith.Power(2, NatArith.Log2Floor(n)) as real)) + (((m-1) as real) / (NatArith.Power(2, NatArith.Log2Floor(n)) as real)); - { RealArith.AdditionOfFractions(1.0, (m-1) as real, NatArith.Power(2, NatArith.Log2Floor(n)) as real); } - (1.0 + (m-1) as real) / (NatArith.Power(2, NatArith.Log2Floor(n)) as real); - { assert 1.0 + (m-1) as real == (m as real); } - (m as real) / (NatArith.Power(2, NatArith.Log2Floor(n)) as real); - } - } - } - - // Correctness Theorem for Model.Sample. - // In contrast to UnifCorrectness2, this lemma follows equation (4.8) - // instead of the HOL implementation. - lemma UnifCorrectness(n: nat, k: nat) - requires NatArith.Power(2, k) <= n < NatArith.Power(2, k + 1) - ensures forall m: nat :: UnifIsCorrect(n, k, m) - { - forall m: nat ensures UnifIsCorrect(n, k, m) { - assert n >= 1 by { NatArith.PowerGreater0(2, k); } - if k == 0 { - reveal Model.Sample(); - if m == 0 { - assert (iset s | Model.Sample(1)(s).value == m) == Measures.SampleSpace(); - } else { - assert (iset s | Model.Sample(1)(s).value == m) == iset{}; - } - Rand.ProbIsProbabilityMeasure(); - assert UnifIsCorrect(n, k, m); - } else { - var u := m / 2; - assert RecursiveCorrect: UnifIsCorrect(n / 2, k - 1, m / 2) by { - UnifCorrectness(n / 2, k - 1); - } - if m < NatArith.Power(2, k) { - calc { - Rand.prob(iset s | Model.Sample(n)(s).value == m); - == { SampleRecursiveHalf(n, m); } - Rand.prob(iset s | Model.Sample(n / 2)(s).value == u) / 2.0; - == { reveal RecursiveCorrect; } - (1.0 / NatArith.Power(2, k - 1) as real) / 2.0; - == { RealArith.PowerOfTwoLemma(k - 1); } - 1.0 / (NatArith.Power(2, k) as real); - } - assert UnifIsCorrect(n, k, m); - } else { - calc { - Rand.prob(iset s | Model.Sample(n)(s).value == m); - == { SampleRecursiveHalf(n, m); } - Rand.prob(iset s | Model.Sample(n / 2)(s).value == u) / 2.0; - == { reveal RecursiveCorrect; } - 0.0 / 2.0; - == - 0.0; - } - assert UnifIsCorrect(n, k, m); - } - } - } - } - - // Equation (4.7) - lemma SampleIsIndep(n: nat) - requires n >= 1 - decreases n - ensures Independence.IsIndep(Model.Sample(n)) - { - var fn := Model.Sample(n); - reveal Model.Sample(); - if n == 1 { - Independence.ReturnIsIndep(0 as nat); - } else { - assert Independence.IsIndep(Model.Sample(n / 2)) by { - SampleIsIndep(n / 2); - } - forall m: nat ensures Independence.IsIndep(Model.UnifStep(m)) { - Independence.CoinIsIndep(); - var g := Model.UnifStepHelper(m); - forall b: bool ensures Independence.IsIndep(g(b)) { - Independence.ReturnIsIndep((if b then 2 * m + 1 else 2 * m) as nat); - } - Independence.BindIsIndep(Monad.Coin, g); - } - Independence.BindIsIndep(Model.Sample(n / 2), Model.UnifStep); - } - } - - // This lemma shouldn't be necessary. - // It should be a consequence of (strong?) independence of `Sample(n)` and the fact that it terminates almost surely. - lemma SampleIsMeasurePreserving(n: nat) - requires n >= 1 - ensures Measures.IsMeasurePreserving(Rand.eventSpace, Rand.prob, Rand.eventSpace, Rand.prob, SampleRest(n)) - { - var f := SampleRest(n); - assert Measures.IsMeasurable(Rand.eventSpace, Rand.eventSpace, f) by { - forall e | e in Rand.eventSpace ensures Measures.PreImage(f, e) in Rand.eventSpace { - var resultsWithRestInE := Monad.ResultsWithRestIn(e); - assert resultsWithRestInE in Monad.natResultEventSpace by { - Monad.LiftRestInEventSpaceToResultEventSpace(e, Measures.natEventSpace); - } - var preimage' := Measures.PreImage(Model.Sample(n), resultsWithRestInE); - assert preimage' in Rand.eventSpace by { - SampleIsIndep(n); - Independence.IsIndepImpliesMeasurableNat(Model.Sample(n)); - } - assert Measures.PreImage(f, e) == preimage'; - } - } - if n == 1 { - forall e | e in Rand.eventSpace ensures Rand.prob(Measures.PreImage(f, e)) == Rand.prob(e) { - forall s: Rand.Bitstream ensures f(s) == s { - reveal Model.Sample(); - assert f(s) == s; - } - Measures.PreImageIdentity(f, e); - } - assert Measures.IsMeasurePreserving(Rand.eventSpace, Rand.prob, Rand.eventSpace, Rand.prob, f); - } else { - var g := SampleRest(n / 2); - forall e | e in Rand.eventSpace ensures Rand.prob(Measures.PreImage(f, e)) == Rand.prob(e) { - var e' := (iset s | Rand.Tail(s) in e); - assert e' in Rand.eventSpace by { - assert e' == Measures.PreImage(Rand.Tail, e); - Rand.TailIsMeasurePreserving(); - assert Measures.IsMeasurable(Rand.eventSpace, Rand.eventSpace, Rand.Tail); - } - assert Measures.PreImage(f, e) == Measures.PreImage(g, e') by { - assert forall s :: f(s) in e <==> g(s) in e' by { - forall s ensures f(s) in e <==> g(s) in e' { - calc { - f(s) in e; - <==> { assert f(s) == Model.Sample(n)(s).rest; } - Model.Sample(n)(s).rest in e; - <==> { SampleTailDecompose(n, s); } - Rand.Tail(Model.Sample(n / 2)(s).rest) in e; - <==> - Model.Sample(n / 2)(s).rest in e'; - <==> { assert Model.Sample(n / 2)(s).rest == g(s); } - g(s) in e'; - } - } - } - Measures.PreImagesEqual(f, e, g, e'); - } - assert Rand.prob(Measures.PreImage(f, e)) == Rand.prob(e) by { - calc { - Rand.prob(Measures.PreImage(f, e)); - == - Rand.prob(Measures.PreImage(g, e')); - == { SampleIsMeasurePreserving(n / 2); assert Measures.IsMeasurePreserving(Rand.eventSpace, Rand.prob, Rand.eventSpace, Rand.prob, g); assert e' in Rand.eventSpace; } - Rand.prob(e'); - == { assert e' == Measures.PreImage(Rand.Tail, e); } - Rand.prob(Measures.PreImage(Rand.Tail, e)); - == { Rand.TailIsMeasurePreserving(); } - Rand.prob(e); - } - } - } - assert Measures.IsMeasurePreserving(Rand.eventSpace, Rand.prob, Rand.eventSpace, Rand.prob, f); - } - } - - lemma SampleTailDecompose(n: nat, s: Rand.Bitstream) - requires n >= 2 - ensures Model.Sample(n)(s).rest == Rand.Tail(Model.Sample(n / 2)(s).rest) - { - var Result(a, s') := Model.Sample(n / 2)(s); - var Result(b, s'') := Monad.Coin(s'); - calc { - Model.Sample(n)(s).rest; - == { reveal Model.Sample(); } - Monad.Bind(Model.Sample(n / 2), Model.UnifStep)(s).rest; - == - Model.UnifStep(a)(s').rest; - == - Monad.Bind(Monad.Coin, (b: bool) => Monad.Return((if b then 2*a + 1 else 2*a) as nat))(s').rest; - == - Monad.Return((if b then 2*a + 1 else 2*a) as nat)(s'').rest; - == - s''; - == - Rand.Tail(s'); - == - Rand.Tail(Model.Sample(n / 2)(s).rest); - } - } - - lemma SampleSetEquality(n: nat, m: nat) - requires n >= 2 - ensures - var bOf := (s: Rand.Bitstream) => Monad.Coin(Model.Sample(n / 2)(s).rest).value; - var aOf := (s: Rand.Bitstream) => Model.Sample(n / 2)(s).value; - (iset s | Model.Sample(n)(s).value == m) == (iset s | 2*aOf(s) + NatArith.boolToNat(bOf(s)) == m) - { - var bOf := (s: Rand.Bitstream) => Monad.Coin(Model.Sample(n / 2)(s).rest).value; - var aOf := (s: Rand.Bitstream) => Model.Sample(n / 2)(s).value; - forall s ensures Model.Sample(n)(s).value == m <==> (2 * aOf(s) + NatArith.boolToNat(bOf(s)) == m) { - var Result(a, s') := Model.Sample(n / 2)(s); - var Result(b, s'') := Monad.Coin(s'); - calc { - Model.Sample(n)(s).value; - == { reveal Model.Sample(); } - Monad.Bind(Model.Sample(n / 2), Model.UnifStep)(s).value; - == - Model.UnifStep(a)(s').value; - == - Monad.Bind(Monad.Coin, b => Monad.Return((if b then 2*a + 1 else 2*a) as nat))(s').value; - == - Monad.Return((if b then 2*a + 1 else 2*a) as nat)(s'').value; - == - if b then 2*a + 1 else 2*a; - } - } - } - - lemma SampleRecursiveHalf(n: nat, m: nat) - requires n >= 2 - ensures Rand.prob(iset s | Model.Sample(n)(s).value == m) == Rand.prob(iset s | Model.Sample(n / 2)(s).value == m / 2) / 2.0 - { - var aOf: Rand.Bitstream -> nat := (s: Rand.Bitstream) => Model.Sample(n / 2)(s).value; - var bOf: Rand.Bitstream -> bool := (s: Rand.Bitstream) => Monad.Coin(Model.Sample(n / 2)(s).rest).value; - var A: iset := (iset x: nat | x == m / 2); - var E: iset := (iset s | m % 2 as nat == NatArith.boolToNat(Monad.Coin(s).value)); - var f := (s: Rand.Bitstream) => Model.Sample(n / 2)(s).rest; - - var e1 := (iset s | Model.Sample(n / 2)(s).RestIn(E)); - var e2 := (iset s | Model.Sample(n / 2)(s).In(A)); - var e3 := (iset s | 2*aOf(s) + NatArith.boolToNat(bOf(s)) == m); - - assert SplitEvent: e3 == e1 * e2 by { - forall s ensures s in e3 <==> s in e1 && s in e2 { - var a: nat := aOf(s); - var b: nat := NatArith.boolToNat(bOf(s)); - assert b < 2; - calc { - s in e3; - 2 * a + b == m; - m == a * 2 + b; - (a == m / 2) && (b == m % 2); - s in e1 && s in e2; - } - } - } - - assert Eq2: (iset s | aOf(s) == m / 2) == e2 by { - forall s ensures aOf(s) == m / 2 <==> Model.Sample(n / 2)(s).value in A { - } - } - - assert Eq3: (iset s | aOf(s) == m / 2) == (iset s | Model.Sample(n / 2)(s).value == m / 2) by { - forall s ensures aOf(s) == m / 2 <==> Model.Sample(n / 2)(s).value == m / 2 { - assert aOf(s) == Model.Sample(n / 2)(s).value; - } - } - - assert Eq4: e1 == Measures.PreImage(f, E) by { - forall s ensures Model.Sample(n / 2)(s).rest in E <==> f(s) in E { - } - } - - assert E in Rand.eventSpace && Rand.prob(E) == 0.5 by { - assert E == (iset s | Rand.Head(s) == (m % 2 == 1)); - Rand.CoinHasProbOneHalf(m % 2 == 1); - } - - assert Indep: Rand.prob(e2 * e1) == Rand.prob(e2) * Rand.prob(e1) by { - assert Measures.AreIndepEvents(Rand.eventSpace, Rand.prob, e2, e1) by { - assert Independence.IsIndepFunction(Model.Sample(n / 2)) by { - assert Independence.IsIndep(Model.Sample(n / 2)) by { - SampleIsIndep(n / 2); - } - Independence.IsIndepImpliesIsIndepFunction(Model.Sample(n / 2)); - } - assert E in Rand.eventSpace; - assert Independence.IsIndepFunctionCondition(Model.Sample(n / 2), A, E); - assert e1 == Monad.BitstreamsWithRestIn(Model.Sample(n / 2), E); - assert e2 == Monad.BitstreamsWithValueIn(Model.Sample(n / 2), A); - } - Independence.AreIndepEventsConjunctElimination(e2, e1); - } - - assert ProbE1: Rand.prob(e1) == 0.5 by { - calc { - 0.5; - == - Rand.prob(E); - == { SampleIsMeasurePreserving(n / 2); } - Rand.prob(Measures.PreImage(f, E)); - == { reveal Eq4; } - Rand.prob(e1); - } - } - - calc { - Rand.prob(iset s | Model.Sample(n)(s).value == m); - == { SampleSetEquality(n, m); } - Rand.prob(e3); - == { reveal SplitEvent; } - Rand.prob(e1 * e2); - == { assert e1 * e2 == e2 * e1; } - Rand.prob(e2 * e1); - == { reveal Indep; } - Rand.prob(e2) * Rand.prob(e1); - == { reveal ProbE1; Helper.Congruence(Rand.prob(e1), 0.5, x => x * Rand.prob(e2)); } - 0.5 * Rand.prob(e2); - == - Rand.prob(e2) / 2.0; - == { reveal Eq2; } - Rand.prob(iset s | aOf(s) == m / 2) / 2.0; - == { reveal Eq3; } - Rand.prob(iset s | Model.Sample(n / 2)(s).value == m / 2) / 2.0; - } - } -} diff --git a/src/Distributions/UniformPowerOfTwo/Implementation.dfy b/src/Distributions/UniformPowerOfTwo/Implementation.dfy deleted file mode 100644 index 063cdcfd..00000000 --- a/src/Distributions/UniformPowerOfTwo/Implementation.dfy +++ /dev/null @@ -1,18 +0,0 @@ -/******************************************************************************* - * Copyright by the contributors to the Dafny Project - * SPDX-License-Identifier: MIT - *******************************************************************************/ - -module UniformPowerOfTwo.Implementation { - import Monad - import Model - import Interface - - trait {:termination false} Trait extends Interface.Trait { - method UniformPowerOfTwoSample(n: nat) returns (u: nat) - requires n >= 1 - modifies `s - ensures Model.Sample(n)(old(s)) == Monad.Result(u, s) - - } -} diff --git a/src/Distributions/UniformPowerOfTwo/Interface.dfy b/src/Distributions/UniformPowerOfTwo/Interface.dfy index 77c6f356..98a4c4b9 100644 --- a/src/Distributions/UniformPowerOfTwo/Interface.dfy +++ b/src/Distributions/UniformPowerOfTwo/Interface.dfy @@ -6,10 +6,9 @@ module UniformPowerOfTwo.Interface { import Monad import Model - import Rand + import Bitstream - trait {:termination false} Trait { - ghost var s: Rand.Bitstream + trait {:termination false} Trait extends Bitstream.Interface.Trait { // The return value u is uniformly distributed between 0 <= u < 2^k where 2^k <= n < 2^(k + 1). method UniformPowerOfTwoSample(n: nat) returns (u: nat) @@ -18,4 +17,4 @@ module UniformPowerOfTwo.Interface { ensures Model.Sample(n)(old(s)) == Monad.Result(u, s) } -} +} \ No newline at end of file diff --git a/src/Distributions/UniformPowerOfTwo/Model.dfy b/src/Distributions/UniformPowerOfTwo/Model.dfy index eed5ede3..e341343d 100644 --- a/src/Distributions/UniformPowerOfTwo/Model.dfy +++ b/src/Distributions/UniformPowerOfTwo/Model.dfy @@ -6,10 +6,8 @@ module UniformPowerOfTwo.Model { import Helper import Rand - import Quantifier import Monad import Independence - import Loops import NatArith /************ @@ -18,143 +16,9 @@ module UniformPowerOfTwo.Model { // Adapted from Definition 48 (see issue #79 for the reason of the modification) // The return value u is uniformly distributed between 0 <= u < 2^k where 2^k <= n < 2^(k + 1). - opaque function Sample(n: nat): (h: Monad.Hurd) + function {:axiom} Sample(n: nat): (h: Monad.Hurd) requires n >= 1 ensures forall s :: Sample(n)(s).Result? // always terminates, not just almost surely - { - if n == 1 then - Monad.Return(0) - else - Monad.Bind(Sample(n/2), UnifStep) - } + ensures n == 2 ==> forall s :: h(s)== Monad.Coin(s).Map(b => if b then 1 else 0) - function UnifStepHelper(m: nat): bool -> Monad.Hurd { - (b: bool) => Monad.Return(if b then 2*m + 1 else 2*m) - } - - function UnifStep(m: nat): Monad.Hurd { - Monad.Bind(Monad.Coin, UnifStepHelper(m)) - } - - - // A tail recursive version of Sample - function SampleTailRecursive(n: nat, u: nat := 0): Monad.Hurd - requires n >= 1 - { - (s: Rand.Bitstream) => - if n == 1 then - Monad.Result(u, s) - else - SampleTailRecursive(n / 2, if Rand.Head(s) then 2*u + 1 else 2*u)(Rand.Tail(s)) - } - - /******* - Lemmas - *******/ - - // Equivalence of Sample and its tail-recursive version - lemma SampleCorrespondence(n: nat, s: Rand.Bitstream) - requires n >= 1 - ensures SampleTailRecursive(n)(s) == Sample(n)(s) - { - if n == 1 { - reveal Sample(); - assert SampleTailRecursive(n)(s) == Sample(n)(s); - } else { - var k := NatArith.Log2Floor(n); - assert NatArith.Power(2, k) <= n < NatArith.Power(2, k + 1) by { NatArith.Power2OfLog2Floor(n); } - calc { - SampleTailRecursive(n)(s); - { SampleTailRecursiveEqualIfSameLog2Floor(n, NatArith.Power(2, k), k, 0, s); } - SampleTailRecursive(NatArith.Power(2, k))(s); - Monad.Bind(Sample(NatArith.Power(2, 0)), (u: nat) => SampleTailRecursive(NatArith.Power(2, k), u))(s); - { RelateWithTailRecursive(k, 0, s); } - Sample(NatArith.Power(2, k))(s); - { SampleEqualIfSameLog2Floor(n, NatArith.Power(2, k), k, s); } - Sample(n)(s); - } - } - } - - // All numbers between consecutive powers of 2 behave the same as arguments to SampleTailRecursive - lemma SampleTailRecursiveEqualIfSameLog2Floor(m: nat, n: nat, k: nat, u: nat, s: Rand.Bitstream) - requires m >= 1 - requires n >= 1 - requires NatArith.Power(2, k) <= m < NatArith.Power(2, k + 1) - requires NatArith.Power(2, k) <= n < NatArith.Power(2, k + 1) - ensures SampleTailRecursive(m, u)(s) == SampleTailRecursive(n, u)(s) - { - if k == 0 { - assert m == n; - } else { - assert 1 <= m; - assert 1 <= n; - calc { - SampleTailRecursive(m, u)(s); - SampleTailRecursive(m / 2, if Rand.Head(s) then 2*u + 1 else 2*u)(Rand.Tail(s)); - { SampleTailRecursiveEqualIfSameLog2Floor(m / 2, n / 2, k - 1, if Rand.Head(s) then 2*u + 1 else 2*u, Rand.Tail(s)); } - SampleTailRecursive(n / 2, if Rand.Head(s) then 2*u + 1 else 2*u)(Rand.Tail(s)); - SampleTailRecursive(n, u)(s); - } - } - } - - // All numbers between consecutive powers of 2 behave the same as arguments to Sample - lemma SampleEqualIfSameLog2Floor(m: nat, n: nat, k: nat, s: Rand.Bitstream) - requires m >= 1 - requires n >= 1 - requires NatArith.Power(2, k) <= m < NatArith.Power(2, k + 1) - requires NatArith.Power(2, k) <= n < NatArith.Power(2, k + 1) - ensures Sample(m)(s) == Sample(n)(s) - { - if k == 0 { - assert m == n; - } else { - assert 1 <= m; - assert 1 <= n; - calc { - Sample(m)(s); - { reveal Sample(); } - Monad.Bind(Sample(m / 2), UnifStep)(s); - { SampleEqualIfSameLog2Floor(m / 2, n / 2, k - 1, s); } - Monad.Bind(Sample(n / 2), UnifStep)(s); - { reveal Sample(); } - Sample(n)(s); - } - } - } - - // The induction invariant for the equivalence proof (generalized version of SampleCorrespondence) - lemma RelateWithTailRecursive(l: nat, m: nat, s: Rand.Bitstream) - decreases l - ensures Monad.Bind(Sample(NatArith.Power(2, m)), (u: nat) => SampleTailRecursive(NatArith.Power(2, l), u))(s) == Sample(NatArith.Power(2, m + l))(s) - { - if l == 0 { - calc { - Monad.Bind(Sample(NatArith.Power(2, m)), (u: nat) => SampleTailRecursive(NatArith.Power(2, l), u))(s); - (var Result(u, s') := Sample(NatArith.Power(2, m))(s); SampleTailRecursive(1, u)(s')); - Sample(NatArith.Power(2, m + l))(s); - } - } else { - assert LGreaterZero: NatArith.Power(2, l) >= 1 by { NatArith.PowerGreater0(2, l); } - assert MGreaterZero: NatArith.Power(2, m) >= 1 by { NatArith.PowerGreater0(2, m); } - assert L1GreaterZero: NatArith.Power(2, l - 1) >= 1 by { NatArith.PowerGreater0(2, l - 1); } - calc { - Monad.Bind(Sample(NatArith.Power(2, m)), (u: nat) => SampleTailRecursive(NatArith.Power(2, l), u))(s); - (var Result(u, s') := Sample(NatArith.Power(2, m))(s); SampleTailRecursive(NatArith.Power(2, l), u)(s')); - { reveal LGreaterZero; } - (var Result(u, s') := Sample(NatArith.Power(2, m))(s); - SampleTailRecursive(NatArith.Power(2, l) / 2, if Rand.Head(s') then 2 * u + 1 else 2 * u)(Rand.Tail(s'))); - { assert NatArith.Power(2, l) / 2 == NatArith.Power(2, l - 1); reveal L1GreaterZero; } - (var Result(u', s') := Monad.Bind(Sample(NatArith.Power(2, m)), UnifStep)(s); - SampleTailRecursive(NatArith.Power(2, l - 1), u')(s')); - { assert NatArith.Power(2, m + 1) / 2 == NatArith.Power(2, m); reveal Sample(); } - (var Result(u', s') := Sample(NatArith.Power(2, m + 1))(s); - SampleTailRecursive(NatArith.Power(2, l - 1), u')(s')); - Monad.Bind(Sample(NatArith.Power(2, m + 1)), (u: nat) => SampleTailRecursive(NatArith.Power(2, l - 1), u))(s); - { RelateWithTailRecursive(l - 1, m + 1, s); } - Sample(NatArith.Power(2, m + l))(s); - } - } - } -} +} \ No newline at end of file diff --git a/src/Math/Analysis/Limits.dfy b/src/Math/Analysis/Limits.dfy index cf4b2475..331526ea 100644 --- a/src/Math/Analysis/Limits.dfy +++ b/src/Math/Analysis/Limits.dfy @@ -5,7 +5,6 @@ module Limits { import RealArith - import Reals import Sequences /************ @@ -123,317 +122,4 @@ module Limits { } } - lemma {:axiom} Sandwich(lower: nat -> real, middle: nat -> real, upper: nat -> real, limit: real) - requires ConvergesTo(lower, limit) - requires ConvergesTo(upper, limit) - requires Sequences.IsLeq(lower, middle) - requires Sequences.IsLeq(middle, upper) - ensures ConvergesTo(middle, limit) - - lemma ConstantSequenceConverges(sequence: nat -> real, constant: real, offset: nat := 0) - requires forall n: nat | n >= offset :: sequence(n) == constant - ensures ConvergesTo(sequence, constant) - { - forall epsilon: real | epsilon > 0.0 ensures ExistsCloseSuffix(sequence, constant, epsilon) { - assert SuffixIsClose(sequence, constant, epsilon, offset); - } - } - - lemma LimitIsAdditive(sequence1: nat -> real, limit1: real, sequence2: nat -> real, limit2: real) - requires ConvergesTo(sequence1, limit1) - requires ConvergesTo(sequence2, limit2) - ensures ConvergesTo(Sequences.Add(sequence1, sequence2), limit1 + limit2) - { - var sumSequence := Sequences.Add(sequence1, sequence2); - var sumLimit := limit1 + limit2; - forall epsilon: real | epsilon > 0.0 ensures ExistsCloseSuffix(sumSequence, sumLimit, epsilon) { - assert ExistsCloseSuffix(sequence1, limit1, epsilon / 2.0); - var N1: nat :| SuffixIsClose(sequence1, limit1, epsilon / 2.0, N1); - assert ExistsCloseSuffix(sequence2, limit2, epsilon / 2.0); - var N2: nat :| SuffixIsClose(sequence2, limit2, epsilon / 2.0, N2); - var N: nat :| N >= N1 && N >= N2; - assert SuffixIsClose(sumSequence, sumLimit, epsilon, N) by { - forall n: nat | n >= N ensures RealArith.Dist(sumSequence(n), sumLimit) < epsilon { - calc { - RealArith.Dist(sumSequence(n), sumLimit); - == - RealArith.Dist(sequence1(n) + sequence2(n), limit1 + limit2); - <= - RealArith.Dist(sequence1(n), limit1) + RealArith.Dist(sequence2(n), limit2); - < - epsilon / 2.0 + epsilon / 2.0; - == - epsilon; - } - } - } - } - } - - lemma LimitIsMultiplicative(sequence1: nat -> real, limit1: real, sequence2: nat -> real, limit2: real) - requires ConvergesTo(sequence1, limit1) - requires ConvergesTo(sequence2, limit2) - ensures ConvergesTo(Sequences.Mul(sequence1, sequence2), limit1 * limit2) - { - var bound1 := BoundOfConvergentSequence(sequence1, limit1); - var bound2 := BoundOfConvergentSequence(sequence2, limit2); - var productSequence := Sequences.Mul(sequence1, sequence2); - var productLimit := limit1 * limit2; - forall epsilon: real | epsilon > 0.0 ensures ExistsCloseSuffix(productSequence, productLimit, epsilon) { - var epsilon1 := epsilon / 2.0 / RealArith.Max(RealArith.Abs(limit2), 1.0); - var epsilon2 := epsilon / 2.0 / RealArith.Max(bound1, 1.0); - assert ExistsCloseSuffix(sequence1, limit1, epsilon1); - var N1: nat :| SuffixIsClose(sequence1, limit1, epsilon1, N1); - assert ExistsCloseSuffix(sequence2, limit2, epsilon2); - var N2: nat :| SuffixIsClose(sequence2, limit2, epsilon2, N2); - var N: nat :| N >= N1 && N >= N2; - assert SuffixIsClose(productSequence, productLimit, epsilon, N) by { - forall n: nat | n >= N ensures RealArith.Dist(productSequence(n), productLimit) < epsilon { - var s1 := sequence1(n); - var s2 := sequence2(n); - calc { - RealArith.Dist(productSequence(n), productLimit); - == { assert productSequence(n) == sequence1(n) * sequence2(n) == s1 * s2; } - RealArith.Dist(s1 * s2, limit1 * limit2); - < { LimitIsMultiplicativeSuffixHelper(s1, limit1, s2, limit2, bound1, epsilon); } - epsilon; - } - } - } - } - } - - lemma LimitIsMultiplicativeSuffixHelper(s1: real, limit1: real, s2: real, limit2: real, bound1: real, epsilon: real) - requires epsilon > 0.0 - requires bound1 > 0.0 - requires RealArith.Dist(s1, limit1) < epsilon / 2.0 / RealArith.Max(RealArith.Abs(limit2), 1.0) - requires RealArith.Dist(s2, limit2) < epsilon / 2.0 / RealArith.Max(bound1, 1.0) - requires RealArith.Abs(s1) <= bound1 - ensures RealArith.Dist(s1 * s2, limit1 * limit2) < epsilon - { - assert FirstSummand: RealArith.Abs(limit2) * RealArith.Dist(s1, limit1) <= epsilon / 2.0 by { - var d1 := RealArith.Max(RealArith.Abs(limit2), 1.0); - var epsilon1 := epsilon / 2.0 / RealArith.Max(RealArith.Abs(limit2), 1.0); - calc { - RealArith.Abs(limit2) * RealArith.Dist(s1, limit1); - <= { RealArith.MulMonotonic(RealArith.Abs(limit2), RealArith.Dist(s1, limit1), epsilon1); } - RealArith.Abs(limit2) * epsilon1; - <= { RealArith.MulMonotonic(epsilon1, RealArith.Abs(limit2), d1); } - d1 * epsilon1; - == - epsilon / 2.0; - } - } - assert SecondSummand: bound1 * RealArith.Dist(s2, limit2) < epsilon / 2.0 by { - var d2 := RealArith.Max(bound1, 1.0); - var epsilon2 := epsilon / 2.0 / RealArith.Max(bound1, 1.0); - calc { - bound1 * RealArith.Dist(s2, limit2); - < { RealArith.MulMonotonicStrict(bound1, RealArith.Dist(s2, limit2), epsilon2); } - bound1 * epsilon2; - <= { RealArith.MulMonotonic(epsilon2, bound1, d2); } - d2 * epsilon2; - == - epsilon / 2.0; - } - } - calc { - RealArith.Dist(s1 * s2, limit1 * limit2); - <= { MultiplicationLimitHelper(s1, limit1, s2, limit2, bound1); } - bound1 * RealArith.Dist(s2, limit2) + RealArith.Abs(limit2) * RealArith.Dist(s1, limit1); - < { reveal FirstSummand; reveal SecondSummand; } - epsilon / 2.0 + epsilon / 2.0; - == - epsilon; - } - } - - lemma MultiplicationLimitHelper(s1: real, limit1: real, s2: real, limit2: real, bound1: real) - requires RealArith.Abs(s1) <= bound1 - ensures RealArith.Dist(s1 * s2, limit1 * limit2) <= bound1 * RealArith.Dist(s2, limit2) + RealArith.Abs(limit2) * RealArith.Dist(s1, limit1) - { - calc { - RealArith.Dist(s1 * s2, limit1 * limit2); - == - RealArith.Abs(s1 * s2 - limit1 * limit2); - == - RealArith.Abs(s1 * (s2 - limit2) + limit2 * (s1 - limit1)); - <= - RealArith.Abs(s1 * (s2 - limit2)) + RealArith.Abs(limit2 * (s1 - limit1)); - == { RealArith.AbsMul(s1, s2 - limit2); } - RealArith.Abs(s1) * RealArith.Abs(s2 - limit2) + RealArith.Abs(limit2 * (s1 - limit1)); - == { RealArith.AbsMul(limit2, s1 - limit1); } - RealArith.Abs(s1) * RealArith.Abs(s2 - limit2) + RealArith.Abs(limit2) * RealArith.Abs(s1 - limit1); - <= { RealArith.MultiplicationIsMonotonic(RealArith.Abs(s1), bound1, RealArith.Abs(s2 - limit2)); } - bound1 * RealArith.Abs(s2 - limit2) + RealArith.Abs(limit2) * RealArith.Abs(s1 - limit1); - == - bound1 * RealArith.Dist(s2, limit2) + RealArith.Abs(limit2) * RealArith.Dist(s1, limit1); - } - } - - lemma LimitOfMultiplicationWithZeroSequence(sequence: nat -> real, bound: real, zeroSeq: nat -> real) - requires Sequences.IsBounded(sequence, bound) - requires ConvergesTo(zeroSeq, 0.0) - ensures ConvergesTo(Sequences.Mul(sequence, zeroSeq), 0.0) - { - var productSequence := Sequences.Mul(sequence, zeroSeq); - forall epsilon: real | epsilon > 0.0 ensures ExistsCloseSuffix(productSequence, 0.0, epsilon) { - var epsilon' := epsilon / RealArith.Max(bound, 1.0); - assert ExistsCloseSuffix(zeroSeq, 0.0, epsilon'); - var N :| SuffixIsClose(zeroSeq, 0.0, epsilon', N); - assert SuffixIsClose(productSequence, 0.0, epsilon, N) by { - forall n: nat | n >= N ensures RealArith.Dist(productSequence(n), 0.0) < epsilon { - var s := sequence(n); - var z := zeroSeq(n); - calc { - RealArith.Dist(productSequence(n), 0.0); - == - RealArith.Abs(s * z); - == { RealArith.AbsMul(s, z); } - RealArith.Abs(s) * RealArith.Abs(z); - <= { RealArith.MulMonotonic(RealArith.Abs(s), RealArith.Abs(z), epsilon'); } - RealArith.Abs(s) * epsilon'; - < { RealArith.MulMonotonicStrict(epsilon', RealArith.Abs(s), bound); } - bound * epsilon'; - <= { RealArith.MulMonotonic(epsilon', bound, RealArith.Max(bound, 1.0)); } - RealArith.Max(bound, 1.0) * epsilon'; - == - epsilon; - } - } - } - } - } - - lemma LimitOfInverse(sequence: nat -> real, limit: real) - requires forall n: nat :: sequence(n) != 0.0 - requires limit != 0.0 - requires ConvergesTo(sequence, limit) - ensures ConvergesTo(Sequences.Inverse(sequence), 1.0 / limit) - { - var invSeq := Sequences.Inverse(sequence); - var invLimit := 1.0 / limit; - forall epsilon: real | epsilon > 0.0 ensures ExistsCloseSuffix(invSeq, invLimit, epsilon) { - var limitSquared := limit * limit; - var epsilon' := RealArith.Min(RealArith.Abs(limit) / 2.0, (epsilon * limitSquared) / 2.0); - assert ExistsCloseSuffix(sequence, limit, epsilon'); - var N: nat :| SuffixIsClose(sequence, limit, epsilon', N); - assert SuffixIsClose(invSeq, invLimit, epsilon, N) by { - forall n: nat | n >= N ensures RealArith.Dist(invSeq(n), invLimit) < epsilon { - var s := sequence(n); - calc { - RealArith.Dist(invSeq(n), invLimit); - == { assert invSeq(n) == 1.0 / s; } - RealArith.Dist(1.0 / s, 1.0 / limit); - == { LimitOfInverseHelper1(s, limit); } - RealArith.Dist(s, limit) / RealArith.Abs(limit) / RealArith.Abs(s); - <= { LimitOfInverseHelper2(s, limit); } - 2.0 * RealArith.Dist(s, limit) / limitSquared; - < { RealArith.DivisionIsMonotonicStrict(2.0 * RealArith.Dist(s, limit), 2.0 * epsilon', limitSquared); } - 2.0 * epsilon' / limitSquared; - <= { RealArith.DivisionIsMonotonic(2.0 * epsilon', 2.0 * (epsilon * limitSquared) / 2.0, limitSquared); } - 2.0 * (epsilon * limitSquared) / 2.0 / limitSquared; - == { assert 2.0 * (epsilon * limitSquared) / 2.0 == epsilon * limitSquared; } - (epsilon * limitSquared) / limitSquared; - == - epsilon; - } - } - } - } - } - - lemma LimitOfInverseHelper1(s: real, limit: real) - requires s != 0.0 - requires limit != 0.0 - ensures RealArith.Dist(1.0 / s, 1.0 / limit) == RealArith.Dist(s, limit) / RealArith.Abs(limit) / RealArith.Abs(s) - { - calc { - RealArith.Dist(1.0 / s, 1.0 / limit); - == - RealArith.Abs((1.0 / s) - (1.0 / limit)); - == { RealArith.ExpandFraction(1.0, s, limit); RealArith.ExpandFraction(1.0, limit, s); } - RealArith.Abs(((limit * 1.0) / (limit * s)) - ((1.0 * s) / (limit * s))); - == - RealArith.Abs((limit / (limit * s)) - (s / (limit * s))); - == { RealArith.SubtractionOfFractions(limit, s, limit * s); } - RealArith.Abs((limit - s) / (limit * s)); - == { RealArith.DivMulEqualsDivDiv((limit - s), limit, s); } - RealArith.Abs((limit - s) / limit / s); - == { RealArith.AbsDiv((limit - s) / limit, s); } - RealArith.Abs((limit - s) / limit) / RealArith.Abs(s); - == { RealArith.AbsDiv((limit - s), RealArith.Abs(limit)); } - RealArith.Abs((limit - s)) / RealArith.Abs(limit) / RealArith.Abs(s); - == - RealArith.Dist(s, limit) / RealArith.Abs(limit) / RealArith.Abs(s); - } - } - - lemma LimitOfInverseHelper2(s: real, limit: real) - requires s != 0.0 - requires limit != 0.0 - requires RealArith.Abs(s) >= RealArith.Abs(limit) / 2.0 - ensures limit * limit != 0.0 - ensures RealArith.Dist(s, limit) / RealArith.Abs(limit) / RealArith.Abs(s) <= 2.0 * RealArith.Dist(s, limit) / (limit * limit) - { - var AbsLimit := RealArith.Abs(limit); - assert AbsLimit > 0.0; - assert AbsLimit * AbsLimit != 0.0 by { - if AbsLimit * AbsLimit == 0.0 { - var x := AbsLimit * AbsLimit; - calc { - x; - == - 0.0; - < - AbsLimit * AbsLimit; - == - x; - } - } - } - assert RealArith.Dist(s, limit) / RealArith.Abs(limit) / RealArith.Abs(s) <= 2.0 * RealArith.Dist(s, limit) / (limit * limit) by { - calc { - RealArith.Dist(s, limit) / AbsLimit / RealArith.Abs(s); - <= { RealArith.DivisionIsAntiMonotonic(RealArith.Dist(s, limit) / AbsLimit, RealArith.Abs(s), AbsLimit / 2.0); } - RealArith.Dist(s, limit) / AbsLimit / (AbsLimit / 2.0); - == { RealArith.DivMulEqualsDivDiv2(RealArith.Dist(s, limit) / AbsLimit, AbsLimit, 2.0); } - RealArith.Dist(s, limit) / AbsLimit * 2.0 / AbsLimit; - == { RealArith.DivMulEqualsMulDiv(RealArith.Dist(s, limit), AbsLimit, 2.0); } - RealArith.Dist(s, limit) * 2.0 / AbsLimit / AbsLimit; - == { RealArith.DivMulEqualsDivDiv(2.0 * RealArith.Dist(s, limit), AbsLimit, AbsLimit); } - (2.0 * RealArith.Dist(s, limit)) / (AbsLimit * AbsLimit); - == { assert AbsLimit * AbsLimit == limit * limit; } - 2.0 * RealArith.Dist(s, limit) / (limit * limit); - } - } - } - - lemma OneOverNPlus1ConvergesToZero() - ensures ConvergesTo(Sequences.OneOverNPlus1, 0.0) - { - forall epsilon: real | epsilon > 0.0 ensures ExistsCloseSuffix(Sequences.OneOverNPlus1, 0.0, epsilon) { - var epsilonInv := 1.0 / epsilon; - var N := epsilonInv.Floor; - assert SuffixIsClose(Sequences.OneOverNPlus1, 0.0, epsilon, N) by { - forall n: nat ensures n >= N ==> RealArith.Dist(Sequences.OneOverNPlus1(n), 0.0) < epsilon { - assert Sequences.OneOverNPlus1(n) > 0.0; - assert RealArith.Dist(Sequences.OneOverNPlus1(n), 0.0) == Sequences.OneOverNPlus1(n); - if n >= N { - calc { - Sequences.OneOverNPlus1(n); - <= { Sequences.OneOverNPlus1IsAntimonotonic(N, n); } - Sequences.OneOverNPlus1(N); - == - 1.0 / (N + 1) as real; - < { RealArith.DivisionIsAntiMonotonicStrict(1.0, (N + 1) as real, epsilonInv); } - 1.0 / epsilonInv; - == - epsilon; - } - } - } - } - } - } -} +} \ No newline at end of file diff --git a/src/Math/Analysis/Reals.dfy b/src/Math/Analysis/Reals.dfy index 2f180f21..343079a1 100644 --- a/src/Math/Analysis/Reals.dfy +++ b/src/Math/Analysis/Reals.dfy @@ -29,167 +29,16 @@ module Reals { && forall other: real :: IsUpperBound(s, other) ==> candidate <= other } - // The least upper bound property is one way to characterize the completeness of the reals. - // See, e.g.: https://en.wikipedia.org/wiki/Least-upper-bound_property - // or: https://en.wikipedia.org/wiki/Completeness_of_the_real_numbers - lemma {:axiom} LeastUpperBoundProperty(s: iset, upperBound: real) returns (supremum: real) - requires s != iset{} - requires IsUpperBound(s, upperBound) - ensures IsSupremum(s, supremum) - - // A slight variation of the Dedekind completeness property. - lemma DedekindCompleteness(lower: iset, upper: iset) returns (between: real) - requires lower != iset{} - requires upper != iset{} - requires forall x <- lower, y <- upper :: x <= y - ensures IsUpperBound(lower, between) - ensures IsLowerBound(upper, between) - { - var upperBound :| upperBound in upper; - between := LeastUpperBoundProperty(lower, upperBound); - assert IsLowerBound(upper, between) by { - forall y <- upper ensures between <= y { - assert IsUpperBound(lower, y); - } - } - } - - lemma Completeness(lower: iset, upper: iset) - requires lower != iset{} - requires upper != iset{} - requires forall x <- lower, y <- upper :: x <= y - ensures exists between: real :: IsUpperBound(lower, between) && IsLowerBound(upper, between) - { - assert exists between: real :: IsUpperBound(lower, between) && IsLowerBound(upper, between) by { - var between := DedekindCompleteness(lower, upper); - assert (forall x <- lower :: x <= between) && (forall x <- upper :: between <= x); - } - } - - ghost function Infimum(s: iset, lowerBound: real): (infimum: real) - requires s != iset{} - requires IsLowerBound(s, lowerBound) - ensures IsInfimum(s, infimum) - { - var lowerBounds := iset x: real | IsLowerBound(s, x); - assert lowerBound in lowerBounds; - Completeness(lowerBounds, s); - var infimum :| IsUpperBound(lowerBounds, infimum) && IsLowerBound(s, infimum); - assert forall other: real :: IsLowerBound(s, other) ==> other <= infimum by { - forall other: real ensures IsLowerBound(s, other) ==> other <= infimum { - if IsLowerBound(s, other) { - assert other in lowerBounds; - } - } - } - infimum - } - lemma InfimumIsUnique(s: iset, infimum1: real, infimum2: real) requires IsInfimum(s, infimum1) requires IsInfimum(s, infimum2) ensures infimum1 == infimum2 {} - ghost function Supremum(s: iset, upperBound: real): (supremum: real) - requires s != iset{} - requires IsUpperBound(s, upperBound) - ensures IsSupremum(s, supremum) - { - var upperBounds := iset x: real | IsUpperBound(s, x); - assert upperBound in upperBounds; - Completeness(s, upperBounds); - var supremum :| IsUpperBound(s, supremum) && IsLowerBound(upperBounds, supremum); - assert forall other: real :: IsUpperBound(s, other) ==> supremum <= other by { - forall other: real ensures IsUpperBound(s, other) ==> supremum <= other { - if IsUpperBound(s, other) { - assert other in upperBounds; - } - } - } - supremum - } - lemma SupremumIsUnique(s: iset, infimum1: real, infimum2: real) requires IsSupremum(s, infimum1) requires IsSupremum(s, infimum2) ensures infimum1 == infimum2 {} -} - -// As a sanity check for the above definitons, we prove the existence of the square root of 2: -module Sqrt2Proof { - import RealArith - import Reals - function Square(x: real): real { - x * x - } - - lemma Sqrt2Exists() returns (sqrt2: real) - ensures sqrt2 * sqrt2 == 2.0 - { - var lower := iset x: real | x >= 0.0 && Square(x) < 2.0; - var upper := iset x: real | x >= 0.0 && Square(x) > 2.0; - forall x <- lower, y <- upper ensures x < y { - if x >= y { - calc { - 2.0; - < - Square(y); - <= { RealArith.MulMonotonic(y, y, x); RealArith.MulMonotonic(x, y, x); } - Square(x); - < - 2.0; - } - } - } - assert 1.0 in lower; - assert 2.0 in upper; - sqrt2 := Reals.DedekindCompleteness(lower, upper); - assert 1.0 <= sqrt2 <= 2.0; - assert Square(sqrt2) == 2.0 by { - if sqrt2 * sqrt2 > 2.0 { - var eps := (sqrt2 * sqrt2 - 2.0) / (2.0 * sqrt2); - assert 0.0 < eps < 1.0; - var y := sqrt2 - eps; - assert y * y > 2.0 by { - calc { - y * y; - sqrt2 * sqrt2 - 2.0 * sqrt2 * eps + eps * eps; - sqrt2 * sqrt2 - (sqrt2 * sqrt2 - 2.0) + eps * eps; - 2.0 + eps * eps; - > - 2.0; - } - } - assert y in upper by { - assert y >= 0.0; - assert y * y > 2.0; - } - assert false; - } - if sqrt2 * sqrt2 < 2.0 { - var eps := (2.0 - sqrt2 * sqrt2) / (2.0 * sqrt2 + 1.0); - assert 0.0 < eps < 1.0; - var y := sqrt2 + eps; - assert y * y < 2.0 by { - calc { - y * y; - sqrt2 * sqrt2 + 2.0 * sqrt2 * eps + eps * eps; - sqrt2 * sqrt2 + (2.0 * sqrt2 + eps) * eps; - < { RealArith.MulMonotonicStrict(eps, 2.0 * sqrt2 + eps, 2.0 * sqrt2 + 1.0); } - sqrt2 * sqrt2 + (2.0 * sqrt2 + 1.0) * eps; - sqrt2 * sqrt2 + (2.0 - sqrt2 * sqrt2); - 2.0; - } - } - assert y in lower by { - assert y >= 0.0; - assert y * y < 2.0; - } - assert false; - } - } - } -} +} \ No newline at end of file diff --git a/src/Math/Analysis/Sequences.dfy b/src/Math/Analysis/Sequences.dfy index 6bac9b6e..64bc63f5 100644 --- a/src/Math/Analysis/Sequences.dfy +++ b/src/Math/Analysis/Sequences.dfy @@ -70,4 +70,4 @@ module Sequences { OneOverNPlus1(m) >= OneOverNPlus1(n); } } -} +} \ No newline at end of file diff --git a/src/Math/Analysis/Series.dfy b/src/Math/Analysis/Series.dfy index ffc61a2a..e76a31ae 100644 --- a/src/Math/Analysis/Series.dfy +++ b/src/Math/Analysis/Series.dfy @@ -1,10 +1,12 @@ -module Series { + module Series { import NatArith import RealArith - import Reals - import Sequences import Limits + ghost predicate SumsTo(summands: nat -> real, sum: real) { + Limits.ConvergesTo(PartialSums(summands), sum) + } + function SumFromTo(sequence: nat -> real, start: nat, end: nat): real decreases end - start { @@ -19,10 +21,6 @@ module Series { (n: nat) => SumTo(sequence, n) } - ghost predicate SumsTo(summands: nat -> real, sum: real) { - Limits.ConvergesTo(PartialSums(summands), sum) - } - ghost predicate IsSummable(summands: nat -> real) { exists sum: real :: SumsTo(summands, sum) } @@ -33,195 +31,4 @@ module Series { Limits.Limit(PartialSums(summands)) } - // This would be trivial if Dafny had function extensionality - lemma SumFromToOfEqualsIsEqual(s1: nat -> real, s2: nat -> real, start: nat, end: nat) - decreases end - start - requires forall n: nat | start <= n < end :: s1(n) == s2(n) - ensures SumFromTo(s1, start, end) == SumFromTo(s2, start, end) - { - if end <= start { - calc { - SumFromTo(s1, start, end); - 0.0; - SumFromTo(s2, start, end); - } - } else { - calc { - SumFromTo(s1, start, end); - s1(start) + SumFromTo(s1, start + 1, end); - s2(start) + SumFromTo(s1, start + 1, end); - { SumFromToOfEqualsIsEqual(s1, s2, start + 1, end); } - s2(start) + SumFromTo(s1, start + 1, end); - SumFromTo(s2, start, end); - } - } - } - - // This would be trivial if Dafny had function extensionality - lemma SumOfEqualsIsEqual(summands1: nat -> real, summands2: nat -> real, sum: real) - requires forall n: nat :: summands1(n) == summands2(n) - requires SumsTo(summands1, sum) - ensures SumsTo(summands2, sum) - { - forall n: nat ensures PartialSums(summands1)(n) == PartialSums(summands2)(n) { - calc { - PartialSums(summands1)(n); - SumTo(summands1, n); - { SumFromToOfEqualsIsEqual(summands1, summands2, 0, n); } - SumTo(summands2, n); - PartialSums(summands2)(n); - } - } - Limits.LimitOfEqualsIsEqual(PartialSums(summands1), PartialSums(summands2), sum); - } - - lemma SumIsUnique(summands: nat -> real, sum1: real, sum2: real) - requires SumsTo(summands, sum1) - requires SumsTo(summands, sum2) - ensures sum1 == sum2 - { - Limits.LimitIsUnique(PartialSums(summands), sum1, sum2); - } - - lemma SumIsUniqueAuto(summands: nat -> real) - ensures forall sum1: real, sum2: real :: SumsTo(summands, sum1) && SumsTo(summands, sum2) ==> sum1 == sum2 - { - forall sum1: real, sum2: real ensures SumsTo(summands, sum1) && SumsTo(summands, sum2) ==> sum1 == sum2 { - if SumsTo(summands, sum1) && SumsTo(summands, sum2) { - SumIsUnique(summands, sum1, sum2); - } - } - } - - lemma SumsToImpliesSumIs(summands: nat -> real, sum: real) - requires SumsTo(summands, sum) - ensures Sum(summands) == sum - { - SumIsUnique(summands, Sum(summands), sum); - } - - lemma RemoveFirstSummandFinite(summands: nat -> real, summands': nat -> real, start: nat, end: nat) - decreases end - start - requires forall n: nat :: summands(n + 1) == summands'(n) - ensures SumFromTo(summands, start + 1, end + 1) == SumFromTo(summands', start, end) - { - if end <= start {} else { - calc { - SumFromTo(summands, start + 1, end + 1); - summands(start + 1) + SumFromTo(summands, start + 2, end + 1); - { RemoveFirstSummandFinite(summands, summands', start + 1, end); } - summands'(start) + SumFromTo(summands', start + 1, end); - SumFromTo(summands', start, end); - } - } - } - - lemma RemoveLastSummand(summands: nat -> real, start: nat, end: nat) - decreases end - start - requires start < end - ensures SumFromTo(summands, start, end) == SumFromTo(summands, start, end - 1) + summands(end - 1) - { - if start + 1 == end {} else { - calc { - SumFromTo(summands, start, end); - summands(start) + SumFromTo(summands, start + 1, end); - { RemoveLastSummand(summands, start + 1, end); } - summands(start) + SumFromTo(summands, start + 1, end - 1) + summands(end - 1); - SumFromTo(summands, start, end - 1) + summands(end - 1); - } - } - } - - lemma RemoveFirstSummand(summands: nat -> real, summands': nat -> real, first: real, sum': real) - requires first == summands(0) - requires forall n: nat :: summands(n + 1) == summands'(n) - ensures SumsTo(summands, first + sum') <==> SumsTo(summands', sum') - { - var partialSums' := PartialSums(summands'); - var firstPlusPartialSums' := Sequences.Add(Sequences.Constant(first), partialSums'); - var partialSums := PartialSums(summands); - assert Sequences.IsSuffixOf(firstPlusPartialSums', partialSums, 1) by { - forall n: nat ensures partialSums(n + 1) == firstPlusPartialSums'(n) { - calc { - partialSums(n + 1); - SumTo(summands, n + 1); - first + SumFromTo(summands, 1, n + 1); - { RemoveFirstSummandFinite(summands, summands', 0, n); } - first + SumTo(summands', n); - first + partialSums'(n); - firstPlusPartialSums'(n); - } - } - } - assert limitPlusFirst: Limits.ConvergesTo(firstPlusPartialSums', first + sum') <==> Limits.ConvergesTo(partialSums', sum') by { - assert Limits.ConvergesTo(Sequences.Constant(first), first) by { - Limits.ConstantSequenceConverges(Sequences.Constant(first), first); - } - if Limits.ConvergesTo(partialSums', sum') { - Limits.LimitIsAdditive(Sequences.Constant(first), first, partialSums', sum'); - } - if Limits.ConvergesTo(firstPlusPartialSums', first + sum') { - var canceled := Sequences.Add(Sequences.Constant(-first), firstPlusPartialSums'); - assert Sequences.IsSuffixOf(canceled, partialSums', 0); - Limits.ConstantSequenceConverges(Sequences.Constant(-first), -first); - Limits.LimitIsAdditive(Sequences.Constant(-first), -first, firstPlusPartialSums', first + sum'); - Limits.SuffixConvergesToSame(partialSums', canceled, 0, sum'); - } - } - calc { - SumsTo(summands, first + sum'); - Limits.ConvergesTo(partialSums, first + sum'); - { Limits.SuffixConvergesToSame(partialSums, firstPlusPartialSums', 1, first + sum'); } - Limits.ConvergesTo(firstPlusPartialSums', first + sum'); - { reveal limitPlusFirst; } - Limits.ConvergesTo(partialSums', sum'); - SumsTo(summands', sum'); - } - } - - lemma PartialSumsZero(summands: nat -> real, end: nat, start: nat := 0) - decreases end - start - requires forall i: nat :: summands(i) == 0.0 - ensures SumFromTo(summands, start, end) == 0.0 - { - if end <= start {} else { - calc { - SumFromTo(summands, start, end); - SumFromTo(summands, start + 1, end); - { PartialSumsZero(summands, end, start + 1); } - 0.0; - } - } - } - - lemma ZeroSuffixSum(summands: nat -> real, prefix: nat, sum: real) - requires PartialSums(summands)(prefix) == sum - requires forall n: nat | n >= prefix :: summands(n) == 0.0 - ensures SumsTo(summands, sum) - { - if prefix == 0 { - forall n: nat ensures PartialSums(summands)(n) == 0.0 { - PartialSumsZero(summands, n); - } - Limits.ConstantSequenceConverges(PartialSums(summands), 0.0); - } else { - var rest := (n: nat) => summands(n + 1); - var restSum := PartialSums(rest)(prefix - 1); - assert restSum == sum - summands(0) by { - calc { - restSum; - { RemoveFirstSummandFinite(summands, rest, 1, prefix - 1); } - SumFromTo(summands, 1, prefix); - sum - summands(0); - } - } - assert SumsTo(rest, restSum) by { - RemoveFirstSummandFinite(summands, rest, 0, prefix - 1); - ZeroSuffixSum(rest, prefix - 1, restSum); - } - assert SumsTo(summands, sum) by { - RemoveFirstSummand(summands, rest, summands(0), restSum); - } - } - } -} +} \ No newline at end of file diff --git a/src/Math/Measures.dfy b/src/Math/Measures.dfy index ad81b0ac..a3d494df 100644 --- a/src/Math/Measures.dfy +++ b/src/Math/Measures.dfy @@ -122,79 +122,6 @@ module Measures { ensures PreImage(f, e) == PreImage(f', e') {} - lemma {:axiom} ProbabilityLe1(event: iset, eventSpace: iset>, prob: iset -> real) - requires IsProbability(eventSpace, prob) - requires event in eventSpace - ensures 0.0 <= prob(event) <= 1.0 - - lemma {:axiom} IsMonotonic(eventSpace: iset>, mu: iset -> real, set1: iset, set2: iset) - requires IsMeasure(eventSpace, mu) - requires set1 in eventSpace - requires set2 in eventSpace - requires set1 <= set2 - ensures mu(set1) <= mu(set2) - - lemma MeasureOfDisjointUnionIsSum(eventSpace: iset>, mu: iset -> real, set1: iset, set2: iset) - requires IsMeasure(eventSpace, mu) - requires set1 in eventSpace - requires set2 in eventSpace - requires set1 * set2 == iset{} - ensures mu(set1 + set2) == mu(set1) + mu(set2) - { - assert IsAdditive(eventSpace, mu) by { - PosCountAddImpliesAdd(eventSpace, mu); - } - } - - lemma MeasureOfCountableDisjointUnionIsSum(eventSpace: iset>, mu: iset -> real, parts: nat -> iset, muParts: nat -> real) - requires IsMeasure(eventSpace, mu) - requires forall n: nat :: parts(n) in eventSpace - requires PairwiseDisjoint(parts) - requires forall n: nat :: muParts(n) == mu(parts(n)) - ensures Series.SumsTo(muParts, mu(CountableUnion(parts))) - { - assert Series.SumsTo((n: nat) => mu(parts(n)), mu(CountableUnion(parts))); - Series.SumOfEqualsIsEqual((n: nat) => mu(parts(n)), muParts, mu(CountableUnion(parts))); - } - - // Equation (2.18) - lemma PosCountAddImpliesAdd(eventSpace: iset>, Prob: iset -> real) - requires IsSigmaAlgebra(eventSpace) - requires IsPositive(eventSpace, Prob) - requires IsCountablyAdditive(eventSpace, Prob) - ensures IsAdditive(eventSpace, Prob) - { - forall e1, e2 | e1 in eventSpace && e2 in eventSpace && e1 * e2 == iset{} ensures Prob(e1) + Prob(e2) == Prob(e1 + e2) { - var f : nat -> iset := (n: nat) => if n == 0 then e1 else if n == 1 then e2 else iset{}; - assert CountableUnion(f) == e1 + e2 by { - calc { - CountableUnion(f); - f(0) + f(1); - e1 + e2; - } - } - var probs := (n: nat) => Prob(f(n)); - var probSum := Prob(e1) + Prob(e2); - assert Series.SumsTo(probs, probSum) by { - assert seq(2, probs) == [probs(0), probs(1)]; - calc { - Series.PartialSums(probs)(2); - Series.SumTo(probs, 2); - probs(0) + Series.SumFromTo(probs, 1, 2); - probs(0) + probs(1) + Series.SumFromTo(probs, 2, 2); - Prob(e1) + Prob(e2); - } - Series.ZeroSuffixSum(probs, 2, Prob(e1) + Prob(e2)); - } - assert Series.SumsTo(probs, Prob(CountableUnion(f))) by { - assert IsCountablyAdditive(eventSpace, Prob); - } - Series.SumsToImpliesSumIs(probs, probSum); - Series.SumsToImpliesSumIs(probs, Prob(CountableUnion(f))); - assert Prob(e1 + e2) == Prob(e1) + Prob(e2); - } - } - lemma CountableUnionSplit(f: nat -> iset, i: nat) ensures CountableUnion(f, i) == f(i) + CountableUnion(f, i + 1) {} @@ -232,4 +159,4 @@ module Measures { assert e1 * e2 == Complement(Complement(e1) + Complement(e2)); } -} +} \ No newline at end of file diff --git a/src/ProbabilisticProgramming/Independence.dfy b/src/ProbabilisticProgramming/Independence.dfy index ac80e07d..64a69750 100644 --- a/src/ProbabilisticProgramming/Independence.dfy +++ b/src/ProbabilisticProgramming/Independence.dfy @@ -56,59 +56,17 @@ module Independence { } } - lemma {:axiom} IsIndepImpliesMeasurableBool(f: Monad.Hurd) - requires IsIndep(f) - ensures Measures.IsMeasurable(Rand.eventSpace, Monad.boolResultEventSpace, f) - - lemma IsIndepImpliesMeasurablePreImageBool(f: Monad.Hurd, bSet: iset) - requires IsIndep(f) - ensures Monad.BitstreamsWithValueIn(f, bSet) in Rand.eventSpace - { - var resultSet := Monad.ResultsWithValueIn(bSet); - assert resultSet in Monad.boolResultEventSpace by { - Monad.LiftInEventSpaceToResultEventSpace(bSet, Measures.boolEventSpace); - } - assert Measures.IsMeasurable(Rand.eventSpace, Monad.boolResultEventSpace, f) by { - IsIndepImpliesMeasurableBool(f); - } - assert Monad.BitstreamsWithValueIn(f, bSet) == Measures.PreImage(f, resultSet); - } - - lemma {:axiom} IsIndepImpliesMeasurableNat(f: Monad.Hurd) - requires IsIndep(f) - ensures Measures.IsMeasurable(Rand.eventSpace, Monad.natResultEventSpace, f) - // Equation (3.14) lemma {:axiom} IsIndepImpliesIsIndepFunction(f: Monad.Hurd) requires IsIndep(f) ensures IsIndepFunction(f) - // Equation (3.17) - lemma {:axiom} CoinIsIndep() - ensures IsIndep(Monad.Coin) - - // Equation (3.18) - lemma {:axiom} ReturnIsIndep(x: T) - ensures IsIndep(Monad.Return(x)) - - lemma MapIsIndep(f: Monad.Hurd, g: A -> B) + lemma {:axiom} MapIsIndep(f: Monad.Hurd, g: A -> B) requires IsIndep(f) ensures IsIndep(Monad.Map(f, g)) - { - forall a: A ensures IsIndep(Monad.Return(g(a))) { - ReturnIsIndep(g(a)); - } - BindIsIndep(f, (a: A) => Monad.Return(g(a))); - } - - // Equation (3.19) - lemma {:axiom} BindIsIndep(f: Monad.Hurd, g: A -> Monad.Hurd) - requires IsIndep(f) - requires forall a :: IsIndep(g(a)) - ensures IsIndep(Monad.Bind(f, g)) lemma AreIndepEventsConjunctElimination(e1: iset, e2: iset) requires Measures.AreIndepEvents(Rand.eventSpace, Rand.prob, e1, e2) ensures Rand.prob(e1 * e2) == Rand.prob(e1) * Rand.prob(e2) {} -} +} \ No newline at end of file diff --git a/src/ProbabilisticProgramming/Loops.dfy b/src/ProbabilisticProgramming/Loops.dfy deleted file mode 100644 index 95e6fc0f..00000000 --- a/src/ProbabilisticProgramming/Loops.dfy +++ /dev/null @@ -1,475 +0,0 @@ -/******************************************************************************* - * Copyright by the contributors to the Dafny Project - * SPDX-License-Identifier: MIT - *******************************************************************************/ - -module Loops { - import Helper - import Measures - import Monad - import Quantifier - import Independence - import Rand - - /************ - Definitions - ************/ - - // Definition 37 - function WhileCut(condition: A -> bool, body: A -> Monad.Hurd, init: A, fuel: nat): Monad.Hurd { - if fuel == 0 || !condition(init) then - Monad.Return(init) - else - Monad.Bind(body(init), (init': A) => WhileCut(condition, body, init', fuel - 1)) - } - - ghost predicate WhileTerminatesOn(condition: A -> bool, body: A -> Monad.Hurd, init: A, s: Rand.Bitstream) { - exists fuel: nat :: WhileCutTerminatesWithFuel(condition, body, init, s)(fuel) - } - - ghost function WhileCutTerminatesWithFuel(condition: A -> bool, body: A -> Monad.Hurd, init: A, s: Rand.Bitstream): nat -> bool { - (fuel: nat) => !WhileCut(condition, body, init, fuel)(s).Satisfies(condition) - } - - ghost function WhileCutDivergenceProbability(condition: A -> bool, body: A -> Monad.Hurd, init: A): nat -> real { - (fuel: nat) => Rand.prob(iset s | !WhileCutTerminatesWithFuel(condition, body, init, s)(fuel)) - } - - ghost predicate WhileTerminatesAlmostSurelyInit(condition: A -> bool, body: A -> Monad.Hurd, init: A) { - Quantifier.AlmostSurely((s: Rand.Bitstream) => WhileTerminatesOn(condition, body, init, s)) - } - - // Definition 39 / True iff Prob(iset s | While(condition, body)(a)(s) terminates) == 1 - ghost predicate WhileTerminatesAlmostSurely(condition: A -> bool, body: A -> Monad.Hurd) { - forall init :: WhileTerminatesAlmostSurelyInit(condition, body, init) - } - - // Definition of while loops. - // This definition is opaque because the details are not very useful. - // For proofs, use the lemma `WhileUnroll`. - // Equation (3.25), but modified to use `Monad.Diverging` instead of HOL's `arb` in case of nontermination - opaque ghost function While(condition: A -> bool, body: A -> Monad.Hurd): A -> Monad.Hurd { - (init: A) => - (s: Rand.Bitstream) => - if WhileTerminatesOn(condition, body, init, s) - then - var fuel := LeastFuel(condition, body, init, s); - WhileCut(condition, body, init, fuel)(s) - else - Monad.Diverging - } - - ghost function LeastFuel(condition: A -> bool, body: A -> Monad.Hurd, init: A, s: Rand.Bitstream): (fuel: nat) - requires WhileTerminatesOn(condition, body, init, s) - ensures WhileCutTerminatesWithFuel(condition, body, init, s)(fuel) - ensures forall fuel': nat :: WhileCutTerminatesWithFuel(condition, body, init, s)(fuel') ==> fuel <= fuel' - { - var fuelBound :| WhileCutTerminatesWithFuel(condition, body, init, s)(fuelBound); - Least(WhileCutTerminatesWithFuel(condition, body, init, s), fuelBound) - } - - ghost function Least(property: nat -> bool, bound: nat, start: nat := 0): (l: nat) - decreases bound - start - requires start <= bound - requires property(bound) - ensures property(l) - ensures start <= l <= bound - ensures forall n: nat | start <= n :: property(n) ==> l <= n - { - if start == bound || property(start) - then start - else Least(property, bound, start + 1) - } - - ghost predicate UntilTerminatesAlmostSurely(proposal: Monad.Hurd, accept: A -> bool) { - var reject := (a: A) => !accept(a); - var body := (a: A) => proposal; - WhileTerminatesAlmostSurely(reject, body) - } - - // Definition of until loops (rejection sampling). - // For proofs, use the lemma `UntilUnroll`. - // Definition 44 - ghost function Until(proposal: Monad.Hurd, accept: A -> bool): Monad.Hurd - requires UntilTerminatesAlmostSurely(proposal, accept) - { - reveal While(); - var reject := (a: A) => !accept(a); - var body := (a: A) => proposal; - Monad.Bind(proposal, While(reject, body)) - } - - function WhileLoopExitsAfterOneIteration(condition: A -> bool, body: A -> Monad.Hurd, init: A): (Rand.Bitstream -> bool) { - (s: Rand.Bitstream) => - body(init)(s).Satisfies(v => !condition(v)) - } - - ghost function WhileLoopGloballyExitsAfterOneIteration(condition: A -> bool, body: A -> Monad.Hurd): Rand.Bitstream -> bool { - (s: Rand.Bitstream) => forall init: A :: WhileLoopExitsAfterOneIteration(condition, body, init)(s) - } - - function ProposalIsAccepted(proposal: Monad.Hurd, accept: A -> bool): (Rand.Bitstream -> bool) { - (s: Rand.Bitstream) => - proposal(s).Satisfies(accept) - } - - ghost function UntilLoopResultIsAccepted(proposal: Monad.Hurd, accept: A -> bool): (Rand.Bitstream -> bool) - requires UntilTerminatesAlmostSurely(proposal, accept) - { - (s: Rand.Bitstream) => Until(proposal, accept)(s).Satisfies(accept) - } - - ghost function UntilLoopResultHasProperty(proposal: Monad.Hurd, accept: A -> bool, property: A -> bool): iset - requires UntilTerminatesAlmostSurely(proposal, accept) - { - iset s | Until(proposal, accept)(s).Satisfies(property) - } - - ghost function ProposalIsAcceptedAndHasProperty(proposal: Monad.Hurd, accept: A -> bool, property: A -> bool): iset - { - iset s | proposal(s).Satisfies(property) && proposal(s).Satisfies(accept) - } - - ghost function ProposalAcceptedEvent(proposal: Monad.Hurd, accept: A -> bool): iset - { - iset s | proposal(s).Satisfies(accept) - } - - - /******* - Lemmas - *******/ - - lemma LeastFuelUnroll(condition: A -> bool, body: A -> Monad.Hurd, init: A, s: Rand.Bitstream, init': A, s': Rand.Bitstream, fuel': nat) - requires WhileTerminatesOn(condition, body, init', s') - requires LeastFuel(condition, body, init', s') == fuel' - requires condition(init) - requires body(init)(s) == Monad.Result(init', s') - ensures WhileTerminatesOn(condition, body, init, s) - ensures LeastFuel(condition, body, init, s) == fuel' + 1 - { - assert WhileTerminatesOn(condition, body, init, s) by { - WhileCutTerminatesWithFuelUnroll(condition, body, init, s, init', s', fuel'); - } - var fuel := LeastFuel(condition, body, init, s); - assert fuel == fuel' + 1 by { - WhileCutTerminatesWithFuelUnroll(condition, body, init, s, init', s', fuel'); - WhileCutTerminatesWithFuelUnroll(condition, body, init, s, init', s', fuel - 1); - } - } - - lemma WhileCutUnroll(condition: A -> bool, body: A -> Monad.Hurd, init: A, s: Rand.Bitstream, init': A, s': Rand.Bitstream, fuel: nat) - requires condition(init) - requires body(init)(s) == Monad.Result(init', s') - ensures WhileCut(condition, body, init, fuel + 1)(s) == WhileCut(condition, body, init', fuel)(s') - {} - - - lemma WhileCutTerminatesWithFuelUnroll(condition: A -> bool, body: A -> Monad.Hurd, init: A, s: Rand.Bitstream, init': A, s': Rand.Bitstream, fuel: nat) - requires condition(init) - requires body(init)(s) == Monad.Result(init', s') - ensures WhileCutTerminatesWithFuel(condition, body, init, s)(fuel + 1) == WhileCutTerminatesWithFuel(condition, body, init', s')(fuel) - {} - - lemma WhileCutTerminatesUnroll(condition: A -> bool, body: A -> Monad.Hurd, init: A, s: Rand.Bitstream, init': A, s': Rand.Bitstream) - requires condition(init) - requires body(init)(s) == Monad.Result(init', s') - ensures WhileTerminatesOn(condition, body, init, s) == WhileTerminatesOn(condition, body, init', s') - { - if WhileTerminatesOn(condition, body, init, s) { - var fuel: nat :| WhileCutTerminatesWithFuel(condition, body, init, s)(fuel); - WhileCutTerminatesWithFuelUnroll(condition, body, init, s, init', s', fuel - 1); - } - if WhileTerminatesOn(condition, body, init', s') { - var fuel: nat :| WhileCutTerminatesWithFuel(condition, body, init', s')(fuel); - WhileCutTerminatesWithFuelUnroll(condition, body, init, s, init', s', fuel); - } - } - - lemma WhileUnrollIfConditionSatisfied(condition: A -> bool, body: A -> Monad.Hurd, init: A, s: Rand.Bitstream, init': A, s': Rand.Bitstream, loop: Monad.Result, unrolled: Monad.Result) - requires WhileTerminatesOn(condition, body, init, s) - requires condition(init) - requires body(init)(s) == Monad.Result(init', s') - requires loop == While(condition, body)(init)(s) - requires unrolled == While(condition, body)(init')(s') - ensures loop == unrolled - { - var fuel: nat := LeastFuel(condition, body, init, s); - assert fuel >= 1; - var fuel': nat := fuel - 1; - assert WhileCutTerminatesWithFuel(condition, body, init', s')(fuel'); - assert WhileTerminatesOn(condition, body, init', s'); - var minFuel: nat := LeastFuel(condition, body, init', s'); - assert minFuel == fuel' by { - LeastFuelUnroll(condition, body, init, s, init', s', minFuel); - } - assert loop == unrolled by { - calc { - loop; - { reveal While(); } - WhileCut(condition, body, init, fuel)(s); - { WhileCutUnroll(condition, body, init, s, init', s', fuel'); } - WhileCut(condition, body, init', fuel')(s'); - { reveal While(); } - unrolled; - } - } - } - - lemma WhileUnrollIfTerminates(condition: A -> bool, body: A -> Monad.Hurd, init: A, s: Rand.Bitstream, fuel: nat, loop: Monad.Result, unrolled: Monad.Result) - requires WhileTerminatesOn(condition, body, init, s) - requires fuel == LeastFuel(condition, body, init, s) - requires loop == While(condition, body)(init)(s) - requires unrolled == (if condition(init) then Monad.Bind(body(init), While(condition, body)) else Monad.Return(init))(s) - ensures loop == unrolled - { - if condition(init) { - assert fuel >= 1; - match body(init)(s) - case Diverging => - calc { - loop; - { reveal While(); } - WhileCut(condition, body, init, fuel)(s); - Monad.Diverging; - unrolled; - } - case Result(init', s') => - calc { - loop; - { WhileUnrollIfConditionSatisfied(condition, body, init, s, init', s', loop, unrolled); } - While(condition, body)(init')(s'); - unrolled; - } - } else { - WhileInitialConditionNegated(condition, body, init, s); - calc { - loop; - Monad.Result(init, s); - unrolled; - } - } - } - - lemma WhileUnrollIfDiverges(condition: A -> bool, body: A -> Monad.Hurd, init: A, s: Rand.Bitstream, loop: Monad.Result, unrolled: Monad.Result) - requires !WhileTerminatesOn(condition, body, init, s) - requires loop == While(condition, body)(init)(s) - requires unrolled == (if condition(init) then Monad.Bind(body(init), While(condition, body)) else Monad.Return(init))(s) - ensures loop == unrolled == Monad.Diverging - { - reveal While(); - if !condition(init) { - WhileInitialConditionNegated(condition, body, init, s); - } - match body(init)(s) - case Diverging => - assert unrolled == Monad.Diverging; - case Result(init', s') => - assert !WhileTerminatesOn(condition, body, init', s') by { - WhileCutTerminatesUnroll(condition, body, init, s, init', s'); - } - } - - // Theorem 38 - lemma WhileUnroll(condition: A -> bool, body: A -> Monad.Hurd, init: A, s: Rand.Bitstream) - requires WhileTerminatesAlmostSurely(condition, body) - ensures While(condition, body)(init)(s) == (if condition(init) then Monad.Bind(body(init), While(condition, body)) else Monad.Return(init))(s) - { - var loop := While(condition, body)(init)(s); - var unrolled := (if condition(init) then Monad.Bind(body(init), While(condition, body)) else Monad.Return(init))(s); - assert loop == unrolled by { - if WhileTerminatesOn(condition, body, init, s) { - var fuel: nat := LeastFuel(condition, body, init, s); - WhileUnrollIfTerminates(condition, body, init, s, fuel, loop, unrolled); - } else { - WhileUnrollIfDiverges(condition, body, init, s, loop, unrolled); - } - } - } - - lemma EnsureUntilTerminates(proposal: Monad.Hurd, accept: A -> bool) - requires Independence.IsIndep(proposal) - requires Quantifier.WithPosProb((s: Rand.Bitstream) => proposal(s).Satisfies(accept)) - ensures UntilTerminatesAlmostSurely(proposal, accept) - { - var reject := (a: A) => !accept(a); - var body := (a: A) => proposal; - var proposalIsAccepted := (s: Rand.Bitstream) => proposal(s).Satisfies(accept); - assert UntilTerminatesAlmostSurely(proposal, accept) by { - forall a: A ensures Independence.IsIndep(body(a)) { - assert body(a) == proposal; - } - forall a: A ensures Quantifier.WithPosProb(WhileLoopExitsAfterOneIteration(reject, body, a)) { - assert Quantifier.WithPosProb(proposalIsAccepted); - assert (iset s | proposalIsAccepted(s)) == (iset s | WhileLoopExitsAfterOneIteration(reject, body, a)(s)); - } - assert WhileTerminatesAlmostSurely(reject, body) by { - assert Quantifier.WithPosProb(WhileLoopGloballyExitsAfterOneIteration(reject, body)) by { - var acceptsImmediately := (s: Rand.Bitstream) => proposal(s).Satisfies(accept); - var event1 := iset s | acceptsImmediately(s); - var event2 := iset s | WhileLoopGloballyExitsAfterOneIteration(reject, body)(s); - assert event1 <= event2 by { - forall s ensures s in event1 ==> s in event2 { - assert acceptsImmediately(s) ==> WhileLoopGloballyExitsAfterOneIteration(reject, body)(s) by { - if acceptsImmediately(s) { - forall a: A ensures WhileLoopExitsAfterOneIteration(reject, body, a)(s) { - assert proposal == body(a); - } - } - } - } - } - assert event2 in Rand.eventSpace by { - if inhabitant: A :| true { - assert event2 <= event1 by { - forall s ensures s in event2 ==> s in event1 { - assert proposal == body(inhabitant); - if s in event2 { - calc { - WhileLoopGloballyExitsAfterOneIteration(reject, body)(s); - WhileLoopExitsAfterOneIteration(reject, body, inhabitant)(s); - acceptsImmediately(s); - } - } - } - } - assert event1 == event2; - } else { - assert event2 == iset s :: s by { - forall s ensures s in event2 { - forall a: A ensures WhileLoopExitsAfterOneIteration(reject, body, a)(s) { - assert false; - } - } - } - } - } - calc ==> { - Quantifier.WithPosProb(acceptsImmediately); - Rand.prob(event1) > 0.0; - { Rand.ProbIsProbabilityMeasure(); Measures.IsMonotonic(Rand.eventSpace, Rand.prob, event1, event2); } - Rand.prob(event2) > 0.0; - Quantifier.WithPosProb(WhileLoopGloballyExitsAfterOneIteration(reject, body)); - } - } - EnsureWhileTerminates(reject, body); - } - } - } - - // (Equation 3.30) / Sufficient conditions for while-loop termination - lemma {:axiom} EnsureWhileTerminates(condition: A -> bool, body: A -> Monad.Hurd) - requires forall a :: Independence.IsIndep(body(a)) - requires Quantifier.WithPosProb(WhileLoopGloballyExitsAfterOneIteration(condition, body)) - ensures WhileTerminatesAlmostSurely(condition, body) - - ghost function WhileCutProbability(condition: A -> bool, body: A -> Monad.Hurd, init: A, resultSet: iset): nat -> real { - (fuel: nat) => Rand.prob(Monad.BitstreamsWithValueIn(WhileCut(condition, body, init, fuel), resultSet)) - } - - // Theorem 45 (wrong!) / PROB_BERN_UNTIL (correct!) - lemma {:axiom} UntilProbabilityFraction(proposal: Monad.Hurd, accept: A -> bool, d: A -> bool) - requires Independence.IsIndep(proposal) - requires Quantifier.WithPosProb(ProposalIsAccepted(proposal, accept)) - ensures UntilTerminatesAlmostSurely(proposal, accept) - ensures - && UntilLoopResultHasProperty(proposal, accept, d) in Rand.eventSpace - && ProposalIsAcceptedAndHasProperty(proposal, accept, d) in Rand.eventSpace - && ProposalAcceptedEvent(proposal, accept) in Rand.eventSpace - && Rand.prob(ProposalAcceptedEvent(proposal, accept)) != 0.0 - && Rand.prob(UntilLoopResultHasProperty(proposal, accept, d)) == Rand.prob(ProposalIsAcceptedAndHasProperty(proposal, accept, d)) / Rand.prob(ProposalAcceptedEvent(proposal, accept)) - - // Equation (3.39) - lemma UntilUnroll(proposal: Monad.Hurd, accept: A -> bool, s: Rand.Bitstream) - requires Independence.IsIndep(proposal) - requires UntilTerminatesAlmostSurely(proposal, accept) - ensures Until(proposal, accept)(s) == Monad.Bind(proposal, (x: A) => if accept(x) then Monad.Return(x) else Until(proposal, accept))(s) - { - var reject := (a: A) => !accept(a); - var body := (a: A) => proposal; - UntilAsWhile(proposal, accept, s); - match proposal(s) - case Diverging => - case Result(init, s') => WhileUnroll(reject, body, init, s'); - } - - // Equation (3.40) - lemma EnsureUntilTerminatesAndForAll(proposal: Monad.Hurd, accept: A -> bool) - requires Independence.IsIndep(proposal) - requires Quantifier.WithPosProb(ProposalIsAccepted(proposal, accept)) - ensures UntilTerminatesAlmostSurely(proposal, accept) - ensures Quantifier.AlmostSurely(UntilLoopResultIsAccepted(proposal, accept)) - { - EnsureUntilTerminates(proposal, accept); - assume {:axiom} Quantifier.AlmostSurely(UntilLoopResultIsAccepted(proposal, accept)); // add later - } - - lemma WhileCutIsIndep(condition: A -> bool, body: A -> Monad.Hurd, init: A, fuel: nat) - requires forall a: A :: Independence.IsIndep(body(a)) - ensures Independence.IsIndep(WhileCut(condition, body, init, fuel)) - { - if fuel == 0 || !condition(init) { - Independence.ReturnIsIndep(init); - } else { - forall init': A ensures Independence.IsIndep(WhileCut(condition, body, init', fuel - 1)) { - WhileCutIsIndep(condition, body, init', fuel - 1); - } - Independence.BindIsIndep(body(init), init' => WhileCut(condition, body, init', fuel - 1)); - } - } - - lemma WhileIsIndep(condition: A -> bool, body: A -> Monad.Hurd, init: A) - requires forall a: A :: Independence.IsIndep(body(a)) - requires WhileTerminatesAlmostSurely(condition, body) - ensures Independence.IsIndep(While(condition, body)(init)) - { - // To prove this, we need a definition of Independence.IsIndep - assume {:axiom} false; - } - - lemma UntilIsIndep(proposal: Monad.Hurd, accept: A -> bool) - requires Independence.IsIndep(proposal) - requires UntilTerminatesAlmostSurely(proposal, accept) - ensures Independence.IsIndep(Until(proposal, accept)) - { - var reject := (a: A) => !accept(a); - var body := (a: A) => proposal; - forall init: A ensures Independence.IsIndep(While(reject, body)(init)) { - WhileIsIndep(reject, body, init); - } - Independence.BindIsIndep(proposal, While(reject, body)); - } - - lemma WhileNegatesCondition(condition: A -> bool, body: A -> Monad.Hurd, init: A, s: Rand.Bitstream) - requires While(condition, body)(init)(s).Result? - ensures !condition(While(condition, body)(init)(s).value) - { - reveal While(); - } - - lemma WhileInitialConditionNegated(condition: A -> bool, body: A -> Monad.Hurd, init: A, s: Rand.Bitstream) - requires !condition(init) - ensures While(condition, body)(init)(s) == Monad.Return(init)(s) - { - reveal While(); - assert WhileCutTerminatesWithFuel(condition, body, init, s)(0); - } - - lemma UntilResultIsAccepted(proposal: Monad.Hurd, accept: A -> bool, s: Rand.Bitstream) - requires UntilTerminatesAlmostSurely(proposal, accept) - requires Until(proposal, accept)(s).Result? - ensures accept(Until(proposal, accept)(s).value) - { - reveal While(); - } - - lemma UntilAsWhile(proposal: Monad.Hurd, accept: A -> bool, s: Rand.Bitstream) - requires UntilTerminatesAlmostSurely(proposal, accept) - ensures - var reject := (a: A) => !accept(a); - var body := (a: A) => proposal; - Until(proposal, accept)(s) == proposal(s).Bind(While(reject, body)) - { - reveal While(); - } -} diff --git a/src/ProbabilisticProgramming/Monad.dfy b/src/ProbabilisticProgramming/Monad.dfy index 748654a2..b793324f 100644 --- a/src/ProbabilisticProgramming/Monad.dfy +++ b/src/ProbabilisticProgramming/Monad.dfy @@ -173,69 +173,4 @@ module Monad { ensures Join(Map(fff, Join))(s) == Join(Join(fff))(s) {} - lemma LiftInEventSpaceToResultEventSpace(event: iset, eventSpace: iset>) - requires event in eventSpace - ensures ResultsWithValueIn(event) in ResultEventSpace(eventSpace) - { - var results := ResultsWithValueIn(event); - assert Measures.IsSigmaAlgebra(Rand.eventSpace) by { - Rand.ProbIsProbabilityMeasure(); - } - assert Values(results) == event by { - forall v: A ensures v in event <==> v in Values(results) { - var s: Rand.Bitstream :| true; - assert v in event <==> Result(v, s) in results; - } - } - assert Rests(results) in Rand.eventSpace by { - if v :| v in event { - 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; - true; - } - } - } - } else { - assert Rests(results) == iset{}; - } - } - } - - lemma LiftRestInEventSpaceToResultEventSpace(rests: iset, eventSpace: iset>) - requires rests in Rand.eventSpace - requires iset{} in eventSpace - requires Measures.SampleSpace() in eventSpace - ensures ResultsWithRestIn(rests) in ResultEventSpace(eventSpace) - { - var results := ResultsWithRestIn(rests); - assert Measures.IsSigmaAlgebra(Rand.eventSpace) by { - Rand.ProbIsProbabilityMeasure(); - } - assert Values(results) in eventSpace by { - if rest :| rest in rests { - assert Values(results) == Measures.SampleSpace() by { - forall v: A ensures v in Values(results) { - assert Result(v, rest) in results; - } - } - } else { - assert Values(results) == iset{}; - } - } - assert Rests(results) in Rand.eventSpace by { - if v: A :| true { - assert Rests(results) == rests by { - forall s: Rand.Bitstream ensures s in rests <==> s in Rests(results) { - assert s in rests <==> Result(v, s) in results; - } - } - } else { - assert Rests(results) == iset{}; - } - } - } -} - +} \ No newline at end of file diff --git a/src/ProbabilisticProgramming/Quantifier.dfy b/src/ProbabilisticProgramming/Quantifier.dfy deleted file mode 100644 index 435da579..00000000 --- a/src/ProbabilisticProgramming/Quantifier.dfy +++ /dev/null @@ -1,24 +0,0 @@ -/******************************************************************************* - * Copyright by the contributors to the Dafny Project - * SPDX-License-Identifier: MIT - *******************************************************************************/ - -module Quantifier { - import Rand - - /************ - Definitions - ************/ - - ghost predicate AlmostSurely(p: Rand.Bitstream -> bool) { - var e := iset s | p(s); - && e in Rand.eventSpace - && Rand.prob(e) == 1.0 - } - - ghost predicate WithPosProb(p: Rand.Bitstream -> bool) { - var e := iset s | p(s); - && e in Rand.eventSpace - && Rand.prob(e) > 0.0 - } -} diff --git a/src/ProbabilisticProgramming/RandomSource.dfy b/src/ProbabilisticProgramming/RandomSource.dfy index 951f384e..405b6512 100644 --- a/src/ProbabilisticProgramming/RandomSource.dfy +++ b/src/ProbabilisticProgramming/RandomSource.dfy @@ -50,20 +50,4 @@ module Rand { lemma {:axiom} ProbIsProbabilityMeasure() ensures Measures.IsProbability(eventSpace, prob) - // Equation (2.68) && (2.77) - lemma {:axiom} CoinHasProbOneHalf(b: bool) - ensures - var e := (iset s | Head(s) == b); - && e in eventSpace - && prob(e) == 0.5 - - // Equation (2.82) - lemma {:axiom} MeasureHeadDrop(n: nat, s: Bitstream) - ensures - && (iset s | Head(Drop(n, s))) in eventSpace - && prob(iset s | Head(Drop(n, s))) == 0.5 - - // Equation (2.78) - lemma {:axiom} TailIsMeasurePreserving() - ensures Measures.IsMeasurePreserving(eventSpace, prob, eventSpace, prob, Tail) -} +} \ No newline at end of file