fstar - 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标准库中有一个很好的资源。