Tactic: add hoare split

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.

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

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

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)

src/phl/ecPhlHoare.ml

@@ -0,0 +1,27 @@
+(* ------------------------------------------------------------------------ *)
+open EcAst
+open EcFol
+open EcLowPhlGoal
+open EcCoreGoal
+
+(* ------------------------------------------------------------------------ *)
+let t_hoaresplit (tc : tcenv1) =
+  let hoare = tc1_as_hoareS tc in
+  let post  = hs_po hoare in
+
+  match sform_of_form post.inv with
+  | SFand (_, (f1, f2)) ->
+    let cl = { post with inv = f1 } in
+    let cr = { post with inv = f2 } in
+
+    let gl = f_hoareS (snd hoare.hs_m) (hs_pr hoare) hoare.hs_s cl in
+    let gr = f_hoareS (snd hoare.hs_m) (hs_pr hoare) hoare.hs_s cr in
+
+    FApi.xmutate1 tc `HoareSplit [gl; gr]
+
+  | _ ->
+    tc_error !!tc "post-condition should be a conjunction"
+
+(* ------------------------------------------------------------------------ *)
+let process_hoaresplit (tc : tcenv1) =
+  t_hoaresplit tc

src/phl/ecPhlHoare.mli

@@ -0,0 +1,6 @@
+(* ------------------------------------------------------------------------ *)
+open EcCoreGoal.FApi
+
+(* ------------------------------------------------------------------------ *)
+val t_hoaresplit : backward
+val process_hoaresplit : backward