Exists Statement

[dreamqin68]

Hello,

The predicate is intended to check if a natural number exists within the range [0, length).

predicate existsNat(length:nat)
{
    if length == 0 then true
    else
        exists a :nat :: 0<= a <length
}

Could anyone help me understand why assert existsNat(length) is not verifying correctly?

Thank you for your time and assistance!

[stefan-aws]

Please provide a minimal failing example. Which version of Dafny are you using? Where do you use assert existsNat(length)? Thanks!

[dreamqin68]

I use Dafny 4.6.0.

I think this predicate is always true. But the below lemma is failed.

lemma theoremExistsNat(length:nat)
    ensures existsNat(length)
{
    assert existsNat(length);
}

[racko]

1. Help the verifier by asserting that some value (which you have to manually specify) actually satisifies the predicate 0 <= a <length. E.g. by assert 0 <= 0 < length; Since the predicate is not trivial enough, this still fails to verify because the verifier can't "connect" this assertion with the exists expression. The warning "Could not find a trigger for this quantifier." hints at this. So you also need to
2. Name the predicate¹. E.g. var p := x => 0 <= x < length; assert p(0); exists a: nat :: p(a). Now the verifier is able to proof that such a value exists, but there is a new error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce or compile a bounded set of values for 'a'. So you need to
3. Specify bounds for a: exists a: nat | 0 <= a < length :: p(a).

Now theoremExistsNat verifies.

Here's the final result:

predicate existsNat(length: nat)
{
    if length == 0 then
        true
    else
        var p := x => 0 <= x < length;
        assert p(0);
        exists a: nat | 0 <= a < length :: p(a)
}

lemma theoremExistsNat(length: nat)
    ensures existsNat(length)
{
    assert existsNat(length);
}

Footnotes

1. See https://github.com/dafny-lang/dafny/discussions/5374#discussioncomment-9244228 ↩

[dreamqin68]

Thanks a lot!