-
-
Save hath995/008921599add4c3a1a980c90da9af3c5 to your computer and use it in GitHub Desktop.
Group Theory in Dafny
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
abstract module Group { | |
type T(==) | |
const elems : set<T> | |
function identity(): (r: T) | |
ensures r in elems | |
ensures forall a :: a in elems ==> compose(a, r) == a && compose(r, a) == a | |
function compose(a: T, b: T): (r: T) | |
requires a in elems && b in elems | |
ensures r in elems | |
function inverse(a: T) : (r: T) | |
requires a in elems | |
ensures r in elems | |
ensures compose(a, r) == identity() && compose(r, a) == identity() | |
lemma composeLemma(a: T, b: T, c: T) | |
requires a in elems && b in elems && c in elems | |
ensures compose(a, compose(b, c)) == compose(compose(a, b), c) | |
} | |
abstract module GroupExtras refines Group { | |
function power(a: T, n: int): (r: T) | |
decreases n * n | |
requires a in elems | |
ensures r in elems | |
{ | |
if n == 0 then identity() | |
else if n > 0 then compose(a, power(a, n-1)) | |
else compose(inverse(a), power(a, n+1)) | |
} | |
lemma powerLemma(a: T, n: nat, m: int) | |
requires a in elems | |
ensures compose(power(a, n), power(a, m)) == power(a, n + m) | |
{ | |
if n == 0 {} | |
else { | |
calc { | |
compose(power(a, n), power(a, m)); | |
compose(compose(a, power(a, n-1)), power(a, m)); | |
{ composeLemma(a, power(a, n-1), power(a, m)); } | |
compose(a, compose(power(a, n-1), power(a, m))); | |
{ powerLemma(a, n-1, m); } | |
compose(a, power(a, n + m - 1)); | |
} | |
if n + m > 0 {} | |
else { | |
calc { | |
compose(a, power(a, n + m - 1)); | |
compose(a, compose(inverse(a), power(a, n + m))); | |
{ composeLemma(a, inverse(a), power(a, n + m)); } | |
compose(compose(a, inverse(a)), power(a, n + m)); | |
} | |
} | |
} | |
} | |
lemma {:verify true} groupCompositionInverse(a: T, b: T, abar: T, bbar: T, abbar: T) | |
requires a in elems | |
requires b in elems | |
requires bbar in elems | |
requires abar in elems | |
requires abbar in elems | |
requires inverse(a) == abar | |
requires inverse(b) == bbar | |
requires inverse(compose(a,b)) == abbar | |
ensures abbar == compose(bbar, abar) | |
{ | |
calc { | |
compose(compose(a, b), compose(bbar, abar)); | |
== {composeLemma(a,b,compose(bbar,abar));} | |
compose(a, compose(b, compose(bbar,abar))); | |
== {composeLemma(b,bbar,abar);} | |
compose(a, compose(compose(b, bbar),abar)); | |
compose(a, compose(identity(),abar)); | |
== | |
compose(a, abar); | |
== | |
identity(); | |
} | |
calc { | |
compose(compose(bbar, abar), compose(a, b)); | |
== {composeLemma(bbar,abar,compose(a,b));} | |
compose(bbar, compose(abar, compose(a,b))); | |
== {composeLemma(abar,a,b);} | |
compose(bbar, compose(compose(abar, a),b)); | |
compose(bbar, compose(identity(),b)); | |
== | |
compose(bbar, b); | |
== | |
identity(); | |
} | |
} | |
} | |
module ZMod3 refines GroupExtras { | |
type T = int | |
const elems := {0, 1, 2} | |
function identity ... { 0 } | |
function compose ... { (a + b) % 3 } | |
function inverse ... { (3 - a) % 3 } | |
lemma composeLemma ... | |
{ | |
calc { | |
compose(a, compose(b, c)); | |
(a + b + c) % 3; | |
compose(compose(a, b), c); | |
} | |
} | |
function power ... | |
lemma powerLemma ... | |
lemma testPowerLemma() | |
ensures compose(power(1, 10), power(1, 11)) == power(1, 21) | |
{} | |
} |
Some more progress here over weekend. I am able to state in dafny what we want to prove (// TODOs). Whole file verifies except lemma with TODOs
abstract module Group {
type T(==)
const elems : set<T>
function identity(): (r: T)
ensures r in elems
ensures forall a :: a in elems ==> compose(a, r) == a && compose(r, a) == a
function compose(a: T, b: T): (r: T)
requires a in elems && b in elems
ensures r in elems
function inverse(a: T) : (r: T)
requires a in elems
ensures r in elems
ensures compose(a, r) == identity() && compose(r, a) == identity()
lemma composeLemma(a: T, b: T, c: T)
requires a in elems && b in elems && c in elems
ensures compose(a, compose(b, c)) == compose(compose(a, b), c)
function {:opaque true} power(a: T, n: int): (r: T)
decreases n * n
requires a in elems
ensures r in elems
{
if n == 0 then identity()
else if n > 0 then compose(a, power(a, n-1))
else compose(inverse(a), power(a, n+1))
}
lemma powerLemma(a: T, n: nat, m: nat)
requires a in elems
ensures compose(power(a, n), power(a, m)) == power(a, n + m)
{
reveal_power();
if n == 0 {}
else {
calc {
compose(power(a, n), power(a, m));
compose(compose(a, power(a, n-1)), power(a, m));
{ composeLemma(a, power(a, n-1), power(a, m)); }
compose(a, compose(power(a, n-1), power(a, m)));
{ powerLemma(a, n-1, m); }
compose(a, power(a, n + m - 1));
}
if n + m > 0 {}
else {
calc {
compose(a, power(a, n + m - 1));
compose(a, compose(inverse(a), power(a, n + m)));
{ composeLemma(a, inverse(a), power(a, n + m)); }
compose(compose(a, inverse(a)), power(a, n + m));
}
}
}
}
function generator(): (r: T)
ensures r in elems
ensures elems == (set x | 1 <= x <= |elems| :: power(r, x))
}
abstract module SubGroup refines Group {
const sub_elems: set<T>
lemma subGroupLemma() ensures sub_elems <= elems
function sub_identity(): (r: T)
ensures r in sub_elems
ensures r == identity()
function sub_compose(a: T, b: T): (r: T)
requires a in sub_elems && b in sub_elems
ensures r in sub_elems
function sub_inverse(a: T) : (r: T)
requires a in sub_elems
ensures r in sub_elems
lemma subComposeLemma(a: T, b: T)
requires a in sub_elems && b in sub_elems
requires sub_elems <= elems
ensures sub_compose(a, b) == compose(a, b)
predicate sub_generator_property(r: T)
{
r in sub_elems && r in elems && sub_elems == (set x | 1 <= x <= |sub_elems| :: power(r, x))
}
lemma sub_generator_exists() returns (r: T)
ensures sub_generator_property(r)
{
if generator() in sub_elems {
forall x | x in elems ensures x in sub_elems {
assume x in sub_elems; // TODO
}
subGroupLemma();
assert sub_elems == elems;
assert |elems| == |sub_elems|;
var temp :| temp == generator() &&
temp in elems &&
temp in sub_elems &&
(elems == (set x | 1 <= x <= |elems| :: power(temp, x)));
r := temp;
}
else {
// TODO
assert sub_identity() in sub_elems;
var temp :| temp in sub_elems;
r := temp;
assume false;
}
}
}
module ZMod6 refines Group {
type T = int
const elems := {0, 1, 2, 3, 4, 5}
function identity ... { 0 }
function compose ... { (a + b) % 6 }
function inverse ... { (6 - a) % 6 }
lemma composeLemma ...
{
calc {
compose(a, compose(b, c));
(a + b + c) % 6;
compose(compose(a, b), c);
}
}
lemma generatorLemma()
ensures 1 in elems
ensures elems == (set x | 1 <= x <= |elems| :: power(1, x))
{
assert power(1, 1) == 1 by { reveal_power(); }
assert power(1, 2) == 2 by { reveal_power(); }
assert power(1, 3) == 3 by { reveal_power(); }
assert power(1, 4) == 4 by { reveal_power(); }
assert power(1, 5) == 5 by { reveal_power(); }
assert power(1, 6) == 0 by { reveal_power(); }
assert elems == {0, 1, 2, 3, 4, 5};
assert (set x | 1 <= x <= |elems| :: power(1, x)) == {power(1, 1), power(1, 2), power(1, 3), power(1, 4), power(1, 5), power(1, 6)};
assert {power(1, 1), power(1, 2), power(1, 3), power(1, 4), power(1, 5), power(1, 6)} == {0, 1, 2, 3, 4, 5};
}
function generator ... {
generatorLemma();
1
}
}
module ZMod6SubGroup refines SubGroup {
type T = int
const elems := {0, 1, 2, 3, 4, 5}
const sub_elems := {0, 2, 4};
lemma subGroupLemma ... {}
function identity ... { 0 }
function sub_identity ... { 0 }
function compose ... { (a + b) % 6 }
function sub_compose ... { (a + b) % 6 }
lemma subComposeLemma ... {}
function inverse ... { (6 - a) % 6 }
function sub_inverse ... { (6 - a) % 6 }
lemma composeLemma ...
{
calc {
compose(a, compose(b, c));
(a + b + c) % 6;
compose(compose(a, b), c);
}
}
lemma generatorLemma()
ensures 1 in elems
ensures elems == (set x | 1 <= x <= |elems| :: power(1, x))
{
assert power(1, 1) == 1 by { reveal_power(); }
assert power(1, 2) == 2 by { reveal_power(); }
assert power(1, 3) == 3 by { reveal_power(); }
assert power(1, 4) == 4 by { reveal_power(); }
assert power(1, 5) == 5 by { reveal_power(); }
assert power(1, 6) == 0 by { reveal_power(); }
assert elems == {0, 1, 2, 3, 4, 5};
assert (set x | 1 <= x <= |elems| :: power(1, x)) == {power(1, 1), power(1, 2), power(1, 3), power(1, 4), power(1, 5), power(1, 6)};
assert {power(1, 1), power(1, 2), power(1, 3), power(1, 4), power(1, 5), power(1, 6)} == {0, 1, 2, 3, 4, 5};
}
function generator ... {
generatorLemma();
1
}
}
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Thanks again for your help. I was aware of Lean, however, my goal with all this is to actually prove things about programs. In some software I work on I have an algebraic object which I would like to prove programs about. I am working my way through Artin's Algebra to get used to proving things about groups in Dafny.