[Merged by Bors] - feat(order/cover): The covering relation

src/order/basic.lean

@@ -115,6 +115,12 @@ lemma lt_iff_ne [partial_order α] {x y : α} (h : x ≤ y) : x < y ↔ x ≠ y
 lemma le_iff_eq [partial_order α] {x y : α} (h : x ≤ y) : y ≤ x ↔ y = x :=
 ⟨λ h', h'.antisymm h, eq.le⟩
 
+lemma eq_of_not_lt [partial_order α] {a b : α} (hab : a ≤ b) (hba : ¬ a < b) : a = b :=
+hab.antisymm $ not_not.1 $ λ h, hba $ hab.lt_of_not_le h
+
+lemma eq_of_not_gt [partial_order α] {a b : α} (hab : a ≤ b) (hba : ¬ a < b) : b = a :=
+(hab.eq_of_not_lt hba).symm
+
 lemma lt_or_le [linear_order α] {a b : α} (h : a ≤ b) (c : α) : a < c ∨ c ≤ b :=
 (lt_or_ge a c).imp id $ λ hc, le_trans hc h
 

src/order/cover.lean

@@ -0,0 +1,73 @@
+/-
+Copyright (c) 2021 Yaël Dillies. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yaël Dillies, Violeta Hernández Palacios, Grayson Burton
+-/
+import data.set.intervals.basic
+
+/-!
+# The covering relation
+
+This file defines the covering relation in an order. `b` is said to cover `a` if `a < b` and there
+is no element in between.
+
+## Notation
+
+`a ⋖ b` means that `b` covers `a`.
+-/
+
+open set
+
+variables {α : Type*}
+
+section has_lt
+variables [has_lt α] {a b : α}
+
+/-- `covers a b` means that `b` covers `a`: `a < b` and there is no element in between. -/
+def covers (a b : α) : Prop := a < b ∧ ∀ ⦃c⦄, a < c → ¬ c < b
+
+infix ` ⋖ `:50 := covers
+
+lemma covers.lt (h : a ⋖ b) : a < b := h.1
+
+/-- If `a < b`, then `b` does not cover `a` iff there's an element in between. -/
+lemma not_cover_iff (h : a < b) : ¬a ⋖ b ↔ ∃ c, a < c ∧ c < b :=
+by { simp_rw [covers, not_and, not_forall, exists_prop, not_not], exact imp_iff_right h }
+
+open order_dual
+
+@[simp] lemma to_dual_cover_to_dual_iff : to_dual b ⋖ to_dual a ↔ a ⋖ b :=
+and_congr_right' $ forall_congr $ λ c, forall_swap
+
+end has_lt
+
+section preorder
+variables [preorder α] {a b : α}
+
+lemma covers.le (h : a ⋖ b) : a ≤ b := h.1.le
+lemma covers.ne (h : a ⋖ b) : a ≠ b := h.lt.ne
+
+lemma covers.Ioo_eq (h : a ⋖ b) : Ioo a b = ∅ :=
+eq_empty_iff_forall_not_mem.2 $ λ x hx, h.2 hx.1 hx.2
+
+instance covers.is_irrefl : is_irrefl α (⋖) := ⟨λ a ha, ha.ne rfl⟩
+
+/-- In a dense order, nothing covers anything. -/
+lemma not_cover [densely_ordered α] : ¬ a ⋖ b :=
+λ h, let ⟨c, hc⟩ := exists_between h.1 in h.2 hc.1 hc.2
+
+end preorder
+
+section partial_order
+variables [partial_order α] {a b : α}
+
+lemma covers.Ico_eq (h : a ⋖ b) : Ico a b = {a} :=
+by rw [←set.Ioo_union_left h.lt, h.Ioo_eq, empty_union]
+
+lemma covers.Ioc_eq (h : a ⋖ b) : Ioc a b = {b} :=
+by rw [←set.Ioo_union_right h.lt, h.Ioo_eq, empty_union]
+
+lemma covers.Icc_eq (h : a ⋖ b) : Icc a b = {a, b} :=
+by { rw [←set.Ico_union_right h.le, h.Ico_eq], refl }
+
+end partial_order

src/order/succ_pred.lean

@@ -3,10 +3,11 @@ Copyright (c) 2021 Yaël Dillies. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies
 -/
+import order.bounded_order
 import order.complete_lattice
+import order.cover
 import order.iterate
 import tactic.monotonicity
-import order.bounded_order
 
 /-!
 # Successor and predecessor
