val eq_hint_type (ht1 ht2: proof_hint_type) : b: bool{b <==> (ht1 == ht2)}
let eq_hint_type (ht1 ht2:proof_hint_type)
  : b:bool { b <==> (ht1 == ht2) }
  = match ht1, ht2 with
    | ASSERT { p=p1 }, ASSERT { p=p2 } ->
      eq_tm p1 p2
    | FOLD { names=ns1; p=p1}, FOLD { names=ns2; p=p2 }
    | UNFOLD { names=ns1; p=p1}, UNFOLD { names=ns2; p=p2 } ->
      eq_opt (eq_list (fun n1 n2 -> n1 = n2)) ns1 ns2 &&
      eq_tm p1 p2
    | RENAME { pairs=ps1; goal=p1 }, RENAME { pairs=ps2; goal=p2 } ->
      eq_list (fun (x1, y1) (x2, y2) -> eq_tm x1 x2 && eq_tm y1 y2) ps1 ps2 &&
      eq_opt eq_tm p1 p2
    | REWRITE { t1; t2 }, REWRITE { t1=s1; t2=s2 } ->
      eq_tm t1 s1 &&
      eq_tm t2 s2
    | _ -> false
val eq_hint_type (ht1 ht2: proof_hint_type) : b: bool{b <==> (ht1 == ht2)}
let eq_hint_type (ht1 ht2: proof_hint_type) : b: bool{b <==> (ht1 == ht2)} =
match ht1, ht2 with
| ASSERT { p = p1 }, ASSERT { p = p2 } -> eq_tm p1 p2
| FOLD { names = ns1 ; p = p1 }, FOLD { names = ns2 ; p = p2 }
| UNFOLD { names = ns1 ; p = p1 }, UNFOLD { names = ns2 ; p = p2 } ->
  eq_opt (eq_list (fun n1 n2 -> n1 = n2)) ns1 ns2 && eq_tm p1 p2
| RENAME { pairs = ps1 ; goal = p1 }, RENAME { pairs = ps2 ; goal = p2 } ->
  eq_list (fun (x1, y1) (x2, y2) -> eq_tm x1 x2 && eq_tm y1 y2) ps1 ps2 && eq_opt eq_tm p1 p2
| REWRITE { t1 = t1 ; t2 = t2 }, REWRITE { t1 = s1 ; t2 = s2 } -> eq_tm t1 s1 && eq_tm t2 s2
| _ -> false
Pulse.Syntax.Base.fst.checked
prims.fst.checked FStar.Tactics.V2.fst.checked FStar.Sealed.fsti.checked FStar.Reflection.V2.TermEq.fst.checked FStar.Reflection.V2.fst.checked FStar.Reflection.Typing.Builtins.fsti.checked FStar.Reflection.Typing.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked
Pulse.Syntax.Base.fst
Pulse.Syntax.Base.proof_hint_type FStar.Pervasives.Native.Mktuple2 Pulse.Syntax.Base.vprop Pulse.Syntax.Base.eq_tm FStar.Pervasives.Native.option Prims.list Prims.string Prims.op_AmpAmp Pulse.Syntax.Base.eq_opt Pulse.Syntax.Base.eq_list Prims.op_Equality Prims.bool Prims.l_iff Prims.b2t Prims.eq2 FStar.Pervasives.Native.tuple2 Pulse.Syntax.Base.term
module Pulse.Syntax.Base
module RTB = FStar.Reflection.Typing.Builtins
module RT = FStar.Reflection.Typing
module R = FStar.Reflection.V2
module T = FStar.Tactics.V2

let eq_univ (u1 u2:universe) : b:bool{b <==> u1 == u2} =
  let open FStar.Reflection.V2.TermEq in
  assume (faithful_univ u1);
  assume (faithful_univ u2);
  univ_eq_dec u1 u2

let rec eq_tm (t1 t2:term)
  : Tot (b:bool { b <==> (t1 == t2) }) (decreases t1)
  = match t1.t, t2.t with
    | Tm_VProp, Tm_VProp
    | Tm_Emp, Tm_Emp
    | Tm_Inames, Tm_Inames
    | Tm_EmpInames, Tm_EmpInames
    | Tm_Unknown, Tm_Unknown -> true
    | Tm_Star l1 r1, Tm_Star l2 r2 ->
      eq_tm l1 l2 &&
      eq_tm r1 r2
    | Tm_Pure p1, Tm_Pure p2 ->
      eq_tm p1 p2
    | Tm_ExistsSL u1 t1 b1, Tm_ExistsSL u2 t2 b2
    | Tm_ForallSL u1 t1 b1, Tm_ForallSL u2 t2 b2 ->
      eq_univ u1 u2 &&
      eq_tm t1.binder_ty t2.binder_ty &&
      eq_tm b1 b2
    | Tm_FStar t1, Tm_FStar t2 ->
      let open FStar.Reflection.V2.TermEq in
      assume (faithful t1);
      assume (faithful t2);
      term_eq_dec t1 t2
    | _ -> false

