I would've thought that any proof method would prove such result trivially. Yet it's not the case

image.png

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 a*x+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 a*x+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.

Thank you

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: Sep 25 2022 at 23:25 UTC