#342 Generalized Modus Ponens on Boolean expressions

[Laurent Voisin]

The Generalized Modus Ponens reasoner has been enhanced to detect similar predicates and treat them as identical. However, the case of Boolean expressions has been forgotten which makes some proofs unnecessarily complicated.

A typical case is the sequent

   f ∈ ℤ → BOOL
   f(1) = TRUE ⇒ f(2) = TRUE
   f(2) = FALSE
|- f(1) = FALSE

which should be discharged by the Generalized Modus Ponens, but is not because it mixes predicates with TRUE and FALSE which are not matched with each other.

See attached file for a Rodin project archive containing this example.

[Laurent Voisin]

Note: the CONTR_HYPS reasoner has the same issue.

[Laurent Voisin]

To be implemented at the same time as [#343].

[Guillaume Verdier]

This has been implemented in commit [12a736].