Skip to content

Commit aadb2ea

Browse files
stefan-awsstefan-aws
committed
skeleton
1 parent e1bdf43 commit aadb2ea

File tree

4 files changed

+371
-226
lines changed

4 files changed

+371
-226
lines changed

‎audit.log

Lines changed: 5 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -28,6 +28,9 @@ src/Math/Exponential.dfy(61,17): Increasing: Declaration has explicit `{:axiom}`
2828
src/Math/Exponential.dfy(65,17): EvalOne: Declaration has explicit `{:axiom}` attribute.
2929
src/Math/Measures.dfy(125,17): ProbabilityLe1: Declaration has explicit `{:axiom}` attribute.
3030
src/Math/Measures.dfy(130,17): IsMonotonic: Declaration has explicit `{:axiom}` attribute.
31+
src/Math/Permutations.dfy(224,4): PermutationsPreserveCardinality: Definition has `assume {:axiom}` statement in body.
32+
src/Math/Permutations.dfy(87,17): CorrectnessOfNumberOfPermutationsOf: Declaration has explicit `{:axiom}` attribute.
33+
src/Math/Permutations.dfy(87,53): type parameter T of ghost lemma CorrectnessOfNumberOfPermutationsOf is declared (==), which is unnecessary because the lemma doesn't contain any compiled code
3134
src/ProbabilisticProgramming/Independence.dfy(105,17): BindIsIndep: Declaration has explicit `{:axiom}` attribute.
3235
src/ProbabilisticProgramming/Independence.dfy(30,27): IsIndep: Declaration has explicit `{:axiom}` attribute.
3336
src/ProbabilisticProgramming/Independence.dfy(55,6): ResultsIndependent: Definition has `assume {:axiom}` statement in body.
@@ -46,10 +49,5 @@ src/ProbabilisticProgramming/RandomSource.dfy(50,17): ProbIsProbabilityMeasure:
4649
src/ProbabilisticProgramming/RandomSource.dfy(54,17): CoinHasProbOneHalf: Declaration has explicit `{:axiom}` attribute.
4750
src/ProbabilisticProgramming/RandomSource.dfy(61,17): MeasureHeadDrop: Declaration has explicit `{:axiom}` attribute.
4851
src/ProbabilisticProgramming/RandomSource.dfy(67,17): TailIsMeasurePreserving: Declaration has explicit `{:axiom}` attribute.
49-
src/Util/FisherYates/Correctness.dfy(102,6): CorrectnessFisherYatesGeneral: Definition has `assume {:axiom}` statement in body.
50-
src/Util/FisherYates/Correctness.dfy(163,8): CorrectnessMultiset: Definition has `assume {:axiom}` statement in body.
51-
src/Util/FisherYates/Correctness.dfy(192,12): CorrectnessMultiset: Definition has `assume {:axiom}` statement in body.
52-
src/Util/FisherYates/Correctness.dfy(200,10): CorrectnessMultiset: Definition has `assume {:axiom}` statement in body.
53-
src/Util/FisherYates/Correctness.dfy(215,12): CorrectnessMultiset: Definition has `assume {:axiom}` statement in body.
54-
src/Util/FisherYates/Correctness.dfy(245,12): CorrectnessMultiset: Definition has `assume {:axiom}` statement in body.
55-
src/Util/FisherYates/Correctness.dfy(96,8): CorrectnessFisherYatesGeneral: Definition has `assume {:axiom}` statement in body.
52+
src/Util/FisherYates/Correctness.dfy(112,17): CorrectnessMultiset: Declaration has explicit `{:axiom}` attribute.
53+
src/Util/FisherYates/Correctness.dfy(34,17): CorrectnessFisherYatesGeneral: Declaration has explicit `{:axiom}` attribute.

‎src/Math/Permutations.dfy

