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)

  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 powerSumLemma(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)));
        { powerSumLemma(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 powerProductLemma(a: T, m: nat, n: nat)
    requires a in elems
    ensures power(power(a, m), n) == power(a, m*n)
  {
    reveal_power();
    if n == 0 {
      assert m * n == 0;
    }
    else {
      powerProductLemma(a, m, n-1);
      assert power(power(a, m), n-1) == power(a, m*n -m);
      calc {
        power(power(a, m), n);
        compose(power(a, m), power(power(a, m), n-1));
        compose(power(a, m), power(a, m*n-m));
        { powerSumLemma(a, m, m*n-m);}
        power(a, m + m * n -m);
      }
    }
  }

  function generator(): (r: T)
    ensures r in elems
    ensures elems == (set x | 1 <= x <= |elems| :: power(r, x))
    ensures power(r, |elems|) == identity()

}


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_power_lemma(x: T, n: nat)
    requires x in elems && x in sub_elems
    ensures power(x, n) in sub_elems
  {
    reveal_power();
    if n == 0 {
       var r := sub_identity();
    }
    else {
      sub_power_lemma(x, n-1);
      subGroupLemma();
      subComposeLemma(x, power(x, n-1));
    }
  }

  function Minimum(s: set<nat>) : (r: nat)
    requires s != {}
    ensures forall x :: x in s ==> r <= x
    ensures r in s
  {
    var x :| x in s;
    if s == {x} then x
    else
      var y := Minimum(s - {x});
      assert forall z :: z in (s - {x}) ==> y <= z;
      assert s == s - {x} + {x};
      if x < y then x else y
  }

  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 {
        var t : nat :| power(generator(), t) == x;
        sub_power_lemma(generator(), t);
      }
      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 {

      var temp := (set x | 1 <= x <= |elems| && power(generator(), x) in sub_elems);
      assert sub_identity() in sub_elems && identity() in sub_elems;
      var x :| x in temp && 1 <= x <= |elems| && power(generator(), x) == identity();
      var m := Minimum(temp);
      r := power(generator(), m);
      assert m in temp && r in sub_elems && r in elems;
      var s := (set y | 1 <= y <= |sub_elems| :: power(r, y));

      forall y | y in sub_elems ensures y in s {
        subGroupLemma();
        assert y in elems;
        var t :| 1 <= t <= |elems| && power(generator(), t) == y;
        assert t in temp && m <= t;
        assert t % m == 0 && m <= t <= m*|sub_elems| by {
          // TODO
          assume false;
        }
        assert power(generator(), t) in sub_elems;
        assert power(power(generator(), m), t/m) == power(generator(), t) by {
          powerProductLemma(generator(), m, t/m);
        }
        assert power(r, t/m) == power(generator(), t);
      }
      forall y | y in s ensures y in sub_elems {
        var t :| 1 <= t <= |sub_elems| && power(r, t) == y;
        sub_power_lemma(r, t);
        assert y in sub_elems;
      }
      assert s == sub_elems;
    }
  }
}


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))
    ensures power(1, |elems|) == 0
  {
    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))
    ensures power(1, |elems|) == 0
  {
    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
  }
}