Revision 9d08a76fb50773e0b6b1afad31f37dfb821fee75 authored by Benjamin Gregoire on 24 November 2022, 16:10:02 UTC, committed by Benjamin Gregoire on 24 November 2022, 16:10:02 UTC
1 parent 69c9c2e
Raw File
ecLowGoal.ml
(* -------------------------------------------------------------------- *)
open EcUtils
open EcLocation
open EcIdent
open EcSymbols
open EcPath
open EcTypes
open EcFol
open EcEnv
open EcMatching
open EcReduction
open EcCoreGoal
open EcBaseLogic
open EcProofTerm

module EP  = EcParsetree
module ER  = EcReduction
module TTC = EcProofTyping
module LG  = EcCoreLib.CI_Logic
module PT  = EcProofTerm

(* -------------------------------------------------------------------- *)
let (@!) (t1 : FApi.backward) (t2 : FApi.backward) =
  FApi.t_seq t1 t2

let (@+) (t : FApi.backward) (ts : FApi.backward list) =
  FApi.t_seqsub t ts

let (@>) (t1 : FApi.backward) (t2 : FApi.backward) =
  fun tc -> FApi.t_last t1 (t2 tc)

let (@~) (t : FApi.backward) (tt : FApi.tactical) =
  fun tc -> tt (t tc)

let (@!+) (tt : FApi.tactical) (t : FApi.backward) =
  fun tc -> FApi.t_onall t (tt tc)

let (@~+) (tt : FApi.tactical) (ts : FApi.backward list) =
  fun tc -> FApi.t_sub ts (tt tc)

(* -------------------------------------------------------------------- *)
exception InvalidProofTerm

type side    = [`Left|`Right]
type lazyred = [`Full | `NoDelta | `None]

(* -------------------------------------------------------------------- *)
module LowApply = struct
  type ckenv = [
    | `Tc   of rtcenv * ident option
    | `Hyps of EcEnv.LDecl.hyps * proofenv
  ]

  (* ------------------------------------------------------------------ *)
  let hyps_of_ckenv = function
    | `Hyps hyps -> (fst hyps)
    | `Tc (tc, target) -> RApi.tc_hyps ?target tc

  (* ------------------------------------------------------------------ *)
  let sub_hyps (hy1 : LDecl.hyps) (hy2 : LDecl.hyps) =
    if hy1 (*φ*)== hy2 then true else

    let env1, ld1 = LDecl.baseenv hy1, LDecl.tohyps hy1 in
    let env2, ld2 = LDecl.baseenv hy2, LDecl.tohyps hy2 in

    if env1        (*φ*)!= env2        then false else
    if ld1.h_tvar  (*φ*)!= ld2.h_tvar  then false else
    if ld1.h_local (*φ*)== ld2.h_local then true  else

    let env     = env1 in
    let hyps    = LDecl.init env ld1.h_tvar in
    let tophyps = Mid.of_list ld2.h_local in

    let h_eqs (x, v) =
      match Mid.find_opt x tophyps  with
      | None -> false | Some v' ->

        (v (*φ*)== v') ||
          match v, v' with
          | LD_var (t1, f1), LD_var (t2, f2) ->
                EqTest.for_type env t1 t2
             && oeq (is_alpha_eq hyps) f1 f2

          | LD_mem m1, LD_mem m2 ->
             EcMemory.mt_equal m1 m2

          | LD_modty mt1, LD_modty mt2 ->
            mt1 == mt2

          | LD_hyp f1, LD_hyp f2 ->
             is_alpha_eq hyps f1 f2

          | LD_abs_st au1, LD_abs_st au2 ->
             au1 (*φ*)== au2

          | _, _ -> false

   in List.for_all h_eqs ld1.h_local

  (* ------------------------------------------------------------------ *)
  let rec check_pthead (pt : pt_head) (tc : ckenv) =
    let hyps = hyps_of_ckenv tc in

    match pt with
    | PTCut f -> begin
        match tc with
        | `Hyps ( _, _) -> (PTCut f, f)
        | `Tc   (tc, _) ->
            (* cut - create a dedicated subgoal *)
            let handle = RApi.newgoal tc ~hyps f in
            (PTHandle handle, f)
    end

    | PTHandle hd -> begin
        let subgoal =
          match tc with
          | `Hyps tc -> FApi.get_pregoal_by_id hd (snd tc)
          | `Tc   tc -> RApi.tc_get_pregoal_by_id hd (fst tc)
        in
        (* proof reuse - fetch corresponding subgoal*)
        if not (sub_hyps subgoal.g_hyps (hyps_of_ckenv tc)) then
          raise InvalidProofTerm;
        (pt, subgoal.g_concl)
    end

    | PTLocal x -> begin
        let hyps = hyps_of_ckenv tc in
        try  (pt, LDecl.hyp_by_id x hyps)
        with LDecl.LdeclError _ -> raise InvalidProofTerm
    end

    | PTGlobal (p, tys) ->
        (* FIXME: poor API ==> poor error recovery *)
        let env = LDecl.toenv (hyps_of_ckenv tc) in
        (pt, EcEnv.Ax.instanciate p tys env)

    | PTSchema (p, tys, mt, mps, es) ->
      let env = LDecl.toenv (hyps_of_ckenv tc) in
      (pt, EcEnv.Schema.instanciate p tys mt mps es env)

  (* ------------------------------------------------------------------ *)
  and check (mode : [`Intro | `Elim]) (pt : proofterm) (tc : ckenv) =
    let hyps = hyps_of_ckenv tc in
    let env  = LDecl.toenv hyps in

    let rec check_args (sbt, ax, nargs) args =
      match args with
      | [] -> (Fsubst.f_subst sbt ax, List.rev nargs)

      | arg :: args ->
          let ((sbt, ax), narg) = check_arg (sbt, ax) arg in
          check_args (sbt, ax, narg :: nargs) args

    and check_arg (sbt, ax) arg =
      let check_binder (x, xty) f =
        let xty = Fsubst.subst_gty sbt xty in

        match xty, arg with
        | GTty xty, PAFormula arg ->
            if not (EcReduction.EqTest.for_type env xty arg.f_ty) then
              raise InvalidProofTerm;
            (Fsubst.f_bind_local sbt x arg, f)

        | GTmem _, PAMemory m ->
            (Fsubst.f_bind_mem sbt x m, f)

        | GTmodty emt, PAModule (mp, mt) -> begin
          (* FIXME: poor API ==> poor error recovery *)
          try
            let obl = EcTyping.check_modtype env mp mt emt in

            let f = match obl with
              | `Ok ->  f
              | `ProofObligation obl ->
                if mode = `Elim then f_imps obl f
                else f_and (f_ands obl) f
            in

            (Fsubst.f_bind_mod sbt x mp, f)
          with _ -> raise InvalidProofTerm
        end

        | _ -> raise InvalidProofTerm
      in

      match mode with
      | `Elim -> begin
          match TTC.destruct_product hyps ax, arg with
          | Some (`Imp (f1, f2)), PASub subpt when mode = `Elim ->
              let f1    = Fsubst.f_subst sbt f1 in
              let subpt =
                match subpt with
                | None       -> { pt_head = PTCut f1; pt_args = []; }
                | Some subpt -> subpt
              in
              let subpt, subax = check mode subpt tc in
                if not (EcReduction.is_conv hyps f1 subax) then
                  raise InvalidProofTerm;
                ((sbt, f2), PASub (Some subpt))

          | Some (`Forall (x, xty, f)), _ ->
              (check_binder (x, xty) f, arg)

          | _, _ ->
              if Fsubst.is_subst_id sbt then
                raise InvalidProofTerm;
              check_arg (Fsubst.f_subst_id, Fsubst.f_subst sbt ax) arg
      end

      | `Intro -> begin
          match TTC.destruct_exists hyps ax with
          | Some (`Exists (x, xty, f)) -> (check_binder (x, xty) f, arg)
          | None ->
              if Fsubst.is_subst_id sbt then
                raise InvalidProofTerm;
              check_arg (Fsubst.f_subst_id, Fsubst.f_subst sbt ax) arg
      end
    in

    let (nhd, ax) = check_pthead pt.pt_head tc in
    let ax, nargs = check_args (Fsubst.f_subst_id, ax, []) pt.pt_args in

    ({ pt_head = nhd; pt_args = nargs }, ax)
end

(* -------------------------------------------------------------------- *)
let t_abort (_ : tcenv1) =
  raise InvalidGoalShape

(* -------------------------------------------------------------------- *)
let t_admit (tc : tcenv1) =
  FApi.close (FApi.tcenv_of_tcenv1 tc) VAdmit

(* -------------------------------------------------------------------- *)
let t_fail (tc : tcenv1) =
  tc_error !!tc ~who:"fail" "explicit call to [fail]"

(* -------------------------------------------------------------------- *)
let t_close ?who (t : FApi.backward) (tc : tcenv1) =
  let tc = t tc in

  if not (FApi.tc_done tc) then
    tc_error !$tc ?who "expecting a closed goal";
  tc

(* -------------------------------------------------------------------- *)
let t_id (tc : tcenv1) =
  FApi.tcenv_of_tcenv1 tc

(* -------------------------------------------------------------------- *)
let t_shuffle (ids : EcIdent.t list) (tc : tcenv1) =
  let module E = struct exception InvalidShuffle end in

  try
    let hypstc, concl = FApi.tc1_flat tc in
    let { h_tvar; h_local = hyps } = EcEnv.LDecl.tohyps hypstc in
    let hyps = Mid.of_list hyps in

    let test_fv known fv =
      let test x _ =
        (* Either the variable is in known or was not in the previous hyps,
           in that case the variable is declared in the environment *)
        Mid.mem x known || not (LDecl.has_id x hypstc) in
      if not (Mid.for_all test fv) then raise E.InvalidShuffle in

    let for_form known f = test_fv known f.f_fv in
    let for_type known ty = test_fv known ty.ty_fv in

    let new_ = LDecl.init (LDecl.baseenv hypstc) h_tvar in

    let known, new_ =
      let add1 (known, new_) x =
        if Sid.mem x known then raise E.InvalidShuffle;
        let bd = Mid.find_opt x hyps in
        let bd = oget ~exn:E.InvalidShuffle bd in

        begin match bd with
        | LD_var (ty, f) -> for_type known ty; oiter (for_form known) f

        | LD_hyp f -> for_form known f

        | LD_mem _ | LD_abs_st _ | LD_modty _ -> ()
        end;
        (Sid. add x known, LDecl.add_local x bd new_)

      in List.fold_left add1 (Sid.empty, new_) ids in
    for_form known concl;
    FApi.xmutate1_hyps tc (VShuffle ids) [(new_, concl)]

  with E.InvalidShuffle ->
    tc_error !!tc "invalid shuffle"

(* -------------------------------------------------------------------- *)
let t_change_r ?(fail=false) ?target action (tc : tcenv1) =
  match target with
  | None -> begin
      let hyps, concl = FApi.tc1_flat tc in
      match action (lazy hyps) concl with
      | None -> if fail then raise InvalidGoalShape else tc
      | Some fp when fp == concl -> tc
      | Some fp -> FApi.mutate1 tc (fun hd -> VConv (hd, Sid.empty)) fp
  end

  | Some tg -> begin
      let action hyps fp = action hyps fp |> odfl fp in
      match LDecl.hyp_convert tg action (FApi.tc1_hyps tc) with
      | None      -> tc
      | Some hyps ->
          let concl = FApi.tc1_goal tc in
          FApi.mutate1 tc (fun hd -> VLConv (hd, tg)) ~hyps concl
  end

(* -------------------------------------------------------------------- *)
let t_change1 ?ri ?target (fp : form) (tc : tcenv1) =
  let action (lazy hyps) tgfp =
    if not (EcReduction.is_conv ?ri hyps fp tgfp) then
      raise InvalidGoalShape;
    if fp == tgfp then None else Some fp

  in t_change_r ?target action tc

let t_change ?ri ?target f tc =
  FApi.tcenv_of_tcenv1 (t_change1 ?ri ?target f tc)

(* -------------------------------------------------------------------- *)
type simplify_t =
  ?target:ident -> ?delta:bool -> ?logic:rlogic_info -> FApi.backward

type simplify_with_info_t =
  ?target:ident -> reduction_info -> FApi.backward

(* -------------------------------------------------------------------- *)
let t_cbv_with_info ?target (ri : reduction_info) (tc : tcenv1) =
  let action (lazy hyps) fp = Some (EcCallbyValue.norm_cbv ri hyps fp) in
  FApi.tcenv_of_tcenv1 (t_change_r ?target action tc)

