feat(order/well_founded_set): Higman's Lemma (#7212)

Proves Higman's Lemma: if `r` is partially well-ordered on `s`, then `list.sublist_forall2` is partially well-ordered on the set of lists whose elements are in `s`.

docs/references.bib

@@ -453,6 +453,17 @@ @Article{         Haze09
   pages         = {319–472}
 }
 
+@Article{         Higman52,
+  author        = {Higman, Graham},
+  title         = {Ordering by Divisibility in Abstract Algebras},
+  journal       = {Proceedings of the London Mathematical Society},
+  volume        = {s3-2},
+  number        = {1},
+  pages         = {326-336},
+  doi           = {https://doi.org/10.1112/plms/s3-2.1.326},
+  year          = {1952}
+}
+
 @Book{            Hofstadter-1979,
   author        = "Douglas R Hofstadter",
   title         = "{{G}ödel, {E}scher, {B}ach: an eternal golden braid}",
@@ -724,6 +735,18 @@ @Article{         MR577178
   url           = {https://doi.org/10.1007/BF00417500}
 }
 
+@Article{         Nash-Williams63,
+  title         = {On well-quasi-ordering finite trees},
+  volume        = {59},
+  DOI           = {10.1017/S0305004100003844},
+  number        = {4},
+  journal       = {Mathematical Proceedings of the Cambridge Philosophical Society},
+  publisher     = {Cambridge University Press},
+  author        = {Nash-Williams, C. St. J. A.},
+  year          = {1963},
+  pages         = {833–835}
+}
+
 @Article{         orosi2018faulhaber,
   author        = {Greg {Orosi}},
   title         = {{A simple derivation of Faulhaber's formula}},

src/order/well_founded_set.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Aaron Anderson
 -/
 import data.set.finite
-import data.fintype.basic
 import order.well_founded
 import order.order_iso_nat
 import algebra.pointwise
@@ -18,8 +17,10 @@ A well-founded subset of an ordered type is one on which the relation `<` is wel
  * `set.well_founded_on s r` indicates that the relation `r` is
   well-founded when restricted to the set `s`.
  * `set.is_wf s` indicates that `<` is well-founded when restricted to `s`.
+ * `set.partially_well_ordered_on s r` indicates that the relation `r` is
+  partially well-ordered (also known as well quasi-ordered) when restricted to the set `s`.
  * `set.is_pwo s` indicates that any infinite sequence of elements in `s`
-  contains an infinite monotone subsequence.
+  contains an infinite monotone subsequence. Note that
 
 ### Definitions for Hahn Series
  * `set.add_antidiagonal s t a` and `set.mul_antidiagonal s t a` are the sets of pairs of elements
@@ -28,12 +29,19 @@ A well-founded subset of an ordered type is one on which the relation `<` is wel
   `set.add_antidiagonal` and `set.mul_antidiagonal` defined when `s` and `t` are well-founded.
 
 ## Main Results
+ * Higman's Lemma, `set.partially_well_ordered_on.partially_well_ordered_on_sublist_forall₂`,
+  shows that if `r` is partially well-ordered on `s`, then `list.sublist_forall₂` is partially
+  well-ordered on the set of lists of elements of `s`. The result was originally published by
+  Higman, but this proof more closely follows Nash-Williams.
  * `set.well_founded_on_iff` relates `well_founded_on` to the well-foundedness of a relation on the
  original type, to avoid dealing with subtypes.
  * `set.is_wf.mono` shows that a subset of a well-founded subset is well-founded.
  * `set.is_wf.union` shows that the union of two well-founded subsets is well-founded.
  * `finset.is_wf` shows that all `finset`s are well-founded.
 
+## References
+ * [Higman, *Ordering by Divisibility in Abstract Algebras*][Higman52]
+ * [Nash-Williams, *On Well-Quasi-Ordering Finite Trees*][Nash-Williams63]
 -/
 
 variables {α : Type*}
@@ -332,7 +340,7 @@ end set
 namespace finset
 
 @[simp]
-theorem partially_well_ordered_on {r : α → α → Prop} [is_refl α r] {f : finset α} :
+theorem partially_well_ordered_on {r : α → α → Prop} [is_refl α r] (f : finset α) :
   set.partially_well_ordered_on (↑f : set α) r :=
 begin
   intros g hg,
@@ -349,12 +357,12 @@ begin
 end
 
 @[simp]
-theorem is_pwo [partial_order α] {f : finset α} :
+theorem is_pwo [partial_order α] (f : finset α) :
   set.is_pwo (↑f : set α) :=
-finset.partially_well_ordered_on
+f.partially_well_ordered_on
 
 @[simp]
-theorem well_founded_on {r : α → α → Prop} [is_strict_order α r] {f : finset α} :
+theorem well_founded_on {r : α → α → Prop} [is_strict_order α r] (f : finset α) :
   set.well_founded_on (↑f : set α) r :=
 begin
   rw [set.well_founded_on_iff_no_descending_seq],
@@ -364,8 +372,8 @@ begin
 end
 
 @[simp]
-theorem is_wf [partial_order α] {f : finset α} : set.is_wf (↑f : set α) :=
-finset.is_pwo.is_wf
+theorem is_wf [partial_order α] (f : finset α) : set.is_wf (↑f : set α) :=
+f.is_pwo.is_wf
 
 end finset
 
@@ -375,7 +383,7 @@ variables [partial_order α] {s : set α} {a : α}
 theorem finite.is_pwo (h : s.finite) : s.is_pwo :=
 begin
   rw ← h.coe_to_finset,
-  exact finset.is_pwo,
+  exact h.to_finset.is_pwo,
 end
 
 @[simp]
@@ -499,6 +507,133 @@ end
 end set
 
 namespace set
+namespace partially_well_ordered_on
+
+/-- In the context of partial well-orderings, a bad sequence is a nonincreasing sequence
+  whose range is contained in a particular set `s`. One exists if and only if `s` is not
+  partially well-ordered. -/
+def is_bad_seq (r : α → α → Prop) (s : set α) (f : ℕ → α) : Prop :=
+set.range f ⊆ s ∧ ∀ (m n : ℕ), m < n → ¬ r (f m) (f n)
+
+lemma iff_forall_not_is_bad_seq (r : α → α → Prop) (s : set α) :
+  s.partially_well_ordered_on r ↔
+    ∀ f, ¬ is_bad_seq r s f :=
+begin
+  rw [set.partially_well_ordered_on],
+  apply forall_congr (λ f, _),
+  simp [is_bad_seq]
+end
+
+/-- This indicates that every bad sequence `g` that agrees with `f` on the first `n`
+  terms has `rk (f n) ≤ rk (g n)`. -/
+def is_min_bad_seq (r : α → α → Prop) (rk : α → ℕ) (s : set α) (n : ℕ) (f : ℕ → α) : Prop :=
+  ∀ g : ℕ → α, (∀ (m : ℕ), m < n → f m = g m) → rk (g n) < rk (f n) → ¬ is_bad_seq r s g
+
+/-- Given a bad sequence `f`, this constructs a bad sequence that agrees with `f` on the first `n`
+  terms and is minimal at `n`.
+-/
+noncomputable def min_bad_seq_of_bad_seq (r : α → α → Prop) (rk : α → ℕ) (s : set α)
+  (n : ℕ) (f : ℕ → α) (hf : is_bad_seq r s f) :
+  { g : ℕ → α // (∀ (m : ℕ), m < n → f m = g m) ∧ is_bad_seq r s g ∧ is_min_bad_seq r rk s n g } :=
+begin
+  classical,
+  have h : ∃ (k : ℕ) (g : ℕ → α), (∀ m, m < n → f m = g m) ∧ is_bad_seq r s g
+        ∧ rk (g n) = k :=
+  ⟨_, f, λ _ _, rfl, hf, rfl⟩,
+  obtain ⟨h1, h2, h3⟩ := classical.some_spec (nat.find_spec h),
+  refine ⟨classical.some (nat.find_spec h), h1, by convert h2, λ g hg1 hg2 con, _⟩,
+  refine nat.find_min h _ ⟨g, λ m mn, (h1 m mn).trans (hg1 m mn), by convert con, rfl⟩,
+  rwa ← h3,
+end
+
+lemma exists_min_bad_of_exists_bad (r : α → α → Prop) (rk : α → ℕ) (s : set α) :
+  (∃ f, is_bad_seq r s f) → ∃ f, is_bad_seq r s f ∧ ∀ n, is_min_bad_seq r rk s n f :=
+begin
+  rintro ⟨f0, (hf0 : is_bad_seq r s f0)⟩,
+  let fs : Π (n : ℕ), { f :  ℕ → α // is_bad_seq r s f ∧ is_min_bad_seq r rk s n f },
+  { refine nat.rec _ _,
+    { exact ⟨(min_bad_seq_of_bad_seq r rk s 0 f0 hf0).1,
+        (min_bad_seq_of_bad_seq r rk s 0 f0 hf0).2.2⟩, },
+    { exact λ n fn, ⟨(min_bad_seq_of_bad_seq r rk s (n + 1) fn.1 fn.2.1).1,
+        (min_bad_seq_of_bad_seq r rk s (n + 1) fn.1 fn.2.1).2.2⟩ } },
+  have h : ∀ m n, m ≤ n → (fs m).1 m = (fs n).1 m,
+  { intros m n mn,
+    obtain ⟨k, rfl⟩ := exists_add_of_le mn,
+    clear mn,
+    induction k with k ih,
+    { refl },
+    rw [ih, ((min_bad_seq_of_bad_seq r rk s (m + k).succ (fs (m + k)).1 (fs (m + k)).2.1).2.1 m
+        (nat.lt_succ_iff.2 (nat.add_le_add_left k.zero_le m)))],
+    refl },
+  refine ⟨λ n, (fs n).1 n, ⟨set.range_subset_iff.2 (λ n, ((fs n).2).1.1 (mem_range_self n)),
+    λ m n mn, _⟩, λ n g hg1 hg2, _⟩,
+  { dsimp,
+    rw [← subtype.val_eq_coe, h m n (le_of_lt mn)],
+    convert (fs n).2.1.2 m n mn },
+  { convert (fs n).2.2 g (λ m mn, eq.trans _ (hg1 m mn)) (lt_of_lt_of_le hg2 (le_refl _)),
+    rw ← h m n (le_of_lt mn) },
+end
+
+lemma iff_not_exists_is_min_bad_seq {r : α → α → Prop} (rk : α → ℕ) {s : set α} :
+  s.partially_well_ordered_on r ↔ ¬ ∃ f, is_bad_seq r s f ∧ ∀ n, is_min_bad_seq r rk s n f :=
+begin
+  rw [iff_forall_not_is_bad_seq, ← not_exists, not_congr],
+  split,
+  { apply exists_min_bad_of_exists_bad },
+  rintro ⟨f, hf1, hf2⟩,
+  exact ⟨f, hf1⟩,
+end
+
+/-- Higman's Lemma, which states that for any reflexive, transitive relation `r` which is
+  partially well-ordered on a set `s`, the relation `list.sublist_forall₂ r` is partially
+  well-ordered on the set of lists of elements of `s`. That relation is defined so that
+  `list.sublist_forall₂ r l₁ l₂` whenever `l₁` related pointwise by `r` to a sublist of `l₂`.  -/
+lemma partially_well_ordered_on_sublist_forall₂ (r : α → α → Prop) [is_refl α r] [is_trans α r]
+  {s : set α} (h : s.partially_well_ordered_on r) :
+  { l : list α | ∀ x, x ∈ l → x ∈ s }.partially_well_ordered_on (list.sublist_forall₂ r) :=
+begin
+  rcases s.eq_empty_or_nonempty with rfl | ⟨as, has⟩,
+  { apply partially_well_ordered_on.mono (finset.partially_well_ordered_on {list.nil}),
+    { intros l hl,
+      rw [finset.mem_coe, finset.mem_singleton, list.eq_nil_iff_forall_not_mem],
+      exact hl, },
+    apply_instance },
+  haveI : inhabited α := ⟨as⟩,
+  rw [iff_not_exists_is_min_bad_seq (list.length)],
+  rintro ⟨f, hf1, hf2⟩,
+  have hnil : ∀ n, f n ≠ list.nil :=
+    λ n con, (hf1).2 n n.succ n.lt_succ_self (con.symm ▸ list.sublist_forall₂.nil),
+  obtain ⟨g, hg⟩ := h.exists_monotone_subseq (list.head ∘ f) _,
+  swap, { simp only [set.range_subset_iff, function.comp_apply],
+    exact λ n, hf1.1 (set.mem_range_self n) _ (list.head_mem_self (hnil n)) },
+  have hf' := hf2 (g 0) (λ n, if n < g 0 then f n else list.tail (f (g (n - g 0))))
+    (λ m hm, (if_pos hm).symm) _,
+  swap, { simp only [if_neg (lt_irrefl (g 0)), nat.sub_self],
+    rw [list.length_tail, ← nat.pred_eq_sub_one],
+    exact nat.pred_lt (λ con, hnil _ (list.length_eq_zero.1 con)) },
+  rw [is_bad_seq] at hf',
+  push_neg at hf',
+  obtain ⟨m, n, mn, hmn⟩ := hf' _,
+  swap, { rw set.range_subset_iff,
+    rintro n x hx,
+    split_ifs at hx with hn hn,
+    { exact hf1.1 (set.mem_range_self _) _ hx },
+    { refine hf1.1 (set.mem_range_self _) _ (list.tail_subset _ hx), } },
+  by_cases hn : n < g 0,
+  { apply hf1.2 m n mn,
+    rwa [if_pos hn, if_pos (mn.trans hn)] at hmn },
+  { obtain ⟨n', rfl⟩ := le_iff_exists_add.1 (not_lt.1 hn),
+    rw [if_neg hn, add_comm (g 0) n', nat.add_sub_cancel] at hmn,
+    split_ifs at hmn with hm hm,
+    { apply hf1.2 m (g n') (lt_of_lt_of_le hm (g.monotone n'.zero_le)),
+      exact trans hmn (list.tail_sublist_forall₂_self _) },
+    { rw [← (nat.sub_lt_left_iff_lt_add (le_of_not_lt hm))] at mn,
+      apply hf1.2 _ _ (g.lt_iff_lt.2 mn),
+      rw [← list.cons_head_tail (hnil (g (m - g 0))), ← list.cons_head_tail (hnil (g n'))],
+      exact list.sublist_forall₂.cons (hg _ _ (le_of_lt mn)) hmn, } }
+end
+
+end partially_well_ordered_on
 
 /-- `set.mul_antidiagonal s t a` is the set of all pairs of an element in `s` and an element in `t`
   that multiply to `a`. -/