Skip to content

Commit

Permalink
fix
Browse files Browse the repository at this point in the history
  • Loading branch information
@fzaiser
fzaiser committed Oct 13, 2023
1 parent 68928fd commit 5f74b4f
Show file tree
Hide file tree
Showing 10 changed files with 79 additions and 79 deletions.
18 changes: 9 additions & 9 deletions src/Distributions/Bernoulli/Correctness.dfy
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;

Expand All @@ -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;
Expand All @@ -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);
}

Expand All @@ -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; }
Expand Down
2 changes: 1 addition & 1 deletion src/Distributions/BernoulliExpNeg/Correctness.dfy
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
28 changes: 14 additions & 14 deletions src/Distributions/Uniform/Correctness.dfy
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;

Expand All @@ -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) {
Expand All @@ -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); }
Expand All @@ -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 {
Expand All @@ -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); }
Expand All @@ -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);
}
Expand All @@ -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 {
Expand Down
4 changes: 2 additions & 2 deletions src/Distributions/Uniform/Model.dfy
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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);
>
Expand Down
80 changes: 40 additions & 40 deletions src/Distributions/UniformPowerOfTwo/Correctness.dfy
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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);
Expand Down Expand Up @@ -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;

Expand All @@ -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); }
Expand Down Expand Up @@ -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); }
Expand All @@ -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;
==
Expand Down Expand Up @@ -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 {
Expand All @@ -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);
Expand All @@ -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);
}
}

Expand Down Expand Up @@ -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;
Expand Down Expand Up @@ -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);
Expand All @@ -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;
}
}
}
6 changes: 3 additions & 3 deletions src/ProbabilisticProgramming/Independence.dfy
View file
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,7 @@ module Independence {
ghost predicate IsIndepFunctionCondition<A(!new)>(f: Monad.Hurd<A>, A: iset<A>, E: iset<Random.Bitstream>) {
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
Expand Down Expand Up @@ -62,7 +62,7 @@ module Independence {
ensures IsIndep(Monad.Bind(f, g))

lemma AreIndepEventsConjunctElimination(e1: iset<Random.Bitstream>, e2: iset<Random.Bitstream>)
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)
{}
}
4 changes: 2 additions & 2 deletions src/ProbabilisticProgramming/Loops.dfy
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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<A(!new)>(proposal: Monad.Hurd<A>, accept: A -> bool, s: Random.Bitstream)
Expand Down
Loading

0 comments on commit 5f74b4f

Please sign in to comment.