Failure of existential introduction

[jtristan]

The following two examples give: Error: A postcondition might not hold on this return path.

	lemma example_failing_1(a: nat)
		ensures exists x: nat :: a == x
	{
		assert a == a;
	}

	lemma example_failing_2()
		ensures forall a: nat :: exists x: nat :: a == x
	{
		forall a: nat {
			assert a == a;
		}
	}	

Note for reference that the following does work:

	datatype Step =
		| Step(n: nat)

	lemma example_working(a: nat)
		ensures forall a: nat :: exists x: nat :: Step(a) == Step(x) 
	{
		assert Step(a) == Step(a); 
	}

Finally, a Coq reference:

Lemma test: forall a: nat, exists x: nat, a = x.
Proof.
  intro a.
  exists a. 
  reflexivity.
Qed.

[RustanLeino]

This issue has to do with how quantifiers are instantiated, see https://github.com/dafny-lang/dafny/wiki/FAQ#how-does-dafny-handle-quantifiers-ive-heard-about-triggers-what-are-those. (More precisely, how universal quantifiers are instantiated and how witnesses for existential quantifiers are found.) Essentially, the a == x expression does have a good matching pattern (aka "trigger"), whereas the expression Step(x) does.

There may be a way to change Dafny's verification-condition generation so that some of these examples would go through automatically. For example, Dafny already is able to verify

var x: nat :| a == x;

whose proof obligation is the same as the postcondition of example_failing_1. (Implementation note: To try this, incorporate some logic in TrSplitExpr in Translator.cs akin the analysis and logic involved in :|.)

There are workarounds to make the examples above verify. Each one involves either manually giving triggers or changing the expressions involved in such a way that Dafny can find triggers for them automatically. Manual triggers are to be used very sparingly, if at all, but they can be effective in examples like those above. Depending on your taste, you may have objections to either workaround. In the following, I will show solutions using both.

ghost function Id<X>(x: X): X { x }

lemma example_failing_1'(a: nat)
  ensures exists x: nat :: a == Id(x) // Dafny picks Id(x) as the matching pattern
{
  assert Id(a) == a; // this occurrence of Id(a) triggers the matching pattern
  assert a == a;
}

ghost predicate LookAtMe<X>(x: X) { true }

lemma example_failing_1''(a: nat)
  ensures exists x: nat {:trigger LookAtMe(x)} :: a == x
{
  assert LookAtMe(a);
  assert a == a;
}

ghost predicate Outer<X>(x: X) { true }
ghost predicate Inner<X>(x: X) { true }

lemma example_failing_2()
  ensures forall a: nat :: Outer(a) ==> exists x: nat :: Inner(x) && a == x
{
  forall a: nat | Outer(a)
    ensures exists x: nat :: Inner(x) && a == x
  {
    assert Inner(a);
    assert a == a;
  }
}

[MikaelMayer]

Also, you don't need to modify the inner part of the exists to prove it, you can also manually set up a trigger like this:

function Trigger<T>(t: T): T { t }

lemma example_failing_1(a: nat)
  ensures exists x: nat {:trigger Trigger(x)}:: a == x
{
  var _ := Trigger(a);
}