--
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.
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 formB. 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 HelpersD. Figure out how to generalize it so one proof can be used to produce all of David's associative Algebra Helpers.
A = ( ( ( ( x x. D ) + E ) x. F ) ^ G )
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.
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.
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)?
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?
* Use metamath's built in substitution to eliminate the need for multiple versions of the 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.To use unification in a proof we would need the following steps:
- template: $e A template to be unified in which a set variable appears twice
- substitute: $e Equality of two Class expression to be substituted into different instances of the set variable.
- 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.
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 ) ABCFKZDGKZEHKCBFKZDGKZEHKIAOQEHANPDGJLLM $.$)Notes:1. This proof still has only one hypothesis2. 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 variantsIf we also count one X on the RHS and the other on the LHS we get three versions of each variantIf 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?
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.