dafny

Why Dafny can't verify the existence of a minimum element in seq<nat>

Why Dafny can't verify this lemma:

lemma min_exists(xs: seq<nat>)
    requires |xs| > 0
{
    assert exists min :: min in xs && forall x :: x in xs ==> min <= x;
}
Solution

  • This is covered by the following paper. Basically, there are many mathematical facts that seem obvious but must be shown to the Dafny compiler.

    https://leino.science/papers/krml275.html