1

有时，子类型判断太难让 f-star 自动计算出来，f-star 希望我更详细地说明我的证明。我也遇到了一些情况，我想写一个引理来证明 f-star 可以做出一些类型判断。

一段看起来像它的语法确实可以解析，但它似乎没有做我想要的。我怀疑我误解了这个语法的作用。在这里，我试图证明 x 具有带引理的类型 nat。为什么这不像我认为的那样？

let x: nat = 3
val tj_lem: unit -> Lemma (x: nat)
let tj_lem () = ()

我也很惊讶我可以在那个位置写“x：nat”。如果需要，我如何“证明 x 是 nat”？

4

1 回答 1

1

您遇到了 F* 语法的丑陋角落。 https://github.com/FStarLang/FStar/issues/1905 我们一直在讨论改进它的方法。

特别是，F* 允许您将名称与在某些情况下无意义的类型相关联。在您的示例中，在引理类型中出现的名称x是没有意义的。x:natF* 将其解释为unit -> Lemma nat：这是表明该nat类型被居住的证明类型……这并不是特别有趣。作为记录，证明无趣类型的一种方法是

let nat_is_inhabited () : Lemma nat = FStar.Squash.return_squash #nat 0

现在，关于如何拼出子类型证明的实际问题。有很多方法。一种常见的方法如下：

假设你有这种类型

let tp = x:t { p }

在某些时候你有

let f (x:t) = … assert (q x); let y : tp = x in …

即，由于某些上下文信息为您提供了属性q x，因此您希望x:t在 type 处进行处理tp。

如果你能证明形式的引理

val q_implies_p (x:t) : Lemma (requires q x) (ensures p x)

然后通过在代码中的正确位置调用引理，您可以为 F* 和 SMT 求解器提供足够的信息来接受 to 的子类型x:t化tp。例如，像这样：

let f (x:t) = … assert (q x); q_implies_p x; let y : tp = x in …

希望有帮助。对不起，令人困惑的语法！

于 2020-03-13T19:00:10.667 回答