val rename_lookup (sg: src_env) (a x y: var)
    : Lemma
      (ensures
        (match lookup sg a with
          | None -> None? (lookup (rename_env sg x y) a)
          | Some (Inl t) -> lookup (rename_env sg x y) a == Some (Inl t)
          | Some (Inr (e1, e2)) ->
            lookup (rename_env sg x y) a == Some (Inr (rename e1 x y, rename e2 x y))))
      (decreases sg)
      [SMTPat (lookup (rename_env sg x y) a)]
val rename_lookup (sg: src_env) (a x y: var)
    : Lemma
      (ensures
        (match lookup sg a with
          | None -> None? (lookup (rename_env sg x y) a)
          | Some (Inl t) -> lookup (rename_env sg x y) a == Some (Inl t)
          | Some (Inr (e1, e2)) ->
            lookup (rename_env sg x y) a == Some (Inr (rename e1 x y, rename e2 x y))))
      (decreases sg)
      [SMTPat (lookup (rename_env sg x y) a)]
let rec rename_lookup (sg:src_env) (a:var) (x y:var)
  : Lemma
    (ensures (
      match lookup sg a with
      | None -> None? (lookup (rename_env sg x y) a)
      | Some (Inl t) -> lookup (rename_env sg x y) a == Some (Inl t)
      | Some (Inr (e1, e2)) -> lookup (rename_env sg x y) a == Some (Inr (rename e1 x y, rename e2 x y))))
    (decreases sg)
    [SMTPat (lookup (rename_env sg x y) a)]
  = match sg with
    | [] -> ()
    | hd::tl -> rename_lookup tl a x y
module BoolRefinement
module T = FStar.Tactics.V2
module R = FStar.Reflection.V2
module L = FStar.List.Tot
open FStar.List.Tot
#push-options "--z3cliopt 'smt.qi.eager_threshold=100' --z3cliopt 'smt.arith.nl=false'"

let var = nat
let index = nat

let tun = R.pack_ln R.Tv_Unknown

type src_exp =
  | EBVar : index -> src_exp
  | EVar  : var -> src_exp
  | EBool : bool -> src_exp
  | EIf   : src_exp -> src_exp -> src_exp -> src_exp
  | ELam  : src_ty -> src_exp -> src_exp
  | EApp  : src_exp -> src_exp -> src_exp

and src_ty =
  | TBool : src_ty
  | TRefineBool : src_exp -> src_ty
  | TArrow : src_ty -> src_ty -> src_ty

let rec size (e:src_exp)
  : nat
  = match e with
    | EBool _
    | EBVar _ 
    | EVar _ -> 1
    | EIf b e1 e2 -> size b + size e1 + size e2 + 1
    | ELam _ e -> 1 + size e
    | EApp e1 e2 -> 1 + size e1 + size e2

let rec freevars (e:src_exp) 
  : FStar.Set.set var
  = match e with
    | EVar v -> Set.singleton v
    | EBool _
    | EBVar _ -> Set.empty
    | EIf b e1 e2 -> Set.union (freevars b) (Set.union (freevars e1) (freevars e2))
    | ELam t e -> Set.union (freevars_ty t) (freevars e)
    | EApp e1 e2 -> Set.union (freevars e1) (freevars e2)
and freevars_ty (t:src_ty)
  : Set.set var
  = match t with
    | TBool -> Set.empty
    | TArrow t1 t2 -> freevars_ty t1 `Set.union` freevars_ty t2
    | TRefineBool e -> freevars e
  
let rec closed (e:src_exp) 
  : b:bool{ b <==> freevars e `Set.equal` Set.empty }
  = match e with
    | EVar v -> 
      assert (v `Set.mem` freevars e);
      false
    | EBool _
    | EBVar _ -> true
    | EIf b e1 e2 -> closed b && closed e1 && closed e2
    | ELam t e -> closed_ty t && closed e
    | EApp e1 e2 -> closed e1 && closed e2
and closed_ty (t:src_ty)
  : b:bool{ b <==> freevars_ty t `Set.equal` Set.empty }
  = match t with
    | TBool -> true
    | TRefineBool e -> closed e
    | TArrow t1 t2 -> closed_ty t1 && closed_ty t2
  
let rec ln' (e:src_exp) (n:int)
  : bool
  = match e with
    | EBool _
    | EVar _ -> true
    | EBVar m -> m <= n
    | EIf b e1 e2 -> ln' b n && ln' e1 n && ln' e2 n
    | ELam t e -> ln_ty t && ln' e (n + 1)
    | EApp e1 e2 -> ln' e1 n && ln' e2 n
and ln_ty (e:src_ty)
  : b:bool{ b ==> closed_ty e }
  = match e with
    | TBool -> true
    | TRefineBool e -> ln' e (- 1) && closed e
    | TArrow t1 t2 -> ln_ty t1 && ln_ty t2

