feat(logic/relation): characterization of the accessible predicate in…

… terms of `well_founded_on` (#16720)

+ Show that `acc r a` (read: `a` is accessible under the relation `r`) if and only if `r` is well-founded on the subset of elements below `a` (transitively) under `r`, including (`refl_trans_gen`) or excluding (`trans_gen`) `a`. Stated as a `list.tfae`.

+ Move `relation.fibration` (used by the proof) to *logic/relation* to avoid importing *logic/hydra*. Add lemma `acc_trans_gen_iff` used in the proof.

src/logic/hydra.lean

@@ -5,7 +5,6 @@ Authors: Junyan Xu
 -/
 import data.multiset.basic
 import order.game_add
-import order.well_founded
 
 /-!
 # Termination of a hydra game
@@ -24,47 +23,18 @@ valid "moves" of the game are modelled by the relation `cut_expand r` on `multis
 `cut_expand r s' s` is true iff `s'` is obtained by removing one head `a ∈ s` and
 adding back an arbitrary multiset `t` of heads such that all `a' ∈ t` satisfy `r a' a`.
 
-To prove this theorem, we follow the proof by Peter LeFanu Lumsdaine at
-https://mathoverflow.net/a/229084/3332, and along the way we introduce the notion of `fibration`
-of relations.
+We follow the proof by Peter LeFanu Lumsdaine at https://mathoverflow.net/a/229084/3332.
 
 TODO: formalize the relations corresponding to more powerful (e.g. Kirby–Paris and Buchholz)
 hydras, and prove their well-foundedness.
 -/
 
 namespace relation
 
-variables {α β : Type*}
-
-section fibration
-variables (rα : α → α → Prop) (rβ : β → β → Prop) (f : α → β)
-
-/-- A function `f : α → β` is a fibration between the relation `rα` and `rβ` if for all
-  `a : α` and `b : β`, whenever `b : β` and `f a` are related by `rβ`, `b` is the image
-  of some `a' : α` under `f`, and `a'` and `a` are related by `rα`. -/
-def fibration := ∀ ⦃a b⦄, rβ b (f a) → ∃ a', rα a' a ∧ f a' = b
-
-variables {rα rβ}
-
-/-- If `f : α → β` is a fibration between relations `rα` and `rβ`, and `a : α` is
-  accessible under `rα`, then `f a` is accessible under `rβ`. -/
-lemma _root_.acc.of_fibration (fib : fibration rα rβ f) {a} (ha : acc rα a) : acc rβ (f a) :=
-begin
-  induction ha with a ha ih,
-  refine acc.intro (f a) (λ b hr, _),
-  obtain ⟨a', hr', rfl⟩ := fib hr,
-  exact ih a' hr',
-end
-
-lemma _root_.acc.of_downward_closed (dc : ∀ {a b}, rβ b (f a) → b ∈ set.range f)
-  (a : α) (ha : acc (inv_image rβ f) a) : acc rβ (f a) :=
-ha.of_fibration f (λ a b h, let ⟨a', he⟩ := dc h in ⟨a', he.substr h, he⟩)
-
-end fibration
-
-section hydra
 open multiset prod
 
+variables {α β : Type*}
+
 /-- The relation that specifies valid moves in our hydra game. `cut_expand r s' s`
   means that `s'` is obtained by removing one head `a ∈ s` and adding back an arbitrary
   multiset `t` of heads such that all `a' ∈ t` satisfy `r a' a`.
@@ -152,6 +122,5 @@ 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 }⟩
-end hydra
 
 end relation

src/logic/relation.lean

@@ -147,6 +147,33 @@ end
 
 end comp
 
