> 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/91f2ca0c-9be1-4a25-b6ff-ea9f343ac6f5n%40googlegroups.com.
