如何从存在子句中提取变量

Question

我正在尝试用 Dafny 简单地简化为荒谬的证明，通常当我这样做时（在现实生活中的数学中）我使用诸如“好吧，现在让我们选择一个 p 来满足我们知道存在的这个属性，因为 [... ]”，然后继续使用该 p 进行其余的演示。我正在尝试用 Dafny 复制这种形式的推理，但我不知道如何从“exists”子句中“提取”变量 p。希望你能帮助我！

if(exists p | ini <= p < border <= fin :: is_true_on_segment(s, p, fin, P)){
                    closed_on_left_lemma(P);
                    upper_limit(s, ini, fin - 1, P);

                    assert exists p | ini <= p < border <= fin :: is_true_on_segment(s, p, fin - 1, P);

                    assert false;
                }

这似乎是一个标准的数学过程，所以我希望有一种方法可以做到。我尝试搜索文档和“程序证明”一书，但没有成功。

Answer 1

语法是

var p :| ini <= p < border <= fin && is_true_on_segment(s, p, fin - 1, P);

这会将满足这些谓词的变量

p

带入范围。