diff --git a/doc/tactics/hoare-split.rst b/doc/tactics/hoare-split.rst
new file mode 100644
index 000000000..7e75507ff
--- /dev/null
+++ b/doc/tactics/hoare-split.rst
@@ -0,0 +1,73 @@
+========================================================================
+Tactic: `hoare split`
+========================================================================
+
+The `hoare split` tactic applies to **Hoare-logic goals only** whose
+postcondition is a conjunction.
+
+In this situation, the program is required to establish *all* components of
+the postcondition. The `hoare split` tactic makes this explicit by splitting
+the original goal into independent Hoare goals, one for each conjunct.
+
+Applying `hoare split` does not modify the program or the precondition. It
+only decomposes the logical structure of the postcondition.
+
+.. note::
+
+   The `hoare split` tactic is new and subject to change. Its interface and
+   behavior may evolve in future versions of EasyCrypt.
+
+.. contents::
+   :local:
+
+------------------------------------------------------------------------
+Syntax
+------------------------------------------------------------------------
+
+.. admonition:: Syntax
+
+   `hoare split`
+
+This tactic takes no arguments. It can be applied whenever the conclusion
+of a Hoare goal is a conjunction.
+
+------------------------------------------------------------------------
+Example
+------------------------------------------------------------------------
+
+.. ecproof::
+   :title: Splitting a conjunctive postcondition
+
+   require import AllCore.
+
+   module M = {
+     proc incr(x : int) : int = {
+       var y : int;
+       y <- x + 1;
+       return y;
+     }
+   }.
+
+   lemma L (n : int) : 0 <= n =>
+     hoare [M.incr : x = n ==> n < res /\ 0 <= res].
+   proof.
+     move=> ge0_n; proc.
+
+     (*$*) (* Split the conjunctive postcondition *)
+     hoare split.
+
+     - (* First conjunct: n < y *)
+       wp; skip; smt().
+
+     - (* Second conjunct: 0 <= y *)
+       wp; skip; smt().
+   qed.
+
+------------------------------------------------------------------------
+Note
+------------------------------------------------------------------------
+
+This tactic is specific to Hoare logic. An analogous transformation would be
+unsound in other program logics supported by EasyCrypt (such as probabilistic
+or relational program logics), where a conjunctive postcondition does not, in
+general, decompose into independent proof obligations.
diff --git a/src/ecHiTacticals.ml b/src/ecHiTacticals.ml
index 88ce90195..8c4c4eae2 100644
--- a/src/ecHiTacticals.ml
+++ b/src/ecHiTacticals.ml
@@ -232,6 +232,7 @@ and process1_phl (_ : ttenv) (t : phltactic located) (tc : tcenv1) =
     | Pprocrewrite (s, p, f)    -> EcPhlRewrite.process_rewrite s p f
     | Pchangestmt (s, p, c)     -> EcPhlRewrite.process_change_stmt s p c
     | Prwprgm infos             -> EcPhlRwPrgm.process_rw_prgm infos
+    | Phoaresplit               -> EcPhlHoare.process_hoaresplit
   in
 
   try  tx tc
diff --git a/src/ecParser.mly b/src/ecParser.mly
index cda6b5afa..69b9d3c30 100644
--- a/src/ecParser.mly
+++ b/src/ecParser.mly
@@ -3163,6 +3163,9 @@ interleave_info:
 | PROC REWRITE side=side? pos=codepos SLASHEQ
     { Pprocrewrite (side, pos, `Simpl) }
 
+| HOARE SPLIT
+    { Phoaresplit }
+
 | IDASSIGN o=codepos x=lvalue_var
     { Prwprgm (`IdAssign (o, x)) }
 
diff --git a/src/ecParsetree.ml b/src/ecParsetree.ml
index 6b4f1e2b9..1d5e858f0 100644
--- a/src/ecParsetree.ml
+++ b/src/ecParsetree.ml
@@ -773,7 +773,7 @@ type phltactic =
   | Prwprgm of rwprgm
   | Pprocrewrite   of side option * pcodepos * prrewrite
   | Pchangestmt    of side option * pcodepos_range * pstmt
-
+  | Phoaresplit
 
     (* Eager *)
   | Peager_seq       of (pcodepos1 pair * pstmt * pformula doption)
diff --git a/src/phl/ecPhlConseq.mli b/src/phl/ecPhlConseq.mli
index 18c2c22e4..464135813 100644
--- a/src/phl/ecPhlConseq.mli
+++ b/src/phl/ecPhlConseq.mli
@@ -21,6 +21,8 @@ val t_ehoareS_conseq      : ss_inv -> ss_inv -> FApi.backward
 val t_bdHoareS_conseq_bd  : hoarecmp -> ss_inv -> FApi.backward
 val t_bdHoareF_conseq_bd  : hoarecmp -> ss_inv -> FApi.backward
 
+val t_hoareS_conseq_conj : ss_inv -> ss_inv -> ss_inv -> ss_inv -> FApi.backward
+
 (* -------------------------------------------------------------------- *)
 val t_equivF_conseq_nm    : ts_inv -> ts_inv -> FApi.backward
 val t_equivS_conseq_nm    : ts_inv -> ts_inv -> FApi.backward
diff --git a/src/phl/ecPhlHoare.ml b/src/phl/ecPhlHoare.ml
new file mode 100644
index 000000000..5f4ae03ed
--- /dev/null
+++ b/src/phl/ecPhlHoare.ml
@@ -0,0 +1,29 @@
+(* ------------------------------------------------------------------------ *)
+open EcAst
+open EcFol
+open EcLowPhlGoal
+open EcCoreGoal
+
+(* ------------------------------------------------------------------------ *)
+let t_hoaresplit (tc : tcenv1) =
+  let hoare = tc1_as_hoareS tc in
+  let pre   = hs_pr hoare in
+  let post  = hs_po hoare in
+
+  match sform_of_form post.inv with
+  | SFand (`Sym, (f1, f2)) ->
+    let dp = map_ss_inv2 f_and pre pre in
+    let cl = { post with inv = f1 } in
+    let cr = { post with inv = f2 } in
+
+    EcPhlConseq.t_hoareS_conseq dp (hs_po hoare) tc
+      |> FApi.t_firsts EcHiGoal.process_done 2
+      |> FApi.as_tcenv1
+      |> EcPhlConseq.t_hoareS_conseq_conj (hs_pr hoare) cr (hs_pr hoare) cl
+
+  | _ ->
+    tc_error !!tc "post-condition should be a conjunction"
+
+(* ------------------------------------------------------------------------ *)
+let process_hoaresplit (tc : tcenv1) =
+  t_hoaresplit tc
diff --git a/src/phl/ecPhlHoare.mli b/src/phl/ecPhlHoare.mli
new file mode 100644
index 000000000..90c995b4b
--- /dev/null
+++ b/src/phl/ecPhlHoare.mli
@@ -0,0 +1,6 @@
+(* ------------------------------------------------------------------------ *)
+open EcCoreGoal.FApi
+
+(* ------------------------------------------------------------------------ *)
+val t_hoaresplit : backward
+val process_hoaresplit : backward