Using pointless Id to help instantiation

Apr 10, 2014 at 7:40 AM
Sometimes something like
assume forall x:: property in x;
assert for all x:: property in x;
fails to verify because (I understand) the universal-instantiation rules won't instantiate x to x; and I do realise there are good reasons for that. But sometimes it's just what I need :-(

I "solve" this problem, for the present, by introducing a function method Id, the identity, and writing
assume forall x:: property in Id(x);
assert for all x:: property in Id(x);
This Id(x) is just complicated enough for Dafny to decide it's worth instantiating x to x.

My question --- is there a better way, involving some kind of "trigger" hint for example?

Thanks!
Coordinator
Sep 9, 2014 at 11:37 PM
It is almost always best to let the tool figure these things out for you. But Dafny does have a hook that lets you indicate the matching trigger manually. You do it using the custom attribute :trigger. Before you start making frequent use (let alone any permanent use) of this feature, consider that in the entire Dafny test suite, there is currently only one use of :trigger (and it was added rather recently, by experts, to improve performance).

Here is an example where :trigger makes a difference:
function f(x: int): int
function g(x: int): int { f(x) }

lemma Example(y: int)
{
  assume forall x {:trigger f(x)} :: x < y ==> g(x) == x;
  assert forall x :: x < y ==> f(x) == x;
}
Without the trigger indication, the assertion would not verify because the assumption would never be instantiated. Rather than using the manual trigger in this case, using an extra lemma (here, in the form of an assertion) does the trick:
  assume forall x :: x < y ==> g(x) == x;
  assert forall x :: f(x) == g(x);  // here is the lemma
  assert forall x :: x < y ==> f(x) == x;
Note that in order to use the :trigger mechanism, you need to have some function symbol (like f or Id) to talk about -- and if there is such a function symbol, then chances are that the automatic triggers will figure it all out for you.

Rustan
Marked as answer by rustanleino on 9/9/2014 at 4:39 PM
Coordinator
Sep 9, 2014 at 11:39 PM
If you care to design a different kind of hook that would be useful to you in these cases, I'd be happy to consider it.

Rustan