val lookup_mem (e: list (var & 'a)) (x: var)
    : Lemma (requires Some? (lookup e x)) (ensures exists elt. L.memP elt e /\ fst elt == x)
val lookup_mem (e: list (var & 'a)) (x: var)
    : Lemma (requires Some? (lookup e x)) (ensures exists elt. L.memP elt e /\ fst elt == x)
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 ()
        )
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
/
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
e: Prims.list (BoolRefinement.var * 'a) -> x: BoolRefinement.var
  -> FStar.Pervasives.Lemma (requires Some? (BoolRefinement.lookup e x))
      (ensures
        exists (elt: (BoolRefinement.var * 'a)).
          FStar.List.Tot.Base.memP elt e /\ FStar.Pervasives.Native.fst elt == x)
Prims.list FStar.Pervasives.Native.tuple2 BoolRefinement.var BoolRefinement.lookup Prims._assert FStar.List.Tot.Base.memP FStar.Pervasives.Native.option FStar.Classical.Sugar.exists_elim Prims.l_and Prims.eq2 FStar.Pervasives.Native.fst Prims.l_Exists Prims.squash FStar.Classical.Sugar.exists_intro Prims.unit BoolRefinement.lookup_mem Prims.b2t FStar.Pervasives.Native.uu___is_Some Prims.Nil FStar.Pervasives.pattern
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 ())