https://github.com/EasyCrypt/easycrypt
Tip revision: 3798b1a269fc1f40f3c09e248d29530f1a66d8d5 authored by Pierre-Yves Strub on 28 September 2021, 13:50:14 UTC
CI
CI
Tip revision: 3798b1a
ecLowGoal.ml
(* --------------------------------------------------------------------
* Copyright (c) - 2012--2016 - IMDEA Software Institute
* Copyright (c) - 2012--2018 - Inria
* Copyright (c) - 2012--2018 - Ecole Polytechnique
*
* Distributed under the terms of the CeCILL-C-V1 license
* -------------------------------------------------------------------- *)
(* -------------------------------------------------------------------- *)
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 ->
oeq EcMemory.lmt_equal m1 m2
| LD_modty (mt1, mr1), LD_modty (mt2, mr2) ->
(mt1 == mt2) && (mr1 == mr2)
| 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)
(* ------------------------------------------------------------------ *)
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.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, restr), PAModule (mp, mt) -> begin
(* FIXME: poor API ==> poor error recovery *)
try
EcTyping.check_modtype_with_restrictions env mp mt emt restr;
EcPV.check_module_in env mp emt;
(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
type kind = [`Value | `Module | `Memory]
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, r) ->
LowIntro.check_name_validity !!tc `Module name;
(id, LD_modty (i, r), 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
| 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
| 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
| _ 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 =
List.fold_left 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
FApi.close tc (VIntros (hd, List.map tg_val ids))
end
(* -------------------------------------------------------------------- *)
let t_intros (ids : ident mloc list) (tc : tcenv1) =
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) =
t_intros_x (EcUtils.List.make n (notag None)) tc
(* -------------------------------------------------------------------- *)
let t_intro_i_x (id : EcIdent.t option) (tc : tcenv1) =
t_intros_x [notag id] tc
(* -------------------------------------------------------------------- *)
let t_intro_i (id : EcIdent.t) (tc : tcenv1) =
t_intro_i_x (Some id) tc
(* -------------------------------------------------------------------- *)
let t_intro_s (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_intros_i (ids : EcIdent.t list) (tc : tcenv1) =
t_intros_x (List.map (notag |- some) ids) tc
(* -------------------------------------------------------------------- *)
let t_intros_s (ids : inames) (tc : tcenv1) =
match ids with
| `Symbol x -> t_intros_i (List.map EcIdent.create x) tc
| `Ident x -> t_intros_i x 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 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
raise InvalidGoalShape;
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 rec 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,r) ->
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.Mod.by_mpath mp env).EcModules.me_sig in
let bds = `Forall (x, GTmodty (mt, r)) :: 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 declare 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,r) -> f_forall [id, GTmodty(mt,r)] 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)
| 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