@@ -18,7 +18,7 @@ module FisherYates.Correctness {
1818 *******/
1919
2020 lemma CorrectnessFisherYatesUniqueElements< T (!new)> (xs: seq < T> , p: seq < T> )
21- requires forall x | x in xs :: multiset (xs)[x] == 1
21+ requires forall a, b | 0 <= a < b < |xs| :: xs[a] != xs[b]
2222 requires multiset (p) == multiset (xs)
2323 ensures
2424 var e := iset s | Model. Shuffle (xs)(s). Equals (p);
@@ -32,11 +32,25 @@ module FisherYates.Correctness {
3232 CorrectnessFisherYatesUniqueElementsGeneral (xs, p, 0);
3333 }
3434
35+ lemma MultisetOfSequence< T> (xs: seq < T> , i: nat , j: nat )
36+ requires i <= j < |xs|
37+ ensures multiset (xs[i..]) - multiset (xs[i..j]) == multiset (xs[j..])
38+ {
39+ calc {
40+ multiset (xs[i..]) - multiset (xs[i..j]);
41+ { assert xs[i.. ] == xs[i.. j] + xs[j.. ]; }
42+ multiset (xs[i..j] + xs[j..]) - multiset (xs[i..j]);
43+ { assert multiset (xs[i..j] + xs[j..]) == multiset (xs[i..j]) + multiset (xs[j..]); }
44+ multiset (xs[i..j]) + multiset (xs[j..]) - multiset (xs[i..j]);
45+ multiset (xs[j..]);
46+ }
47+ }
48+
3549 lemma CorrectnessFisherYatesUniqueElementsGeneral< T (!new)> (xs: seq < T> , p: seq < T> , i: nat )
3650 decreases |xs| - i
3751 requires i <= |xs|
3852 requires i <= |p|
39- requires forall x | x in xs[i .. ] :: multiset ( xs[i..])[x] == 1
53+ requires forall a, b | i <= a < b < |xs| :: xs[a] != xs[b]
4054 requires multiset (p[i..]) == multiset (xs[i..])
4155 ensures
4256 var e := iset s | Model. Shuffle (xs, i)(s). Result? && Model. Shuffle (xs, i)(s). value[i.. ] == p[i.. ];
@@ -95,23 +109,72 @@ module FisherYates.Correctness {
95109 var ys := Model. Swap (xs, i, j);
96110 var e' := iset s | Model. Shuffle (ys, i+1)(s). Result? && Model. Shuffle (ys, i+1)(s). value[i+ 1.. ] == p[i+ 1.. ];
97111 assert InductionHypothesis: e' in Rand. eventSpace && Rand. prob (e') == 1. 0 / (NatArith. FactorialTraditional (|xs|-(i+1)) as real ) by {
98- assert forall x | x in ys[ i+ 1.. ] :: multiset ( ys[i+1..])[x] == 1 by {
99- forall x | x in ys[ i+ 1.. ]
100- ensures multiset ( ys[i+1..])[x] == 1
112+ assert forall a, b | i+ 1 <= a < b < |ys| :: ys[a] != ys[b] by {
113+ forall a, b | i+ 1 <= a < b < |ys|
114+ ensures ys[a] != ys[b]
101115 {
116+ assume {:axiom} false ;
117+ /* if x == ys[i] {
118+ calc {
119+ multiset(ys[i+1..])[x];
120+ multiset(ys[i..])[x] - multiset([ys[i]])(x);
121+ multiset(ys[i..])[x] - 1;
122+
123+ }
124+ }
125+
102126 calc {
103127 1;
104128 <= { assert x in ys[i+1..]; }
105129 multiset(ys[i+1..])[x];
106130 }
107131 calc {
108132 multiset(ys[i+1..])[x];
109- <= { assert multiset (ys[i+1..]) <= multiset (ys[i..]); }
110- multiset (ys[i..])[x];
111- == { assert multiset (ys[i..]) == multiset (xs[i..]); }
112- multiset (xs[i..])[x];
113- ==
114- 1;
133+ ==
134+ (multiset(ys) - multiset(ys[..i]))[x];
135+ ==
136+ multiset(ys)[x] - multiset(ys[..i])[x];
137+ ==
138+ multiset(xs)[x] - multiset(xs[..i])[x];
139+ == { }
140+ 1 - multiset(ys[..i])[x];
141+ <=
142+ 1
143+ } */
144+ }
145+ }
146+ assert multiset (ys[i+1..]) == multiset (p[i+1..]) by {
147+ if j == i {
148+ calc {
149+ multiset (ys[i+1..]);
150+ { assert ys[i+ 1.. ] == xs[i+ 1.. ] by { assert xs == ys; } }
151+ multiset (xs[i+1..]);
152+ { MultisetOfSequence (xs, i, i+1); }
153+ multiset (xs[i..]) - multiset (xs[i..i+1]);
154+ { assert xs[i.. i+ 1] == [xs[i]]; }
155+ multiset (xs[i..]) - multiset ([xs[i]]);
156+ { assert multiset (xs[i..]) == multiset (p[i..]); assert xs[i] == xs[j] by { assert i == j; } }
157+ multiset (p[i..]) - multiset ([xs[j]]);
158+ { assert xs[j] == p[i]; }
159+ multiset (p[i..]) - multiset ([p[i]]);
160+ { assert [p[i]] == p[i.. i+ 1]; }
161+ multiset (p[i..]) - multiset (p[i..i+1]);
162+ { MultisetOfSequence (p, i, i+1); }
163+ multiset (p[i+1..]);
164+ }
165+ } else {
166+ calc {
167+ multiset (ys[i+1..]);
168+ { assert ys[i+ 1.. ] == ys[i+ 1.. j] + [ys[j]] + ys[j+ 1.. ]; }
169+ multiset (ys[i+1..j] + [ys[j]] + ys[j+1..]);
170+ { assume {:axiom} false ; assert ys[i+ 1.. j] == xs[i+ 1.. j]; assert ys[j] == xs[i]; assert ys[j+ 1.. ] == xs[j+ 1.. ]; }
171+ multiset (xs[i+1..j] + [xs[i]] + xs[j+1..]);
172+ { assume {:axiom} false ; }
173+ multiset (xs[i..]) - multiset ([xs[j]]);
174+ { assume {:axiom} false ; assert multiset (xs[i..]) == multiset (p[i..]); assert xs[j] == p[i]; }
175+ multiset (p[i..]) - multiset (p[i..i+1]);
176+ { MultisetOfSequence (p, i, i+1); }
177+ multiset (p[i+1..]);
115178 }
116179 }
117180 }
@@ -121,39 +184,39 @@ module FisherYates.Correctness {
121184 assume {:axiom} false ;
122185 }
123186 assert Rand. prob (e) == 1. 0 / (NatArith. FactorialTraditional (|xs|-i) as real ) by {
124- /* calc {
125- Rand.prob(e);
126- { reveal DecomposeE; }
127- Rand.prob(Monad.BitstreamsWithValueIn(h, A) * Monad.BitstreamsWithRestIn(h, e'));
128- { reveal HIsIndependent; reveal InductionHypothesis; Independence.ResultsIndependent(h, A, e'); }
129- Rand.prob(Monad.BitstreamsWithValueIn(h, A)) * Rand.prob(e');
130- { assert Rand.prob(Monad.BitstreamsWithValueIn(h, A)) == Rand.prob(iset s | Uniform.Model.IntervalSample(i, |xs|)(s).Equals(j)) by { reveal BitStreamsInA; } }
131- Rand.prob(iset s | Uniform.Model.IntervalSample(i, |xs|)(s).Equals(j)) * Rand.prob(e');
132- { assert Rand.prob(iset s | Uniform.Model.IntervalSample(i, |xs|)(s).Equals(j)) == (1.0 / ((|xs|-i) as real)) by { Uniform.Correctness.UniformFullIntervalCorrectness(i, |xs|, j); } }
133- (1.0 / ((|xs|-i) as real)) * Rand.prob(e');
134- { assert Rand.prob(e') == (1.0 / (NatArith.FactorialTraditional(|xs|-(i+1)) as real)) by { reveal InductionHypothesis; } }
135- (1.0 / ((|xs|-i) as real)) * (1.0 / (NatArith.FactorialTraditional(|xs|-(i+1)) as real));
136- { assert |xs|-(i+1) == |xs|-i-1; }
137- (1.0 / ((|xs|-i) as real)) * (1.0 / (NatArith.FactorialTraditional((|xs|-i)-1) as real));
138- //{ RealArith.SimplifyFractionsMultiplication(1.0, (|xs|-i) as real, 1.0, NatArith.Factorial((|xs|-i)-1) as real); }
139- { assume {:axiom} false; }
140- (1.0 * 1.0) / (((|xs|-i) as real) * (NatArith.FactorialTraditional((|xs|-i)-1) as real));
141- { assume {:axiom} false; assert 1.0 * 1.0 == 1.0; assert ((|xs|-i) as real) * (NatArith.FactorialTraditional((|xs|-i)-1) as real) == ((|xs|-i) * NatArith.FactorialTraditional((|xs|-i)-1)) as real; }
142- 1.0 / (((|xs|-i) * NatArith.FactorialTraditional((|xs|-i)-1)) as real);
143- { assume {:axiom} false; assert (|xs|-i) * NatArith.FactorialTraditional((|xs|-i)-1) == NatArith.FactorialTraditional(|xs|-i) by { reveal NatArith.FactorialTraditional(); } }
144- 1.0 / (NatArith.FactorialTraditional(|xs|-i) as real);
145- } */
187+ /* calc {
188+ Rand.prob(e);
189+ { reveal DecomposeE; }
190+ Rand.prob(Monad.BitstreamsWithValueIn(h, A) * Monad.BitstreamsWithRestIn(h, e'));
191+ { reveal HIsIndependent; reveal InductionHypothesis; Independence.ResultsIndependent(h, A, e'); }
192+ Rand.prob(Monad.BitstreamsWithValueIn(h, A)) * Rand.prob(e');
193+ { assert Rand.prob(Monad.BitstreamsWithValueIn(h, A)) == Rand.prob(iset s | Uniform.Model.IntervalSample(i, |xs|)(s).Equals(j)) by { reveal BitStreamsInA; } }
194+ Rand.prob(iset s | Uniform.Model.IntervalSample(i, |xs|)(s).Equals(j)) * Rand.prob(e');
195+ { assert Rand.prob(iset s | Uniform.Model.IntervalSample(i, |xs|)(s).Equals(j)) == (1.0 / ((|xs|-i) as real)) by { Uniform.Correctness.UniformFullIntervalCorrectness(i, |xs|, j); } }
196+ (1.0 / ((|xs|-i) as real)) * Rand.prob(e');
197+ { assert Rand.prob(e') == (1.0 / (NatArith.FactorialTraditional(|xs|-(i+1)) as real)) by { reveal InductionHypothesis; } }
198+ (1.0 / ((|xs|-i) as real)) * (1.0 / (NatArith.FactorialTraditional(|xs|-(i+1)) as real));
199+ { assert |xs|-(i+1) == |xs|-i-1; }
200+ (1.0 / ((|xs|-i) as real)) * (1.0 / (NatArith.FactorialTraditional((|xs|-i)-1) as real));
201+ //{ RealArith.SimplifyFractionsMultiplication(1.0, (|xs|-i) as real, 1.0, NatArith.Factorial((|xs|-i)-1) as real); }
202+ { assume {:axiom} false; }
203+ (1.0 * 1.0) / (((|xs|-i) as real) * (NatArith.FactorialTraditional((|xs|-i)-1) as real));
204+ { assume {:axiom} false; assert 1.0 * 1.0 == 1.0; assert ((|xs|-i) as real) * (NatArith.FactorialTraditional((|xs|-i)-1) as real) == ((|xs|-i) * NatArith.FactorialTraditional((|xs|-i)-1)) as real; }
205+ 1.0 / (((|xs|-i) * NatArith.FactorialTraditional((|xs|-i)-1)) as real);
206+ { assume {:axiom} false; assert (|xs|-i) * NatArith.FactorialTraditional((|xs|-i)-1) == NatArith.FactorialTraditional(|xs|-i) by { reveal NatArith.FactorialTraditional(); } }
207+ 1.0 / (NatArith.FactorialTraditional(|xs|-i) as real);
208+ } */
146209 assume {:axiom} false ;
147210 }
148211 assert e in Rand. eventSpace by {
149212 assume {:axiom} false ;
150- /* reveal DecomposeE;
151- reveal HIsIndependent;
152- reveal InductionHypothesis;
153- assert Independence.IsIndepFunctionCondition(h, A, e');
154- assert Monad.BitstreamsWithValueIn(h, A) in Rand.eventSpace;
155- assert Monad.BitstreamsWithRestIn(h, e') in Rand.eventSpace;
156- Measures.BinaryUnionIsMeasurable(Rand.eventSpace, Monad.BitstreamsWithValueIn(h, A), Monad.BitstreamsWithRestIn(h, e')); */
213+ /* reveal DecomposeE;
214+ reveal HIsIndependent;
215+ reveal InductionHypothesis;
216+ assert Independence.IsIndepFunctionCondition(h, A, e');
217+ assert Monad.BitstreamsWithValueIn(h, A) in Rand.eventSpace;
218+ assert Monad.BitstreamsWithRestIn(h, e') in Rand.eventSpace;
219+ Measures.BinaryUnionIsMeasurable(Rand.eventSpace, Monad.BitstreamsWithValueIn(h, A), Monad.BitstreamsWithRestIn(h, e')); */
157220 }
158221 }
159222 }
0 commit comments