let rec ln_weaker (e:src_exp) (n:int) (m:int{n <= m})
  : Lemma 
    (requires ln' e n)
    (ensures ln' e m)
  = match e with
    | EBool _
    | EVar _
    | EBVar _ -> ()
    | EIf b e1 e2 -> 
      ln_weaker b n m;
      ln_weaker e1 n m;
      ln_weaker e2 n m
    | ELam t e ->
      ln_weaker e (n + 1) (m + 1)
    | EApp e1 e2 ->
      ln_weaker e1 n m;
      ln_weaker e2 n m    

let ln e = ln' e (-1)

let rec open_exp' (e:src_exp) (v:var) (n:index)
  : e':src_exp { size e == size e'}
    = match e with
    | EBool _ -> e
    | EVar m -> EVar m
    | EBVar m -> if m = n then EVar v else EBVar m
    | EIf b e1 e2 -> EIf (open_exp' b v n) (open_exp' e1 v n) (open_exp' e2 v n)
    | ELam t e -> ELam t (open_exp' e v (n + 1))
    | EApp e1 e2 -> EApp (open_exp' e1 v n) (open_exp' e2 v n)

let rec close_exp' (e:src_exp) (v:var) (n:nat)
  : e':src_exp { size e == size e'}
  = match e with
    | EBool _ -> e
    | EVar m -> if m = v then EBVar n else EVar m
    | EBVar m -> EBVar m
    | EIf b e1 e2 -> EIf (close_exp' b v n) (close_exp' e1 v n) (close_exp' e2 v n)
    | ELam t e -> ELam t (close_exp' e v (n + 1))
    | EApp e1 e2 -> EApp (close_exp' e1 v n) (close_exp' e2 v n)

let open_exp e v = open_exp' e v 0
let close_exp e v = close_exp' e v 0

let rec open_close' (e:src_exp) (x:var) (n:nat { ln' e (n - 1) })
  : Lemma (open_exp' (close_exp' e x n) x n == e)
  = match e with
    | EBool _ -> ()
    | EVar _ -> ()
    | EBVar m -> ()
    | EIf b e1 e2 -> 
      open_close' b x n;
      open_close' e1 x n;
      open_close' e2 x n
    | ELam _ e -> open_close' e x (n + 1)
    | EApp e1 e2 -> 
      open_close' e1 x n; 
      open_close' e2 x n

let open_close (e:src_exp) (x:var)
  : Lemma 
    (requires ln e)
    (ensures open_exp (close_exp e x) x == e)
    [SMTPat (open_exp (close_exp e x) x)]
  = open_close' e x 0

let rec open_exp_ln (e:src_exp) (v:var) (n:index) (m:int)
  : Lemma 
    (requires ln' e n /\
              m == n - 1)
    (ensures ln' (open_exp' e v n) m)
    [SMTPat (ln' e n);
     SMTPat (ln' (open_exp' e v n) m)]
  = match e with
    | EBool _ -> ()
    | EVar _ -> ()
    | EBVar m -> ()
    | EIf b e1 e2 ->
      open_exp_ln b v n m;
      open_exp_ln e1 v n m;
      open_exp_ln e2 v n m
    | ELam _ e -> open_exp_ln e v (n + 1) (m + 1)
    | EApp e1 e2 -> open_exp_ln e1 v n m; open_exp_ln e2 v n m

let rec close_exp_ln (e:src_exp) (v:var) (n:nat)
  : Lemma 
    (requires ln' e (n - 1))
    (ensures ln' (close_exp' e v n) n)
    [SMTPat (ln' (close_exp' e v n) n)]
  = match e with
    | EBool _ -> ()
    | EVar _ -> ()
    | EBVar m -> ()
    | EIf b e1 e2 ->
      close_exp_ln b v n;
      close_exp_ln e1 v n;
      close_exp_ln e2 v n
    | ELam _ e -> close_exp_ln e v (n + 1)
    | EApp e1 e2 -> close_exp_ln e1 v n; close_exp_ln e2 v n

