Unknown assertion failed in FStar

Question

I'd like to understand what's wrong with this simple exercise.

let even n = (n % 2) = 0

let rec even_sqr (n:nat {even n}) : Lemma (even (n * n)) = 
match n with
  | 0 -> ()
  | _ -> even_sqr (n - 2)

FStar returns '(Error) Unknown assertion failed'.

Answer 1

An "Unknown assertion failed" error means that Z3 did not give F* any reason for the proof failing. Usually, this is either evidence for the need for a more detailed proof, or that the statement is false. In this particular case, the statement is true, it is just that Z3 is not great at non-linear arithmetic (and this example combines both multiplication and modulo operators).

In such a case, some small amount of hand-holding helps. You can do this by adding some assertions that might help point it in the right direction.

In this particular case, I added a new assertion that expands n*n in terms of n-2, and the proof then goes through:

let rec even_sqr (n:nat {even n}) : Lemma (even (n * n)) =
  match n with
  | 0 -> ()
  | _ ->
    assert (n * n == (n - 2) * (n - 2) + 4 * n - 4); (* OBSERVE *)
    even_sqr (n - 2)

Notice that I am not adding any complex proofs, but merely surfacing some properties that might be helpful for the solver to go along. Sometimes with non-linear proofs, however, this may not be enough, and you may require writing a few lemmas, at which point, a good resource is FStar.Math.Lemmas in the standard library.