Add option to specify the conjuction to split

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 =

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

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

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,16 +1510,35 @@ 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
 
     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
+      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
 

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

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 }

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