On Fri, 9 Aug 2019 09:46:48 -0700 (PDT), Noam Tene <noam.t...@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 -- 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/E1hwBa0-0001Hf-0B%40rmmprod07.runbox.
