chore: use a type synonym instead of an abbrev for Interval (#37508)

Otherwise, there are conflicting instances between `Interval` and its definition `WithBot ...`, creating diamonds: the multiplication is not defined in the same way (on `WithBot`, we have `0 * bot = 0` while on `Interval` we have `0 * bot = bot`), and the `nsmul` fields are also different.

Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>

Author: sgouezel

Mathlib/Algebra/Order/Interval/Basic.lean

@@ -44,6 +44,10 @@ variable [Preorder α] [One α]
 instance : One (NonemptyInterval α) :=
   ⟨NonemptyInterval.pure 1⟩
 
+@[to_additive]
+instance : One (Interval α) :=
+  ⟨(1 : NonemptyInterval α)⟩
+
 namespace NonemptyInterval
 
 @[to_additive (attr := simp) toProd_zero]
@@ -74,9 +78,9 @@ namespace Interval
 theorem pure_one : pure (1 : α) = 1 :=
   rfl
 
-@[to_additive] lemma one_ne_bot : (1 : Interval α) ≠ ⊥ := pure_ne_bot
+@[to_additive (attr := simp)] lemma one_ne_bot : (1 : Interval α) ≠ ⊥ := pure_ne_bot
 
-@[to_additive] lemma bot_ne_one : (⊥ : Interval α) ≠ 1 := bot_ne_pure
+@[to_additive (attr := simp)] lemma bot_ne_one : (⊥ : Interval α) ≠ 1 := bot_ne_pure
 
 end Interval
 
@@ -167,7 +171,7 @@ variable (s t : Interval α)
 theorem bot_mul : ⊥ * t = ⊥ :=
   WithBot.map₂_bot_left _ _
 
-@[to_additive]
+@[to_additive (attr := simp)]
 theorem mul_bot : s * ⊥ = ⊥ :=
   WithBot.map₂_bot_right _ _
 
@@ -219,7 +223,7 @@ namespace NonemptyInterval
 @[to_additive]
 instance commMonoid [CommMonoid α] [Preorder α] [IsOrderedMonoid α] :
     CommMonoid (NonemptyInterval α) :=
-  NonemptyInterval.toProd_injective.commMonoid _ toProd_one toProd_mul toProd_pow
+  fast_instance% NonemptyInterval.toProd_injective.commMonoid _ toProd_one toProd_mul toProd_pow
 
 end NonemptyInterval
 
@@ -235,10 +239,9 @@ instance Interval.mulOneClass [CommMonoid α] [Preorder α] [IsOrderedMonoid α]
 
 @[to_additive]
 instance Interval.commMonoid [CommMonoid α] [Preorder α] [IsOrderedMonoid α] :
-    CommMonoid (Interval α) :=
-  { Interval.mulOneClass with
-    mul_comm := fun _ _ => Option.map₂_comm mul_comm
-    mul_assoc := fun _ _ _ => Option.map₂_assoc mul_assoc }
+    CommMonoid (Interval α) where
+  mul_comm := fun _ _ => Option.map₂_comm mul_comm
+  mul_assoc := fun _ _ _ => Option.map₂_assoc mul_assoc
 
 namespace NonemptyInterval
 
@@ -294,7 +297,7 @@ namespace NonemptyInterval
 
 instance [CommSemiring α] [PartialOrder α] [CanonicallyOrderedAdd α] :
     CommSemiring (NonemptyInterval α) :=
-  NonemptyInterval.toProd_injective.commSemiring _
+  fast_instance% NonemptyInterval.toProd_injective.commSemiring _
     toProd_zero toProd_one toProd_add toProd_mul (swap toProd_nsmul) toProd_pow (fun _ => rfl)
 
 end NonemptyInterval
@@ -482,34 +485,32 @@ protected theorem mul_eq_one_iff : s * t = 1 ↔ ∃ a b, s = pure a ∧ t = pur
 
 instance subtractionCommMonoid {α : Type u}
     [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] :
-    SubtractionCommMonoid (NonemptyInterval α) :=
-  { NonemptyInterval.addCommMonoid with
-    sub_eq_add_neg := fun s t => by
-      refine NonemptyInterval.ext (Prod.ext ?_ ?_) <;>
-      exact sub_eq_add_neg _ _
-    neg_neg := fun s => by apply NonemptyInterval.ext; exact neg_neg _
-    neg_add_rev := fun s t => by
-      refine NonemptyInterval.ext (Prod.ext ?_ ?_) <;>
-      exact neg_add_rev _ _
-    neg_eq_of_add := fun s t h => by
-      obtain ⟨a, b, rfl, rfl, hab⟩ := NonemptyInterval.add_eq_zero_iff.1 h
-      rw [neg_pure, neg_eq_of_add_eq_zero_right hab]
-    -- TODO: use a better defeq
-    zsmul := zsmulRec }
+    SubtractionCommMonoid (NonemptyInterval α) where
+  sub_eq_add_neg := fun s t => by
+    refine NonemptyInterval.ext (Prod.ext ?_ ?_) <;>
+    exact sub_eq_add_neg _ _
+  neg_neg := fun s => by apply NonemptyInterval.ext; exact neg_neg _
+  neg_add_rev := fun s t => by
+    refine NonemptyInterval.ext (Prod.ext ?_ ?_) <;>
+    exact neg_add_rev _ _
+  neg_eq_of_add := fun s t h => by
+    obtain ⟨a, b, rfl, rfl, hab⟩ := NonemptyInterval.add_eq_zero_iff.1 h
+    rw [neg_pure, neg_eq_of_add_eq_zero_right hab]
+  -- TODO: use a better defeq
+  zsmul := zsmulRec
 
 @[to_additive existing NonemptyInterval.subtractionCommMonoid]
-instance divisionCommMonoid : DivisionCommMonoid (NonemptyInterval α) :=
-  { NonemptyInterval.commMonoid with
-    div_eq_mul_inv := fun s t => by
-      refine NonemptyInterval.ext (Prod.ext ?_ ?_) <;>
-      exact div_eq_mul_inv _ _
-    inv_inv := fun s => by apply NonemptyInterval.ext; exact inv_inv _
-    mul_inv_rev := fun s t => by
-      refine NonemptyInterval.ext (Prod.ext ?_ ?_) <;>
-      exact mul_inv_rev _ _
-    inv_eq_of_mul := fun s t h => by
-      obtain ⟨a, b, rfl, rfl, hab⟩ := NonemptyInterval.mul_eq_one_iff.1 h
-      rw [inv_pure, inv_eq_of_mul_eq_one_right hab] }
+instance divisionCommMonoid : DivisionCommMonoid (NonemptyInterval α) where
+  div_eq_mul_inv := fun s t => by
+    refine NonemptyInterval.ext (Prod.ext ?_ ?_) <;>
+    exact div_eq_mul_inv _ _
+  inv_inv := fun s => by apply NonemptyInterval.ext; exact inv_inv _
+  mul_inv_rev := fun s t => by
+    refine NonemptyInterval.ext (Prod.ext ?_ ?_) <;>
+    exact mul_inv_rev _ _
+  inv_eq_of_mul := fun s t h => by
+    obtain ⟨a, b, rfl, rfl, hab⟩ := NonemptyInterval.mul_eq_one_iff.1 h
+    rw [inv_pure, inv_eq_of_mul_eq_one_right hab]
 
 end NonemptyInterval
 
@@ -524,39 +525,37 @@ protected theorem mul_eq_one_iff : s * t = 1 ↔ ∃ a b, s = pure a ∧ t = pur
   cases t
   · simp
   · simp_rw [← NonemptyInterval.coe_mul_interval, ← NonemptyInterval.coe_one_interval,
-      WithBot.coe_inj, NonemptyInterval.coe_eq_pure]
+      Interval.coe_inj, NonemptyInterval.coe_eq_pure]
     exact NonemptyInterval.mul_eq_one_iff
 
 instance subtractionCommMonoid {α : Type u}
     [AddCommGroup α] [PartialOrder α] [IsOrderedAddMonoid α] :
