> On Dec 27, 2021, at 9:08 PM, Brian Larson <[email protected]> wrote:
>
> I often want to use substitution to do something like this:
> |- ph & |- x = y |- ( [ y / x ] ph <-> ps ) ==> |- ps
> But I'm having trouble showing that ps results from the proper substitution
> of y for x in ph.
>
> Mario wrote some hints:
>
> In Conversation: Trying to generalize David Wheeler's Algebra helpers:
>
> "This isn't the way we usually prove substitutions. df-sb is not really a
> substitution operator, it is more like a "deferred substitution", a term that
> is equivalent to the result of the substitution without actually performing
> it. To actually perform a substitution, we use so-called "equality theorems".
> These theorems usually end in *eq, *eq1,*eq1i, *eq1d and so on, and prove A =
> B -> P(A) = P(B) for different values of P. By cobbling them together you can
> subtitute into any expression."
Perhaps another way to understand it is that you have to start by showing that
two
simple expressions are equivalent, then use other theorems to build up & prove
that the
larger expressions including them are equivalent.
My "Algebra helpers" were intended to make it easier to skip those steps in
common cases.
I made samples & stopped because I didn't know if anyone would use them.
Also, I made both deduction form (ph -> ... ) & non-deduction form versions;
if the deduction forms are all that would be used, well, let's focus on that.
If someone *does* find them useful, let me know, that work could be continued
if there were actual users :-).
--- David A. Wheeler
>
> In Conversation: Breaking news: LTL section valid:
>
> "This kind of statement does not work for metamath, because we don't have a
> general proper substitution mechanism. The one we have (df-sb) reduces to the
> metatheorem ( x = y -> F(x) = F(y) ) which still must be provided separately,
> which is why we need equality theorems or axioms for every primitive
> operation."
>
> MM> sh st *eq
> (and *eq1, *eq1i, and *eq1d)
> return scads of interesting theorems, but I don't understand how to use the
> "equality theorems" to perform proper substitution.
>
> Please describe the general principle, and give a simple example.
>
> --Brian
>
>
>
> --
> 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/c7d4d8a3-b112-43cd-b154-5fcf816d978dn%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/ED71E4F0-7D61-4913-B4E9-CA4191E45506%40dwheeler.com.
