-
-
Save hath995/008921599add4c3a1a980c90da9af3c5 to your computer and use it in GitHub Desktop.
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) | |
{} | |
} |
You can define cyclic group and abelian group this way. I am not sure how much you can push dafny for verifying mathematics, it was developed for verifying functional and object oriented languages (For example I am not happy with my modeling of subgroup. It has lots of repetition) . If you are looking for better language for verifying mathematics take a look at lean. Here is group modeled in lean https://github.com/leanprover-community/mathlib/tree/master/src/algebra/group
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 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))
}
}
abstract module AbelianGroup refines Group {
lemma abelianLemma(a: T, b: T)
requires a in elems && b in elems
ensures compose(a, b) == compose(b, a)
}
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)
}
abstract module cyclicGroup refines Group {
function generator(): (r: T)
ensures r in elems
ensures power(r, |elems|) == identity()
ensures elems == (set x | 1 <= x <= |elems| :: power(r, x))
ensures forall x :: power(r, x) == identity() ==> x >= |elems|
}
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.
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
}
}
The proof of AllSubgroupsOfCyclicSubgroupsAreCyclic goes something like the following. Let$G$ be a group and $H$ be a cyclic subgroup of $G$ generated by $x$ and let $H_2$ be a subgroup of $H$ .
If$x$ in $H_2$ then $H_2 = H$ by the closure of composition. If we assume $x$ is not in $H_2$ and we pick some $y \in H_2$ then by definition $y = x^k$ for some $k$ and we pick another element $z=x^l \in H_2$ either $x^l = x^{k c}$ for some $c$ for all other elements in $H_2$ implying it is cyclic or $\gcd(k,l) = 1$ which implies there exists $s,t \in \mathbb{Z}$ such that $s k + t l = 1$ and therefore $x^{s k + t l}=x^1$ which means the generator for H is in H_2 implying H_2 == H and is cyclic.