feat(order/well_founded): well_founded_lt.has_min, etc.

src/order/rel_classes.lean

@@ -233,12 +233,18 @@ def to_has_well_founded : has_well_founded α := ⟨r, is_well_founded.wf⟩
 
 end is_well_founded
 
+/-- There are no 2-cycles in a well-founded relation. -/
 theorem well_founded.asymmetric {α : Sort*} {r : α → α → Prop} (h : well_founded r) :
   ∀ ⦃a b⦄, r a b → ¬ r b a
 | a := λ b hab hba, well_founded.asymmetric hba hab
 using_well_founded { rel_tac := λ _ _, `[exact ⟨_, h⟩],
                      dec_tac := tactic.assumption }
 
+/-- There are no 1-cycles in a well-founded relation. -/
+theorem well_founded.irreflexive {α : Sort*} {r : α → α → Prop} (h : well_founded r) :
+  ∀ ⦃a⦄, ¬ r a a :=
+λ a ha, h.asymmetric ha ha
+
 @[priority 100] -- see Note [lower instance priority]
 instance is_well_founded.is_asymm (r : α → α → Prop) [is_well_founded α r] : is_asymm α r :=
 ⟨is_well_founded.wf.asymmetric⟩

src/order/well_founded.lean

@@ -23,45 +23,28 @@ and an induction principle `well_founded.induction_bot`.
 
 variables {α : Type*}
 
-namespace well_founded
-
-protected theorem is_asymm {α : Sort*} {r : α → α → Prop} (h : well_founded r) : is_asymm α r :=
-⟨h.asymmetric⟩
-
-instance {α : Sort*} [has_well_founded α] : is_asymm α has_well_founded.r :=
-has_well_founded.wf.is_asymm
-
-protected theorem is_irrefl {α : Sort*} {r : α → α → Prop} (h : well_founded r) : is_irrefl α r :=
-(@is_asymm.is_irrefl α r h.is_asymm)
+/-! ### Minimal and maximal elements of sets -/
 
-instance {α : Sort*} [has_well_founded α] : is_irrefl α has_well_founded.r :=
-is_asymm.is_irrefl
+namespace well_founded
+variables {r : α → α → Prop} (H : well_founded r)
 
 /-- 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
+theorem has_min (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.
-
-If you're working with a nonempty linear order, consider defining a
-`conditionally_complete_linear_order_bot` instance via
-`well_founded.conditionally_complete_linear_order_with_bot` and using `Inf` instead. -/
-noncomputable def min {r : α → α → Prop} (H : well_founded r)
-  (s : set α) (h : s.nonempty) : α :=
+/-- An arbitrary minimal element of a nonempty set in a well-founded order. -/
+noncomputable def min (s : set α) (h : s.nonempty) : α :=
 classical.some (H.has_min s h)
 
-theorem min_mem {r : α → α → Prop} (H : well_founded r)
-  (s : set α) (h : s.nonempty) : H.min s h ∈ s :=
+theorem min_mem (s : set α) (h : s.nonempty) : H.min s h ∈ s :=
 let ⟨h, _⟩ := classical.some_spec (H.has_min s h) in h
 
-theorem not_lt_min {r : α → α → Prop} (H : well_founded r)
-  (s : set α) (h : s.nonempty) {x} (hx : x ∈ s) : ¬ r x (H.min s h) :=
+theorem not_lt_min (s : set α) (h : s.nonempty) {x} (hx : x ∈ s) : ¬ r x (H.min s h) :=
 let ⟨_, h'⟩ := classical.some_spec (H.has_min s h) in h' _ hx
 
-theorem well_founded_iff_has_min {r : α → α → Prop} : (well_founded r) ↔
+theorem well_founded_iff_has_min {r : α → α → Prop} : well_founded r ↔
   ∀ (s : set α), s.nonempty → ∃ m ∈ s, ∀ x ∈ s, ¬ r x m :=
 begin
   refine ⟨λ h, h.has_min, λ h, ⟨λ x, _⟩⟩,
@@ -72,29 +55,112 @@ begin
   exact hm' y hy' hy
 end
 
+end well_founded
+
+namespace is_well_founded
+variables (r : α → α → Prop) [h : is_well_founded α r]
+
+/-- If `r` is a well-founded relation, then any nonempty set has a minimal element
+with respect to `r`. -/
+theorem has_min : ∀ s : set α, s.nonempty → ∃ a ∈ s, ∀ x ∈ s, ¬ r x a := h.wf.has_min
+
+theorem is_well_founded_iff_has_min {r : α → α → Prop} : is_well_founded α r ↔
+  ∀ s : set α, s.nonempty → ∃ m ∈ s, ∀ x ∈ s, ¬ r x m :=
+by rw [is_well_founded_iff, well_founded.well_founded_iff_has_min]
+
+end is_well_founded
+
+namespace well_founded_lt
+section has_lt
+variables [has_lt α] [h : well_founded_lt α]
+
+/-- If `<` is well-founded, then any nonempty set has a minimal element.
+
+If you're working with a nonempty linear order, consider defining a
+`conditionally_complete_linear_order_bot` instance via
+`well_founded.conditionally_complete_linear_order_with_bot` and using `Inf` instead.-/
+theorem has_min' : ∀ s : set α, s.nonempty → ∃ a ∈ s, ∀ x ∈ s, ¬ x < a := h.wf.has_min
+
+theorem well_founded_lt_iff_has_min' {α : Type*} [has_lt α] : well_founded_lt α ↔
+  ∀ s : set α, s.nonempty → ∃ m ∈ s, ∀ x ∈ s, ¬ x < m :=
+is_well_founded.is_well_founded_iff_has_min
+
+end has_lt
+
+section linear_order
+variables [linear_order α] [well_founded_lt α]
+
+/-- If `<` is well-founded, then any nonempty set has a minimal element. -/
+theorem has_min : ∀ s : set α, s.nonempty → ∃ a ∈ s, ∀ x ∈ s, a ≤ x :=
+by { simp_rw ←not_lt, exact has_min' }
+
+theorem well_founded_lt_iff_has_min {α : Type*} [linear_order α] : well_founded_lt α ↔
+  ∀ s : set α, s.nonempty → ∃ m ∈ s, ∀ x ∈ s, m ≤ x :=
+by { simp_rw ←not_lt, exact well_founded_lt_iff_has_min' }
+
+end linear_order
+end well_founded_lt
+
+namespace well_founded_gt
+section has_lt
+variables [has_lt α] [h : well_founded_gt α]
+
+/-- If `>` is well-founded, then any nonempty set has a maximal element. -/
+theorem has_max' : ∀ s : set α, s.nonempty → ∃ a ∈ s, ∀ x ∈ s, ¬ a < x :=
+h.wf.has_min
+
+theorem well_founded_gt_iff_has_max' {α : Type*} [has_lt α] : well_founded_gt α ↔
+  ∀ s : set α, s.nonempty → ∃ m ∈ s, ∀ x ∈ s, ¬ m < x :=
+is_well_founded.is_well_founded_iff_has_min
+
+end has_lt
+
+section linear_order
+variables [linear_order α] [well_founded_gt α]
+
+/-- If `>` is well-founded, then any nonempty set has a maximal element. -/
+theorem has_max : ∀ s : set α, s.nonempty → ∃ a ∈ s, ∀ x ∈ s, x ≤ a :=
+by { simp_rw ←not_lt, exact has_max' }
+
+theorem well_founded_gt_iff_has_max {α : Type*} [linear_order α] : well_founded_gt α ↔
+  ∀ s : set α, s.nonempty → ∃ m ∈ s, ∀ x ∈ s, x ≤ m :=
+by { simp_rw ←not_lt, exact well_founded_gt_iff_has_max' }
+
+end linear_order
+end well_founded_gt
+
+/-! ### Suprema and successors -/
+
+-- TODO: a lot of the following should either be ported to `well_founded_lt` and `well_founded_gt`,
+-- or removed outright.
+
+namespace well_founded
 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
+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
+min_mem wf { x | ∀ a ∈ s, r a x } h x hx
 
-section
+section classical
 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
+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) :
+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)
+end classical
+
+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,
@@ -148,6 +214,8 @@ end linear_order
 
 end well_founded
 
+/-! ### Minimum argument of function -/
+
 namespace function
 
 variables {β : Type*} (f : α → β)
@@ -196,6 +264,8 @@ end linear_order
 
 end function
 
+/-! ### Induction principles -/
+
 section induction
 
 /-- Let `r` be a relation on `α`, let `f : α → β` be a function, let `C : β → Prop`, and

src/set_theory/zfc/basic.lean

@@ -217,7 +217,6 @@ end⟩
 theorem mem_wf : @well_founded pSet (∈) := ⟨λ x, mem_wf_aux $ equiv.refl x⟩
 
 instance : has_well_founded pSet := ⟨_, mem_wf⟩
-instance : is_asymm pSet (∈) := mem_wf.is_asymm
 
 theorem mem_asymm {x y : pSet} : x ∈ y → y ∉ x := asymm
 theorem mem_irrefl (x : pSet) : x ∉ x := irrefl x
@@ -774,8 +773,6 @@ mem_wf.induction x h
 
 instance : has_well_founded Set := ⟨_, mem_wf⟩
 
-instance : is_asymm Set (∈) := mem_wf.is_asymm
-
 theorem mem_asymm {x y : Set} : x ∈ y → y ∉ x := asymm
 theorem mem_irrefl (x : Set) : x ∉ x := irrefl x
 
@@ -1009,7 +1006,6 @@ theorem mem_wf : @well_founded Class.{u} (∈) :=
 end⟩
 
 instance : has_well_founded Class := ⟨_, mem_wf⟩
-instance : is_asymm Class (∈) := mem_wf.is_asymm
 
 theorem mem_asymm {x y : Class} : x ∈ y → y ∉ x := asymm
 theorem mem_irrefl (x : Class) : x ∉ x := irrefl x