#371 Apply equality and hide it

[Guillaume Verdier]

When there is an hypothesis with an equality, two tactics are proposed when clicking on the = sign: “Apply equality from left to right” and “Equality from right to left”. These tactics replace one side of the equality with the other one in the goal and the other hypotheses. Then, the equality remains in the hypotheses, but it is typically not needed anymore.
It would be simpler if some tactics could apply the equality and then hide the hypothesis.

[Laurent Voisin]

Actually, it depends on the rewriting that is performed. For instance, if the used equality is x = y + 1, then rewriting all occurrence of x with y + 1, then removing the equality is OK. On the other have, if we rewrite y + 1 with x, then it would be a bad idea to remove the equality. There might still be some occurrences of y that have not been rewritten.

I would thus propose to create a new level of the reasoner that removes (hides) the equality only when the rewritten expression is a bare identifier, and behaves as current otherwise.

[Guillaume Verdier]

This feature request has been implemented and merged in commit [79a6c5].