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)

Issue with a simple assertion in FStar