Jason Hu (Sep 01 2022 at 19:25): Jason Hu (Sep 01 2022 at 19:25):Hi, I am wondering if there is a decision procedure for deciding whether two expressions from the same commutative monoid are equal? in a sense, it is also a permutation decision procedure. if not, how do I write such procedure?
Manuel Eberl (Sep 01 2022 at 20:03):What is your setting here? Are you using a typeclass like comm_monoid_mult or are you in HOL-Algebra?
Manuel Eberl (Sep 01 2022 at 20:04):In either case, isn't this decidable simply be adding the ac rules (associativity and commutativity) and the neutral element rules to the simp set and running the simplifier?
Jason Hu (Sep 02 2022 at 01:28):is that this easy? the simplifier can solve this?
Mathias Fleury (Sep 02 2022 at 07:26):yes: the simplifer (with AC) will reorder terms in canonical form (getting a + b + c + ... where a is larger (for a certain order) than b, itself larger than c and so one). So something like simp add: ac_simps or similar should work
Manuel Eberl (Sep 02 2022 at 16:49):Or just simp add: algebra_simps.
Last updated: Apr 20 2024 at 01:05 UTC