val tele_star_vprop_correct_exists
      (v: vprop)
      (p: prop)
      (ty: _)
      (body: (ty -> gen_elim_tele))
      (ih:
          (x: ty
              -> GTot
                (vprop_rewrite (((tele_p (body x)) `star` v) `star` (pure p))
                    (tele_p (tele_star_vprop (body x) v p)))))
    : Tot
    (vprop_rewrite (((tele_p (TExists ty body)) `star` v) `star` (pure p))
        (tele_p (tele_star_vprop (TExists ty body) v p)))
let tele_star_vprop_correct_exists
  (v: vprop) (p: prop)
  (ty: _) (body: ty -> gen_elim_tele) (ih: (x: ty) -> GTot (vprop_rewrite (tele_p (body x) `star` v `star` pure p) (tele_p (tele_star_vprop (body x) v p))))
: Tot (vprop_rewrite (tele_p (TExists ty body) `star` v `star` pure p) (tele_p (tele_star_vprop (TExists ty body) v p)))
= fun _ ->
    rewrite_with_trefl (tele_p _) (exists_ (fun x -> tele_p (body x)));
    let x = elim_exists' () in
    ih x _;
    intro_exists x (fun x -> tele_p (tele_star_vprop (body x) v p));
    rewrite_with_trefl (exists_ (fun x -> tele_p (tele_star_vprop (body x) v p))) (tele_p _)
val tele_star_vprop_correct_exists
      (v: vprop)
      (p: prop)
      (ty: _)
      (body: (ty -> gen_elim_tele))
      (ih:
          (x: ty
              -> GTot
                (vprop_rewrite (((tele_p (body x)) `star` v) `star` (pure p))
                    (tele_p (tele_star_vprop (body x) v p)))))
    : Tot
    (vprop_rewrite (((tele_p (TExists ty body)) `star` v) `star` (pure p))
        (tele_p (tele_star_vprop (TExists ty body) v p)))
let tele_star_vprop_correct_exists
      (v: vprop)
      (p: prop)
      (ty: _)
      (body: (ty -> gen_elim_tele))
      (ih:
          (x: ty
              -> GTot
                (vprop_rewrite (((tele_p (body x)) `star` v) `star` (pure p))
                    (tele_p (tele_star_vprop (body x) v p)))))
    : Tot
    (vprop_rewrite (((tele_p (TExists ty body)) `star` v) `star` (pure p))
        (tele_p (tele_star_vprop (TExists ty body) v p))) =
fun _ ->
  rewrite_with_trefl (tele_p _) (exists_ (fun x -> tele_p (body x)));
  let x = elim_exists' () in
  ih x _;
  intro_exists x (fun x -> tele_p (tele_star_vprop (body x) v p));
  rewrite_with_trefl (exists_ (fun x -> tele_p (tele_star_vprop (body x) v p))) (tele_p _)
Steel.ST.GenElim.fst.checked
prims.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Ghost.fsti.checked FStar.Classical.fsti.checked
Steel.ST.GenElim.fst
Steel.Effect.Common.vprop Prims.prop Steel.ST.GenElim.Base.gen_elim_tele Steel.ST.GenElim.vprop_rewrite Steel.Effect.Common.star Steel.ST.GenElim.tele_p Steel.ST.Util.pure Steel.ST.GenElim.Base.tele_star_vprop Steel.Memory.inames Steel.ST.GenElim.rewrite_with_trefl Steel.ST.Util.exists_ Steel.ST.GenElim.Base.TExists Prims.unit Steel.ST.Util.intro_exists Steel.ST.GenElim.elim_exists'
module Steel.ST.GenElim

let gen_elim_f
  (p: vprop)
  (a: Type0) // FIXME: generalize this universe
  (q: (a -> vprop))
  (post: (a -> prop))
: Tot Type
= ((opened: inames) -> STGhost a opened p q True post)

let gen_unit_elim_t (i: gen_unit_elim_i) : Tot Type =
  gen_elim_f (compute_gen_unit_elim_p i) unit (fun _ -> compute_gen_unit_elim_q i) (fun _ -> compute_gen_unit_elim_post i)

let compute_gen_unit_elim_f_id
  (v: vprop)
: Tot (gen_unit_elim_t (GUEId v))
= fun _ -> noop ()

let compute_gen_unit_elim_f_pure
  (p: prop)
: Tot (gen_unit_elim_t (GUEPure p))
= fun _ ->
  rewrite (compute_gen_unit_elim_p (GUEPure p)) (pure p);
  elim_pure p

let compute_gen_unit_elim_f_star
  (i1 i2: gen_unit_elim_i)
  (f1: gen_unit_elim_t i1)
  (f2: gen_unit_elim_t i2)
