Trying to generalize David Wheeler's Algebra helpers.

[Noam Tene]

The following proof is inspired by David Wheeler's Algebra helpers.

It tries to generate something similar to them for a more complicated expression.

If I can get something like this to work, my next steps would hopefully be to:

A. Translate it to deduction form

B. Generate an inference form proof from it (so it can be used to make other proofs shorter).

C. Figure out how to generalize it so one proof can be used to produce all of David's commutative Algebra Helpers 

D. Figure out how to generalize it so one proof can be used to produce all of David's associative Algebra Helpers.

For now, though, I do not even know how to get from step 80 to step 99

$( <MM> <PROOF_ASST> THEOREM=comexpr_NT  LOC_AFTER=?

h50::comexpr_NT.6 |- A = ( ( ( B + C ) * D ) + E )

h51::comexpr_NT.1 |- A e. CC

h52::comexpr_NT.2 |- B e. CC

h53::comexpr_NT.3 |- C e. CC

h54::comexpr_NT.4 |- D e. CC

h55::comexpr_NT.5 |- E e. CC

73:52,53:addcomi |- ( B + C ) = ( C + B )

80::dfsbcq         |- (  ( B + C ) = ( C + B ) -> 

                         (   [. ( B + C ) /  x ]. A = ( ( x * D ) + E )

                         <-> [. ( C + B ) /  x ]. A = ( ( x * D ) + E ) ) )

99::              |- (      A = ( ( ( B + C ) * D ) + E ) 

                      <->   A = ( ( ( C + B ) * D ) + E ) )

qed:50,99:mpbi |- A = ( ( ( C + B ) * D ) + E )

$)

Any suggestions?

[Mario Carneiro]

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. Here's a proof of your theorem:

h50::comexpr_NT.6   |- A = ( ( ( B + C ) * D ) + E )
h51::comexpr_NT.1  |- A e. CC
h52::comexpr_NT.2   |- B e. CC
h53::comexpr_NT.3   |- C e. CC
h54::comexpr_NT.4  |- D e. CC
h55::comexpr_NT.5  |- E e. CC

d2:52,53:addcomi   |- ( B + C ) = ( C + B )
d3:d2:oveq1i       |- ( ( B + C ) * D ) = ( ( C + B ) * D )
d1:d3:oveq1i       |- ( ( ( B + C ) * D ) + E ) = ( ( ( C + B ) * D ) + E )
qed:50,d1:eqtri |- A = ( ( ( C + B ) * D ) + E )

By the way, I proved this in one step in mmj2 - I wrote the statement of the theorem and "qed:50:eqtri" on the last line and the other steps were generated automatically (including the addcomi application). If this doesn't happen for you double check the ProofAsstUseAutotransformations and MacrosEnabled runparms (the default values should work).

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/17c95885-5554-4918-8b7e-34cd8d4adfa1%40googlegroups.com.

[Mario Carneiro]

On Fri, Aug 9, 2019 at 12:46 PM Noam Tene <noam...@gmail.com> wrote:

The following proof is inspired by David Wheeler's Algebra helpers.

It tries to generate something similar to them for a more complicated expression.

If I can get something like this to work, my next steps would hopefully be to:

A. Translate it to deduction form

B. Generate an inference form proof from it (so it can be used to make other proofs shorter).

C. Figure out how to generalize it so one proof can be used to produce all of David's commutative Algebra Helpers 

D. Figure out how to generalize it so one proof can be used to produce all of David's associative Algebra Helpers.

You can't prove all of David's theorems with one proof. In fact, you can almost never apply one proof (sequence of theorem applications) to prove multiple theorems, unless one is a substitution instance of another, and we generally try to avoid that in the library. What you can do instead is write a program that will generate proofs for all statements in a certain class, for example equalities in the theory of rings, but metamath and its IDEs will not help you here - they are designed for proving concrete theorems, not families of theorems. (Metamath will often call its theorems "schemes", but they are only schematic under substitution of variables; no more complicated collection of theorems can be proven with a single theorem.)

While this is fine for exploratory purposes, I wouldn't want this theorem in set.mm - it's too specific. The entropy of the statement is comparable to the entropy of the sequence "eqtri oveq1i oveq1i addcomi" that was used to prove it, so you would need a huge number of variations on the theorem and there probably wouldn't be enough use of any individual such theorem to be worth the work of writing the whole set.

Also the use of * in the theorem doesn't mean what you think it means. The symbol for multiplication is "x."; the symbol " * " is a unary function that denotes conjugation of complex numbers, as in:

