Mario, Thanks for the suggestion of sbie. That looks like just what I need.
--Brian On Sunday, January 2, 2022 at 8:39:31 PM UTC-6 [email protected] wrote: > On Fri, Dec 31, 2021 at 9:18 PM Brian Larson <[email protected]> > wrote: > >> Thank you Mario for the perspicuous example. >> This also shows the power of the deductive form. >> I'm encouraged to prove deductive form of my own theorems. >> >> I tried Mario's example in mmj2, and it was too easy: >> h1::sbdmo.1 |- x = y >> d1::oveq1 |- ( x = y -> ( x + 2 ) = ( y + 2 ) ) >> qed:d1:breq1d |- ( x = y -> ( ( x + 2 ) < 5 <-> ( y + 2 ) < 5 >> ) ) >> $= ( cv wceq c2 caddc co c5 clt oveq1 breq1d ) ACZBCZDLEFGMEFGHILMEFJK $. >> >> For my theorems, I often wanted to substitute a wff for a wff. >> I had ( ph <-> ps ), and wanted to prove something that had ph, but >> needed ps there. >> I fumbled around and got a proof (not very elegant) "building up" as >> David suggested. >> > > Brian, it would help if you gave a snippet from a proof you are working on > so that the example can be more pertinent. > > >> I had two other uses for substitution in mind. >> I'm trying to use Metamath to prove soundness of some logic used to prove >> program correctness. >> The Hoare triples used for proof obligations have three formulas, two >> predicates in a first-order temporal logic, and a formula (to be) satisfied >> by constructing a computation lattice. It's analogous to the (old) guarded >> commands proofs of Dijkstra and Gries: >> { P } S { Q } >> Though the syntax uses << >> instead of { } >> For { P ) x:=e { Q }, that means proving P -> [ e / x ] Q, thus my "need" >> for substitution. >> Thinking about the problem, my proof assistant does the substitution >> (whether it does so correctly is another matter), so proving the rhs of >> df-sb and df-sbc is all I need (perhaps with a temporary variable y=e to >> substitute [ y / x ]). >> > > The normal way to prove this (for concrete propositions P and Q) is to > apply a theorem like http://us.metamath.org/mpeuni/sbie.html (adapted to > have a conclusion like |- { P ) x:=e { Q } instead of |- ( [ x / e ] Q <-> > P ) ), which, like most theorems that require a substitution, has a ( x = e > -> ( P <-> Q ) ) hypothesis that you can prove as mentioned earlier. > > The other use is for using labeled predicates. This makes proof outlines >> much more compact and understandable. At user command, a tactic will >> replace predicate labels with the text of the predicate, having substituted >> actual parameters for formals. >> Here is a bit trickier because I want to substitute a predicate for a >> predicate label rather than set or class variables. >> >> Do any such wff labels (variables) exist in set.mm? >> > > I don't think so, if I understand you correctly. You can use wff > metavariables to make a wff opaque for the duration of a lemma when the > content of the proposition is not used by the lemma, but unless your proof > assistant supports it (and AFAIK MM-PA and mmj2 don't) you can't hide the > value of an assigned wff metavariable, they are always displayed in full. > > Mario > -- 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/666a2349-4360-4d73-a658-98cb9089626an%40googlegroups.com.