: Tot (gen_unit_elim_t (GUEStar i1 i2))
= fun _ ->
  rewrite (compute_gen_unit_elim_p (GUEStar i1 i2)) (compute_gen_unit_elim_p i1 `star` compute_gen_unit_elim_p i2);
  f1 _; f2 _;
  rewrite (compute_gen_unit_elim_q i1 `star` compute_gen_unit_elim_q i2) (compute_gen_unit_elim_q (GUEStar i1 i2))

let rec compute_gen_unit_elim_f
  (i: gen_unit_elim_i)
: GTot (gen_unit_elim_t i)
= match i returns (gen_unit_elim_t i) with
  | GUEId v -> compute_gen_unit_elim_f_id v
  | GUEPure p -> compute_gen_unit_elim_f_pure p
  | GUEStar i1 i2 -> compute_gen_unit_elim_f_star i1 i2 (compute_gen_unit_elim_f i1) (compute_gen_unit_elim_f i2)

let gen_elim_t (i: gen_elim_i) : Tot Type =
  gen_elim_f (compute_gen_elim_p i) (compute_gen_elim_a i) (compute_gen_elim_q i) (compute_gen_elim_post i)

let compute_gen_elim_f_unit
  (i: gen_unit_elim_i)
: GTot (gen_elim_t (GEUnit i))
= compute_gen_unit_elim_f i

let compute_gen_elim_f_star_l
  (i1: gen_elim_i)
  (f1: gen_elim_t i1)
  (i2: gen_unit_elim_i)
