From fec084c3c5231fe8f751a56e6f3f551dad7ed248 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= <yael.dillies@gmail.com>
Date: Sat, 18 Dec 2021 18:09:30 +0000
Subject: [PATCH] feat(order/cover): The covering relation (#10676)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This defines `a ⋖ b` to mean that `a < b` and there is no element in between. It is generally useful, but in particular in the context of polytopes and successor orders.

Co-authored-by: Violeta Hernández <vi.hdz.p@gmail.com>
Co-authored-by: Grayson Burton <noobie365@gmail.com>
---
 src/order/atoms.lean     | 31 +++++++++++-----
 src/order/basic.lean     |  9 +++++
 src/order/cover.lean     | 76 ++++++++++++++++++++++++++++++++++++++++
 src/order/succ_pred.lean | 59 ++++++++++++++++++++++++++++---
 4 files changed, 163 insertions(+), 12 deletions(-)
 create mode 100644 src/order/cover.lean

diff --git a/src/order/atoms.lean b/src/order/atoms.lean
index d7a7d7230465b..111d680ebc3df 100644
--- a/src/order/atoms.lean
+++ b/src/order/atoms.lean
@@ -5,6 +5,7 @@ Authors: Aaron Anderson
 -/
 
 import order.complete_boolean_algebra
+import order.cover
 import order.modular_lattice
 import data.fintype.basic
 
@@ -53,41 +54,53 @@ section atoms
 
 section is_atom
 
-variables [partial_order α] [order_bot α]
+variables [partial_order α] [order_bot α] {a b x : α}
 
 /-- An atom of an `order_bot` is an element with no other element between it and `⊥`,
   which is not `⊥`. -/
 def is_atom (a : α) : Prop := a ≠ ⊥ ∧ (∀ b, b < a → b = ⊥)
 
-lemma eq_bot_or_eq_of_le_atom {a b : α} (ha : is_atom a) (hab : b ≤ a) : b = ⊥ ∨ b = a :=
+lemma eq_bot_or_eq_of_le_atom (ha : is_atom a) (hab : b ≤ a) : b = ⊥ ∨ b = a :=
 hab.lt_or_eq.imp_left (ha.2 b)
 
-lemma is_atom.Iic {x a : α} (ha : is_atom a) (hax : a ≤ x) : is_atom (⟨a, hax⟩ : set.Iic x) :=
+lemma is_atom.Iic (ha : is_atom a) (hax : a ≤ x) : is_atom (⟨a, hax⟩ : set.Iic x) :=
 ⟨λ con, ha.1 (subtype.mk_eq_mk.1 con), λ ⟨b, hb⟩ hba, subtype.mk_eq_mk.2 (ha.2 b hba)⟩
 
-lemma is_atom.of_is_atom_coe_Iic {x : α} {a : set.Iic x} (ha : is_atom a) : is_atom (a : α) :=
+lemma is_atom.of_is_atom_coe_Iic {a : set.Iic x} (ha : is_atom a) : is_atom (a : α) :=
 ⟨λ con, ha.1 (subtype.ext con), λ b hba, subtype.mk_eq_mk.1 (ha.2 ⟨b, hba.le.trans a.prop⟩ hba)⟩
 
+@[simp] lemma bot_covers_iff : ⊥ ⋖ a ↔ is_atom a :=
+⟨λ h, ⟨h.lt.ne', λ b hba, not_not.1 $ λ hb, h.2 (ne.bot_lt hb) hba⟩,
+  λ h, ⟨h.1.bot_lt, λ b hb hba, hb.ne' $ h.2 _ hba⟩⟩
+
+alias bot_covers_iff ↔ covers.is_atom is_atom.bot_covers
+
 end is_atom
 
 section is_coatom
 
-variables [partial_order α] [order_top α]
+variables [partial_order α] [order_top α] {a b x : α}
 
 /-- A coatom of an `order_top` is an element with no other element between it and `⊤`,
   which is not `⊤`. -/
 def is_coatom (a : α) : Prop := a ≠ ⊤ ∧ (∀ b, a < b → b = ⊤)
 
-lemma eq_top_or_eq_of_coatom_le {a b : α} (ha : is_coatom a) (hab : a ≤ b) : b = ⊤ ∨ b = a :=
+lemma eq_top_or_eq_of_coatom_le (ha : is_coatom a) (hab : a ≤ b) : b = ⊤ ∨ b = a :=
 hab.lt_or_eq.imp (ha.2 b) eq_comm.2
 
-lemma is_coatom.Ici {x a : α} (ha : is_coatom a) (hax : x ≤ a) : is_coatom (⟨a, hax⟩ : set.Ici x) :=
+lemma is_coatom.Ici (ha : is_coatom a) (hax : x ≤ a) : is_coatom (⟨a, hax⟩ : set.Ici x) :=
 ⟨λ con, ha.1 (subtype.mk_eq_mk.1 con), λ ⟨b, hb⟩ hba, subtype.mk_eq_mk.2 (ha.2 b hba)⟩
 
-lemma is_coatom.of_is_coatom_coe_Ici {x : α} {a : set.Ici x} (ha : is_coatom a) :
+lemma is_coatom.of_is_coatom_coe_Ici {a : set.Ici x} (ha : is_coatom a) :
   is_coatom (a : α) :=
 ⟨λ con, ha.1 (subtype.ext con), λ b hba, subtype.mk_eq_mk.1 (ha.2 ⟨b, le_trans a.prop hba.le⟩ hba)⟩
 
+@[simp] lemma covers_top_iff : a ⋖ ⊤ ↔ is_coatom a :=
+⟨λ h, ⟨h.ne, λ b hab, not_not.1 $ λ hb, h.2 hab $ ne.lt_top hb⟩,
+  λ h, ⟨h.1.lt_top, λ b hab hb, hb.ne $ h.2 _ hab⟩⟩
+
+alias covers_top_iff ↔ covers.is_coatom is_coatom.covers_top
+
 end is_coatom
 
 section pairwise
@@ -331,6 +344,8 @@ protected def is_simple_order.linear_order [decidable_eq α] : linear_order α :
 
 @[simp] lemma is_coatom_bot : is_coatom (⊥ : α) := is_atom_dual_iff_is_coatom.1 is_atom_top
 
+lemma bot_covers_top : (⊥ : α) ⋖ ⊤ := is_atom_top.bot_covers
+
 end is_simple_order
 
 namespace is_simple_order
diff --git a/src/order/basic.lean b/src/order/basic.lean
index 9c44cf4117a75..c9033597bdf77 100644
--- a/src/order/basic.lean
+++ b/src/order/basic.lean
@@ -190,6 +190,15 @@ alias eq_or_lt_of_le ← has_le.le.eq_or_lt
 
 attribute [nolint decidable_classical] has_le.le.eq_or_lt_dec
 
+lemma eq_of_le_of_not_lt [partial_order α] {a b : α} (hab : a ≤ b) (hba : ¬ a < b) : a = b :=
+hab.eq_or_lt.resolve_right hba
+
+lemma eq_of_ge_of_not_gt [partial_order α] {a b : α} (hab : a ≤ b) (hba : ¬ a < b) : b = a :=
+(hab.eq_or_lt.resolve_right hba).symm
+
+alias eq_of_le_of_not_lt ← has_le.le.eq_of_not_lt
+alias eq_of_ge_of_not_gt ← has_le.le.eq_of_not_gt
+
 lemma ne.le_iff_lt [partial_order α] {a b : α} (h : a ≠ b) : a ≤ b ↔ a < b :=
 ⟨λ h', lt_of_le_of_ne h' h, λ h, h.le⟩
 
diff --git a/src/order/cover.lean b/src/order/cover.lean
new file mode 100644
index 0000000000000..714eafe82bef1
--- /dev/null
+++ b/src/order/cover.lean
@@ -0,0 +1,76 @@
+/-
+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. ∃ b, a < b
+
+## 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_covers_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_covers_to_dual_iff : to_dual b ⋖ to_dual a ↔ a ⋖ b :=
+and_congr_right' $ forall_congr $ λ c, forall_swap
+
+alias to_dual_covers_to_dual_iff ↔ _ covers.to_dual
+
+/-- In a dense order, nothing covers anything. -/
+lemma not_covers [densely_ordered α] : ¬ a ⋖ b :=
+λ h, let ⟨c, hc⟩ := exists_between h.1 in h.2 hc.1 hc.2
+
+end has_lt
+
+section preorder
+variables [preorder α] {a b : α}
+
+lemma covers.le (h : a ⋖ b) : a ≤ b := h.1.le
+protected lemma covers.ne (h : a ⋖ b) : a ≠ b := h.lt.ne
+lemma covers.ne' (h : a ⋖ b) : b ≠ a := 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⟩
+
+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
diff --git a/src/order/succ_pred.lean b/src/order/succ_pred.lean
index 15a72e7bee7d5..efa1b368e03c9 100644
--- a/src/order/succ_pred.lean
+++ b/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,14 @@ 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)
 
