fstar - FStar 中的简单断言问题

Question

我刚开始学习FStar。我想表达一个事实，即每一个自然数都存在一个更大的数。

let _ = assert (forall (m:nat). exists (n: nat). n > m)

它失败了，我想知道为什么。谢谢你。

Answer 1

默认情况下，使用 Z3 的启发式方法处理基于模式的量化实例化的量化公式，例如您在此处拥有的公式。您可以在此处阅读有关 Z3 模式的更多信息：https ://rise4fun.com/Z3/tutorialcontent/guide#h28 和https://github.com/FStarLang/FStar/wiki/Quantifiers-and-patterns

简而言之，你需要帮助 F* 和 Z3 找到存在量词的见证。一种方法是这样的：

let lem (m:nat)
  : Lemma (exists (n:nat). n > m)
  = assert (m + 1 > m)

这证明了一个引理，即对于任何m:nat存在n:nat大于m。它对 F*+Z3 的证明暗示这m + 1是一个很好的证人可供选择n。

您可以通过多种方式将这样的引理转化为量化的断言。有关这方面的一些示例，请参见 FStar.Classical。例如，这有效：

let _ =
  FStar.Classical.forall_intro lem;
  assert (forall (m:nat). exists (n: nat). n > m)

这是另一种避免定义中间引理的方法，而是使用中间断言。

let _ =
  assert (forall (m:nat). m + 1 > m);
  assert (forall (m:nat). exists (n: nat). n > m)