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 both 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.

Currently, it only splits the top-most conjunction into two conjuncts. If you have nested conjunctions in the postcondition, you can apply hoare split multiple times to fully decompose the postcondition.

Syntax

Syntax

hoare split

This tactic takes no arguments. It can be applied whenever the conclusion of a Hoare goal is a conjunction.

Example

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.