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

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 }

src/ecParsetree.ml

@@ -939,7 +939,7 @@ type logtactic =
   | Preflexivity
   | Passumption
   | Psmt        of pprover_infos
-  | Psplit
+  | Psplit      of int option
   | Pfield      of psymbol list
   | Pring       of psymbol list
   | Palg_norm

src/ecProofTerm.ml

@@ -746,7 +746,6 @@ and apply_pterm_to_oarg ?loc ({ ptev_env = pe; ptev_pt = rawpt; } as pt) oarg =
 
   let oarg = oarg |> omap (fun arg -> arg.ptea_arg) in
 
-
   match PT.destruct_product pe.pte_hy (get_head_symbol pe pt.ptev_ax) with
   | None   -> tc_pterm_apperror ?loc pe AE_NotFunctional
   | Some t ->
@@ -757,6 +756,7 @@ and apply_pterm_to_oarg ?loc ({ ptev_env = pe; ptev_pt = rawpt; } as pt) oarg =
             | PVASub arg -> begin
               try
                 pf_form_match ~mode:EcMatching.fmdelta pe ~ptn:f1 arg.ptev_ax;
+
                 (f2, PASub (Some arg.ptev_pt))
               with EcMatching.MatchFailure ->
                 tc_pterm_apperror ?loc pe (AE_InvalidArgProof (arg.ptev_ax, f1))
@@ -911,6 +911,7 @@ type prept = [
   | `G    of EcPath.path * ty list
   | `UG   of EcPath.path
   | `HD   of handle
+  | `PE   of pt_ev
   | `App  of prept * prept_arg list
 ]
 
@@ -923,14 +924,13 @@ and prept_arg =  [
 ]
 
 (* -------------------------------------------------------------------- *)
-let pt_of_prept tc (pt : prept) =
-  let ptenv = ptenv_of_penv (FApi.tc1_hyps tc) !!tc in
-
-  let rec build_pt = function
+let pt_of_prept_r (ptenv : pt_env) : prept -> pt_ev =
+  let rec build_pt : prept -> pt_ev = function
     | `Hy  id         -> pt_of_hyp_r ptenv id
     | `G   (p, tys)   -> pt_of_global_r ptenv p tys
     | `UG  p          -> pt_of_global_r ptenv p []
     | `HD  hd         -> pt_of_handle_r ptenv hd
+    | `PE  pe         -> pe
     | `App (pt, args) -> List.fold_left app_pt_ev (build_pt pt) args
 
   and app_pt_ev pt_ev = function
@@ -940,7 +940,12 @@ let pt_of_prept tc (pt : prept) =
     | `Sub pt -> apply_pterm_to_arg_r pt_ev (PVASub (build_pt pt))
     | `H_     -> apply_pterm_to_hole pt_ev
 
-  in build_pt pt
+  in fun pt -> build_pt pt
+
+(* -------------------------------------------------------------------- *)
+let pt_of_prept (tc : tcenv1) (pt : prept) : pt_ev =
+  let ptenv = ptenv_of_penv (FApi.tc1_hyps tc) !!tc in
+  pt_of_prept_r ptenv pt
 
 (* -------------------------------------------------------------------- *)
 module Prept = struct

src/ecProofTerm.mli

@@ -166,6 +166,7 @@ type prept = [
   | `G    of EcPath.path * ty list
   | `UG   of EcPath.path
   | `HD   of handle
+  | `PE   of pt_ev
   | `App  of prept * prept_arg list
 ]
 
@@ -177,6 +178,7 @@ and prept_arg =  [
   | `H_
 ]
 
+val pt_of_prept_r: pt_env -> prept -> pt_ev
 val pt_of_prept: tcenv1 -> prept -> pt_ev
 
 (* -------------------------------------------------------------------- *)

tests/split.ec

@@ -0,0 +1,11 @@
+(* -------------------------------------------------------------------- *)
+require import AllCore.
+
+lemma test : forall a b c d e f,
+    a && b /\ c && d  =>
+    e /\ f =>
+    a && b /\ c && d /\ e /\ f.
+proof.
+move=> *.
+split 3; assumption.
+qed.

theories/prelude/Tactics.ec

@@ -28,8 +28,10 @@ lemma andaW a b c : (a => b => c) => (a && b) => c by smt().
 
 lemma andaWl a b : (a && b) => a by smt().
 lemma andaWr a b : (a && b) => (a => b) by smt().
+lemma andaWrs a b : (a && b) => b by smt().
 
 lemma andaI a b : a => (a => b) => (a && b) by smt().
+lemma andaIs a b : a => b => (a && b) by smt().
 
 (* -------------------------------------------------------------------- *)
 lemma oraW a b c : (a => c) => (!a => b => c) => (a || b) => c by smt().