search

expln / metamath-lamp

Metamath-lamp (Lite Assistant for Metamath Proofs) is a GUI-based proof assistant for creating formal mathematical proofs in Metamath that does not require installation (just run it directly using your web browser).
https://expln.github.io/lamp/latest/index.html
MIT License
13 stars 5 forks source link

Variables cannot unify with themselves #198

Open CatsAreFluffy opened 5 months ago

CatsAreFluffy commented 5 months ago

If I try to unify R with R (using unification and not matching), I get an error, even though they should trivially unify.

expln commented 5 months ago

Thanks for reporting this. I will take a look.

expln commented 3 days ago

Hi @CatsAreFluffy. I am sorry for the long delay in response. Looks like this is not a bug. The Unification mode works with meta variables only. Check the Prefix of metavariables in unification setting on the Settings tab.

image

That symbol defines meta variables. By default, it is &. For example, R is not a meta variable, but &R is a meta variable.

You can create a local variable &R and try to unify it with itself. You should see Found substitutions: 1 valid, 0 invalid.. However, you will not see &R -> &R. This is a bit confusing, but this is done intentionally.

image

The way how mm-lamp is implemented, is that it includes all variables present in the editor to the list of found substitutions. It could be a big number of variables. Usually, only a few variables get substituted with something else, and others are substituted with itself. Mm-lamp shows only "useful" substitutions, where a variable is substituted with something different from itself. For example:

image

Currently, this distinction between meta variables and usual variables is used in the Unification mode of the Find substitutions feature only. In all other places all variables are treated equally. This is done because of how the unification algorithm works. In some sense, the unification algorithm divides all symbols into two groups: symbols not to replace and placeholders. The algorithm will try to find substitutions for placeholders only. The issue here is that, firstly, symbols not to replace include not only Metamath constants but also Metamath variables. Secondly, placeholders include Metamath variables only, but not all of them. So, Metamath variables can be in both symbols not to replace and placeholders. Therefore, the Prefix of metavariables in unification setting was introduced, and only variables prefixed with this prefix will be considered as placeholders in the unification algorithm. There is another issue with some interesting discussions related to this topic https://github.com/expln/metamath-lamp/issues/77#issuecomment-1608487072

All of this might be too complicated. Even I didn't recognize this problem by its description. I had to dive into the code to find out that this is not a bug. Maybe it makes sense to add some hints to the Unification dialog. I will think on that.