https://github.com/EasyCrypt/easycrypt
Tip revision: a2c11f189da68d291d48547461aff2432662e9e8 authored by François Dupressoir on 05 September 2024, 14:37:36 UTC
[ci] diversified external CI selects a valid branch
[ci] diversified external CI selects a valid branch
Tip revision: a2c11f1
ecLowGoal.ml
(* -------------------------------------------------------------------- *)
open EcUtils
open EcMaps
open EcLocation
open EcIdent
open EcSymbols
open EcPath
open EcAst
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) (subgoals : _) (tc : ckenv) =
let hyps = hyps_of_ckenv tc in
match pt with
| PTCut (f, cutsolve) -> begin
match tc with
| `Hyps ( _, _) -> (PTCut (f, None), f, subgoals) (* FIXME *)
| `Tc (tc, _) ->
(* cut - create a dedicated subgoal *)
let handle = RApi.newgoal tc ~hyps f in
let subgoals =
ofold
(fun cutsolve subgoals -> DMap.add handle cutsolve subgoals)
subgoals cutsolve
in (PTHandle handle, f, subgoals)
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, subgoals)
end
| PTLocal x -> begin
let hyps = hyps_of_ckenv tc in
try (pt, LDecl.hyp_by_id x hyps, subgoals)
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, subgoals)
| PTTerm pt ->
let pt, ax, subgoals = check_ `Elim pt subgoals tc in
(PTTerm pt, ax, subgoals)
(* ------------------------------------------------------------------ *)
and check_ (mode : [`Intro | `Elim]) (pt : proofterm) (subgoals : _) (tc : ckenv) =
let hyps = hyps_of_ckenv tc in
let env = LDecl.toenv hyps in
let rec check_args (sbt, ax, nargs) subgoals args =
match args with
| [] -> (Fsubst.f_subst sbt ax, List.rev nargs, subgoals)
| arg :: args ->
let ((sbt, ax), narg, subgoals) = check_arg (sbt, ax) subgoals arg in
check_args (sbt, ax, narg :: nargs) subgoals args
and check_arg (sbt, ax) subgoals arg =
let check_binder (x, xty) f =
let xty = Fsubst.gty_subst 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
EcTyping.check_modtype env mp mt emt;
(EcFol.f_bind_mod sbt x mp env, 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 -> EcCoreGoal.ptcut f1
| Some subpt -> subpt
in
let subpt, subax, subgoals = check_ mode subpt subgoals tc in
if not (EcReduction.is_conv hyps f1 subax) then
raise InvalidProofTerm;
((sbt, f2), PASub (Some subpt), subgoals)
| Some (`Forall (x, xty, f)), _ ->
(check_binder (x, xty) f, arg, subgoals)
| _, _ ->
if Fsubst.is_subst_id sbt then
raise InvalidProofTerm;
check_arg (Fsubst.f_subst_id, Fsubst.f_subst sbt ax) subgoals arg
end
| `Intro -> begin
match TTC.destruct_exists hyps ax with
| Some (`Exists (x, xty, f)) ->
(check_binder (x, xty) f, arg, subgoals)
| None ->
if Fsubst.is_subst_id sbt then
raise InvalidProofTerm;
check_arg (Fsubst.f_subst_id, Fsubst.f_subst sbt ax) subgoals arg
end
in
match pt with
| PTApply pt ->
let (nhd, ax, subgoals) = check_pthead pt.pt_head subgoals tc in
let ax, nargs, subgoals =
check_args (Fsubst.f_subst_id, ax, []) subgoals pt.pt_args in
(PTApply { pt_head = nhd; pt_args = nargs }, ax, subgoals)
| PTQuant (bd, pt) -> begin
match mode with
| `Intro -> raise InvalidProofTerm
| `Elim ->
let pt, ax, subgoals = check_ `Elim pt subgoals tc in
(PTQuant (bd, pt), f_forall [bd] ax, subgoals)
end
let check_with_cutsolve (mode : [`Intro | `Elim]) (pt : proofterm) (tc : ckenv) =
check_ mode pt DMap.empty tc
let check (mode : [`Intro | `Elim]) (pt : proofterm) (tc : ckenv) =
let pt, f, subgoals = check_ mode pt DMap.empty tc in
assert (DMap.is_empty subgoals);
(pt, f)
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 opmode = EcReduction.deltap
type simplify_t =
?target:ident -> ?delta:opmode -> ?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 = `IfTransparent) ?(logic = Some `Full) (tc : tcenv1) =
let ri = { nodelta with delta_p = fun _ -> delta } 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 = `IfTransparent) ?(logic = Some `Full) (tc : tcenv1) =
let ri = { nodelta with delta_p = fun _ -> delta } 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.gty_subst 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_absmod sbt x (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 = ty_subst sbt 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 ?(clear = false) (n : int) (tc : tcenv1) =
let tc, xs = t_intros_x (EcUtils.List.make n (notag None)) tc in
if clear then FApi.t_first (t_clears xs) tc else tc
(* -------------------------------------------------------------------- *)
let t_intros_n_x (n : int) (tc : tcenv1) =
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_s_1 (ids : inames) (tc : tcenv1) =
FApi.as_tcenv1 (t_intros_s 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
(* -------------------------------------------------------------------- *)
type cutsolver = {
smt : FApi.backward;
done_ : FApi.backward;
}
(* -------------------------------------------------------------------- *)
let tt_apply ?(cutsolver : cutsolver option) (pt : proofterm) (tc : tcenv) =
let (hyps, concl) = FApi.tc_flat tc in
let tc, (pt, ax, subgoals) =
RApi.to_pure (fun tc -> LowApply.check_with_cutsolve `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;
let tc = FApi.close tc (VApply pt) in
match cutsolver with
| None ->
assert (DMap.is_empty subgoals);
tc
| Some cutsolver -> begin
Format.eprintf "%d@." (DMap.cardinal subgoals);
FApi.t_onall (fun tc ->
let tactic =
match DMap.find_opt (FApi.tc1_handle tc) subgoals with
| Some `Smt -> cutsolver.smt
| Some `Done -> cutsolver.done_
| Some `DoneSmt -> FApi.t_seq cutsolver.done_ cutsolver.smt
| None -> t_id in
tactic tc
) tc
end
(* -------------------------------------------------------------------- *)
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
ptlocal ~args x 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
ptglobal ~args ~tys p 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
pthandle ~args hd in
tt_apply pt tc
(* -------------------------------------------------------------------- *)
let t_apply ?(cutsolver : cutsolver option) (pt : proofterm) (tc : tcenv1) =
tt_apply ?cutsolver 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_absmod s id 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 = ptcut ~args:(List.rev args) ff 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 = pthandle ~args (FApi.tc1_handle tc) 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 = ptapply ind 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 = ptglobal ~tys:typ p 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 = ptglobal ~tys:typ p 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 = pthandle hd in
(tc, pt, 0)
| _ when EcReduction.EqTest.for_type env tunit ty ->
let pt = ptglobal ~tys:[] LG.p_unit_elim in
(tc, pt, 0)
| _ when EcReduction.EqTest.for_type env tint ty ->
let pt = ptglobal ~tys:[] EcCoreLib.CI_Int.p_int_elim in
(tc, pt, 1)
| _ when EcReduction.EqTest.for_type env tbool ty ->
let pt = ptglobal ~tys:[] LG.p_bool_elim 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 = ptlocal h 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) -> begin
match LDecl.hyp_convert h (fun _ _ -> tgfp) (RApi.tc_hyps tc) with
| Some hyps ->
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))
| None -> ()
end;
RApi.tcenv_of_rtcenv tc
(* -------------------------------------------------------------------- *)
let t_rewrite_hyp ?xconv ?mode ?donot (id : EcIdent.t) pos (tc : tcenv1) =
t_rewrite ?xconv ?mode ?donot (ptlocal id) pos tc
(* -------------------------------------------------------------------- *)
type vsubst = [
| `Local of EcIdent.t
| `Glob of EcIdent.t * 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', _)) when kind.sk_glob ->
if EcIdent.id_equal mp mp'
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 (EcPath.mident 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 (EcPath.mident 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 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)
| 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:`No) 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 = pthandle hd 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:`No @! 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 = pthandle hd 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 = pthandle hd 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 = [`Sloppy | `Strict | `Report of EcLocation.t option]
(* -------------------------------------------------------------------- *)
let t_smt ~(mode:smtmode) pi tc =
let error () =
match mode with
| `Sloppy ->
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_coq
~(loc : EcLocation.t)
~(name : string)
~(mode : smtmode)
(coqmode : EcProvers.coq_mode option)
(pi : EcProvers.prover_infos)
(tc : tcenv1)
=
let error () =
match mode with
| `Sloppy ->
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: Coq 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 EcCoq.check ~loc ~name ~notify ?coqmode pi hyps concl
then FApi.xmutate1 tc `Smt []
else error ()
(* -------------------------------------------------------------------- *)
let t_solve ?(canfail = true) ?(bases = [EcEnv.Auto.dname]) ?(mode = fmdelta) ?(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 ~canview:false pt tc
with Apply.NoInstance _ -> t_fail tc in
let rec t_apply ctn p tc =
if ctn > depth
then t_fail tc
else (t_apply1 p @! t_trivial @! t_solve (ctn + 1) bases) tc
and t_solve ctn bases tc =
match bases with
| [] -> t_abort tc
| p::bases -> (FApi.t_or (t_apply ctn p) (t_solve ctn bases)) tc 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
