val compute_gen_elim_nondep_a' (ty: list Type0) : Tot Type0
let compute_gen_elim_nondep_a' (ty: list Type0) : Tot Type0 =
    match ty with
    | [] -> unit
    | [t1] -> t1
    | [t1; t2] -> tuple2 t1 t2
    | [t1; t2; t3] -> tuple3 t1 t2 t3
    | [t1; t2; t3; t4] -> tuple4 t1 t2 t3 t4
    | [t1; t2; t3; t4; t5] -> tuple5 t1 t2 t3 t4 t5
    | [t1; t2; t3; t4; t5; t6] -> tuple6 t1 t2 t3 t4 t5 t6
    | [t1; t2; t3; t4; t5; t6; t7] -> tuple7 t1 t2 t3 t4 t5 t6 t7
    | [t1; t2; t3; t4; t5; t6; t7; t8] -> tuple8 t1 t2 t3 t4 t5 t6 t7 t8
    | [t1; t2; t3; t4; t5; t6; t7; t8; t9] -> tuple9 t1 t2 t3 t4 t5 t6 t7 t8 t9
    | [t1; t2; t3; t4; t5; t6; t7; t8; t9; t10] -> tuple10 t1 t2 t3 t4 t5 t6 t7 t8 t9 t10
    | [t1; t2; t3; t4; t5; t6; t7; t8; t9; t10; t11] -> tuple11 t1 t2 t3 t4 t5 t6 t7 t8 t9 t10 t11
    | [t1; t2; t3; t4; t5; t6; t7; t8; t9; t10; t11; t12] -> tuple12 t1 t2 t3 t4 t5 t6 t7 t8 t9 t10 t11 t12
    | [t1; t2; t3; t4; t5; t6; t7; t8; t9; t10; t11; t12; t13] -> tuple13 t1 t2 t3 t4 t5 t6 t7 t8 t9 t10 t11 t12 t13
    | [t1; t2; t3; t4; t5; t6; t7; t8; t9; t10; t11; t12; t13; t14] -> tuple14 t1 t2 t3 t4 t5 t6 t7 t8 t9 t10 t11 t12 t13 t14
    | _ -> unit
val compute_gen_elim_nondep_a' (ty: list Type0) : Tot Type0
let compute_gen_elim_nondep_a' (ty: list Type0) : Tot Type0 =
match ty with
| [] -> unit
| [t1] -> t1
| [t1 ; t2] -> tuple2 t1 t2
| [t1 ; t2 ; t3] -> tuple3 t1 t2 t3
| [t1 ; t2 ; t3 ; t4] -> tuple4 t1 t2 t3 t4
| [t1 ; t2 ; t3 ; t4 ; t5] -> tuple5 t1 t2 t3 t4 t5
| [t1 ; t2 ; t3 ; t4 ; t5 ; t6] -> tuple6 t1 t2 t3 t4 t5 t6
| [t1 ; t2 ; t3 ; t4 ; t5 ; t6 ; t7] -> tuple7 t1 t2 t3 t4 t5 t6 t7
| [t1 ; t2 ; t3 ; t4 ; t5 ; t6 ; t7 ; t8] -> tuple8 t1 t2 t3 t4 t5 t6 t7 t8
| [t1 ; t2 ; t3 ; t4 ; t5 ; t6 ; t7 ; t8 ; t9] -> tuple9 t1 t2 t3 t4 t5 t6 t7 t8 t9
| [t1 ; t2 ; t3 ; t4 ; t5 ; t6 ; t7 ; t8 ; t9 ; t10] -> tuple10 t1 t2 t3 t4 t5 t6 t7 t8 t9 t10
| [t1 ; t2 ; t3 ; t4 ; t5 ; t6 ; t7 ; t8 ; t9 ; t10 ; t11] ->
  tuple11 t1 t2 t3 t4 t5 t6 t7 t8 t9 t10 t11
| [t1 ; t2 ; t3 ; t4 ; t5 ; t6 ; t7 ; t8 ; t9 ; t10 ; t11 ; t12] ->
  tuple12 t1 t2 t3 t4 t5 t6 t7 t8 t9 t10 t11 t12
| [t1 ; t2 ; t3 ; t4 ; t5 ; t6 ; t7 ; t8 ; t9 ; t10 ; t11 ; t12 ; t13] ->
  tuple13 t1 t2 t3 t4 t5 t6 t7 t8 t9 t10 t11 t12 t13