(* -------------------------------------------------------------------- *)
let t_cbv ?target ?(delta = true) ?(logic = Some `Full) (tc : tcenv1) =
  let ri = if delta then full_red else nodelta in
  let ri = { ri with logic } in
  t_cbv_with_info ?target ri tc

(* -------------------------------------------------------------------- *)
let t_cbn_with_info ?target (ri : reduction_info) (tc : tcenv1) =
  let action (lazy hyps) fp = Some (EcCallbyValue.norm_cbv ri hyps fp) in
  FApi.tcenv_of_tcenv1 (t_change_r ?target action tc)

(* -------------------------------------------------------------------- *)
let t_cbn ?target ?(delta = true) ?(logic = Some `Full) (tc : tcenv1) =
  let ri = if delta then full_red else nodelta in
  let ri = { ri with logic } in
  t_cbv_with_info ?target ri tc

(* -------------------------------------------------------------------- *)
let t_hred_with_info ?target (ri : reduction_info) (tc : tcenv1) =
  let action (lazy hyps) fp = EcReduction.h_red_opt ri hyps fp in
  FApi.tcenv_of_tcenv1 (t_change_r ~fail:true ?target action tc)

(* -------------------------------------------------------------------- *)
let rec t_lazy_match ?(reduce = `Full) (tx : form -> FApi.backward)
  (tc : tcenv1) =
  let concl = FApi.tc1_goal tc in
  try tx concl tc
  with TTC.NoMatch ->
    let strategy =
      match reduce with
      | `None    -> raise InvalidGoalShape
      | `Full    -> EcReduction.full_red
      | `NoDelta -> EcReduction.nodelta in
    FApi.t_seq (t_hred_with_info strategy) (t_lazy_match ~reduce tx) tc

(* -------------------------------------------------------------------- *)
type smode = [ `Cbv | `Cbn ]

let dmode : smode = `Cbv

(* -------------------------------------------------------------------- *)
let t_simplify_with_info ?(mode = dmode) =
  match mode with
  | `Cbn -> t_cbn_with_info
  | `Cbv -> t_cbv_with_info

(* -------------------------------------------------------------------- *)
let t_simplify ?(mode = dmode) =
  match mode with
  | `Cbn -> t_cbn
  | `Cbv -> t_cbv

(* -------------------------------------------------------------------- *)
let t_clears1 ?(leniant = false) xs tc =
  let (hyps, concl) = FApi.tc1_flat tc in

  let xs =
    if not (Mid.set_disjoint xs concl.f_fv) then
      if leniant then Mid.set_diff xs concl.f_fv else
      let ids () = Sid.elements (Mid.set_inter xs concl.f_fv) in
      raise (ClearError (lazy (`ClearInGoal (ids ()))))
    else xs
  in

  if Sid.is_empty xs then tc else

  let hyps =
    try  LDecl.clear ~leniant xs hyps
    with LDecl.LdeclError (LDecl.CannotClear (id1, id2)) ->
      raise (ClearError (lazy (`ClearDep (id1, id2))))
  in

  FApi.mutate1 tc (fun hd -> VConv (hd, xs)) ~hyps concl

(* -------------------------------------------------------------------- *)
let t_clear1 ?leniant x tc =
  t_clears1 ?leniant (Sid.singleton x) tc

(* -------------------------------------------------------------------- *)
let t_clear ?leniant x tc =
  FApi.tcenv_of_tcenv1 (t_clears1 ?leniant (Sid.singleton x) tc)

(* -------------------------------------------------------------------- *)
let t_clears1 ?leniant xs tc =
  t_clears1 ?leniant (Sid.of_list xs) tc

(* -------------------------------------------------------------------- *)
let t_clears ?leniant xs tc =
  FApi.tcenv_of_tcenv1 (t_clears1 ?leniant xs tc)

(* -------------------------------------------------------------------- *)
module LowIntro = struct
  let valid_anon_name chk x =
    if x <> "" then
      x.[0] = '`' && chk (String.sub x 1 (String.length x - 1))
    else false

  let valid_name chk x =
    x = "_" || chk x || valid_anon_name chk x

  let valid_value_name (x : symbol) = valid_name EcIo.is_sym_ident x
  let valid_mod_name   (x : symbol) = valid_name EcIo.is_mod_ident x
  let valid_mem_name   (x : symbol) = valid_name EcIo.is_mem_ident x

  let tc_no_product (pe : proofenv) ?loc () =
    tc_error pe ?loc "nothing to introduce"

  let check_name_validity pe kind x : unit =
    let ok =
      match kind with
      | `Value  -> valid_value_name (tg_val x)
      | `Module -> valid_mod_name   (tg_val x)
      | `Memory -> valid_mem_name   (tg_val x)
    in
      if not ok then
        tc_error pe ?loc:(tg_tag x) "invalid name: %s" (tg_val x)
end

(* -------------------------------------------------------------------- *)
let t_intros_x (ids : (ident  option) mloc list) (tc : tcenv1) =
  let add_local hyps id sbt x gty =
    let gty = Fsubst.subst_gty sbt gty in
    let id  = tg_map (function
      | Some id -> id
      | None    -> EcEnv.LDecl.fresh_id hyps (EcIdent.name x)) id
    in

    let name = tg_map EcIdent.name id in

    match gty with
    | GTty ty ->
        LowIntro.check_name_validity !!tc `Value name;
        (id, LD_var (ty, None), Fsubst.f_bind_rename sbt x (tg_val id) ty)
    | GTmem me ->
        LowIntro.check_name_validity !!tc `Memory name;
        (id, LD_mem me, Fsubst.f_bind_mem sbt x (tg_val id))
    | GTmodty i ->
        LowIntro.check_name_validity !!tc `Module name;
        (id, LD_modty i, Fsubst.f_bind_mod sbt x (EcPath.mident (tg_val id)))
  in

  let add_ld id ld hyps =
    EcLocation.set_oloc
      (tg_tag id)
      (fun () -> LDecl.add_local (tg_val id) ld hyps) ()
  in

  let rec intro1 ((hyps, concl), sbt) id =
    match EcFol.sform_of_form concl with
    | SFquant (Lforall, (x, gty), lazy concl) ->
        let (id, ld, sbt) = add_local hyps id sbt x gty in
        let hyps = add_ld id ld hyps in
        ((hyps, concl), sbt), id

    | SFimp (prem, concl) ->
        let prem = Fsubst.f_subst sbt prem in
        let id = tg_map (function
          | None    -> EcIdent.create "_"
          | Some id -> id) id in
        let hyps = add_ld id (LD_hyp prem) hyps in
        ((hyps, concl), sbt), id

    | SFlet (LSymbol (x, xty), xe, concl) ->
        let id = tg_map (function
          | None    -> EcEnv.LDecl.fresh_id hyps (EcIdent.name x)
          | Some id -> id) id in
        let xty  = sbt.fs_ty xty in
        let xe   = Fsubst.f_subst sbt xe in
        let sbt  = Fsubst.f_bind_rename sbt x (tg_val id) xty in
        let hyps = add_ld id (LD_var (xty, Some xe)) hyps in
        ((hyps, concl), sbt), id

    | _ when sbt !=(*φ*) Fsubst.f_subst_id ->
        let concl = Fsubst.f_subst sbt concl in
        intro1 ((hyps, concl), Fsubst.f_subst_id) id

    | _ ->
        match h_red_opt full_red hyps concl with
        | None       -> LowIntro.tc_no_product !!tc ?loc:(tg_tag id) ()
        | Some concl -> intro1 ((hyps, concl), sbt) id
  in

  let tc = FApi.tcenv_of_tcenv1 tc in

  if List.is_empty ids then (tc, []) else begin
    let sbt = Fsubst.f_subst_id in
    let ((hyps, concl), sbt), ids =
      List.fold_left_map intro1 (FApi.tc_flat tc, sbt) ids in
    let concl = Fsubst.f_subst sbt concl in
    let (tc, hd) = FApi.newgoal tc ~hyps concl in
    let ids = List.map tg_val ids in
    (FApi.close tc (VIntros (hd, ids)), ids)
  end

(* -------------------------------------------------------------------- *)
let t_intros (ids : ident mloc list) (tc : tcenv1) =
  fst (t_intros_x (List.map (tg_map some) ids) tc)

(* -------------------------------------------------------------------- *)
type iname  = [
  | `Symbol of symbol
  | `Fresh
  | `Ident  of EcIdent.t
]

type inames = [`Symbol of symbol list | `Ident of EcIdent.t list]

(* -------------------------------------------------------------------- *)
let t_intros_n (n : int) (tc : tcenv1) =
  fst (t_intros_x (EcUtils.List.make n (notag None)) tc)

(* -------------------------------------------------------------------- *)
let t_intro_i_x (id : EcIdent.t option) (tc : tcenv1) =
  snd_map EcUtils.as_seq1 (t_intros_x [notag id] tc)

(* -------------------------------------------------------------------- *)
let t_intro_i (id : EcIdent.t) (tc : tcenv1) =
  fst (t_intro_i_x (Some id) tc)

(* -------------------------------------------------------------------- *)
let t_intro_sx (id : iname) (tc : tcenv1) =
  match id with
  | `Symbol x -> t_intro_i_x (Some (EcIdent.create x)) tc
  | `Ident  x -> t_intro_i_x (Some x) tc
  | `Fresh    -> t_intro_i_x None tc

(* -------------------------------------------------------------------- *)
let t_intro_s (id : iname) (tc : tcenv1) =
  fst (t_intro_sx id tc)

(* -------------------------------------------------------------------- *)
let t_intros_i_x (ids : EcIdent.t list) (tc : tcenv1) =
  t_intros_x (List.map (notag |- some) ids) tc

(* -------------------------------------------------------------------- *)
let t_intros_i (ids : EcIdent.t list) (tc : tcenv1) =
  fst (t_intros_i_x ids tc)

(* -------------------------------------------------------------------- *)
let t_intros_sx (ids : inames) (tc : tcenv1) =
  match ids with
  | `Symbol x -> t_intros_i_x (List.map EcIdent.create x) tc
  | `Ident  x -> t_intros_i_x x tc

(* -------------------------------------------------------------------- *)
let t_intros_s (ids : inames) (tc : tcenv1) =
  fst (t_intros_sx ids tc)

(* -------------------------------------------------------------------- *)
let t_intros_i_1 (ids : EcIdent.t list) (tc : tcenv1) =
  FApi.as_tcenv1 (t_intros_i ids tc)

(* -------------------------------------------------------------------- *)
let t_intros_i_seq ?(clear = false) ids tt tc =
  let tt = if clear then FApi.t_seq tt (t_clears ids) else tt in
  FApi.t_focus tt (t_intros_i ids tc)

(* -------------------------------------------------------------------- *)
let t_intros_s_seq ids tt tc =
  FApi.t_focus tt (t_intros_s ids tc)

(* -------------------------------------------------------------------- *)
let t_intros_sx_seq ids tt tc =
  let tc, ids = t_intros_sx ids tc in
  FApi.t_focus (tt ids) tc

(* -------------------------------------------------------------------- *)
let t_intro_sx_seq id tt tc =
  let tc, id = t_intro_sx id tc in
  FApi.t_focus (tt id) tc

(* -------------------------------------------------------------------- *)
let tt_apply (pt : proofterm) (tc : tcenv) =
  let (hyps, concl) = FApi.tc_flat tc in
  let tc, (pt, ax)  =
    RApi.to_pure (fun tc -> LowApply.check `Elim pt (`Tc (tc, None))) tc in

  if not (EcReduction.is_conv hyps ax concl) then begin
    (*
    let env = FApi.tc_env tc in
    let ppe = EcPrinting.PPEnv.ofenv env in
    (* FIXME: add this to the exception *)
    Format.eprintf "%a@.should be convertible to:@.%a@.but is not@."
      (EcPrinting.pp_form ppe) ax
      (EcPrinting.pp_form ppe) concl;
    *)
    raise InvalidGoalShape;
  end;

  FApi.close tc (VApply pt)

(* -------------------------------------------------------------------- *)
let tt_apply_hyp (x : EcIdent.t) ?(args = []) ?(sk = 0) tc =
  let pt =
    let args = (List.map paformula args) @ (List.make sk (PASub None)) in
    { pt_head = PTLocal x; pt_args = args; } in

  tt_apply pt tc

(* -------------------------------------------------------------------- *)
let tt_apply_s (p : path) tys ?(args = []) ?(sk = 0) tc =
  let pt =
    let args = (List.map paformula args) @ (List.make sk (PASub None)) in
    { pt_head = PTGlobal (p, tys); pt_args = args; } in

  tt_apply pt tc

(* -------------------------------------------------------------------- *)
let tt_apply_hd (hd : handle) ?(args = []) ?(sk = 0) tc =
  let pt =
    let args = (List.map paformula args) @ (List.make sk (PASub None)) in
    { pt_head = PTHandle hd; pt_args = args; } in

  tt_apply pt tc

(* -------------------------------------------------------------------- *)
let t_apply (pt : proofterm) (tc : tcenv1) =
  tt_apply pt (FApi.tcenv_of_tcenv1 tc)

(* -------------------------------------------------------------------- *)
let t_apply_hyp (x : EcIdent.t) ?args ?sk tc =
  tt_apply_hyp x ?args ?sk (FApi.tcenv_of_tcenv1 tc)

(* -------------------------------------------------------------------- *)
let t_hyp (x : EcIdent.t) tc =
  t_apply_hyp x ~args:[] ~sk:0 tc

(* -------------------------------------------------------------------- *)
let t_apply_s (p : path) (tys : ty list) ?args ?sk tc =
  tt_apply_s p tys ?args ?sk (FApi.tcenv_of_tcenv1 tc)

(* -------------------------------------------------------------------- *)
let t_apply_hd (hd : handle) ?args ?sk tc =
  tt_apply_hd hd ?args ?sk (FApi.tcenv_of_tcenv1 tc)

(* -------------------------------------------------------------------- *)
module Apply = struct
  type reason = [`DoNotMatch | `IncompleteInference]

  exception NoInstance of (bool * reason * PT.pt_env * (form * form))

  let t_apply_bwd_r ?(mode = fmdelta) ?(canview = true) pt (tc : tcenv1) =
    let ((hyps, concl), pterr) = (FApi.tc1_flat tc, PT.copy pt.ptev_env) in

    let noinstance ?(dpe = false) reason =
      raise (NoInstance (dpe, reason, pterr, (pt.ptev_ax, concl))) in

    let rec instantiate canview istop pt =
      match istop && PT.can_concretize pt.PT.ptev_env with
      | true ->
          let ax = PT.concretize_form pt.PT.ptev_env pt.PT.ptev_ax in
          if   EcReduction.is_conv ~ri:EcReduction.full_compat hyps ax concl
          then pt
          else instantiate canview false pt

      | false -> begin
          try
            PT.pf_form_match ~mode pt.PT.ptev_env ~ptn:pt.PT.ptev_ax concl;
            if not (PT.can_concretize pt.PT.ptev_env) then
              noinstance `IncompleteInference;
            pt
          with EcMatching.MatchFailure ->
            match TTC.destruct_product hyps pt.PT.ptev_ax with
            | Some _ ->
                (* FIXME: add internal marker *)
                instantiate canview false (PT.apply_pterm_to_hole pt)

            | None when not canview ->
                noinstance `DoNotMatch

            | None ->
                let forview (p, fs) =
                  (* Current proof-term is view argument *)
                  (* Copy PT environment to set a back-track point *)
                  let ptenv = PT.copy pt.ptev_env in
                  let argpt = { pt with ptev_env = ptenv } in
                  let argpt = { ptea_env = argpt.ptev_env;
                                ptea_arg = PVASub argpt; } in

                  (* Type-check view - FIXME: the current API is perfectible *)
                  let viewpt = PT.pt_of_global_r ptenv p [] in
                  let viewpt =
                    List.fold_left
                      (fun viewpt arg -> apply_pterm_to_arg_r viewpt (PVAFormula arg))
                      viewpt fs in

                  (* Apply view to its actual arguments *)
                  let viewpt = apply_pterm_to_arg viewpt argpt in

                  try  Some (instantiate false true viewpt)
                  with NoInstance _ -> None
                in

                let views =
                  match sform_of_form pt.PT.ptev_ax with
                  | SFiff (f1, f2) ->
                      [(LG.p_iff_rl, [f1; f2]);
                       (LG.p_iff_lr, [f1; f2])]

                  | SFnot f1 ->
                      [(LG.p_negbTE, [f1])]

                  | _ -> []
                in

                try  List.find_map forview views
                with Not_found -> noinstance `DoNotMatch
      end
    in

    let pt = instantiate canview true pt in
    let pt = fst (PT.concretize pt) in

    t_apply pt tc

  let t_apply_bwd ?mode ?canview pt (tc : tcenv1) =
    let hyps   = FApi.tc1_hyps tc in
    let pt, ax = LowApply.check `Elim pt (`Hyps (hyps, !!tc)) in
    let ptenv  = ptenv_of_penv hyps !!tc in
    let pt     = { ptev_env = ptenv; ptev_pt = pt; ptev_ax = ax; } in
    t_apply_bwd_r ?mode ?canview pt tc

  let t_apply_bwd_hi ?(dpe = true) ?mode ?canview pt (tc : tcenv1) =
    try  t_apply_bwd ?mode ?canview pt tc
    with (NoInstance (_, r, pt, f)) ->
      tc_error_exn !!tc (NoInstance (dpe, r, pt, f))
end

(* -------------------------------------------------------------------- *)
type genclear = [`Clear | `TryClear | `NoClear]

let t_generalize_hyps_x ?(missing = false) ?naming ?(letin = false) ids tc =
  let env, hyps, concl = FApi.tc1_eflat tc in

  let fresh x =
    match naming with
    | None   -> EcIdent.fresh x
    | Some f ->
      match f x with
      | None   -> EcIdent.fresh x
      | Some x -> EcIdent.create x
  in

  let for1 (s, bds, args, cls) (clid, id) =
    try
      let cls =
        match clid with
        | `TryClear -> (true , id) :: cls
        | `Clear    -> (false, id) :: cls
        | `NoClear  -> cls
      in

      match LDecl.ld_subst s (LDecl.by_id id hyps) with
      | LD_var (ty, Some body) when letin ->
          let x    = fresh id in
          let s    = Fsubst.f_bind_rename s id x ty in
          let bds  = `LetIn (x, GTty ty, body) :: bds in
          let args = args in
          (s, bds, args, cls)

      | LD_var (ty, _) ->
          let x    = fresh id in
          let s    = Fsubst.f_bind_rename s id x ty in
          let bds  = `Forall (x, GTty ty) :: bds in
          let args = PAFormula (f_local id ty) :: args in
          (s, bds, args, cls)

      | LD_mem mt ->
        let x    = fresh id in
        let s    = Fsubst.f_bind_mem s id x in
        let bds  = `Forall (x, GTmem mt) :: bds in
        let args = PAMemory id :: args in
        (s, bds, args, cls)

      | LD_modty mt ->
        let x    = fresh id in
        let s    = Fsubst.f_bind_mod s id (EcPath.mident x) in
        let mp   = EcPath.mident id in
        let sig_ = EcEnv.NormMp.sig_of_mp env mp in
        let bds  = `Forall (x, GTmodty mt) :: bds in
        let args = PAModule (mp, sig_) :: args in
        (s, bds, args, cls)

      | LD_hyp f ->
        let bds  = `Imp f :: bds in
        let args = palocal id :: args in
        (s, bds, args, cls)

      | LD_abs_st _ ->
          raise InvalidGoalShape

    with LDecl.LdeclError _ when missing -> (s, bds, args, cls)

  in

  let (s, bds, args, cls) = (Fsubst.f_subst_id, [], [], []) in
  let (s, bds, args, cls) = List.fold_left for1 (s, bds, args, cls) ids in

  let cltry, cldo = List.partition fst cls in
  let cltry, cldo = (List.map snd cltry, List.map snd cldo) in

  let ff =
    List.fold_left
      (fun ff bd ->
        match bd with
        | `Forall (x, xty)  -> f_forall [x, xty] ff
        | `Imp    pre       -> f_imp pre ff
        | `LetIn  (x, _, f) -> f_let1 x f ff)
      (Fsubst.f_subst s concl) bds in

  let pt = { pt_head = PTCut ff; pt_args = List.rev args; } in
  let tc = t_apply pt tc in
  let ct = fun tc -> tc
    |> t_clears1 ~leniant:true  cltry
    |> t_clears1 ~leniant:false cldo
    |> FApi.tcenv_of_tcenv1

  in FApi.t_onall ct tc

let t_generalize_hyps ?(clear = `No) ?missing ?naming ?letin ids tc =
  let ids =
    match clear with
    | `Yes -> List.map (fun x -> (`Clear   , x)) ids
    | `Try -> List.map (fun x -> (`TryClear, x)) ids
    | `No  -> List.map (fun x -> (`NoClear , x)) ids
  in t_generalize_hyps_x ?missing ?naming ?letin ids tc

