Add @[simp] for Bool.or_assoc and Bool.and_assoc

[4e554c4c]

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
  • Reduced the issue to a self-contained, reproducible test case.

Description

Bool.or_assoc and Bool.and_assoc are not marked as @[simp] even though they are defined in Init.SimpLemmas

lean4/src/Init/SimpLemmas.lean

Lines 117 to 120 in a095dab

	theorem Bool.and_assoc (a b c : Bool) : (a && b && c) = (a && (b && c)) := by
	cases a <;> cases b <;> cases c <;> decide
	theorem Bool.or_assoc (a b c : Bool) : (a || b || c) = (a || (b || c)) := by
	cases a <;> cases b <;> cases c <;> decide

This causes a digression in behavior between the simplifier in Lean3 and Lean4.

Versions

version observed: Lean (version 4.0.0-nightly-2023-01-06, commit fedf235cba35, Release)
OS: Linux 6.1.2-arch1-1 GNU/Linux

Additional Information

Related mathport PR: leanprover-community/mathlib4#1404

[gebner]

FWIW, we explicitly removed and_assoc and or_assoc from the simp set in Lean 3. It's only consistent to do the same for Bool.and_assoc and Bool.or_assoc.