-    SubtractionCommMonoid (Interval α) :=
-  { Interval.addCommMonoid with
-    sub_eq_add_neg := by
-      rintro (_ | s) (_ | t) <;> first | rfl | exact congr_arg WithBot.some (sub_eq_add_neg _ _)
-    neg_neg := by rintro (_ | s) <;> first | rfl | exact congr_arg WithBot.some (neg_neg _)
-    neg_add_rev := by
-      rintro (_ | s) (_ | t) <;> first | rfl | exact congr_arg WithBot.some (neg_add_rev _ _)
-    neg_eq_of_add := by
-      rintro (_ | s) (_ | t) h <;>
-        first
-          | cases h
-          | exact congr_arg WithBot.some (neg_eq_of_add_eq_zero_right <| WithBot.coe_injective h)
-    -- TODO: use a better defeq
-    zsmul := zsmulRec }
+    SubtractionCommMonoid (Interval α) where
+  sub_eq_add_neg := by
+    rintro (_ | s) (_ | t) <;> first | rfl | exact congr_arg WithBot.some (sub_eq_add_neg _ _)
+  neg_neg := by rintro (_ | s) <;> first | rfl | exact congr_arg WithBot.some (neg_neg _)
+  neg_add_rev := by
+    rintro (_ | s) (_ | t) <;> first | rfl | exact congr_arg WithBot.some (neg_add_rev _ _)
+  neg_eq_of_add := by
+    rintro (_ | s) (_ | t) h <;>
+      first
+        | cases h
+        | exact congr_arg WithBot.some (neg_eq_of_add_eq_zero_right <| WithBot.coe_injective h)
+  -- TODO: use a better defeq
+  zsmul := zsmulRec
 
 @[to_additive existing Interval.subtractionCommMonoid]
