move(order/{boolean_algebra → basic}): move has_compl and trivial instances (#15602)

We move the trivial `pi.has_sdiff`, `pi.has_compl`, and `Prop.has_compl` instances to `order/basic.lean`. The main effect of this is that `rᶜ` for the complement of a relation is now available basically anywhere.

Author: vihdzp

src/order/basic.lean

@@ -29,6 +29,7 @@ classes and allows to transfer order instances.
 
 * `has_sup`: type class for the `⊔` notation
 * `has_inf`: type class for the `⊓` notation
+* `has_compl`: type class for the `ᶜ` notation
 * `densely_ordered`: An order with no gap, i.e. for any two elements `a < b` there exists `c` such
   that `a < c < b`.
 
@@ -446,6 +447,31 @@ linear_order.ext $ λ _ _, iff.rfl
 
 end order_dual
 
+/-! ### `has_compl` -/
+
+/-- Set / lattice complement -/
+@[notation_class] class has_compl (α : Type*) := (compl : α → α)
+
+export has_compl (compl)
+
+postfix `ᶜ`:(max+1) := compl
+
+instance Prop.has_compl : has_compl Prop := ⟨not⟩
+
+instance pi.has_compl {ι : Type u} {α : ι → Type v} [∀ i, has_compl (α i)] :
+  has_compl (Π i, α i) :=
+⟨λ x i, (x i)ᶜ⟩
+
+lemma pi.compl_def {ι : Type u} {α : ι → Type v} [∀ i, has_compl (α i)] (x : Π i, α i) :
+  xᶜ = λ i, (x i)ᶜ := rfl
+
+@[simp]
+lemma pi.compl_apply {ι : Type u} {α : ι → Type v} [∀ i, has_compl (α i)] (x : Π i, α i) (i : ι)  :
+  xᶜ i = (x i)ᶜ := rfl
+
+instance is_irrefl.compl (r) [is_irrefl α r] : is_refl α rᶜ := ⟨@irrefl α r _⟩
+instance is_refl.compl (r) [is_refl α r] : is_irrefl α rᶜ := ⟨λ a, not_not_intro (refl a)⟩
+
 /-! ### Order instances on the function space -/
 
 instance pi.has_le {ι : Type u} {α : ι → Type v} [∀ i, has_le (α i)] : has_le (Π i, α i) :=
@@ -484,6 +510,17 @@ instance pi.partial_order {ι : Type u} {α : ι → Type v} [∀ i, partial_ord
 { le_antisymm := λ f g h1 h2, funext (λ b, (h1 b).antisymm (h2 b)),
   ..pi.preorder }
 
+instance pi.has_sdiff {ι : Type u} {α : ι → Type v} [∀ i, has_sdiff (α i)] :
+  has_sdiff (Π i, α i) :=
+⟨λ x y i, x i \ y i⟩
+
+lemma pi.sdiff_def {ι : Type u} {α : ι → Type v} [∀ i, has_sdiff (α i)] (x y : Π i, α i) :
+  (x \ y) = λ i, x i \ y i := rfl
+
+@[simp]
+lemma pi.sdiff_apply {ι : Type u} {α : ι → Type v} [∀ i, has_sdiff (α i)] (x y : Π i, α i) (i : ι) :
+  (x \ y) i = x i \ y i := rfl
+
 /-! ### `min`/`max` recursors -/
 
 section min_max_rec

src/order/boolean_algebra.lean

@@ -26,7 +26,6 @@ intervals.)
 
 ## Main declarations
 
-* `has_compl`: a type class for the complement operator
 * `generalized_boolean_algebra`: a type class for generalized Boolean algebras
 * `boolean_algebra`: a type class for Boolean algebras.
 * `Prop.boolean_algebra`: the Boolean algebra instance on `Prop`
@@ -42,11 +41,6 @@ complement operator `a \ b` for all `a`, `b`. Instead, the postulates there amou
 that for all `a, b : α` where `a ≤ b`, the equations `x ⊔ a = b` and `x ⊓ a = ⊥` have a solution
 `x`. `disjoint.sdiff_unique` proves that this `x` is in fact `b \ a`.
 
-## Notations
-
-* `xᶜ` is notation for `compl x`
-* `x \ y` is notation for `sdiff x y`.
-
 ## References
 
 * <https://en.wikipedia.org/wiki/Boolean_algebra_(structure)#Generalizations>
@@ -586,14 +580,6 @@ end generalized_boolean_algebra
 ### Boolean algebras
 -/
 
-
-/-- Set / lattice complement -/
-@[notation_class] class has_compl (α : Type*) := (compl : α → α)
-
-export has_compl (compl)
-
-postfix `ᶜ`:(max+1) := compl
-
 /-- A Boolean algebra is a bounded distributive lattice with a complement operator `ᶜ` such that
 `x ⊓ xᶜ = ⊥` and `x ⊔ xᶜ = ⊤`. For convenience, it must also provide a set difference operation `\`
 satisfying `x \ y = x ⊓ yᶜ`.
@@ -773,37 +759,12 @@ by rw [sdiff_eq, compl_inf, compl_compl]
 end boolean_algebra
 
 instance Prop.boolean_algebra : boolean_algebra Prop :=
-{ compl := not,
-  inf_compl_le_bot := λ p ⟨Hp, Hpc⟩, Hpc Hp,
+{ inf_compl_le_bot := λ p ⟨Hp, Hpc⟩, Hpc Hp,
   top_le_sup_compl := λ p H, classical.em p,
+  .. Prop.has_compl,
   .. Prop.distrib_lattice,
   .. Prop.bounded_order }
 
-instance pi.has_sdiff {ι : Type u} {α : ι → Type v} [∀ i, has_sdiff (α i)] :
-  has_sdiff (Π i, α i) :=
-⟨λ x y i, x i \ y i⟩
-
-lemma pi.sdiff_def {ι : Type u} {α : ι → Type v} [∀ i, has_sdiff (α i)] (x y : Π i, α i) :
-  (x \ y) = λ i, x i \ y i := rfl
-
-@[simp]
-lemma pi.sdiff_apply {ι : Type u} {α : ι → Type v} [∀ i, has_sdiff (α i)] (x y : Π i, α i) (i : ι) :
-  (x \ y) i = x i \ y i := rfl
-
-instance pi.has_compl {ι : Type u} {α : ι → Type v} [∀ i, has_compl (α i)] :
-  has_compl (Π i, α i) :=
-⟨λ x i, (x i)ᶜ⟩
-
-lemma pi.compl_def {ι : Type u} {α : ι → Type v} [∀ i, has_compl (α i)] (x : Π i, α i) :
-  xᶜ = λ i, (x i)ᶜ := rfl
-
-instance is_irrefl.compl (r) [is_irrefl α r] : is_refl α rᶜ := ⟨@irrefl α r _⟩
-instance is_refl.compl (r) [is_refl α r] : is_irrefl α rᶜ := ⟨λ a, not_not_intro (refl a)⟩
-
-@[simp]
-lemma pi.compl_apply {ι : Type u} {α : ι → Type v} [∀ i, has_compl (α i)] (x : Π i, α i) (i : ι)  :
-  xᶜ i = (x i)ᶜ := rfl
-
 instance pi.boolean_algebra {ι : Type u} {α : ι → Type v} [∀ i, boolean_algebra (α i)] :
   boolean_algebra (Π i, α i) :=
 { sdiff_eq := λ x y, funext $ λ i, sdiff_eq,