let t_generalize_hyp ?clear ?missing ?naming ?letin id tc =
  t_generalize_hyps ?clear ?missing ?naming ?letin [id] tc

(* -------------------------------------------------------------------- *)
module LowAssumption = struct
  (* ------------------------------------------------------------------ *)
  let gen_find_in_hyps test hyps =
    let test (_, lk) =
      match lk with
      | LD_hyp f  -> test f
      | _         -> false
    in
      fst (List.find test (LDecl.tohyps hyps).h_local)

  (* ------------------------------------------------------------------ *)
  let t_gen_assumption tests tc =
    let (hyps, concl) = FApi.tc1_flat tc in

    let hyp =
      try
        List.find_map
          (fun test ->
            try  Some (gen_find_in_hyps (test hyps concl) hyps)
            with Not_found -> None)
          tests
      with Not_found -> tc_error !!tc "no assumption"
    in
    FApi.t_internal (t_hyp hyp) tc
end

(* -------------------------------------------------------------------- *)
let alpha_find_in_hyps hyps f =
   LowAssumption.gen_find_in_hyps (EcReduction.is_alpha_eq hyps f) hyps

let t_assumption mode (tc : tcenv1) =
  let convs =
    match mode with
    | `Alpha -> [EcReduction.is_alpha_eq]
    | `Conv  -> [EcReduction.is_alpha_eq; EcReduction.is_conv]
  in
    LowAssumption.t_gen_assumption convs tc

(* -------------------------------------------------------------------- *)
let t_cut (fp : form) (tc : tcenv1) =
  let concl = FApi.tc1_goal tc in
  t_apply_s LG.p_cut_lemma [] ~args:[fp; concl] ~sk:2 tc

(* -------------------------------------------------------------------- *)
let t_cutdef (pt : proofterm) (fp : form) (tc : tcenv1) =
  FApi.t_first (t_apply pt) (t_cut fp tc)

(* -------------------------------------------------------------------- *)
let t_true (tc : tcenv1) =
  t_apply_s LG.p_true_intro [] tc

(* -------------------------------------------------------------------- *)
let t_reflex_s (f : form) (tc : tcenv1) =
  t_apply_s LG.p_eq_refl [f.f_ty] ~args:[f] tc