let eq_st_comp (s1 s2:st_comp)  
  : b:bool { b <==> (s1 == s2) }
  = eq_univ s1.u s2.u &&
    eq_tm s1.res s2.res &&
    eq_tm s1.pre s2.pre &&
    eq_tm s1.post s2.post

let eq_comp (c1 c2:comp)
  : b:bool { b <==> (c1 == c2) }
  = match c1, c2 with
    | C_Tot t1, C_Tot t2 ->
      eq_tm t1 t2
    | C_ST s1, C_ST s2 ->
      eq_st_comp s1 s2
    | C_STAtomic i1 s1, C_STAtomic i2 s2
    | C_STGhost i1 s1, C_STGhost i2 s2 ->
      eq_tm i1 i2 &&
      eq_st_comp s1 s2
    | _ -> false

let rec eq_list (f: (x:'a -> y:'a -> b:bool { b <==> (x == y)})) (l m:list 'a)
  : b:bool { b <==> (l == m) }
  = match l, m with
    | [], [] -> true
    | h1::t1, h2::t2 ->
      f h1 h2 &&
      eq_list f t1 t2
    | _ -> false

let eq_opt (f: (x:'a -> y:'a -> b:bool { b <==> (x == y)})) (l m:option 'a)
  : b:bool { b <==> (l == m) }
  = match l, m with
    | None, None -> true
    | Some l, Some m -> f l m
    | _ -> false

let eq_tm_opt (t1 t2:option term)
  : b:bool { b <==> (t1 == t2) }
  = eq_opt eq_tm t1 t2

let eq_comp_opt (c1 c2:option comp)
  : b:bool { b <==> (c1 == c2) }
  = eq_opt eq_comp c1 c2

let rec eq_list_dec top1 top2
   (f: (x:'a -> y:'a{x << top1 /\ y << top2} -> b:bool { b <==> (x == y)}))
   (l : list 'a{l << top1})
   (m : list 'a{m << top2})
  : b:bool { b <==> (l == m) }
  = match l, m with
    | [], [] -> true
    | h1::t1, h2::t2 ->
      f h1 h2 &&
      eq_list_dec top1 top2 f t1 t2
    | _ -> false

let eq_binder (b0 b1:binder) : b:bool { b <==> (b0 == b1) } =
  eq_tm b0.binder_ty b1.binder_ty

let eq_tm_list (t1 t2:list term) = eq_list eq_tm t1 t2

// wire to Reflection.TermEq
assume val fstar_const_eq : c1:R.vconst -> c2:R.vconst -> b:bool{b <==> (c1==c2)}

let rec sealed_list_eq #a (l1 l2 : list (Sealed.sealed a))
  : Lemma ((length l1 = length l2) ==> (l1 == l2))
  = match l1, l2 with
    | [], [] -> ()
    | h1::t1, h2::t2 ->
      Sealed.sealed_singl h1 h2;
      sealed_list_eq t1 t2
    | _ -> ()

let rec eq_pattern (p1 p2 : pattern) : b:bool{ b <==> (p1 == p2) } =
  match p1, p2 with
  | Pat_Cons f1 vs1,
    Pat_Cons f2 vs2 ->
    f1.fv_name = f2.fv_name &&
    eq_list_dec p1 p2 eq_sub_pat vs1 vs2

  | Pat_Constant c1, Pat_Constant c2 ->
    fstar_const_eq c1 c2

  | Pat_Var _ _, Pat_Var _ _ -> true
  
  | Pat_Dot_Term to1, Pat_Dot_Term to2 -> eq_opt eq_tm to1 to2

  | _ -> false

and eq_sub_pat (pb1 pb2 : pattern & bool) : b:bool{b <==> pb1 == pb2} =
  let (p1, b1) = pb1 in
  let (p2, b2) = pb2 in
  eq_pattern p1 p2 && b1 = b2

let eq_hint_type (ht1 ht2:proof_hint_type)
val eq_hint_type (ht1 ht2: proof_hint_type) : b: bool{b <==> (ht1 == ht2)}
ht1: Pulse.Syntax.Base.proof_hint_type -> ht2: Pulse.Syntax.Base.proof_hint_type
  -> b: Prims.bool{b <==> ht1 == ht2}