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
<http://us.metamath.org/mpeuni/quart.html>
- Imagine trying to reproduce the quart
<http://us.metamath.org/mpeuni/quart.html> proof for fields other than
CC.
- If tools like mmj2 could automatically generate quart
<http://us.metamath.org/mpeuni/quart.html> proofs for other fields,
would we want to store each of them separately?
--
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+unsubscr...@googlegroups.com.
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/02359165-0501-41a8-8c6b-7411ad76eb64%40googlegroups.com.
