|
| 1 | +======================================================================== |
| 2 | +Tactic: `hoare split` |
| 3 | +======================================================================== |
| 4 | + |
| 5 | +The `hoare split` tactic applies to **Hoare-logic goals only** whose |
| 6 | +postcondition is a conjunction. |
| 7 | + |
| 8 | +In this situation, the program is required to establish *both* components of |
| 9 | +the postcondition. The `hoare split` tactic makes this explicit by splitting |
| 10 | +the original goal into independent Hoare goals, one for each conjunct. |
| 11 | + |
| 12 | +Applying `hoare split` does not modify the program or the precondition. It |
| 13 | +only decomposes the logical structure of the postcondition. |
| 14 | + |
| 15 | +.. note:: |
| 16 | + |
| 17 | + The `hoare split` tactic is new and subject to change. Its interface and |
| 18 | + behavior may evolve in future versions of EasyCrypt. |
| 19 | + |
| 20 | + Currently, it only splits the top-most conjunction into two conjuncts. |
| 21 | + If you have nested conjunctions in the postcondition, you can |
| 22 | + apply `hoare split` multiple times to fully decompose the postcondition. |
| 23 | + |
| 24 | +.. contents:: |
| 25 | + :local: |
| 26 | + |
| 27 | +------------------------------------------------------------------------ |
| 28 | +Syntax |
| 29 | +------------------------------------------------------------------------ |
| 30 | + |
| 31 | +.. admonition:: Syntax |
| 32 | + |
| 33 | + `hoare split` |
| 34 | + |
| 35 | +This tactic takes no arguments. It can be applied whenever the conclusion |
| 36 | +of a Hoare goal is a conjunction. |
| 37 | + |
| 38 | +------------------------------------------------------------------------ |
| 39 | +Example |
| 40 | +------------------------------------------------------------------------ |
| 41 | + |
| 42 | +.. ecproof:: |
| 43 | + :title: Splitting a conjunctive postcondition |
| 44 | + |
| 45 | + require import AllCore. |
| 46 | + |
| 47 | + module M = { |
| 48 | + proc incr(x : int) : int = { |
| 49 | + var y : int; |
| 50 | + y <- x + 1; |
| 51 | + return y; |
| 52 | + } |
| 53 | + }. |
| 54 | + |
| 55 | + lemma L (n : int) : 0 <= n => |
| 56 | + hoare [M.incr : x = n ==> n < res /\ 0 <= res]. |
| 57 | + proof. |
| 58 | + move=> ge0_n; proc. |
| 59 | + |
| 60 | + (*$*) (* Split the conjunctive postcondition *) |
| 61 | + hoare split. |
| 62 | +
|
| 63 | + - (* First conjunct: n < y *) |
| 64 | + wp; skip; smt(). |
| 65 | +
|
| 66 | + - (* Second conjunct: 0 <= y *) |
| 67 | + wp; skip; smt(). |
| 68 | + qed. |
| 69 | +
|
| 70 | +------------------------------------------------------------------------ |
| 71 | +Note |
| 72 | +------------------------------------------------------------------------ |
| 73 | + |
| 74 | +This tactic is specific to Hoare logic. An analogous transformation would be |
| 75 | +unsound in other program logics supported by EasyCrypt (such as probabilistic |
| 76 | +or relational program logics), where a conjunctive postcondition does not, in |
| 77 | +general, decompose into independent proof obligations. |
![github-actions[bot]](https://avatars.githubusercontent.com/in/15368?v=4&size=40){kind=avatar}
0 commit comments