Add optional parameter to the split tactic to specify

on which conjunction the split should be done.

Co-authored-by: Pierre-Yves Strub <[email protected]>

Author: lyonel2017

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"

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

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

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 =

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

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
@@ -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
 

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

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 }