为何Dafny无法验证seq<nat>中最小元素的存在性？

核心原因 #

Dafny的自动定理证明器无法直接验证这个断言，本质有两点：

1. 该结论依赖自然数的良序性——每个非空自然数子集都存在最小元素，但这个性质不是Dafny默认会自动调用的公理，需要显式触发。
2. 原代码仅直接抛出存在性断言，未提供任何推导逻辑，Dafny无法凭空完成这种需要归纳或公理应用的证明。

解决方案：显式提供证明逻辑 #

有两种常用方式完成这个引理的验证：

方式1：基于序列长度的结构归纳

通过递归拆分序列，利用子序列的最小值推导整体最小值：

lemma min_exists(xs: seq<nat>)
    requires |xs| > 0
    ensures exists min :: min in xs && forall x :: x in xs ==> min <= x
{
    if |xs| == 1 {
        let min := xs[0];
        assert min in xs;
        assert forall x :: x in xs ==> min <= x;
    } else {
        let head := xs[0];
        let tail := xs[1..];
        min_exists(tail);
        var tail_min :| tail_min in tail && forall x in tail :: tail_min <= x;
        let min := if head <= tail_min then head else tail_min;
        assert min in xs;
        assert forall x in xs :: min <= x;
    }
}

逻辑说明：

• 基础情况：单元素序列的唯一元素就是最小值，直接验证。
• 递归情况：将序列拆分为头元素和非空尾部，先证明尾部存在最小值，再比较头元素和尾部最小值，取较小值作为整个序列的最小值。

方式2：利用自然数良序性的反证法

通过构造矛盾来证明存在性：

lemma min_exists(xs: seq<nat>)
    requires |xs| > 0
{
    var min :| min in xs && forall x in xs :: min <= x by {
        // 先确认序列非空，存在至少一个元素
        assert exists m: nat :: m in xs;
        var m :| m in xs;
        // 假设不存在最小元素，可构造无限递减的自然数序列
        var n := m;
        while n in xs {
            var k :| k in xs && k < n; // 无最小元素则必有更小的元素
            n := k;
        }
        // 自然数无法无限递减，循环不可能终止，矛盾
    }
}

逻辑说明：
假设序列不存在最小元素，那么从任意元素出发，总能找到更小的元素，这会生成无限递减的自然数序列——但自然数是良序的，不存在这样的序列，因此假设不成立，原断言为真。

内容的提问来源于stack exchange，提问作者Germán Ferrero