-instance divisionCommMonoid : DivisionCommMonoid (Interval α) :=
-  { Interval.commMonoid with
-    div_eq_mul_inv := by
-      rintro (_ | s) (_ | t) <;> first | rfl | exact congr_arg WithBot.some (div_eq_mul_inv _ _)
-    inv_inv := by rintro (_ | s) <;> first | rfl | exact congr_arg WithBot.some (inv_inv _)
-    mul_inv_rev := by
-      rintro (_ | s) (_ | t) <;> first | rfl | exact congr_arg WithBot.some (mul_inv_rev _ _)
-    inv_eq_of_mul := by
-      rintro (_ | s) (_ | t) h <;>
-        first
-          | cases h
-          | exact congr_arg WithBot.some (inv_eq_of_mul_eq_one_right <| WithBot.coe_injective h) }
+instance divisionCommMonoid : DivisionCommMonoid (Interval α) where
+  div_eq_mul_inv := by
+    rintro (_ | s) (_ | t) <;> first | rfl | exact congr_arg WithBot.some (div_eq_mul_inv _ _)
+  inv_inv := by rintro (_ | s) <;> first | rfl | exact congr_arg WithBot.some (inv_inv _)
+  mul_inv_rev := by
+    rintro (_ | s) (_ | t) <;> first | rfl | exact congr_arg WithBot.some (mul_inv_rev _ _)
+  inv_eq_of_mul := by
+    rintro (_ | s) (_ | t) h <;>
+      first
+        | cases h
+        | exact congr_arg WithBot.some (inv_eq_of_mul_eq_one_right <| WithBot.coe_injective h)
 
 end Interval
 
@@ -635,6 +634,10 @@ theorem length_neg : ∀ s : Interval α, (-s).length = s.length
   | ⊥ => rfl
   | (s : NonemptyInterval α) => s.length_neg
 
+omit [IsOrderedAddMonoid α] in
+@[simp]
+theorem length_bot : (⊥ : Interval α).length = 0 := rfl
+
 theorem length_add_le : ∀ s t : Interval α, (s + t).length ≤ s.length + t.length
   | ⊥, _ => by simp
   | _, ⊥ => by simp

Mathlib/Order/Interval/Basic.lean

@@ -283,24 +283,21 @@ end NonemptyInterval
 We represent intervals either as `⊥` or a nonempty interval given by its endpoints `fst`, `snd`.
 To convert intervals to the set of elements between these endpoints, use the coercion
 `Interval α → Set α`. -/
-abbrev Interval (α : Type*) [LE α] :=
+def Interval (α : Type*) [LE α] :=
   WithBot (NonemptyInterval α)
+deriving Inhabited, LE, OrderBot
 
 namespace Interval
 
 section LE
 
 variable [LE α]
 
