Bilel Ghorbel (Nov 30 2021 at 11:17): Bilel Ghorbel (Nov 30 2021 at 11:17):I would've thought that any proof method would prove such result trivially. Yet it's not the case
image.png
Lukas Stevens (Nov 30 2021 at 11:32):Many proof methods don't deal with schematic variables very well. Do you have a theorem that you did not instantiate fully?
Bilel Ghorbel (Nov 30 2021 at 13:02):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
Alex Weisberger (Nov 30 2021 at 14:14):Can you share the full theory? That might show something interesting.
Fabian Huch (Nov 30 2021 at 15:26):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.
Manuel Eberl (Dec 01 2021 at 18:39):Commutativity and associativity are not used by default.
Notification Bot (Dec 08 2021 at 11:13):Bilel Ghorbel has marked this topic as resolved.
Bilel Ghorbel (Dec 08 2021 at 11:14):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.
Thank you
Manuel Eberl (Dec 08 2021 at 11:21):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 auto, simp, force, 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: Nov 13 2025 at 08:29 UTC