> The first line is the proved statement, and the lines after it are the proof. If you insert it in metamath-lamp line by line (marking A e. CC and B e. CC as hypotheses), it would successfully unify.
The first line doesn’t look like a full expansion, because A gets multiplied by a sum of other variables. The right part of the last line seems to be the full expansion. But when I inserted all the lines to metamath-lamp <https://expln.github.io/lamp/dev/index.html?editorState=eyJzcmNzIjpbeyJ0eXAiOiJXZWIiLCJmaWxlTmFtZSI6IiIsInVybCI6Imh0dHBzOi8vdXMubWV0YW1hdGgub3JnL21ldGFtYXRoL3NldC5tbSIsInJlYWRJbnN0ciI6IlJlYWRBbGwiLCJsYWJlbCI6IiIsInJlc2V0TmVzdGluZ0xldmVsIjp0cnVlLCJhbGxMYWJlbHMiOltdfV0sImRlc2NyIjoiIiwidmFyc1RleHQiOiIiLCJkaXNqVGV4dCI6IiIsInN0bXRzIjpbeyJsYWJlbCI6InFlZC4xIiwidHlwIjoiZSIsImlzR29hbCI6ZmFsc2UsImlzQmttIjpmYWxzZSwiY29udCI6InwtIEEgZS4gQ0MiLCJqc3RmVGV4dCI6IiJ9LHsibGFiZWwiOiJxZWQuMiIsInR5cCI6ImUiLCJpc0dvYWwiOmZhbHNlLCJpc0JrbSI6ZmFsc2UsImNvbnQiOiJ8LSBCIGUuIENDIiwianN0ZlRleHQiOiIifSx7ImxhYmVsIjoiMSIsInR5cCI6InAiLCJpc0dvYWwiOmZhbHNlLCJpc0JrbSI6ZmFsc2UsImNvbnQiOiJ8LSAoIEEgeC4gQSApIGUuIENDIiwianN0ZlRleHQiOiJxZWQuMSBxZWQuMSA6IG11bGNsaSJ9LHsibGFiZWwiOiIyIiwidHlwIjoicCIsImlzR29hbCI6ZmFsc2UsImlzQmttIjpmYWxzZSwiY29udCI6InwtICggQiB4LiBBICkgZS4gQ0MiLCJqc3RmVGV4dCI6InFlZC4yIHFlZC4xIDogbXVsY2xpIn0seyJsYWJlbCI6IjMiLCJ0eXAiOiJwIiwiaXNHb2FsIjpmYWxzZSwiaXNCa20iOmZhbHNlLCJjb250IjoifC0gKCAoIEEgeC4gQSApICsgKCBCIHguIEEgKSApIGUuIENDIiwianN0ZlRleHQiOiIxIDIgOiBhZGRjbGkifSx7ImxhYmVsIjoiNCIsInR5cCI6InAiLCJpc0dvYWwiOmZhbHNlLCJpc0JrbSI6ZmFsc2UsImNvbnQiOiJ8LSAoIEEgeC4gQiApIGUuIENDIiwianN0ZlRleHQiOiJxZWQuMSBxZWQuMiA6IG11bGNsaSJ9LHsibGFiZWwiOiI1IiwidHlwIjoicCIsImlzR29hbCI6ZmFsc2UsImlzQmttIjpmYWxzZSwiY29udCI6InwtICggQiB4LiBCICkgZS4gQ0MiLCJqc3RmVGV4dCI6InFlZC4yIHFlZC4yIDogbXVsY2xpIn0seyJsYWJlbCI6IjYiLCJ0eXAiOiJwIiwiaXNHb2FsIjpmYWxzZSwiaXNCa20iOmZhbHNlLCJjb250IjoifC0gKCAoIEEgeC4gQiApICsgKCBCIHguIEIgKSApIGUuIENDIiwianN0ZlRleHQiOiI0IDUgOiBhZGRjbGkifSx7ImxhYmVsIjoiNyIsInR5cCI6InAiLCJpc0dvYWwiOmZhbHNlLCJpc0JrbSI6ZmFsc2UsImNvbnQiOiJ8LSAoICggKCAoIEEgeC4gQSApICsgKCBCIHguIEEgKSApICsgKCAoIEEgeC4gQiApICsgKCBCIHguIEIgKSApICkgeC4gQSApID0gKCAoICggKCBBIHguIEEgKSArICggQiB4LiBBICkgKSB4LiBBICkgKyAoICggKCBBIHguIEIgKSArICggQiB4LiBCICkgKSB4LiBBICkgKSIsImpzdGZUZXh0IjoiMyA2IHFlZC4xIDogYWRkZGlyaSJ9LHsibGFiZWwiOiI4IiwidHlwIjoicCIsImlzR29hbCI6ZmFsc2UsImlzQmttIjpmYWxzZSwiY29udCI6InwtICggKCAoIEEgeC4gQSApICsgKCBCIHguIEEgKSApIHguIEEgKSA9ICggKCAoIEEgeC4gQSApIHguIEEgKSArICggKCBCIHguIEEgKSB4LiBBICkgKSIsImpzdGZUZXh0IjoiMSAyIHFlZC4xIDogYWRkZGlyaSJ9LHsibGFiZWwiOiI5IiwidHlwIjoicCIsImlzR29hbCI6ZmFsc2UsImlzQmttIjpmYWxzZSwiY29udCI6InwtICggKCAoIEEgeC4gQiApICsgKCBCIHguIEIgKSApIHguIEEgKSA9ICggKCAoIEEgeC4gQiApIHguIEEgKSArICggKCBCIHguIEIgKSB4LiBBICkgKSIsImpzdGZUZXh0IjoiNCA1IHFlZC4xIDogYWRkZGlyaSJ9LHsibGFiZWwiOiIxMCIsInR5cCI6InAiLCJpc0dvYWwiOmZhbHNlLCJpc0JrbSI6ZmFsc2UsImNvbnQiOiJ8LSAoICggKCAoIEEgeC4gQSApICsgKCBCIHguIEEgKSApIHguIEEgKSArICggKCAoIEEgeC4gQiApICsgKCBCIHguIEIgKSApIHguIEEgKSApID0gKCAoICggKCBBIHguIEEgKSB4LiBBICkgKyAoICggQiB4LiBBICkgeC4gQSApICkgKyAoICggKCBBIHguIEIgKSArICggQiB4LiBCICkgKSB4LiBBICkgKSIsImpzdGZUZXh0IjoiOCA6IG92ZXExaSJ9LHsibGFiZWwiOiIxMSIsInR5cCI6InAiLCJpc0dvYWwiOmZhbHNlLCJpc0JrbSI6ZmFsc2UsImNvbnQiOiJ8LSAoICggKCAoIEEgeC4gQSApIHguIEEgKSArICggKCBCIHguIEEgKSB4LiBBICkgKSArICggKCAoIEEgeC4gQiApICsgKCBCIHguIEIgKSApIHguIEEgKSApID0gKCAoICggKCBBIHguIEEgKSB4LiBBICkgKyAoICggQiB4LiBBICkgeC4gQSApICkgKyAoICggKCBBIHguIEIgKSB4LiBBICkgKyAoICggQiB4LiBCICkgeC4gQSApICkgKSIsImpzdGZUZXh0IjoiOSA6IG92ZXEyaSJ9LHsibGFiZWwiOiIxMiIsInR5cCI6InAiLCJpc0dvYWwiOmZhbHNlLCJpc0JrbSI6ZmFsc2UsImNvbnQiOiJ8LSAoICggKCAoIEEgeC4gQSApICsgKCBCIHguIEEgKSApICsgKCAoIEEgeC4gQiApICsgKCBCIHguIEIgKSApICkgeC4gQSApID0gKCAoICggKCBBIHguIEEgKSB4LiBBICkgKyAoICggQiB4LiBBICkgeC4gQSApICkgKyAoICggKCBBIHguIEIgKSB4LiBBICkgKyAoICggQiB4LiBCICkgeC4gQSApICkgKSIsImpzdGZUZXh0IjoiNyAxMCAxMSA6IDNlcXRyaSJ9LHsibGFiZWwiOiJxZWQiLCJ0eXAiOiJwIiwiaXNHb2FsIjp0cnVlLCJpc0JrbSI6ZmFsc2UsImNvbnQiOiJ8LSAoICggKCBBICsgQiApIHguICggQSArIEIgKSApIHguIEEgKSA9ICggKCAoICggQSB4LiBBICkgKyAoIEIgeC4gQSApICkgKyAoICggQSB4LiBCICkgKyAoIEIgeC4gQiApICkgKSB4LiBBICkiLCJqc3RmVGV4dCI6IiJ9XX0=> (this link leads to my attempt to unify your proof), there was one not unified step, basically the first line in your proof was not unified. It could be a bug in metamath-lamp (I need more time to understand what’s going on). But also it looks like some steps are missing in your proof. For example, I would expect a line which proves “( A + B ) e. CC”, but it is missing in your proof. Anyway, I understand the idea of your approach, and it looks very reasonable. > Of course your tactics are superior, but at least mine didn't require any intermediate variables or manual input For this example, my tactics require only one intermediate variable and almost no manual input either. Here is a demo - https://drive.google.com/file/d/1ihCwiCyW0Ha_1qK6AY8xpa_BqsKlb51r/view?usp=drive_link Intermediate variables become necessary for my tactics when there are also constants, for example, ( A x. ( ( 2 + 1 ) x. B ) ). If you try to apply the same tactic as shown on the demo above, you’ll end up with something like … ( 2 x. B ) … + … ( 1 x. B ) … , which is obviously not the desired result. Anyway, I am not insisting on any of the approaches. This is just what I came to during work on proof for 3cubes. However, I found usage of intermediate variables very convenient. Here is why I like this approach. The demos I showed run very smooth because I prepared by repeating those proofs several times before recording. But even there I made a few mistakes. When I was working on proofs for 3cubes, I made a lot more mistakes and encountered a lot of errors (due to both my inexperience and bugs in tactics). But thanks to usage of intermediate variables, which made all the statements short and readable, I was able to resolve errors sufficiently fast. So, intermediate variables may look awkward and negatively impact the quality of the resulting proof, but they may save a bit of mental health for such beginners as me :) > I hope the usage of variables doesn't have a negative impact on the proof's length. I don’t think the variables negatively impact the proof’s length. The tactics itself may produce long proofs. > you will quickly notice that quite often the tactic simply tries to apply some theorem from a carefully chosen list when it is possible or when the expression matches some pattern. That seems to be enough to perform basic arithmetic (prove stuff like ; 1 2 + ; 3 9 = ; 5 1). I noticed that. The bottom-up prover in metamath-lamp (this is the core of all my tactics) also uses a similar approach. However, from what I see, transformations.js uses trickier algorithms. Comparing to it my prover is more straightforward. I am not sure if my prover will be able to prove statements like ; 1 2 + ; 3 9 = ; 5 1, but I think it should be able (probably after some revision). - Igor On Tuesday, January 16, 2024 at 4:08:56 PM UTC+1 savask wrote: > > Intermediate variables are used to make the statements more readable. > Also a special naming convention for the variables is used, so that tactics > can understand what to do with each variable. > > I hope the usage of variables doesn't have a negative impact on the > proof's length. > > > I think it is possible to make a full automation for such types of > proofs. Maybe I will do it in some time. > > That would be great. Say, if you have two polynomials f(A, B) and g(A, B) > and you want to prove |- f(A, B) = g(A, B), a tactic should be able to do > that, and leave some unproved goals of the form |- A e. CC and |- B e. CC. > > I tried making a rudimentary polynomial-expansion tactic in Haskell, for > example to expand ( A + B ) x. ( A + B ) x. A it would output: > > ghci> let (exp, pf) = expand ((va .+. vb) .*. (va .+. vb) .*. va) > ghci> mapM_ print $ clean pf > ( ( ( A + B ) x. ( A + B ) ) x. A ) = ( ( ( ( A x. A ) + ( B x. A ) ) + ( > ( A x. B ) + ( B x. B ) ) ) x. A ) > A e. CC > ( A x. A ) e. CC > B e. CC > ( B x. A ) e. CC > ( ( A x. A ) + ( B x. A ) ) e. CC > ( A x. B ) e. CC > ( B x. B ) e. CC > ( ( A x. B ) + ( B x. B ) ) e. CC > ( ( ( ( A x. A ) + ( B x. A ) ) + ( ( A x. B ) + ( B x. B ) ) ) x. A ) = ( > ( ( ( A x. A ) + ( B x. A ) ) x. A ) + ( ( ( A x. B ) + ( B x. B ) ) x. A ) > ) > ( ( ( A x. A ) + ( B x. A ) ) x. A ) = ( ( ( A x. A ) x. A ) + ( ( B x. A > ) x. A ) ) > ( ( ( A x. B ) + ( B x. B ) ) x. A ) = ( ( ( A x. B ) x. A ) + ( ( B x. B > ) x. A ) ) > ( ( ( ( A x. A ) + ( B x. A ) ) x. A ) + ( ( ( A x. B ) + ( B x. B ) ) x. > A ) ) = ( ( ( ( A x. A ) x. A ) + ( ( B x. A ) x. A ) ) + ( ( ( A x. B ) + > ( B x. B ) ) x. A ) ) > ( ( ( ( A x. A ) x. A ) + ( ( B x. A ) x. A ) ) + ( ( ( A x. B ) + ( B x. > B ) ) x. A ) ) = ( ( ( ( A x. A ) x. A ) + ( ( B x. A ) x. A ) ) + ( ( ( A > x. B ) x. A ) + ( ( B x. B ) x. A ) ) ) > ( ( ( ( A x. A ) + ( B x. A ) ) + ( ( A x. B ) + ( B x. B ) ) ) x. A ) = ( > ( ( ( A x. A ) x. A ) + ( ( B x. A ) x. A ) ) + ( ( ( A x. B ) x. A ) + ( ( > B x. B ) x. A ) ) ) > > The first line is the proved statement, and the lines after it are the > proof. If you insert it in metamath-lamp line by line (marking A e. CC and > B e. CC as hypotheses), it would successfully unify. Of course your tactics > are superior, but at least mine didn't require any intermediate variables > or manual input :-) > > > Thanks for the transformations.js script. I will review it. > > It would be nice to hear what Mario has to say about it, but you will > quickly notice that quite often the tactic simply tries to apply some > theorem from a carefully chosen list when it is possible or when the > expression matches some pattern. That seems to be enough to perform basic > arithmetic (prove stuff like ; 1 2 + ; 3 9 = ; 5 1). > -- 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 [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/7ae12db4-a02b-4649-8dd2-f73029f4bd2an%40googlegroups.com.
