ac_refl for and

Stream: general

[Alexander Bentkamp]

Hello everybody! Why does ac_refl not work for and?

example (a b : Prop) : (a ∧ b) = (b ∧ a) := by ac_refl -- ac_refl failed
example (a b c d : Prop) : (a ∧ b ∧ d ∧ c) = (c ∧ b ∧ d ∧ a) := by ac_refl -- ac_refl failed

Or is there some other tactic that can do this purely propositional reasoning?

[Patrick Massot]

tauto (or maybe ext ; toto to fight the weird equal sign) should work

[Alex J. Best]

Patrick is right of course that tauto seems like the right choice for this, but I was curious so I did some more digging:
ac_refl uses the is_commutative and is_associative typeclasses which aren't set for and, but if we add those it seems to work

import data.nat.basic

instance : is_commutative Prop ((∧) : Prop → Prop → Prop) := inf_is_commutative
instance : is_associative Prop ((∧) : Prop → Prop → Prop) := inf_is_associative

example (a b : Prop) : (a ∧ b) = (b ∧ a) := by ac_refl
example (a b c d : Prop) : (a ∧ b ∧ d ∧ c) = (c ∧ b ∧ d ∧ a) := by ac_refl

This also suggests a different fix, which is just to state the theorems using lattice operations so that typeclasses don't get confused e.g:

example (a b : Prop) : (a ⊓ b) = (b ⊓ a) := by ac_refl

[Alexander Bentkamp]

Haha, thanks for investigating! I'll stickt to ∧, though :)