From a219fbf7fdb227c6909a8eef7664d7b6af27464a Mon Sep 17 00:00:00 2001
From: Jeremy Tan Jie Rui <reddeloostw@gmail.com>
Date: Sun, 15 Sep 2024 08:25:57 +0000
Subject: [PATCH] refactor: `Logic.OpClass` (#16748)

Put `IsSymmOp`, `LeftCommutative` and `RightCommutative` under a new file `Logic.OpClass`. This has the effect of completely deprecating `Init.Algebra.Classes`.

All remaining undeprecated `Init` code now consists of attributes and relational definitions in `Init.Logic`. One instance that is not needed anywhere in mathlib and that would cause a dependency of `Logic.OpClass` on `Order.Defs` has been removed.
---
 Mathlib.lean                      |  1 +
 Mathlib/Data/List/Basic.lean      |  1 +
 Mathlib/Data/List/Zip.lean        |  1 -
 Mathlib/Init/Algebra/Classes.lean | 18 ----------
 Mathlib/Init/Logic.lean           | 28 ++-------------
 Mathlib/Logic/Function/Basic.lean |  2 +-
 Mathlib/Logic/OpClass.lean        | 60 +++++++++++++++++++++++++++++++
 Mathlib/Order/MinMax.lean         |  1 +
 8 files changed, 66 insertions(+), 46 deletions(-)
 create mode 100644 Mathlib/Logic/OpClass.lean

diff --git a/Mathlib.lean b/Mathlib.lean
index c83a7532fc074..e5889e2925b78 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -3135,6 +3135,7 @@ import Mathlib.Logic.Lemmas
 import Mathlib.Logic.Nonempty
 import Mathlib.Logic.Nontrivial.Basic
 import Mathlib.Logic.Nontrivial.Defs
+import Mathlib.Logic.OpClass
 import Mathlib.Logic.Pairwise
 import Mathlib.Logic.Relation
 import Mathlib.Logic.Relator
diff --git a/Mathlib/Data/List/Basic.lean b/Mathlib/Data/List/Basic.lean
index 59cf323bc5e1c..d80f05bbc19cd 100644
--- a/Mathlib/Data/List/Basic.lean
+++ b/Mathlib/Data/List/Basic.lean
@@ -7,6 +7,7 @@ import Mathlib.Data.Nat.Defs
 import Mathlib.Data.Option.Basic
 import Mathlib.Data.List.Defs
 import Mathlib.Data.List.Monad
+import Mathlib.Logic.OpClass
 import Mathlib.Logic.Unique
 import Mathlib.Order.Basic
 import Mathlib.Tactic.Common
diff --git a/Mathlib/Data/List/Zip.lean b/Mathlib/Data/List/Zip.lean
index e8139e99ff8db..cb8b7daa47501 100644
--- a/Mathlib/Data/List/Zip.lean
+++ b/Mathlib/Data/List/Zip.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Kenny Lau
 -/
 import Mathlib.Data.List.Forall2
-import Mathlib.Init.Algebra.Classes
 
 /-!
 # zip & unzip
diff --git a/Mathlib/Init/Algebra/Classes.lean b/Mathlib/Init/Algebra/Classes.lean
index 9155864aa6a8c..98fbccbde3cf3 100644
--- a/Mathlib/Init/Algebra/Classes.lean
+++ b/Mathlib/Init/Algebra/Classes.lean
@@ -13,8 +13,6 @@ The files in `Mathlib/Init` are leftovers from the port from Mathlib3.
 We intend to move all the content of these files out into the main `Mathlib` directory structure.
 Contributions assisting with this are appreciated.
 
-(Jeremy Tan: The only non-deprecated thing in this file now is `IsSymmOp`)
-
 # Unbundled algebra classes
 
 These classes were part of an incomplete refactor described
@@ -29,22 +27,6 @@ universe u v
 
 variable {α : Sort u} {β : Sort v}
 
-/-- `IsSymmOp op` where `op : α → α → β` says that `op` is a symmetric operation,
-i.e. `op a b = op b a`.
-It is the natural generalisation of `Std.Commutative` (`β = α`) and `IsSymm` (`β = Prop`). -/
-class IsSymmOp (op : α → α → β) : Prop where
-  /-- A symmetric operation satisfies `op a b = op b a`. -/
-  symm_op : ∀ a b, op a b = op b a
-
-instance (priority := 100) isSymmOp_of_isCommutative (α : Sort u) (op : α → α → α)
-    [Std.Commutative op] : IsSymmOp op where symm_op := Std.Commutative.comm
-
-instance (priority := 100) isSymmOp_of_isSymm (α : Sort u) (op : α → α → Prop) [IsSymm α op] :
-    IsSymmOp op where symm_op a b := propext <| Iff.intro (IsSymm.symm a b) (IsSymm.symm b a)
-
-theorem IsSymmOp.flip_eq (op : α → α → β) [IsSymmOp op] : flip op = op :=
-  funext fun a ↦ funext fun b ↦ (IsSymmOp.symm_op a b).symm
-
 @[deprecated (since := "2024-09-11")]
 class IsLeftCancel (α : Sort u) (op : α → α → α) : Prop where
   left_cancel : ∀ a b c, op a b = op a c → b = c
diff --git a/Mathlib/Init/Logic.lean b/Mathlib/Init/Logic.lean
index cfc9e1a09488c..8afa61d3f654d 100644
--- a/Mathlib/Init/Logic.lean
+++ b/Mathlib/Init/Logic.lean
@@ -72,6 +72,8 @@ theorem InvImage.irreflexive (f : α → β) (h : Irreflexive r) : Irreflexive (
 
 end Relation
 
+-- Everything below this line is deprecated
+
 section Binary
 
 variable {α : Type u} {β : Type v} (f : α → α → α) (inv : α → α) (one : α)
@@ -106,34 +108,8 @@ def LeftDistributive  := ∀ a b c, a * (b + c) = a * b + a * c
 @[deprecated (since := "2024-09-03")] -- unused in Mathlib
 def RightDistributive := ∀ a b c, (a + b) * c = a * c + b * c
 
-/-- `LeftCommutative op` where `op : α → β → β` says that `op` is a left-commutative operation,
-i.e. `op a₁ (op a₂ b) = op a₂ (op a₁ b)`. -/
-class LeftCommutative (op : α → β → β) : Prop where
-  /-- A left-commutative operation satisfies `op a₁ (op a₂ b) = op a₂ (op a₁ b)`. -/
-  left_comm : (a₁ a₂ : α) → (b : β) → op a₁ (op a₂ b) = op a₂ (op a₁ b)
-
-/-- `RightCommutative op` where `op : β → α → β` says that `op` is a right-commutative operation,
-i.e. `op (op b a₁) a₂ = op (op b a₂) a₁`. -/
-class RightCommutative (op : β → α → β) : Prop where
-  /-- A right-commutative operation satisfies `op (op b a₁) a₂ = op (op b a₂) a₁`. -/
-  right_comm : (b : β) → (a₁ a₂ : α) → op (op b a₁) a₂ = op (op b a₂) a₁
-
-instance {f : α → β → β} [h : LeftCommutative f] : RightCommutative (fun x y ↦ f y x) :=
-  ⟨fun _ _ _ ↦ (h.left_comm _ _ _).symm⟩
-
-instance {f : β → α → β} [h : RightCommutative f] : LeftCommutative (fun x y ↦ f y x) :=
-  ⟨fun _ _ _ ↦ (h.right_comm _ _ _).symm⟩
-
-instance {f : α → α → α} [hc : Std.Commutative f] [ha : Std.Associative f] : LeftCommutative f :=
-  ⟨fun a b c ↦ by rw [← ha.assoc, hc.comm a, ha.assoc]⟩
-
-instance {f : α → α → α} [hc : Std.Commutative f] [ha : Std.Associative f] : RightCommutative f :=
-  ⟨fun a b c ↦ by rw [ha.assoc, hc.comm b, ha.assoc]⟩
-
 end Binary
 
--- Everything below this line is deprecated
-
 @[deprecated (since := "2024-09-03")] alias not_of_eq_false := of_eq_false
 @[deprecated (since := "2024-09-03")] -- unused in Mathlib
 theorem cast_proof_irrel {β : Sort u} (h₁ h₂ : α = β) (a : α) : cast h₁ a = cast h₂ a := rfl
diff --git a/Mathlib/Logic/Function/Basic.lean b/Mathlib/Logic/Function/Basic.lean
index eb302a3362015..a568026c23889 100644
--- a/Mathlib/Logic/Function/Basic.lean
+++ b/Mathlib/Logic/Function/Basic.lean
@@ -3,8 +3,8 @@ Copyright (c) 2016 Johannes Hölzl. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Mario Carneiro
 -/
-import Mathlib.Init.Logic
 import Mathlib.Data.Set.Defs
+import Mathlib.Init.Logic
 import Mathlib.Logic.Basic
 import Mathlib.Logic.ExistsUnique
 import Mathlib.Logic.Nonempty
diff --git a/Mathlib/Logic/OpClass.lean b/Mathlib/Logic/OpClass.lean
new file mode 100644
index 0000000000000..2f65fe0b3d85e
--- /dev/null
+++ b/Mathlib/Logic/OpClass.lean
@@ -0,0 +1,60 @@
+/-
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+
+/-!
+# Typeclasses for commuting heterogeneous operations
+
+The three classes in this file are for two-argument functions where one input is of type `α`,
+the output is of type `β` and the other input is of type `α` or `β`.
+They express the property that permuting arguments of type `α` does not change the result.
+
+## Main definitions
+
+* `IsSymmOp`: for `op : α → α → β`, `op a b = op b a`.
+* `LeftCommutative`: for `op : α → β → β`, `op a₁ (op a₂ b) = op a₂ (op a₁ b)`.
+* `RightCommutative`: for `op : β → α → β`, `op (op b a₁) a₂ = op (op b a₂) a₁`.
+-/
+
+universe u v
+
+variable {α : Sort u} {β : Sort v}
+
+/-- `IsSymmOp op` where `op : α → α → β` says that `op` is a symmetric operation,
+i.e. `op a b = op b a`.
+It is the natural generalisation of `Std.Commutative` (`β = α`) and `IsSymm` (`β = Prop`). -/
+class IsSymmOp (op : α → α → β) : Prop where
+  /-- A symmetric operation satisfies `op a b = op b a`. -/
+  symm_op : ∀ a b, op a b = op b a
+
+/-- `LeftCommutative op` where `op : α → β → β` says that `op` is a left-commutative operation,
+i.e. `op a₁ (op a₂ b) = op a₂ (op a₁ b)`. -/
+class LeftCommutative (op : α → β → β) : Prop where
+  /-- A left-commutative operation satisfies `op a₁ (op a₂ b) = op a₂ (op a₁ b)`. -/
+  left_comm : (a₁ a₂ : α) → (b : β) → op a₁ (op a₂ b) = op a₂ (op a₁ b)
+
+/-- `RightCommutative op` where `op : β → α → β` says that `op` is a right-commutative operation,
+i.e. `op (op b a₁) a₂ = op (op b a₂) a₁`. -/
+class RightCommutative (op : β → α → β) : Prop where
+  /-- A right-commutative operation satisfies `op (op b a₁) a₂ = op (op b a₂) a₁`. -/
+  right_comm : (b : β) → (a₁ a₂ : α) → op (op b a₁) a₂ = op (op b a₂) a₁
+
+instance (priority := 100) isSymmOp_of_isCommutative (α : Sort u) (op : α → α → α)
+    [Std.Commutative op] : IsSymmOp op where symm_op := Std.Commutative.comm
+
+theorem IsSymmOp.flip_eq (op : α → α → β) [IsSymmOp op] : flip op = op :=
+  funext fun a ↦ funext fun b ↦ (IsSymmOp.symm_op a b).symm
+
+instance {f : α → β → β} [h : LeftCommutative f] : RightCommutative (fun x y ↦ f y x) :=
+  ⟨fun _ _ _ ↦ (h.left_comm _ _ _).symm⟩
+
+instance {f : β → α → β} [h : RightCommutative f] : LeftCommutative (fun x y ↦ f y x) :=
+  ⟨fun _ _ _ ↦ (h.right_comm _ _ _).symm⟩
+
+instance {f : α → α → α} [hc : Std.Commutative f] [ha : Std.Associative f] : LeftCommutative f :=
+  ⟨fun a b c ↦ by rw [← ha.assoc, hc.comm a, ha.assoc]⟩
+
+instance {f : α → α → α} [hc : Std.Commutative f] [ha : Std.Associative f] : RightCommutative f :=
+  ⟨fun a b c ↦ by rw [ha.assoc, hc.comm b, ha.assoc]⟩
diff --git a/Mathlib/Order/MinMax.lean b/Mathlib/Order/MinMax.lean
index b59ac2dc8ab3c..6bff790a5da29 100644
--- a/Mathlib/Order/MinMax.lean
+++ b/Mathlib/Order/MinMax.lean
@@ -3,6 +3,7 @@ Copyright (c) 2017 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
+import Mathlib.Logic.OpClass
 import Mathlib.Order.Lattice
 
 /-!