关于子类型判断的引理/证明

Question

有时候子类型判断对于 f-star 来说太难自动计算出来，f-star 希望我更详细地说明我的证明。我也运行遇到这样的情况，我想写一个引理来证明 f-star 可以做出某种类型判断。

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

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

我也很惊讶我能在那个位置写"x: nat"。如果需要，我该如何 "prove that x is a nat"？

Answer 1

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

特别是，F* 允许您将名称与在某些情况下毫无意义的类型相关联。在您的示例中，名称 x 在引理类型中出现的 x:nat 中没有意义。它被 F* 解释为 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，您希望在 tp.

类型处处理 x:t

如果你能证明形式为

的引理

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

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

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

希望对您有所帮助。抱歉语法混乱！

Lemmas / proofs about subtyping judgments