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." 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.