( * ` ( A + ( B x. _i ) ) ) = ( A - ( B x. _i ) )

Mario

[David A. Wheeler]

On Fri, 9 Aug 2019 09:46:48 -0700 (PDT), Noam Tene <noam...@gmail.com> wrote:
> The following proof is inspired by David Wheeler's Algebra helpers

> <http://us.metamath.org/mpeuni/mmtheorems308.html#mm30784s>.

Glad to be an inspiration!

> It tries to generate something similar to them for a more complicated
> expression.

I think this proof is way too specific.
It's unlikely to be something someone wants directly
and it's unlikely to be used by something else.

I'm skeptical it's worth the trouble, but you could at least generalize this to:

( ( ( B + C ) F D ) G E ) = ( ( ( C + B ) F D ) G E )

> If I can get something like this to work, my next steps would hopefully be
> to:
>
> A. Translate it to deduction form

That's key. If you want something general, deduction form is a good place to be.

> For now, though, I do not even know how to get from step 80 to step 99
>
> $( <MM> <PROOF_ASST> THEOREM=comexpr_NT LOC_AFTER=?
>
> h50::comexpr_NT.6 |- A = ( ( ( B + C ) * D ) + E )
> h51::comexpr_NT.1 |- A e. CC
> h52::comexpr_NT.2 |- B e. CC
> h53::comexpr_NT.3 |- C e. CC
> h54::comexpr_NT.4 |- D e. CC
> h55::comexpr_NT.5 |- E e. CC
> 73:52,53:addcomi |- ( B + C ) = ( C + B )
> 80::dfsbcq |- ( ( B + C ) = ( C + B ) ->
> ( [. ( B + C ) / x ]. A = ( ( x * D ) + E )
> <-> [. ( C + B ) / x ]. A = ( ( x * D ) + E ) ) )
> 99:: |- ( A = ( ( ( B + C ) * D ) + E )
> <-> A = ( ( ( C + B ) * D ) + E ) )
> qed:50,99:mpbi |- A = ( ( ( C + B ) * D ) + E )

If you want to prove this sort of thing, I
find it easier to state the known equivalence,
then repeatedly add an operation "on both sides" to build up to what you want.
Basically, you "build up" expressions as mentioned in the
algebra helpers intro. E.g.:

|- ( B + C ) = ( C + B )

|- ( ( B + C ) * D ) = ( ( C + B ) * D )
|- ( ( ( B + C ) * D ) + E ) = ( ( ( C + B ) * D ) + E )

That said, "building up the equivalence" every time is a pain,
which is why I created my Algebra helpers.

I haven't completed the Algebra helpers because I wasn't sure
if anyone else would use them. If they are *used* then I'd want them in
the main body, but there's no point in going further
until there's actual *use*.

So.... would anyone else use the Algebra helpers if they were more complete?
I'd be happy to add to them and improve them, but only if they would be used.

I suspect the helpers should primarily be deduction form,
and then prove the induction form (if desired) from them.
(I had started in induction form, and I now think that was the wrong order).
It might be useful to prove more general theorems and then derive
the current Algebra helpers as special cases, but I think the current special
cases are useful because they're common. But all of these
are ways to improve them, and I only want to improve them if they'd be used.

--- David A. Wheeler

[Jon P]

I used mvllmuld as the final step of this proof. I like the algebra helpers in general, I think they are useful.

[David A. Wheeler]

On Fri, 9 Aug 2019 13:49:49 -0700 (PDT), Jon P <drjonp...@gmail.com> wrote:
> I used mvllmuld as the final step of this proof

> <http://us.metamath.org/mpegif/itgpowd.html>. I like the algebra helpers in

> general, I think they are useful.

Thank you! That's a vote of confidence *and* an actual cross-mathbox use
(at least for one of the deduction forms)!

Now that we have an actual cross-mathbox use, that's an argument for moving them
into the main body, at least for the deduction forms.

Does moving them to the main body seem acceptable?
Would it be reasonable to move the induction forms
as well (if they were proved from the deduction forms)?

--- David A. Wheeler

[Noam Tene]

Thank you Mario for the detailed explanation.

Sorry about the mistake with "*" vs "x." but it seems that you addressed my main questions anyway.

I was actually surprised that the complex conjugate "*" worked as a binary operator and did not generate an error.

I am so used to errors being generated by type checking that I did not realize that ( A * B ) may be valid syntax for something with an obscure meaning.

Writing "qed:50:eqtri" instead of ""qed:50" as Mario suggested "proves" the conjugate nonsense in one mmj2 unification step that generates several proof steps.

I should have known better but it takes some getting used to.

I wouldn't want this theorem in set.mm either.

In fact, I purposely chose the expression to be "too specific" in order to make that point.

I proved "$e A = (( ( B + C ) x. D )  $p |- A = ( ( C + B ) x. D ) " myself in one step before I tried this example.

I originally thought that adding the "+ E" was enough to confuse mmj2 and make my point.

I was wrong, using "qed:50:eqtri" works in one mmj2 step even for:

h50::comexpr_NT.1 |- A = ( ( ( ( ( B + C ) x. D ) + E ) x. F ) ^ G )

h60::comexpr_NT.2   |- ( B + C ) = ( C + B )

qed:50:eqtri |- A = ( ( ( ( ( C + B ) x. D ) + E ) x. F ) ^ G )

A single Mmj2 "unify" automatically created 4 oveqli proof steps to generate the proof for this larger expression.

I am impressed that that mmj2 can do this manipulation.

This feature can be very useful for generating parts of long proofs.

The proof above generated 4 steps for a tree depth of 6.  Longer expressions could easily require more of these intermediate steps.

I still wonder if there is some way to use something like dfsbcq to:

    * reduce proof length (number of steps) and size (number of symbols displayed)

    * make proofs more readable.

    * Use metamath's built in substitution to eliminate the need for multiple versions of the Algebra helpers

    * Reduce the size of set.mm by eliminating multiple versions of useful patterns.

    * Facilitate proofs by variable substitution. 

Can we use Metamath substitution to unify both the antecedent and the result as instances of the expression:

A = ( ( ( ( x x. D ) + E ) x. F ) ^ G )

Can we build that capability into a proof? 

You can't prove all of David's theorems with one proof. In fact, you can almost never apply one proof (sequence of theorem applications) to prove multiple theorems, unless one is a substitution instance of another, and we generally try to avoid that in the library.

To use unification in a proof we would need the following steps:

1. template:   $e  A template to be unified in which a set variable appears twice
2. substitute:  $e  Equality of two Class expression to be substituted into different instances of the set variable.
3. instantiate: $p  theorem: the template unified with the two substitutions.

For relatively shallow expressions like David's Algebra Helpers, it may be easy to generate short proofs that do not use substitutions.

As the tree depth of the expression grows, using substitution will make more sense and have more benefits.

Metamath allows us to use unification on lemmas.

I understand why we want to avoid having too many lemmas.

Using lemmas (instead of a sequence of proof steps) inflates the library size and increases maintenance overhead.

David's Algebra Helpers (and my more esoteric examples) can already be added as "lemmas" in personal toolboxes.

I prefer using 3 proof steps (template, substitute, instantiate) to creating a new lemma for every template we might need.

Is there a way to do that?

 

The entropy of the statement is comparable to the entropy of the sequence "eqtri oveq1i oveq1i addcomi" that was used to prove it, so you would need a huge number of variations on the theorem and there probably wouldn't be enough use of any individual such theorem to be worth the work of writing the whole set.

That is exactly why I want to use substitution:  I want to avoid having to add every possibly useful variation as a lemma.

It will also save David the trouble of moving his helpers into the "main body".

In the long run, we may want to look for repeating patterns in set.mm proofs and see if we can extract "lemmas" that appear often enough that that stating them as "theorems"  will actually reduce the overall database size.  

For now, I just want to avoid having to write a lemma for every math rule I ever learned in high school and having to wonder how many other people might or might not want to use it.

[Norman Megill]

On Friday, August 9, 2019 at 5:01:46 PM UTC-4, David A. Wheeler wrote:

On Fri, 9 Aug 2019 13:49:49 -0700 (PDT), Jon P wrote:
> I used mvllmuld as the final step of this proof
> <http://us.metamath.org/mpegif/itgpowd.html>. I like the algebra helpers in
> general, I think they are useful.

Thank you! That's a vote of confidence *and* an actual cross-mathbox use
(at least for one of the deduction forms)!

Now that we have an actual cross-mathbox use, that's an argument for moving them
into the main body, at least for the deduction forms.

Does moving them to the main body seem acceptable?
Would it be reasonable to move the induction forms
as well (if they were proved from the deduction forms)?

mvllmuld is essentially one direction of the more general divmuld.  Although we would need an extra mpbird to use divmuld instead, I think mvllmuld is too specialized and would need a large number of uses to be justified.  So I would suggest that we continue to use divmuld and friends.  If at some point in the future a special case such as mvllmuld will shorten enough proofs, it's relatively easy to update them.

Norm

[David A. Wheeler]

On August 9, 2019 6:50:19 PM EDT, Norman Megill <n...@alum.mit.edu> wrote:
>mvllmuld is essentially one direction of the more general divmuld.
>Although we would need an extra mpbird to use divmuld instead, I think
>mvllmuld is too specialized and would need a large number of uses to be
>justified.

The purpose of algebra helpers like mvllmuld is not to make the proofs shorter, but to support a different style of proof.

The idea is to enable moving an outermost expression from one side to the other of an equality statement using a single step. I think this approach sometimes results in easier to understand proofs, and it is closer to how I usually think about algebraic expressions (so I find the proofs easier to create).

The whole point of the helpers is to make moving something from one side to the other a single step. So the fact that there are multistep approaches is true, but not relevant. I think it is worth doing, as the helpers can produce more human-friendly proofs (in my opinion). I do not know how many other people like them. It appears there is at least one other person, though!



--- David A.Wheeler

[Mario Carneiro]

On Fri, Aug 9, 2019 at 6:39 PM Noam Tene <noam...@gmail.com> wrote:

A single Mmj2 "unify" automatically created 4 oveqli proof steps to generate the proof for this larger expression.

I am impressed that that mmj2 can do this manipulation.

This feature can be very useful for generating parts of long proofs.

The proof above generated 4 steps for a tree depth of 6.  Longer expressions could easily require more of these intermediate steps.

By the way, this magic was brought to you by the mmj2 macro system, specifically "transformations.js" in the macro folder of mmj2. The way it works is simply to apply any theorem that unifies with the goal and produces no additional metavariables, except for a big blacklist of theorems that are not reversible (e.g. theorems that drop hypotheses). This turns out to be really effective at proving equality theorems (provided both sides of the equality are known), as well as closure theorems like

( ( 1 + 2 ) x. ( A - B ) ) e. RR

but it sometimes applies some bad theorems anyway, and you have to manually delete the bad steps. You can use the macro system to write your own tactics, although no one has attempted it except me so far, so the documentation is probably pretty bad.

 

I still wonder if there is some way to use something like dfsbcq to:

    * reduce proof length (number of steps) and size (number of symbols displayed)

    * make proofs more readable.

    * Use metamath's built in substitution to eliminate the need for multiple versions of the Algebra helpers

    * Reduce the size of set.mm by eliminating multiple versions of useful patterns.

    * Facilitate proofs by variable substitution. 

Can we use Metamath substitution to unify both the antecedent and the result as instances of the expression:

A = ( ( ( ( x x. D ) + E ) x. F ) ^ G )

Can we build that capability into a proof? 

Not without changing the metamath spec. There is a rigid specification of what metamath proofs can and can't do, which is used as the basis for the implementation of the several dozen metamath verifiers, and the stability of this spec is seen as a virtue, but it implies some fundamental limitations on what the proof format itself will support. That said, you can still obtain most of your goals without changing the spec by adding tooling on top.

To reduce the number of proof steps and symbols displayed, you can change the tool you are using to display the proof, so that it ignores some steps or hides some symbols. It already does that today; neither the metamath web site nor mmj2 display syntax steps, but they nevertheless appear in the proof that is stored in the .mm file. Compare this proof of id1, displayed using metamath.exe:

MM> sh p id1/all
 1     wph=wph   $f wff ph
 2       wph=wph   $f wff ph
 3       wps=wph   $f wff ph
 4   4:wps=wi    $a wff ( ph -> ph )
 5 5:wph=wi    $a wff ( ph -> ( ph -> ph ) )
 6   wps=4     $a wff ( ph -> ph )
 7     wph=wph   $f wff ph
 8     wps=wph   $f wff ph
 9   min=ax-1  $a |- ( ph -> ( ph -> ph ) )
10       wph=wph   $f wff ph
11         wph=4     $a wff ( ph -> ph )
12         wps=wph   $f wff ph
13       wps=wi    $a wff ( ( ph -> ph ) -> ph )
14     wph=wi    $a wff ( ph -> ( ( ph -> ph ) -> ph ) )
15       wph=5     $a wff ( ph -> ( ph -> ph ) )
16       wps=4     $a wff ( ph -> ph )
17     wps=wi    $a wff ( ( ph -> ( ph -> ph ) ) -> ( ph -> ph ) )
18       wph=wph   $f wff ph
19       wps=4     $a wff ( ph -> ph )
20     min=ax-1  $a |- ( ph -> ( ( ph -> ph ) -> ph ) )
21       wph=wph   $f wff ph
22       wps=4     $a wff ( ph -> ph )
23       wch=wph   $f wff ph
24     maj=ax-2  $a |- ( ( ph -> ( ( ph -> ph ) -> ph ) ) -> ( ( ph -> ( ph ->
                                                     ph ) ) -> ( ph -> ph ) ) )
25   maj=ax-mp $a |- ( ( ph -> ( ph -> ph ) ) -> ( ph -> ph ) )
26 id1=ax-mp $a |- ( ph -> ph )

to the same proof without syntax steps:

MM> sh p id1
 9   min=ax-1  $a |- ( ph -> ( ph -> ph ) )
20     min=ax-1  $a |- ( ph -> ( ( ph -> ph ) -> ph ) )
24     maj=ax-2  $a |- ( ( ph -> ( ( ph -> ph ) -> ph ) ) -> ( ( ph -> ( ph ->
                                                     ph ) ) -> ( ph -> ph ) ) )
25   maj=ax-mp $a |- ( ( ph -> ( ph -> ph ) ) -> ( ph -> ph ) )
26 id1=ax-mp $a |- ( ph -> ph )

(Actually even this form reveals the missing steps, since you can see that the step numbers are not sequential. They are renumbered to be sequential in the web site version http://us2.metamath.org/mpeuni/id1.html .)

We've talked a lot about how to identify and hide "inessential" steps from the proof display, but I've never seen anything fully satisfactory. I would just recommend to learn how to skim a metamath proof display for the relevant information.

    * Use metamath's built in substitution to eliminate the need for multiple versions of the Algebra helpers

We already make extensive use of metamath's substitution to minimize proof work. For example, if we have a function like

df-foo $a |- foo = ( x e. CC , y e. CC |- ( ( x + y ) x. ( x x. y ) ) )

then the very first theorem we will usually prove is the value of this given some (class) arguments:

fooval $p |- ( ( A e. CC /\ B e. CC ) -> ( A foo B ) = ( ( A + B ) x. ( A x. B ) ) )

This may look like a silly thing since all I've done is use capital letters instead of lowercase, but it performs an important function. Inside the proof of this theorem will be a proof of

|- ( ( x = A /\ y = B ) -> ( ( x + y ) x. ( x x. y ) ) = ( ( A + B ) x. ( A x. B ) ) )

which will apply oveq12d and so on. The important part is that this is "doing the equality proof so you don't have to", in the sense that without the theorem I would have to prove this equality theorem for every choice of input to foo, while with the theorem it's only one step, and I can easily instantiate it to get

|- ( ( 1 e. CC /\ A e. CC ) -> ( 1 foo A ) = ( ( 1 + A ) x. ( 1 x. A ) ) )

|- ( ( ( 2 + 2 ) e. CC /\ 4 e. CC ) -> ( ( 2 + 2 ) foo 4 ) = ( ( ( 2 + 2 ) + 4 ) x. ( ( 2 + 2 ) x. 4 ) ) )

and so on, with one application of fooval each. If fooval was stated as

fooval2 $p |- ( ( x e. CC /\ y e. CC ) -> ( x foo y ) = ( ( x + y ) x. ( x x. y ) ) )

instead, then although it is logically equivalent to fooval, you wouldn't be able to leverage metamath's built in substitution to apply it to the case x = ( 2 + 2 ), y = 4, because set variables can only be substituted for other set variables. You would have to prove the substitution inside the logic, which means lots of oveq12d type steps.

In summary, a metamath theorem encodes a "template" which will match against the goal modulo substitution to the class and wff variables of the statement. A fixed theorem cannot do anything more complicated than that, which means in particular that you can't "pre-substitute" a term into an expression - you have to give that subgoal back to the user. This is why theorems like nnind (http://us2.metamath.org/mpeuni/nnind.html) have a bunch of hypotheses like ( x = 1 -> ( ph <-> ps ) ), because the theorem is trying to make it convenient to do the substitution (here ps is meant to denote [ 1 / x ] ph), but the best it can do is set up the required equality subproof, because it doesn't yet know what the expressions are so it can't apply the right equality theorem. A theorem cannot conditionally apply a theorem, and it can't do proofs by recursion on the structure of the input expression.

You can't prove all of David's theorems with one proof. In fact, you can almost never apply one proof (sequence of theorem applications) to prove multiple theorems, unless one is a substitution instance of another, and we generally try to avoid that in the library.

To use unification in a proof we would need the following steps:

1. template:   $e  A template to be unified in which a set variable appears twice
2. substitute:  $e  Equality of two Class expression to be substituted into different instances of the set variable.
3. instantiate: $p  theorem: the template unified with the two substitutions.

For relatively shallow expressions like David's Algebra Helpers, it may be easy to generate short proofs that do not use substitutions.

As the tree depth of the expression grows, using substitution will make more sense and have more benefits.

Hopefully I've explained why this cannot be done in the language of metamath for fundamental logical reasons. That of course does not mean that it can't be done outside the language, in the tooling, and this is exactly what mmj2 does. The choice to spam text to the screen on success as mmj2 does is an implementation detail; my new proof assistant for metamath zero doesn't display autogenerated steps which makes it significantly less verbose (for better or worse).

 

Metamath allows us to use unification on lemmas.

I understand why we want to avoid having too many lemmas.

Using lemmas (instead of a sequence of proof steps) inflates the library size and increases maintenance overhead.

David's Algebra Helpers (and my more esoteric examples) can already be added as "lemmas" in personal toolboxes.

I prefer using 3 proof steps (template, substitute, instantiate) to creating a new lemma for every template we might need.

Is there a way to do that?

This procedure can be implemented as a macro or tactic in a proof assistant, which is in some ways better than a lemma (they are more flexible) and in some ways worse (the tactic itself is not stored, just the result, so if you come back to the theorem later there will be no evidence that you used a program to generate the proof).

 

The entropy of the statement is comparable to the entropy of the sequence "eqtri oveq1i oveq1i addcomi" that was used to prove it, so you would need a huge number of variations on the theorem and there probably wouldn't be enough use of any individual such theorem to be worth the work of writing the whole set.

That is exactly why I want to use substitution:  I want to avoid having to add every possibly useful variation as a lemma.

It will also save David the trouble of moving his helpers into the "main body".

In the long run, we may want to look for repeating patterns in set.mm proofs and see if we can extract "lemmas" that appear often enough that that stating them as "theorems"  will actually reduce the overall database size.  

For now, I just want to avoid having to write a lemma for every math rule I ever learned in high school and having to wonder how many other people might or might not want to use it.

This project is possible, but you need to have a more rigid definition of "repeating pattern" for it to work. The kind of repeating pattern that can be extracted to a lemma is the kind where you apply the same sequence of theorems in the same order. For example, suppose you apply mpbird with divmuld as the second hypothesis, that is, you have the proof structure "mpbird ?a (divmuld ?b ?c ?d ?e)". You can imagine searching for this tree fragment in the library (unifying on the leaves and looking in subterms). You can also work out by unification what this proof fragment is a proof of, namely:

$e |- ( ph -> ( A / B ) = C )

$e |- ( ph -> A e. CC )

$e |- ( ph -> B e. CC )

$e |- ( ph -> C e. CC )

$e |- ( ph -> B =/= 0 )

$p |- ( ph -> ( B x. C ) = A )

You can generate this statement entirely by looking at the proof and naming the metavariables remaining after unification. This statement is proven by "mpbird h1 (divmuld h2 h3 h4 h5)" by construction, and if we call it "mvllmuld2" (the naming is not automatic, unfortunately), then we can replace all instances of "mpbird ?a (divmuld ?b ?c ?d ?e)" by "mvllmuld2 ?a ?b ?c ?d ?e". This decreases the number of steps used in all these proofs, as well as possibly the number of theorems referenced, and If it is used enough, this may cause a net decrease in total size of set.mm.

There are some small variations you can do to this pattern, but this is essentially how you can do lemma-compression in a MM database. It's an explicitly solvable problem exactly because we know that theorems are simple unification matches and don't do anything fancy like analyze their arguments.

Personally, I think that "every lemma you learned in high school" is already captured in the existing set.mm algebra theorems. But because of the combinatorial explosion you get by combining lemmas in different ways, we want to have a relatively small set of theorems that all play well together and can be powerfully combined, not necessarily an exhaustive enumeration of all ways to combine symbols. In this case, we are combining the relatively complete prop calc library (mpbird) with the deduction-form algebra library (divmuld). If you think of theorems as words, then you are able to express most atomic operations in one word, and the way it applies to your context in two. With this perspective, metamath is actually not that verbose at all, and creating more compound words like mvllmuld2 is of dubious advantage.

Mario

[Noam Tene]

As I newcomer, still trying to learn the ropes I tried to make sense of what Mario and David have been saying.

This is what I came up with:

A one line proof of comraddd that works for any associative operator:

$( <MM> <PROOF_ASST> THEOREM=comradd1d  LOC_AFTER=?

h1::comradd1d.1 |- ( ph -> ( A F B ) = ( B F A ) )

qed:1:eqeq2d     |- ( ph -> ( X = ( A F B ) <-> X = ( B F A ) ) )

$=  ( comradd1d.1 co eqeq2d ) ABCDGCBDGEFH $.

$)

Notes: 

1. This proof has only one hypothesis as opposed to David's 3

2. Using David's comraddd requires only one proof step, Using this version requires three (prove the commutativity, eqeq2d, use the biconditional)

3. This single proof covers more ground (any commutative infix operation on any set, not limited to CC)

4. The biconditional can be used in both directions whereas induction form can only be used in one direction, but in this case they are the same.

I do not see a need to move either comraddd or my version to the main body of set.mm considering how easy it is to bypass them.

My next step was to try something longer to see if I can make a helper that would be worth adding because it would save proof steps:

$( <MM> <PROOF_ASST> THEOREM=inner_commd  LOC_AFTER=?

h1::inner_commd.1 |- ( ph -> ( A F B ) = ( B F A ) )

2:1:oveq1d        |- ( ph -> ( ( A F B ) G C )       =   ( ( B F A ) G C ) ) 

3:2:oveq1d        |- ( ph -> ( ( ( A F B ) G C ) H D ) = ( ( ( B F A ) G C ) H D ) )

qed:3:eqeq2d      |- ( ph -> ( X = ( ( ( A F B ) G C ) H D ) <-> X = ( ( ( B F A ) G C ) H D ) ) )

$=  ( inner_commd.1 co oveq1d eqeq2d ) ABCFKZDGKZEHKCBFKZDGKZEHKIAOQE

    HANPDGJLLM $.

$)

Notes:

1. This proof still has only one hypothesis

2. Using this version still requires only three proof steps (prove the commutativity, inner_commd, use the biconditional).

3. Thanks to David's suggestion - this generalized single proof covers any commutative infix operation inside a large expression on any set, not limited to CC.

4. The biconditional can be used in both directions whereas induction form can only be used in one direction, but in this case they are the same.

5. Proofs that use this would save the two oveq1d steps.

I still do not see a need to move this in to the main body of set.mm until we can generalize it even further.

Here are at least 6 variants all with X on the LHS: 

X =       (     ( A F B ) G C       ) <-> X =       (     ( B F A ) G C )       

X =       ( C G ( A F B )           ) <-> X =       ( C G ( B F A )     )       

X = (     (     ( A F B ) G C ) H D ) <-> X = (     (     ( B F A ) G C ) H D )

X = (     ( C G ( A F B )     ) H D ) <-> X = (     ( C G ( B F A )     ) H D )

X = ( D H (     ( A F B ) G C )     ) <-> X = ( D H (     ( B F A ) G C )     )

X = ( D H ( C G ( A F B )     )     ) <-> X = ( D H ( C G ( B F A )     )     )

If we count the ones with X on the RHS we get twice as many variants

If we also count one X on the RHS and the other on the LHS we get three versions of each variant

If we also state the equality (eliminating X and the bijection) we get four versions of each variant

Notes: 

1. The first two lines above use only 3 variables. They are more likely to be used but their benefit is limited because they are easier to bypass.

2. The next four lines use 4 variables.  There are more variants which may not be as common as the first two but they save more lines for proofs that do use them.

3. This is just the tip of an iceberg: with 5 or more variables these effects will only grow.

 

Proofs that use such theorems could apply eqcomi separately to each side of the bijection as needed.

They can also eliminate X to recover the equality (is there a way to introduce X back out of nothing?).

So there is no clear need to have several versions of each variant.

If the goal is to save steps and make proofs readable, having many versions may reduce the overall size of the database.

Even if these theorems do reduce the size of the database there is something inelegant and inefficient about adding all of them.

I am still looking for a clean and elegant way to do this with one or two theorems instead of 24.

• If you can't imagine needing these theorems for expressions with more than 5 variable take a look at the proof for quart 
• Imagine trying to reproduce the quart proof for fields other than CC.
• If tools like mmj2 could automatically generate quart proofs for other fields, would we want to store each of them separately?

[David A. Wheeler]

On Sun, 11 Aug 2019 12:19:45 -0700 (PDT), Noam Tene <noam...@gmail.com> wrote:
> A one line proof of comraddd that works for any associative operator:
>
> $( <MM> <PROOF_ASST> THEOREM=comradd1d LOC_AFTER=?
> h1::comradd1d.1 |- ( ph -> ( A F B ) = ( B F A ) )
> qed:1:eqeq2d |- ( ph -> ( X = ( A F B ) <-> X = ( B F A ) ) )
> $= ( comradd1d.1 co eqeq2d ) ABCDGCBDGEFH $.
> $)

> I do not see a need to move either comraddd or my version to the main body
> of set.mm considering how easy it is to bypass them.

comraddd is less interesting, it'd be okay to leave it behind.
What's more interesting are the ones that let you move expressions
from one side of an equality to the other in one step
(instead of having to build up from equalities).

That said, let me explain why I did it.

> Notes:
> 1. This proof has only one hypothesis as opposed to David's 3

Yes, but in *practice* you now have to prove the hypothesis,
which will typically require additional theorems and so on.
I find that the hypotheses listed above are often "already hanging around"
in the theorem or database.

> 2. Using David's comraddd requires only one proof step, Using this version
> requires three (prove the commutativity, eqeq2d, use the biconditional)

Right. My theory is that "+" is so common that handling things and
directly is useful.

> 3. This single proof covers more ground (any commutative infix operation on
> any set, not limited to CC)

Yes, it's definitely more general, but now you have to prove the case.

Normally we go for the general case, which is why these helpers are an experiment.

...

As I noted earlier, the point of the "helpers" is not to reduce the database
size (I doubt they will), but to enable a different approach to proofs so
that people don't need to "build up" from equalities.
The "building up" always works, but it can be a pain and people
don't typically do this when doing Algebra. Metamath is
*capable* of doing it this other way, but doing it efficiently
requires helpers.

--- David A. Wheeler

[Mario Carneiro]

On Sun, Aug 11, 2019 at 3:19 PM Noam Tene <noam...@gmail.com> wrote:

As I newcomer, still trying to learn the ropes I tried to make sense of what Mario and David have been saying.

This is what I came up with:

A one line proof of comraddd that works for any associative operator:

$( <MM> <PROOF_ASST> THEOREM=comradd1d  LOC_AFTER=?

h1::comradd1d.1 |- ( ph -> ( A F B ) = ( B F A ) )

qed:1:eqeq2d     |- ( ph -> ( X = ( A F B ) <-> X = ( B F A ) ) )

$=  ( comradd1d.1 co eqeq2d ) ABCDGCBDGEFH $.

$)

Notes: 

1. This proof has only one hypothesis as opposed to David's 3

2. Using David's comraddd requires only one proof step, Using this version requires three (prove the commutativity, eqeq2d, use the biconditional)

3. This single proof covers more ground (any commutative infix operation on any set, not limited to CC)

4. The biconditional can be used in both directions whereas induction form can only be used in one direction, but in this case they are the same.

I do not see a need to move either comraddd or my version to the main body of set.mm considering how easy it is to bypass them.

I'm wondering how to make this more precise, but my intuition is that these theorems have no added value. I can explain very easily at least in this case: comradd1d is literally a substitution instance of eqeq2d, so anything you prove with comradd1d can also be proven in the same number of steps using eqeq2d. (Technically that's a lie, because I'm ignoring the syntax steps - you can see "co" in the compressed proof, so it's really abbreviating two theorem applications, one of which is syntax.)

My next step was to try something longer to see if I can make a helper that would be worth adding because it would save proof steps:

$( <MM> <PROOF_ASST> THEOREM=inner_commd  LOC_AFTER=?

h1::inner_commd.1 |- ( ph -> ( A F B ) = ( B F A ) )

2:1:oveq1d        |- ( ph -> ( ( A F B ) G C )       =   ( ( B F A ) G C ) ) 

3:2:oveq1d        |- ( ph -> ( ( ( A F B ) G C ) H D ) = ( ( ( B F A ) G C ) H D ) )

qed:3:eqeq2d      |- ( ph -> ( X = ( ( ( A F B ) G C ) H D ) <-> X = ( ( ( B F A ) G C ) H D ) ) )

$=  ( inner_commd.1 co oveq1d eqeq2d ) ABCFKZDGKZEHKCBFKZDGKZEHKIAOQE

    HANPDGJLLM $.

$)

Notes:

1. This proof still has only one hypothesis

2. Using this version still requires only three proof steps (prove the commutativity, inner_commd, use the biconditional).

3. Thanks to David's suggestion - this generalized single proof covers any commutative infix operation inside a large expression on any set, not limited to CC.

4. The biconditional can be used in both directions whereas induction form can only be used in one direction, but in this case they are the same.

5. Proofs that use this would save the two oveq1d steps.

In this case the theorem does not abbreviate one step, but rather the sequence "oveq1d oveq1d eqeq2d". It is still unnecessarily specific for this sequence of theorems; the most general unifier of this theorem sequence is

h1          |- ( ph -> A = B )

2:1:oveq1d        |- ( ph -> ( A G C )       =   ( B G C ) ) 

3:2:oveq1d        |- ( ph -> ( ( A G C ) H D ) = ( ( B G C ) H D ) )

qed:3:eqeq2d      |- ( ph -> ( X = ( ( A G C ) H D ) <-> X = ( ( B G C ) H D ) ) )

Note that inner_commd is a substitution instance of this theorem, let's call it foo. However, I don't think even foo is worth inclusion. Consider that I derived the statement of this theorem directly from the sequence "oveq1d oveq1d eqeq2d". So this theorem has literally no added content over that sequence of lemmas from an information entropy perspective. This is somewhat analogous to the lisp convention, if you are familiar with it, of having functions like

(cadr x) := (car (cdr x))

(cadar x) := (car (cdr (car x)))

(cddadr x) := (cdr (car (cdr (cdr x))))

and so on. (If you aren't familiar, "car" and "cdr" are the names of functions that get the first and second element of a pair, so we can compose them to dig into larger trees composed of pairs.) There is a combinatorial explosion of definitions with these names, so we are limited in how far we can define them; I think most lisps go up to around 4 deep of combinations of c[ad]*r. In so doing we are making the bet that by precomposing them we make things easier for the user, either because we think the definitions will be used enough to make the definition worthwhile, or because we think having a complete set with regular naming allows the user to just treat them parametrically (i.e. they can write "caddadadar" and get the expected result). But the probability of use goes down the deeper the precomposition, and the cost of definition increases exponentially, so we usually end up fairly low on that tradeoff curve.

I have not yet seen evidence that David's algebra helpers are not too far along the curve, and your lemmas seem to take it quite a bit further beyond what I would think is valuable by any objective metric I can see. I'm not saying it can't be justified, but I would need to better understand what value metric is being used.

I still do not see a need to move this in to the main body of set.mm until we can generalize it even further.

Here are at least 6 variants all with X on the LHS: 

X =       (     ( A F B ) G C       ) <-> X =       (     ( B F A ) G C )       

X =       ( C G ( A F B )           ) <-> X =       ( C G ( B F A )     )       

X = (     (     ( A F B ) G C ) H D ) <-> X = (     (     ( B F A ) G C ) H D )

X = (     ( C G ( A F B )     ) H D ) <-> X = (     ( C G ( B F A )     ) H D )

X = ( D H (     ( A F B ) G C )     ) <-> X = ( D H (     ( B F A ) G C )     )

X = ( D H ( C G ( A F B )     )     ) <-> X = ( D H ( C G ( B F A )     )     )

If we count the ones with X on the RHS we get twice as many variants

If we also count one X on the RHS and the other on the LHS we get three versions of each variant

If we also state the equality (eliminating X and the bijection) we get four versions of each variant

These are pointless variations. We already have equality commutation covered by the prop calc theorems, exactly because they allow us to be more rigid in the way we state domain specific theorems. Theorem enumeration is a pointless enterprise, unless you have a concrete use case. Also as I've pointed out none of these are mgu's of their proofs, even after generalizing the + and * to arbitrary operations.

Notes: 

1. The first two lines above use only 3 variables. They are more likely to be used but their benefit is limited because they are easier to bypass.

2. The next four lines use 4 variables.  There are more variants which may not be as common as the first two but they save more lines for proofs that do use them.

3. This is just the tip of an iceberg: with 5 or more variables these effects will only grow.

 

Proofs that use such theorems could apply eqcomi separately to each side of the bijection as needed.

They can also eliminate X to recover the equality (is there a way to introduce X back out of nothing?).

So there is no clear need to have several versions of each variant.

If the goal is to save steps and make proofs readable, having many versions may reduce the overall size of the database.

I am *highly* doubtful that these theorems will decrease the size of the database, even only at the 2 or 3 variable level. You really have to actually do the legwork of optimizing the database before you make a claim like that. I think David did an automated optimization pass a while back and the things he came up with were like "1 e. _V", which is a composition of two theorems that happens to come up a lot because of the way the set theory stuff is structured. The chance of some more complicated thing like a commutation applied 3 deep in an expression is vanishingly small in comparison.

 

Even if these theorems do reduce the size of the database there is something inelegant and inefficient about adding all of them.

I am still looking for a clean and elegant way to do this with one or two theorems instead of 24.

• If you can't imagine needing these theorems for expressions with more than 5 variable take a look at the proof for quart 
• Imagine trying to reproduce the quart proof for fields other than CC.
• If tools like mmj2 could automatically generate quart proofs for other fields, would we want to store each of them separately?

First of all, quart is kind of a special case. The algebra there is complicated even on paper. If you want to generalize it to other fields, what I would do is find/replace + and * with the general versions, and then replace the theorem applications with the generalized versions. It should be short work. But also, did you actually try to find instances of your theorem in quart? I'm pretty sure you won't find a 3 deep commutation, because the proof isn't structured that way. The much more efficient approach is to enter a subterm, do all the manipulations you need to until you can't anymore, and then go back out to the main term, rather than applying small operations at a distance. It is unfortunate that we usually structure these proofs in math books as equality chains with deeply embedded manipulations, because it leads to this inefficient proof style if you carry it over uncritically. I've talked about this also on one of Jon's threads:

https://groups.google.com/d/msg/metamath/DDN4noc0TYU/RbnkiEU9BwAJ

On Sun, Aug 11, 2019 at 4:15 PM David A. Wheeler <dwhe...@dwheeler.com> wrote:

As I noted earlier, the point of the "helpers" is not to reduce the database
size (I doubt they will), but to enable a different approach to proofs so
that people don't need to "build up" from equalities.
The "building up" always works, but it can be a pain and people
don't typically do this when doing Algebra.  Metamath is
*capable* of doing it this other way, but doing it efficiently
requires helpers.

To put it another way, I claim that there is a fundamental combinatorial issue with this proof approach (taken to its extremes), where you wish to stay at the top level the whole time and perform manipulations arbitrarily deep in subexpressions. With another proof system this might be possible (or at least automated at a different level), but in metamath theorems always match syntactically, so the deeper the manipulation you want to perform the longer the theorem has to be. To extract the right-most conjunct of a sequence of 10 formulas requires simpr, but the leftmost conjunct requires simp-10l. One of these is fundamentally a more complicated thing than the other. If that theorem wasn't there you would have to chain 10 adantr applications, but even with it you still have the work of writing (at least) 10 variations to get to simp-10l, plus the entropy of the digit sequence "10" to pick the right one (and I've biased left associated sequences here, which is a kind of cheating; with the cadr convention it would be caaaaaaaaaar or simpllllllllll which is a lot longer).

The further a subexpression is from the root, the fundamentally more expensive it is to manipulate. So I try to encourage a proof style where the thing you want to manipulate is right there at the root, and theorem applications manipulate the tree to bring the thing you want to work on to the root. Anything else is asymptotically more expensive, and this manifests itself in a number of ways depending on how you address it but the problem doesn't go away even if you automate it or prepare a lemma set to make it easier.

[Thierry Arnoux]

Hi Noam and all,

I would like to highlight that MMJ2 already supports automatically what you want to achieve.
If you fill in

1: |- ( ph -> ( B F A ) = ( A F B ) )
!qed: |- ( ph -> ( X = ( ( B F A ) G C ) <-> X = ( A F B ) G C ) ) )

and ask it to unify, MMJ2 automatically fills in the ~ oveq1d and ~ eqeq2d missing steps.
It will actually do so at any depth, and for any left/right combinations.
So we already have a way to automatically handle these cases, don’t we? Have you tried that out?

I believe that a more generic version of your theorem is actually just the chained application of ~ oveq1d and ~ eqeq2d, like:

h1: |- ( ph -> A = B )

!qed: |- ( ph -> ( X = ( A G C ) <-> X = ( B G C ) ) )
However, like Mario, I’m not convinced we should go ahead and include in the data base all possible combinations of such theorems.
BR,
_
Thierry

[Benoit]

For a few other examples, you can look at the subsection "21.29.8.2  Complex numbers (supplements)" (beginning with ~bj-subcom), in my mathbox.  They are in deduction form and for most of them, the conclusion is an equivalence.  There are a few other algebraic lemmas in other mathboxes as well.  In my case, I haven't tried to be systematic and haven't thought too much about the most economical way to treat these, but I used some of them to prove a formula for barycentric coordinates in ~bj-bary1.

Benoit