feat(order/rel_classes): housekeeping

src/logic/hydra.lean

@@ -136,7 +136,8 @@ begin
 end
 
 /-- `cut_expand r` is well-founded when `r` is. -/
-theorem _root_.well_founded.cut_expand (hr : well_founded r) : well_founded (cut_expand r) :=
-⟨by { letI h := hr.is_irrefl, exact λ s, acc_of_singleton $ λ a _, (hr.apply a).cut_expand }⟩
+instance _root_.is_well_founded.cut_expand [is_well_founded α r] :
+  is_well_founded _ (cut_expand r) :=
+⟨⟨λ s, acc_of_singleton $ λ a _, (is_well_founded.apply r a).cut_expand⟩⟩
 
 end relation

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

@@ -25,18 +25,6 @@ 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)
-
-instance {α : Sort*} [has_well_founded α] : is_irrefl α has_well_founded.r :=
-is_asymm.is_irrefl
-
 /-- 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)
@@ -61,7 +49,7 @@ 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) :=
 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, _⟩⟩,
@@ -73,28 +61,31 @@ begin
 end
 
 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,

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