Trivial assertion might not hold

[Marti2203]

Dafny version: 3.5.0
Hello, I am currently a tutor for a course where we use Dafny and I was shown a very strange piece of code which should work but does not.
code:

method test(){
    var b:=1;
    assert exists a | 0<= a <2 :: a == b;
}

expected result: Assertion should be satisfied and not saying that it might not hold.

How to understand why Dafny does not accept this?

[fabiomadge]

As the warning suggests, Dafny is unable to select a trigger for the existential quantifier. Look here for a little more context.
Here's a version that works:

predicate InRange(i: int) {
    0 <= i < 2
}

method Main() {
    var b := 1;
    assert InRange(b);
    assert exists a | InRange(a) :: a == b;
}

[RustanLeino]

What I mentioned here as "looking at the structure of the body of the quantifier" is achieved using something that's called matching patterns, also known as triggers. Here is some addition information about triggers. However, I strongly suggest not writing your own triggers--instead, using a trick like the one @fabiomadge showed here, namely to introduce some predicate or function that makes the body of the quantifier "less bland".

[RustanLeino]

Finally, to reiterate what @fabiomadge said about the "no trigger" warning. This warning indicates that the the verifier might not be able to use the quantifier (or other comprehension) effectively. Indeed, that is the case for @Marti2203 's example.
Oh, and a good reminder to mention here is that every error message that the Dafny verifier gives says that the verifier failed to prove what needed to be proved. The condition to be proved may still hold (as is the case here), but the verifier was unable to prove it.

[Marti2203]

Hello Mr. Leino,
Thank you for the explanation! This is nice to know, I know about triggers but I did not work too much with them. I think it should be mentioned in the FAQ or somewhere else that the operators you mentioned are not usable as triggers, I have had this issue a couple of times and it is not very obvious for an undergrad student.

[mathprocessing]

Hello Mr. Leino.

Example above can be simplified:

// Without some fix
method Main()
{
  assert exists a :: a == 0; // Fails
}

// With some fix
method Main()
{
  assert exists a :: a == 0; // Verified
}

I think that exists must work "equally" to forall: in all cases where forall works exists must work.

Perhaps this feature helps to view this problem of exists quantifier from another hand:

Possible feature:
if assert can return information symmetrical to false/true state:
This means that assert expr; can be simplified to assert true; or assert false; or simplification fails:

Statement	Message	Counterexamples
assert true;	no message	No
assert false;	dafny proved assert !expr	Yes
assert undertermined;	assert may not hold	Yes

This creates new problem: Dafny must check all asserts twice (1. for true 2. for false).
To reduce amount of computation in already existing projects (user can update Dafny and realize that time of proving in new version of Dafny is twice as long and it's leads to possible bad user experience) this feature requires adding another option to Dafny /checkFalseCase or something like that.

How this feature helps?

• This just about symmetries, logic states to which prover must reacts equally.
• Equally reaction for some thing in future can simplify behaviour (and testing) of whole system.
• And just to think about: How to prove P1 that some proof P2 is must have concrete set of properties S.
  Last question (may only for me) is really hard.

Also exist way working in Dafny without this feature:

predicate P();

method test_proving_of_true()
{
  assert P();
}

method test_proving_of_false()
{
  assert !P();
}

But this leads to bad user experience and begger code base.

What do you think about it Mr. Leino?

Why it's not possible?

[MikaelMayer]

Let me ask you some questions and give some hints to clarify.

1. Can you please elaborate on the example you give, by providing something the contexts that makes the assertion actually fails and succeeds in different contexts?
2. I wasn't able to find a discrepancy between exists and forall even by tweaking the examples you gave. Please elaborate on that
3. Assertions can't be simplified to true/false.
4. I do get your point that, whenever we have assert expr;, if it fails, we could try to prove assert !expr; to see if it's always false. But in practice, this is not useful. Most of the time, expr is almost correct, it's just that it misses assumptions.
   Note that expr is not a closed expression, and it has variables, so every assert is already "For all free variables that satisfy the program assumptions at this given point, do this expression holds", which is a forall statement. So if you wanted to prove the negation of it, that is a wholly different problem. you could have counter-examples for either and that wouldn't bring any useful information.
   For example:

method f(x: int) {
  assert x > 0; // Fails, counter-example -1
}
method f2(x: int) {
  assert !(x > 0); // Fails, counter-example 0
}