Commit 2024-09-14 09:22 c4edb0ea

View on Github →

refactor: make (Left|Right)Commutative typeclasses (#16751) LeftCommutative and RightCommutative are currently pure definitions, but they are used in other declarations as if they were typeclasses. As they are not actually typeclasses they have to be passed in explicitly, which causes unnecessary repetition and code bloat. This PR makes them typeclasses and adds supporting instances: two converted from the theorems left_comm and right_comm and two others extracted from Data.Multiset.Basic. In #16748 they will be moved with the very structurally similar typeclass IsSymmOp out of Init.Logic to a new file. The shaking of this PR revealed some uses of lemmas deprecated in #16438 but not caught by the linter. We fix these too.

Estimated changes

modified theorem mul_left_comm
modified theorem mul_right_comm
modified theorem List.Perm.foldl_eq
modified theorem List.Perm.foldr_eq
modified theorem Multiset.coe_foldl
modified theorem Multiset.coe_foldr
modified theorem Multiset.coe_foldr_swap
modified def Multiset.foldl
modified theorem Multiset.foldl_add
modified theorem Multiset.foldl_cons
modified theorem Multiset.foldl_induction'
modified theorem Multiset.foldl_induction
modified theorem Multiset.foldl_swap
modified theorem Multiset.foldl_zero
modified def Multiset.foldr
modified theorem Multiset.foldr_add
modified theorem Multiset.foldr_cons
modified theorem Multiset.foldr_induction'
modified theorem Multiset.foldr_induction
modified theorem Multiset.foldr_singleton
modified theorem Multiset.foldr_swap
modified theorem Multiset.foldr_zero
modified theorem Multiset.sub_eq_fold_erase
deleted def LeftCommutative
deleted def RightCommutative
deleted theorem left_comm
deleted theorem right_comm
modified theorem max_left_comm
modified theorem min_left_comm
modified theorem Max.left_comm
modified theorem Max.right_comm
modified theorem max_left_commutative
modified theorem min_left_commutative
modified theorem min_right_comm