@@ -49,8 +50,7 @@ Is `galois_connection pred succ` always true? If not, we should introduce
 class succ_pred_order (α : Type*) [preorder α] extends succ_order α, pred_order α :=
 (pred_succ_gc : galois_connection (pred : α → α) succ)
 ```
-This gives `succ (pred n) = n` and `pred (succ n)` for free when `no_bot_order α` and
-`no_top_order α` respectively.
+`covers` should help here.
 -/
 
 open function
@@ -103,6 +103,9 @@ lemma succ_mono : monotone (succ : α → α) := λ a b, succ_le_succ
 lemma lt_succ_of_not_maximal {a b : α} (h : a < b) : a < succ a :=
 (le_succ a).lt_of_not_le (λ ha, maximal_of_succ_le ha h)
 
+lemma covers_succ_of_not_maximal {a b : α} (h : a < b) : a ⋖ succ a :=
+⟨lt_succ_of_not_maximal h, λ c hc, (succ_le_of_lt hc).not_lt⟩
+
 section no_top_order
 variables [no_top_order α] {a b : α}
 
@@ -127,6 +130,8 @@ alias succ_lt_succ_iff ↔ lt_of_succ_lt_succ succ_lt_succ
 
 lemma succ_strict_mono : strict_mono (succ : α → α) := λ a b, succ_lt_succ
 
+lemma covers_succ (a : α) : a ⋖ succ a := ⟨lt_succ a, λ c hc, (succ_le_of_lt hc).not_lt⟩
+
 end no_top_order
 
 end preorder
@@ -162,6 +167,9 @@ begin
   { exact ⟨le_succ a, le_rfl⟩ }
 end
 
+lemma _root_.covers.succ_eq {a b : α} (h : a ⋖ b) : succ a = b :=
+(succ_le_of_lt h.lt).eq_of_not_lt $ λ h', h.2 (lt_succ_of_not_maximal h.lt) h'
+
 section no_top_order
 variables [no_top_order α] {a b : α}
 
@@ -186,6 +194,9 @@ lt_succ_iff.trans le_iff_lt_or_eq
 lemma le_succ_iff_lt_or_eq : a ≤ succ b ↔ (a ≤ b ∨ a = succ b) :=
 by rw [←lt_succ_iff, ←lt_succ_iff, lt_succ_iff_lt_or_eq]
 
+lemma _root_.covers_iff_succ_eq : a ⋖ b ↔ succ a = b :=
+⟨_root_.covers.succ_eq, by { rintro rfl, exact covers_succ _ }⟩
+
 end no_top_order
 
 end partial_order
@@ -225,7 +236,7 @@ lemma succ_ne_bot (a : α) : succ a ≠ ⊥ :=
 end order_bot
 
 section linear_order
-variables [linear_order α]
+variables [linear_order α] {a b : α}
 
 /-- A constructor for `succ_order α` usable when `α` is a linear order with no maximal element. -/
 def of_succ_le_iff (succ : α → α) (hsucc_le_iff : ∀ {a b}, succ a ≤ b ↔ a < b) :
@@ -299,6 +310,9 @@ lemma pred_mono : monotone (pred : α → α) := λ a b, pred_le_pred
 lemma pred_lt_of_not_minimal {a b : α} (h : b < a) : pred a < a :=
 (pred_le a).lt_of_not_le (λ ha, minimal_of_le_pred ha h)
 
+lemma pred_covers_of_not_minimal {a b : α} (h : b < a) : pred a ⋖ a :=
+⟨pred_lt_of_not_minimal h, λ c hc, (le_of_pred_lt hc).not_lt⟩
+
 section no_bot_order
 variables [no_bot_order α] {a b : α}
 
@@ -323,6 +337,8 @@ alias pred_lt_pred_iff ↔ lt_of_pred_lt_pred pred_lt_pred
 
 lemma pred_strict_mono : strict_mono (pred : α → α) := λ a b, pred_lt_pred
 
+lemma pred_covers (a : α) : pred a ⋖ a := ⟨pred_lt a, λ c hc, (le_of_pred_lt hc).not_lt⟩
+
 end no_bot_order
 
 end preorder
@@ -358,6 +374,9 @@ begin
   { exact ⟨le_rfl, pred_le a⟩ }
 end
 
+lemma _root_.covers.pred_eq {a b : α} (h : a ⋖ b) : pred b = a :=
+(le_pred_of_lt h.lt).eq_of_not_gt $ λ h', h.2 h' $ pred_lt_of_not_minimal h.lt
+
 section no_bot_order
 variables [no_bot_order α] {a b : α}
 
@@ -380,6 +399,9 @@ pred_lt_iff.trans le_iff_lt_or_eq
 lemma le_pred_iff_lt_or_eq : pred a ≤ b ↔ (a ≤ b ∨ pred a = b) :=
 by rw [←pred_lt_iff, ←pred_lt_iff, pred_lt_iff_lt_or_eq]
 
+lemma _root_.covers_iff_pred_eq : a ⋖ b ↔ pred b = a :=
+⟨covers.pred_eq, by { rintro rfl, exact pred_covers _ }⟩
+
 end no_bot_order
 
 end partial_order
@@ -419,7 +441,7 @@ lemma pred_ne_top [nontrivial α] (a : α) : pred a ≠ ⊤ :=
 end order_top
 
 section linear_order
-variables [linear_order α]
+variables [linear_order α] {a b : α}
 
 /-- A constructor for `pred_order α` usable when `α` is a linear order with no maximal element. -/
 def of_le_pred_iff (pred : α → α) (hle_pred_iff : ∀ {a b}, a ≤ pred b ↔ a < b) :
@@ -449,6 +471,22 @@ end pred_order
 
 open succ_order pred_order
 
+/-! ### Successor-predecessor orders -/
+
+section succ_pred_order
+variables [partial_order α] [succ_order α] [pred_order α] {a b : α}
+
+@[simp] lemma succ_pred_of_not_minimal (h : b < a) : succ (pred a) = a :=
+(pred_covers_of_not_minimal h).succ_eq
+
+@[simp] lemma pred_succ_of_not_maximal (h : a < b) : pred (succ a) = a :=
+(covers_succ_of_not_maximal h).pred_eq
+
+@[simp] lemma succ_pred [no_bot_order α] (a : α) : succ (pred a) = a := (pred_covers _).succ_eq
+@[simp] lemma pred_succ [no_top_order α] (a : α) : pred (succ a) = a := (covers_succ _).pred_eq
+
+end succ_pred_order
+
 /-! ### Dual order -/
 
 section order_dual