Revision 9d08a76fb50773e0b6b1afad31f37dfb821fee75 authored by Benjamin Gregoire on 24 November 2022, 16:10:02 UTC, committed by Benjamin Gregoire on 24 November 2022, 16:10:02 UTC
1 parent 69c9c2e
ecPhlExists.ml
(* -------------------------------------------------------------------- *)
open EcUtils
open EcFol
open EcEnv
open EcModules
open EcCoreGoal
open EcLowGoal
open EcLowPhlGoal
module L = EcLocation
module APT = EcParsetree
module TTC = EcProofTyping
module PT = EcProofTerm
(* -------------------------------------------------------------------- *)
let get_to_gens fs =
let do_id f =
let id =
match f.f_node with
| Fpvar (pv, m) -> id_of_pv pv m
| Fglob (mp, m) -> id_of_mp mp m
| _ -> EcIdent.create "f" in
id, f in
List.map do_id fs
(* -------------------------------------------------------------------- *)
let t_hr_exists_elim_r ?bound tc =
let pre = tc1_get_pre tc in
let bd, pre =
try destr_exists_prenex pre
with DestrError _ -> [], pre in
let bd, pre =
bound
|> omap (fun bound ->
let bound = min bound (List.length bd) in
let bd1, bd2 = List.takedrop bound bd in
(bd1, f_exists bd2 pre))
|? (bd, pre) in
(* FIXME: check that bd is not bound in the post *)
let concl = f_forall bd (set_pre ~pre (FApi.tc1_goal tc)) in
FApi.xmutate1 tc `HlExists [concl]
(* -------------------------------------------------------------------- *)
let t_hr_exists_intro_r fs tc =
let hyps = FApi.tc1_hyps tc in
let concl = FApi.tc1_goal tc in
let pre = tc1_get_pre tc in
let post = tc1_get_post tc in
let side = is_equivS concl || is_equivF concl in
let gen = get_to_gens fs in
let eqs = List.map (fun (id, f) -> f_eq (f_local id f.f_ty) f) gen in
let bd = List.map (fun (id, f) -> (id, GTty f.f_ty)) gen in
let pre = f_exists bd (f_and (f_ands eqs) pre) in
let h = LDecl.fresh_id hyps "h" in
let ms, subst =
match side with
| true ->
let ml, mr = as_seq2 (LDecl.fresh_ids hyps ["&ml"; "&mr"]) in
let s = Fsubst.f_subst_id in
let s = Fsubst.f_bind_mem s mleft ml in
let s = Fsubst.f_bind_mem s mright mr in
([ml; mr], s)
| false ->
let m = LDecl.fresh_id hyps "&m" in
let s = Fsubst.f_subst_id in
let s = Fsubst.f_bind_mem s mhr m in
([m], s)
in
let args =
let do1 (_, f) = PAFormula (Fsubst.f_subst subst f) in
List.map do1 gen
in
let tactic =
FApi.t_seqsub (EcPhlConseq.t_conseq pre post)
[ FApi.t_seqs [
t_intros_i (ms@[h]);
t_exists_intro_s args;
t_apply_hyp h;
];
t_trivial;
t_id]
in
FApi.t_internal tactic tc
(* -------------------------------------------------------------------- *)
let t_hr_exists_elim = FApi.t_low0 "hr-exists-elim" t_hr_exists_elim_r
let t_hr_exists_intro = FApi.t_low1 "hr-exists-intro" t_hr_exists_intro_r
(* -------------------------------------------------------------------- *)
let process_exists_intro ~(elim : bool) fs tc =
let (hyps, concl) = FApi.tc1_flat tc in
let penv =
match concl.f_node with
| FhoareF hf -> fst (LDecl.hoareF hf.hf_f hyps)
| FhoareS hs -> LDecl.push_active hs.hs_m hyps
| FcHoareF hf -> fst (LDecl.hoareF hf.chf_f hyps)
| FcHoareS hs -> LDecl.push_active hs.chs_m hyps
| FbdHoareF bhf -> fst (LDecl.hoareF bhf.bhf_f hyps)
| FbdHoareS bhs -> LDecl.push_active bhs.bhs_m hyps
| FequivF ef -> fst (LDecl.equivF ef.ef_fl ef.ef_fr hyps)
| FequivS es -> LDecl.push_all [es.es_ml; es.es_mr] hyps
| _ -> tc_error_noXhl ~kinds:hlkinds_Xhl !!tc
in
let fs =
List.map
(fun f -> TTC.pf_process_form_opt !!tc penv None f)
fs
in
let tc = t_hr_exists_intro_r fs tc in
if elim then
t_hr_exists_elim_r ~bound:(List.length fs) (FApi.as_tcenv1 tc)
else tc
(* -------------------------------------------------------------------- *)
let process_ecall oside (l, tvi, fs) tc =
let (hyps, concl) = FApi.tc1_flat tc in
let hyps, kind =
match concl.f_node with
| FhoareS hs when is_none oside ->
(LDecl.push_active hs.hs_m hyps, `Hoare (List.length hs.hs_s.s_node))
| FequivS es ->
let n1 = List.length es.es_sl.s_node in
let n2 = List.length es.es_sr.s_node in
(LDecl.push_all [es.es_ml; es.es_mr] hyps, `Equiv (n1, n2))
| _ -> tc_error_noXhl ~kinds:[`Hoare `Stmt; `Equiv `Stmt] !!tc
in
let t_local_seq p1 tc =
match kind, oside with
| `Hoare n, _ ->
EcPhlApp.t_hoare_app
(Zpr.cpos (n-1)) p1 tc
| `Equiv (n1, n2), None ->
EcPhlApp.t_equiv_app
(Zpr.cpos (n1-1), Zpr.cpos (n2-1)) p1 tc
| `Equiv (n1, n2), Some `Left ->
EcPhlApp.t_equiv_app
(Zpr.cpos (n1-1), Zpr.cpos n2) p1 tc
| `Equiv(n1, n2), Some `Right ->
EcPhlApp.t_equiv_app
(Zpr.cpos n1, Zpr.cpos (n2-1)) p1 tc
in
let fs =
List.map
(fun f -> TTC.pf_process_form_opt !!tc hyps None f)
fs
in
let ids, p1 =
let sub = t_local_seq f_true tc in
let sub = FApi.t_rotate `Left 1 sub in
let sub = FApi.t_focus (t_hr_exists_intro_r fs) sub in
let sub = FApi.t_focus (t_hr_exists_elim_r ~bound:(List.length fs)) sub in
let ids =
try fst (EcFol.destr_forall (FApi.tc_goal sub))
with DestrError _ -> [] in
let ids = List.map (snd_map gty_as_ty) ids in
let nms = List.map (fun (_, x) -> (EcIdent.create "_", x)) ids in
let sub = FApi.t_focus (EcLowGoal.t_intros_i (List.fst nms)) sub in
let pte = PT.ptenv_of_penv (FApi.tc_hyps sub) !!tc in
let pt = PT.process_pterm pte (APT.FPNamed (l, tvi)) in
let pt =
List.fold_left (fun pt (id, ty) ->
PT.apply_pterm_to_arg_r pt (PT.PVAFormula (f_local id ty)))
pt ids in
assert (PT.can_concretize pt.PT.ptev_env);
let _pt, ax = PT.concretize pt in
let sub = FApi.t_focus (EcPhlCall.t_call oside ax) sub in
let sub = FApi.t_rotate `Left 1 sub in
let sub = oget (get_post (FApi.tc_goal sub)) in
let subst =
List.fold_left2
(fun s id f -> Fsubst.f_bind_local s id f)
Fsubst.f_subst_id (List.fst ids) fs in
(nms, Fsubst.f_subst subst sub) in
let tc = t_local_seq p1 tc in
let tc = FApi.t_rotate `Left 1 tc in
let tc = FApi.t_focus (t_hr_exists_intro_r fs) tc in
let tc = FApi.t_focus (t_hr_exists_elim_r ~bound:(List.length fs)) tc in
let tc = FApi.t_focus (EcLowGoal.t_intros_i (List.fst ids)) tc in
let pte = PT.ptenv_of_penv (FApi.tc_hyps tc) (FApi.tc_penv tc) in
let pt = PT.process_pterm pte (APT.FPNamed (l, tvi)) in
let pt =
List.fold_left (fun pt (id, ty) ->
PT.apply_pterm_to_arg_r pt (PT.PVAFormula (f_local id ty)))
pt ids in
assert (PT.can_concretize pt.PT.ptev_env);
let pt, ax = PT.concretize pt in
let tc = FApi.t_focus (EcPhlCall.t_call oside ax) tc in
let tc = FApi.t_focus (EcLowGoal.Apply.t_apply_bwd_hi ~dpe:true pt) tc in
FApi.t_last EcPhlAuto.t_auto (FApi.t_rotate `Right 1 tc)
Computing file changes ...