Issue with a simple assertion in FStar

Question

I've just started to study FStar. I'd like to express the fact that for every natural number there exists a bigger one.

let _ = assert (forall (m:nat). exists (n: nat). n > m)

It fails and I'd like to know why. Thank you.

Answer 1

Quantified formulas such as the one you have here are handled, by default, using Z3's heuristics for pattern-based quantified instantiation. You can read more about Z3 patterns here: https://rise4fun.com/Z3/tutorialcontent/guide#h28 and https://github.com/FStarLang/FStar/wiki/Quantifiers-and-patterns

In short, you need to help F* and Z3 find a witness for the existential quantifier. One way to do it is like this:

let lem (m:nat)
  : Lemma (exists (n:nat). n > m)
  = assert (m + 1 > m)

which proves a lemma that for any m:nat there exists an n:nat greater than m. Its proof to F*+Z3 hints that m + 1 is a good witness to choose for n.

You can turn an lemma like this into a quantified assertion in many ways. See FStar.Classical for some examples of that. For example, this works:

let _ =
  FStar.Classical.forall_intro lem;
  assert (forall (m:nat). exists (n: nat). n > m)

Here's another approach that avoids defining an intermediate lemma, but uses an intermediate assertion instead.

let _ =
  assert (forall (m:nat). m + 1 > m);
  assert (forall (m:nat). exists (n: nat). n > m)