`ensures exists x :: OpaquePredicate(x)` always needs triggers

[xtrm0]

Currently we need to explicitly define a trigger for exists x :: OpaquePredicate(x) and the trigger is not learned by asserting the statement. Ideally it would be nice for the trigger to be automatically generated, but in the meantime, a warning saying calling the lemma ThereIsAPositiveNumber has no effect would be nice.

module M1 {
  predicate {:opaque} Positive(x: int) {
    x > 0
  }
  predicate ExistsPositive() {
    (exists x: int :: Positive(x))
  }

  lemma ThereIsAPositiveNumber()
  ensures (exists x: int :: Positive(x))
  {
    var y : int := 1;
    reveal Positive();
    assert Positive(y);
    assert (exists x: int :: Positive(x));
  }

  lemma ThereIsAPositiveNumberReturnsTrigger()
  ensures ExistsPositive()
  {
    var y : int := 1;
    reveal Positive();
    assert Positive(y);
    assert (exists x: int :: Positive(x));
  }

  lemma NotWorking()
   ensures true
  {
    ThereIsAPositiveNumber();
    assert (exists x: int :: Positive(x)); // assertion violation
  }

  lemma NotWorking2()
  ensures true
  {
    assert (exists x: int :: Positive(x)) by // assertion violation
    {
      ThereIsAPositiveNumber();
    }
  } 

  lemma NotWorking3()
  ensures true
  {
    assert ExistsPositive() by // assertion violation
    {
      ThereIsAPositiveNumber();
    }
  } 

  lemma Working()
   ensures true
  {
    ThereIsAPositiveNumberReturnsTrigger();
    assert (exists x: int :: Positive(x));
  }

  lemma Working2()
  ensures true
  {
    assert (exists x: int :: Positive(x)) by 
    {
      ThereIsAPositiveNumberReturnsTrigger();
    }
  } 

  lemma Working3()
  ensures true
  {
    assert ExistsPositive() by 
    {
      ThereIsAPositiveNumberReturnsTrigger();
    }
    assert (exists x: int :: Positive(x));
  } 

  lemma NotWorking4()
  ensures true
  {
    assert (exists x: int :: Positive(x)) by 
    {
      ThereIsAPositiveNumberReturnsTrigger();
    }
    assert (exists x: int :: Positive(x)); // assertion violation
  }
}

[cpitclaudel]

I don't think this is a trigger issue: we do generate triggers for existentials (in your case, the trigger ends up being Positive(x)). I think a summarized version of your issue is the following failing code:

predicate {:opaque} PREDICATE(x: int)

method test() {
  assume exists VARIABLE : int :: PREDICATE(VARIABLE);
  assert exists VARIABLE : int :: PREDICATE(VARIABLE);
}

The problem is at the boogie level. Without the opaque qualifier, you get the following, which Boogie proves easily:

    assume (exists VARIABLE#1: int :: 
      { _module.__default.PREDICATE(VARIABLE#1) } 
      _module.__default.PREDICATE(VARIABLE#1));
    assert (exists VARIABLE#3: int :: 
      { _module.__default.PREDICATE(VARIABLE#3) } 
      _module.__default.PREDICATE(VARIABLE#3));

But with the opaque qualifier you get a different encoding:

    assume (exists VARIABLE#1: int :: 
      { _module.__default.PREDICATE(StartFuelAssert__module._default.PREDICATE, VARIABLE#1) } 
      _module.__default.PREDICATE(StartFuelAssert__module._default.PREDICATE, VARIABLE#1));
    assert (exists VARIABLE#3: int :: 
      { _module.__default.PREDICATE(StartFuel__module._default.PREDICATE, VARIABLE#3) } 
      _module.__default.PREDICATE(StartFuel__module._default.PREDICATE, VARIABLE#3));

I don't know why the encoding changes.

[MikaelMayer]

Thanks @cpitclaudel, thus, this is the same bug as this one https://github.com/dafny-lang/dafny/issues/1631