|
| 1 | +/- |
| 2 | +Copyright (c) 2022 Junyan Xu. All rights reserved. |
| 3 | +Released under Apache 2.0 license as described in the file LICENSE. |
| 4 | +Authors: Junyan Xu |
| 5 | +-/ |
| 6 | +import data.dfinsupp.lex |
| 7 | +import order.game_add |
| 8 | +import order.antisymmetrization |
| 9 | +import set_theory.ordinal.basic |
| 10 | + |
| 11 | +/-! |
| 12 | +# Well-foundedness of the lexicographic and product orders on `dfinsupp` and `pi` |
| 13 | +
|
| 14 | +The primary results are `dfinsupp.lex.well_founded` and the two variants that follow it, |
| 15 | +which essentially say that if `(>)` is a well order on `ι`, `(<)` is well-founded on each |
| 16 | +`α i`, and `0` is a bottom element in `α i`, then the lexicographic `(<)` is well-founded |
| 17 | +on `Π₀ i, α i`. The proof is modelled on the proof of `well_founded.cut_expand`. |
| 18 | +
|
| 19 | +The results are used to prove `pi.lex.well_founded` and two variants, which say that if |
| 20 | +`ι` is finite and equipped with a linear order and `(<)` is well-founded on each `α i`, |
| 21 | +then the lexicographic `(<)` is well-founded on `Π i, α i`, and the same is true for |
| 22 | +`Π₀ i, α i` (`dfinsupp.lex.well_founded_of_finite`), because `dfinsupp` is order-isomorphic |
| 23 | +to `pi` when `ι` is finite. |
| 24 | +
|
| 25 | +Finally, we deduce `dfinsupp.well_founded_lt`, `pi.well_founded_lt`, |
| 26 | +`dfinsupp.well_founded_lt_of_finite` and variants, which concern the product order |
| 27 | +rather than the lexicographic one. An order on `ι` is not required in these results, |
| 28 | +but we deduce them from the well-foundedness of the lexicographic order by choosing |
| 29 | +a well order on `ι` so that the product order `(<)` becomes a subrelation |
| 30 | +of the lexicographic `(<)`. |
| 31 | +
|
| 32 | +All results are provided in two forms whenever possible: a general form where the relations |
| 33 | +can be arbitrary (not the `(<)` of a preorder, or not even transitive, etc.) and a specialized |
| 34 | +form provided as `well_founded_lt` instances where the `(d)finsupp/pi` type (or their `lex` |
| 35 | +type synonyms) carries a natural `(<)`. |
| 36 | +
|
| 37 | +Notice that the definition of `dfinsupp.lex` says that `x < y` according to `dfinsupp.lex r s` |
| 38 | +iff there exists a coordinate `i : ι` such that `x i < y i` according to `s i`, and at all |
| 39 | +`r`-smaller coordinates `j` (i.e. satisfying `r j i`), `x` remains unchanged relative to `y`; |
| 40 | +in other words, coordinates `j` such that `¬ r j i` and `j ≠ i` are exactly where changes |
| 41 | +can happen arbitrarily. This explains the appearance of `rᶜ ⊓ (≠)` in |
| 42 | +`dfinsupp.acc_single` and `dfinsupp.well_founded`. When `r` is trichotomous (e.g. the `(<)` |
| 43 | +of a linear order), `¬ r j i ∧ j ≠ i` implies `r i j`, so it suffices to require `r.swap` |
| 44 | +to be well-founded. |
| 45 | +-/ |
| 46 | + |
| 47 | +variables {ι : Type*} {α : ι → Type*} |
| 48 | + |
| 49 | +namespace dfinsupp |
| 50 | + |
| 51 | +variables [hz : Π i, has_zero (α i)] (r : ι → ι → Prop) (s : Π i, α i → α i → Prop) |
| 52 | +include hz |
| 53 | + |
| 54 | +open relation prod |
| 55 | + |
| 56 | +/-- This key lemma says that if a finitely supported dependent function `x₀` is obtained by merging |
| 57 | + two such functions `x₁` and `x₂`, and if we evolve `x₀` down the `dfinsupp.lex` relation one |
| 58 | + step and get `x`, we can always evolve one of `x₁` and `x₂` down the `dfinsupp.lex` relation |
| 59 | + one step while keeping the other unchanged, and merge them back (possibly in a different way) |
| 60 | + to get back `x`. In other words, the two parts evolve essentially independently under |
| 61 | + `dfinsupp.lex`. This is used to show that a function `x` is accessible if |
| 62 | + `dfinsupp.single i (x i)` is accessible for each `i` in the (finite) support of `x` |
| 63 | + (`dfinsupp.lex.acc_of_single`). -/ |
| 64 | +lemma lex_fibration [Π i (s : set ι), decidable (i ∈ s)] : fibration |
| 65 | + (inv_image (game_add (dfinsupp.lex r s) (dfinsupp.lex r s)) snd) |
| 66 | + (dfinsupp.lex r s) |
| 67 | + (λ x, piecewise x.2.1 x.2.2 x.1) := |
| 68 | +begin |
| 69 | + rintro ⟨p, x₁, x₂⟩ x ⟨i, hr, hs⟩, |
| 70 | + simp_rw [piecewise_apply] at hs hr, |
| 71 | + split_ifs at hs, classical, |
| 72 | + work_on_goal 1 |
| 73 | + { refine ⟨⟨{j | r j i → j ∈ p}, piecewise x₁ x {j | r j i}, x₂⟩, game_add.fst ⟨i, _⟩, _⟩ }, |
| 74 | + work_on_goal 3 |
| 75 | + { refine ⟨⟨{j | r j i ∧ j ∈ p}, x₁, piecewise x₂ x {j | r j i}⟩, game_add.snd ⟨i, _⟩, _⟩ }, |
| 76 | + swap 3, iterate 2 |
| 77 | + { simp_rw piecewise_apply, |
| 78 | + refine ⟨λ j h, if_pos h, _⟩, |
| 79 | + convert hs, |
| 80 | + refine ite_eq_right_iff.2 (λ h', (hr i h').symm ▸ _), |
| 81 | + rw if_neg h <|> rw if_pos h }, |
| 82 | + all_goals { ext j, simp_rw piecewise_apply, split_ifs with h₁ h₂ }, |
| 83 | + { rw [hr j h₂, if_pos (h₁ h₂)] }, |
| 84 | + { refl }, |
| 85 | + { rw [set.mem_set_of, not_imp] at h₁, rw [hr j h₁.1, if_neg h₁.2] }, |
| 86 | + { rw [hr j h₁.1, if_pos h₁.2] }, |
| 87 | + { rw [hr j h₂, if_neg (λ h', h₁ ⟨h₂, h'⟩)] }, |
| 88 | + { refl }, |
| 89 | +end |
| 90 | + |
| 91 | +variables {r s} |
| 92 | + |
| 93 | +lemma lex.acc_of_single_erase [decidable_eq ι] {x : Π₀ i, α i} (i : ι) |
| 94 | + (hs : acc (dfinsupp.lex r s) $ single i (x i)) |
| 95 | + (hu : acc (dfinsupp.lex r s) $ x.erase i) : acc (dfinsupp.lex r s) x := |
| 96 | +begin |
| 97 | + classical, |
| 98 | + convert ← @acc.of_fibration _ _ _ _ _ |
| 99 | + (lex_fibration r s) ⟨{i}, _⟩ (inv_image.accessible snd $ hs.prod_game_add hu), |
| 100 | + convert piecewise_single_erase x i, |
| 101 | +end |
| 102 | + |
| 103 | +variable (hbot : ∀ ⦃i a⦄, ¬ s i a 0) |
| 104 | +include hbot |
| 105 | + |
| 106 | +lemma lex.acc_zero : acc (dfinsupp.lex r s) 0 := acc.intro 0 $ λ x ⟨_, _, h⟩, (hbot h).elim |
| 107 | + |
| 108 | +lemma lex.acc_of_single [decidable_eq ι] [Π i (x : α i), decidable (x ≠ 0)] (x : Π₀ i, α i) : |
| 109 | + (∀ i ∈ x.support, acc (dfinsupp.lex r s) $ single i (x i)) → acc (dfinsupp.lex r s) x := |
| 110 | +begin |
| 111 | + generalize ht : x.support = t, revert x, classical, |
| 112 | + induction t using finset.induction with b t hb ih, |
| 113 | + { intros x ht, rw support_eq_empty.1 ht, exact λ _, lex.acc_zero hbot }, |
| 114 | + refine λ x ht h, lex.acc_of_single_erase b (h b $ t.mem_insert_self b) _, |
| 115 | + refine ih _ (by rw [support_erase, ht, finset.erase_insert hb]) (λ a ha, _), |
| 116 | + rw [erase_ne (ha.ne_of_not_mem hb)], |
| 117 | + exact h a (finset.mem_insert_of_mem ha), |
| 118 | +end |
| 119 | + |
| 120 | +variable (hs : ∀ i, well_founded (s i)) |
| 121 | +include hs |
| 122 | + |
| 123 | +lemma lex.acc_single [decidable_eq ι] {i : ι} (hi : acc (rᶜ ⊓ (≠)) i) : |
| 124 | + ∀ a, acc (dfinsupp.lex r s) (single i a) := |
| 125 | +begin |
| 126 | + induction hi with i hi ih, |
| 127 | + refine λ a, (hs i).induction a (λ a ha, _), |
| 128 | + refine acc.intro _ (λ x, _), |
| 129 | + rintro ⟨k, hr, hs⟩, classical, |
| 130 | + rw single_apply at hs, |
| 131 | + split_ifs at hs with hik, |
| 132 | + swap, { exact (hbot hs).elim }, subst hik, |
| 133 | + refine lex.acc_of_single hbot x (λ j hj, _), |
| 134 | + obtain rfl | hij := eq_or_ne i j, { exact ha _ hs }, |
| 135 | + by_cases r j i, |
| 136 | + { rw [hr j h, single_eq_of_ne hij, single_zero], exact lex.acc_zero hbot }, |
| 137 | + { exact ih _ ⟨h, hij.symm⟩ _ }, |
| 138 | +end |
| 139 | + |
| 140 | +lemma lex.acc [decidable_eq ι] [Π i (x : α i), decidable (x ≠ 0)] (x : Π₀ i, α i) |
| 141 | + (h : ∀ i ∈ x.support, acc (rᶜ ⊓ (≠)) i) : acc (dfinsupp.lex r s) x := |
| 142 | +lex.acc_of_single hbot x $ λ i hi, lex.acc_single hbot hs (h i hi) _ |
| 143 | + |
| 144 | +theorem lex.well_founded (hr : well_founded $ rᶜ ⊓ (≠)) : well_founded (dfinsupp.lex r s) := |
| 145 | +⟨λ x, by classical; exact lex.acc hbot hs x (λ i _, hr.apply i)⟩ |
| 146 | + |
| 147 | +theorem lex.well_founded' [is_trichotomous ι r] |
| 148 | + (hr : well_founded r.swap) : well_founded (dfinsupp.lex r s) := |
| 149 | +lex.well_founded hbot hs $ subrelation.wf |
| 150 | + (λ i j h, ((@is_trichotomous.trichotomous ι r _ i j).resolve_left h.1).resolve_left h.2) hr |
| 151 | + |
| 152 | +omit hz hbot hs |
| 153 | + |
| 154 | +instance lex.well_founded_lt [has_lt ι] [is_trichotomous ι (<)] |
| 155 | + [hι : well_founded_gt ι] [Π i, canonically_ordered_add_monoid (α i)] |
| 156 | + [hα : ∀ i, well_founded_lt (α i)] : well_founded_lt (lex (Π₀ i, α i)) := |
| 157 | +⟨lex.well_founded' (λ i a, (zero_le a).not_lt) (λ i, (hα i).wf) hι.wf⟩ |
| 158 | + |
| 159 | +end dfinsupp |
| 160 | + |
| 161 | +open dfinsupp |
| 162 | + |
| 163 | +variables (r : ι → ι → Prop) {s : Π i, α i → α i → Prop} |
| 164 | + |
| 165 | +theorem pi.lex.well_founded [is_strict_total_order ι r] [finite ι] |
| 166 | + (hs : ∀ i, well_founded (s i)) : well_founded (pi.lex r s) := |
| 167 | +begin |
| 168 | + obtain h | ⟨⟨x⟩⟩ := is_empty_or_nonempty (Π i, α i), |
| 169 | + { convert empty_wf, ext1 x, exact (h.1 x).elim }, |
| 170 | + letI : Π i, has_zero (α i) := λ i, ⟨(hs i).min ⊤ ⟨x i, trivial⟩⟩, |
| 171 | + haveI := is_trans.swap r, haveI := is_irrefl.swap r, haveI := fintype.of_finite ι, |
| 172 | + refine inv_image.wf equiv_fun_on_fintype.symm (lex.well_founded' (λ i a, _) hs _), |
| 173 | + exacts [(hs i).not_lt_min ⊤ _ trivial, finite.well_founded_of_trans_of_irrefl r.swap], |
| 174 | +end |
| 175 | + |
| 176 | +instance pi.lex.well_founded_lt [linear_order ι] [finite ι] [Π i, has_lt (α i)] |
| 177 | + [hwf : ∀ i, well_founded_lt (α i)] : well_founded_lt (lex (Π i, α i)) := |
| 178 | +⟨pi.lex.well_founded (<) (λ i, (hwf i).1)⟩ |
| 179 | + |
| 180 | +instance function.lex.well_founded_lt {α} [linear_order ι] [finite ι] [has_lt α] |
| 181 | + [well_founded_lt α] : well_founded_lt (lex (ι → α)) := pi.lex.well_founded_lt |
| 182 | + |
| 183 | +theorem dfinsupp.lex.well_founded_of_finite [is_strict_total_order ι r] [finite ι] |
| 184 | + [Π i, has_zero (α i)] (hs : ∀ i, well_founded (s i)) : well_founded (dfinsupp.lex r s) := |
| 185 | +have _ := fintype.of_finite ι, |
| 186 | + by exactI inv_image.wf equiv_fun_on_fintype (pi.lex.well_founded r hs) |
| 187 | + |
| 188 | +instance dfinsupp.lex.well_founded_lt_of_finite [linear_order ι] [finite ι] [Π i, has_zero (α i)] |
| 189 | + [Π i, has_lt (α i)] [hwf : ∀ i, well_founded_lt (α i)] : well_founded_lt (lex (Π₀ i, α i)) := |
| 190 | +⟨dfinsupp.lex.well_founded_of_finite (<) $ λ i, (hwf i).1⟩ |
| 191 | + |
| 192 | +protected theorem dfinsupp.well_founded_lt [Π i, has_zero (α i)] [Π i, preorder (α i)] |
| 193 | + [∀ i, well_founded_lt (α i)] (hbot : ∀ ⦃i⦄ ⦃a : α i⦄, ¬ a < 0) : well_founded_lt (Π₀ i, α i) := |
| 194 | +⟨begin |
| 195 | + letI : Π i, has_zero (antisymmetrization (α i) (≤)) := λ i, ⟨to_antisymmetrization (≤) 0⟩, |
| 196 | + let f := map_range (λ i, @to_antisymmetrization (α i) (≤) _) (λ i, rfl), |
| 197 | + refine subrelation.wf (λ x y h, _) (inv_image.wf f $ lex.well_founded' _ (λ i, _) _), |
| 198 | + { exact well_ordering_rel.swap }, { exact λ i, (<) }, |
| 199 | + { haveI := is_strict_order.swap (@well_ordering_rel ι), |
| 200 | + obtain ⟨i, he, hl⟩ := lex_lt_of_lt_of_preorder well_ordering_rel.swap h, |
| 201 | + exact ⟨i, λ j hj, quot.sound (he j hj), hl⟩ }, |
| 202 | + { rintro i ⟨a⟩, apply hbot }, |
| 203 | + exacts [is_well_founded.wf, is_trichotomous.swap _, is_well_founded.wf], |
| 204 | +end⟩ |
| 205 | + |
| 206 | +instance dfinsupp.well_founded_lt' [Π i, canonically_ordered_add_monoid (α i)] |
| 207 | + [∀ i, well_founded_lt (α i)] : well_founded_lt (Π₀ i, α i) := |
| 208 | +dfinsupp.well_founded_lt $ λ i a, (zero_le a).not_lt |
| 209 | + |
| 210 | +instance pi.well_founded_lt [finite ι] [Π i, preorder (α i)] |
| 211 | + [hw : ∀ i, well_founded_lt (α i)] : well_founded_lt (Π i, α i) := |
| 212 | +⟨begin |
| 213 | + obtain h | ⟨⟨x⟩⟩ := is_empty_or_nonempty (Π i, α i), |
| 214 | + { convert empty_wf, ext1 x, exact (h.1 x).elim }, |
| 215 | + letI : Π i, has_zero (α i) := λ i, ⟨(hw i).wf.min ⊤ ⟨x i, trivial⟩⟩, |
| 216 | + haveI := fintype.of_finite ι, |
| 217 | + refine inv_image.wf equiv_fun_on_fintype.symm (dfinsupp.well_founded_lt $ λ i a, _).wf, |
| 218 | + exact (hw i).wf.not_lt_min ⊤ _ trivial, |
| 219 | +end⟩ |
| 220 | + |
| 221 | +instance function.well_founded_lt {α} [finite ι] [preorder α] |
| 222 | + [well_founded_lt α] : well_founded_lt (ι → α) := pi.well_founded_lt |
| 223 | + |
| 224 | +instance dfinsupp.well_founded_lt_of_finite [finite ι] [Π i, has_zero (α i)] [Π i, preorder (α i)] |
| 225 | + [∀ i, well_founded_lt (α i)] : well_founded_lt (Π₀ i, α i) := |
| 226 | +have _ := fintype.of_finite ι, |
| 227 | + by exactI ⟨inv_image.wf equiv_fun_on_fintype pi.well_founded_lt.wf⟩ |
0 commit comments