Tactic: simplify if

The simplify if transformation performs an if-conversion on program statements, i.e., it rewrites if statements into conditional expressions. This transformation preserves the program semantics.

This conversion helps prevent the weakest precondition from growing exponentially with the number of if statements.

To illustrate this issue, consider the following example, which shows how the weakest precondition can grow exponentially:

Since the tactic preserves semantics, it can be applied to all program logics.

Syntax

simplify if side? codepos?

The side argument is required when the goal is an equiv judgment; it specifies on which side the transformation should be applied. The codepos argument allows you to indicate which if statement the transformation should target.

Variant: Transform at a given code position

The tactic applies only if the branches of the selected if statement consist solely of assignments.

Variant: Transform as much as possible

Syntax

simplify if

This variant attempts to find a position where the transformation can be applied and applies it. The process is repeated until no applicable position remains.