#push-options "--z3rlimit 15"
let rec open_exp_freevars (e:src_exp) (v:var) (n:nat)
  : Lemma ((freevars e `Set.subset` freevars (open_exp' e v n))  /\
           (freevars (open_exp' e v n) `Set.subset` (freevars e `Set.union` Set.singleton v)))
          [SMTPat (freevars (open_exp' e v n))]
  = match e with
    | EBool _
    | EBVar _ 
    | EVar _ -> ()
    | EApp e1 e2 ->
      open_exp_freevars e1 v n;
      open_exp_freevars e2 v n
    | EIf b e1 e2 ->
      open_exp_freevars b v n;    
      open_exp_freevars e1 v n;
      open_exp_freevars e2 v n
    | ELam t e ->
      open_exp_freevars e v (n + 1)
#pop-options

let minus (s:Set.set 'a) (x:'a) = Set.intersect s (Set.complement (Set.singleton x))

let rec close_exp_freevars (m:int) (e:src_exp { ln' e m } ) (v:var) (n:nat)
  : Lemma 
    (ensures freevars (close_exp' e v n) `Set.equal`
             (freevars e `minus` v))
    (decreases e)
  = match e with
    | EBool _
    | EBVar _ 
    | EVar _ -> ()
    | EApp e1 e2 ->
      close_exp_freevars m e1 v n;
      close_exp_freevars m e2 v n
    | EIf b e1 e2 ->
      close_exp_freevars m b v n;    
      close_exp_freevars m e1 v n;
      close_exp_freevars m e2 v n
    | ELam t body ->
      close_exp_freevars (m + 1) body v (n + 1)

let s_exp = e:src_exp { ln e }
let src_eqn = s_exp & s_exp

let s_ty = t:src_ty { ln_ty t }
//environment binds types or equations
let src_env = list (var & either s_ty src_eqn) 

let rec lookup (e:list (var & 'a)) (x:var)
  : option 'a
  = match e with
    | [] -> None
    | (y, v) :: tl -> if x = y then Some v else lookup tl x

let rec src_env_ok (s:src_env)
  : bool
  = match s with
    | [] -> true
    | (x, _)::tl -> None? (lookup tl x) && src_env_ok tl

let lookup_ty (e:src_env) (x:var)
  : option src_ty
  = match lookup e x with
    | Some (Inl t) -> Some t
    | _ -> None
    
let max (n1 n2:nat) = if n1 < n2 then n2 else n1

let rec fresh (e:list (var & 'a))
  : var
  = match e with
    | [] -> 0
    | (y, _) :: tl ->  max (fresh tl) y + 1
    | _ :: tl -> fresh tl

let rec fresh_not_mem (e:list (var & 'a)) (elt: (var & 'a))
  : Lemma (ensures L.memP elt e ==> fresh e > fst elt)
  = match e with
    | [] -> ()
    | hd :: tl -> fresh_not_mem tl elt
  
let rec lookup_mem (e:list (var & 'a)) (x:var)
  : Lemma
    (requires Some? (lookup e x))
    (ensures exists elt. L.memP elt e /\ fst elt == x)
  = match e with
    | [] -> ()
    | hd :: tl -> 
      match lookup tl x with
      | None -> assert (L.memP hd e)
      | _ -> 
        lookup_mem tl x;
        eliminate exists elt. L.memP elt tl /\ fst elt == x
        returns _
        with _ . ( 
          introduce exists elt. L.memP elt e /\ fst elt == x
          with elt
          and ()
        )

let fresh_is_fresh (e:src_env)
  : Lemma (None? (lookup e (fresh e)))
  =  match lookup e (fresh e) with
     | None -> ()
     | Some _ ->
       lookup_mem e (fresh e);
       FStar.Classical.forall_intro (fresh_not_mem e)

module RT = FStar.Reflection.Typing

let r_b2t (t:R.term) 
  : R.term 
  = R.(pack_ln (Tv_App (pack_ln (Tv_FVar RT.b2t_fv)) (t, Q_Explicit)))

let rec elab_exp (e:src_exp)
  : Tot R.term
  = let open R in
    match e with
    | EBool true ->
      pack_ln (Tv_Const R.C_True)

    | EBool false ->
      pack_ln (Tv_Const R.C_False)

    | EBVar n -> 
      let bv = R.pack_bv (RT.make_bv n) in
      R.pack_ln (Tv_BVar bv)
      
    | EVar n ->
      let namedv = R.pack_namedv (RT.make_namedv n) in
      R.pack_ln (Tv_Var namedv)

    | ELam t e ->
      let t = elab_ty t in
      let e = elab_exp e in
      R.pack_ln (Tv_Abs (RT.mk_simple_binder RT.pp_name_default t) e)
             
    | EApp e1 e2 ->
      let e1 = elab_exp e1 in
      let e2 = elab_exp e2 in
      R.pack_ln (Tv_App e1 (e2, Q_Explicit))

    | EIf b e1 e2 ->
      let b = elab_exp b in
      let e1 = elab_exp e1 in
      let e2 = elab_exp e2 in
      R.pack_ln (Tv_Match b None [(Pat_Constant C_True, e1); (Pat_Constant C_False, e2)])
      
and elab_ty (t:src_ty) 
  : R.term  
  = let open R in
    match t with
    | TBool -> 
      RT.bool_ty
      
    | TArrow t1 t2 ->
      let t1 = elab_ty t1 in
      let t2 = elab_ty t2 in
      R.pack_ln 
        (R.Tv_Arrow 
          (RT.mk_simple_binder RT.pp_name_default t1)
          (RT.mk_total t2)) //.pack_comp (C_Total t2 u_unk [])))
          
    | TRefineBool e ->
      let e = elab_exp e in
      let b : R.simple_binder = RT.mk_simple_binder RT.pp_name_default RT.bool_ty in
      let bv = R.pack_bv (RT.make_bv 0) in
      let refinement = r_b2t (R.pack_ln (Tv_App e (R.pack_ln (Tv_BVar bv), Q_Explicit))) in
      R.pack_ln (Tv_Refine b refinement)

let elab_eqn (e1 e2:src_exp)
  : R.term
  = RT.eq2 RT.u_zero RT.bool_ty (elab_exp e1) (elab_exp e2)

let binding = either s_ty src_eqn
let elab_binding (b:binding)
  : R.term 
  = match b with
    | Inl t -> elab_ty t
    | Inr (e1, e2) -> elab_eqn e1 e2
    
let extend_env_l (g:R.env) (sg:src_env) = 
  L.fold_right 
    (fun (x, b) g ->  RT.extend_env g x (elab_binding b))
     sg
     g

let as_bindings (sg:src_env) 
  : RT.bindings
  = L.map (fun (x, b) -> x, elab_binding b) sg

let extend_env_alt (g:R.env) (sg:src_env) = 
  RT.extend_env_l g (as_bindings sg)

let rec extend_env_equiv (g:R.env) (sg:src_env)
  : Lemma 
    (ensures extend_env_l g sg == extend_env_alt g sg)
    (decreases sg)
  = match sg with
    | [] -> ()
    | hd::tl -> extend_env_equiv g tl

let rec extend_env_alt_append (g:R.env) (sg0 sg1:src_env)
  : Lemma 
    (ensures 
      extend_env_alt g (sg0 @ sg1) == 
      extend_env_alt (extend_env_alt g sg1) sg0)
    (decreases sg0)
  = match sg0 with
    | [] -> ()
    | hd::tl -> extend_env_alt_append g tl sg1

[@@erasable]
noeq
type sub_typing (f:RT.fstar_top_env) : src_env -> s_ty -> s_ty -> Type =
  | S_Refl : g:src_env -> t:s_ty -> sub_typing f g t t
  | S_ELab : g:src_env -> t0:s_ty -> t1:s_ty ->
             RT.sub_typing (extend_env_l f g) (elab_ty t0) (elab_ty t1) ->
             sub_typing f g t0 t1

  
[@@erasable]
noeq
type src_typing (f:RT.fstar_top_env) : src_env -> src_exp -> s_ty -> Type =
  | T_Bool :
      g:src_env ->
      b:bool ->
      src_typing f g (EBool b) TBool
  
  | T_Var  :
      g:src_env ->
      x:var { Some? (lookup_ty g x) } ->
      src_typing f g (EVar x) (Some?.v (lookup_ty g x))

  | T_Lam  :
      g:src_env ->
      t:s_ty ->
      e:src_exp ->
      t':s_ty ->
      x:var { None? (lookup g x) /\ ~ (x `Set.mem` freevars e)} ->
      src_ty_ok f g t ->
      src_typing f ((x, Inl t) :: g) (open_exp e x) t' ->
      src_typing f g (ELam t e) (TArrow t t')

  | T_App  :
      g:src_env ->
      e1:src_exp ->
      e2:src_exp ->
      t:s_ty ->
      t':s_ty ->
      t0:s_ty ->
      src_typing f g e1 (TArrow t t') ->
      src_typing f g e2 t0 ->
      sub_typing f g t0 t ->
      src_typing f g (EApp e1 e2) t'

   | T_If :
       g:src_env ->
       b:s_exp ->
       e1:src_exp ->
       e2:src_exp ->
       t1:s_ty ->
       t2:s_ty ->
       t:s_ty ->
       hyp:var { None? (lookup g hyp) /\ ~ (hyp `Set.mem` freevars e1) /\ ~ (hyp `Set.mem` freevars e2) } ->
       src_typing f g b TBool ->
       src_typing f ((hyp, Inr (b, EBool true)) :: g) e1 t1 ->
       src_typing f ((hyp, Inr (b, EBool false)) :: g) e2 t2 ->
       sub_typing f ((hyp, Inr (b, EBool true)) :: g) t1 t ->
       sub_typing f ((hyp, Inr (b, EBool false)) :: g) t2 t ->
       src_ty_ok f g t ->
       src_typing f g (EIf b e1 e2) t
       
and src_ty_ok (f:RT.fstar_top_env) : src_env -> s_ty -> Type =
  | OK_TBool  : g:src_env -> src_ty_ok f g TBool
  | OK_TArrow : g:src_env -> t:s_ty -> t':s_ty ->
                src_ty_ok f g t ->
                src_ty_ok f g t' ->                
                src_ty_ok f g (TArrow t t')
  | OK_TRefine: g:src_env ->
                e:src_exp { ln e && closed e}  ->
                src_typing f [] e (TArrow TBool TBool) ->
                src_ty_ok f g (TRefineBool e)

let s_height #f #g #t0 #t1 (d:sub_typing f g t0 t1)
  : GTot nat
  = 1
  
let rec height #f #g #e #t (d:src_typing f g e t)
  : GTot nat (decreases d)
  = match d with
    | T_Bool _ _ -> 1
    | T_Var _ _ -> 1
    | T_Lam _ _ _ _ _ ty_ok body -> max (height body) (t_height ty_ok) + 1
    | T_App _ _ _ _ _ _  tl tr ts -> max (max (height tl) (height tr)) (s_height ts) + 1
    | T_If _ _ _ _ _ _ _ _ tb tl tr sl sr st ->
      max (height tb) 
          (max (max (height tl) (height tr))
               (max (s_height sl) (max (s_height sr) (t_height st)))) + 1
    
and t_height #f (#g:src_env) (#t:s_ty) (d:src_ty_ok f g t)    
  : GTot nat (decreases d)
  = match d with
    | OK_TBool _ -> 1
    | OK_TArrow _ _ _ d0 d1 -> max (t_height d0) (t_height d1) + 1
    | OK_TRefine _ _ d -> height d + 1

module FTB = FStar.Stubs.Tactics.V2.Builtins

let check_sub_typing (f:RT.fstar_top_env)
                     (sg:src_env)
                     (t0 t1:s_ty)
  : T.Tac (sub_typing f sg t0 t1)
  = if t0 = t1 then S_Refl _ t0
    else let t0' = elab_ty t0 in
         let t1' = elab_ty t1 in
         let f' = extend_env_l f sg in
         let token_opt, _issues = FTB.check_subtyping f' t0' t1' in
         match token_opt with
         | None -> T.fail "Not subtypes"
         | Some token ->
           S_ELab sg t0 t1
             (RT.Rel_subtyping_token f' t0' t1' (FStar.Squash.return_squash token))

let weaken (f:RT.fstar_top_env) (sg:src_env) (hyp:var { None? (lookup sg hyp) } ) (b:s_exp) (t0 t1:s_ty)
  : T.Tac (t:s_ty &
           sub_typing f ((hyp,Inr(b, EBool true))::sg) t0 t &
           sub_typing f ((hyp,Inr(b, EBool false))::sg) t1 t)
  = if t0 = t1
    then (| t0, S_Refl _ t0, S_Refl _ t1 |)
    else T.fail "weaken is very dumb"

let exp (sg:src_env) = e:src_exp { ln e /\ (forall x. x `Set.mem` freevars e ==> Some? (lookup sg x)) }

#push-options "--fuel 2 --ifuel 2 --z3rlimit_factor 6 --query_stats"
let rec check (f:RT.fstar_top_env)
              (sg:src_env)
              (e:exp sg)
  : T.Tac (t:s_ty &
           src_typing f sg e t)
  = match e with
    | EBool b ->
      (| TBool, T_Bool _ b |)

    | EVar n ->
      begin
      match lookup_ty sg n with
      | None -> T.fail "Ill-typed"
      | Some t ->
        let d = T_Var sg n in
        (| t, d |)
      end

    | ELam t body -> 
      let t_ok = check_ty f sg t in
      let x = fresh sg in
      fresh_is_fresh sg;
      let (| tbody, dbody |) = check f ((x, Inl t)::sg) (open_exp body x) in
      let e' = ELam t body in
      let dd : src_typing f sg e' (TArrow t tbody) = 
             T_Lam sg t body tbody x t_ok dbody in
      (| TArrow t tbody, dd |)

    | EApp e1 e2 ->
      let (| t1, d1 |) = check f sg e1  in
      let (| t2, d2 |) = check f sg e2 in
      begin
      match t1 with
      | TArrow t_arg t_res ->
        let st_ok = check_sub_typing f sg t2 t_arg in
        (| t_res, T_App _ _ _ t_arg t_res _ d1 d2 st_ok |)

      | _ -> 
        T.fail "Expected a function"
      end

    | EIf b e1 e2 ->
      let (| tb, ok_b |) = check f sg b in
      let hyp = fresh sg in
      fresh_is_fresh sg;
      if tb = TBool
      then (
        let (| t1, ok_1 |) = check f ((hyp, Inr(b, EBool true))::sg) e1 in
        let (| t2, ok_2 |) = check f ((hyp, Inr(b, EBool false))::sg) e2 in      
        let (| t, w1, w2 |) = weaken f sg hyp b t1 t2 in
        let t_ok = check_ty f sg t in
        (| t, T_If _ _ _ _ _ _ _ hyp ok_b ok_1 ok_2 w1 w2 t_ok |)
      )
      else T.fail "Branching on a non-boolean"

and check_ty (f:RT.fstar_top_env)
             (sg:src_env)
             (t:s_ty)
  : T.Tac (src_ty_ok f sg t)
  = match t with
    | TBool -> OK_TBool _

    | TArrow t t' ->
      let t_ok  = check_ty f sg t in
      let t'_ok = check_ty f sg t' in      
      OK_TArrow _ _ _ t_ok t'_ok
      
    | TRefineBool e ->
      let (| te, de |) = check f [] e in
      match te with
      | TArrow TBool TBool -> OK_TRefine _ _ de
      | _ -> T.fail "Ill-typed refinement"
#pop-options
  
let rec extend_env_l_lookup_bvar (g:R.env) (sg:src_env) (x:var)
  : Lemma 
    (requires (forall x. RT.lookup_bvar g x == None))
    (ensures (
      match lookup sg x with
      | Some b -> RT.lookup_bvar (extend_env_l g sg) x == Some (elab_binding b)
      | None -> RT.lookup_bvar (extend_env_l g sg) x == None))
    (decreases sg)
    [SMTPat (RT.lookup_bvar (extend_env_l g sg) x)]
  = match sg with
    | [] -> ()
    | hd :: tl -> extend_env_l_lookup_bvar g tl x

//key lemma about src types: Their elaborations are closed
#push-options "--z3rlimit_factor 4 --fuel 8 --ifuel 2"
let rec src_refinements_are_closed_core
                       (n:nat)
                       (e:src_exp {ln' e (n - 1) && closed e}) 
                       (elt:RT.subst_elt)
  : Lemma (ensures RT.subst_term (elab_exp e) (RT.shift_subst_n n [elt]) ==
                   elab_exp e)
          (decreases e)
  = match e with
    | EBool _ -> ()
    | EBVar _ -> ()
    | EApp e1 e2 ->
      src_refinements_are_closed_core n e1 elt;
      src_refinements_are_closed_core n e2 elt
    | EIf b e1 e2 ->
      src_refinements_are_closed_core n b elt;    
      src_refinements_are_closed_core n e1 elt;
      src_refinements_are_closed_core n e2 elt
    | ELam t e1 ->
      src_types_are_closed_core t elt n;
      src_refinements_are_closed_core (n + 1) e1 elt
and src_types_are_closed_core (ty:s_ty) (elt:RT.subst_elt) (n:nat)
  : Lemma (ensures RT.subst_term (elab_ty ty) (RT.shift_subst_n n [elt]) ==
                   elab_ty ty)
          (decreases ty)
  = match ty with
    | TBool -> ()
    | TArrow t1 t2 ->
      src_types_are_closed_core t1 elt n;
      src_types_are_closed_core t2 elt (n + 1)
    | TRefineBool e ->
      assert (ln e);
      assert (closed e);
      ln_weaker e (-1) n;
      src_refinements_are_closed_core (n + 1) e elt
#pop-options

let src_refinements_are_closed (e:src_exp {ln e && closed e}) 
                               (elt:RT.subst_elt)
  : Lemma (ensures RT.subst_term (elab_exp e) [elt] == elab_exp e)
          (decreases e)
 =  ln_weaker e (-1) 0;
    src_refinements_are_closed_core 0 e elt
 

#push-options "--query_stats --fuel 8 --ifuel 2 --z3rlimit_factor 2"
let rec elab_open_commute' (n:nat) (e:src_exp { ln' e n }) (x:var) 
  : Lemma (ensures
              RT.subst_term (elab_exp e) (RT.open_with_var x n) ==
              elab_exp (open_exp' e x n))
          (decreases e)
  = match e with
    | EBool _ -> ()
    | EBVar _ -> ()
    | EVar _ -> ()
    | EApp e1 e2 -> 
      elab_open_commute' n e1 x;
      elab_open_commute' n e2 x
    | EIf b e1 e2 ->
      elab_open_commute' n b x;    
      elab_open_commute' n e1 x;
      elab_open_commute' n e2 x;
      let opening = RT.open_with_var x in
      assert (RT.subst_term (elab_exp e) (opening n) ==
              R.(pack_ln (Tv_Match (RT.subst_term (elab_exp b) (opening n))
                                  None
                                  [(Pat_Constant C_True, RT.subst_term (elab_exp e1) (opening n));
                                   (Pat_Constant C_False, RT.subst_term (elab_exp e2) (opening n))])))
    | ELam t e ->
      calc (==) {
        elab_exp (open_exp' (ELam t e) x n);
      (==) {}
        elab_exp (ELam t (open_exp' e x (n + 1)));      
      (==) {  }
        R.(pack_ln (Tv_Abs (RT.mk_simple_binder RT.pp_name_default (elab_ty t)) (elab_exp (open_exp' e x (n + 1)))));
      (==) { elab_open_commute' (n + 1) e x } 
        R.(pack_ln (Tv_Abs (RT.mk_simple_binder RT.pp_name_default (elab_ty t))
                           (RT.subst_term (elab_exp e) RT.(open_with_var x (n + 1)))));
      (==) { src_types_are_closed_core t (RT.open_with_var_elt x n) 0 }
        RT.subst_term
          R.(pack_ln (Tv_Abs (RT.mk_simple_binder RT.pp_name_default (elab_ty t)) (elab_exp e)))
          RT.(open_with_var x n);    
      }
#pop-options

let elab_open_commute (e:src_exp { ln' e 0 }) (x:var)
  : Lemma (RT.open_term (elab_exp e) x == elab_exp (open_exp e x))
          [SMTPat (RT.open_term (elab_exp e) x)]
  = elab_open_commute' 0 e x;
    RT.open_term_spec (elab_exp e) x

//key lemma about src types
let src_types_are_closed1 (ty:s_ty) (v:R.term)
  : Lemma (RT.open_with (elab_ty ty) v == elab_ty ty)
          [SMTPat (RT.open_with (elab_ty ty) v)]
  = src_types_are_closed_core ty (RT.DT 0 v) 0;
    RT.open_with_spec (elab_ty ty) v

let src_types_are_closed2 (ty:s_ty) (x:R.var)
  : Lemma (RT.close_term (elab_ty ty) x == elab_ty ty)
          [SMTPat (RT.close_term (elab_ty ty) x)]
  = src_types_are_closed_core ty (RT.ND x 0) 0;
    RT.close_term_spec (elab_ty ty) x

let src_types_are_closed3 (ty:s_ty) (x:R.var)
  : Lemma (RT.open_term (elab_ty ty) x == elab_ty ty)
          [SMTPat (RT.open_term (elab_ty ty) x)]
  = src_types_are_closed_core ty (RT.open_with_var_elt x 0) 0;
    RT.open_term_spec (elab_ty ty) x

let b2t_typing (g:RT.fstar_env) (t:R.term) (dt:RT.tot_typing g t RT.bool_ty)
  : RT.tot_typing g (r_b2t t) (RT.tm_type RT.u_zero)
  = let b2t_typing : RT.tot_typing g _ RT.b2t_ty = RT.T_FVar g RT.b2t_fv in
    let app_ty : _ = RT.T_App _ _ _ _ (RT.tm_type RT.u_zero) _ b2t_typing dt in
    RT.open_with_spec (RT.tm_type RT.u_zero) t;
    app_ty

let rec extend_env_l_lookup_fvar (g:R.env) (sg:src_env) (fv:R.fv)
  : Lemma 
    (ensures
      RT.lookup_fvar (extend_env_l g sg) fv ==
      RT.lookup_fvar g fv)
    [SMTPat (RT.lookup_fvar (extend_env_l g sg) fv)]
  = match sg with
    | [] -> ()
    | hd::tl -> extend_env_l_lookup_fvar g tl fv

open FStar.List.Tot    
let rec src_ty_ok_weakening (#f:RT.fstar_top_env)
                            (sg sg':src_env)
                            (x:var { None? (lookup sg x) && None? (lookup sg' x) })
                            (b:binding)
                            (t:s_ty)
                            (d:src_ty_ok f (sg'@sg) t)
  : GTot (d':src_ty_ok f (sg'@((x, b)::sg)) t { t_height d' == t_height d })
         (decreases d)
  = match d with
    | OK_TBool _ -> OK_TBool _
    | OK_TArrow _ _ _ d1 d2 -> 
      let d1 = src_ty_ok_weakening _ _ _ _ _ d1 in
      let d2 = src_ty_ok_weakening _ _ _ _ _ d2 in      
      OK_TArrow _ _ _ d1 d2
    | OK_TRefine _ _ d -> OK_TRefine _ _ d

let rec rename (e:src_exp) (x y:var) 
  : e':src_exp { forall m. ln' e m ==> ln' e' m }
  = match e with
    | EBool _ -> e
    | EBVar _ -> e
    | EVar m -> if m = x then EVar y else EVar m
    | EIf b e1 e2 -> EIf (rename b x y) (rename e1 x y) (rename e2 x y)
    | ELam t e -> ELam t (rename e x y)
    | EApp e1 e2 -> EApp (rename e1 x y) (rename e2 x y)

let rename_binding (b:binding) (x y:var)
  : either s_ty src_eqn
  = match b with
    | Inl t -> Inl t
    | Inr (e1, e2) -> Inr (rename e1 x y, rename e2 x y)

let rename_src_env_elt (x y:var) (e : (var & either s_ty src_eqn))
  = let (a, b) = e in
    a, rename_binding b x y
    
let rename_env (sg:src_env) (x y:var)
  : src_env
  = L.map (rename_src_env_elt x y) sg

let rec rename_freevars (e:src_exp) (x y:var)
  : Lemma (freevars (rename e x y) `Set.subset` (freevars e `Set.union` (Set.singleton y)))
          [SMTPat (freevars (rename e x y))]
  = match e with
    | EBool _
    | EBVar _ 
    | EVar _ -> ()
    | EApp e1 e2 -> 
      rename_freevars e1 x y;
      rename_freevars e2 x y
    | EIf b e1 e2 ->
      rename_freevars b x y;    
      rename_freevars e1 x y;
      rename_freevars e2 x y    
    | ELam t body ->
      rename_freevars body x y

let rec lookup_middle (sg sg':src_env)
                      (x:var { None? (lookup sg' x) })
                      (b:binding)
  : Lemma 
    (ensures lookup (sg'@(x,b)::sg) x == Some b)
    (decreases sg')
  = match sg' with
    | [] -> ()
    | hd::tl ->
      lookup_middle sg tl x b

let rec lookup_append_inverse (sg sg':src_env)
                              (z:var)
  : Lemma 
    (ensures (match lookup (sg'@sg) z with
              | None -> None? (lookup sg' z) && None? (lookup sg z)
              | Some b -> (lookup sg' z == Some b) \/
                         (None? (lookup sg' z) /\ lookup sg z == Some b)))
    (decreases sg')
  = match sg' with
    | [] -> ()
    | hd::tl -> lookup_append_inverse sg tl z

let cons_append_assoc (sg sg':list 'a) (x:'a)
  : Lemma (x::(sg'@sg) == (x::sg')@sg)
  = ()

let rec rename_open' (x y:var) 
                     (e:src_exp { ~ (x `Set.mem` freevars e) })
                     (n:nat)
  : Lemma 
    (ensures rename (open_exp' e x n) x y == open_exp' e y n)
    (decreases e)
  = match e with
    | EBool _ -> ()
    | EVar _ -> ()
    | EBVar _ -> ()
    | EApp e1 e2 -> 
      rename_open' x y e1 n;
      rename_open' x y e2 n    
    | EIf b e1 e2 ->
      rename_open' x y b n;    
      rename_open' x y e1 n;
      rename_open' x y e2 n
    | ELam t e ->
      rename_open' x y e (n + 1)

let rec rename_id (x y:var) 
                  (e:src_exp { ~ (x `Set.mem` freevars e) \/ x == y })
  : Lemma 
    (ensures rename e x y == e)
    (decreases e)
  = match e with
    | EBool _ -> ()
    | EVar _ -> ()
    | EBVar _ -> ()
    | EApp e1 e2 -> 
      rename_id x y e1;
      rename_id x y e2      
    | EIf b e1 e2 ->
      rename_id x y b;    
      rename_id x y e1;
      rename_id x y e2      
    | ELam t e ->
      rename_id x y e

// This is a key lemma in renaming
// The precondition on `x` necessitates a a lot more reasoning on 
// freevars, freshness etc
let rename_open (e:src_exp) (x:var { ~(x `Set.mem` freevars e) }) (y:var)
  : Lemma (rename (open_exp e x) x y == open_exp e y)
  = rename_open' x y e 0

let rename_trivial (e:src_exp) (x:var) 
  : Lemma (rename e x x == e)
          [SMTPat (rename e x x)]
  = rename_id x x e

let rec rename_open_commute' (e:src_exp) (z:var) (x y:var) (n:nat)
  : Lemma
    (requires z <> x /\ z <> y)
    (ensures rename (open_exp' e z n) x y == open_exp' (rename e x y) z n)
    (decreases e)
  = match e with
    | EBool _ -> ()
    | EVar _ -> ()
    | EBVar _ -> ()
    | EApp e1 e2 -> 
      rename_open_commute' e1 z x y n;
      rename_open_commute' e2 z x y n
    | EIf b e1 e2 ->
      rename_open_commute' b z x y n;    
      rename_open_commute' e1 z x y n;
      rename_open_commute' e2 z x y n
    | ELam t e ->
      rename_open_commute' e z x y (n + 1)


let rename_open_commute (e:src_exp) (z:var) (x y:var)
  : Lemma
    (requires z <> x /\ z <> y)
    (ensures rename (open_exp e z) x y == open_exp (rename e x y) z)
  = rename_open_commute' e z x y 0
/
prims.fst.checked FStar.Tactics.V2.fst.checked FStar.Stubs.Tactics.V2.Builtins.fsti.checked FStar.Squash.fsti.checked FStar.Set.fsti.checked FStar.Reflection.V2.fst.checked FStar.Reflection.Typing.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked FStar.Classical.Sugar.fsti.checked FStar.Classical.fsti.checked FStar.Calc.fsti.checked
BoolRefinement.fst

    sg: BoolRefinement.src_env ->
    a: BoolRefinement.var ->
    x: BoolRefinement.var ->
    y: BoolRefinement.var
  -> FStar.Pervasives.Lemma
      (ensures
        ((match BoolRefinement.lookup sg a with
            | FStar.Pervasives.Native.None #_ ->
              None? (BoolRefinement.lookup (BoolRefinement.rename_env sg x y) a)
            | FStar.Pervasives.Native.Some #_ (FStar.Pervasives.Inl #_ #_ t) ->
              BoolRefinement.lookup (BoolRefinement.rename_env sg x y) a ==
              FStar.Pervasives.Native.Some (FStar.Pervasives.Inl t)
            | FStar.Pervasives.Native.Some
              #_
              (FStar.Pervasives.Inr #_ #_ (FStar.Pervasives.Native.Mktuple2 #_ #_ e1 e2)) ->
              BoolRefinement.lookup (BoolRefinement.rename_env sg x y) a ==
              FStar.Pervasives.Native.Some
              (FStar.Pervasives.Inr (BoolRefinement.rename e1 x y, BoolRefinement.rename e2 x y)))
          <:
          Type0))
      (decreases sg)
      [SMTPat (BoolRefinement.lookup (BoolRefinement.rename_env sg x y) a)]
BoolRefinement.src_env BoolRefinement.var FStar.Pervasives.Native.tuple2 FStar.Pervasives.either BoolRefinement.s_ty BoolRefinement.src_eqn Prims.list BoolRefinement.rename_lookup Prims.unit Prims.l_True Prims.squash BoolRefinement.lookup Prims.b2t FStar.Pervasives.Native.uu___is_None BoolRefinement.rename_env Prims.eq2 FStar.Pervasives.Native.option FStar.Pervasives.Native.Some FStar.Pervasives.Inl BoolRefinement.s_exp FStar.Pervasives.Inr FStar.Pervasives.Native.Mktuple2 BoolRefinement.rename Prims.Cons FStar.Pervasives.pattern FStar.Pervasives.smt_pat Prims.Nil
let rec rename_lookup (sg: src_env) (a x y: var)
    : Lemma
      (ensures
        (match lookup sg a with
          | None -> None? (lookup (rename_env sg x y) a)
          | Some (Inl t) -> lookup (rename_env sg x y) a == Some (Inl t)
          | Some (Inr (e1, e2)) ->
            lookup (rename_env sg x y) a == Some (Inr (rename e1 x y, rename e2 x y))))
      (decreases sg)
      [SMTPat (lookup (rename_env sg x y) a)] =
  
match sg with
| [] -> ()
| hd :: tl -> rename_lookup tl a x y