Noob - Help me understand assert

[callendorph]

I'm trying to go through the exercises about termination here:

https://fstar-lang.org/tutorial/book/part1/part1_termination.html#exercise-tail-recursive-reversal

The code for the tail-call optimized version of rev looks like this:

let rec rev_aux #a (l1 l2:list a)
  : Tot (list a) (decreases l2)
  = match l2 with
    | []     -> l1
    | hd :: tl -> rev_aux (hd :: l1) tl

// {length r == (length l1) + (length l2)}

let rev2 #a (l:list a) : list a = rev_aux [] l

I've added the decreases l2 as explained in the answer.

I then add the following assert statements to check that this is consistent and working:

let _ = assert ((rev2 [1]) == [1])

// Notice that the lists of ints are reversed as is expected
//  based on what this function is supposed to do.
let _ = assert ((rev2 [1, 2]) == [2, 1])
let _ = assert ((rev2 [1, 2, 3]) == [3, 2, 1])

When I execute this, I get the following error message:

* Error 19 at Part1.Termination.fst(53,8-53,14):
  - Assertion failed
  - The SMT solver could not prove the query. Use --query_stats for more
    details.
  - See also Part1.Termination.fst(53,15-53,40)

1 error was reported (see above)

If I change my asserts to:

let _ = assert ((rev2 [1]) == [1])

// Notice that the lists that I'm comparing against are NOT reversed. 
let _ = assert ((rev2 [1, 2]) == [1, 2])
let _ = assert ((rev2 [1, 2, 3]) == [1, 2, 3])

and I get no errors:

Verified module: Part1.Termination
All verification conditions discharged successfully

I feel like I'm misunderstanding some critical aspect of how this system is supposed to work.

1. Why does the assert pass when I compare against a non-reversed list ?
2. Should I be using = (decidable equality) here or == propositional equality ? I've tried both and I get the same result for each.

Thanks in advance.

[mtzguido]

Hi Carl,

lists in F* are separated with ;, not ,. Comma is used to separate tuple components, and outer parentheses are not required (I think both OCaml and F# use similar syntax). So, in your examples all your lists are actually one-element long, and the element is a tuple. So rev2 [(1,2,3)] is indeed [(1,2,3)].

(It is sometimes confusing to me though... I stared at this for a couple of minutes being completely dumbfounded.)

[callendorph]

Great - that makes a lot more sense. My ocaml is evidently more rusty than I thought.
Thank you!