Dafny existence statement cause slowness?

Question

apowAddition verifies when I comment out containsInverses(g) in my definition of a valid group theory algebra, but when I uncomment it fails to verify, death by timeout. I can guess that Dafny is trying to generate elements that exist to match the definition. However, since I'm not using that property in the proof or ensuring it is discharged by the lemma why is it causing problems in the proof?

datatype Group<!A> = Group(elements: set<A>, identity: A, compose: (A,A) -> A)

predicate ValidGroup<A>(g: Group<A>) {
    g.identity in g.elements &&
    isIdentity(g) &&
    closedComposition(g) &&
    associativeComposition(g) //&& 
    // containsInverses(g)
}
function apow<A>(g: Group, elem: A, n: nat): A 
    requires elem in g.elements
{
    if n == 0 then g.identity else g.compose(elem, apow(g, elem, n-1))
}


lemma {:verify true} apowAddition<A>(g: Group<A>, elem: A, n: nat, k: nat)
    requires elem in g.elements
    requires ValidGroup(g)
    ensures g.compose(apow(g, elem, n), apow(g, elem, k)) == apow(g, elem, n+k)
{
    apowClosed(g, elem, n);
    apowClosed(g, elem, k);
    if k == 0 {
        assert apow(g, elem, k) == g.identity;
        assert g.compose(apow(g, elem, n), g.identity) == apow(g, elem, n+0);
    }else if n == 0 {
        assert apow(g, elem, n) == g.identity;
        assert g.compose(g.identity, apow(g, elem, k)) == apow(g, elem, k+0);
    }else{
        apowClosed(g, elem, n-1);
        apowClosed(g, elem, n+k);
        calc {
            g.compose(apow(g, elem, n), apow(g, elem, k));
            g.compose(g.compose(elem, apow(g, elem, n-1)), apow(g, elem, k));
            g.compose(elem, g.compose(apow(g, elem, n-1), apow(g, elem, k)));
            == {apowAddition(g,elem, n-1,k);}
            g.compose(elem, apow(g, elem, n-1+k));
            apow(g, elem, n+k);
        }
    }
}

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

predicate closedComposition<A>(g: Group<A>) {
    forall x,y :: x in g.elements && y in g.elements ==> g.compose(x,y) in g.elements
}

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

predicate containsInverses<A>(g: Group<A>) {
    forall x :: x in g.elements ==> exists xbar :: xbar in g.elements && g.compose(x,xbar) == g.identity
}

lemma apowClosed<A>(g: Group, elem: A, n: nat)
    requires elem in g.elements
    requires g.identity in g.elements
    requires isIdentity(g)
    requires closedComposition(g)
    ensures apow(g,elem, n) in g.elements
{}

Edit 2: Adding the right inverse to isInverse verifies groupCompositionInverse quickly, but apowAddition again endlessly verifies. Edit 3: Adding apowClosed(g, elem, n+k) to apowAddition fixes it all!

predicate isInverse<A>(g: Group<A>) {
  forall x {:trigger g.inverse(x)} :: x in g.elements ==> g.compose(x,g.inverse(x)) == g.identity && g.compose(g.inverse(x),x) == g.identity
}
lemma {:verify true} groupCompositionInverse<A>(g: Group<A>, a: A, b: A, abar: A, bbar: A, abbar: A)
    requires ValidGroup(g)
    requires a in g.elements
    requires b in g.elements
    // requires containsInverses(g)
    // requires abar in g.elements
    // requires bbar in g.elements
    // requires abbar in g.elements
    requires g.inverse(a) == abar
    requires g.inverse(b) == bbar
    requires g.inverse(g.compose(a,b)) == abbar
    // requires g.compose(a, abar) == g.identity
    // requires g.compose(b, bbar) == g.identity
    // requires g.compose(g.compose(a, b), abbar) == g.identity
    ensures abbar == g.compose(bbar, abar)
{
    calc {
        g.compose(g.compose(a, b), g.compose(bbar, abar));
        ==
        g.compose(a, g.compose(g.compose(b, bbar),abar));
        ==
        g.compose(a, g.compose(g.identity,abar));
        ==
        g.compose(a, abar);
        ==
        g.identity;
    }
}

Answer 1

That axiom is problematic for trigger-based quantifier instantiation. A trigger is a syntactic pattern involving quantified variables that serves as heuristic for the solver to do something with the quantifier. With a forall quantifier, the trigger tells Dafny when to instantiate the quantified formula with other expressions. Otherwise, Dafny will never use the quantified formula.

The way a trigger works is whenever there is an expression that syntactically matches the pattern in the trigger, Dafny creates a copy of the body of the forall for that expression.

The axiom in question is:

forall x :: 
  x in g.elements ==> 
  exists xbar :: 
    xbar in g.elements && 
    g.compose(x,xbar) == g.identity

If you hover your mouse over the forall, you can see what triggers Dafny is using. For the forall, the trigger is:

x in g.elements

This is a problem because the body of the forall generates a new expression that also matches the outer trigger (xbar in g.elements). That means that whenever Dafny instantiates the outer trigger, it will create a new expression that has never been seen before that also matches the outer trigger, which will cause another instantiation, which will generate another new expression, causing another instantiation, and so on forever.

There are several ways to fix this. One would be to artificially tighten the trigger on the outer forall so that it can only get instantiated manually, like this:

predicate PleaseInstantiateMe<A>(x: A) {
    true
}

predicate containsInverses<A>(g: Group<A>) {
  forall x {:trigger PleaseInstantiateMe(x)} :: 
    PleaseInstantiateMe(x) && x in g.elements ==> 
    exists xbar :: 
      xbar in g.elements && g.compose(x,xbar) == g.identity
}

We introduce a dummy function PleaseInstantiateMe whose only purpose is to be a pattern we can tell Dafny to wait for until it instantiates the trigger. In this version, uncommenting containsInverses in ValidGroup leads to an instant proof of apowAddition. The downside is that whenever you want to use containsInverses, you will have to manually say

assert PleaseInstantiateMe(whatever);

where whatever is the group element you want Dafny to realize has an inverse. This can be tedious.

An alternative approach that is more tailored to your specific situation would be to instead axiomatize group inverses as a function from A to A. Then when you write the axiom about that function, you could use that function itself as the trigger.

predicate closedInverse<A>(g: Group<A>) {
  forall x {:trigger g.inverse(x)} :: x in g.elements ==> g.inverse(x) in g.elements
}

predicate isInverse<A>(g: Group<A>) {
  forall x {:trigger g.inverse(x)} :: x in g.elements ==> g.compose(x,g.inverse(x)) == g.identity
}

predicate ValidGroup<A>(g: Group<A>) {
    g.identity in g.elements &&
    isIdentity(g) &&
    closedComposition(g) &&
    associativeComposition(g) &&
    closedInverse(g) &&
    isInverse(g)
}

I tried this approach and it still seemed to timeout. It looks like you also have some trigger problems with your other axioms. Dafny is inferring extremely aggressive triggers like x in g.elements, which is very likely to cause an infinite matching loop. Let me know if you want more help pursuing this approach.