+alias lt_succ_of_not_maximal ← has_lt.lt.lt_succ
+
+protected lemma _root_.has_lt.lt.covers_succ {a b : α} (h : a < b) : a ⋖ succ a :=
+⟨h.lt_succ, λ c hc, (succ_le_of_lt hc).not_lt⟩
+
+@[simp] lemma covers_succ_of_nonempty_Ioi {a : α} (h : (set.Ioi a).nonempty) : a ⋖ succ a :=
+has_lt.lt.covers_succ h.some_mem
+
 section no_top_order
 variables [no_top_order α] {a b : α}
 
@@ -127,6 +135,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 +172,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 +199,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 :=
+⟨covers.succ_eq, by { rintro rfl, exact covers_succ _ }⟩
+
 end no_top_order
 
 end partial_order
@@ -299,6 +315,14 @@ 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)
 
+alias pred_lt_of_not_minimal ← has_lt.lt.pred_lt
+
+protected lemma _root_.has_lt.lt.pred_covers {a b : α} (h : b < a) : pred a ⋖ a :=
+⟨h.pred_lt, λ c hc, (le_of_pred_lt hc).not_lt⟩
+
+@[simp] lemma pred_covers_of_nonempty_Iio {a : α} (h : (set.Iio a).nonempty) : pred a ⋖ a :=
+has_lt.lt.pred_covers h.some_mem
+
 section no_bot_order
 variables [no_bot_order α] {a b : α}
 
@@ -323,6 +347,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 +384,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 +409,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 +451,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 +481,25 @@ end pred_order
 
 open succ_order pred_order
 
+/-! ### Successor-predecessor orders -/
+
+section succ_pred_order
+variables [partial_order α] [succ_order α] [pred_order α] {a b : α}
+
+protected lemma _root_.has_lt.lt.succ_pred (h : b < a) : succ (pred a) = a := h.pred_covers.succ_eq
+protected lemma _root_.has_lt.lt.pred_succ (h : a < b) : pred (succ a) = a := h.covers_succ.pred_eq
+
+@[simp] lemma succ_pred_of_nonempty_Iio {a : α} (h : (set.Iio a).nonempty) : succ (pred a) = a :=
+has_lt.lt.succ_pred h.some_mem
+
+@[simp] lemma pred_succ_of_nonempty_Ioi {a : α} (h : (set.Ioi a).nonempty) : pred (succ a) = a :=
+has_lt.lt.pred_succ h.some_mem
+
+@[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