val tot_or_ghost_typing_freevars (#g #t #ty #eff: _) (d: typing g t eff ty)
    : Lemma
    (ensures (freevars t) `Set.subset` (vars_of_env g) /\ (freevars ty) `Set.subset` (vars_of_env g)
    )
let tot_or_ghost_typing_freevars
  (#g:_) (#t:_) (#ty:_) (#eff:_)
  (d:typing g t eff ty)
  : Lemma 
    (ensures freevars t `Set.subset` vars_of_env g /\
             freevars ty `Set.subset` vars_of_env g)
  = elab_freevars t;
    elab_freevars ty;      
    let E d = d in
    refl_typing_freevars d;
    assert (vars_of_env_r (elab_env g) `Set.equal` (vars_of_env g))
val tot_or_ghost_typing_freevars (#g #t #ty #eff: _) (d: typing g t eff ty)
    : Lemma
    (ensures (freevars t) `Set.subset` (vars_of_env g) /\ (freevars ty) `Set.subset` (vars_of_env g)
    )
let tot_or_ghost_typing_freevars (#g #t #ty #eff: _) (d: typing g t eff ty)
    : Lemma
    (ensures (freevars t) `Set.subset` (vars_of_env g) /\ (freevars ty) `Set.subset` (vars_of_env g)
    ) =
elab_freevars t;
elab_freevars ty;
let E d = d in
refl_typing_freevars d;
assert ((vars_of_env_r (elab_env g)) `Set.equal` (vars_of_env g))
Pulse.Typing.FV.fst.checked
Pulse.Typing.fst.checked Pulse.Syntax.fst.checked Pulse.Soundness.Common.fst.checked Pulse.Elaborate.fsti.checked prims.fst.checked FStar.Set.fsti.checked FStar.Reflection.V2.fst.checked FStar.Reflection.Typing.fsti.checked FStar.Range.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked FStar.Calc.fsti.checked
Pulse.Typing.FV.fst
Pulse.Typing.Env.env Pulse.Syntax.Base.term FStar.Stubs.TypeChecker.Core.tot_or_ghost Pulse.Typing.typing FStar.Reflection.Typing.typing Pulse.Typing.elab_env Pulse.Elaborate.Pure.elab_term FStar.Pervasives.Native.Mktuple2 FStar.Reflection.Types.typ Prims._assert FStar.Set.equal Pulse.Syntax.Base.var Pulse.Typing.FV.vars_of_env_r Pulse.Typing.FV.vars_of_env Prims.unit Pulse.Typing.FV.refl_typing_freevars Pulse.Elaborate.elab_freevars Prims.l_True Prims.squash Prims.l_and FStar.Set.subset Pulse.Syntax.Naming.freevars Prims.Nil FStar.Pervasives.pattern
module Pulse.Typing.FV
module RT = FStar.Reflection.Typing
module R = FStar.Reflection.V2
module L = FStar.List.Tot
open FStar.List.Tot
open Pulse.Syntax
open Pulse.Typing
open Pulse.Elaborate
open Pulse.Soundness.Common

let vars_of_rt_env (g:R.env) = Set.intension (fun x -> Some? (RT.lookup_bvar g x))

let freevars_close_term_host_term (t:host_term) (x:var) (i:index)
  : Lemma
    (ensures (freevars (close_term' (tm_fstar t FStar.Range.range_0) x i)
            `Set.equal`
             (freevars (tm_fstar t FStar.Range.range_0) `set_minus` x)))
  = admit()

#push-options "--query_stats --z3rlimit_factor 2"
let rec freevars_close_term' (e:term) (x:var) (i:index)
  : Lemma 
    (ensures freevars (close_term' e x i) `Set.equal`
             (freevars e `set_minus` x))
  = match e.t with
    | Tm_Emp
    | Tm_VProp
    | Tm_Inames
    | Tm_EmpInames
    | Tm_Unknown -> ()

    | Tm_Pure p ->
      freevars_close_term' p x i

    | Tm_Star l r ->
      freevars_close_term' l x i;
      freevars_close_term' r x i

    | Tm_ExistsSL _ t b
    | Tm_ForallSL _ t b ->
      freevars_close_term' t.binder_ty x i;    
      freevars_close_term' b x (i + 1)

    | Tm_FStar t ->
      freevars_close_term_host_term t x i

let freevars_close_comp (c:comp)
                        (x:var)
                        (i:index)
  : Lemma 
    (ensures freevars_comp (close_comp' c x i) `Set.equal`
             (freevars_comp c `set_minus` x))
    [SMTPat (freevars_comp (close_comp' c x i))]
  = match c with
    | C_Tot t ->
      freevars_close_term' t x i

    | C_ST s ->
      freevars_close_term' s.res x i;
      freevars_close_term' s.pre x i;      
      freevars_close_term' s.post x (i + 1)

    | C_STAtomic n s
    | C_STGhost n s ->    
      freevars_close_term' n x i;    
      freevars_close_term' s.res x i;
      freevars_close_term' s.pre x i;      
      freevars_close_term' s.post x (i + 1)

let freevars_close_term_opt' (t:option term) (x:var) (i:index)
  : Lemma
    (ensures (freevars_term_opt (close_term_opt' t x i) `Set.equal`
             (freevars_term_opt t `set_minus` x)))
    (decreases t)
  = match t with
    | None -> ()
    | Some t -> freevars_close_term' t x i

let rec freevars_close_term_list' (t:list term) (x:var) (i:index)
  : Lemma
    (ensures (freevars_list (close_term_list' t x i) `Set.equal`
             (freevars_list t `set_minus` x)))
    (decreases t)
  = match t with
    | [] -> ()
    | hd::tl ->
      freevars_close_term' hd x i;
      freevars_close_term_list' tl x i

let rec freevars_close_term_pairs' (t:list (term & term)) (x:var) (i:index)
  : Lemma
    (ensures (freevars_pairs (close_term_pairs' t x i) `Set.equal`
             (freevars_pairs t `set_minus` x)))
    (decreases t)
  = match t with
    | [] -> ()
    | (u, v)::tl ->
      freevars_close_term' u x i;
      freevars_close_term' v x i;
      freevars_close_term_pairs' tl x i

let freevars_close_proof_hint' (ht:proof_hint_type) (x:var) (i:index)
  : Lemma
    (ensures (freevars_proof_hint (close_proof_hint' ht x i) `Set.equal`
             (freevars_proof_hint ht `set_minus` x)))
  = match ht with
    | ASSERT { p }
    | FOLD { p }
    | UNFOLD { p } ->
      freevars_close_term' p x i
    | RENAME { pairs; goal } ->
      freevars_close_term_pairs' pairs x i;
      freevars_close_term_opt' goal x i
    | REWRITE { t1; t2 } ->
      freevars_close_term' t1 x i;
      freevars_close_term' t2 x i

// Needs a bit more rlimit sometimes. Also splitting is too expensive
#push-options "--z3rlimit 20 --split_queries no"
let rec freevars_close_st_term' (t:st_term) (x:var) (i:index)
  : Lemma
    (ensures (freevars_st (close_st_term' t x i) `Set.equal`
             (freevars_st t `set_minus` x)))
    (decreases t)
  = match t.term with
    | Tm_Return { term } ->
      freevars_close_term' term x i

    | Tm_STApp { head; arg } ->
      freevars_close_term' head x i;
      freevars_close_term' arg x i
    
    | Tm_Abs { b; ascription=c; body } ->
      freevars_close_term' b.binder_ty x i;
      freevars_close_comp c x (i + 1);
      freevars_close_st_term' body x (i + 1)

    | Tm_Bind { binder; head; body } ->
      freevars_close_term' binder.binder_ty x i;
      freevars_close_st_term' head x i;
      freevars_close_st_term' body x (i + 1)

    | Tm_TotBind { binder; head; body } ->
      freevars_close_term' binder.binder_ty x i;
      freevars_close_term' head x i;
      freevars_close_st_term' body x (i + 1)
      
    | Tm_If { b; then_; else_; post } ->
      freevars_close_term' b x i;    
      freevars_close_st_term' then_ x i;    
      freevars_close_st_term' else_ x i;          
      freevars_close_term_opt' post x (i + 1)      

    | Tm_Match _ ->
      admit ()

    | Tm_IntroPure { p } 
    | Tm_ElimExists { p } ->
      freevars_close_term' p x i
      
    | Tm_IntroExists { p; witnesses } ->
      freevars_close_term' p x i;
      freevars_close_term_list' witnesses x i

    | Tm_While { invariant; condition; body } ->
      freevars_close_term' invariant x (i + 1);
      freevars_close_st_term' condition x i;
      freevars_close_st_term' body x i

    | Tm_Par { pre1; body1; post1; pre2; body2; post2 } ->
      freevars_close_term' pre1 x i;
      freevars_close_st_term' body1 x i;
      freevars_close_term' post1 x (i + 1);
      freevars_close_term' pre2 x i;
      freevars_close_st_term' body2 x i;
      freevars_close_term' post2 x (i + 1)

    | Tm_Rewrite { t1; t2 } ->
      freevars_close_term' t1 x i;
      freevars_close_term' t2 x i

    | Tm_WithLocal { binder; initializer; body } ->
      freevars_close_term' binder.binder_ty x i;
      freevars_close_term' initializer x i;
      freevars_close_st_term' body x (i + 1)

    | Tm_WithLocalArray { binder; initializer; length; body } ->
      freevars_close_term' binder.binder_ty x i;
      freevars_close_term' initializer x i;
      freevars_close_term' length x i;
      freevars_close_st_term' body x (i + 1)

    | Tm_Admit { typ; post } ->
      freevars_close_term' typ x i;
      freevars_close_term_opt' post x (i + 1)

    | Tm_ProofHintWithBinders { binders; hint_type; t } ->
      let n = L.length binders in
      freevars_close_proof_hint' hint_type x (i + n);
      freevars_close_st_term' t x (i + n)
#pop-options

let freevars_close_term (e:term) (x:var) (i:index)
  : Lemma 
    (ensures freevars (close_term' e x i) `Set.equal`
             (freevars e `set_minus` x))
  = freevars_close_term' e x i

let freevars_close_st_term e x i = freevars_close_st_term' e x i

let contains_r (g:R.env) (x:var) = Some? (RT.lookup_bvar g x)
let vars_of_env_r (g:R.env) = Set.intension (contains_r g)

assume
val refl_typing_freevars (#g:R.env) (#e:R.term) (#t:R.term) (#eff:_) 
                         (_:RT.typing g e (eff, t))
  : Lemma 
    (ensures RT.freevars e `Set.subset` (vars_of_env_r g) /\
             RT.freevars t `Set.subset` (vars_of_env_r g))

assume
val refl_equiv_freevars (#g:R.env) (#e1 #e2:R.term) (d:RT.equiv g e1 e2)
  : Lemma (RT.freevars e1 `Set.subset` (vars_of_env_r g) /\
           RT.freevars e2 `Set.subset` (vars_of_env_r g))

let freevars_open_term_inv (e:term) 
                           (x:var {~ (x `Set.mem` freevars e) })
  : Lemma 
    (ensures freevars e `Set.equal` (freevars (open_term e x) `set_minus` x))
    [SMTPat (freevars (open_term e x))]
  = calc (==) {
     freevars e;
     (==) {  close_open_inverse e x }
     freevars (close_term (open_term e x) x);
     (==) {  freevars_close_term (open_term e x) x 0 }
     freevars (open_term e x) `set_minus` x;
    }

assume
val freevars_open_term (e:term) (x:term) (i:index)
  : Lemma (freevars (open_term' e x i) `Set.subset` 
           (freevars e `Set.union` freevars x))
    [SMTPat (freevars (open_term' e x i))]

assume
val freevars_open_comp (c:comp) (x:term) (i:index)
  : Lemma 
    (ensures
      freevars_comp (open_comp' c x i) `Set.subset` 
      (freevars_comp c `Set.union` freevars x))
    [SMTPat (freevars_comp (open_comp' c x i))]

#push-options "--fuel 2 --ifuel 2"
let tot_or_ghost_typing_freevars
  (#g:_) (#t:_) (#ty:_) (#eff:_)
  (d:typing g t eff ty)
  : Lemma 
    (ensures freevars t `Set.subset` vars_of_env g /\
val tot_or_ghost_typing_freevars (#g #t #ty #eff: _) (d: typing g t eff ty)
    : Lemma
    (ensures (freevars t) `Set.subset` (vars_of_env g) /\ (freevars ty) `Set.subset` (vars_of_env g)
    )
d: Pulse.Typing.typing g t eff ty
  -> FStar.Pervasives.Lemma
    (ensures
      FStar.Set.subset (Pulse.Syntax.Naming.freevars t) (Pulse.Typing.FV.vars_of_env g) /\
      FStar.Set.subset (Pulse.Syntax.Naming.freevars ty) (Pulse.Typing.FV.vars_of_env g))