chore(order/well_founded): move to a file (#4568)

I want to use `order/rel_classes` before `data/set/basic`.

Author: urkud

archive/imo/imo1988_q6.lean

@@ -5,6 +5,7 @@ Authors: Johan Commelin
 -/
 
 import data.rat.basic
+import order.well_founded
 import tactic.linarith
 import tactic.omega
 

src/data/fintype/basic.lean

@@ -10,6 +10,7 @@ import data.finset.powerset
 import data.finset.lattice
 import data.finset.pi
 import data.array.lemmas
+import order.well_founded
 
 open_locale nat
 

src/order/lattice.lean

@@ -5,7 +5,7 @@ Authors: Johannes Hölzl
 
 Defines the inf/sup (semi)-lattice with optionally top/bot type class hierarchy.
 -/
-import order.basic
+import order.rel_classes
 
 set_option old_structure_cmd true
 
@@ -42,6 +42,9 @@ class semilattice_sup (α : Type u) extends has_sup α, partial_order α :=
 (le_sup_right : ∀ a b : α, b ≤ a ⊔ b)
 (sup_le : ∀ a b c : α, a ≤ c → b ≤ c → a ⊔ b ≤ c)
 
+instance (α : Type*) [has_inf α] : has_sup (order_dual α) := ⟨((⊓) : α → α → α)⟩
+instance (α : Type*) [has_sup α] : has_inf (order_dual α) := ⟨((⊔) : α → α → α)⟩
+
 section semilattice_sup
 variables [semilattice_sup α] {a b c d : α}
 
@@ -104,12 +107,14 @@ lemma sup_ind [is_total α (≤)] (a b : α) {p : α → Prop} (ha : p a) (hb :
 (is_total.total a b).elim (λ h : a ≤ b, by rwa sup_eq_right.2 h) (λ h, by rwa sup_eq_left.2 h)
 
 @[simp] lemma sup_lt_iff [is_total α (≤)] {a b c : α} : b ⊔ c < a ↔ b < a ∧ c < a :=
-⟨λ h, ⟨lt_of_le_of_lt le_sup_left h, lt_of_le_of_lt le_sup_right h⟩,
-  λ h, sup_ind b c h.1 h.2⟩
+⟨λ h, ⟨le_sup_left.trans_lt h, le_sup_right.trans_lt h⟩, λ h, sup_ind b c h.1 h.2⟩
 
 @[simp] lemma le_sup_iff [is_total α (≤)] {a b c : α} : a ≤ b ⊔ c ↔ a ≤ b ∨ a ≤ c :=
 by rw [← not_iff_not]; simp only [not_or_distrib, @sup_lt_iff α, @not_le (as_linear_order α)]
 
+@[simp] lemma lt_sup_iff [is_total α (≤)] {a b c : α} : a < b ⊔ c ↔ a < b ∨ a < c :=
+by { rw ← not_iff_not, simp only [not_or_distrib, @not_lt (as_linear_order α), sup_le_iff] }
+
 @[simp] theorem sup_idem : a ⊔ a = a :=
 by apply le_antisymm; simp
 
@@ -171,6 +176,18 @@ class semilattice_inf (α : Type u) extends has_inf α, partial_order α :=
 (inf_le_right : ∀ a b : α, a ⊓ b ≤ b)
 (le_inf : ∀ a b c : α, a ≤ b → a ≤ c → a ≤ b ⊓ c)
 
+instance (α) [semilattice_inf α] : semilattice_sup (order_dual α) :=
+{ le_sup_left  := semilattice_inf.inf_le_left,
+  le_sup_right := semilattice_inf.inf_le_right,
+  sup_le := assume a b c hca hcb, @semilattice_inf.le_inf α _ _ _ _ hca hcb,
+  .. order_dual.partial_order α, .. order_dual.has_sup α }
+
+instance (α) [semilattice_sup α] : semilattice_inf (order_dual α) :=
+{ inf_le_left  := @le_sup_left α _,
+  inf_le_right := @le_sup_right α _,
+  le_inf := assume a b c hca hcb, @sup_le α _ _ _ _ hca hcb,
+  .. order_dual.partial_order α, .. order_dual.has_inf α }
+
 section semilattice_inf
 variables [semilattice_inf α] {a b c d : α}
 
@@ -196,8 +213,7 @@ theorem inf_le_right_of_le (h : b ≤ c) : a ⊓ b ≤ c :=
 le_trans inf_le_right h
 
 @[simp] theorem le_inf_iff : a ≤ b ⊓ c ↔ a ≤ b ∧ a ≤ c :=
-⟨assume h : a ≤ b ⊓ c, ⟨le_trans h inf_le_left, le_trans h inf_le_right⟩,
-  assume ⟨h₁, h₂⟩, le_inf h₁ h₂⟩
+@sup_le_iff (order_dual α) _ _ _ _
 
 @[simp] theorem inf_eq_left : a ⊓ b = a ↔ a ≤ b :=
 le_antisymm_iff.trans $ by simp [le_refl]
@@ -230,51 +246,40 @@ theorem le_of_inf_eq (h : a ⊓ b = a) : a ≤ b :=
 by { rw ← h, simp }
 
 lemma inf_ind [is_total α (≤)] (a b : α) {p : α → Prop} (ha : p a) (hb : p b) : p (a ⊓ b) :=
-(is_total.total a b).elim (λ h : a ≤ b, by rwa inf_eq_left.2 h) (λ h, by rwa inf_eq_right.2 h)
+@sup_ind (order_dual α) _ _ _ _ _ ha hb
 
 @[simp] lemma lt_inf_iff [is_total α (≤)] {a b c : α} : a < b ⊓ c ↔ a < b ∧ a < c :=
-⟨λ h, ⟨lt_of_lt_of_le h inf_le_left, lt_of_lt_of_le h inf_le_right⟩,
-  λ h, inf_ind b c h.1 h.2⟩
+@sup_lt_iff (order_dual α) _ _ _ _ _
 
 @[simp] lemma inf_le_iff [is_total α (≤)] {a b c : α} : b ⊓ c ≤ a ↔ b ≤ a ∨ c ≤ a :=
-by rw [← not_iff_not]; simp only [not_or_distrib, @lt_inf_iff α, @not_le (as_linear_order α)]
+@le_sup_iff (order_dual α) _ _ _ _ _
 
 @[simp] theorem inf_idem : a ⊓ a = a :=
-by apply le_antisymm; simp
+@sup_idem (order_dual α) _ _
 
 instance inf_is_idempotent : is_idempotent α (⊓) := ⟨@inf_idem _ _⟩
 
 theorem inf_comm : a ⊓ b = b ⊓ a :=
-by apply le_antisymm; simp
+@sup_comm (order_dual α) _ _ _
 
 instance inf_is_commutative : is_commutative α (⊓) := ⟨@inf_comm _ _⟩
 
 theorem inf_assoc : a ⊓ b ⊓ c = a ⊓ (b ⊓ c) :=
-le_antisymm
-  (le_inf
-    (inf_le_left_of_le inf_le_left)
-    (le_inf (inf_le_left_of_le inf_le_right) inf_le_right))
-  (le_inf
-    (le_inf inf_le_left (inf_le_right_of_le inf_le_left))
-    (inf_le_right_of_le inf_le_right))
+@sup_assoc (order_dual α) _ a b c
 
 instance inf_is_associative : is_associative α (⊓) := ⟨@inf_assoc _ _⟩
 
 @[simp] lemma inf_left_idem : a ⊓ (a ⊓ b) = a ⊓ b :=
-by rw [← inf_assoc, inf_idem]
+@sup_left_idem (order_dual α) _ a b
 
 @[simp] lemma inf_right_idem : (a ⊓ b) ⊓ b = a ⊓ b :=
-by rw [inf_assoc, inf_idem]
+@sup_right_idem (order_dual α) _ a b
 
 lemma inf_left_comm (a b c : α) : a ⊓ (b ⊓ c) = b ⊓ (a ⊓ c) :=
-by rw [← inf_assoc, ← inf_assoc, @inf_comm α _ a]
+@sup_left_comm (order_dual α) _ a b c
 
 lemma forall_le_or_exists_lt_inf (a : α) : (∀b, a ≤ b) ∨ (∃b, b < a) :=
-suffices (∃b, ¬a ≤ b) → (∃b, b < a),
-  by rwa [or_iff_not_imp_left, not_forall],
-assume ⟨b, hb⟩,
-have a ⊓ b ≠ a, from assume eq, hb $ eq ▸ inf_le_right,
-⟨a ⊓ b, lt_of_le_of_ne inf_le_left ‹a ⊓ b ≠ a›⟩
+@forall_le_or_exists_lt_sup (order_dual α) _ a
 
 theorem semilattice_inf.ext_inf {α} {A B : semilattice_inf α}
   (H : ∀ x y : α, (by haveI := A; exact x ≤ y) ↔ x ≤ y)
@@ -293,11 +298,14 @@ end
 
 end semilattice_inf
 
-/- Lattices -/
+/-! ### Lattices -/
 
 /-- A lattice is a join-semilattice which is also a meet-semilattice. -/
 class lattice (α : Type u) extends semilattice_sup α, semilattice_inf α
 
+instance (α) [lattice α] : lattice (order_dual α) :=
+{ .. order_dual.semilattice_sup α, .. order_dual.semilattice_inf α }
+
 section lattice
 variables [lattice α] {a b c d : α}
 
@@ -355,6 +363,10 @@ calc x ⊓ (y ⊔ z) = (x ⊓ (x ⊔ z)) ⊓ (y ⊔ z)       : by rw [inf_sup_se
              ... = ((x ⊓ y) ⊔ x) ⊓ ((x ⊓ y) ⊔ z) : by rw [sup_comm]
              ... = (x ⊓ y) ⊔ (x ⊓ z)             : by rw [sup_inf_left]
 
+instance (α : Type*) [distrib_lattice α] : distrib_lattice (order_dual α) :=
+{ le_sup_inf := assume x y z, le_of_eq inf_sup_left.symm,
+  .. order_dual.lattice α }
+
 theorem inf_sup_right : (y ⊔ z) ⊓ x = (y ⊓ x) ⊔ (z ⊓ x) :=
 by simp only [inf_sup_left, λy:α, @inf_comm α _ y x, eq_self_iff_true]
 
@@ -374,10 +386,13 @@ le_antisymm
 
 end distrib_lattice
 
-/- Lattices derived from linear orders -/
+/-!
+### Lattices derived from linear orders
+-/
 
 @[priority 100] -- see Note [lower instance priority]
-instance lattice_of_decidable_linear_order {α : Type u} [o : decidable_linear_order α] : lattice α :=
+instance lattice_of_decidable_linear_order {α : Type u} [o : decidable_linear_order α] :
+  lattice α :=
 { sup          := max,
   le_sup_left  := le_max_left,
   le_sup_right := le_max_right,
@@ -427,39 +442,10 @@ le_inf (h inf_le_left) (h inf_le_right)
 lemma map_inf [semilattice_inf α] [is_total α (≤)] [semilattice_inf β] {f : α → β}
   (hf : monotone f) (x y : α) :
   f (x ⊓ y) = f x ⊓ f y :=
-(is_total.total x y).elim
-  (λ h : x ≤ y, by simp only [h, hf h, inf_of_le_left])
-  (λ h, by simp only [h, hf h, inf_of_le_right])
+@monotone.map_sup (order_dual α) _ _ _ _ _ hf.order_dual x y
 
 end monotone
 
-namespace order_dual
-variable (α)
-
-instance [has_inf α] : has_sup (order_dual α) := ⟨((⊓) : α → α → α)⟩
-instance [has_sup α] : has_inf (order_dual α) := ⟨((⊔) : α → α → α)⟩
-
-instance [semilattice_inf α] : semilattice_sup (order_dual α) :=
-{ le_sup_left  := @inf_le_left α _,
-  le_sup_right := @inf_le_right α _,
-  sup_le := assume a b c hca hcb, @le_inf α _ _ _ _ hca hcb,
-  .. order_dual.partial_order α, .. order_dual.has_sup α }
-
-instance [semilattice_sup α] : semilattice_inf (order_dual α) :=
-{ inf_le_left  := @le_sup_left α _,
-  inf_le_right := @le_sup_right α _,
-  le_inf := assume a b c hca hcb, @sup_le α _ _ _ _ hca hcb,
-  .. order_dual.partial_order α, .. order_dual.has_inf α }
-
-instance [lattice α] : lattice (order_dual α) :=
-{ .. order_dual.semilattice_sup α, .. order_dual.semilattice_inf α }
-
-instance [distrib_lattice α] : distrib_lattice (order_dual α) :=
-{ le_sup_inf := assume x y z, le_of_eq inf_sup_left.symm,
-  .. order_dual.lattice α }
-
-end order_dual
-
 namespace prod
 variables (α β)
 

src/order/pilex.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes
 -/
 import algebra.group.pi
-import order.rel_classes
+import order.well_founded
 import algebra.order_functions
 
 variables {ι : Type*} {β : ι → Type*} (r : ι → ι → Prop)

src/order/rel_classes.lean

@@ -3,7 +3,7 @@ Copyright (c) 2020 Jeremy Avigad. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Mario Carneiro, Yury G. Kudryashov
 -/
-import data.set.basic
+import order.basic
 
 /-!
 # Unbundled relation classes
@@ -80,6 +80,9 @@ instance [linear_order α] : is_linear_order α (≥) := {}
 instance [linear_order α] : is_trichotomous α (<) := ⟨lt_trichotomy⟩
 instance [linear_order α] : is_trichotomous α (>) := is_trichotomous.swap _
 
+instance order_dual.is_total_le [has_le α] [is_total α (≤)] : is_total (order_dual α) (≤) :=
+@is_total.swap α _ _
+
 lemma trans_trichotomous_left [is_trans α r] [is_trichotomous α r] {a b c : α} :
   ¬r b a → r b c → r a c :=
 begin
@@ -273,99 +276,3 @@ end
 
 @[simp] lemma not_unbounded_iff {r : α → α → Prop} (s : set α) : ¬unbounded r s ↔ bounded r s :=
 by { classical, rw [not_iff_comm, not_bounded_iff] }
-
-namespace well_founded
-/-- If `r` is a well-founded relation, then any nonempty set has a minimal element
-with respect to `r`. -/
-theorem has_min {α} {r : α → α → Prop} (H : well_founded r)
-  (s : set α) : s.nonempty → ∃ a ∈ s, ∀ x ∈ s, ¬ r x a
-| ⟨a, ha⟩ := (acc.rec_on (H.apply a) $ λ x _ IH, not_imp_not.1 $ λ hne hx, hne $
-  ⟨x, hx, λ y hy hyx, hne $ IH y hyx hy⟩) ha
-
-/-- A minimal element of a nonempty set in a well-founded order -/
-noncomputable def min {α} {r : α → α → Prop} (H : well_founded r)
-  (p : set α) (h : p.nonempty) : α :=
-classical.some (H.has_min p h)
-
-theorem min_mem {α} {r : α → α → Prop} (H : well_founded r)
-  (p : set α) (h : p.nonempty) : H.min p h ∈ p :=
-let ⟨h, _⟩ := classical.some_spec (H.has_min p h) in h
-
-theorem not_lt_min {α} {r : α → α → Prop} (H : well_founded r)
-  (p : set α) (h : p.nonempty) {x} (xp : x ∈ p) : ¬ r x (H.min p h) :=
-let ⟨_, h'⟩ := classical.some_spec (H.has_min p h) in h' _ xp
-
-theorem well_founded_iff_has_min  {α} {r : α → α → Prop} : (well_founded r) ↔
-  ∀ (p : set α), p.nonempty → ∃ m ∈ p, ∀ x ∈ p, ¬ r x m :=
-begin
-  classical,
-  split,
-  { exact has_min, },
-  { set counterexamples := { x : α | ¬ acc r x},
-    intro exists_max,
-    fconstructor,
-    intro x,
-    by_contra hx,
-    obtain ⟨m, m_mem, hm⟩ := exists_max counterexamples ⟨x, hx⟩,
-    refine m_mem (acc.intro _ ( λ y y_gt_m, _)),
-    by_contra hy,
-    exact hm y hy y_gt_m, },
-end
-
-lemma eq_iff_not_lt_of_le {α} [partial_order α] {x y : α} : x ≤ y → y = x ↔ ¬ x < y :=
-begin
-  split,
-  { intros xle nge,
-    cases le_not_le_of_lt nge,
-    rw xle left at nge,
-    exact lt_irrefl x nge },
-  { intros ngt xle,
-    contrapose! ngt,
-    exact lt_of_le_of_ne xle (ne.symm ngt) }
-end
-
-theorem well_founded_iff_has_max' [partial_order α] : (well_founded ((>) : α → α → Prop) ↔
-  ∀ (p : set α), p.nonempty → ∃ m ∈ p, ∀ x ∈ p, m ≤ x → x = m) :=
-by simp only [eq_iff_not_lt_of_le, well_founded_iff_has_min]
-
-theorem well_founded_iff_has_min' [partial_order α] : (well_founded (has_lt.lt : α → α → Prop)) ↔
-  ∀ (p : set α), p.nonempty → ∃ m ∈ p, ∀ x ∈ p, x ≤ m → x = m :=
-@well_founded_iff_has_max' (order_dual α) _
-
-open set
-/-- The supremum of a bounded, well-founded order -/
-protected noncomputable def sup {α} {r : α → α → Prop} (wf : well_founded r) (s : set α)
-  (h : bounded r s) : α :=
-wf.min { x | ∀a ∈ s, r a x } h
-
-protected lemma lt_sup {α} {r : α → α → Prop} (wf : well_founded r) {s : set α} (h : bounded r s)
-  {x} (hx : x ∈ s) : r x (wf.sup s h) :=
-min_mem wf { x | ∀a ∈ s, r a x } h x hx
-
-section
-open_locale classical
-/-- A successor of an element `x` in a well-founded order is a minimal element `y` such that
-`x < y` if one exists. Otherwise it is `x` itself. -/
-protected noncomputable def succ {α} {r : α → α → Prop} (wf : well_founded r) (x : α) : α :=
-if h : ∃y, r x y then wf.min { y | r x y } h else x
-
-protected lemma lt_succ {α} {r : α → α → Prop} (wf : well_founded r) {x : α} (h : ∃y, r x y) :
-  r x (wf.succ x) :=
-by { rw [well_founded.succ, dif_pos h], apply min_mem }
-end
-
-protected lemma lt_succ_iff {α} {r : α → α → Prop} [wo : is_well_order α r] {x : α} (h : ∃y, r x y)
-  (y : α) : r y (wo.wf.succ x) ↔ r y x ∨ y = x :=
-begin
-  split,
-  { intro h', have : ¬r x y,
-    { intro hy, rw [well_founded.succ, dif_pos] at h',
-      exact wo.wf.not_lt_min _ h hy h' },
-    rcases trichotomous_of r x y with hy | hy | hy,
-    exfalso, exact this hy,
-    right, exact hy.symm,
-    left, exact hy },
-  rintro (hy | rfl), exact trans hy (wo.wf.lt_succ h), exact wo.wf.lt_succ h
-end
-
-end well_founded