From 77c9f79cad945ea2348d8505b2956f49f3c38557 Mon Sep 17 00:00:00 2001 From: Pierre-Yves Strub Date: Mon, 25 May 2026 15:46:16 +0200 Subject: [PATCH] split: add `split *` and `split +` to iterate over top-level conjunctions `split *` peels every top-level /\ and && until the head is no longer a conjunction; it is a no-op when the goal is not a conjunction. `split +` is the same but errors if the outermost goal is not a conjunction. No unfolding; only the SFand head is matched. For asymmetric && (`a && X`), the right side may depend on `a`, so the recursion intros `a` as a hypothesis, peels X, then re-generalizes the hypothesis over every leaf produced. This mirrors how plain `split` handles a single &&, and keeps the semantics sound when /\ or && is nested under &&. E.g. `a && (b /\ c)` yields three subgoals `a`, `a => b`, `a => c`. --- src/ecHiGoal.ml | 4 +++ src/ecHiGoal.mli | 1 + src/ecHiTacticals.ml | 4 ++- src/ecLowGoal.ml | 26 ++++++++++++++ src/ecLowGoal.mli | 1 + src/ecParser.mly | 8 ++++- src/ecParsetree.ml | 2 +- tests/split-star.ec | 84 ++++++++++++++++++++++++++++++++++++++++++++ 8 files changed, 127 insertions(+), 3 deletions(-) create mode 100644 tests/split-star.ec diff --git a/src/ecHiGoal.ml b/src/ecHiGoal.ml index 93389a275..c58de527f 100644 --- a/src/ecHiGoal.ml +++ b/src/ecHiGoal.ml @@ -2172,6 +2172,10 @@ let process_split ?(i : int option) (tc : tcenv1) = "cannot apply `split/%a` on that goal" (EcPrinting.pp_opt Format.pp_print_int) i +(* -------------------------------------------------------------------- *) +let process_split_all ~(must : bool) (tc : tcenv1) = + EcLowGoal.t_split_all ~must tc + (* -------------------------------------------------------------------- *) let process_elim (pe, qs) tc = let doelim tc = diff --git a/src/ecHiGoal.mli b/src/ecHiGoal.mli index 81cf7a6b9..78f61f3b0 100644 --- a/src/ecHiGoal.mli +++ b/src/ecHiGoal.mli @@ -88,6 +88,7 @@ val process_cutdef : ttenv -> cutdef_t -> backward val process_left : backward val process_right : backward val process_split : ?i:int -> backward +val process_split_all : must:bool -> 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 2a9747533..8a6576983 100644 --- a/src/ecHiTacticals.ml +++ b/src/ecHiTacticals.ml @@ -130,7 +130,9 @@ 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 i -> process_split ?i + | Psplit (`Default i) -> process_split ?i + | Psplit (`All `Maybe)-> process_split_all ~must:false + | Psplit (`All `One) -> process_split_all ~must:true | 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 ae5a28eb0..4a73fc517 100644 --- a/src/ecLowGoal.ml +++ b/src/ecLowGoal.ml @@ -1648,6 +1648,32 @@ let t_split ?(i = 0) ?(closeonly = false) ?reduce (tc : tcenv1) = in t_lazy_match ?reduce t_split_r tc +(* -------------------------------------------------------------------- *) +let rec t_split_all ?(must = false) (tc : tcenv1) = + let concl = FApi.tc1_goal tc in + match sform_of_form concl with + | SFand (`Sym, (f1, f2)) -> + let tc = t_and_intro_s `Sym (f1, f2) tc in + FApi.t_onall (t_split_all ~must:false) tc + | SFand (`Asym, (f1, f2)) -> + let tc = t_and_intro_s `Asym (f1, f2) tc in + (* subgoal 0 = f1; subgoal 1 = f1 => f2. + On the second, intro the f1-hypothesis, recurse on f2, then + generalize-and-clear so each produced leaf becomes f1 => leaf. *) + FApi.t_onalli (fun i tc -> + if i = 0 then + t_split_all ~must:false tc + else + let h = LDecl.fresh_id (FApi.tc1_hyps tc) "h" in + let tc = t_intros_i_1 [h] tc in + let tc = t_split_all ~must:false tc in + FApi.t_onall (t_generalize_hyp ~clear:`Yes h) tc + ) tc + | _ when must -> + tc_error !!tc "split+: goal is not a top-level conjunction" + | _ -> + FApi.tcenv_of_tcenv1 tc + (* -------------------------------------------------------------------- *) let t_split_prind ?reduce (tc : tcenv1) = let t_split_r (fp : form) (tc : tcenv1) = diff --git a/src/ecLowGoal.mli b/src/ecLowGoal.mli index c17b4e4b2..2581c9bb0 100644 --- a/src/ecLowGoal.mli +++ b/src/ecLowGoal.mli @@ -163,6 +163,7 @@ val t_duplicate_top_assumtion : FApi.backward (* -------------------------------------------------------------------- *) val t_split : ?i: int -> ?closeonly:bool -> ?reduce:lazyred -> FApi.backward +val t_split_all : ?must:bool -> FApi.backward val t_split_prind : ?reduce:lazyred -> FApi.backward (* -------------------------------------------------------------------- *) diff --git a/src/ecParser.mly b/src/ecParser.mly index 8633c1312..117ccf9a1 100644 --- a/src/ecParser.mly +++ b/src/ecParser.mly @@ -2817,7 +2817,13 @@ logtactic: { Psmt (SMT.mk_smt_option [`WANTEDLEMMAS dbmap]) } | SPLIT i=word? - { Psplit i } + { Psplit (`Default i) } + +| SPLIT STAR + { Psplit (`All `Maybe) } + +| SPLIT PLUS + { Psplit (`All `One) } | FIELD eqs=ident* { Pfield eqs } diff --git a/src/ecParsetree.ml b/src/ecParsetree.ml index 9644cfde6..7d060227e 100644 --- a/src/ecParsetree.ml +++ b/src/ecParsetree.ml @@ -1044,7 +1044,7 @@ type logtactic = | Preflexivity | Passumption | Psmt of pprover_infos - | Psplit of int option + | Psplit of [ `Default of int option | `All of [ `Maybe | `One ] ] | Pfield of psymbol list | Pring of psymbol list | Palg_norm diff --git a/tests/split-star.ec b/tests/split-star.ec new file mode 100644 index 000000000..3af53dd8b --- /dev/null +++ b/tests/split-star.ec @@ -0,0 +1,84 @@ +(* -------------------------------------------------------------------- *) +require import AllCore. + +(* `split *` peels every top-level /\ and &&; the right side of && gets + the left as a hypothesis (matches plain `split` semantics). *) +lemma L1 (a b c d e : bool) : + a => b => c => d => e => + a /\ b /\ (c && d) /\ e. +proof. +move=> ha hb hc hd he. +split *. ++ exact: ha. ++ exact: hb. ++ exact: hc. ++ move=> _; exact: hd. ++ exact: he. +qed. + +(* `split +` requires at least one top-level conjunction *) +lemma L2 (a b c d e : bool) : + a => b => c => d => e => + a /\ b /\ (c && d) /\ e. +proof. +move=> ha hb hc hd he. +split +. ++ exact: ha. ++ exact: hb. ++ exact: hc. ++ move=> _; exact: hd. ++ exact: he. +qed. + +(* `split *` does NOT descend into other connectives *) +lemma L3 (p q r s : bool) : + (p => q) => (r \/ s) => + (p => q) /\ (r \/ s). +proof. +move=> hpq hrs. +split *. ++ exact: hpq. ++ exact: hrs. +qed. + +(* `split *` is a no-op on a non-conjunction goal *) +lemma L4 (p : bool) : p => p. +proof. +move=> hp. +split *. +exact: hp. +qed. + +(* `split +` fails on a non-conjunction goal *) +lemma L5 (p : bool) : p => p. +proof. +move=> hp. +fail split +. +exact: hp. +qed. + +(* recursing under && carries the left side as a hypothesis to every + subgoal produced from the right side. E.g. a && (b /\ c) becomes + a, a => b, a => c (not a, a => b /\ c). *) +lemma L6 (a b c : bool) : + a => (a => b) => (a => c) => + a && (b /\ c). +proof. +move=> ha hab hac. +split *. ++ exact: ha. ++ exact: hab. ++ exact: hac. +qed. + +(* deeper: a && (b && c) becomes a, a => b, a => (b => c) *) +lemma L7 (a b c : bool) : + a => (a => b) => (a => b => c) => + a && (b && c). +proof. +move=> ha hab habc. +split *. ++ exact: ha. ++ exact: hab. ++ exact: habc. +qed.