Group Theory in Dafny

group.dfy

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 need one more lemma to prove it

lemma InverseLemma(a: T, b: T)
    requires a in elems && b in elems
    requires compose(a, b) == identity()
    requires compose(b, a) == identity()
    ensures a == inverse(b) && b == inverse(a)
  {
     var x := inverse(b);
     calc {
         compose(compose(a, b), x);
         {
           composeLemma(a, b, x);
         }
         compose(a, compose(b, x));
         compose(a, identity());
         a;
     }
     var y := inverse(a);
     calc {
         compose(compose(b, a), y);
         {
           composeLemma(b, a, y);
         }
         compose(b, compose(a, y));
         compose(b, identity());
         b;
      }
  }

I see, thank you. I will continue to develop the module representation. How would you recommend expanding on it to add additional properties. For example, previously I had:

predicate commutativeComposition<A>(g: Group<A>) {
    forall a,b :: a in g.elements && b in g.elements ==> g.compose(a,b) == g.compose(b,a)
}

predicate ValidSubGroup<A>(g: Group<A>, h: Group<A>) {
      h.elements <= g.elements &&
      g.identity in h.elements &&
      g.identity == h.identity &&
      g.compose == h.compose &&
      closedComposition(h) //&&
      // containsInverses(h)
  }

predicate AbelianGroup<A>(g: Group<A>) {
    ValidGroup(g) && commutativeComposition(g)
}

Because group was a data structure, it required just creating another parameter or by asserting that some value existed that I could show that every value matched a predicate.

What I'm really getting at is how to describe extensionality of modules. Here is an example of something I'm trying to prove.

    predicate CyclicGroupGeneratedBy<A(!new)>(g: Group, elem: A)
        requires elem in g.elements
    {
        exists n :: n == |g.elements| &&
            apow(g, elem, n) == g.identity &&
            (forall ns :: ns != n && apow(g, elem, ns) == g.identity ==> n < ns) &&
            n != 0 &&
            forall x :: x in g.elements && exists n :: apow(g, elem, n) == x
    }

    lemma {:verify false} AllSubgroupsOfCyclicSubgroupsAreCyclic<A(!new)>(g: Group, elem: A, h:Group)
        requires elem in g.elements
        requires CyclicGroupGeneratedBy(g, elem)
        requires ValidGroup(g)
        requires h.elements <= g.elements
        requires ValidGroup(h)
        requires ValidSubGroup(g, h)
        ensures exists hx: A :: hx in h.elements && CyclicGroupGeneratedBy(h, hx)
    {

    }

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.

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
  }
}