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，都存在大于m的n:nat。它向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)