+section fibration
+
+variables (rα : α → α → Prop) (rβ : β → β → Prop) (f : α → β)
+
+/-- A function `f : α → β` is a fibration between the relation `rα` and `rβ` if for all
+  `a : α` and `b : β`, whenever `b : β` and `f a` are related by `rβ`, `b` is the image
+  of some `a' : α` under `f`, and `a'` and `a` are related by `rα`. -/
+def fibration := ∀ ⦃a b⦄, rβ b (f a) → ∃ a', rα a' a ∧ f a' = b
+
+variables {rα rβ}
+
+/-- If `f : α → β` is a fibration between relations `rα` and `rβ`, and `a : α` is
+  accessible under `rα`, then `f a` is accessible under `rβ`. -/
+lemma _root_.acc.of_fibration (fib : fibration rα rβ f) {a} (ha : acc rα a) : acc rβ (f a) :=
+begin
+  induction ha with a ha ih,
+  refine acc.intro (f a) (λ b hr, _),
+  obtain ⟨a', hr', rfl⟩ := fib hr,
+  exact ih a' hr',
+end
+
+lemma _root_.acc.of_downward_closed (dc : ∀ {a b}, rβ b (f a) → ∃ c, f c = b)
+  (a : α) (ha : acc (inv_image rβ f) a) : acc rβ (f a) :=
+ha.of_fibration f (λ a b h, let ⟨a', he⟩ := dc h in ⟨a', he.substr h, he⟩)
+
+end fibration
+
 /--
 The map of a relation `r` through a pair of functions pushes the
 relation to the codomains of the functions.  The resulting relation is
@@ -373,16 +400,19 @@ end
 
 end trans_gen
 
-lemma _root_.acc.trans_gen {α} {r : α → α → Prop} {a : α} (h : acc r a) : acc (trans_gen r) a :=
+lemma _root_.acc.trans_gen (h : acc r a) : acc (trans_gen r) a :=
 begin
   induction h with x _ H,
   refine acc.intro x (λ y hy, _),
   cases hy with _ hyx z _ hyz hzx,
   exacts [H y hyx, (H z hzx).inv hyz],
 end
 
-lemma _root_.well_founded.trans_gen {α} {r : α → α → Prop} (h : well_founded r) :
-  well_founded (trans_gen r) := ⟨λ a, (h.apply a).trans_gen⟩
+lemma _root_.acc_trans_gen_iff : acc (trans_gen r) a ↔ acc r a :=
+⟨subrelation.accessible (λ _ _, trans_gen.single), acc.trans_gen⟩
+
+lemma _root_.well_founded.trans_gen (h : well_founded r) : well_founded (trans_gen r) :=
+⟨λ a, (h.apply a).trans_gen⟩
 
 section trans_gen
 

src/order/well_founded_set.lean

@@ -6,6 +6,7 @@ Authors: Aaron Anderson
 import order.antichain
 import order.order_iso_nat
 import order.well_founded
+import tactic.tfae
 
 /-!
 # Well-founded sets
@@ -96,6 +97,28 @@ end
 
 lemma subset (h : t.well_founded_on r) (hst : s ⊆ t) : s.well_founded_on r := h.mono le_rfl hst
 
+open relation
+
+/-- `a` is accessible under the relation `r` iff `r` is well-founded on the downward transitive
+  closure of `a` under `r` (including `a` or not). -/
+lemma acc_iff_well_founded_on {α} {r : α → α → Prop} {a : α} :
+  [ acc r a,
+    {b | refl_trans_gen r b a}.well_founded_on r,
+    {b | trans_gen r b a}.well_founded_on r ].tfae :=
+begin
+  tfae_have : 1 → 2,
+  { refine λ h, ⟨λ b, _⟩, apply inv_image.accessible,
+    rw ← acc_trans_gen_iff at h ⊢,
+    obtain h'|h' := refl_trans_gen_iff_eq_or_trans_gen.1 b.2,
+    { rwa h' at h }, { exact h.inv h' } },
+  tfae_have : 2 → 3,
+  { exact λ h, h.subset (λ _, trans_gen.to_refl) },
+  tfae_have : 3 → 1,
+  { refine λ h, acc.intro _ (λ b hb, (h.apply ⟨b, trans_gen.single hb⟩).of_fibration subtype.val _),
+    exact λ ⟨c, hc⟩ d h, ⟨⟨d, trans_gen.head h hc⟩, h, rfl⟩ },
+  tfae_finish,
+end
+
 end well_founded_on
 end any_rel