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.
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 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?
On Tuesday, December 28, 2021 at 9:01:22 PM UTC-6 [email protected] wrote:
> On Tue, Dec 28, 2021 at 4:11 PM Brian Larson <[email protected]>
> wrote:
>
>> Alexander's proofs of sbiei and sbieg are so simple and elegant, I'm
>> sorry I didn't try it myself.
>> The challenge will be establishing ( [ y / x ] ph <-> ps ). Given a
>> distinct variable hypothesis $d y ph $. there should be some (easy?) way
>> to show that ps is the same as ph having y substituted for x.
>>
>
> An equivalent way to write that hypothesis, and by far preferred in set.mm,
> is ( x = y -> ( ph <-> ps ) ). Since we still have $d y ph $., you can't
> just take ps to be ph; if ph contains any occurrences of x you are forced
> to go and replace the x by something else, and the obvious thing is to use
> the equality hypothesis to replace each x with a y. The *eq theorems are
> the means by which we do this. For example, suppose ph was ( x + 2 ) < 5.
> Then when you apply this theorem, you will get a subgoal of the form
>
> 1: |- ( x = y -> ( ( x + 2 ) < 5 <-> ?ps ) )
>
> where ?ps is a placeholder to say that we don't know what to put in place
> of it yet. In this case, we want to prove it for ?ps := ( y + 2 ) < 5,
> because this is the result of proper substitution of y for x in ph. But
> anything equivalent to ( y + 2 ) < 5, like ( ( y + 2 ) < 5 /\ T. ) would
> also be provable in this position.
>
> 1: |- ( x = y -> ( ( x + 2 ) < 5 <-> ( y + 2 ) < 5 ) )
>
> To simplify this goal, we notice that the head expression in ph is a
> binary relation df-br (applied to three arguments "( x + 2 )", "<", and
> "5"), and only the first one needs to change, the other two are constants.
> So we apply http://us.metamath.org/mpeuni/breq1d.html , which yields:
>
> 2: |- ( x = y -> ( x + 2 ) = ( y + 2 ) )
> 1:2:breq1d |- ( x = y -> ( ( x + 2 ) < 5 <-> ( y + 2 ) < 5 ) )
>
> Now the head term of the LHS is df-ov applied to "x", "+" and "2", and
> again only the first term needs to change. In fact, the first term is
> actually the x we want to replace, so we can use oveq1 instead of oveq1d
> here:
>
> 2::oveq1 |- ( x = y -> ( x + 2 ) = ( y + 2 ) )
> 1:2:breq1d |- ( x = y -> ( ( x + 2 ) < 5 <-> ( y + 2 ) < 5 ) )
>
> and now we're done. This is a small example but hopefully it shows you how
> these *eq theorems can be used to prove theorems of the form ( x = y ->
> P(x) = P(y) ) where P(x) is any class or wff expression with one or more
> x's in it, and P(y) is the corresponding expression with the x's replaced
> by y.
>
> If you have a more pertinent example for your use case, please speak up.
>
> Mario
>
> On Tue, Dec 28, 2021 at 4:50 PM David A. Wheeler <[email protected]>
> wrote:
>
>>
>>
>> > On Dec 28, 2021, at 4:11 PM, Brian Larson <[email protected]>
>> wrote:
>> >
>> > I will look more closely at David's algebra helpers.
>>
>> Enjoy. You won't find any cleverness or elegance in them.
>> Their purpose is to prove "obvious" things, generally from the outside in,
>> so you don't have to do them.
>>
>> --- David A. Wheeler
>>
>> --
>> 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/E5BB092F-3464-4B61-BBF2-DD170628896E%40dwheeler.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/015b6c20-4fd4-407e-85bb-9f2b286dd4bcn%40googlegroups.com.