| [t1 ; t2 ; t3 ; t4 ; t5 ; t6 ; t7 ; t8 ; t9 ; t10 ; t11 ; t12 ; t13 ; t14] ->
  tuple14 t1 t2 t3 t4 t5 t6 t7 t8 t9 t10 t11 t12 t13 t14
| _ -> unit
Steel.ST.GenElim.Base.fsti.checked
Steel.ST.Util.fsti.checked Steel.Effect.Common.fsti.checked prims.fst.checked FStar.Tactics.fst.checked FStar.Reflection.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked FStar.Ghost.fsti.checked
Steel.ST.GenElim.Base.fsti
Prims.list Prims.unit FStar.Pervasives.Native.tuple2 FStar.Pervasives.Native.tuple3 FStar.Pervasives.Native.tuple4 FStar.Pervasives.Native.tuple5 FStar.Pervasives.Native.tuple6 FStar.Pervasives.Native.tuple7 FStar.Pervasives.Native.tuple8 FStar.Pervasives.Native.tuple9 FStar.Pervasives.Native.tuple10 FStar.Pervasives.Native.tuple11 FStar.Pervasives.Native.tuple12 FStar.Pervasives.Native.tuple13 FStar.Pervasives.Native.tuple14
module Steel.ST.GenElim.Base
include Steel.ST.Util

module T = FStar.Tactics

let is_fvar     = Reflection.is_fvar
let is_any_fvar = Reflection.is_any_fvar

/// A tactic to automatically generate a unique binder

[@@erasable]
noeq
type gen_unit_elim_i
= | GUEId: (v: vprop) -> gen_unit_elim_i
  | GUEPure: (p: prop) -> gen_unit_elim_i
  | GUEStar: (left: gen_unit_elim_i) -> (right: gen_unit_elim_i) -> gen_unit_elim_i

