Skip to content

Commit 453c6b9

Browse files
stefan-awsstefan-aws
committed
InductionHypothesisPrecondition1
1 parent f7ece57 commit 453c6b9

File tree

2 files changed

+76
-64
lines changed

2 files changed

+76
-64
lines changed

‎audit.log

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -48,5 +48,5 @@ src/ProbabilisticProgramming/RandomSource.dfy(61,17): MeasureHeadDrop: Declarati
4848
src/ProbabilisticProgramming/RandomSource.dfy(67,17): TailIsMeasurePreserving: Declaration has explicit `{:axiom}` attribute.
4949
src/Util/FisherYates/Correctness.dfy(104,8): CorrectnessFisherYatesUniqueElementsGeneral: Definition has `assume {:axiom}` statement in body.
5050
src/Util/FisherYates/Correctness.dfy(113,12): CorrectnessFisherYatesUniqueElementsGeneral: Definition has `assume {:axiom}` statement in body.
51-
src/Util/FisherYates/Correctness.dfy(208,8): CorrectnessFisherYatesUniqueElementsGeneral: Definition has `assume {:axiom}` statement in body.
52-
src/Util/FisherYates/Correctness.dfy(218,8): CorrectnessFisherYatesUniqueElementsGeneral: Definition has `assume {:axiom}` statement in body.
51+
src/Util/FisherYates/Correctness.dfy(147,8): CorrectnessFisherYatesUniqueElementsGeneral: Definition has `assume {:axiom}` statement in body.
52+
src/Util/FisherYates/Correctness.dfy(157,8): CorrectnessFisherYatesUniqueElementsGeneral: Definition has `assume {:axiom}` statement in body.

‎src/Util/FisherYates/Correctness.dfy