: GTot (gen_elim_t (GEStarL i1 i2))
= let f2 = compute_gen_unit_elim_f i2 in
  fun _ ->
  rewrite (compute_gen_elim_p (GEStarL i1 i2)) (compute_gen_elim_p i1 `star` compute_gen_unit_elim_p i2);
  let res = f1 _ in
  f2 _;
  let res' : compute_gen_elim_a (GEStarL i1 i2) = coerce_with_trefl res in
  rewrite (compute_gen_elim_q i1 res `star` compute_gen_unit_elim_q i2) (compute_gen_elim_q (GEStarL i1 i2) res');
  res'

let compute_gen_elim_f_star_r
  (i1: gen_unit_elim_i)
  (i2: gen_elim_i)
  (f2: gen_elim_t i2)
: GTot (gen_elim_t (GEStarR i1 i2))
= let f1 = compute_gen_unit_elim_f i1 in
  fun _ ->
  rewrite (compute_gen_elim_p (GEStarR i1 i2)) (compute_gen_unit_elim_p i1 `star` compute_gen_elim_p i2);
  f1 _;
  let res = f2 _ in
  let res' : compute_gen_elim_a (GEStarR i1 i2) = coerce_with_trefl res in
  rewrite (compute_gen_unit_elim_q i1 `star` compute_gen_elim_q i2 res) (compute_gen_elim_q (GEStarR i1 i2) res');
  res'

let compute_gen_elim_f_star
  (i1: gen_elim_i)
  (f1: gen_elim_t i1)
  (i2: gen_elim_i)
  (f2: gen_elim_t i2)
: GTot (gen_elim_t (GEStar i1 i2))
= fun _ ->
  rewrite (compute_gen_elim_p (GEStar i1 i2)) (compute_gen_elim_p i1 `star` compute_gen_elim_p i2);
  let res1 = f1 _ in
  let res2 = f2 _ in
  let res : compute_gen_elim_a (GEStar i1 i2) = coerce_with_trefl (res1, res2) in
  rewrite (compute_gen_elim_q i1 res1 `star` compute_gen_elim_q i2 res2) (compute_gen_elim_q (GEStar i1 i2) res);
  res

let compute_gen_elim_f_exists_no_abs
  (a: Type0)
  (body: (a -> vprop))
: GTot (gen_elim_t (GEExistsNoAbs body))
= fun _ ->
  rewrite (compute_gen_elim_p (GEExistsNoAbs body)) (exists_ body);
  let gres = elim_exists () in
  let res : compute_gen_elim_a (GEExistsNoAbs body) = coerce_with_trefl (Ghost.reveal gres) in
  rewrite (body gres) (compute_gen_elim_q (GEExistsNoAbs body) res);
  res

let rewrite_with_trefl (#opened:_) (p q:vprop)
  : STGhost unit opened
      p
      (fun _ -> q)
      (requires T.with_tactic T.trefl (p == q))
      (ensures fun _ -> True)
= rewrite p q

let compute_gen_elim_f_exists_unit
  (a: Type0)
  (body: a -> gen_unit_elim_i)
: Tot (gen_elim_t (GEExistsUnit body))
= fun _ ->
  rewrite_with_trefl (compute_gen_elim_p (GEExistsUnit body)) (exists_ (fun x -> compute_gen_unit_elim_p (body x)));
  let gres = elim_exists () in
  compute_gen_unit_elim_f (body gres) _;
  let res : compute_gen_elim_a (GEExistsUnit body) = coerce_with_trefl (Ghost.reveal gres) in
  rewrite (compute_gen_unit_elim_q (body gres)) (compute_gen_elim_q (GEExistsUnit body) res);
  res

let compute_gen_elim_f_exists
  (a: Type0)
  (body: a -> gen_elim_i)
  (f: (x: a) -> GTot (gen_elim_t (body x)))
: Tot (gen_elim_t (GEExists body))
= fun _ ->
  rewrite_with_trefl (compute_gen_elim_p (GEExists body)) (exists_ (fun x -> compute_gen_elim_p (body x)));
  let gres1 = elim_exists () in
  let gres2 = f gres1 _ in
  let res : compute_gen_elim_a (GEExists body) = coerce_with_trefl (Mkdtuple2 #a #(fun x -> compute_gen_elim_a (body x)) (Ghost.reveal gres1) (Ghost.reveal gres2)) in
  rewrite (compute_gen_elim_q (body gres1) gres2) (compute_gen_elim_q (GEExists body) res);
  res

let rec compute_gen_elim_f
  (i: gen_elim_i)
: GTot (gen_elim_t i)
= match i returns (gen_elim_t i) with
  | GEUnit i -> compute_gen_elim_f_unit i
  | GEStarL i1 i2 -> compute_gen_elim_f_star_l i1 (compute_gen_elim_f i1) i2
  | GEStarR i1 i2 -> compute_gen_elim_f_star_r i1 i2 (compute_gen_elim_f i2)
  | GEStar i1 i2 -> compute_gen_elim_f_star i1 (compute_gen_elim_f i1) i2 (compute_gen_elim_f i2)
  | GEExistsNoAbs body -> compute_gen_elim_f_exists_no_abs _ body
  | GEExistsUnit body -> compute_gen_elim_f_exists_unit _ body
  | GEExists body -> compute_gen_elim_f_exists _ body (fun x -> compute_gen_elim_f (body x))

let rec tele_p (x: gen_elim_tele) : Tot vprop =
  match x with
  | TRet v p -> v `star` pure p
  | TExists ty body -> exists_ (fun x -> tele_p (body x))

let elim_exists' (#a:Type)
                (#opened_invariants:_)
                (#p:a -> vprop)
                (_:unit)
  : STGhostT (a) opened_invariants
             (exists_ p)
             (fun x -> p x)
= let gx = elim_exists () in
  let x = Ghost.reveal gx in
  rewrite (p gx) (p x);
  x

let vprop_rewrite (from to: vprop) : Tot Type =
  gen_elim_f from unit (fun _ -> to) (fun _ -> True)

let tele_star_vprop_correct_ret
  (v': vprop) (p': prop) (v: vprop) (p: prop)
: Tot (vprop_rewrite (tele_p (TRet v' p') `star` v `star` pure p) (tele_p (tele_star_vprop (TRet v' p') v p)))
= fun _ ->
    elim_pure p;
    rewrite (tele_p _) (v' `star` pure p');
    elim_pure p';
    intro_pure (p /\ p');
    rewrite ((v `star` v') `star` pure (p /\ p')) (tele_p _)

let tele_star_vprop_correct_exists
  (v: vprop) (p: prop)
  (ty: _) (body: ty -> gen_elim_tele) (ih: (x: ty) -> GTot (vprop_rewrite (tele_p (body x) `star` v `star` pure p) (tele_p (tele_star_vprop (body x) v p))))
val tele_star_vprop_correct_exists
      (v: vprop)
      (p: prop)
      (ty: _)
      (body: (ty -> gen_elim_tele))
      (ih:
          (x: ty
              -> GTot
                (vprop_rewrite (((tele_p (body x)) `star` v) `star` (pure p))
                    (tele_p (tele_star_vprop (body x) v p)))))
    : Tot
    (vprop_rewrite (((tele_p (TExists ty body)) `star` v) `star` (pure p))
        (tele_p (tele_star_vprop (TExists ty body) v p)))

    v: Steel.Effect.Common.vprop ->
    p: Prims.prop ->
    ty: Type0 ->
    body: (_: ty -> Steel.ST.GenElim.Base.gen_elim_tele) ->
    ih:
      (x: ty
          -> Prims.GTot
            (Steel.ST.GenElim.vprop_rewrite (Steel.Effect.Common.star (Steel.Effect.Common.star (Steel.ST.GenElim.tele_p
                            (body x))
                        v)
                    (Steel.ST.Util.pure p))
                (Steel.ST.GenElim.tele_p (Steel.ST.GenElim.Base.tele_star_vprop (body x) v p))))
  -> Steel.ST.GenElim.vprop_rewrite (Steel.Effect.Common.star (Steel.Effect.Common.star (Steel.ST.GenElim.tele_p
                  (Steel.ST.GenElim.Base.TExists ty body))
              v)
          (Steel.ST.Util.pure p))
      (Steel.ST.GenElim.tele_p (Steel.ST.GenElim.Base.tele_star_vprop (Steel.ST.GenElim.Base.TExists
                  ty body)
              v
              p))