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/CAFXXJSsX1Y6LiC8cUZv6x11k8YwO3sGnp_4ABq8DdcYt7E9zyA%40mail.gmail.com.
