>In all fairness, it's pretty hard to understand what's going on in the videos, but it looks like your tactics use a lot of intermediate variables in the process (which get eliminated in the end, I guess). I think any intermediate variables can be avoided whatsoever.
You are right. 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 also think that intermediate variables can be avoided. But this depends on personal preferences and tools used. For example, I cannot work with very long statements containing a lot of parenthesis. That’s why I prefer to use intermediate variables. Also, the special naming convention helps to improve performance a bit. Tactics can easily parse a variable name to get required information about that variable’s value instead of analyzing the value itself. > Also I was expecting a lot less manual interaction for comparing two polynomials, but I probably don't understand some details. I think it is possible to make a full automation for such types of proofs. Maybe I will do it in some time. Thanks for the transformations.js script. I will review it. - Igor On Monday, January 15, 2024 at 3:40:48 PM UTC+1 savask wrote: > > Here are a few videos which show the automation I used to prove some > parts of 3cubes (all videos are speechless) > > That's impressive! > > In all fairness, it's pretty hard to understand what's going on in the > videos, but it looks like your tactics use a lot of intermediate variables > in the process (which get eliminated in the end, I guess). I think any > intermediate variables can be avoided whatsoever. Also I was expecting a > lot less manual interaction for comparing two polynomials, but I probably > don't understand some details. > > You might know about this already, but mmj2 also has some macros, see > https://github.com/digama0/mmj2/blob/master/mmj2jar/macros/transformations.js > Maybe this can serve as inspiration for future work. > -- 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/294a3e7c-81ee-4956-8410-3a3370616270n%40googlegroups.com.
