#765 Generalized Modus Ponens turns goal into "false"

[Son Hoang]

In the attached development, and the partial proof of theorem "thm", in the last step, generalised MP rewrite the goal to "false", leads to unprovable sequent. This is unexpected behaviour from generalised MP. Before this generalised MP step, the sequent is always provable.

[Laurent Voisin]

The proof is done by contradiction. In the example, the user has selected one hypothesis for contradiction and brung it to the goal. The hypothesis then gets deselected, but it is not hidden.

Consequently, the genMP reasoner uses the hypothesis to rewrite the goal. This is the expected behavior of the reasoner.

The sequent after genMP reasoner is still provable: just simplify the hypothesis x+1 = 1, and the rest is discharged by the default auto-tactic.

I think that the correct fix would rather be to hide the hypothesis when contradicting it.

[Laurent Voisin]

In summary, my opinion is that in Rodin 3.3, we should change the ct tactic so that it hides the hypothesis which is moved to the goal (this cannot lead to a dead-end).

In the longer term (beyond Rodin 3.3), we should modify the genMP reasoner so that it would consider arithmetic simplification when building the list of variants of some predicate (in which case your example will get automatically discharged).

Son, do you agree with my analysis?

[Son Hoang]

Hi Laurent,
I did not notice that the hypothesis not(x = 0) is only deselected, but not hidden. When I mean that it leads to dead-end is that the sequent cannot be discharged by P0. In the real situation, I do want to work a bit more on the goal, and can only do that by pruning the generalised MP step.
I agree with you that we should hide the hypothesis when applying ct. Now with generalised MP ignoring the hidden hypotheses, it should fix this problem.
Cheers,
Son

[Laurent Voisin]

This bug has indeed been fixed in Rodin 3.3 [fe908c].
The proposed improvement of Generalized MP is the subject of ticket [feature-requests:#354].