Proper Substitution: df-sb & df-sbc

[Brian Larson]

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

[Thierry Arnoux]

Hi Brian,

As you found out, equality theorems end in `eq`. They prove the equality for an expression, given equality for one term of that expression. For example, ~ sumeq1d states |- ( ph -> A = B ) ==> ( ph -> sum_ k e. A C = sum_ k e. B C ) . Here we have effectively substituted ` A ` for ` B ` in the sum expression.

There is another theorem ~ sumeq2dv, for equality of the other term (the summand ` C `).

There is also a related family of theorems for changing the bound variable ` k ` into another variable (for my sum example, that would be ~ cbvsum). Change bound variable theorems are not equality theorems per se, but they also allow a substitution of a part of the formula, namely, the bound (set) variables.

You can for example have a look at http://us2.metamath.org:88/mpeuni/breprval.html, step 3~8 for how several equality theorems are used together to prove a more complex substitution.

What we end up with is an equality, or an equivalence, if you look at the result of step 6, ~ eqeq1d, which we can then chain with more equalities to get the desired result.

I hope this helps!

Maybe if you could give the actual case you'd like to solve, we could help you prove it or rewrite it in a way which is easier to prove.

BR,
_
Thierry

--
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 metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/c7d4d8a3-b112-43cd-b154-5fcf816d978dn%40googlegroups.com.

[Alexander van der Vekens]

On Tuesday, December 28, 2021 at 3:08:36 AM UTC+1 brianral...@gmail.com 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.

 

What is the problem with Brian's theorem? A proof of it (mainly based on ~sbequ12) is as follows:

    sbiei.1 $e |- ph $.
    sbiei.2 $e |- x = y $.
    sbiei.3 $e |- ( [ y / x ] ph <-> ps ) $.
    sbiei $p |- ps $=

1 sbiei.1        $e |- ph
2 sbiei.2        $e |- x = y
3 sbequ12        $p |- ( x = y -> ( ph <-> [ y / x ] ph ) )
4 2,3 ax-mp      $a |- ( ph <-> [ y / x ] ph )
5 1,4 mpbi       $p |- [ y / x ] ph
6 sbiei.3        $e |- ( [ y / x ] ph <-> ps )
7 5,6 mpbi       $p |- ps

Even in closed form the theorem is valid:

  sbieg $p |- ( ( ph /\ x = y /\ ( [ y / x ] ph <-> ps ) ) -> ps ) $=

 1 bicom         $p |- ( ( ps <-> ph ) <-> ( ph <-> ps ) )
 2 sbequ12       $p |- ( x = y -> ( ph <-> [ y / x ] ph ) )
 3 2 bibi1d      $p |- ( x = y -> ( ( ph <-> ps ) <-> ( [ y / x ] ph <-> ps ) ) )
 4 3 adantl      $p |- ( ( ph /\ x = y ) -> ( ( ph <-> ps ) <-> ( [ y / x ] ph <-> ps ) ) )
 5 1,4 syl5bb    $p |- ( ( ph /\ x = y ) -> ( ( ps <-> ph ) <-> ( [ y / x ] ph <-> ps ) ) )
 6 bianir        $p |- ( ( ph /\ ( ps <-> ph ) ) -> ps )
 7 6 ex          $p |- ( ph -> ( ( ps <-> ph ) -> ps ) )
 8 7 adantr      $p |- ( ( ph /\ x = y ) -> ( ( ps <-> ph ) -> ps ) )
 9 5,8 sylbird   $p |- ( ( ph /\ x = y ) -> ( ( [ y / x ] ph <-> ps ) -> ps ) )
10 9 3impia      $p |- ( ( ph /\ x = y /\ ( [ y / x ] ph <-> ps ) ) -> ps )

[David A. Wheeler]

> On Dec 27, 2021, at 9:08 PM, Brian Larson <brianral...@gmail.com> 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
>
>
>

[Brian Larson]

Thank you all for your helpful suggestions.

Thierry's proof of brepval is similar to my "workarounds":  building-up equalities or equivalences in lieu of actual substitution.

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.

I will look more closely at David's algebra helpers.

--Brian

[David A. Wheeler]

> On Dec 28, 2021, at 4:11 PM, Brian Larson <brianral...@gmail.com> 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

[Mario Carneiro]

On Tue, Dec 28, 2021 at 4:11 PM Brian Larson <brianral...@gmail.com> 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

--
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 metamath+u...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/E5BB092F-3464-4B61-BBF2-DD170628896E%40dwheeler.com.

[Brian Larson]

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?

[Mario Carneiro]

On Fri, Dec 31, 2021 at 9:18 PM Brian Larson <brianral...@gmail.com> 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

[Brian Larson]

Mario,

Thanks for the suggestion of sbie.  That looks like just what I need.

--Brian

[Glauco]

Hi Brian, w.r.t. this part of your post

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

we use local class definition a lot, but you can also use local wff definition.

For example, you can take a look at the last hypothesis of ~ ioodvbdlimc1lem2

|- ( ch <-> ( ( ( ( ( ph /\ x e. RR+ )
       /\ j e. ( ZZ>= ` N ) )
       /\ ( abs ` ( ( S ` j ) - ( limsup ` S ) ) ) < ( x / 2 ) )
       /\ z e. ( A (,) B ) ) /\ ( abs ` ( z - A ) ) < ( 1 / j ) ) )

Disclaimer: today I would write a much sorter, more readable proof of that lemma (at the cost of more sublemmas) but I tried this "technique" as an experiment of local definition of a wff (as you write, it "could" make proof outlines more compact and understandable, not sure I succeeded in this specific example).

The invoking theorem, most of the time, will simply use a biid or a bitri and a bunch of cbv* (if disjoint vars have to be handled), in a very similar way of local class definitions (eqid and may be cbv*)

Doing a quick search, other contributors used local definitions for wffs, see for instance ~ bnj1189

Glauco