split: add split * and split + to iterate over top-level conjunctions

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 =

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

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

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) =

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
 
 (* -------------------------------------------------------------------- *)

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 }

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

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.