Lines changed: 179 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -6,12 +6,34 @@
66
module Permutations {
77
import NatArith
88

9+
/*************************************************************************************
10+
* Defines the notion of a permutation and establishes that the formula
11+
* `NumberOfPermutationsOf` is correct, in the sense that:
12+
* - NumberOfPermutationsOf(s) == |CalculateAllPermutationsOf(s)|
13+
* - (iset p | p in CalculateAllPermutationsOf(s)) == iset p | IsPermutationOf(p, s)
14+
*************************************************************************************/
15+
916
/************
1017
Definitions
1118
************/
1219

13-
function NumberOfPermutationsOf<T(==)>(s: seq<T>): nat {
14-
|CalculateAllPermutationsOf(s)|
20+
predicate IsPermutationOf<T(==)>(p: seq<T>, s: seq<T>) {
21+
multiset(p) == multiset(s)
22+
}
23+
24+
function NumberOfPermutationsOf<T(==)>(s: seq<T>): (n: nat)
25+
ensures n != 0
26+
{
27+
if |s| <= 1 then
28+
1
29+
else
30+
var multiplicity := multiset(s)[s[0]];
31+
var length := |s|;
32+
(length / multiplicity) * NumberOfPermutationsOf(s[1..])
33+
}
34+
35+
ghost function AllPermutationsOf<T(!new)>(s: seq<T>): iset<seq<T>> {
36+
iset p | IsPermutationOf(p, s)
1537
}
1638

1739
function CalculateAllPermutationsOf<T(==)>(s: seq<T>): (x: set<seq<T>>)
@@ -23,16 +45,48 @@ module Permutations {
2345
set p, i | p in CalculateAllPermutationsOf(s[1..]) && 0 <= i <= |s|-1 :: InsertAt(p, s[0], i)
2446
}
2547

48+
function DeleteAt<T>(s: seq<T>, i: nat): seq<T>
49+
requires i < |s|
50+
{
51+
s[..i] + s[i+1..]
52+
}
53+
2654
function InsertAt<T>(s: seq<T>, x: T, i: nat): seq<T>
2755
requires i <= |s|
2856
{
2957
s[..i] + [x] + s[i..]
3058
}
3159

60+
function FirstOccurrence<T(==)>(p: seq<T>, x: T): (i: nat)
61+
requires x in multiset(p)
62+
ensures i < |p|
63+
ensures p[i] == x
64+
{
65+
if p[0] == x then
66+
0
67+
else
68+
FirstOccurrence(p[1..], x) + 1
69+
}
70+
71+
function Swap<T>(s: seq<T>, i: nat, j: nat): (t: seq<T>)
72+
requires i <= j
73+
requires 0 <= i < |s|
74+
requires 0 <= j < |s|
75+
ensures |s| == |t|
76+
{
77+
if i == j then
78+
s
79+
else
80+
s[..i] + [s[j]] + s[i+1..j] + [s[i]] + s[j+1..]
81+
}
82+
3283
/*******
3384
Lemmas
3485
*******/
3586

87+
lemma {:axiom} CorrectnessOfNumberOfPermutationsOf<T(==)>(s: seq<T>)
88+
ensures NumberOfPermutationsOf(s) == |CalculateAllPermutationsOf(s)|
89+
3690
lemma CalculateAllPermutationsOfIsNonEmpty<T>(s: seq<T>)
3791
ensures s in CalculateAllPermutationsOf(s)
3892
ensures NumberOfPermutationsOf(s) > 0
@@ -47,4 +101,127 @@ module Permutations {
47101
}
48102
}
49103
}
104+
105+
lemma CorrectnessOfCalculateAllPermutationsOf<T(!new)>(s: seq<T>)
106+
ensures (iset p | p in CalculateAllPermutationsOf(s)) == AllPermutationsOf(s)
107+
{
108+
assert (iset p | p in CalculateAllPermutationsOf(s)) == AllPermutationsOf(s) by {
109+
assert forall p :: p in CalculateAllPermutationsOf(s) <==> p in AllPermutationsOf(s) by {
110+
forall p
111+
ensures p in CalculateAllPermutationsOf(s) <==> p in AllPermutationsOf(s)
112+
{
113+
CorrectnessOfCalculateAllPermutationsOfImplicationOne(s, p);
114+
CorrectnessOfCalculateAllPermutationsOfImplicationTwo(s, p);
115+
}
116+
}
117+
}
118+
}
119+
120+
lemma CorrectnessOfCalculateAllPermutationsOfImplicationOne<T(!new)>(s: seq<T>, p: seq<T>)
121+
ensures p in CalculateAllPermutationsOf(s) ==> p in AllPermutationsOf(s)
122+
{
123+
if |s| == 0 {
124+
// induction base, no proof hints needed
125+
} else {
126+
// induction step
127+
if p in CalculateAllPermutationsOf(s) {
128+
assert p in AllPermutationsOf(s) by {
129+
assert IsPermutationOf(p, s) by {
130+
var p', i :| p' in CalculateAllPermutationsOf(s[1..]) && 0 <= i <= |p'| && p == InsertAt(p', s[0], i);
131+
calc == {
132+
multiset(p);
133+
multiset(InsertAt(p', s[0], i));
134+
{ MultisetAfterInsertAt(p', s[0], i); }
135+
multiset([s[0]]) + multiset(p');
136+
{ CorrectnessOfCalculateAllPermutationsOfImplicationOne(s[1..], p'); } // induction hypothesis
137+
multiset([s[0]]) + multiset(s[1..]);
138+
multiset([s[0]] + s[1..]);
139+
{ assert [s[0]] + s[1..] == s; }
140+
multiset(s);
141+
}
142+
}
143+
}
144+
}
145+
}
146+
}
147+
148+
lemma CorrectnessOfCalculateAllPermutationsOfImplicationTwo<T(!new)>(s: seq<T>, p: seq<T>)
149+
ensures p in CalculateAllPermutationsOf(s) <== p in AllPermutationsOf(s)
150+
{
151+
if |s| == 0 {
152+
// induction base, no proof hints needed
153+
} else {
154+
// induction step
155+
if p in AllPermutationsOf(s) {
156+
assert p in CalculateAllPermutationsOf(s) by {
157+
var i := FirstOccurrence(p, s[0]);
158+
var p' := DeleteAt(p, i);
159+
assert p' in CalculateAllPermutationsOf(s[1..]) by {
160+
assert p' in AllPermutationsOf(s[1..]) by {
161+
PermutationBeforeAndAfterDeletionAt(p, s, i, 0);
162+
}
163+
CorrectnessOfCalculateAllPermutationsOfImplicationTwo(s[1..], p'); // induction hypothesis
164+
}
165+
assert p == InsertAt(p', s[0], i) by {
166+
InsertAfterDeleteAt(p, i);
167+
}
168+
}
169+
}
170+
}
171+
}
172+
173+
lemma MultisetAfterInsertAt<T>(s: seq<T>, x: T, i: nat)
174+
requires i <= |s|
175+
ensures multiset(InsertAt(s, x, i)) == multiset([x]) + multiset(s)
176+
{
177+
calc == {
178+
multiset(InsertAt(s, x, i));
179+
multiset(s[..i] + [x] + s[i..]);
180+
multiset(s[..i]) + multiset([x]) + multiset(s[i..]);
181+
multiset([x]) + multiset(s[..i]) + multiset(s[i..]);
182+
multiset([x]) + multiset(s[..i] + s[i..]);
183+
{ assert s[..i] + s[i..] == s; }
184+
multiset([x]) + multiset(s);
185+
}
186+
}
187+
188+
lemma PermutationBeforeAndAfterDeletionAt<T>(p: seq<T>, s: seq<T>, i: nat, j: nat)
189+
requires IsPermutationOf(p, s)
190+
requires i < |p|
191+
requires j < |s|
192+
requires p[i] == s[j]
193+
ensures IsPermutationOf(DeleteAt(p, i), DeleteAt(s, j))
194+
{
195+
assert IsPermutationOf(DeleteAt(p, i), DeleteAt(s, j)) by {
196+
calc == {
197+
multiset(DeleteAt(p, i));
198+
multiset(p[..i] + p[i+1..]);
199+
multiset(p[..i]) + multiset(p[i+1..]);
200+
multiset(p[..i]) + multiset([p[i]]) + multiset(p[i+1..]) - multiset([p[i]]);
201+
multiset(p[..i] + [p[i]] + p[i+1..]) - multiset([p[i]]);
202+
{ assert p[..i] + [p[i]] + p[i+1..] == p; }
203+
multiset(p) - multiset([p[i]]);
204+
multiset(s) - multiset([s[j]]);
205+
{ assert s[..j] + [s[j]] + s[j+1..] == s; }
206+
multiset(s[..j] + [s[j]] + s[j+1..]) - multiset([s[j]]);
207+
multiset(s[..j]) + multiset([s[j]]) + multiset(s[j+1..]) - multiset([s[j]]);
208+
multiset(s[..j]) + multiset(s[j+1..]);
209+
multiset(s[..j] + s[j+1..]);
210+
multiset(DeleteAt(s, j));
211+
}
212+
}
213+
}
214+
215+
lemma InsertAfterDeleteAt<T>(s: seq<T>, i: nat)
216+
requires i < |s|
217+
ensures s == InsertAt(DeleteAt(s, i), s[i], i)
218+
{}
219+
220+
lemma PermutationsPreserveCardinality<T>(p: seq<T>, s: seq<T>)
221+
requires multiset(p) == multiset(s)
222+
ensures |p| == |s|
223+
{
224+
assume {:axiom} false;
225+
}
226+
50227
}

0 commit comments

Comments
 (0)