swh:1:snp:1160b607213f14ec0f922dad3284705c8e588b30
Tip revision: 03fd7f2c77df23d8f806e8b05d08b20b36f5d9d6 authored by Pierre-Yves Strub on 10 October 2017, 09:04:16 UTC
compile with up-to-date toolchain
compile with up-to-date toolchain
Tip revision: 03fd7f2
ecLowGoal.ml
(* --------------------------------------------------------------------
* Copyright (c) - 2012--2016 - IMDEA Software Institute
* Copyright (c) - 2012--2016 - Inria
*
* 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 (@~) (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 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 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)
| 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_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_value_name (x : symbol) =
x = "_" || EcIo.is_sym_ident x || EcIo.is_mem_ident x
let valid_mod_name (x : symbol) = x = "_" || EcIo.is_mod_ident x
let valid_mem_name (x : symbol) = x = "_" || EcIo.is_mem_ident x
let valid_mdistr_name (x : symbol) = x = "_" || EcIo.is_mdistr_ident x
type kind = [`Value | `Module | `MemDistr]
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)
| `MemDistr -> valid_mdistr_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 (ids : ident mloc list) (tc : tcenv1) =
let add_local id sbt x gty =
let gty = Fsubst.gty_subst sbt gty in
let name = tg_map EcIdent.name id in
let id = tg_val id in
match gty with
| GTty ty ->
LowIntro.check_name_validity !!tc `Value name;
(LD_var (ty, None), Fsubst.f_bind_local sbt x (f_local id ty))
| GTmodty (i, r) ->
LowIntro.check_name_validity !!tc `Module name;
(LD_modty (i, r), Fsubst.f_bind_mod sbt x (EcPath.mident 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 (ld, sbt) = add_local 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 hyps = add_ld id (LD_hyp prem) hyps in
(hyps, concl), sbt
| SFlet (LSymbol (x, xty), xe, concl) ->
let xty = sbt.fs_ty xty in
let xe = Fsubst.f_subst sbt xe in
let sbt = Fsubst.f_bind_local sbt x (f_local (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
(* -------------------------------------------------------------------- *)
type iname = [`Symbol of symbol | `Ident of EcIdent.t ]
type inames = [`Symbol of symbol list | `Ident of EcIdent.t list]
(* -------------------------------------------------------------------- *)
let t_intro_i (id : EcIdent.t) (tc : tcenv1) =
t_intros [notag id] tc
(* -------------------------------------------------------------------- *)
let t_intro_s (id : iname) (tc : tcenv1) =
match id with
| `Symbol x -> t_intro_i (EcIdent.create x) tc
| `Ident x -> t_intro_i x tc
(* -------------------------------------------------------------------- *)
let t_intros_i (ids : EcIdent.t list) (tc : tcenv1) =
t_intros (List.map notag 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 argpt = { pt with ptev_env = PT.copy pt.ptev_env } 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_head = PTGlobal (p, []);
pt_args = List.map (fun f -> PAFormula f) fs; } in
let viewpt, ax = LowApply.check `Elim viewpt (`Hyps (hyps, !!tc)) in
(* Apply view to its actual arguments *)
let viewpt = apply_pterm_to_arg
{ ptev_env = argpt.ptea_env;
ptev_pt = viewpt;
ptev_ax = ax; }
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_lr, [f1; f2]);
(LG.p_iff_rl, [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 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, _) ->
let x = fresh id in
let s = Fsubst.f_bind_local s id (f_local 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_modty (mt,r) ->
let x = EcIdent.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)
(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 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 ids tc
let t_generalize_hyp ?clear ?missing ?naming id tc =
t_generalize_hyps ?clear ?missing ?naming [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 ((_, 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;
RApi.tcenv_of_rtcenv tc
| _ -> raise TTC.NoMatch
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
?target ?(mode : rwmode option) (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 (left, right) =
let doit ax =
match sform_of_form ax, mode with
| SFeq (f1, f2), (None | Some `Eq) -> (f1, f2)
| SFiff (f1, f2), (None | Some `Eq) -> (f1, f2)
| _, (None | Some `Bool) when
s = `LtoR && ER.EqTest.for_type env ax.f_ty tbool
-> (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 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 (id : EcIdent.t) pos (tc : tcenv1) =
let pt = { pt_head = PTLocal id; pt_args = []; } in
t_rewrite ?mode:None pt pos tc
(* -------------------------------------------------------------------- *)
type vsubst = [
| `Local of EcIdent.t
| `Glob of EcPath.mpath * form
| `PVar of EcTypes.prog_var * form
]
(* -------------------------------------------------------------------- *)
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 | `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' && f_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 : tside)) hyps var (f1, f2) =
let canl = match tside with `All | `LtoR -> true | `RtoL -> false in
let canr = match tside with `All | `RtoL -> true | `LtoR -> false in
let is_member_for_subst ?kind side env var f =
match side with
| `Left when canl -> is_member_for_subst ?kind env var f
| `Right when canr -> is_member_for_subst ?kind env var f
| _ -> None
in
let env = LDecl.toenv hyps in
let var =
match is_member_for_subst ?kind `Left env var f1 with
| Some var -> Some (var, f2)
| None ->
match is_member_for_subst ?kind `Right env var f2 with
| Some var -> Some (var, f1)
| None -> None
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 m = destr_local m in
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 m = destr_local m in
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 ?(clear = true) ?var ?tside ?eqid (tc : tcenv1) =
let env, hyps, concl = FApi.tc1_eflat tc in
let subst1 (subst, check) moved (id, lk) =
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_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 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 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 ()