Stream: Beginner Questions

Topic: ✔ Dealing with trivial arithmetic

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Alex Weisberger (Nov 30 2021 at 14:14):

Can you share the full theory? That might show something interesting.

view this post on Zulip 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.

view this post on Zulip Manuel Eberl (Dec 01 2021 at 18:39):

Commutativity and associativity are not used by default.

view this post on Zulip Notification Bot (Dec 08 2021 at 11:13):

Bilel Ghorbel has marked this topic as resolved.

view this post on Zulip 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

view this post on Zulip 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: Sep 25 2022 at 23:25 UTC