Missing `rec` results in post-condition proof failure

[owickstrom]

This code is from the tutorial, section "4.2. To type intrinsically, or to prove lemmas?" I typed it in myself and forgot a rec when defining rev_involutive:

module Bug_Report

open FStar.List.Tot

val reverse: list 'a -> Tot (list 'a)
let rec reverse = function
  | [] -> []
  | hd :: tl -> append (reverse tl) [hd]

let snoc l h = append l [h]

val snoc_cons: l:list 'a -> h:'a -> Lemma (reverse (snoc l h) == h :: reverse l)
let rec snoc_cons l h = match l with
  | [] -> ()
  | hd :: tl -> snoc_cons tl h

val rev_involutive: l:list 'a -> Lemma (reverse (reverse l) == l)
let rev_involutive l = match l with
  | [] -> ()
  | hd :: tl -> 
    rev_involutive tl;
    snoc_cons (reverse tl) hd

I would expect the compiler to complain about rev_involutive not being in scope, but instead if says:

$ fstar.exe  bug_report.fst 
bug_report.fst(18,23-22,29): (Error 19) could not prove post-condition (see also bug_report.fst(17,39-17,65))
Verified module: Bug_Report (842 milliseconds)
1 error was reported (see above)

Making it let rec rev_involutive ... it verifies correctly. Is this expected behavior or a bug? I found it a bit confusing.

Reproducing

I compiled fstar.exe from the git repository using the provided OCaml sources:

$ fstar.exe --version
F* 0.9.7.0~dev
platform=Linux_x86_64
compiler=OCaml 4.07.1
date=<not set>
commit=0f326698b8e268f06a56297a6af49510cb0e02e8

[mtzguido]

This is confusing, but not a bug!

The rev_involutive in the body is resolving to FStar.List.Tot.Properties.rev_involutive, and not to the one you're defining. When you add the rec, it does resolve to the one in your module, as expected.

Now why are you getting a could not prove post-condition error? Because the lemma in ulib speaks about FStar.List.Tot.Base.rev, and not the reverse you are defining which is potentially completely different.

Just for fun, you can add this just before your last lemma to make it succeed (and prove it if you want):

val rev_is_reverse : l:list 'a -> Lemma (reverse l == rev l) [SMTPat (reverse l)]
let rev_is_reverse l = admit ()

[owickstrom]

Oh, nice one! Thanks for the quick and detailed response.

So, follow-up question. In F*, can I open modules in a way that they're qualified? I'm mostly doing Haskell programming otherwise, and I'd like to do something like:

import qualified FStar.List.Tot as List
import           FStar.List.Tot (list, Cons, Nil)

I'm not very good with OCaml/ML in general, maybe there's a way of doing this that also exists in F*? Thanks!

[mtzguido]

You can qualify the import with

module List = FStar.List.Tot

But I don't think you can select what to import from it.

[owickstrom]

Thanks!