[@@erasable]
noeq
type gen_elim_i =
  | GEUnit: (i: gen_unit_elim_i) -> gen_elim_i
  | GEStarL: (left: gen_elim_i) -> (right: gen_unit_elim_i) -> gen_elim_i
  | GEStarR: (left: gen_unit_elim_i) -> (right: gen_elim_i) -> gen_elim_i
  | GEStar: (left: gen_elim_i) -> (right: gen_elim_i) -> gen_elim_i
  | GEExistsNoAbs: (#a: Type0) -> (body: (a -> vprop)) -> gen_elim_i // FIXME: generalize the universe
  | GEExistsUnit: (#a: Type0) -> (body: (a -> gen_unit_elim_i)) -> gen_elim_i
  | GEExists: (#a: Type0) -> (body: (a -> gen_elim_i)) -> gen_elim_i

val gen_elim_reduce: unit

[@@ gen_elim_reduce]
let rec compute_gen_unit_elim_p
  (x: gen_unit_elim_i)
: Tot vprop
= match x with
  | GUEId v -> v
  | GUEPure p -> pure p
  | GUEStar left right -> compute_gen_unit_elim_p left `star` compute_gen_unit_elim_p right

[@@ gen_elim_reduce]
let rec compute_gen_unit_elim_q
  (x: gen_unit_elim_i)
: Tot vprop
= match x with
  | GUEId v -> v
  | GUEPure _ -> emp
  | GUEStar left right -> compute_gen_unit_elim_q left `star` compute_gen_unit_elim_q right

[@@gen_elim_reduce; noextract_to "Plugin"]
let rec compute_gen_unit_elim_post
  (x: gen_unit_elim_i)
: Tot prop
= match x with
  | GUEId _ -> True
  | GUEPure p -> p
  | GUEStar left right -> compute_gen_unit_elim_post left /\ compute_gen_unit_elim_post right

[@@gen_elim_reduce]
let rec compute_gen_elim_p
  (x: gen_elim_i)
: Tot vprop
= match x with
  | GEUnit i -> compute_gen_unit_elim_p i
  | GEStarL left right -> compute_gen_elim_p left `star` compute_gen_unit_elim_p right
  | GEStarR left right -> compute_gen_unit_elim_p left `star` compute_gen_elim_p right
  | GEStar left right -> compute_gen_elim_p left `star` compute_gen_elim_p right
  | GEExistsNoAbs #a p -> exists_ p
  | GEExistsUnit #a p -> exists_ (fun x -> compute_gen_unit_elim_p (p x))
  | GEExists #a body -> exists_ (fun x -> compute_gen_elim_p (body x))

let compute_gen_elim_p' = compute_gen_elim_p

[@@ gen_elim_reduce; __steel_reduce__; noextract_to "Plugin"]
let rec compute_gen_elim_a
  (x: gen_elim_i)
: Tot Type0
= match x with
  | GEUnit _ -> unit
  | GEStarL left _ -> compute_gen_elim_a left
  | GEStarR _ right -> compute_gen_elim_a right
  | GEStar left right -> (compute_gen_elim_a left & compute_gen_elim_a right)
  | GEExistsNoAbs #a _
  | GEExistsUnit #a _ -> a
  | GEExists #a body -> dtuple2 a (fun x -> compute_gen_elim_a (body x))

[@@noextract_to "Plugin"]
let dfstp #a #b t = dfst #a #b t
[@@noextract_to "Plugin"]
let dsndp #a #b t = dsnd #a #b t
[@@noextract_to "Plugin"]
let fstp #a #b t = fst #a #b t
[@@noextract_to "Plugin"]
let sndp #a #b t = snd #a #b t

[@@gen_elim_reduce; __steel_reduce__; noextract_to "Plugin"]
let coerce_with_trefl (#tfrom #tto: Type) (x: tfrom) : Pure tto (requires (T.with_tactic T.trefl (tfrom == tto))) (ensures (fun _ -> True)) = x

[@@gen_elim_reduce]
let rec compute_gen_elim_q
  (x: gen_elim_i)
: Tot (compute_gen_elim_a x -> Tot vprop)
  (decreases x)
= match x as x' returns (compute_gen_elim_a x' -> Tot vprop) with
  | GEUnit u -> fun _ -> compute_gen_unit_elim_q u
  | GEStarL left right -> fun v -> compute_gen_elim_q left (coerce_with_trefl v) `star` compute_gen_unit_elim_q right
  | GEStarR left right -> fun v -> compute_gen_unit_elim_q left `star` compute_gen_elim_q right (coerce_with_trefl v)
  | GEStar left right ->
    let tleft = compute_gen_elim_a left in
    let tright = compute_gen_elim_a right in
    fun v ->
      let v' : (tleft & tright) = coerce_with_trefl v in
      compute_gen_elim_q left (fstp #tleft #tright v') `star` compute_gen_elim_q right (sndp #tleft #tright v')
  | GEExistsNoAbs #a p -> p
  | GEExistsUnit #a p -> fun v -> compute_gen_unit_elim_q (p v)
  | GEExists #a body ->
    let dept = (fun x -> compute_gen_elim_a (body x)) in
    fun v ->
    let v' : dtuple2 a dept = coerce_with_trefl v in
    compute_gen_elim_q
      (body (dfstp #a #dept v'))
      (dsndp #a #dept v')

[@@gen_elim_reduce; noextract_to "Plugin"]
let rec compute_gen_elim_post
  (x: gen_elim_i)
: Tot (compute_gen_elim_a x -> Tot prop)
  (decreases x)
= match x as x' returns (compute_gen_elim_a x' -> Tot prop) with
  | GEUnit u -> fun _ -> compute_gen_unit_elim_post u
  | GEStarL left right -> fun v -> compute_gen_elim_post left (coerce_with_trefl v) /\ compute_gen_unit_elim_post right
  | GEStarR left right -> fun v -> compute_gen_unit_elim_post left /\ compute_gen_elim_post right (coerce_with_trefl v)
  | GEStar left right ->
    let tleft = compute_gen_elim_a left in
    let tright = compute_gen_elim_a right in
    fun v ->
      let v' : (tleft & tright) = coerce_with_trefl v in
      compute_gen_elim_post left (fstp #tleft #tright v') /\ compute_gen_elim_post right (sndp #tleft #tright v')
  | GEExistsNoAbs #a p -> fun _ -> True
  | GEExistsUnit #a p -> fun v -> compute_gen_unit_elim_post (p v)
  | GEExists #a body ->
    let dept = (fun x -> compute_gen_elim_a (body x)) in
    fun v ->
    let v' : dtuple2 a dept = coerce_with_trefl v in
    compute_gen_elim_post
      (body (dfstp #a #dept v'))
      (dsndp #a #dept v')

[@@erasable]
noeq
type gen_elim_tele =
  | TRet: vprop -> prop -> gen_elim_tele
  | TExists: (ty: Type u#0) -> (ty -> gen_elim_tele) -> gen_elim_tele

[@@gen_elim_reduce]
let rec tele_star_vprop (i: gen_elim_tele) (v: vprop) (p: prop) : Tot gen_elim_tele (decreases i) =
  match i with
  | TRet v' p' -> TRet (v `star` v') (p /\ p')
  | TExists ty f -> TExists ty (fun x -> tele_star_vprop (f x) v p)

[@@gen_elim_reduce]
let rec tele_star (i1 i2: gen_elim_tele) : Tot gen_elim_tele =
  match i1, i2 with
  | TRet v1 p1, _ -> tele_star_vprop i2 v1 p1
  | _, TRet v2 p2 -> tele_star_vprop i1 v2 p2
  | TExists ty1 f1, TExists ty2 f2 -> TExists ty1 (fun x1 -> TExists ty2 (fun x2 -> tele_star (f1 x1) (f2 x2)))

[@@gen_elim_reduce]
let rec compute_gen_elim_tele (x: gen_elim_i) : Tot gen_elim_tele =
  match x with
  | GEUnit v -> TRet (compute_gen_unit_elim_q v) (compute_gen_unit_elim_post v)
  | GEStarL l ru -> tele_star_vprop (compute_gen_elim_tele l) (compute_gen_unit_elim_q ru) (compute_gen_unit_elim_post ru)
  | GEStarR lu r -> tele_star_vprop (compute_gen_elim_tele r) (compute_gen_unit_elim_q lu) (compute_gen_unit_elim_post lu)
  | GEStar l r -> tele_star (compute_gen_elim_tele l) (compute_gen_elim_tele r)
  | GEExistsNoAbs #ty body -> TExists ty (fun x -> TRet (body x) True)
  | GEExistsUnit #ty body -> TExists ty (fun x -> TRet (compute_gen_unit_elim_q (body x)) (compute_gen_unit_elim_post (body x)))
  | GEExists #ty f -> TExists ty (fun x -> compute_gen_elim_tele (f x))

[@@gen_elim_reduce; noextract_to "Plugin"]
let rec curried_function_type (x: list (Type u#a)) (ret_t: Type u#(max a b)) : Tot (Type u#(max a b)) =
  match x with
  | [] -> ret_t
  | t1 :: q -> t1 -> Tot (curried_function_type q ret_t)

[@@erasable]
noeq
type gen_elim_nondep_t =
| GENonDep: (ty: list Type0) -> curried_function_type ty vprop -> curried_function_type ty prop -> gen_elim_nondep_t
| GEDep

[@@gen_elim_reduce]
let mk_gen_elim_nondep
  (ty: list Type0)
  (tvprop: Type)
  (q: tvprop)
  (tprop: Type)
  (post: tprop)
: Pure gen_elim_nondep_t
  (requires (
    tvprop == curried_function_type ty vprop /\
    tprop == curried_function_type ty prop
  ))
  (ensures (fun _ -> True))
= GENonDep ty q post

[@@gen_elim_reduce]
let mk_gen_elim_nondep_by_tac
  (ty: list Type0)
  (tvprop: Type)
  (q: tvprop)
  (tprop: Type)
  (post: tprop)
: Pure gen_elim_nondep_t
  (requires (
    T.with_tactic (fun _ -> T.norm [delta_attr [(`%gen_elim_reduce)]; iota; zeta]) (tvprop == curried_function_type ty vprop) /\
    T.with_tactic (fun _ -> T.norm [delta_attr [(`%gen_elim_reduce)]; iota; zeta]) (tprop == curried_function_type ty prop)
  ))
  (ensures (fun _ -> True))
= GENonDep ty q post

[@@gen_elim_reduce]
let rec gen_elim_nondep_sem (ty: list Type0) : Tot (curried_function_type ty vprop -> curried_function_type ty prop -> Tot gen_elim_tele) =
  match ty as ty' returns curried_function_type ty' vprop -> curried_function_type ty' prop -> Tot gen_elim_tele with
  | [] -> fun q post -> TRet q post
  | t :: tq -> fun q post -> TExists t (fun x -> gen_elim_nondep_sem tq (q x) (post x))

[@@gen_elim_reduce; noextract_to "Plugin"]
let check_gen_elim_nondep_sem (i: gen_elim_i) (nd: gen_elim_nondep_t) : Tot prop =
  match nd with
  | GENonDep ty q post -> compute_gen_elim_tele i == gen_elim_nondep_sem ty q post
  | GEDep -> True

[@@gen_elim_reduce; noextract_to "Plugin"]
val compute_gen_elim_nondep_a' (ty: list Type0) : Tot Type0
ty: Prims.list Type0 -> Type0