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.
Last updated: Jul 15 2022 at 23:21 UTC