--- The `Inhabited, LE, OrderBot` instances should be constructed by a deriving handler.
--- https://github.com/leanprover-community/mathlib4/issues/380
--- Note(kmill): `Interval` is an `abbrev`, so none of these `instance`s are needed.
-instance : Inhabited (Interval α) := WithBot.inhabited
-instance : LE (Interval α) := WithBot.instLE
-instance : OrderBot (Interval α) := WithBot.instOrderBot
+/-- Canonical coercion from nonempty intervals to intervals -/
+@[coe] def coe (x : NonemptyInterval α) : Interval α := (x : WithBot _)
 
 instance : Coe (NonemptyInterval α) (Interval α) :=
-  WithBot.coe
+  ⟨coe⟩
 
 instance canLift : CanLift (Interval α) (NonemptyInterval α) (↑) fun r => r ≠ ⊥ :=
   WithBot.canLift
@@ -340,7 +337,7 @@ section Preorder
 variable [Preorder α] [Preorder β] [Preorder γ]
 
 instance : Preorder (Interval α) :=
-  WithBot.instPreorder
+  inferInstanceAs <| Preorder (WithBot _)
 
 /-- `{a}` as an interval. -/
 def pure (a : α) : Interval α :=
@@ -386,10 +383,14 @@ theorem dual_map (f : α →o β) (s : Interval α) : dual (s.map f) = s.dual.ma
   · rfl
   · exact WithBot.map_comm rfl _
 
+@[simp, norm_cast]
+lemma coe_le_coe {s t : NonemptyInterval α} : (s : Interval α) ≤ t ↔ s ≤ t :=
+  WithBot.coe_le_coe
+
 variable [BoundedOrder α]
 
 instance boundedOrder : BoundedOrder (Interval α) :=
-  WithBot.instBoundedOrder
+  inferInstanceAs <| BoundedOrder (WithBot _)
 
 @[simp]
 theorem dual_top : dual (⊤ : Interval α) = ⊤ :=
@@ -402,7 +403,7 @@ section PartialOrder
 variable [PartialOrder α] [PartialOrder β] {s t : Interval α} {a b : α}
 
 instance partialOrder : PartialOrder (Interval α) :=
-  WithBot.instPartialOrder
+  inferInstanceAs <| PartialOrder (WithBot _)
 
 /-- Consider an interval `[a, b]` as the set `[a, b]`. -/
 def coeHom : Interval α ↪o Set α :=
@@ -469,7 +470,7 @@ section Lattice
 variable [Lattice α]
 
 instance semilatticeSup : SemilatticeSup (Interval α) :=
-  WithBot.semilatticeSup
+  inferInstanceAs <| SemilatticeSup (WithBot _)
 
 section Decidable
 
@@ -483,8 +484,7 @@ instance lattice : Lattice (Interval α) :=
       | _, ⊥ => ⊥
       | some s, some t =>
         if h : s.fst ≤ t.snd ∧ t.fst ≤ s.snd then
-          WithBot.some
-            ⟨⟨s.fst ⊔ t.fst, s.snd ⊓ t.snd⟩,
+          coe ⟨⟨s.fst ⊔ t.fst, s.snd ⊓ t.snd⟩,
               sup_le (le_inf s.fst_le_snd h.1) <| le_inf h.2 t.fst_le_snd⟩
         else ⊥
     inf_le_left := fun s t =>
@@ -514,8 +514,8 @@ instance lattice : Lattice (Interval α) :=
         lift t to NonemptyInterval α using ne_bot_of_le_ne_bot WithBot.coe_ne_bot hb
         lift c to NonemptyInterval α using ne_bot_of_le_ne_bot WithBot.coe_ne_bot hc
         change _ ≤ dite _ _ _
-        simp only [WithBot.coe_le_coe] at hb hc ⊢
-        rw [dif_pos, WithBot.coe_le_coe]
+        simp only [Interval.coe_le_coe] at hb hc ⊢
+        rw [dif_pos, Interval.coe_le_coe]
         · exact ⟨sup_le hb.1 hc.1, le_inf hb.2 hc.2⟩
         -- Porting note: had to add the next 6 lines including the changes because
         -- it seems that lean cannot automatically turn `NonemptyInterval.toDualProd s`
@@ -529,6 +529,12 @@ instance lattice : Lattice (Interval α) :=
         -- Porting note: originally it just had `hb.1` etc. in this next line
         exact ⟨hb₁.trans <| s.fst_le_snd.trans hc₂, hc₁.trans <| s.fst_le_snd.trans hb₂⟩ }
 
