feat(phl): add simplify if tactic

[bgregoir]

Summary

• Add a new simplify if tactic that performs if-conversion on program
  statements, rewriting if statements into conditional expressions.
• It is well known that wp on code containing sequences of if grows
  exponentially. By converting if statements into if expressions,
  the weakest precondition becomes linear in the size of the program.
• The tactic preserves program semantics and can be applied to all
  program logics (hoare, bdhoare, ehoare).

Changes

• ecPhlCodeTx: implement transform_if and recursive variant
• ecLowPhlGoal: extend t_code_transform to support eHoare
  judgments, removing the now-unnecessary bdhoare flag
• ecMatching: add MatchByPos branch selection variant to code
  positions
• ecParser/ecParsetree: wire up the simplify if syntax
• Add documentation (doc/tactics/simplify-if.rst) and worked
  examples (examples/tactics/simplify_if.ec)

Usage

(* Transform all if statements whose branches are pure assignments *)
simplify if.

(* Transform a specific if at a given code position *)
simplify if ^if.
simplify if ^if{2}.