let t_reflex ?(mode=`Conv) ?reduce (tc : tcenv1) =
  let t_reflex_r (fp : form) (tc : tcenv1) =
    match sform_of_form fp with
    | SFeq (f1, f2) ->
      if mode = `Conv || EcReduction.is_alpha_eq (FApi.tc1_hyps tc) f1 f2 then
        t_reflex_s f1 tc
      else
        raise InvalidGoalShape
    | _ -> raise TTC.NoMatch
  in
    t_lazy_match ?reduce t_reflex_r tc

(* -------------------------------------------------------------------- *)
let t_symmetry_s f1 f2 tc =
  t_apply_s LG.p_eq_sym_imp [f1.f_ty] ~args:[f2; f1] ~sk:1 tc

let t_symmetry ?reduce (tc : tcenv1) =
  let t_symmetry_r (fp : form) (tc : tcenv1) =
    match sform_of_form fp with
    | SFeq (f1, f2) -> t_symmetry_s f1 f2 tc
    | _ -> raise TTC.NoMatch
  in
    t_lazy_match ?reduce t_symmetry_r tc

(* -------------------------------------------------------------------- *)
let t_transitivity_s f1 f2 f3 tc =
  t_apply_s LG.p_eq_trans [f1.f_ty] ~args:[f1; f2; f3] ~sk:2 tc

let t_transitivity ?reduce f2 (tc : tcenv1) =
  let t_transitivity_r (fp : form) (tc : tcenv1) =
    match sform_of_form fp with
    | SFeq (f1, f3) -> t_transitivity_s f1 f2 f3 tc
    | _ -> raise TTC.NoMatch
  in
    t_lazy_match ?reduce t_transitivity_r tc

(* -------------------------------------------------------------------- *)
let t_exists_intro_s (args : pt_arg list) (tc : tcenv1) =
  let hyps = FApi.tc1_hyps tc in
  let pt = { pt_head = PTHandle (FApi.tc1_handle tc);
             pt_args = args; } in
  let ax = snd (LowApply.check `Intro pt (`Hyps (hyps, !!tc))) in
  FApi.xmutate1 tc (`Exists args) [ax]

(* -------------------------------------------------------------------- *)
let t_or_intro_s opsym (side : side) (f1, f2 : form pair) (tc : tcenv1) =
  let p =
    match side, opsym with
    | `Left , `Asym -> LG.p_ora_intro_l
    | `Right, `Asym -> LG.p_ora_intro_r
    | `Left , `Sym  -> LG.p_or_intro_l
    | `Right, `Sym  -> LG.p_or_intro_r
  in
  t_apply_s p [] ~args:[f1; f2] ~sk:1 tc

let t_or_intro ?reduce (side : side) (tc : tcenv1) =
  let t_or_intro_r (fp : form) (tc : tcenv1) =
    match sform_of_form fp with
    | SFor (b, (left, right)) -> t_or_intro_s b side (left, right) tc
    | _ -> raise TTC.NoMatch
  in
    t_lazy_match ?reduce t_or_intro_r tc

let t_left  ?reduce tc = t_or_intro ?reduce `Left  tc
let t_right ?reduce tc = t_or_intro ?reduce `Right tc

(* -------------------------------------------------------------------- *)
let t_and_intro_s opsym (f1, f2 : form pair) (tc : tcenv1) =
  let p =
    match opsym with
    | `Asym -> LG.p_anda_intro
    | `Sym  -> LG.p_and_intro
  in

  t_apply_s p [] ~args:[f1; f2] ~sk:2 tc

let t_and_intro ?reduce (tc : tcenv1) =
  let t_and_intro_r (fp : form) (tc : tcenv1) =
    match sform_of_form fp with
    | SFand (b, (left, right)) -> t_and_intro_s b (left, right) tc
    | _ -> raise TTC.NoMatch
  in
    t_lazy_match ?reduce t_and_intro_r tc

(* -------------------------------------------------------------------- *)
let t_iff_intro_s (f1, f2 : form pair) (tc : tcenv1) =
  t_apply_s LG.p_iff_intro [] ~args:[f1; f2] ~sk:2 tc

let t_iff_intro ?reduce (tc : tcenv1) =
  let t_iff_intro_r (fp : form) (tc : tcenv1) =
    match sform_of_form fp with
    | SFiff (f1, f2) -> t_iff_intro_s (f1, f2) tc
    | _ -> raise TTC.NoMatch
  in
    t_lazy_match ?reduce t_iff_intro_r tc

(* -------------------------------------------------------------------- *)
let gen_tuple_intro tys =
  let var ty name i =
    let var = EcIdent.create (Printf.sprintf "%s%d" name (i+1)) in
    (var, f_local var ty) in

  let eq i ty =
    let (x, fx) = var ty "x" i in
    let (y, fy) = var ty "y" i in
    ((x, fx), (y, fy), f_eq fx fy) in

  let eqs   = List.mapi eq tys in
  let concl = f_eq (f_tuple (List.map (snd |- proj3_1) eqs))
                   (f_tuple (List.map (snd |- proj3_2) eqs)) in
  let concl = f_imps (List.map proj3_3 eqs) concl in
  let concl =
    let bindings =
      let for1 ((x, fx), (y, fy), _) bindings =
        (x, GTty fx.f_ty) :: (y, GTty fy.f_ty) :: bindings in
      List.fold_right for1 eqs [] in
    f_forall bindings concl
  in

  concl

(* -------------------------------------------------------------------- *)
let pf_gen_tuple_intro tys hyps pe =
  let fp = gen_tuple_intro tys in
  FApi.newfact pe (VExtern (`TupleCongr tys, [])) hyps fp

(* -------------------------------------------------------------------- *)
let t_tuple_intro_s (fs : form pair list) (tc : tcenv1) =
  let tc  = RApi.rtcenv_of_tcenv1 tc in
  let tys = List.map (fun f -> (fst f).f_ty) fs in
  let hd  = RApi.bwd_of_fwd (pf_gen_tuple_intro tys (RApi.tc_hyps tc)) tc in
  let fs  = List.flatten (List.map (fun (x, y) -> [x; y]) fs) in

  RApi.of_pure_u (tt_apply_hd hd ~args:fs ~sk:(List.length tys)) tc;
  RApi.tcenv_of_rtcenv tc

let t_tuple_intro ?reduce (tc : tcenv1) =
  let t_tuple_intro_r (fp : form) (tc : tcenv1) =
    match sform_of_form fp with
    | SFeq (f1, f2) when is_tuple f1 && is_tuple f2 ->
        let fs = List.combine (destr_tuple f1) (destr_tuple f2) in
        t_tuple_intro_s fs tc
    | _ -> raise TTC.NoMatch
  in
    t_lazy_match ?reduce t_tuple_intro_r tc

