Missing universes in SMT encoding

[gebner]

In #3644, Guido thankfully pointed me to the old discussion #2069 about missing universe instantiations in the SMT encoding. Apparently, the most obvious way to encounter that issue was eliminated in #2205 by removing the axiom f x << f.

However, the underlying unsoundness due to missing universe instantiations is still present. We can easily define a "predicate" is_univ_zero u#a which is true if and only if a is zero. The SMT encoding of this predicate is clearly inconsistent if we omit the universe instantiation:

module MissingUniv
open FStar.Functions
open FStar.Cardinality.Universes

// is_univ_zero u#a  <==>  a == 0
let is_univ_zero = exists (f: Type u#a -> Type u#0). is_inj f

let is_univ_zero_zero () : Lemma (is_univ_zero u#0) =
  assert is_inj fun (t: Type u#0) -> t

let not_is_univ_zero_succ () : Lemma (~(is_univ_zero u#(a+1))) =
  introduce forall (f: Type u#(a+1) -> Type u#0). ~(is_inj f) with
  no_inj_universes u#0 u#(a+1) f

let _ : squash False =
  is_univ_zero_zero (); not_is_univ_zero_succ u#0 ()

[gebner]

A minimized version that might (or might not) be easier to digest:

module MissingUniv

let contradiction : squash False =
  assert Functions.is_inj (id #Type0);
  Classical.forall_intro (Cardinality.Universes.no_inj_universes u#0 u#(a+1))