Replaced |- ( [ x / y ] with |- ( [ y / x ] in set.mm, iset.mm and nf.mm

[GinoGiotto]

Towards #777. I replaced all occurrences of |- ( [ x / y ] with |- ( [ y / x ] in all databases that have them.

The only question I have is whether Norman Megill intended more generally to replace all occurrences of [ x / y ] or only the occurrences of |- ( [ x / y ]. Based on the search function he used #775 (comment), it appears to be the latter.

In case he meant the first interpretation then I will continue with other PRs, in case he meant the second interpretation then this PR should suffice for closing #777.

[tirix]

Ok. It's also more natural to me to think about substituting x with y, rather than the converse.

(Of course this does not change the definition)

[avekens]

Why does this proof become so much longer?

[GinoGiotto]

Because I made the cosmetic choice of keeping x = y in the hypothesis instead of switching into y = x. Do you prefer to have y = x, but with the original proof length? (For me it's fine both ways).

Some useful data might be that currently x = y appears 486 times in iset.mm, while y = x appears only 19 times (and most of those 19 times are there to show commutation properties).

[avekens]

@GinoGiotto thank you for the explanation. We should not switch the antecedent in the hypothesis (x = y should be the preferred way), so we can keep the longer proof.

[benjub]

I don't really have an opinion about these renamings, as long as they are only renamings.
When we write x = y -> ( ph <-> ps ), this generally goes with DV(x,ps) and/or DV(y,ph), so if you swap x and y, do it consistently. (I haven't checked the present case.)

[GinoGiotto]

When we write x = y -> ( ph <-> ps ), this generally goes with DV(x,ps) and/or DV(y,ph).

I didn't know that x is coupled with ps and y is coupled with ph. I'll try to fix this in a next PR.

[avekens]

I do not know what @benjub wants to say with his comment, and I don't see any need for a fix/change: DV(x,ps) means that x does not occur in ps, but of course y can (and usually should) occur in ps, analogously with ph. So we (usually) have ps(y) and ph(x). If the theorem is valid without DV conditions, they should not be added.

[benjub]

Of course, DV conditions should not be added if they are not necessary. What I mean is that when they are needed, it is usual to write that kind of hypotheses as x = y -> (ph(x) <-> ps(y)) (or sometimes x = y -> (ph(x,y) <-> ps(y)) or x = y -> (ph(x) <-> ps(x,y))), where I made explicit the variables that may occur instead of the variables that do not.

[jkingdon]

As Norm said in the linked issue, "[ y / x ] is almost always used except in a few places, and someday we should make them consistent" so this is a good idea.

[benjub]

This MR was not a mere renaming. In the case I checked (sbralie, from the above thread), there was more than a renaming, this is actually a different theorem, and the implicit substitution hypothesis is now written in an unusual way.

I think this should be fixed.

I haven't checked other cases.

[GinoGiotto]

This MR was not a mere renaming. In the case I checked (sbralie, from the above thread), there was more than a renaming, this is actually a different theorem, and the implicit substitution hypothesis is now written in an unusual way.

Sbralie is actually the only statement for which I didn't make a trivial adjustment, because of the choice of keeping x = y. So unless the coupling issue mentioned before isn't the only problem, the only theorem to fix is sbralie.

[benjub]

This MR was not a mere renaming. In the case I checked (sbralie, from the above thread), there was more than a renaming, this is actually a different theorem, and the implicit substitution hypothesis is now written in an unusual way.

Sbralie is actually the only statement for which I didn't make a trivial adjustment, because of the choice of keeping x = y. So unless the coupling issue mentioned before isn't the only problem, the only theorem to fix is sbralie.

Thanks for the checking.