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'.
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.