From 096ff0d77fb7e4332c16011c460e788599e8a2f4 Mon Sep 17 00:00:00 2001 From: Lionel Blatter Date: Wed, 20 Nov 2024 18:49:42 +0100 Subject: [PATCH] Add optional parameter to the split tactic to specify on which conjunction the split should be done. Co-authored-by: Pierre-Yves Strub --- src/ecCoreLib.ml | 2 + src/ecCoreLib.mli | 2 + src/ecFol.ml | 4 +- src/ecHiGoal.ml | 13 +++-- src/ecHiGoal.mli | 2 +- src/ecHiTacticals.ml | 2 +- src/ecLowGoal.ml | 94 +++++++++++++++++++++++++++++++++---- src/ecLowGoal.mli | 2 +- src/ecMatching.ml | 7 ++- src/ecParser.mly | 4 +- src/ecParsetree.ml | 2 +- src/ecProofTerm.ml | 17 ++++--- src/ecProofTerm.mli | 2 + tests/split.ec | 11 +++++ theories/prelude/Tactics.ec | 2 + 15 files changed, 135 insertions(+), 31 deletions(-) create mode 100644 tests/split.ec diff --git a/src/ecCoreLib.ml b/src/ecCoreLib.ml index 18dd82e1f2..365213fe54 100644 --- a/src/ecCoreLib.ml +++ b/src/ecCoreLib.ml @@ -241,6 +241,7 @@ module CI_Logic = struct let p_and_proj_r = _Logic "andWr" let p_anda_proj_l = _Logic "andaWl" let p_anda_proj_r = _Logic "andaWr" + let p_anda_proj_rs = _Logic "andaWrs" let p_or_elim = _Logic "orW" let p_ora_elim = _Logic "oraW" let p_iff_elim = _Logic "iffW" @@ -249,6 +250,7 @@ module CI_Logic = struct let p_true_intro = _Logic "trueI" let p_and_intro = _Logic "andI" let p_anda_intro = _Logic "andaI" + let p_anda_intro_s = _Logic "andaIs" let p_or_intro_l = _Logic "orIl" let p_ora_intro_l = _Logic "oraIl" let p_or_intro_r = _Logic "orIr" diff --git a/src/ecCoreLib.mli b/src/ecCoreLib.mli index aa04529e21..49ff1a9405 100644 --- a/src/ecCoreLib.mli +++ b/src/ecCoreLib.mli @@ -213,6 +213,7 @@ module CI_Logic : sig val p_and_proj_r : path val p_anda_proj_l : path val p_anda_proj_r : path + val p_anda_proj_rs : path val p_or_elim : path val p_ora_elim : path val p_iff_elim : path @@ -221,6 +222,7 @@ module CI_Logic : sig val p_true_intro : path val p_and_intro : path val p_anda_intro : path + val p_anda_intro_s : path val p_or_intro_l : path val p_ora_intro_l : path val p_or_intro_r : path diff --git a/src/ecFol.ml b/src/ecFol.ml index e5d6eb2c2c..b1f839a6f1 100644 --- a/src/ecFol.ml +++ b/src/ecFol.ml @@ -1039,9 +1039,7 @@ let destr_ands ~deep = in fun f -> doit f - -(*---------------------------------------------*) - +(* -------------------------------------------------------------------- *) let rec one_sided mem fp = match fp.f_node with | Fint _ -> true diff --git a/src/ecHiGoal.ml b/src/ecHiGoal.ml index 52f091d732..5d2b68b088 100644 --- a/src/ecHiGoal.ml +++ b/src/ecHiGoal.ml @@ -2025,10 +2025,17 @@ let process_right (tc : tcenv1) = tc_error !!tc "cannot apply `right` on that goal" (* -------------------------------------------------------------------- *) -let process_split (tc : tcenv1) = - try t_ors [EcLowGoal.t_split; EcLowGoal.t_split_prind] tc +let process_split ?(i : int option) (tc : tcenv1) = + let tactics : FApi.backward list = + match i with + | None -> [EcLowGoal.t_split; EcLowGoal.t_split_prind] + | Some i -> [EcLowGoal.t_split ~i] in + + try t_ors tactics tc with InvalidGoalShape -> - tc_error !!tc "cannot apply `split` on that goal" + tc_error !!tc + "cannot apply `split/%a` on that goal" + (EcPrinting.pp_opt Format.pp_print_int) i (* -------------------------------------------------------------------- *) let process_elim (pe, qs) tc = diff --git a/src/ecHiGoal.mli b/src/ecHiGoal.mli index dbc3ff0fad..3b22249c3e 100644 --- a/src/ecHiGoal.mli +++ b/src/ecHiGoal.mli @@ -82,7 +82,7 @@ val process_cut : ?mode:cutmode -> engine -> ttenv -> cut_t -> backward val process_cutdef : ttenv -> cutdef_t -> backward val process_left : backward val process_right : backward -val process_split : backward +val process_split : ?i:int -> backward val process_elim : prevert * pqsymbol option -> backward val process_case : ?doeq:bool -> prevertv -> backward val process_exists : ppt_arg located list -> backward diff --git a/src/ecHiTacticals.ml b/src/ecHiTacticals.ml index e662709d22..1973bef557 100644 --- a/src/ecHiTacticals.ml +++ b/src/ecHiTacticals.ml @@ -129,7 +129,7 @@ and process1_logic (ttenv : ttenv) (t : logtactic located) (tc : tcenv1) = | Preflexivity -> process_reflexivity | Passumption -> process_assumption | Psmt pi -> process_smt ~loc:(loc t) ttenv (Some pi) - | Psplit -> process_split + | Psplit i -> process_split ?i | Pfield st -> process_algebra `Solve `Field st | Pring st -> process_algebra `Solve `Ring st | Palg_norm -> EcStrongRing.t_alg_eq diff --git a/src/ecLowGoal.ml b/src/ecLowGoal.ml index 003bf07a9a..273d5a4130 100644 --- a/src/ecLowGoal.ml +++ b/src/ecLowGoal.ml @@ -638,7 +638,7 @@ type cutsolver = { smt : FApi.backward; done_ : FApi.backward; } - + (* -------------------------------------------------------------------- *) let tt_apply ?(cutsolver : cutsolver option) (pt : proofterm) (tc : tcenv) = let (hyps, concl) = FApi.tc_flat tc in @@ -1509,16 +1509,91 @@ let t_elim_iso_or ?reduce tc = let tc = t_elim_prind_r ?reduce ~accept `Case tc in (oget !outgoals, tc) + +(* -------------------------------------------------------------------- *) +let t_split_and_i i b f1 f2 tc = + let i = i - 1 in + let rec destr acc_sym acc_f i f = + if i < 0 then + acc_sym, acc_f, f + else + match sform_of_form f with + | SFand (b, (f1, f2)) -> + destr (b :: acc_sym) (f1 :: acc_f) (i - 1) f2 + | _ -> tc_error !!tc ~catchable:true "not enought conjunctions" in + + let l_sym , l_fsl, fsr = destr [b] [f1] i f2 in + + let sym = List.hd l_sym in + let syms = List.tl l_sym in + let fsl = List.hd l_fsl in + let fsls = List.tl l_fsl in + + let fsl = + List.fold_left2(fun acc sym f -> + match sym with + | `Asym -> f_anda f acc + | `Sym -> f_and f acc + ) fsl syms fsls in + + let tc = FApi.tcenv_of_tcenv1 tc in + let tc, gl = FApi.newgoal tc fsl in + + let tc, gr = + match sym with + | `Asym -> + let fsr = f_imp fsl fsr in + let tc, gr = FApi.newgoal tc fsr in + tc,`App (`HD gr, [`Sub (`HD gl:>prept)]) + | `Sym -> + let tc, gr = FApi.newgoal tc fsr in + tc,(`HD gr:>prept) in + + let pelim (sym : [`Sym | `Asym]) (side : [`L | `R]) = + match sym, side with + | `Sym , `L -> LG.p_and_proj_l + | `Sym , `R -> LG.p_and_proj_r + | `Asym, `L -> LG.p_anda_proj_l + | `Asym, `R -> LG.p_anda_proj_rs in + + let pte = ptenv_of_penv (FApi.tc_hyps tc) !$tc in + + let proj, projs = + List.fold_left_map (fun h sym -> + let j : prept = `App (`G (pelim sym `L, []), [`H_; `H_; `Sub h]) in + let h : prept = `App (`G (pelim sym `R, []), [`H_; `H_; `Sub h]) in + let j = pt_of_prept_r pte j in + let h = pt_of_prept_r pte h in + (`PE h, (sym, `PE j)) + ) (`HD gl :> prept) (List.rev syms) in + + let projs = projs @ [sym, proj] in + + let pintro (sym : [`Sym | `Asym]) = + match sym with + | `Sym -> LG.p_and_intro + | `Asym -> LG.p_anda_intro_s in + + let pt = + List.fold_right + (fun (sym, ptproj) pt -> + `App (`G (pintro sym, []), [`H_; `H_; `Sub ptproj; `Sub pt])) + projs gr in + + let pt = pt_of_prept_r pte pt in + + FApi.t_first (Apply.t_apply_bwd_r pt) tc + (* -------------------------------------------------------------------- *) -let t_split ?(closeonly = false) ?reduce (tc : tcenv1) = +let t_split ?(i = 0) ?(closeonly = false) ?reduce (tc : tcenv1) = let t_split_r (fp : form) (tc : tcenv1) = let concl = FApi.tc1_goal tc in match sform_of_form fp with | SFtrue -> t_true tc - | SFand (b, (f1, f2)) when not closeonly -> - t_and_intro_s b (f1, f2) tc + | SFand (b, (f1,f2)) when not closeonly -> + t_split_and_i i b f1 f2 tc | SFiff (f1, f2) when not closeonly -> t_iff_intro_s (f1, f2) tc | SFeq (f1, f2) when not closeonly && (is_tuple f1 && is_tuple f2) -> @@ -2182,13 +2257,14 @@ let t_progress ?options ?ti (tt : FApi.backward) (tc : tcenv1) = end | _ when options.pgo_split -> - let thesplit = + let (thesplit:tcenv1 -> tcenv) = match options.pgo_delta.pgod_split with - | true -> t_split ~closeonly:false ~reduce:`Full + | true -> (fun x -> t_split ~closeonly:false ~reduce:`Full x) | false -> - FApi.t_or - (t_split ~reduce:`NoDelta) - (t_split ~closeonly:true ~reduce:`Full) in + FApi.t_or + (t_split ~reduce:`NoDelta) + (t_split ~closeonly:true ~reduce:`Full) + in FApi.t_try (FApi.t_seq thesplit aux0) tc diff --git a/src/ecLowGoal.mli b/src/ecLowGoal.mli index 093f144240..30148db5c0 100644 --- a/src/ecLowGoal.mli +++ b/src/ecLowGoal.mli @@ -160,7 +160,7 @@ val t_right : ?reduce:lazyred -> FApi.backward val t_or_intro_prind : ?reduce:lazyred -> side -> FApi.backward (* -------------------------------------------------------------------- *) -val t_split : ?closeonly:bool -> ?reduce:lazyred -> FApi.backward +val t_split : ?i: int -> ?closeonly:bool -> ?reduce:lazyred -> FApi.backward val t_split_prind : ?reduce:lazyred -> FApi.backward (* -------------------------------------------------------------------- *) diff --git a/src/ecMatching.ml b/src/ecMatching.ml index fd7f256330..a2f5fce026 100644 --- a/src/ecMatching.ml +++ b/src/ecMatching.ml @@ -501,8 +501,7 @@ let f_match_core opts hyps (ue, ev) f1 f2 = let var_form_match ((x, xty) : ident * ty) (f : form) = match EV.get x !ev.evm_form with - | None -> - failure () + | None -> assert false | Some `Unset -> let f = norm f in @@ -583,10 +582,10 @@ let f_match_core opts hyps (ue, ev) f1 f2 = with EcUnify.UnificationFailure _ -> failure () end - | Flocal x, _ -> + | Flocal x, _ when EV.mem x !ev.evm_form -> var_form_match (x, f1.f_ty) f2 - | _, Flocal y -> + | _, Flocal y when EV.mem y !ev.evm_form -> var_form_match (y, f2.f_ty) f1 | Fapp (f1, fs1), Fapp (f2, fs2) -> diff --git a/src/ecParser.mly b/src/ecParser.mly index c7d89e783c..e07035a281 100644 --- a/src/ecParser.mly +++ b/src/ecParser.mly @@ -2656,8 +2656,8 @@ logtactic: | SMT LPAREN dbmap=dbmap1* RPAREN { Psmt (SMT.mk_smt_option [`WANTEDLEMMAS dbmap]) } -| SPLIT - { Psplit } +| SPLIT i=word? + { Psplit i } | FIELD eqs=ident* { Pfield eqs } diff --git a/src/ecParsetree.ml b/src/ecParsetree.ml index 13f8f8e604..3fd5c16f93 100644 --- a/src/ecParsetree.ml +++ b/src/ecParsetree.ml @@ -939,7 +939,7 @@ type logtactic = | Preflexivity | Passumption | Psmt of pprover_infos - | Psplit + | Psplit of int option | Pfield of psymbol list | Pring of psymbol list | Palg_norm diff --git a/src/ecProofTerm.ml b/src/ecProofTerm.ml index b17fe4649b..7f3c3d0e16 100644 --- a/src/ecProofTerm.ml +++ b/src/ecProofTerm.ml @@ -746,7 +746,6 @@ and apply_pterm_to_oarg ?loc ({ ptev_env = pe; ptev_pt = rawpt; } as pt) oarg = let oarg = oarg |> omap (fun arg -> arg.ptea_arg) in - match PT.destruct_product pe.pte_hy (get_head_symbol pe pt.ptev_ax) with | None -> tc_pterm_apperror ?loc pe AE_NotFunctional | Some t -> @@ -757,6 +756,7 @@ and apply_pterm_to_oarg ?loc ({ ptev_env = pe; ptev_pt = rawpt; } as pt) oarg = | PVASub arg -> begin try pf_form_match ~mode:EcMatching.fmdelta pe ~ptn:f1 arg.ptev_ax; + (f2, PASub (Some arg.ptev_pt)) with EcMatching.MatchFailure -> tc_pterm_apperror ?loc pe (AE_InvalidArgProof (arg.ptev_ax, f1)) @@ -911,6 +911,7 @@ type prept = [ | `G of EcPath.path * ty list | `UG of EcPath.path | `HD of handle + | `PE of pt_ev | `App of prept * prept_arg list ] @@ -923,14 +924,13 @@ and prept_arg = [ ] (* -------------------------------------------------------------------- *) -let pt_of_prept tc (pt : prept) = - let ptenv = ptenv_of_penv (FApi.tc1_hyps tc) !!tc in - - let rec build_pt = function +let pt_of_prept_r (ptenv : pt_env) : prept -> pt_ev = + let rec build_pt : prept -> pt_ev = function | `Hy id -> pt_of_hyp_r ptenv id | `G (p, tys) -> pt_of_global_r ptenv p tys | `UG p -> pt_of_global_r ptenv p [] | `HD hd -> pt_of_handle_r ptenv hd + | `PE pe -> pe | `App (pt, args) -> List.fold_left app_pt_ev (build_pt pt) args and app_pt_ev pt_ev = function @@ -940,7 +940,12 @@ let pt_of_prept tc (pt : prept) = | `Sub pt -> apply_pterm_to_arg_r pt_ev (PVASub (build_pt pt)) | `H_ -> apply_pterm_to_hole pt_ev - in build_pt pt + in fun pt -> build_pt pt + +(* -------------------------------------------------------------------- *) +let pt_of_prept (tc : tcenv1) (pt : prept) : pt_ev = + let ptenv = ptenv_of_penv (FApi.tc1_hyps tc) !!tc in + pt_of_prept_r ptenv pt (* -------------------------------------------------------------------- *) module Prept = struct diff --git a/src/ecProofTerm.mli b/src/ecProofTerm.mli index 55ec0f6c84..8f54208794 100644 --- a/src/ecProofTerm.mli +++ b/src/ecProofTerm.mli @@ -166,6 +166,7 @@ type prept = [ | `G of EcPath.path * ty list | `UG of EcPath.path | `HD of handle + | `PE of pt_ev | `App of prept * prept_arg list ] @@ -177,6 +178,7 @@ and prept_arg = [ | `H_ ] +val pt_of_prept_r: pt_env -> prept -> pt_ev val pt_of_prept: tcenv1 -> prept -> pt_ev (* -------------------------------------------------------------------- *) diff --git a/tests/split.ec b/tests/split.ec new file mode 100644 index 0000000000..8cd2b9a24b --- /dev/null +++ b/tests/split.ec @@ -0,0 +1,11 @@ +(* -------------------------------------------------------------------- *) +require import AllCore. + +lemma test : forall a b c d e f, + a && b /\ c && d => + e /\ f => + a && b /\ c && d /\ e /\ f. +proof. +move=> *. +split 3; assumption. +qed. diff --git a/theories/prelude/Tactics.ec b/theories/prelude/Tactics.ec index ec21321872..f3c05851fa 100644 --- a/theories/prelude/Tactics.ec +++ b/theories/prelude/Tactics.ec @@ -28,8 +28,10 @@ lemma andaW a b c : (a => b => c) => (a && b) => c by smt(). lemma andaWl a b : (a && b) => a by smt(). lemma andaWr a b : (a && b) => (a => b) by smt(). +lemma andaWrs a b : (a && b) => b by smt(). lemma andaI a b : a => (a => b) => (a && b) by smt(). +lemma andaIs a b : a => b => (a && b) by smt(). (* -------------------------------------------------------------------- *) lemma oraW a b c : (a => c) => (!a => b => c) => (a || b) => c by smt().