Dafny存在语句导致慢?

Question

apowAddition在我对有效群论代数的定义中注释掉containsInverses(g)时验证，但当我取消注释时，它无法验证，超时死亡。我可以猜测，Dafny正在尝试生成与定义匹配的元素。然而，既然我没有在证明中使用那个性质或者确保它被引理排除为什么它会在证明中引起问题?

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

编辑2:将右逆添加到isInverse中可以快速验证groupcompostioninverse，但apoaddition再次无休止地验证。编辑3:添加apowClosed(g, element, n+k)到apowAddition修复了这一切!

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

这个公理对于基于触发器的量词实例化是有问题的。触发器是一种涉及量化变量的语法模式，它作为求解器对量词执行某些操作的启发式方法。使用forall量词，触发器告诉Dafny何时用其他表达式实例化量化公式。否则，Dafny将永远不会使用量化公式。

触发器的工作方式是每当有一个表达式在语法上与触发器中的模式匹配时，Dafny就为该表达式创建forall主体的副本。

所讨论的公理是:

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

如果你将鼠标悬停在forall上，你可以看到Dafny正在使用什么触发器。对于forall，触发器是:

x in g.elements

这是一个问题，因为forall的主体生成了一个新的表达式，该表达式也匹配外部触发器(xbar in g.elements)。这意味着每当Dafny实例化外部触发器时，它将创建一个以前从未见过的新表达式，该表达式也匹配外部触发器，这将导致另一个实例化，该实例化将生成另一个新表达式，导致另一个实例化，以此类推，直到永远。

有几种方法可以解决这个问题。一种方法是人为地收紧外部forall的触发器，使其只能手动实例化，如下所示:

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
}

我们引入一个虚拟函数PleaseInstantiateMe，它的唯一目的是作为一个模式，我们可以告诉Dafny等待，直到它实例化触发器。在这个版本中，取消ValidGroup中的containsInverses注释会导致apowAddition的即时证明。缺点是无论何时想要使用containsInverses，都必须手动输入

assert PleaseInstantiateMe(whatever);

，其中whatever是你想让Dafny知道它有逆的群元素。这可能很乏味。

另一种更适合您的具体情况的方法是将群逆公理化为从A到A的函数。然后，当你写出关于该函数的公理时，你可以使用该函数本身作为触发器。

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

我尝试了这个方法，但它似乎仍然超时。看起来你的其他公理也有触发问题。Dafny推断出了像x in g.elements这样极具攻击性的触发器，这很可能导致无限匹配循环。如果你需要更多的帮助，请告诉我。