(* -------------------------------------------------------------------- *)
let t_elim_r ?(reduce = (`Full : lazyred)) txs tc =
  match sform_of_form (FApi.tc1_goal tc) with
  | SFimp (f1, f2) ->
      let rec aux f1 =
        let sf1 = sform_of_form f1 in

        match
          List.opick (fun tx ->
              try  Some (tx (f1, sf1) f2 tc)
              with TTC.NoMatch -> None)
            txs
        with
        | Some gs -> gs
        | None    -> begin
          let strategy =
            match reduce with
            | `None    -> raise InvalidGoalShape
            | `Full    -> EcReduction.full_red
            | `NoDelta -> EcReduction.nodelta in

            match h_red_opt strategy (FApi.tc1_hyps tc) f1 with
            | None    -> raise InvalidGoalShape
            | Some f1 -> aux f1
        end
      in
        aux f1

    | _ -> raise InvalidGoalShape

(* -------------------------------------------------------------------- *)
let t_elim_false_r ((_, sf) : form * sform) concl tc =
  match sf with
  | SFfalse -> t_apply_s LG.p_false_elim [] ~args:[concl] tc
  | _ -> raise TTC.NoMatch

let t_elim_false ?reduce tc = t_elim_r ?reduce [t_elim_false_r] tc

(* --------------------------------------------------------------------- *)
let t_elim_and_r ((_, sf) : form * sform) concl tc =
  match sf with
  | SFand (opsym, (a1, a2)) ->
      let p =
        match opsym with
        | `Asym -> LG.p_anda_elim
        | `Sym  -> LG.p_and_elim

      in t_apply_s p [] ~args:[a1; a2; concl] ~sk:1 tc

  | _ -> raise TTC.NoMatch

let t_elim_and ?reduce goal = t_elim_r ?reduce [t_elim_and_r] goal

(* --------------------------------------------------------------------- *)
let t_elim_or_r ((_, sf) : form * sform) concl tc =
  match sf with
  | SFor (opsym, (a1, a2)) ->
      let p =
        match opsym with
        | `Asym -> LG.p_ora_elim
        | `Sym  -> LG.p_or_elim

      in t_apply_s p [] ~args:[a1; a2; concl] ~sk:2 tc

  | _ -> raise TTC.NoMatch

let t_elim_or ?reduce tc = t_elim_r ?reduce [t_elim_or_r] tc

(* --------------------------------------------------------------------- *)
let t_elim_iff_r ((_, sf) : form * sform) concl tc =
  match sf with
  | SFiff (a1, a2) ->
      t_apply_s LG.p_iff_elim [] ~args:[a1; a2; concl] ~sk:1 tc
  | _ -> raise TTC.NoMatch

let t_elim_iff ?reduce tc = t_elim_r ?reduce [t_elim_iff_r] tc

(* -------------------------------------------------------------------- *)
let t_elim_if_r ((_, sf) : form * sform) concl tc =
  match sf with
  | SFif (a1, a2, a3) ->
      t_apply_s LG.p_if_elim [] ~args:[a1; a2; a3; concl] ~sk:2 tc
  | _ -> raise TTC.NoMatch

let t_elim_if ?reduce tc = t_elim_r ?reduce [t_elim_if_r] tc

(* -------------------------------------------------------------------- *)
let gen_tuple_eq_elim (tys : ty list) : form =
  let p  = EcIdent.create "p" in
  let fp = f_local p tbool in

  let var ty name i =
    let var = EcIdent.create (Printf.sprintf "%s%d" name (i+1)) in
    (var, f_local var ty) in

  let eq i ty =
    let (x, fx) = var ty "x" i in
    let (y, fy) = var ty "y" i in
    ((x, fx), (y, fy), f_eq fx fy) in

  let eqs   = List.mapi eq tys in
  let concl = f_eq (f_tuple (List.map (snd |- proj3_1) eqs))
                   (f_tuple (List.map (snd |- proj3_2) eqs)) in
  let concl = f_imps [f_imps (List.map proj3_3 eqs) fp; concl] fp in
  let concl =
    let bindings =
      let for1 ((x, fx), (y, fy), _) bindings =
        (x, GTty fx.f_ty) :: (y, GTty fy.f_ty) :: bindings in
      List.fold_right for1 eqs [] in
    f_forall bindings concl
  in

  f_forall [(p, GTty tbool)] concl

(* -------------------------------------------------------------------- *)
let pf_gen_tuple_eq_elim tys hyps pe =
  let fp = gen_tuple_eq_elim tys in
  FApi.newfact pe (VExtern (`TupleEqElim tys, [])) hyps fp

(* -------------------------------------------------------------------- *)

let t_elim_eq_tuple_r_n ((_, sf) : form * sform) concl tc =
  match sf with
  | SFeq (a1, a2) when is_tuple a1 && is_tuple a2 ->
      let tc   = RApi.rtcenv_of_tcenv1 tc in
      let hyps = RApi.tc_hyps tc in
      let fs   = List.combine (destr_tuple a1) (destr_tuple a2) in
      let tys  = List.map (f_ty |- fst) fs in
      let hd   = RApi.bwd_of_fwd (pf_gen_tuple_eq_elim tys hyps) tc in
      let args = List.flatten (List.map (fun (x, y) -> [x; y]) fs) in
      let args = concl :: args in

      RApi.of_pure_u (tt_apply_hd hd ~args ~sk:1) tc;
      List.length tys, RApi.tcenv_of_rtcenv tc

  | _ -> raise TTC.NoMatch

let t_elim_eq_tuple_r f concl tc = snd (t_elim_eq_tuple_r_n f concl tc)

let t_elim_eq_tuple ?reduce goal = t_elim_r ?reduce [t_elim_eq_tuple_r] goal

(* -------------------------------------------------------------------- *)
let t_elim_exists_r ((f, _) : form * sform) concl tc =
  match f.f_node with
  | Fquant (Lexists, bd, body) ->
      let subst = Fsubst.f_subst_init ~freshen:true () in
      let subst, bd = Fsubst.add_bindings subst bd in
      let newc  = f_forall bd (f_imp (Fsubst.f_subst subst body) concl) in
      let tc    = FApi.mutate1 tc (fun hd -> VExtern (`Exists, [hd])) newc in
      FApi.tcenv_of_tcenv1 tc
  | _ -> raise TTC.NoMatch

let t_elim_exists ?reduce tc = t_elim_r ?reduce [t_elim_exists_r] tc

(* -------------------------------------------------------------------- *)
(* FIXME: document this function ! *)
let t_elimT_form (ind : proofterm) ?(sk = 0) (f : form) (tc : tcenv1) =
  let tc    = FApi.tcenv_of_tcenv1 tc in
  let _, ax =
    snd (RApi.to_pure (fun tc -> LowApply.check `Elim ind (`Tc (tc, None))) tc) in

  let hyps, concl = FApi.tc_flat tc in
  let env = LDecl.toenv hyps in

  let rec skip i a f =
    match i, EcFol.sform_of_form f with
    | Some i, _ when i <= 0 -> (a, f)
    | Some i, SFimp (_, f2) -> skip (Some (i-1)) (a+1) f2
    | None  , SFimp (_, f2) -> skip None (a+1) f2
    | Some _, _ -> raise InvalidGoalShape
    | None  , _ -> (a, f)
  in

  let (pr, prty, ax) =
    match sform_of_form ax with
    | SFquant (Lforall, (pr, GTty prty), lazy ax) -> (pr, prty, ax)
    | _ -> raise InvalidGoalShape
  in

  if not (EqTest.for_type env prty (tfun f.f_ty tbool)) then
    raise InvalidGoalShape;

  let (aa1, ax) = skip None 0 ax in

  let (x, _xty, ax) =
    match sform_of_form ax with
    | SFquant (Lforall, (x, GTty xty), lazy ax) -> (x, xty, ax)
    | _ -> raise InvalidGoalShape
  in

  let (aa2, ax) =
    let rec doit ax aa =
      match TTC.destruct_product hyps ax with
      | Some (`Imp (f1, f2)) when Mid.mem pr f1.f_fv -> doit f2 (aa+1)
      | _ -> (aa, ax)
    in
      doit ax 0
  in

  let pf =
    let (_, concl) = skip (Some sk) 0 concl in
    let (z, concl) = EcProofTerm.pattern_form ~name:(EcIdent.name x) hyps ~ptn:f concl in
      Fsubst.f_subst_local pr (f_lambda [(z, GTty f.f_ty)] concl) ax
  in

  let pf_inst = Fsubst.f_subst_local x f pf in

  let (aa3, sk) =
    let rec doit pf_inst (aa, sk) =
      if   EcReduction.is_conv hyps pf_inst concl
      then (aa, sk)
      else
        match TTC.destruct_product hyps pf_inst with
        | Some (`Imp (_, f2)) -> doit f2 (aa+1, sk+1)
        | _ -> raise InvalidGoalShape
    in
      doit pf_inst (0, sk)
  in

  let pf   = f_lambda [(x, GTty f.f_ty)] (snd (skip (Some sk) 0 pf)) in
  let args =
    (PAFormula pf :: (List.make aa1 (PASub None)) @
     PAFormula  f :: (List.make (aa2+aa3) (PASub None))) in
  let pt   = { ind with pt_args = ind.pt_args @ args; } in

  (* FIXME: put first goal last *)
  FApi.t_focus (t_apply pt) tc

(* -------------------------------------------------------------------- *)
let t_elimT_form_global p ?(typ = []) ?sk f tc =
  let pt = { pt_head = PTGlobal (p, typ); pt_args = []; } in
  t_elimT_form pt f ?sk tc

(* -------------------------------------------------------------------- *)
let gen_tuple_elim ?(witheq = true) (tys : ty list) : form =
  let var i ty =
    let var = EcIdent.create (Printf.sprintf "%s%d" "x" (i+1)) in
    (var, f_local var ty) in

  let tty  = ttuple tys in
  let p    = EcIdent.create "p" in
  let fp   = f_local p (tfun tty tbool) in
  let t    = EcIdent.create "t" in
  let ft   = f_local t tty in
  let vars = List.mapi var tys in
  let tf   = f_tuple (List.map snd vars) in

  let indh = f_app fp [tf] tbool in
  let indh = if witheq then f_imp (f_eq ft tf) indh else indh in
  let indh = f_forall (List.map (snd_map (fun f -> GTty f.f_ty)) vars) indh in

  let concl = f_forall [] (f_imp indh (f_app fp [ft] tbool)) in
  let concl = f_forall [t, GTty tty] concl in
  let concl = f_forall [p, GTty (tfun tty tbool)] concl in

  concl

(* -------------------------------------------------------------------- *)
let pf_gen_tuple_elim ?witheq tys hyps pe =
  let fp = gen_tuple_elim ?witheq tys in
  FApi.newfact pe (VExtern (`TupleElim tys, [])) hyps fp

(* -------------------------------------------------------------------- *)
let t_elimT_ind ?reduce mode (tc : tcenv1) =
  let elim (id, ty) tc =
    let tc, pt, sk =
      let env, hyps, _ = FApi.tc1_eflat tc in

      match EcEnv.Ty.scheme_of_ty mode ty env with
      | Some (p, typ) ->
          let pt = { pt_head = PTGlobal (p, typ); pt_args = []; } in
          (tc, pt, 0)

      | None ->
          match (EcEnv.ty_hnorm ty env).ty_node with
          | Ttuple tys ->
              let indtc  = pf_gen_tuple_elim ~witheq:false tys hyps in
              let tc, hd = FApi.bwd1_of_fwd indtc tc in
              let pt     = { pt_head = PTHandle hd; pt_args = []; } in
              (tc, pt, 0)

          | _ when EcReduction.EqTest.for_type env tunit ty ->
              let pt = { pt_head = PTGlobal (LG.p_unit_elim, []);
                         pt_args = []; } in
              (tc, pt, 0)

          | _ when EcReduction.EqTest.for_type env tint ty ->
              let pt = { pt_head = PTGlobal (EcCoreLib.CI_Int.p_int_elim, []);
                         pt_args = []; } in
              (tc, pt, 1)

          | _ when EcReduction.EqTest.for_type env tbool ty ->
              let pt = { pt_head = PTGlobal (LG.p_bool_elim, []);
                         pt_args = []; } in
              (tc, pt, 0)

          | _ -> raise InvalidGoalShape
    in
      t_elimT_form ~sk pt (f_local id ty) tc
  in

  let doit fp tc =
    match sform_of_form fp with
    | SFquant (Lforall, (x, GTty ty), _) -> begin
        let hyps = FApi.tc1_hyps tc in
        let id   = LDecl.fresh_id hyps (EcIdent.name x) in

        FApi.t_seqs
          [t_intros_i_seq ~clear:true [id] (elim (id, ty));
           t_simplify_with_info EcReduction.beta_red]
          tc
      end

    | _ -> raise TTC.NoMatch

  in t_lazy_match ?reduce doit tc

(* -------------------------------------------------------------------- *)
let t_elim_default_r = [
  t_elim_false_r;
  t_elim_and_r;
  t_elim_or_r;
  t_elim_iff_r;
  t_elim_if_r;
  t_elim_eq_tuple_r;
  t_elim_exists_r;
]

let t_elim ?reduce tc = t_elim_r ?reduce t_elim_default_r tc

(* -------------------------------------------------------------------- *)
let t_case fp tc = t_elimT_form_global LG.p_case_eq_bool fp tc

(* -------------------------------------------------------------------- *)
let t_elim_hyp h tc =
  (* FIXME: exception? *)
  let f  = LDecl.hyp_by_id h (FApi.tc1_hyps tc) in
  let pt = { pt_head = PTLocal h; pt_args = []; } in
  FApi.t_seq (t_cutdef pt f) t_elim tc

(* -------------------------------------------------------------------- *)
let t_elim_prind_r ?reduce ?accept (_mode : [`Case | `Ind]) tc =
  let doit fp tc =
    let env = FApi.tc1_env tc in

    match sform_of_form fp with
    | SFimp (f1, f2) ->
       let (p, sk), tv, args =
         match fst_map f_node (destr_app f1) with
         | Fop (p, tv), args when EcEnv.Op.is_prind env p -> begin
            if is_some accept then
              let pri = oget (EcEnv.Op.by_path_opt p env) in
              let pri = EcDecl.operator_as_prind pri in
              if not (oget accept pri) then
                raise InvalidGoalShape;
           end;
           (oget (EcEnv.Op.scheme_of_prind env `Case p), tv, args)

         | _ -> raise InvalidGoalShape

       in t_apply_s p tv ~args:(args @ [f2]) ~sk tc

    | _ -> raise TTC.NoMatch

  in t_lazy_match ?reduce doit tc

(* -------------------------------------------------------------------- *)
let t_elim_prind = t_elim_prind_r ?accept:None

(* -------------------------------------------------------------------- *)
let t_elim_iso_and ?reduce tc =
  try
    (2, t_elim_and ?reduce tc)
  with InvalidGoalShape ->
    let outgoals = ref None in

    let accept pri =
      match EcInductive.prind_is_iso_ands pri with
      | None -> false
      | Some (_, ngoals) -> outgoals := Some ngoals; true in

    let tc = t_elim_prind_r ?reduce ~accept `Case tc in (oget !outgoals, tc)

(* -------------------------------------------------------------------- *)
let t_elim_iso_or ?reduce tc =
  try
    ([1; 1], t_elim_or ?reduce tc)
  with InvalidGoalShape ->
    let outgoals = ref None in

    let accept pri =
      match EcInductive.prind_is_iso_ors pri with
      | None -> false
      | Some ((_, n1), (_, n2)) -> outgoals := Some [n1; n2]; true in

    let tc = t_elim_prind_r ?reduce ~accept `Case tc in (oget !outgoals, tc)

(* -------------------------------------------------------------------- *)
let t_split ?(closeonly = false) ?reduce (tc : tcenv1) =
  let t_split_r (fp : form) (tc : tcenv1) =
    let concl = FApi.tc1_goal tc in

    match sform_of_form fp with
    | SFtrue ->
        t_true tc
    | SFand (b, (f1, f2)) when not closeonly ->
        t_and_intro_s b (f1, f2) tc
    | SFiff (f1, f2) when not closeonly ->
        t_iff_intro_s (f1, f2) tc
    | SFeq (f1, f2) when not closeonly && (is_tuple f1 && is_tuple f2) ->
        let fs = List.combine (destr_tuple f1) (destr_tuple f2) in
        t_tuple_intro_s fs tc
    | SFeq (f1, _f2) ->
        t_reflex_s f1 tc
    | SFif (cond, _, _) when not closeonly ->
        (* FIXME: simplify goal *)
        let tc = if f_equal concl fp then tc else t_change1 fp tc in
        let tc = t_case cond tc in
          tc
    | _ -> raise TTC.NoMatch
  in
    t_lazy_match ?reduce t_split_r tc

(* -------------------------------------------------------------------- *)
let t_split_prind ?reduce (tc : tcenv1) =
  let t_split_r (fp : form) (tc : tcenv1) =
    let env = FApi.tc1_env tc in

    let p, tv, args =
      match fst_map f_node (destr_app fp) with
      | Fop (p, tv), args when EcEnv.Op.is_prind env p ->
         (p, tv, args)
      | _ -> raise InvalidGoalShape in
    let pri = oget (EcEnv.Op.by_path_opt p env) in
    let pri = EcDecl.operator_as_prind pri in

    match EcInductive.prind_is_iso_ands pri with
    | None -> raise InvalidGoalShape
    | Some (x, sk) ->
       let p = EcInductive.prind_introsc_path p x in
       t_apply_s p tv ~args ~sk tc

  in t_lazy_match ?reduce t_split_r tc

(* -------------------------------------------------------------------- *)
let t_or_intro_prind ?reduce (side : side) (tc : tcenv1) =
  let t_split_r (fp : form) (tc : tcenv1) =
    let env = FApi.tc1_env tc in

    let p, tv, args =
      match fst_map f_node (destr_app fp) with
      | Fop (p, tv), args when EcEnv.Op.is_prind env p ->
         (p, tv, args)
      | _ -> raise InvalidGoalShape in
    let pri = oget (EcEnv.Op.by_path_opt p env) in
    let pri = EcDecl.operator_as_prind pri in

    match EcInductive.prind_is_iso_ors pri with
    | Some ((x, sk), _) when side = `Left ->
       let p = EcInductive.prind_introsc_path p x in
       t_apply_s p tv ~args ~sk tc
    | Some (_, (x, sk)) when side = `Right ->
       let p = EcInductive.prind_introsc_path p x in
       t_apply_s p tv ~args ~sk tc
    | _  -> raise InvalidGoalShape

  in t_lazy_match ?reduce t_split_r tc

(* -------------------------------------------------------------------- *)
type rwspec = [`LtoR|`RtoL] * ptnpos option
type rwmode = [`Bool | `Eq]

(* -------------------------------------------------------------------- *)
let t_rewrite
   ?xconv ?keyed ?target ?(mode : rwmode option) ?(donot=false)
   (pt : proofterm) (s, pos) (tc : tcenv1)
=
  let tc           = RApi.rtcenv_of_tcenv1 tc in
  let (hyps, tgfp) = RApi.tc_flat ?target tc in
  let env          = LDecl.toenv hyps in
  let (pt, ax)     = LowApply.check `Elim pt (`Tc (tc, target)) in

  let (pt, left, right) =
    let doit ax =
      match sform_of_form ax, mode with
      | SFeq  (f1, f2), (None | Some `Eq) -> (pt, f1, f2)
      | SFiff (f1, f2), (None | Some `Eq) -> (pt, f1, f2)

      | SFnot f, (None | Some `Bool) when s = `LtoR && donot ->
        let ptev_env = ptenv_of_penv hyps (RApi.tc_penv tc) in
        let pt = { ptev_env; ptev_pt = pt; ptev_ax = ax } in
        let pt' = pt_of_global_r ptev_env LG.p_negeqF [] in
        let pt' = apply_pterm_to_arg_r pt' (PVAFormula f) in
        let pt' = apply_pterm_to_arg_r pt' (PVASub pt) in
        let pt, _ = concretize pt' in
        pt, f, f_false

      | _, (None | Some `Bool) when
          s = `LtoR && ER.EqTest.for_type env ax.f_ty tbool
          -> (pt, ax, f_true)

      | _ -> raise TTC.NoMatch
    in oget ~exn:InvalidProofTerm (TTC.lazy_destruct hyps doit ax)
  in

  let (left, right) =
    match s with
    | `LtoR -> (left , right)
    | `RtoL -> (right, left )
  in

  let change f =
    if not (EcReduction.is_conv hyps f left) then
      raise InvalidGoalShape;
    right in

  let npos  =
    match pos with
    | None     -> FPosition.select_form ?keyed ?xconv hyps None left tgfp
    | Some pos -> pos in

  let tgfp =
    try  FPosition.map npos change tgfp
    with InvalidPosition -> raise InvalidGoalShape
  in

  match target with
  | None ->
      let hd   = RApi.newgoal tc tgfp in
      let rwpt = { rpt_proof = pt; rpt_occrs = pos; rpt_lc = None; } in

      RApi.close tc (VRewrite (hd, rwpt));
      RApi.tcenv_of_rtcenv tc

  | Some (h : ident) ->
      let hyps = oget (LDecl.hyp_convert h (fun _ _ -> tgfp) (RApi.tc_hyps tc)) in
      let hd   = RApi.newgoal tc ~hyps (RApi.tc_goal tc) in
      let rwpt = { rpt_proof = pt; rpt_occrs = pos; rpt_lc = Some h; } in

      RApi.close tc (VRewrite (hd, rwpt));
      RApi.tcenv_of_rtcenv tc

(* -------------------------------------------------------------------- *)
let t_rewrite_hyp ?xconv ?mode ?donot (id : EcIdent.t) pos (tc : tcenv1) =
  let pt = { pt_head = PTLocal id; pt_args = []; } in
  t_rewrite ?xconv ?mode ?donot pt pos tc

(* -------------------------------------------------------------------- *)
type vsubst = [
  | `Local of EcIdent.t
  | `Glob  of EcPath.mpath * EcMemory.memory
  | `PVar  of EcTypes.prog_var * EcMemory.memory
]

(* -------------------------------------------------------------------- *)
type subst_kind = {
  sk_local : bool;
  sk_pvar  : bool;
  sk_glob  : bool;
}

let  full_subst_kind = { sk_local = true ; sk_pvar  = true ; sk_glob  = true ; }
let empty_subst_kind = { sk_local = false; sk_pvar  = false; sk_glob  = false; }

type tside = [`All of [`LtoR | `RtoL] option | `LtoR | `RtoL]

(* -------------------------------------------------------------------- *)
module LowSubst = struct
  (* ------------------------------------------------------------------ *)
  let default_subst_kind = full_subst_kind

  (* ------------------------------------------------------------------ *)
  let is_member_for_subst ?kind hyps var f =
    let kind = odfl default_subst_kind kind in
    let env = LDecl.toenv hyps in
    let is_let x = match LDecl.by_id x hyps with LD_var (_, Some _) -> true | _ -> false in
    match f.f_node, var with
    (* Substitution of logical variables *)
    | Flocal x, None when kind.sk_local && not (is_let x) ->
        Some (`Local x)

    | Flocal x, Some (`Local y) when kind.sk_local && id_equal x y && not (is_let x) ->
        Some (`Local x)

    (* Substitution of program variables *)
    | Fpvar (pv, m), None when kind.sk_pvar -> Some (`PVar (pv, m))
    | Fpvar (pv, m), Some (`PVar (pv', m')) when kind.sk_pvar ->
        let pv  = EcEnv.NormMp.norm_pvar env pv  in
        let pv' = EcEnv.NormMp.norm_pvar env pv' in

        if   EcTypes.pv_equal pv pv' && EcMemory.mem_equal m m'
        then Some (`PVar (pv, m))
        else None

    (* Substitution of globs *)
    | Fglob (mp, m), None when kind.sk_glob -> Some (`Glob (mp, m))
    | Fglob (mp, m), Some (`Glob (mp', m')) when kind.sk_glob ->
        let gl  = EcEnv.NormMp.norm_glob env m  mp  in
        let gl' = EcEnv.NormMp.norm_glob env m' mp' in

        if   EcFol.f_equal gl gl'
        then Some (`Glob (mp, m))
        else None

    | _, _ -> None

  (* ------------------------------------------------------------------ *)
  let is_eq_for_subst ?kind ?(tside = (`All None : tside)) hyps var (f1, f2) =
    let can (side : [`LtoR | `RtoL]) =
      match tside with
      | `All  None    -> Some `High
      | `All (Some x) -> Some (if x = side then `High else `Low)
      | _ -> if tside = (side :> tside) then Some `High else None
    in

    let is_member_for_subst ?kind side env var f tg =
      can side |> obind (fun prio ->
        is_member_for_subst ?kind env var f
          |> obind (fun eq -> Some (prio, (side, eq, tg))))
    in

    let env = LDecl.toenv hyps in

    let var = List.pmap identity
      [is_member_for_subst ?kind `LtoR hyps var f1 f2;
       is_member_for_subst ?kind `RtoL hyps var f2 f1] in

    let cmp x y =
      let x = match x with `High -> 1 | `Low -> 0 in
      let y = match y with `High -> 1 | `Low -> 0 in
      Stdlib.compare x y in

    let var = List.ksort ~stable:true ~rev:true ~key:fst ~cmp var in
    let var = List.ohead var |> omap snd in

    let aout =
      match var with
      | None -> None

      (* Substitution of logical variables *)
      | Some ((_, `Local x, f) as aout) ->
        let f = simplify { no_red with delta_h = predT } hyps f in
        if Mid.mem x f.f_fv then None else Some aout

      (* Substitution of program variables *)
      | Some ((_, `PVar (pv, m), f) as aout) ->
        let f  = simplify { no_red with delta_h = predT } hyps f in
        let fv = EcPV.PV.fv env m f in
        if EcPV.PV.mem_pv env pv fv then None else Some aout

      (* Substitution of globs *)
      | Some ((_, `Glob (mp, m), f) as aout) ->
        let f  = simplify { no_red with delta_h = predT } hyps f in
        let fv = EcPV.PV.fv env m f in
        if EcPV.PV.mem_glob env mp fv then None else Some aout in
    match aout with
    | None -> None
    | Some(side,v,f) ->
      let rec add fv x _ =
        if Sid.mem x fv then fv
        else
          (* check if x is a declared module *)
          let fv = Sid.add x fv in
          if EcEnv.Mod.by_mpath_opt (EcPath.mident x) env <> None then fv
          else match LDecl.by_id x hyps with
          | LD_var (_, Some f) -> add_f fv f
          | _ -> fv
      and add_f fv f = Mid.fold_left add fv f.f_fv in
      Some(side,v,f, add_f Sid.empty f)


  (* ------------------------------------------------------------------ *)
  let build_subst env var f =
    match var with
    | `Local x ->
        let subst f = Fsubst.f_subst_local x f in
        let check tg = Mid.mem x tg.f_fv in
        (subst f, check)

    | `PVar (pv, m) ->
        let subst f = EcPV.PVM.subst env (EcPV.PVM.add env pv m f EcPV.PVM.empty) in
        (* FIXME *)
        let check _tg = true in
        (subst f, check)

    | `Glob (mp, m) ->
        let subst f = EcPV.PVM.subst env (EcPV.PVM.add_glob env mp m f EcPV.PVM.empty) in
        (* FIXME *)
        let check _tg = true in
        (subst f, check)
end

(* -------------------------------------------------------------------- *)
type subst_clear =
  | SCnone (* clear nothing *)
  | SChyp  (* clear the hypothesis *)
  | SCall  (* clear the variable and the hypothesis *)

(*
h1, h2, id : x = f; h3; h4 |- concl
h1, id: x = f |- h2 =>

f z = y + z
h1 : x = f w
h2 : y = z
 *)

let gen_hyps post gG =
  let do1 gG (id, d) =
    match d with
    | LD_var (_ty, Some body) -> f_let1 id body gG
    | LD_var (ty, None)       -> f_forall [id, GTty ty] gG
    | LD_mem mt               -> f_forall_mems [id, mt] gG
    | LD_modty mt             -> f_forall [id, GTmodty mt] gG
    | LD_hyp f                -> f_imp f gG
    | LD_abs_st _             -> raise InvalidGoalShape in
  List.fold_left do1 gG post

let build_var var ty =
  match var with
  | `Glob (mp,m) -> f_glob mp m
  | `Local x     -> f_local x ty
  | `PVar(x,m)   -> f_pvar x ty m


let t_rw_for_subst y togen concl side eqid tc =
  let hyps = FApi.tc1_hyps tc in
  let eq = LDecl.hyp_by_id eqid hyps in
  let f1', f2' = destr_eq_or_iff eq in
  let ids = List.map fst togen in
  let ty = f1'.f_ty in
  let posty_G = f_lambda [y, GTty ty] (gen_hyps (List.rev togen) concl) in
  let f1, f2 = if side = `LtoR then f2', f1' else f1', f2' in
  let postx_G = f_app posty_G [f2] tbool in
  let t_eq =
    match destr_eq eq with
    | _ -> t_hyp eqid
    | exception (DestrError _) ->

      FApi.t_seq (t_apply_s LG.p_eq_iff_imp [] ~args:[f1';f2'] ~sk:1) (t_hyp eqid) in

  let t_eq_ind =
    (t_apply_s LG.p_eq_ind [ty] ~args:[f1;f2;posty_G] ~sk:2) @+
      [ if side = `LtoR then t_symmetry @! t_eq else t_eq;
        t_id] in
    FApi.t_seqs [
            (* pre; id: x = f; post |- concl *)
            t_generalize_hyps ~clear:`Yes ~missing:false ~letin:true ids;
            (* pre'; id: x= f |- hpost => post => concl *)
            t_change postx_G;
            (* pre'; id: x = f |- (fun y => (hpost => post => concl){x <- y}) x *)
            t_eq_ind;
            (* pre'; id: x = f |- (fun y => (hpost => post => concl){x <- y}) f *)
            t_hred_with_info beta_red;
            (* pre'; id: x = f |- (hpost => post => concl){x <- f} *)
            t_intros_i ids] tc

let t_subst_x ?kind ?(except = Sid.empty) ?(clear = SCall) ?var ?tside ?eqid (tc : tcenv1) =
  let env, hyps, concl = FApi.tc1_eflat tc in

  let subst_pre (subst, check, depend) moved (id, lk) =
    if Sid.mem id depend then `Pre (id, lk)
    else

    let check_moved f = not (Mid.disjoint (fun _ _ _ -> false) f.f_fv moved) in

    match lk with
    | LD_var (_ty, None) ->
        `Pre (id, lk)

    | LD_var (ty, Some body) ->
      if check_moved body then
        let body =
          if check body && not (Sid.mem id except)
          then subst body
          else body in
        `Post (id, LD_var (ty, Some body))
      else
        if check body && not (Sid.mem id except)
        then `Post (id, LD_var (ty, Some (subst body)))
        else `Pre  (id, lk)

    | LD_hyp body ->
      if check_moved body then
        let body =
          if check body && not (Sid.mem id except) then subst body
          else body in
        `Post (id, LD_hyp body)
      else
        if check body && not (Sid.mem id except)
        then `Post (id, LD_hyp (subst body))
        else `Pre  (id, lk)

    | LD_mem    _ -> `Pre (id, lk)
    | LD_modty  _ -> `Pre (id, lk) (* TODO: subst cost *)
    | LD_abs_st _ -> `Pre (id, lk)
  in

  let try1 eq =
    match eq with
    | id, LD_hyp f  when is_eq_or_iff f -> begin
        let dosubst (side, var, f, depend) =
          let y, fy =
            let y = EcIdent.create "y" in
            y, f_local y f.f_ty in
          let subst, check = LowSubst.build_subst env var fy in
          let post, (id', _), pre =
            try  List.find_pivot (id_equal id |- fst) (LDecl.tohyps hyps).h_local
            with Not_found -> assert false
          in

          assert (id_equal id id');
          let hpost, _ =
            List.fold_right
              (fun ((x,_) as h) (hpost, moved) ->
                match subst_pre (subst, check, depend) moved h with
                | `Pre  _ -> (hpost, moved)
                | `Post (id, lk) -> ((id, lk) :: hpost, Sid.add x moved))
              pre ([], Sid.empty) in
          let post =
            List.fold_right
              (fun h post ->
                assert (not (id_equal (fst h) id));
                match subst_pre (subst, check, depend) Sid.empty h with
                | `Pre (id, lk) | `Post (id, lk) -> (id, lk) :: post )
              post [] in
          let apost = List.rev_append hpost post in
          let concl = subst concl in

          let to_clear =
            match clear with
            | SCnone -> []
            | SChyp -> [id]
            | SCall ->
              match var with
              | `Local x ->
                begin match LDecl.by_id x hyps with
                | LD_var (_, None) -> [x; id]
                | _ -> [id]
                end
              | _ -> [id]
          in

          FApi.t_seqs [
            t_rw_for_subst y apost concl side id;
            t_clears to_clear
            ] tc, (y, apost, side)

        in

        try
          LowSubst.is_eq_for_subst
            ?kind ?tside hyps var (destr_eq_or_iff f)
          |> omap dosubst
        with EcPV.MemoryClash -> None
    end

    | _ -> None
  in

  let eqs =
    eqid
      |> omap  (fun id -> [id, LD_hyp (LDecl.hyp_by_id id hyps)])
      |> ofdfl (fun () -> (LDecl.tohyps hyps).h_local)
  in

  try  List.find_map try1 eqs
  with Not_found -> raise InvalidGoalShape

let t_subst ?kind ?except ?(clear = true) ?var ?tside ?eqid (tc : tcenv1) =
  let clear = if clear then SCall else SChyp in
  fst (t_subst_x ?kind ?except ~clear ?var ?tside ?eqid tc)

(* -------------------------------------------------------------------- *)
let t_absurd_hyp ?(conv  = `AlphaEq) id tc =
  let hyps, concl = FApi.tc1_flat tc in

  let b, f = destr_nots (LDecl.hyp_by_id id hyps) in

  let test f' =
    let b', f' = destr_nots f' in
    (b = not b') && EcReduction.xconv conv hyps f f' in

  let id' =
    try  LowAssumption.gen_find_in_hyps test hyps
    with _ -> raise InvalidGoalShape
  in

  let x, hnx, hx = if b then f, id, id' else f_not f, id', id in

  FApi.t_internal (FApi.t_seqs [
    t_apply_s LG.p_false_elim [] ~args:[concl] ~sk:1;
    FApi.t_seqsub (t_apply_s LG.p_negbTE [] ~args:[x] ~sk:2)
      [ t_apply_hyp hnx; t_apply_hyp hx ]
  ]) tc

(* -------------------------------------------------------------------- *)
let t_absurd_hyp ?conv ?id tc =
  let tabsurd = t_absurd_hyp ?conv in

  match id with
  | Some id -> tabsurd id tc
  | None    ->
      let tott (id, lk) =
        match lk with
        | LD_hyp f when is_not f -> Some (tabsurd id)
        | _ -> None

      in let hyps = (LDecl.tohyps (FApi.tc1_hyps tc)).h_local
      in let tc = FApi.t_try (FApi.t_ors_pmap tott hyps) tc in

      if not (FApi.tc_done tc) then raise InvalidGoalShape; tc

(* -------------------------------------------------------------------- *)
let t_false ?(conv = `Eq) id tc =
  let hy = FApi.tc1_hyps tc in
  let hh = LDecl.hyp_by_id id hy in

  if not (EcReduction.xconv conv hy hh f_false) then
    raise InvalidGoalShape;

  FApi.t_internal ~info:"t_false"
    (FApi.t_seq
       (t_generalize_hyp ~clear:`No id) t_elim_false)
    tc

(* -------------------------------------------------------------------- *)
let t_false ?conv ?id tc =
  let tfalse = t_false ?conv in

  match id with
  | Some id -> tfalse id tc
  | None    ->
      let tott (id, lk) =
        match lk with
        | LD_hyp _ -> Some (tfalse id)
        | _ -> None

      in let hyps = (LDecl.tohyps (FApi.tc1_hyps tc)).h_local
      in FApi.t_ors_pmap tott hyps tc

(* -------------------------------------------------------------------- *)
type pgoptions =  {
  pgo_split  : bool;
  pgo_solve  : bool;
  pgo_subst  : bool;
  pgo_disjct : bool;
  pgo_delta  : pgo_delta;
}

and pgo_delta = {
  pgod_case  : bool;
  pgod_split : bool;
}

module PGOptions = struct
  let default =
    let fordelta =
      { pgod_case  = false;
        pgod_split = true ; }; in

    { pgo_split  = true;
      pgo_solve  = true;
      pgo_subst  = true;
      pgo_disjct = false;
      pgo_delta  = fordelta; }

  let merged1 opts (b, x) =
    match x with
    | None -> { pgod_case = b; pgod_split = b; }
    | Some `Case  -> { opts with pgod_case  = b; }
    | Some `Split -> { opts with pgod_split = b; }

  let merge1 opts ((b, x) : bool * EcParsetree.ppgoption) =
    match x with
    | `Split       -> { opts with pgo_split  = b; }
    | `Solve       -> { opts with pgo_solve  = b; }
    | `Subst       -> { opts with pgo_subst  = b; }
    | `Disjunctive -> { opts with pgo_disjct = b; }

    | `Delta x ->
        { opts with pgo_delta = merged1 opts.pgo_delta (b, x); }

  let merge opts (specs : EcParsetree.ppgoptions) =
    List.fold_left merge1 opts specs
end

module PGInternals = struct
  let pg_cnj_elims = [
    t_elim_false_r   ;
    t_elim_exists_r  ;
    t_elim_and_r     ;
    t_elim_eq_tuple_r;
  ]

  let pg_djn_elims = [
    t_elim_or_r
  ]
end

let t_progress ?options ?ti (tt : FApi.backward) (tc : tcenv1) =
  let options = odfl PGOptions.default options in

  let tt =
    if   options.pgo_solve
    then FApi.t_or (t_assumption `Alpha) tt
    else tt

  and ti = odfl (fun (_ : EcIdent.t) -> t_id) ti in

  let t_progress_subst ?eqid =
    let sk1 = { empty_subst_kind with sk_local = true ; } in
    let sk2 = {  full_subst_kind with sk_local = false; } in
    FApi.t_or (t_subst ~kind:sk1 ?eqid) (t_subst ~kind:sk2 ?eqid)
  in

  let ts =
    if   options.pgo_subst
    then fun id -> FApi.t_or (t_progress_subst ~eqid:id) (ti id)
    else ti in

  (* Entry of progress: simplify goal, and chain with progress *)
  let rec entry tc = FApi.t_seq (t_simplify ~delta:false) aux0 tc

  (* Progress (level 0): try to apply user tactic, chain with level 1. *)
  and aux0 tc = FApi.t_seq (FApi.t_try tt) aux1 tc

  (* Progress (level 1): intro/elim top-level assumption *)
  and aux1 tc =
    let hyps, concl = FApi.tc1_flat tc in

    match sform_of_form concl with
    | SFquant (Lforall, _, _) ->
      let bd  = fst (destr_forall concl) in
      let ids = List.map (EcIdent.name |- fst) bd in
      let ids = LDecl.fresh_ids hyps ids in
      FApi.t_seq (t_intros_i ids) aux0 tc

    | SFlet (LTuple fs, f1, _) ->
      let tys    = List.map snd fs in
      let tc, hd = FApi.bwd1_of_fwd (pf_gen_tuple_elim tys hyps) tc in
      let pt     = { pt_head = PTHandle hd; pt_args = []; } in
      FApi.t_seq (t_elimT_form pt f1) aux0 tc

    | SFimp (_, _) -> begin
      let id = LDecl.fresh_id hyps "H" in

      match t_intros_i_seq [id] tt tc with
      | tc when FApi.tc_done tc -> tc
      | _ ->
          (* FIXME: we'd like to do the following:
             intros id; on_intro id; entry
             on_intro:
               (try subst (if option)
                or default_intro id);
             default_intro id =
               try absurd id;   -- ie if id: b and !b is an assumption
               rewrite_bool id; -- if id: !b -> rewrite b = false,
                                   if id:  b -> rewrite b = true
               default_on_intro id *)
          let iffail tc =
            t_intros_i_seq [id] (FApi.t_seq (ts id) entry) tc in

          let elims = PGInternals.pg_cnj_elims in
          let elims =
            if   options.pgo_disjct
            then PGInternals.pg_djn_elims @ elims
            else elims
          in

          let reduce =
            if options.pgo_delta.pgod_case then `Full else `NoDelta in

          FApi.t_switch ~on:`All (t_elim_r ~reduce elims) ~ifok:aux0 ~iffail tc
    end

    | _ when options.pgo_split ->
       let thesplit =
         match options.pgo_delta.pgod_split with
         | true  -> t_split ~closeonly:false ~reduce:`Full
         | false ->
             FApi.t_or
               (t_split ~reduce:`NoDelta)
               (t_split ~closeonly:true ~reduce:`Full) in

        FApi.t_try (FApi.t_seq thesplit aux0) tc

    | _ -> t_id tc

  in entry tc

(* -------------------------------------------------------------------- *)

let pp_tc tc =
  let pr = proofenv_of_proof (proof_of_tcenv tc) in
  let cl = List.map (FApi.get_pregoal_by_id^~ pr) (FApi.tc_opened tc) in
  let cl = List.map (fun x -> (EcEnv.LDecl.tohyps x.g_hyps, x.g_concl)) cl in

  match cl with [] -> () | hd :: tl ->

  Format.eprintf "%a@."
    (EcPrinting.pp_goal (EcPrinting.PPEnv.ofenv (FApi.tc_env tc)) {prpo_pr = true; prpo_po = true})
    (hd, `All tl)

type cstate = {
  cs_undosubst : Sid.t;
  cs_sbeq : Sid.t;
}

let t_crush ?(delta = true) ?tsolve (tc : tcenv1) =

  let dtsolve =
    [t_assumption `Conv; t_absurd_hyp ~conv:`Conv; t_false ~conv:`Conv] in

  let tsolve = odfl (FApi.t_ors dtsolve) tsolve in

  let tt = FApi.t_try (t_assumption `Alpha) in

(*  let t_print s t tc =
    Format.eprintf "%s@." s;
    pp_tc (FApi.tcenv_of_tcenv1 tc);
    t tc in *)

  (* Entry of progress: simplify goal, and chain with progress *)
  let rec entry (st : cstate) = t_simplify ~delta:false @! aux0 st

  (* Progress (level 0): try to apply user tactic. *)
  and aux0 (st : cstate) = FApi.t_try tt @! aux1 st

  (* Progress (level 1): intro/elim top-level assumption. *)
  and aux1 (st : cstate) tc =
    let hyps, concl = FApi.tc1_flat tc in

    match sform_of_form concl with
    | SFquant (Lforall, _, _) ->
      let bd  = fst (destr_forall concl) in
      let ids = List.map (EcIdent.name |- fst) bd in
      let ids = LDecl.fresh_ids hyps ids in
      let st = { st with cs_undosubst = Sid.of_list (List.map fst (LDecl.tohyps hyps).h_local) } in
      FApi.t_seqs
        [t_intros_i ids; aux0 st;
         t_generalize_hyps ~clear:`Yes ~missing:true ids]
        tc

    | SFlet (LTuple fs, f1, _) ->
      (* FIXME : does t_elimT_form change the hyps ? *)
      let tys    = List.map snd fs in
      let tc, hd = FApi.bwd1_of_fwd (pf_gen_tuple_elim tys hyps) tc in
      let pt     = { pt_head = PTHandle hd; pt_args = []; } in
      FApi.t_seq (t_elimT_form pt f1) (aux0 st) tc

    | SFimp (_, _) -> begin
      let id1 = LDecl.fresh_id hyps "_" in

      match t_intros_i_seq [id1] tt tc with
      | tc when FApi.tc_done tc -> tc
      | tc ->
          let tc = FApi.as_tcenv1 tc in
          let tc =
            let rw =
              t_rewrite_hyp ~xconv:`AlphaEq ~mode:`Bool ~donot:true
                id1 (`LtoR, None) in
            (    FApi.t_try (t_absurd_hyp ~conv:`AlphaEq ~id:id1)
              @! FApi.t_try (FApi.t_seq (FApi.t_try rw) tt)
              @! t_generalize_hyp ~clear:`Yes id1) tc
          in

          let iffail = t_crush_subst st id1 in
          let elims  = PGInternals.pg_cnj_elims in
          let reduce = if delta then `Full else `NoDelta in

          FApi.t_onall
            (FApi.t_switch ~on:`All ~ifok:(aux0 st) ~iffail (t_elim_r ~reduce elims))
            tc
    end

    | _ ->
       let reduce = if delta then `Full else `NoDelta in
       let thesplit tc = t_split ~closeonly:false ~reduce tc in
       let hyps0 = FApi.tc1_hyps tc in
       let shuffle = List.rev_map fst (LDecl.tohyps (FApi.tc1_hyps tc)).h_local in
       let st_split = { st with cs_undosubst = Sid.of_list shuffle } in
       let tc =
         match FApi.t_try_base (thesplit @! aux0 st_split) tc with
         | `Success tc -> tc
         | `Failure _  -> FApi.t_try tsolve tc in
       let pr = proofenv_of_proof (proof_of_tcenv tc) in
       let cl = List.map (FApi.get_pregoal_by_id^~ pr) (FApi.tc_opened tc) in
       let nl = List.length cl in
       match cl with | [] | [_] -> tc
       | _ :: _ ->
       let concl = f_ands (List.map (fun g -> g.g_concl) cl)  in
       let tc, hd = FApi.newgoal tc ~hyps:hyps0 concl in
       let pt = { pt_head = PTHandle hd; pt_args = []; } in
       let rec t_final n tc =
         if n = 1 then (t_intros_n 1 @! t_assumption `Alpha) tc
         else FApi.t_seqs [t_elim_and; t_intros_n 1; t_final (n-1)] tc in

       FApi.t_on1 nl t_id
         ~ttout:(t_shuffle shuffle @! t_cutdef pt concl @! t_final nl) tc

  and t_crush_subst st eqid tc =
    let togen = ref None in
    let t_subst tc =
      let hyps = FApi.tc1_hyps tc in
      let h = LDecl.hyp_by_id eqid hyps in
      match destr_eq_or_iff h with
      | p ->
        let sk = full_subst_kind in
        let newtc, gen =
          match LowSubst.is_eq_for_subst ~kind:sk ~tside:`LtoR hyps None p,
                LowSubst.is_eq_for_subst ~kind:sk ~tside:`RtoL hyps None p
          with
          | None, None -> raise InvalidGoalShape
          | Some _, None ->
            t_subst_x ~clear:SCnone ~kind:sk ~tside:`LtoR ~eqid:eqid ~except:st.cs_sbeq tc
          | None, Some _ ->
            t_subst_x ~clear:SCnone ~kind:sk ~tside:`RtoL ~eqid:eqid ~except:st.cs_sbeq tc
          | Some(_, v1, _, _), Some(_, v2, _, _) ->
            let get = function
              | `Glob (_, m) | `PVar (_, m) -> m
              | `Local x -> x in
            let x1 = get v1 in
            let x2 = get v2 in
            let tside =
              match Sid.mem x1 st.cs_undosubst, Sid.mem x2 st.cs_undosubst with
              | true, false -> `RtoL
              | false, true -> `LtoR
              | _, _ ->
                match v1, v2 with
                | `Local _, _ -> `LtoR
                | _, `Local _ -> `RtoL
                | _, _        -> `LtoR
            in
            t_subst_x ~clear:SCnone ~kind:sk ~tside ~eqid:eqid ~except:st.cs_sbeq tc
        in

(*      let _, _, side = gen in
      let f = EcEnv.LDecl.hyp_by_id eqid (FApi.tc1_hyps tc) in
      Format.eprintf "subst %s %a@." (if side = `LtoR then "LtoR" else "RtoL")
        (EcPrinting.pp_form (EcPrinting.PPEnv.ofenv (FApi.tc1_env tc))) f;
      pp_tc (FApi.tcenv_of_tcenv1 tc); *)
        togen := Some gen;
        newtc
      | exception (DestrError _) -> raise InvalidGoalShape in

    let t_init =
  (*    let sk1 = { empty_subst_kind with sk_local = true ; } in
      let sk2 = {  full_subst_kind with sk_local = false; } in *)
      t_intros_i [eqid] @!
        FApi.t_try t_subst (* (FApi.t_or (t_subst sk1) (t_subst sk2)) *) in

    let t_final tc =
      match !togen with
      | None -> t_generalize_hyp ~clear:`Yes ~missing:false eqid tc
      | Some (y, apost, side) ->
(*        let f = EcEnv.LDecl.hyp_by_id eqid (FApi.tc1_hyps tc) in
        Format.eprintf "subst %s %a@." (if side = `LtoR then "LtoR" else "RtoL")
        (EcPrinting.pp_form (EcPrinting.PPEnv.ofenv (FApi.tc1_env tc))) f;
        Format.eprintf "apost = @[%a@]@." (EcPrinting.pp_list "@ " EcIdent.pp_ident) (List.map fst apost);*)
        let moved = ref Sid.empty in
        let check_moved f = not (Mid.disjoint (fun _ _ _ -> false) f.f_fv !moved) in
        let doit (x,h) =
          let test =
            (Sid.mem x st.cs_undosubst &&
               match h with
               | LD_var (_, Some body) | LD_hyp body ->
              (*   Format.eprintf "body = %a@."
                   (EcPrinting.pp_form (EcPrinting.PPEnv.ofenv (FApi.tc1_env tc))) body; *)
                 Mid.mem y body.f_fv
               | _ -> false)
            || match h with
               | LD_var (_, Some body) | LD_hyp body -> check_moved body
               | _ -> false in
          if test then moved := Sid.add x !moved;
          test in
        let upost = List.filter doit apost in
        if upost = [] then t_clear eqid tc
        else
        let side = if side = `LtoR then `RtoL else `LtoR in
      (*  Format.eprintf "upost = @[%a@]@." (EcPrinting.pp_list "@ " EcIdent.pp_ident) (List.map fst upost); *)
        FApi.t_seqs [
          t_rw_for_subst y upost (FApi.tc1_goal tc) side eqid;
          t_generalize_hyp ~clear:`Yes ~missing:false eqid] tc
    in
    let entry tc =
      match !togen with
      | Some _ -> entry { st with cs_sbeq = Sid.add eqid st.cs_sbeq } tc
      | None   -> entry st tc in

    FApi.t_seqs [t_init; entry; t_final] tc

  in

  let state =
    { cs_undosubst = Sid.empty (*Sid.of_list (List.map fst (LDecl.tohyps (FApi.tc1_hyps tc)).h_local)*) ;
      cs_sbeq = (* Sid.of_list (List.map fst (LDecl.tohyps (FApi.tc1_hyps tc)).h_local)*) Sid.empty;
    } in
  FApi.t_seq (entry state) (t_simplify_with_info EcReduction.nodelta) tc


(* -------------------------------------------------------------------- *)
let t_trivial
  ?(subtc : FApi.backward option) ?(keep = false) ?(conv = `Alpha) (tc : tcenv1)
=
  let core  = FApi.t_or (t_assumption conv) (t_absurd_hyp ~conv:`AlphaEq) in
  let core  = FApi.t_try core in
  let core  = FApi.t_seqs [core; t_progress t_id; core] in

  let subtc = omap (fun tc -> FApi.t_seq tc (FApi.t_try (FApi.t_seq core t_fail))) subtc in
  let subtc = odfl t_id subtc in
  let seqs  = [FApi.t_try (t_false ~conv:`Conv ?id:None); core; subtc] in
  let seqs  = if keep then seqs else seqs @ [t_fail] in

  FApi.t_internal (FApi.t_try (FApi.t_seqs seqs)) tc

(* -------------------------------------------------------------------- *)
let t_congr (f1, f2) (args, ty) tc =
  let rec doit args ty tc =
    match args with
    | [] -> t_id tc

    | (a1, a2) :: args->
        let aty  = a1.f_ty in
        let m1   = f_app f1 (List.rev_map fst args) (tfun aty ty) in
        let m2   = f_app f2 (List.rev_map snd args) (tfun aty ty) in
        let tcgr = t_apply_s LG.p_fcongr [ty; aty] ~args:[m2; a1; a2] ~sk:1 in

        let tsub tc =
          let fx   = EcIdent.create "f" in
          let fty  = tfun aty ty in
          let body = f_app (f_local fx fty) [a1] ty in
          let lam  = EcFol.f_lambda [(fx, GTty fty)] body in
            FApi.t_sub
              [doit args fty]
              (t_apply_s LG.p_fcongr [ty; fty] ~args:[lam; m1; m2] ~sk:1 tc)
        in
          FApi.t_sub
            [tsub; tcgr]
            (t_transitivity (EcFol.f_app m2 [a1] ty) tc)
  in
  doit (List.rev args) ty tc

(* -------------------------------------------------------------------- *)
type smtmode = [`Standard | `Strict | `Report of EcLocation.t option]

(* -------------------------------------------------------------------- *)
let t_smt ~(mode:smtmode) pi tc =
  let error () =
    match mode with
    | `Standard ->
        tc_error !!tc ~catchable:true  "cannot prove goal"
    | `Strict ->
        tc_error !!tc ~catchable:false "cannot prove goal (strict)"
    | `Report loc ->
        EcEnv.notify (FApi.tc1_env tc) `Critical
          "%s: smt call failed"
          (loc |> omap EcLocation.tostring |> odfl "unknown");
        t_admit tc
  in

  let env, hyps, concl = FApi.tc1_eflat tc in
  let notify = (fun lvl (lazy s) -> EcEnv.notify env lvl "%s" s) in

  if   EcSmt.check ~notify pi hyps concl
  then FApi.xmutate1 tc `Smt []
  else error ()

(* -------------------------------------------------------------------- *)
let t_solve ?(canfail = true) ?(bases = [EcEnv.Auto.dname]) ?(depth = 1) (tc : tcenv1) =
  let bases = EcEnv.Auto.getall bases (FApi.tc1_env tc) in

  let t_apply1 p tc =
    let pt = PT.pt_of_uglobal !!tc (FApi.tc1_hyps tc) p in
    try
      Apply.t_apply_bwd_r ~mode:fmdelta ~canview:false pt tc
    with Apply.NoInstance _ -> t_fail tc in

  let rec t_apply ctn p  =
    if   ctn > depth
    then t_fail
    else t_apply1 p @! t_trivial @! t_solve (ctn + 1) bases

  and t_solve ctn bases =
    match bases with
    | [] -> t_abort
    | p::bases -> FApi.t_or (t_apply ctn p) (t_solve ctn bases) in

  let t = t_solve 0 bases in
  let t = if canfail then FApi.t_try t else t in

  t tc

(* --------------------------------------------------------------------- *)
let t_crush_fwd ?(delta = true) nb_intros (tc : tcenv1) =
  let t_progress_subst ?eqid =
    let sk1 = { empty_subst_kind with sk_local = true ; } in
    let sk2 = {  full_subst_kind with sk_local = false; } in
    FApi.t_or
      (t_subst ~clear:false ~kind:sk1 ?eqid)
      (t_subst ~clear:false ~kind:sk2 ?eqid)
  in

  let tt = FApi.t_try (t_assumption `Alpha) in

  let ts id = FApi.t_try (t_progress_subst ~eqid:id) in

  let rec aux0 (nbi : int) tc =
    FApi.t_seq (FApi.t_try tt) (aux1 nbi) tc

  and aux1 (nbi : int) tc =
    if nbi = 0 || FApi.tc_done (FApi.tcenv_of_tcenv1 tc) then t_id tc
    else

    let hyps, concl = FApi.tc1_flat tc in

    match sform_of_form concl with
    | SFimp (_, _) -> begin
      let id = LDecl.fresh_id hyps "_" in

      match t_intros_i_seq [id] tt tc with
      | tc when FApi.tc_done tc -> tc
      | tc ->
        let tc = FApi.as_tcenv1 tc in
        let tc =
          let rw =
            t_rewrite_hyp ~xconv:`AlphaEq ~mode:`Bool ~donot:true
              id (`LtoR, None) in
            (    FApi.t_try (t_absurd_hyp ~conv:`AlphaEq ~id)
              @! FApi.t_try (FApi.t_seq (FApi.t_try rw) tt)
              @! t_generalize_hyp ~clear:`Yes id) tc
        in

        let incr i = nbi + i - 1 in

        let iffail tc =
          (t_intros_i_seq [id] (ts id) @! aux0 (incr 0)) tc
        in

        let t_elim_false_r f concl tc =
          (t_elim_false_r f concl tc, t_id)

        and t_elim_and_r f concl tc =
          (t_elim_and_r f concl tc, aux0 (incr 2))

        and t_elim_eq_tuple_r f concl tc =
          let n, tc = t_elim_eq_tuple_r_n f concl tc in
          (tc, aux0 (incr n)) in

        let elims  = [ t_elim_false_r; t_elim_and_r; t_elim_eq_tuple_r; ] in
        let reduce = if delta then `Full else `NoDelta in

        FApi.t_onall
          (FApi.t_xswitch ~on:`All ~iffail (t_elim_r ~reduce elims))
          tc
      end

    | _ -> t_fail tc
  in

  FApi.t_seq
    (aux0 nb_intros)
    (t_simplify_with_info EcReduction.nodelta) tc
back to top