diff --git a/src/Distributions/Bernoulli/Correctness.dfy b/src/Distributions/Bernoulli/Correctness.dfy index 4762069c..ae4dd4d8 100644 --- a/src/Distributions/Bernoulli/Correctness.dfy +++ b/src/Distributions/Bernoulli/Correctness.dfy @@ -44,7 +44,7 @@ module Bernoulli.Correctness { ensures var e := iset s | Model.Sample(m, n)(s).0; && e in Random.eventSpace - && Random.Prob(e) == m as real / n as real + && Random.prob(e) == m as real / n as real { var e := iset s | Model.Sample(m, n)(s).0; @@ -59,10 +59,10 @@ module Bernoulli.Correctness { } } - assert e in Random.eventSpace && Random.Prob(e) == 0.0 by { + assert e in Random.eventSpace && Random.prob(e) == 0.0 by { Random.ProbIsProbabilityMeasure(); assert Measures.IsSigmaAlgebra(Random.eventSpace, Random.sampleSpace); - assert Measures.IsPositive(Random.eventSpace, Random.Prob); + assert Measures.IsPositive(Random.eventSpace, Random.prob); } } else { var e1 := iset s | Uniform.Model.Sample(n)(s).0 == m-1; @@ -84,12 +84,12 @@ module Bernoulli.Correctness { e1 + e2; } - assert A1: e1 in Random.eventSpace && Random.Prob(e1) == 1.0 / (n as real) by { + assert A1: e1 in Random.eventSpace && Random.prob(e1) == 1.0 / (n as real) by { Uniform.Correctness.UniformFullCorrectness(n, m-1); assert e1 == Uniform.Correctness.SampleEquals(n, m-1); } - assert A2: e2 in Random.eventSpace && Random.Prob(e2) == (m-1) as real / n as real by { + assert A2: e2 in Random.eventSpace && Random.prob(e2) == (m-1) as real / n as real by { BernoulliCorrectness(m-1, n); } @@ -102,11 +102,11 @@ module Bernoulli.Correctness { } calc { - Random.Prob(e); + Random.prob(e); { assert e == e1 + e2; } - Random.Prob(e1 + e2); - { reveal A1; reveal A2; assert e1 * e2 == iset{}; Random.ProbIsProbabilityMeasure(); Measures.PosCountAddImpliesAdd(Random.eventSpace, Random.sampleSpace, Random.Prob); assert Measures.IsAdditive(Random.eventSpace, Random.Prob); } - Random.Prob(e1) + Random.Prob(e2); + Random.prob(e1 + e2); + { reveal A1; reveal A2; assert e1 * e2 == iset{}; Random.ProbIsProbabilityMeasure(); Measures.PosCountAddImpliesAdd(Random.eventSpace, Random.sampleSpace, Random.prob); assert Measures.IsAdditive(Random.eventSpace, Random.prob); } + Random.prob(e1) + Random.prob(e2); { reveal A1; reveal A2; } (1.0 / n as real) + ((m-1) as real / n as real); { reveal A3; } diff --git a/src/Distributions/BernoulliExpNeg/Correctness.dfy b/src/Distributions/BernoulliExpNeg/Correctness.dfy index 578fe1d0..b38f3920 100644 --- a/src/Distributions/BernoulliExpNeg/Correctness.dfy +++ b/src/Distributions/BernoulliExpNeg/Correctness.dfy @@ -12,7 +12,7 @@ module BernoulliExpNeg.Correctness { lemma {:axiom} Correctness(gamma: Rationals.Rational) requires 0 <= gamma.numer - ensures Random.Prob(iset s | Model.Sample(gamma)(s).0) == Exponential.Exp(-Rationals.ToReal(gamma)) + ensures Random.prob(iset s | Model.Sample(gamma)(s).0) == Exponential.Exp(-Rationals.ToReal(gamma)) lemma {:axiom} SampleIsIndep(gamma: Rationals.Rational) requires 0 <= gamma.numer diff --git a/src/Distributions/Uniform/Correctness.dfy b/src/Distributions/Uniform/Correctness.dfy index 83e3b9b3..748de4fd 100644 --- a/src/Distributions/Uniform/Correctness.dfy +++ b/src/Distributions/Uniform/Correctness.dfy @@ -33,7 +33,7 @@ module Uniform.Correctness { lemma UniformFullCorrectness(n: nat, i: nat) requires 0 <= i < n ensures SampleEquals(n, i) in Random.eventSpace - ensures Random.Prob(SampleEquals(n, i)) == 1.0 / (n as real) + ensures Random.prob(SampleEquals(n, i)) == 1.0 / (n as real) { var equalsI := (x: nat) => x == i; @@ -46,7 +46,7 @@ module Uniform.Correctness { var eventProposalAcceptedAndEqualsI := Loops.ProposalIsAcceptedAndHasProperty(Model.Proposal(n), Model.Accept(n), equalsI); var proposalAccepted := Loops.ProposalAcceptedEvent(Model.Proposal(n), Model.Accept(n)); - assert Fraction: Random.Prob(eventResultEqualsI) == Random.Prob(eventProposalAcceptedAndEqualsI) / Random.Prob(proposalAccepted); + assert Fraction: Random.prob(eventResultEqualsI) == Random.prob(eventProposalAcceptedAndEqualsI) / Random.prob(proposalAccepted); assert Eq: eventResultEqualsI == SampleEquals(n, i) by { forall s ensures s in eventResultEqualsI <==> s in SampleEquals(n, i) { @@ -58,15 +58,15 @@ module Uniform.Correctness { reveal Eq; } - assert Random.Prob(SampleEquals(n, i)) == 1.0 / (n as real) by { + assert Random.prob(SampleEquals(n, i)) == 1.0 / (n as real) by { calc { - Random.Prob(SampleEquals(n, i)); + Random.prob(SampleEquals(n, i)); { reveal Eq; } - Random.Prob(eventResultEqualsI); + Random.prob(eventResultEqualsI); { reveal Fraction; } - Random.Prob(eventProposalAcceptedAndEqualsI) / Random.Prob(proposalAccepted); + Random.prob(eventProposalAcceptedAndEqualsI) / Random.prob(proposalAccepted); { ProbabilityProposalAcceptedAndEqualsI(n, i); } - (1.0 / (Helper.Power(2, Helper.Log2Floor(2 * n)) as real)) / Random.Prob(proposalAccepted); + (1.0 / (Helper.Power(2, Helper.Log2Floor(2 * n)) as real)) / Random.prob(proposalAccepted); { ProbabilityProposalAccepted(n); } (1.0 / (Helper.Power(2, Helper.Log2Floor(2 * n)) as real)) / ((n as real) / (Helper.Power(2, Helper.Log2Floor(2 * n)) as real)); { Helper.SimplifyFractions(1.0, n as real, Helper.Power(2, Helper.Log2Floor(2 * n)) as real); } @@ -79,7 +79,7 @@ module Uniform.Correctness { requires 0 <= i < n ensures var e := Loops.ProposalIsAcceptedAndHasProperty(Model.Proposal(n), Model.Accept(n), (x: nat) => x == i); - Random.Prob(e) == 1.0 / (Helper.Power(2, Helper.Log2Floor(2 * n)) as real) + Random.prob(e) == 1.0 / (Helper.Power(2, Helper.Log2Floor(2 * n)) as real) { var e := Loops.ProposalIsAcceptedAndHasProperty(Model.Proposal(n), Model.Accept(n), (x: nat) => x == i); assert i < Helper.Power(2, Helper.Log2Floor(2 * n)) by { @@ -102,7 +102,7 @@ module Uniform.Correctness { lemma ProbabilityProposalAccepted(n: nat) requires n >= 1 ensures - Random.Prob(Loops.ProposalAcceptedEvent(Model.Proposal(n), Model.Accept(n))) == (n as real) / (Helper.Power(2, Helper.Log2Floor(2 * n)) as real) + Random.prob(Loops.ProposalAcceptedEvent(Model.Proposal(n), Model.Accept(n))) == (n as real) / (Helper.Power(2, Helper.Log2Floor(2 * n)) as real) { var e := Loops.ProposalAcceptedEvent(Model.Proposal(n), Model.Accept(n)); assert n < Helper.Power(2, Helper.Log2Floor(2 * n)) by { Helper.NLtPower2Log2FloorOf2N(n); } @@ -115,11 +115,11 @@ module Uniform.Correctness { } } } - assert Random.Prob(Loops.ProposalAcceptedEvent(Model.Proposal(n), Model.Accept(n))) == (n as real) / (Helper.Power(2, Helper.Log2Floor(2 * n)) as real) by { + assert Random.prob(Loops.ProposalAcceptedEvent(Model.Proposal(n), Model.Accept(n))) == (n as real) / (Helper.Power(2, Helper.Log2Floor(2 * n)) as real) by { calc { - Random.Prob(e); + Random.prob(e); { reveal Equal; } - Random.Prob(iset s | UniformPowerOfTwo.Model.Sample(2 * n)(s).0 < n); + Random.prob(iset s | UniformPowerOfTwo.Model.Sample(2 * n)(s).0 < n); { UniformPowerOfTwo.Correctness.UnifCorrectness2Inequality(2 * n, n); } (n as real) / (Helper.Power(2, Helper.Log2Floor(2 * n)) as real); } @@ -132,14 +132,14 @@ module Uniform.Correctness { ensures var e := iset s | Model.IntervalSample(a, b)(s).0 == i; && e in Random.eventSpace - && Random.Prob(e) == (1.0 / ((b-a) as real)) + && Random.prob(e) == (1.0 / ((b-a) as real)) { assert 0 <= i - a < b - a by { assert a <= i < b; } var e' := SampleEquals(b - a, i - a); assert e' in Random.eventSpace by { UniformFullCorrectness(b - a, i - a); } - assert Random.Prob(e') == (1.0 / ((b-a) as real)) by { UniformFullCorrectness(b - a, i - a); } + assert Random.prob(e') == (1.0 / ((b-a) as real)) by { UniformFullCorrectness(b - a, i - a); } var e := iset s | Model.IntervalSample(a, b)(s).0 == i; assert e == e' by { forall s ensures Model.IntervalSample(a, b)(s).0 == i <==> Model.Sample(b-a)(s).0 == i - a { diff --git a/src/Distributions/Uniform/Model.dfy b/src/Distributions/Uniform/Model.dfy index eeb0975b..69102340 100644 --- a/src/Distributions/Uniform/Model.dfy +++ b/src/Distributions/Uniform/Model.dfy @@ -64,13 +64,13 @@ module Uniform.Model { } } assert Quantifier.WithPosProb(Loops.ProposalIsAccepted(Proposal(n), Accept(n))) by { - assert Random.Prob(e) > 0.0 by { + assert Random.prob(e) > 0.0 by { assert e == (iset s | UniformPowerOfTwo.Model.Sample(2 * n)(s).0 < n); assert n <= Helper.Power(2, Helper.Log2Floor(2 * n)) by { Helper.NLtPower2Log2FloorOf2N(n); } calc { - Random.Prob(e); + Random.prob(e); == { UniformPowerOfTwo.Correctness.UnifCorrectness2Inequality(2 * n, n); } n as real / (Helper.Power(2, Helper.Log2Floor(2 * n)) as real); > diff --git a/src/Distributions/UniformPowerOfTwo/Correctness.dfy b/src/Distributions/UniformPowerOfTwo/Correctness.dfy index 58905dc1..98f5c3b2 100644 --- a/src/Distributions/UniformPowerOfTwo/Correctness.dfy +++ b/src/Distributions/UniformPowerOfTwo/Correctness.dfy @@ -20,7 +20,7 @@ module UniformPowerOfTwo.Correctness { ghost predicate UnifIsCorrect(n: nat, k: nat, m: nat) requires Helper.Power(2, k) <= n < Helper.Power(2, k + 1) { - Random.Prob(iset s | Model.Sample(n)(s).0 == m) == if m < Helper.Power(2, k) then 1.0 / (Helper.Power(2, k) as real) else 0.0 + Random.prob(iset s | Model.Sample(n)(s).0 == m) == if m < Helper.Power(2, k) then 1.0 / (Helper.Power(2, k) as real) else 0.0 } function Sample1(n: nat): Random.Bitstream -> Random.Bitstream @@ -41,7 +41,7 @@ module UniformPowerOfTwo.Correctness { ensures var e := iset s | Model.Sample(n)(s).0 == m; && e in Random.eventSpace - && Random.Prob(e) == if m < Helper.Power(2, Helper.Log2Floor(n)) then 1.0 / (Helper.Power(2, Helper.Log2Floor(n)) as real) else 0.0 + && Random.prob(e) == if m < Helper.Power(2, Helper.Log2Floor(n)) then 1.0 / (Helper.Power(2, Helper.Log2Floor(n)) as real) else 0.0 { var e := iset s | Model.Sample(n)(s).0 == m; var k := Helper.Log2Floor(n); @@ -69,7 +69,7 @@ module UniformPowerOfTwo.Correctness { ensures var e := iset s | Model.Sample(n)(s).0 < m; && e in Random.eventSpace - && Random.Prob(e) == (m as real) / (Helper.Power(2, Helper.Log2Floor(n)) as real) + && Random.prob(e) == (m as real) / (Helper.Power(2, Helper.Log2Floor(n)) as real) { var e := iset s | Model.Sample(n)(s).0 < m; @@ -91,11 +91,11 @@ module UniformPowerOfTwo.Correctness { Measures.BinaryUnion(Random.eventSpace, Random.sampleSpace, e1, e2); } calc { - Random.Prob(e); + Random.prob(e); { assert e == e1 + e2; } - Random.Prob(e1 + e2); - { assert e1 * e2 == iset{}; Random.ProbIsProbabilityMeasure(); Measures.PosCountAddImpliesAdd(Random.eventSpace, Random.sampleSpace, Random.Prob); assert Measures.IsAdditive(Random.eventSpace, Random.Prob); } - Random.Prob(e1) + Random.Prob(e2); + Random.prob(e1 + e2); + { assert e1 * e2 == iset{}; Random.ProbIsProbabilityMeasure(); Measures.PosCountAddImpliesAdd(Random.eventSpace, Random.sampleSpace, Random.prob); assert Measures.IsAdditive(Random.eventSpace, Random.prob); } + Random.prob(e1) + Random.prob(e2); { UnifCorrectness2(n, m-1); UnifCorrectness2Inequality(n, m-1); } (1.0 / (Helper.Power(2, Helper.Log2Floor(n)) as real)) + (((m-1) as real) / (Helper.Power(2, Helper.Log2Floor(n)) as real)); { Helper.AdditionOfFractions(1.0, (m-1) as real, Helper.Power(2, Helper.Log2Floor(n)) as real); } @@ -130,9 +130,9 @@ module UniformPowerOfTwo.Correctness { } if m < Helper.Power(2, k) { calc { - Random.Prob(iset s | Model.Sample(n)(s).0 == m); + Random.prob(iset s | Model.Sample(n)(s).0 == m); == { SampleRecursiveHalf(n, m); } - Random.Prob(iset s | Model.Sample(n / 2)(s).0 == u) / 2.0; + Random.prob(iset s | Model.Sample(n / 2)(s).0 == u) / 2.0; == { reveal RecursiveCorrect; } (1.0 / Helper.Power(2, k - 1) as real) / 2.0; == { Helper.PowerOfTwoLemma(k - 1); } @@ -141,9 +141,9 @@ module UniformPowerOfTwo.Correctness { assert UnifIsCorrect(n, k, m); } else { calc { - Random.Prob(iset s | Model.Sample(n)(s).0 == m); + Random.prob(iset s | Model.Sample(n)(s).0 == m); == { SampleRecursiveHalf(n, m); } - Random.Prob(iset s | Model.Sample(n / 2)(s).0 == u) / 2.0; + Random.prob(iset s | Model.Sample(n / 2)(s).0 == u) / 2.0; == { reveal RecursiveCorrect; } 0.0 / 2.0; == @@ -182,7 +182,7 @@ module UniformPowerOfTwo.Correctness { lemma SampleIsMeasurePreserving(n: nat) requires n >= 1 - ensures Measures.IsMeasurePreserving(Random.eventSpace, Random.Prob, Random.eventSpace, Random.Prob, Sample1(n)) + ensures Measures.IsMeasurePreserving(Random.eventSpace, Random.prob, Random.eventSpace, Random.prob, Sample1(n)) { var f := Sample1(n); assert Measures.IsMeasurable(Random.eventSpace, Random.eventSpace, f) by { @@ -191,16 +191,16 @@ module UniformPowerOfTwo.Correctness { assert Independence.IsIndep(Model.Sample(n)); } if n == 1 { - forall e | e in Random.eventSpace ensures Random.Prob(Measures.PreImage(f, e)) == Random.Prob(e) { + forall e | e in Random.eventSpace ensures Random.prob(Measures.PreImage(f, e)) == Random.prob(e) { forall s: Random.Bitstream ensures f(s) == s { assert f(s) == s; } Measures.PreImageIdentity(f, e); } - assert Measures.IsMeasurePreserving(Random.eventSpace, Random.Prob, Random.eventSpace, Random.Prob, f); + assert Measures.IsMeasurePreserving(Random.eventSpace, Random.prob, Random.eventSpace, Random.prob, f); } else { var g := Sample1(n / 2); - forall e | e in Random.eventSpace ensures Random.Prob(Measures.PreImage(f, e)) == Random.Prob(e) { + forall e | e in Random.eventSpace ensures Random.prob(Measures.PreImage(f, e)) == Random.prob(e) { var e' := (iset s | Monad.Tail(s) in e); assert e' in Random.eventSpace by { assert e' == Measures.PreImage(Monad.Tail, e); @@ -225,21 +225,21 @@ module UniformPowerOfTwo.Correctness { } Measures.PreImagesEqual(f, e, g, e'); } - assert Random.Prob(Measures.PreImage(f, e)) == Random.Prob(e) by { + assert Random.prob(Measures.PreImage(f, e)) == Random.prob(e) by { calc { - Random.Prob(Measures.PreImage(f, e)); + Random.prob(Measures.PreImage(f, e)); == - Random.Prob(Measures.PreImage(g, e')); - == { SampleIsMeasurePreserving(n / 2); assert Measures.IsMeasurePreserving(Random.eventSpace, Random.Prob, Random.eventSpace, Random.Prob, g); assert e' in Random.eventSpace; } - Random.Prob(e'); + Random.prob(Measures.PreImage(g, e')); + == { SampleIsMeasurePreserving(n / 2); assert Measures.IsMeasurePreserving(Random.eventSpace, Random.prob, Random.eventSpace, Random.prob, g); assert e' in Random.eventSpace; } + Random.prob(e'); == { assert e' == Measures.PreImage(Monad.Tail, e); } - Random.Prob(Measures.PreImage(Monad.Tail, e)); + Random.prob(Measures.PreImage(Monad.Tail, e)); == { Monad.TailIsMeasurePreserving(); } - Random.Prob(e); + Random.prob(e); } } } - assert Measures.IsMeasurePreserving(Random.eventSpace, Random.Prob, Random.eventSpace, Random.Prob, f); + assert Measures.IsMeasurePreserving(Random.eventSpace, Random.prob, Random.eventSpace, Random.prob, f); } } @@ -298,7 +298,7 @@ module UniformPowerOfTwo.Correctness { lemma SampleRecursiveHalf(n: nat, m: nat) requires n >= 2 - ensures Random.Prob(iset s | Model.Sample(n)(s).0 == m) == Random.Prob(iset s | Model.Sample(n / 2)(s).0 == m / 2) / 2.0 + ensures Random.prob(iset s | Model.Sample(n)(s).0 == m) == Random.prob(iset s | Model.Sample(n / 2)(s).0 == m / 2) / 2.0 { var aOf: Random.Bitstream -> nat := (s: Random.Bitstream) => Model.Sample(n / 2)(s).0; var bOf: Random.Bitstream -> bool := (s: Random.Bitstream) => Monad.Coin(Model.Sample(n / 2)(s).1).0; @@ -341,13 +341,13 @@ module UniformPowerOfTwo.Correctness { } } - assert E in Random.eventSpace && Random.Prob(E) == 0.5 by { + assert E in Random.eventSpace && Random.prob(E) == 0.5 by { assert E == (iset s | Monad.Head(s) == (m % 2 == 1)); Monad.CoinHasProbOneHalf(m % 2 == 1); } - assert Indep: Random.Prob(e1 * e2) == Random.Prob(e1) * Random.Prob(e2) by { - assert Measures.AreIndepEvents(Random.eventSpace, Random.Prob, e1, e2) by { + assert Indep: Random.prob(e1 * e2) == Random.prob(e1) * Random.prob(e2) by { + assert Measures.AreIndepEvents(Random.eventSpace, Random.prob, e1, e2) by { assert Independence.IsIndepFunction(Model.Sample(n / 2)) by { assert Independence.IsIndep(Model.Sample(n / 2)) by { SampleIsIndep(n / 2); @@ -360,34 +360,34 @@ module UniformPowerOfTwo.Correctness { Independence.AreIndepEventsConjunctElimination(e1, e2); } - assert ProbE1: Random.Prob(e1) == 0.5 by { + assert ProbE1: Random.prob(e1) == 0.5 by { calc { 0.5; == - Random.Prob(E); + Random.prob(E); == { SampleIsMeasurePreserving(n / 2); } - Random.Prob(Measures.PreImage(f, E)); + Random.prob(Measures.PreImage(f, E)); == { reveal Eq4; } - Random.Prob(e1); + Random.prob(e1); } } calc { - Random.Prob(iset s | Model.Sample(n)(s).0 == m); + Random.prob(iset s | Model.Sample(n)(s).0 == m); == { SampleSetEquality(n, m); } - Random.Prob(e3); + Random.prob(e3); == { reveal SplitEvent; } - Random.Prob(e1 * e2); + Random.prob(e1 * e2); == { reveal Indep; } - Random.Prob(e1) * Random.Prob(e2); - == { reveal ProbE1; Helper.Congruence(Random.Prob(e1), 0.5, x => x * Random.Prob(e2)); } - 0.5 * Random.Prob(e2); + Random.prob(e1) * Random.prob(e2); + == { reveal ProbE1; Helper.Congruence(Random.prob(e1), 0.5, x => x * Random.prob(e2)); } + 0.5 * Random.prob(e2); == - Random.Prob(e2) / 2.0; + Random.prob(e2) / 2.0; == { reveal Eq2; } - Random.Prob(iset s | aOf(s) == m / 2) / 2.0; + Random.prob(iset s | aOf(s) == m / 2) / 2.0; == { reveal Eq3; } - Random.Prob(iset s | Model.Sample(n / 2)(s).0 == m / 2) / 2.0; + Random.prob(iset s | Model.Sample(n / 2)(s).0 == m / 2) / 2.0; } } } diff --git a/src/ProbabilisticProgramming/Independence.dfy b/src/ProbabilisticProgramming/Independence.dfy index e98bc12f..fede19fd 100644 --- a/src/ProbabilisticProgramming/Independence.dfy +++ b/src/ProbabilisticProgramming/Independence.dfy @@ -16,7 +16,7 @@ module Independence { ghost predicate IsIndepFunctionCondition(f: Monad.Hurd, A: iset, E: iset) { var e1 := iset s | f(s).1 in E; var e2 := iset s | f(s).0 in A; - Measures.AreIndepEvents(Random.eventSpace, Random.Prob, e1, e2) + Measures.AreIndepEvents(Random.eventSpace, Random.prob, e1, e2) } // Definition 33 @@ -62,7 +62,7 @@ module Independence { ensures IsIndep(Monad.Bind(f, g)) lemma AreIndepEventsConjunctElimination(e1: iset, e2: iset) - requires Measures.AreIndepEvents(Random.eventSpace, Random.Prob, e1, e2) - ensures Random.Prob(e1 * e2) == Random.Prob(e1) * Random.Prob(e2) + requires Measures.AreIndepEvents(Random.eventSpace, Random.prob, e1, e2) + ensures Random.prob(e1 * e2) == Random.prob(e1) * Random.prob(e2) {} } diff --git a/src/ProbabilisticProgramming/Loops.dfy b/src/ProbabilisticProgramming/Loops.dfy index 7c1e89da..c24e3b5b 100644 --- a/src/ProbabilisticProgramming/Loops.dfy +++ b/src/ProbabilisticProgramming/Loops.dfy @@ -176,8 +176,8 @@ module Loops { && UntilLoopResultHasProperty(proposal, accept, d) in Random.eventSpace && ProposalIsAcceptedAndHasProperty(proposal, accept, d) in Random.eventSpace && ProposalAcceptedEvent(proposal, accept) in Random.eventSpace - && Random.Prob(ProposalAcceptedEvent(proposal, accept)) != 0.0 - && Random.Prob(UntilLoopResultHasProperty(proposal, accept, d)) == Random.Prob(ProposalIsAcceptedAndHasProperty(proposal, accept, d)) / Random.Prob(ProposalAcceptedEvent(proposal, accept)) + && Random.prob(ProposalAcceptedEvent(proposal, accept)) != 0.0 + && Random.prob(UntilLoopResultHasProperty(proposal, accept, d)) == Random.prob(ProposalIsAcceptedAndHasProperty(proposal, accept, d)) / Random.prob(ProposalAcceptedEvent(proposal, accept)) // Equation (3.39) lemma {:axiom} UntilAsBind(proposal: Monad.Hurd, accept: A -> bool, s: Random.Bitstream) diff --git a/src/ProbabilisticProgramming/Monad.dfy b/src/ProbabilisticProgramming/Monad.dfy index 5c72f366..176b91fe 100644 --- a/src/ProbabilisticProgramming/Monad.dfy +++ b/src/ProbabilisticProgramming/Monad.dfy @@ -139,16 +139,16 @@ module Monad { ensures var e := (iset s | Head(s) == b); && e in Random.eventSpace - && Random.Prob(e) == 0.5 + && Random.prob(e) == 0.5 // Equation (2.82) lemma {:axiom} MeasureHeadDrop(n: nat, s: Random.Bitstream) ensures && (iset s | Head(Drop(n, s))) in Random.eventSpace - && Random.Prob(iset s | Head(Drop(n, s))) == 0.5 + && Random.prob(iset s | Head(Drop(n, s))) == 0.5 // Equation (2.78) lemma {:axiom} TailIsMeasurePreserving() - ensures Measures.IsMeasurePreserving(Random.eventSpace, Random.Prob, Random.eventSpace, Random.Prob, Tail) + ensures Measures.IsMeasurePreserving(Random.eventSpace, Random.prob, Random.eventSpace, Random.prob, Tail) } diff --git a/src/ProbabilisticProgramming/Quantifier.dfy b/src/ProbabilisticProgramming/Quantifier.dfy index d1b483c3..a48345e5 100644 --- a/src/ProbabilisticProgramming/Quantifier.dfy +++ b/src/ProbabilisticProgramming/Quantifier.dfy @@ -13,12 +13,12 @@ module Quantifier { ghost predicate AlmostSurely(p: Random.Bitstream -> bool) { var e := iset s | p(s); && e in Random.eventSpace - && Random.Prob(e) == 1.0 + && Random.prob(e) == 1.0 } ghost predicate WithPosProb(p: Random.Bitstream -> bool) { var e := iset s | p(s); && e in Random.eventSpace - && Random.Prob(e) != 0.0 + && Random.prob(e) != 0.0 } } diff --git a/src/ProbabilisticProgramming/RandomSource.dfy b/src/ProbabilisticProgramming/RandomSource.dfy index 7ddc398a..6ce22c54 100644 --- a/src/ProbabilisticProgramming/RandomSource.dfy +++ b/src/ProbabilisticProgramming/RandomSource.dfy @@ -12,18 +12,18 @@ module Random { type Bitstream = s: nat -> bool | IsBitstream(s) witness * - ghost predicate IsBitstream(stream: nat -> bool) + ghost predicate {:axiom} IsBitstream(stream: nat -> bool) ghost const sampleSpace: iset := iset s: Bitstream ghost const eventSpace: iset> - ghost function Prob(event: iset): real + ghost const prob: iset -> real /******* Lemmas *******/ lemma {:axiom} ProbIsProbabilityMeasure() - ensures Measures.IsProbability(eventSpace, sampleSpace, Prob) + ensures Measures.IsProbability(eventSpace, sampleSpace, prob) }