Unify should automatically implement replacements on work variables

[david-a-wheeler]

The mmj2 tool enables someone to edit a single work variable into an expression, then press "unify" and automatically do a replacement of the work variables. So anyone who has used mmj2 will expect the same thing to work in metamath-lamp, even though it doesn't. Metamath-lamp does support replacement, but not in the same way.

It'd be very helpful if "unify" noted that work variables had been substituted with a specific expression, and then automatically apply applied that replacement everywhere if it had already occurred.

[david-a-wheeler]

I think that in typical cases a work variable will only be replaced when it's already known what the justification & input labels are. That information could be used to instantly determine what the work variable value must become, and then quickly do a substitution across all statements if there's been such a replacement. It could even be a specialized implementation of unification, in the case where you know the specific justification & input labels.

[david-a-wheeler]

I think this is related to #77. In particular, I suspect implementing a full (syntactic) unification algorithm as described there would also resolve this issue.

[expln]

I think that in typical cases a work variable will only be replaced when it's already known what the justification & input labels are. That information could be used to instantly determine what the work variable value must become, and then quickly do a substitution across all statements if there's been such a replacement.

This is very similar to what I meant by "I already have one idea what I can do" in this comment #77 (comment) Thanks for confirming that this is a typical case.

[david-a-wheeler]

Sure! In the long term I think implementing "full unification" (at least as an option) is the best long-term move, as it's a more powerful algorithm & is what users of other tools are expecting. But I appreciate that implementing a subtle core algorithm takes time. The tool is already useful now; added power like that will just make it even more useful :-).