SMT Equality and Extensionality in F*

F* implements a type theory that is in many ways extensional. In particular, any equalities in the context can be directly used and logically combined by the SMT solver without any kind of casts. Previous formalizations of F* (starting with microF*) had in fact 2 rules that together allow us to convert with equalities proved by SMT (G |= t1 == t2):

G |= t1 == t2   G |- t2 : Type
------------------------------ :: Sub-Conv[ersion]
G |- t1 <: t2

G |- e : t1    G |- t1 <: t2
---------------------------- :: T-Sub[sumption]
G |- e : t2

So one way to think about SMT equality is as a notion of definitional equality, since at least it plays that role for conversion. In F*'s prelude == is internalized as squash (equals x y) though, and for that definition it is clear that:

1. equals x y -> x == y (so equality reflection, the main feature of Extensional Type Theory)
2. x == y -> equals x y (by the conversion rules above)

So == is also provably equivalent to propositional equality. One can prove this equivalence in F*:

open FStar.Squash
let reflection a (x y : a) (h:equals x y) : Tot (x == y) = return_squash h
let conversion a (x y : a) (h:(x == y)) : Tot (equals x y) = Refl

Yet the way G |= t1 == t2 is actually implemented is via a complex encoding into SMT. Hopefully that encoding exactly corresponds to equals x y, otherwise it would all break down. In particular, if we were able to prove ~(equals x y) for something the SMT can prove equal, or equals x y for something the SMT can prove unequal we would immediately have an inconsistency.

One interesting feature of the SMT encoding is that for efficiency it maps typed equality in F*:

type eq2 (#a:Type) (x:a) (y:a) :logical = squash (equals x y)

to untyped equality in SMT. This allows the SMT solver to equate and substitute things which in F* have different types. Since F* also has subtyping, this makes F* incompatible with the usual formulations of functional extensionality (see below) and predicate extensionality, but the consequences seem deeper than this and yet to be fully explored.

In particular, our previous formalizations of F* have not considered this untyped substitution aspect. For instance in ufstar.org equality and logical validity G |= φ (trying to capture what's encoded to SMT) are defined as follows:

** Equality:

  eq u (a:Type(u)) : a -> a -> Type(u) {
    Refl : x:a -> eq u a x x
  }

** (4) Logical validity (G |= φ)

  S;G |- e : Tot t
 ------------------ [V-Assume]
  S;G |= t

  S;G |- e : Tot x:t{t'}
 ------------------------ [V-Refine]
  S;G |= t'[e/x]

  S;G |= a     S;G, x:a |= b     x \notin FV(b)
 ----------------------------------------------- [V-Bind]
                    S;G |= b

  S;G, x:a |= b
 ----------------- [V-ForallIntro]
  S;G |= ∀x:a. b

[Note on equality: wherever it says "a = b", it should be understood
that both 'a' and 'b' share a type 't' in a universe 'k', so as to
desugar that equality into "eq k t a b"]

  e ~> e'
  S;G |- e : t
 ----------------- [V-Red]
  S;G |= e =_t e'

  S;G |= e  =_t e'
 ----------------- [V-Sym]
  S;G |= e' =_t e

  S;G |- P : a -> Tot b
  S;G |= e =_a e'
  -------------------- [V-Eq]
  S;G |= P e =_b P e'

  S;G |- a : Type
  --------------- [V-ExMiddle]
  S;G |= a \/ ~a

SMT equality and functional extensionality

Since it is known that

1. F*'s encoding into SMT's untyped equality/substitution is incompatible with vanilla functional extensionality and
2. In Extensional Type Theory one can prove functional extensionality (e.g., see section 1.1 here)

one might wonder how comes F* is still consistent. The only plausible theory is that F*'s SMT equality is not a congruence with respect to lambdas (breaks step 2 of functional extensionality proof in ETT). Since otherwise:

1. F* does have equality reflection (step 1, see reflection proof above)
2. F* has eta (step 3)

Here is an incomplete attempt at proving fun_ext in F* where the missing step would require that SMT equality is a congruence for lambdas:

module FunExt

open FStar.Calc

let eta_fun #a (#b:a -> Type) (f: (x:a -> b x)) :
  Lemma (f == (fun (x:a) -> f x)) = ()

let congruence_fun #a (#b:a -> Type) (f g:(x:a -> b x)) :
  Lemma (requires (forall x. f x == g x))
        (ensures (fun (x:a) -> f x) == (fun (x:a) -> g x)) = admit()

let fun_ext #a (#b:a -> Type) (f g: (x:a -> b x)) :
  Lemma (requires (forall x. f x == g x)) (ensures (f == g)) =
  calc (==) {
    f;
    == { eta_fun f }
    (fun (x:a) -> f x);
    
    == {congruence_fun f g}
    
    (fun (x:a) -> g x);
    == { eta_fun g }    
    g;
  }

The reflection/conversion steps are not needed with the above statement of fun_ext. If one wants to stick closer to the ETT proof one needs to change the statement to use equals instead of ==. Here is a tactic proof for this that uses no SMT:

let fun_ext' #a (#b:a -> Type) (f g: (x:a -> b x)) :
    Lemma (requires (forall x. equals (f x) (g x))) (ensures (equals f g))
  by (
   (* first some boilerplate *)
    let p = forall_intro_as "p" in
    let h = implies_intro() in
    let u = forall_intro() in
    let (h1, h2) = destruct_and h in    
    let h2' = instantiate h2 u in
    mapply h2'; clear h2'; clear h2; clear h;
    (* now the interesting part: *)
    mapply (`conversion);
    l_to_r [`eta_fun]; l_to_r [`eta_fun];
    mapply (`join_squash);
    mapply (`congruence_fun);
    let x = forall_intro() in
    let h1' = instantiate h1 x in
    squash_intro (); mapply h1'
  ) = ()