Hint on FStar proof dead end

Question

Can I get a brief explanation why this proof effort fails? In my studies I'm trying to recognize simple patterns in generated lists of integers. The generator below produces a list of alternating 0s and 1s. I'd like to prove that items at even indexes are 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 returns 'could not prove post-condition'. I'd appreciate any help regarding the approach.

Answer 1

F* should also report a secondary error location pointing to the conjunct in the postcondition that was not provable---in this case, it's just the nth_item (gen_01 lng) n = 0 goal.

One way to diagnose this is to consider one branch of the proof at a time. E.g. if you add an admit(); in the second branch, then you'll see that the first branch is easily provable. So, what's going wrong is the inductive case. You don't have a strong enough induction hypothesis to prove the property you want.

Here's one proof of it ... there are probably many others.

First, I proved this:

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)

Notice the induction on the pair l, n so that the length and the access index decrease together.

This is pretty much the property you wanted to prove, stated slightly differently. To massage it into the form you want, I did this:

First, a lemma to interpret evenb arithmetically:

[Edit: I added an open FStar.Mul to bring the * symbol into scope for multiplication]

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)

Then to prove something very like your lemma, but for an explicit 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

And finally to universally quantify over n using a library that turns lemmas into quantified postconditions.

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