I believe one reason why implicit substitution is often preferred to explicit substitution is that MMJ2 is able to automatically prove the former.
If you have a formula like: !10:: |- ( x = A -> ( ( x + 2 ) = ( B / x ) <-> ( A + 2 ) = ( B / A ) ) ) And choose “Unify” (CTRL-U), MMJ2 will normally fully resolve it. I don’t think it is the case for the “explicit substitution“. There’s probably a way to update MMJ2 (or its JS based rules) to do so, thought. BR, _ Thierry > Le 3 juin 2019 à 04:27, Benoit <[email protected]> a écrit : > >> On Sunday, June 2, 2019 at 7:16:01 PM UTC+2, Thierry Arnoux wrote: >> "x = A -> ( ph <-> ps )" >> would be the way to state with an implicit substitution the same thing as >> “[. A / x ]. ph <-> ps” >> states explicitly, that is >> “ps is the result of taking all instances of ‘x’ in ph, and substituting >> them with ‘A’.” > > For the record, this equivalence between implicit and explicit substitutions, > back and forth, is expressed by the two theorems > sbceq1a $p |- ( x = A -> ( ph <-> [. A / x ]. ph ) ) $= > and > $d x A $. $d x ps $. sbcie.1 $e |- A e. _V $. > sbcie.2 $e |- ( x = A -> ( ph <-> ps ) ) $. > sbcie $p |- ( [. A / x ]. ph <-> ps ) $= > > Benoit > > >> >> My experience is that implicit substitution is more easy to work with. >> _ >> Thierry >> >> > > -- > You received this message because you are subscribed to the Google Groups > "Metamath" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to [email protected]. > To view this discussion on the web visit > https://groups.google.com/d/msgid/metamath/d19c8ebd-2d9c-4924-b798-0b3c62ec6182%40googlegroups.com. -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/0C2C0D8C-DD00-4730-A7FD-7C729495C968%40gmx.net.
