Some utilities on invariant names

[nikswamy]

This PR provides three utilities for working with invariant names.

1 & 2. A form on injectivity on invariant names. Both these lemmas involve eliminating an inv p and so are in stt_atomic Unobservable, i.e., they are computation steps since they involve using the recall operator of underlying monotonic state monad. That's why I also provided it in two forms, since it's not possible to take the contrapositive of these computation steps.

val distinct_invariants_have_distinct_names
    (#p #q:vprop)
    (i:inv p)
    (j:inv q { (p =!= q) })
: stt_atomic (_:squash (name_of_inv i =!= name_of_inv j))
    #Unobservable
    emp_inames
    emp
    (fun _ -> emp)

val invariant_name_identifies_invariant
      (#p #q:vprop)
      (i:inv p)
      (j:inv q { name_of_inv i == name_of_inv j } )
: stt_atomic (squash (p == q /\ i == j))
    #Unobservable
    emp_inames
    emp
    (fun _ -> emp)

3. Allocating invariants fresh w.r.t a given context:

val fresh_invariant
    (ctx:list allocated_name)
    (p:vprop)
: stt_atomic (i:inv p { name_of_inv i `fresh_wrt` ctx }) #Unobservable emp_inames p (fun _ -> emp)

Note, here I use a notion of allocated_name instead of just a raw iname, though the two are related like so:

val allocated_name : Type0
val allocated_name_of_inv #p (i : inv p) : allocated_name
val name_of_allocated_name (a:allocated_name) : GTot iname
val allocated_name_of_inv_equiv (#p:vprop) (i:inv p)
: Lemma (name_of_allocated_name (allocated_name_of_inv i) == name_of_inv i)
       [SMTPat (name_of_allocated_name (allocated_name_of_inv i))]