+lemma inf_coe (s t : NonemptyInterval α) :
+    (s : Interval α) ⊓ t = if h : s.fst ≤ t.snd ∧ t.fst ≤ s.snd then
+      coe ⟨⟨s.fst ⊔ t.fst, s.snd ⊓ t.snd⟩,
+        sup_le (le_inf s.fst_le_snd h.1) <| le_inf h.2 t.fst_le_snd⟩
+      else ⊥ := rfl
+
 @[simp, norm_cast]
 theorem coe_inf : ∀ s t : Interval α, (↑(s ⊓ t) : Set α) = ↑s ∩ ↑t
   | ⊥, _ => by
@@ -538,8 +544,7 @@ theorem coe_inf : ∀ s t : Interval α, (↑(s ⊓ t) : Set α) = ↑s ∩ ↑t
     rw [inf_bot_eq]
     exact (inter_empty _).symm
   | (s : NonemptyInterval α), (t : NonemptyInterval α) => by
-    simp only [Min.min, coe_coe, NonemptyInterval.coe_def, Icc_inter_Icc,
-      SemilatticeInf.inf, Lattice.inf]
+    simp only [coe_coe, NonemptyInterval.coe_def, Icc_inter_Icc, inf_coe]
     split_ifs with h
     · simp only [coe_coe, NonemptyInterval.coe_def]
     · refine (Icc_eq_empty <| mt ?_ h).symm
@@ -562,7 +567,7 @@ namespace NonemptyInterval
 
 section Preorder
 
-variable [Preorder α] {s : NonemptyInterval α} {a : α}
+variable [Preorder α] {s t : NonemptyInterval α} {a : α}
 
 @[simp, norm_cast]
 theorem coe_pure_interval (a : α) : (pure a : Interval α) = Interval.pure a :=
@@ -601,7 +606,7 @@ noncomputable instance completeLattice [DecidableLE α] : CompleteLattice (Inter
   sSup := fun S =>
     if h : S ⊆ {⊥} then ⊥
     else
-      WithBot.some
+      coe
         ⟨⟨⨅ (s : NonemptyInterval α) (_ : ↑s ∈ S), s.fst,
             ⨆ (s : NonemptyInterval α) (_ : ↑s ∈ S), s.snd⟩, by
           obtain ⟨s, hs, ha⟩ := not_subset.1 h
@@ -617,7 +622,7 @@ noncomputable instance completeLattice [DecidableLE α] : CompleteLattice (Inter
       · -- Porting note: This case was
         -- `exact WithBot.some_le_some.2 ⟨iInf₂_le _ ha, le_iSup₂_of_le _ ha le_rfl⟩`
         -- but there seems to be a defEq-problem at `iInf₂_le` that lean cannot resolve yet.
-        apply WithBot.coe_le_coe.2
+        apply Interval.coe_le_coe.2
         constructor
         · apply iInf₂_le
           exact ha
@@ -628,15 +633,15 @@ noncomputable instance completeLattice [DecidableLE α] : CompleteLattice (Inter
       obtain ⟨b, hs, hb⟩ := not_subset.1 h
       lift s to NonemptyInterval α using ne_bot_of_le_ne_bot hb (ha hs)
       exact
-        WithBot.coe_le_coe.2
+        Interval.coe_le_coe.2
           ⟨le_iInf₂ fun c hc => (WithBot.coe_le_coe.1 <| ha hc).1,
             iSup₂_le fun c hc => (WithBot.coe_le_coe.1 <| ha hc).2⟩
   sInf := fun S =>
     if h :
         ⊥ ∉ S ∧
           ∀ ⦃s : NonemptyInterval α⦄,
             ↑s ∈ S → ∀ ⦃t : NonemptyInterval α⦄, ↑t ∈ S → s.fst ≤ t.snd then
-      WithBot.some
+      coe
         ⟨⟨⨆ (s : NonemptyInterval α) (_ : ↑s ∈ S), s.fst,
             ⨅ (s : NonemptyInterval α) (_ : ↑s ∈ S), s.snd⟩,
           iSup₂_le fun s hs => le_iInf₂ <| h.2 hs⟩