Lines changed: 74 additions & 62 deletions
Original file line numberDiff line numberDiff line change
@@ -140,68 +140,7 @@ module FisherYates.Correctness {
140140
} */
141141
}
142142
}
143-
assert multiset(ys[i+1..]) == multiset(p[i+1..]) by {
144-
if j == i {
145-
calc {
146-
multiset(ys[i+1..]);
147-
{ assert ys[i+1..] == xs[i+1..] by { assert xs == ys; } }
148-
multiset(xs[i+1..]);
149-
{ MultisetOfSequence(xs, i, i+1); }
150-
multiset(xs[i..]) - multiset(xs[i..i+1]);
151-
{ assert xs[i..i+1] == [xs[i]]; }
152-
multiset(xs[i..]) - multiset([xs[i]]);
153-
{ assert multiset(xs[i..]) == multiset(p[i..]); assert xs[i] == xs[j] by { assert i == j; } }
154-
multiset(p[i..]) - multiset([xs[j]]);
155-
{ assert multiset([xs[j]]) == multiset([p[i]]) by { assert j in A; assert xs[j] == p[i]; } }
156-
multiset(p[i..]) - multiset([p[i]]);
157-
{ assert multiset([p[i]]) == multiset(p[i..i+1]) by { assert [p[i]] == p[i..i+1]; } }
158-
multiset(p[i..]) - multiset(p[i..i+1]);
159-
{ assert |p| == |xs|; MultisetOfSequence(p, i, i+1); }
160-
multiset(p[i+1..]);
161-
}
162-
} else {
163-
assert i+1 <= j by {
164-
assert i <= j;
165-
assert i != j;
166-
assert i < j;
167-
}
168-
assert |xs| > j;
169-
assert |xs| == |ys|;
170-
calc {
171-
multiset(ys[i+1..]);
172-
{ assert i+1 <= j; assert ys[i+1..] == ys[i+1..j] + ys[j..]; }
173-
multiset(ys[i+1..j] + ys[j..]);
174-
{ assert ys[j..] == [ys[j]] + ys[j+1..]; }
175-
multiset(ys[i+1..j] + [ys[j]] + ys[j+1..]);
176-
{ assert ys[i+1..j] == xs[i+1..j];}
177-
multiset(xs[i+1..j] + [ys[j]] + ys[j+1..]);
178-
{ assert ys[j] == xs[i]; }
179-
multiset(xs[i+1..j] + [xs[i]] + ys[j+1..]);
180-
{ assert ys[j+1..] == xs[j+1..]; }
181-
multiset(xs[i+1..j] + [xs[i]] + xs[j+1..]);
182-
{ assert multiset([xs[j]]) - multiset([xs[j]]) == multiset{}; }
183-
multiset(xs[i+1..j] + [xs[i]] + xs[j+1..]) + multiset([xs[j]]) - multiset([xs[j]]);
184-
{ assert multiset(xs[i+1..j] + [xs[i]] + xs[j+1..]) + multiset([xs[j]]) == multiset(xs[i+1..j] + [xs[i]] + xs[j+1..] + [xs[j]]); }
185-
multiset(xs[i+1..j] + [xs[i]] + xs[j+1..] + [xs[j]]) - multiset([xs[j]]);
186-
{ assert multiset(xs[i+1..j] + [xs[i]] + xs[j+1..] + [xs[j]]) == multiset(xs[i+1..j]) + multiset([xs[i]]) + multiset(xs[j+1..]) + multiset([xs[j]]); }
187-
multiset(xs[i+1..j]) + multiset([xs[i]]) + multiset(xs[j+1..]) + multiset([xs[j]]) - multiset([xs[j]]);
188-
{ assert multiset(xs[i+1..j]) + multiset([xs[i]]) + multiset(xs[j+1..]) + multiset([xs[j]]) == multiset([xs[i]]) + multiset(xs[i+1..j]) + multiset([xs[j]]) + multiset(xs[j+1..]); }
189-
multiset([xs[i]]) + multiset(xs[i+1..j]) + multiset([xs[j]]) + multiset(xs[j+1..]) - multiset([xs[j]]);
190-
{ assert multiset([xs[i]]) + multiset(xs[i+1..j]) + multiset([xs[j]]) + multiset(xs[j+1..]) == multiset([xs[i]] + xs[i+1..j] + [xs[j]] + xs[j+1..]); }
191-
multiset([xs[i]] + xs[i+1..j] + [xs[j]] + xs[j+1..]) - multiset([xs[j]]);
192-
{ assert [xs[i]] + xs[i+1..j] == xs[i..j]; assert [xs[j]] + xs[j+1..] == xs[j..]; }
193-
multiset(xs[i..j] + xs[j..]) - multiset([xs[j]]);
194-
{ assert xs[i..j] + xs[j..] == xs[i..]; }
195-
multiset(xs[i..]) - multiset([xs[j]]);
196-
{ assert multiset(xs[i..]) == multiset(p[i..]); assert j in A; assert xs[j] == p[i]; }
197-
multiset(p[i..]) - multiset([p[i]]);
198-
{ assert [p[i]] == p[i..i+1]; }
199-
multiset(p[i..]) - multiset(p[i..i+1]);
200-
{ assert |p| == |xs|; MultisetOfSequence(p, i, i+1); }
201-
multiset(p[i+1..]);
202-
}
203-
}
204-
}
143+
InductionHypothesisPrecondition1(xs, ys, p, i, j);
205144
CorrectnessFisherYatesUniqueElementsGeneral(ys, p, i+1);
206145
}
207146
assert DecomposeE: e == Monad.BitstreamsWithValueIn(h, A) * Monad.BitstreamsWithRestIn(h, e') by {
@@ -227,6 +166,79 @@ module FisherYates.Correctness {
227166
}
228167
}
229168

