https://github.com/EasyCrypt/easycrypt
Tip revision: 846710a2a656834065e745d19416ebdc83158f55 authored by Benjamin Gregoire on 14 July 2019, 06:50:07 UTC
Start restructuration of the code to be able to avant mutual dependency between type and mpath
Start restructuration of the code to be able to avant mutual dependency between type and mpath
Tip revision: 846710a
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 = EcProofTyping.lazyred
(* -------------------------------------------------------------------- *)
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 rec h_eqs h1 h2 =
match h1, h2 with
| [], _ -> true
| _, [] -> false
| (x1, v1) :: subh1, (x2, v2) :: subh2 ->
if not (id_equal x1 x2) then h_eqs h1 subh2 else
if v1 (*φ*)== v2 then h_eqs subh1 subh2 else begin
match v1, v2 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
end && h_eqs subh1 subh2
in h_eqs ld1.h_local ld2.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_change_r ?target action (tc : tcenv1) =
match target with
| None -> begin
let hyps, concl = FApi.tc1_flat tc in
match action (lazy hyps) concl with
| None -> 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_change ?target (fp : form) (tc : tcenv1) =
let action (lazy hyps) tgfp =
if not (EcReduction.is_conv hyps fp tgfp) then
raise InvalidGoalShape;
if fp == tgfp then None else Some fp
in t_change_r ?target action tc
(* -------------------------------------------------------------------- *)
let t_simplify_with_info ?target (ri : reduction_info) (tc : tcenv1) =
let action (lazy hyps) fp = Some (EcReduction.simplify ri hyps fp) in
FApi.tcenv_of_tcenv1 (t_change_r ?target action tc)
(* -------------------------------------------------------------------- *)
let t_simplify ?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_simplify_with_info ?target ri tc
(* -------------------------------------------------------------------- *)
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 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 ?reduce (tc : tcenv1) =
let t_reflex_r (fp : form) (tc : tcenv1) =
match sform_of_form fp with
| SFeq (f1, _f2) -> t_reflex_s f1 tc
| _ -> raise TTC.NoMatch
in
TTC.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
TTC.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
TTC.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
TTC.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
TTC.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
TTC.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
TTC.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 TTC.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 TTC.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 (-1) in
let accept pri =
match EcInductive.prind_is_iso_ands pri with
| None -> false
| Some (_, ngoals) -> outgoals := ngoals; true in
let tc = t_elim_prind_r ?reduce ~accept `Case tc in (!outgoals, tc)
(* -------------------------------------------------------------------- *)
let t_split ?(closeonly = false) ?reduce (tc : tcenv1) =
let t_split_r (fp : form) (tc : tcenv1) =
let hyps, concl = FApi.tc1_flat 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 EcReduction.is_conv hyps f1 f2 ->
t_reflex_s f1 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
| SFif (cond, _, _) when not closeonly ->
(* FIXME: simplify goal *)
let tc = if f_equal concl fp then tc else t_change fp tc in
let tc = t_case cond tc in
tc
| _ -> raise TTC.NoMatch
in
TTC.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 TTC.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 TTC.t_lazy_match ?reduce t_split_r tc
(* -------------------------------------------------------------------- *)
type rwspec = [`LtoR|`RtoL] * ptnpos option
type rwmode = [`Bool | `Eq]
(* -------------------------------------------------------------------- *)
let t_rewrite
?xconv ?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 ?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 env var f =
let kind = odfl default_subst_kind kind in
match f.f_node, var with
(* Substitution of logical variables *)
| Flocal x, None when kind.sk_local ->
Some (`Local x)
| Flocal x, Some (`Local y) when kind.sk_local && id_equal x y ->
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, (eq, tg))))
in
let env = LDecl.toenv hyps in
let var = List.pmap identity
[is_member_for_subst ?kind `LtoR env var f1 f2;
is_member_for_subst ?kind `RtoL env 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
Pervasives.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
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
(* ------------------------------------------------------------------ *)
let build_subst env var f =
match var with
| `Local x ->
let subst = Fsubst.f_subst_local x f in
let check tg = Mid.mem x tg.f_fv in
(subst, check)
| `PVar (pv, m) ->
let subst = EcPV.PVM.add env pv m f EcPV.PVM.empty in
let check _tg = true in
(EcPV.PVM.subst env subst, check)
| `Glob (mp, m) ->
let subst = EcPV.PVM.add_glob env mp m f EcPV.PVM.empty in
let check _tg = true in
(EcPV.PVM.subst env subst, check)
end
(* -------------------------------------------------------------------- *)
let t_subst ?kind ?tg ?(clear = true) ?var ?tside ?eqid (tc : tcenv1) =
let env, hyps, concl = FApi.tc1_eflat tc in
let subst1 (subst, check) moved (id, lk) =
if tg |> omap (fun tg -> not (Sid.mem id tg)) |> odfl false
then `Pre (id, lk)
else
let check tg =
check tg || not (Mid.disjoint (fun _ _ _ -> false) tg.f_fv moved) in
match lk with
| LD_var (_ty, None) ->
`Pre (id, lk)
| LD_var (ty, Some body) ->
if check body
then `Post (id, LD_var (ty, Some (subst body)))
else `Pre (id, LD_var (ty, Some body))
| LD_hyp hform ->
if check hform
then `Post (id, LD_hyp (subst hform))
else `Pre (id, LD_hyp hform)
| LD_mem _ -> `Pre (id, lk)
| LD_modty _ -> `Pre (id, lk)
| LD_abs_st _ -> `Pre (id, lk)
in
let eqs =
eqid
|> omap (fun id -> [id, LD_hyp (LDecl.hyp_by_id id hyps)])
|> ofdfl (fun () -> (LDecl.tohyps hyps).h_local)
in
let try1 eq =
match eq with
| id, LD_hyp f when is_eq_or_iff f -> begin
let dosubst (var, f) =
let subst, check = LowSubst.build_subst env var f 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 pre, hpost, _ =
List.fold_right
(fun h (pre, hpost, moved) ->
assert (not (id_equal (fst h) id));
match h, var with
| (x, _), _ ->
match subst1 (subst, check) moved h with
| `Pre (id, lk) -> ((id, lk) :: pre, hpost, moved)
| `Post (id, lk) ->
match lk with
| LD_var (_, _) -> (pre, (id, lk) :: hpost, Sid.add x moved)
| _ -> (pre, (id, lk) :: hpost, moved))
pre ([], [], Sid.empty) in
let post =
List.fold_right
(fun h post ->
assert (not (id_equal (fst h) id));
match subst1 (subst, check) Sid.empty h with
| `Pre (id, lk) | `Post (id, lk) -> (id, lk) :: post)
post [] in
let concl' = subst concl in
let hyps' = hpost @ post @ pre in
let hyps' =
LDecl.init (LDecl.baseenv hyps)
~locals:hyps' (LDecl.tohyps hyps).h_tvar in
let clear =
match var with
| `Local x when clear -> begin
match LDecl.by_id x hyps with
| LD_var (_, None) -> t_clear x
| _ -> t_id
end
| _ -> t_id
in
FApi.t_focus clear (FApi.xmutate1_hyps tc `Subst [hyps', concl'])
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
try List.find_map try1 eqs
with Not_found -> raise InvalidGoalShape
(* -------------------------------------------------------------------- *)
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
(* -------------------------------------------------------------------- *)
type cstate = {
cs_sbeq : Sid.t option;
}
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 t_progress_subst ?(tg : Sid.t option) ?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 ?tg ~clear:false ~kind:sk1 ?eqid)
(t_subst ?tg ~clear:false ~kind:sk2 ?eqid)
in
let tt = FApi.t_try (t_assumption `Alpha) in
let ts ?tg id =
FApi.t_try (t_progress_subst ?tg ~eqid:id) in
(* Entry of progress: simplify goal, and chain with progress *)
let rec entry (st : cstate) tc =
FApi.t_seq (t_simplify ~delta:false) (aux0 st) tc
(* Progress (level 0): try to apply user tactic. *)
and aux0 (st : cstate) tc =
FApi.t_seq (FApi.t_try tt) (aux1 st) tc
(* 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_sbeq = st.cs_sbeq |> omap (fun tg ->
List.fold_left ((^~) Sid.add) tg ids) } in
FApi.t_seqs
[t_intros_i ids; aux0 st;
t_generalize_hyps ~clear:`Yes ~missing:true ids]
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 st) tc
| 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 st = { st with cs_sbeq = st.cs_sbeq |> omap (Sid.add id); } in
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 iffail tc =
t_intros_i_seq [id]
(FApi.t_seqs
[ts ?tg:st.cs_sbeq id; entry st;
t_generalize_hyp ~clear:`Yes ~missing:true id])
tc
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 = t_split ~closeonly:false ~reduce in
let tc =
let stsub = { st with cs_sbeq = Some Sid.empty } in
match FApi.t_try_base (FApi.t_seq thesplit (aux0 stsub)) 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 cl = f_ands (List.map (fun g -> g.g_concl) cl) in
let tc, hd = FApi.newgoal tc ~hyps cl in
let pt = { pt_head = PTHandle hd; pt_args = []; } in
FApi.t_on1 nl t_id
~ttout:(FApi.t_seqs [t_cutdef pt cl; aux0 st; t_abort])
tc
in
let state = { cs_sbeq = None; } in
FApi.t_seq (entry state) (t_simplify_with_info EcReduction.nodelta) tc
(* -------------------------------------------------------------------- *)
let t_logic_trivial (tc : tcenv1) =
let seqs = [
FApi.t_try (t_assumption `Conv);
t_progress t_id;
FApi.t_try (t_assumption `Conv);
FApi.t_try (t_absurd_hyp ~conv:`AlphaEq);
t_fail;
]
in FApi.t_internal (FApi.t_try (FApi.t_seqs seqs)) tc
(* -------------------------------------------------------------------- *)
let t_trivial ?(subtc : FApi.backward option) (tc : tcenv1) =
let tryassum = FApi.t_try (t_assumption `Conv) in
let tprogress = t_progress t_id in
let subtc = subtc |> odfl t_id in
let seqs =
[tryassum; tprogress; tryassum; subtc; t_logic_trivial; 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_auto ?(bases = [EcEnv.Auto.dname]) ?(depth = 1) (tc : tcenv1) =
let module E = struct
exception Done of tcenv
exception Fail
end in
let bases = EcEnv.Auto.getall bases (FApi.tc1_env tc) in
let rec forall ctn tc =
if ctn >= depth then t_fail tc else begin
List.iter
(fun p -> try raise (E.Done (for1 ctn p tc)) with E.Fail -> ())
bases;
t_id tc
end
and for1 ctn (p : EcPath.path) tc =
let pt = PT.pt_of_uglobal !!tc (FApi.tc1_hyps tc) p in
try
FApi.t_seqs
[Apply.t_apply_bwd_r ~mode:fmrigid ~canview:false pt;
t_trivial; forall (ctn+1)]
tc
with Apply.NoInstance _ ->
raise E.Fail
in
try forall 0 tc with E.Done tc -> 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