I would've thought that any proof method would prove such result trivially. Yet it's not the case
Many proof methods don't deal with schematic variables very well. Do you have a theorem that you did not instantiate fully?
I did use an intro rule I made to prove some function is polynomial saying if the function can write as ax+b then it is polynomial and I'm using it in this example. So here I expect it to try to express automatically the example as ax+b
Can you share the full theory? That might show something interesting.
I first thought that this might be a type issue, but indeed
auto fails on this even on types where this should hold. If you use
(auto simp: algebra_simps), then it works though.
Commutativity and associativity are not used by default.
Bilel Ghorbel has marked this topic as resolved.
forgot to mark it as resolved.
The solution of @Fabian Huch works perfectly. I tried "try0" and sledgehammer. None of those would indicate that one should use algebra_simps.
That's not surprising. "sledgehammer" does not know that
algebra_simps is something special; it can often find the right rules anyway, but for more complicated goals that involve lots of rewriting, probably not.
And "try0" only calls other methods like
blast etc. which only use the rules that you give to them (plus whatever is in the claset/simpset). They don't try to find other rules that you could potentially have used.
Last updated: Aug 13 2022 at 06:26 UTC