reordering modulo AC

Stream: lean4

[Alexander Bentkamp]

Is there a Lean4 tactic that can reorder modulo AC? Simp doesn't seem to do it:

@[simp] theorem and_comm (a b : Prop)  : a ∧ b = b ∧ a := sorry

@[simp] theorem and_assoc (a b c : Prop)  : a ∧ (b ∧ c) = (a ∧ b) ∧ c := sorry

example (a b c d : Prop) : a ∧ b ∧ c ∧ d = d ∧ c ∧ b ∧ a := by simp
/-
unsolved goals
a b c d : Prop
⊢ a ∧ b ∧ c ∧ c ∧ b ∧ a
-/

Or with an operator that simp does not know:

constant t : Nat → Nat → Nat

infixl :80 " # " => t

@[simp] theorem hash_comm (a b : Nat)  : a # b = b # a := sorry

@[simp] theorem hash_assoc (a b c : Nat)  : a # (b # c) = (a # b) # c := sorry

example (a b c d : Nat) : a # b # c # d = d # c # b # a := by simp
/- doesn't terminate -/

[Kevin Buzzard]

What happens if you make hash_assoc.symm the simp lemma instead? I think this was the way around that it was when add_assoc was a simp lemma

[Gabriel Ebner]

You also need a # (b # c) = b # (a # c) (not 100% sure about the parens).

[Alexander Bentkamp]

Oh, wow, thanks!

[Alexander Bentkamp]

@Gabriel Ebner On another thread you wrote:

Medium-long term there is also AC-simplification in development.

So then simp actually currently doesn't support what I have been trying to do above? I have some examples now where it fails...

[Karl Palmskog]

if anyone wants to implement modulo AC tactics for Lean, please feel free to take inspiration from Coq's AAC tactics, which recently got some enhancements for idempotent operators: https://github.com/coq-community/aac-tactics

[Daniel Fabian]

fyi: https://github.com/leanprover/lean4/pull/1032