0

我能简要解释一下为什么这个证明工作会失败吗？在我的研究中，我试图识别生成的整数列表中的简单模式。下面的生成器生成一个交替的 0 和 1 列表。我想证明偶数索引处的项目为 0。

val evenb : nat -> bool
let rec evenb n =
  match n with
  | 0 -> true
  | 1 -> false
  | n -> evenb (n - 2) 

val nth_item : ls: list nat {length ls > 0} -> n: nat {n < length ls} -> nat
let rec nth_item ls n =
  match ls with
  | [h] -> h
  | h :: t -> if n = 0 then h else nth_item t (n - 1)

val gen_01 : lng: nat {lng >= 2 && evenb lng} -> ls: list nat {length ls = lng}
let rec gen_01 lng =
  match lng with 
  | 2 -> [0; 1]
  | _ -> [0; 1] @ gen_01 (lng - 2)

let rec lemma_01 (lng: nat {lng >= 2 && evenb lng}) :
Lemma (forall (n: nat {n <= lng - 2 && evenb n}) . (nth_item (gen_01 lng) n) = 0) = 
  match lng with 
  | 2 -> ()
  | _ -> lemma_01 (lng - 2)

FStar 返回“无法证明后置条件”。我将不胜感激有关该方法的任何帮助。

4

1 回答 1

1

F* 还应该报告一个次要错误位置，该位置指向无法证明的后置条件中的合取——在这种情况下，它只是nth_item (gen_01 lng) n = 0目标。

诊断此问题的一种方法是一次考虑证明的一个分支。例如，如果您admit();在第二个分支中添加一个，那么您会看到第一个分支很容易证明。所以，出了问题的是归纳案例。您没有足够强大的归纳假设来证明您想要的属性。

这是一个证明……可能还有很多其他证明。

首先，我证明了这一点：

let rec access_2n (l:nat{l >= 2 && evenb l}) (n:nat{2 * n < l})
  : Lemma (ensures nth_item (gen_01 l) (2 * n) = 0)
  = match n with
    | 0 -> ()
    | _ -> access_2n (l - 2) (n - 1)

注意对上的归纳，l, n使得长度和访问索引一起减少。

这几乎就是您想要证明的属性，但表述方式略有不同。为了把它按摩成你想要的形式，我这样做了：

首先，evenb算术解释的引理：

[编辑：我添加了一个open FStar.Mul将*符号带入乘法范围]

open FStar.Mul
let rec evenb_is_even (n:nat{evenb n})
  : Lemma (2 * (n / 2) = n)
  = match n with
    | 0 -> ()
    | _ -> evenb_is_even (n - 2)

然后证明一些非常像你的引理的东西，但是对于一个明确的n.

let lemma_01_aux (lng: nat {lng >= 2 && evenb lng}) (n:nat{n <= lng - 2 && evenb n})
  : Lemma (nth_item (gen_01 lng) n = 0)
  = access_2n lng (n / 2); evenb_is_even n

n最后，通过使用将引理转化为量化后置条件的库来普遍量化。

let lemma_01 (lng: nat {lng >= 2 && evenb lng})
  : Lemma (forall (n: nat {n <= lng - 2 && evenb n}) . (nth_item (gen_01 lng) n) = 0)
  = FStar.Classical.forall_intro_2 lemma_01_aux
于 2020-05-22T06:01:00.450 回答