未知断言在FStar中失败

Question

我想了解一下这个简单的练习有什么问题。

let even n = (n % 2) = 0

let rec even_sqr (n:nat {even n}) : Lemma (even (n * n)) = 
match n with
  | 0 -> ()
  | _ -> even_sqr (n - 2)

FStar返回‘(错误)未知断言失败’。

Answer 1

“未知断言失败”错误意味着Z3没有给F*任何证明失败的理由。通常，这要么是需要更详细证据的证据，要么是陈述是错误的。在这种特殊情况下，这个语句是正确的，只是Z3在非线性算术方面不是很好(这个例子结合了乘法和模运算符)。

在这种情况下，一些小量的手握帮助。您可以通过添加一些可能有助于将其指向正确方向的断言来做到这一点。

在这个特殊的例子中，我添加了一个新的断言，它扩展了n*n的n-2，然后证明如下：

let rec even_sqr (n:nat {even n}) : Lemma (even (n * n)) =
  match n with
  | 0 -> ()
  | _ ->
    assert (n * n == (n - 2) * (n - 2) + 4 * n - 4); (* OBSERVE *)
    even_sqr (n - 2)

请注意，我并没有添加任何复杂的证明，而只是出现了一些可能有助于求解者进行处理的属性。然而，有时使用非线性证明，这可能还不够，您可能需要编写几个引理，此时，标准库中的FStar.Math.Lemmas是一个很好的资源。