169+
lemma InductionHypothesisPrecondition1<T(!new)>(xs: seq<T>, ys: seq<T>, p: seq<T>, i: nat, j: nat)
170+
requires i <= |xs|
171+
requires i <= |p|
172+
requires forall a, b | i <= a < b < |xs| :: xs[a] != xs[b]
173+
requires |xs| == |p|
174+
requires multiset(p[i..]) == multiset(xs[i..])
175+
requires i <= j < |xs| && xs[j] == p[i]
176+
requires ys == Model.Swap(xs, i, j)
177+
requires |xs[i..]| > 1
178+
ensures multiset(ys[i+1..]) == multiset(p[i+1..])
179+
{
180+
if j == i {
181+
calc {
182+
multiset(ys[i+1..]);
183+
{ assert ys[i+1..] == xs[i+1..] by { assert xs == ys; } }
184+
multiset(xs[i+1..]);
185+
{ MultisetOfSequence(xs, i, i+1); }
186+
multiset(xs[i..]) - multiset(xs[i..i+1]);
187+
{ assert xs[i..i+1] == [xs[i]]; }
188+
multiset(xs[i..]) - multiset([xs[i]]);
189+
{ assert multiset(xs[i..]) == multiset(p[i..]); assert xs[i] == xs[j] by { assert i == j; } }
190+
multiset(p[i..]) - multiset([xs[j]]);
191+
{ assert multiset([xs[j]]) == multiset([p[i]]) by { assert xs[j] == p[i]; } }
192+
multiset(p[i..]) - multiset([p[i]]);
193+
{ assert multiset([p[i]]) == multiset(p[i..i+1]) by { assert [p[i]] == p[i..i+1]; } }
194+
multiset(p[i..]) - multiset(p[i..i+1]);
195+
{ assert |p| == |xs|; MultisetOfSequence(p, i, i+1); }
196+
multiset(p[i+1..]);
197+
}
198+
} else {
199+
assert i+1 <= j by {
200+
assert i <= j;
201+
assert i != j;
202+
assert i < j;
203+
}
204+
assert |xs| > j;
205+
assert |xs| == |ys|;
206+
calc {
207+
multiset(ys[i+1..]);
208+
{ assert i+1 <= j; assert ys[i+1..] == ys[i+1..j] + ys[j..]; }
209+
multiset(ys[i+1..j] + ys[j..]);
210+
{ assert ys[j..] == [ys[j]] + ys[j+1..]; }
211+
multiset(ys[i+1..j] + [ys[j]] + ys[j+1..]);
212+
{ assert ys[i+1..j] == xs[i+1..j];}
213+
multiset(xs[i+1..j] + [ys[j]] + ys[j+1..]);
214+
{ assert ys[j] == xs[i]; }
215+
multiset(xs[i+1..j] + [xs[i]] + ys[j+1..]);
216+
{ assert ys[j+1..] == xs[j+1..]; }
217+
multiset(xs[i+1..j] + [xs[i]] + xs[j+1..]);
218+
{ assert multiset([xs[j]]) - multiset([xs[j]]) == multiset{}; }
219+
multiset(xs[i+1..j] + [xs[i]] + xs[j+1..]) + multiset([xs[j]]) - multiset([xs[j]]);
220+
{ assert multiset(xs[i+1..j] + [xs[i]] + xs[j+1..]) + multiset([xs[j]]) == multiset(xs[i+1..j] + [xs[i]] + xs[j+1..] + [xs[j]]); }
221+
multiset(xs[i+1..j] + [xs[i]] + xs[j+1..] + [xs[j]]) - multiset([xs[j]]);
222+
{ assert multiset(xs[i+1..j] + [xs[i]] + xs[j+1..] + [xs[j]]) == multiset(xs[i+1..j]) + multiset([xs[i]]) + multiset(xs[j+1..]) + multiset([xs[j]]); }
223+
multiset(xs[i+1..j]) + multiset([xs[i]]) + multiset(xs[j+1..]) + multiset([xs[j]]) - multiset([xs[j]]);
224+
{ assert multiset(xs[i+1..j]) + multiset([xs[i]]) + multiset(xs[j+1..]) + multiset([xs[j]]) == multiset([xs[i]]) + multiset(xs[i+1..j]) + multiset([xs[j]]) + multiset(xs[j+1..]); }
225+
multiset([xs[i]]) + multiset(xs[i+1..j]) + multiset([xs[j]]) + multiset(xs[j+1..]) - multiset([xs[j]]);
226+
{ assert multiset([xs[i]]) + multiset(xs[i+1..j]) + multiset([xs[j]]) + multiset(xs[j+1..]) == multiset([xs[i]] + xs[i+1..j] + [xs[j]] + xs[j+1..]); }
227+
multiset([xs[i]] + xs[i+1..j] + [xs[j]] + xs[j+1..]) - multiset([xs[j]]);
228+
{ assert [xs[i]] + xs[i+1..j] == xs[i..j]; assert [xs[j]] + xs[j+1..] == xs[j..]; }
229+
multiset(xs[i..j] + xs[j..]) - multiset([xs[j]]);
230+
{ assert xs[i..j] + xs[j..] == xs[i..]; }
231+
multiset(xs[i..]) - multiset([xs[j]]);
232+
{ assert multiset(xs[i..]) == multiset(p[i..]); assert xs[j] == p[i]; }
233+
multiset(p[i..]) - multiset([p[i]]);
234+
{ assert [p[i]] == p[i..i+1]; }
235+
multiset(p[i..]) - multiset(p[i..i+1]);
236+
{ assert |p| == |xs|; MultisetOfSequence(p, i, i+1); }
237+
multiset(p[i+1..]);
238+
}
239+
}
240+
}
241+
230242
lemma ProbabilityOfE<T(!new)>(xs: seq<T>, p: seq<T>, i: nat, j: nat, h: Monad.Hurd<int>, A: iset<int>, e: iset<Rand.Bitstream>, e': iset<Rand.Bitstream>)
231243
requires i <= |xs|
232244
requires i <= |p|

0 commit comments

Comments
 (0)