Unable to prove lemma with trivial universially quantified precondition (forall x. False ==> False) for most types for x

[klinvill]

I'm seeing z3 struggle with some proofs that seem like they should be trivial while succeeding with other proofs that don't semantically differ.

In particular, this trivial lemma seems to be proven without needing to shoot off any queries to z3 (no file is created when using the --log_queries flag):

let test_forall_int_lemma () : Lemma
  (requires forall (x:int). False)
  (ensures False)
= ()

However if I simply change the type of x from int to nat, z3 is unable to prove the lemma:

let test_forall_nat_lemma () : Lemma
  (requires forall (x:nat). False)
  (ensures False)
= ()

Even more oddly, z3 can prove the lemma if I make a trivial change, such as squashing a trivial nat equality using a variable:

let two : nat = 2
// Note: The proof of test_forall_nat_lemma only succeeds when using the variable `two` rather than the value `2`
let two_equals_two : squash(2 == two) = ()

let test_forall_nat_lemma () : Lemma
  (requires forall (x:nat). False)
  (ensures False)
= ()

Does anyone know what's going on with these lemmas? I'm assuming that the first lemma can be trivially discharged by F* without needing to query z3 and that the second lemma needs to send queries to z3 since nat is a refined type, but why can the third lemma be trivially proven when the second lemma can't?

[nikswamy]

For trivially inhabited types t (like int) F*'s simplifier simplifies forall (x:t). False to False

So, your first example becomes False ==> False, which F* proves without going to Z3.

Your second example doesn't get simplified, so Z3 sees (forall (x:nat). False) ==> False, but to instantiate the quantifer in the hypothesis it needs to find a nat, which it can't do. In SMT2, this is roughly (implies (forall ((x Term)). (! (implies (HasType x nat) false) :pattern ((HasType x nat))) false), so Z3 needs to derive (HasType N nat) for some N

In the third example, the goal is still (forall (x:nat). False) ==> False, but now Z3 has in its context an assertion saying that (HasType two nat) /\ (= two (int_as_term 2)). This assertion allows Z3 to find the instantiation it needs to trigger the quantifier.

[klinvill]

Ah ok, thanks Nik! It looks like I can achieve the same thing through the use of the instantiate tactic. E.g. the below proof works for the second example:

let test_forall_nat_lemma () : Lemma
  (requires (forall (x:nat). False))
  (ensures False)
  by (
    let post = forall_intro () in
    let h = implies_intro () in
    let _ = instantiate h (`1) in
    smt ()
  )
= ()

[gowthamk]

Thanks for the answer Nik! A quick followup: Isn't Nat an alias for x:Int{x>=0}? If so, then forall (x:nat). \phi should be compiled to forall (x:Int). x>=0 => \phi, right? Then why couldn't Z3 instantiate?

[nikswamy]

Quoting from my previous reply, the encoding of forall (x:nat). False is

roughly (implies (forall ((x Term)). (! (implies (HasType x nat) false) :pattern ((HasType x nat))) false), so Z3 needs to derive (HasType N nat) for some N

So, to instantiate this quantifier, F* needs find a term N to match the pattern HasType N nat.
No such term exists ambiently by default.

Explicitly introducing HasType two nat in the context solves this problem

[nikswamy]

Also, F* configures Z3 to not use model-based quantifier instantiation (MBQI). So, quantifier instantiation is done purely using E-matching on patterns