From 2497e6d41f39fab57772f042aaa1fc070ab1c100 Mon Sep 17 00:00:00 2001 From: Lionel Blatter Date: Wed, 20 Nov 2024 18:49:42 +0100 Subject: [PATCH] Add option to specify the conjuction to split --- src/ecHiGoal.ml | 7 ++++--- src/ecHiGoal.mli | 2 +- src/ecHiTacticals.ml | 2 +- src/ecLowGoal.ml | 36 ++++++++++++++++++++++++++++-------- src/ecLowGoal.mli | 2 +- src/ecParser.mly | 4 ++-- src/ecParsetree.ml | 2 +- 7 files changed, 38 insertions(+), 17 deletions(-) diff --git a/src/ecHiGoal.ml b/src/ecHiGoal.ml index 6250d10068..6b5591f52c 100644 --- a/src/ecHiGoal.ml +++ b/src/ecHiGoal.ml @@ -1974,10 +1974,11 @@ 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 (tc : tcenv1) = + let i = Option.map (fun n -> int_of_string n.pl_desc) i in + try t_ors [EcLowGoal.t_split ?i; EcLowGoal.t_split_prind] tc with InvalidGoalShape -> - tc_error !!tc "cannot apply `split` on that goal" + tc_error !!tc "cannot apply `split` on(Option.map (fun n -> int_of_string n.pl_desc) i) that goal" (* -------------------------------------------------------------------- *) let process_elim (pe, qs) tc = diff --git a/src/ecHiGoal.mli b/src/ecHiGoal.mli index dbc3ff0fad..589d145187 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:psymbol -> 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 32f6ea2ed3..f6315cc1a2 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 70d352cf42..57dc1af2ed 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 @@ -1510,8 +1510,27 @@ let t_elim_iso_or ?reduce tc = let tc = t_elim_prind_r ?reduce ~accept `Case tc in (oget !outgoals, tc) + +let rec t_and_i i opsym (f1, f2 : form pair) (tc : tcenv1) = + if i <= 0 then + begin + let tc = + FApi.mutate1 tc (fun hd -> VConv (hd, Sid.empty)) + (EcFol.f_and f1 f2) + in + t_and_intro_s opsym (f1, f2) tc + end + else + begin + match sform_of_form f2 with + | SFand (b, (f1', f2')) -> + t_and_i (i - 1) b (EcFol.f_and f1 f1', f2') tc + | _ -> + t_and_intro_s opsym (f1, f2) tc + end + (* -------------------------------------------------------------------- *) -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 @@ -1519,7 +1538,7 @@ let t_split ?(closeonly = false) ?reduce (tc : tcenv1) = | SFtrue -> t_true tc | SFand (b, (f1, f2)) when not closeonly -> - t_and_intro_s b (f1, f2) tc + t_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) -> @@ -2183,13 +2202,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/ecParser.mly b/src/ecParser.mly index 55277b0885..b8f3f9670c 100644 --- a/src/ecParser.mly +++ b/src/ecParser.mly @@ -2785,8 +2785,8 @@ logtactic: | SMT LPAREN dbmap=dbmap1* RPAREN { Psmt (SMT.mk_smt_option [`WANTEDLEMMAS dbmap]) } -| SPLIT - { Psplit } +| SPLIT i=loc(STRING)? + { Psplit i} | FIELD eqs=ident* { Pfield eqs } diff --git a/src/ecParsetree.ml b/src/ecParsetree.ml index 593b1a2004..d434f14ec1 100644 --- a/src/ecParsetree.ml +++ b/src/ecParsetree.ml @@ -938,7 +938,7 @@ type logtactic = | Preflexivity | Passumption | Psmt of pprover_infos - | Psplit + | Psplit of psymbol option | Pfield of psymbol list | Pring of psymbol list | Palg_norm