3

我刚刚开始学习 F*，正在阅读教程。其中一项练习是证明reverse列表上的函数是单射的。因为这是从对合是单射的事实得出的，所以我想将该事实表达为 F* 中的一个引理。为此，我定义

let is_involutive f = forall x. (f (f x) == x)
let is_injective f = forall x y. (f x == f y) ==> x == y

这是f在 F* 中定义内合或内射概念的正确方法吗？

然后我陈述引理

val inv_is_inj: #a:eqtype -> a -> f:(a->a) -> 
    Lemma (requires (is_involutive f)) (ensures(is_injective f))

非正式地，证明可以写成

 { fix (x:a) (y:a)
   assume (f x == f y)
   then have (f (f x) == f (f y))
   with (is_involutive f) have (x == y)
 } hence (forall (x:a) (y:a). f x == f y ==> x == y)
 then have (is_injective f)

我如何在 F* 中表达这样的证明？一般来说，可以使用哪些 F* 语言结构来证明以下形式的语句，类型的谓词在forall (x:a). phi x哪里？phia

4

0 回答 0