Unexpected failed assertion for toy code

[JansthcirlU]

Hi all, I'm working through the Proof Oriented book and I wanted to play around with some of the things that have been covered up until termination proofs.

module StringHelpers

open FStar.List
open FStar.String

let rec all (#a: eqtype) (l: list a) (f: a -> bool) : bool =
    match l with
    | [] -> true
    | head :: tail -> (f head) && all tail f

let rec any (#a: eqtype) (l: list a) (f: a -> bool) : bool =
    match l with
    | [] -> false
    | head :: tail -> (f head) || any tail f

let contains (s: string) (c: char) : b: bool { b = any (list_of_string s) (fun x -> x = c) } =
    let l = list_of_string s in
    any l (fun x -> x = c)

let test =
    assert (list_of_string "estxyz" = ['e'; 's'; 't'; 'x'; 'y'; 'z']);
    assert (any ['e'; 's'; 't'; 'x'; 'y'; 'z'] (fun c -> c = 't') = true);
    assert (contains "estxyz" 't' = true) ///////////////////////////////////

Inside the test block, the assert for contains fails even though the logic in the asserts above reflects what should be happening inside the function. Why is that? Did I miss something obvious?

Sorry for the trailing backlashes, there was a weird rendering bug where it duplicated the first half of the last line.

[nikswamy]

By default, F* uses the SMT solver to prove asserts. SMT solvers are not the ideal tool for proving properties that require computation. They are better suited for equational reasoning.

To ask F* to prove this assert by computation, you can do this:

assert_norm (contains "estxyz" 't' = true)

which F* reduces and proves easily.

There's a bit about it in the wiki: https://github.com/FStarLang/FStar/wiki/Using-SMT-fuel-and-the-normalizer#using-smt-fuel-to-control-fixpoint-unrolling

And a bit about how F* encodes recursive functions to SMT here: https://fstar-lang.org/tutorial/book/under_the_hood/uth_smt.html#recursive-functions-and-fuel

There are a couple of references to assert_norm in the book, but your question is a good reminder that I should write something a more comprehensive about it

• https://fstar-lang.org/tutorial/book/part3/part3_typeclasses.html#ground-instances
• https://fstar-lang.org/tutorial/book/part2/part2_par.html#part2-par

[JansthcirlU]

Thank you for the clarification. Coming from a regular programming background with no CS training, I'm probably missing some important fundamentals to understand the nuances of SMT solvers. I'll work through more chapters to see if it clicks for me!