feat(order/well_founded, data/fin/tuple/*, ...): add `well_founded.in…

…duction_bot`, `tuple.bubble_sort_induction` (#16536)

The main purpose of this PR is to add the following induction principle fir tuples.
```lean
lemma tuple.bubble_sort_induction {n : ℕ} {α : Type*} [linear_order α] {f : fin n → α}
  {P : (fin n → α) → Prop} (hf : P f)
  (h : ∀ (g : fin n → α) (i j : fin n), i < j → g j < g i → P g → P (g ∘ equiv.swap i j)) :
  P (f ∘ sort f)
```
This is in a new file `data/fin/tuple/bubble_sort_induction`.

The additional API lemmas needed for it are mostly added to `data/fin/tuple/sort` (and some in `data/list/perm` and `data/list/sort`).
One of these lemmas is the following induction principle for well-founded relations.
```lean
lemma well_founded.induction_bot {α} {r : α → α → Prop} (hwf : well_founded r) {a bot : α}
  {C : α → Prop} (ha : C a) (ih : ∀ b, b ≠ bot → C b → ∃ c, r c b ∧ C c) : C bot
```

See the discussion on [Zulip](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/.22sort.22.20a.20function/near/299289703).

src/data/fin/tuple/bubble_sort_induction.lean

@@ -0,0 +1,53 @@
+/-
+Copyright (c) 2022 Michael Stoll. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Michael Stoll
+-/
+import data.fin.tuple.sort
+import order.well_founded
+
+/-!
+# "Bubble sort" induction
+
+We implement the following induction principle `tuple.bubble_sort_induction`
+on tuples with values in a linear order `α`.
+
+Let `f : fin n → α` and let `P` be a predicate on `fin n → α`. Then we can show that
+`f ∘ sort f` satisfies `P` if `f` satisfies `P`, and whenever some `g : fin n → α`
+satisfies `P` and `g i > g j` for some `i < j`, then `g ∘ swap i j` also satisfies `P`.
+
+We deduce it from a stronger variant `tuple.bubble_sort_induction'`, which
+requires the assumption only for `g` that are permutations of `f`.
+
+The latter is proved by well-founded induction via `well_founded.induction_bot'`
+with respect to the lexicographic ordering on the finite set of all permutations of `f`.
+-/
+
+namespace tuple
+
+/-- *Bubble sort induction*: Prove that the sorted version of `f` has some property `P`
+if `f` satsifies `P` and `P` is preserved on permutations of `f` when swapping two
+antitone values. -/
+lemma bubble_sort_induction' {n : ℕ} {α : Type*} [linear_order α] {f : fin n → α}
+  {P : (fin n → α) → Prop} (hf : P f)
+  (h : ∀ (σ : equiv.perm (fin n)) (i j : fin n),
+              i < j → (f ∘ σ) j < (f ∘ σ) i → P (f ∘ σ) → P (f ∘ σ ∘ equiv.swap i j)) :
+  P (f ∘ sort f) :=
+begin
+  letI := @preorder.lift _ (lex (fin n → α)) _ (λ σ : equiv.perm (fin n), to_lex (f ∘ σ)),
+  refine @well_founded.induction_bot' _ _ _
+    (@finite.preorder.well_founded_lt (equiv.perm (fin n)) _ _)
+    (equiv.refl _) (sort f) P (λ σ, f ∘ σ) (λ σ hσ hfσ, _) hf,
+  obtain ⟨i, j, hij₁, hij₂⟩ := antitone_pair_of_not_sorted' hσ,
+  exact ⟨σ * equiv.swap i j, pi.lex_desc hij₁ hij₂, h σ i j hij₁ hij₂ hfσ⟩,
+end
+
+/-- *Bubble sort induction*: Prove that the sorted version of `f` has some property `P`
+if `f` satsifies `P` and `P` is preserved when swapping two antitone values. -/
+lemma bubble_sort_induction {n : ℕ} {α : Type*} [linear_order α] {f : fin n → α}
+  {P : (fin n → α) → Prop} (hf : P f)
+  (h : ∀ (g : fin n → α) (i j : fin n), i < j → g j < g i → P g → P (g ∘ equiv.swap i j)) :
+  P (f ∘ sort f) :=
+bubble_sort_induction' hf (λ σ, h _)
+
+end tuple

src/data/fin/tuple/sort.lean

@@ -72,11 +72,14 @@ finset.order_iso_of_fin _ (by simp)
 def sort (f : fin n → α) : equiv.perm (fin n) :=
 (graph_equiv₂ f).to_equiv.trans (graph_equiv₁ f).symm
 
+lemma graph_equiv₂_apply (f : fin n → α) (i : fin n) :
+  graph_equiv₂ f i = graph_equiv₁ f (sort f i) :=
+((graph_equiv₁ f).apply_symm_apply _).symm
+
 lemma self_comp_sort (f : fin n → α) : f ∘ sort f = graph.proj ∘ graph_equiv₂ f :=
 show graph.proj ∘ ((graph_equiv₁ f) ∘ (graph_equiv₁ f).symm) ∘ (graph_equiv₂ f).to_equiv = _,
   by simp
 
-
 lemma monotone_proj (f : fin n → α) : monotone (graph.proj : graph f → α) :=
 begin
   rintro ⟨⟨x, i⟩, hx⟩ ⟨⟨y, j⟩, hy⟩ (h|h),
@@ -91,3 +94,71 @@ begin
 end
 
 end tuple
+
+namespace tuple
+
+open list
+
+variables {n : ℕ} {α : Type*}
+
+/-- If two permutations of a tuple `f` are both monotone, then they are equal. -/
+lemma unique_monotone [partial_order α] {f : fin n → α} {σ τ : equiv.perm (fin n)}
+  (hfσ : monotone (f ∘ σ)) (hfτ : monotone (f ∘ τ)) : f ∘ σ = f ∘ τ :=
+of_fn_injective $ eq_of_perm_of_sorted
+  ((σ.of_fn_comp_perm f).trans (τ.of_fn_comp_perm f).symm) hfσ.of_fn_sorted hfτ.of_fn_sorted
+
+variables [linear_order α] {f : fin n → α} {σ : equiv.perm (fin n)}
+
+/-- A permutation `σ` equals `sort f` if and only if the map `i ↦ (f (σ i), σ i)` is
+strictly monotone (w.r.t. the lexicographic ordering on the target). -/
+lemma eq_sort_iff' : σ = sort f ↔ strict_mono (σ.trans $ graph_equiv₁ f) :=
+begin
+  split; intro h,
+  { rw [h, sort, equiv.trans_assoc, equiv.symm_trans_self], exact (graph_equiv₂ f).strict_mono },
+  { have := subsingleton.elim (graph_equiv₂ f) (h.order_iso_of_surjective _ $ equiv.surjective _),
+    ext1, exact (graph_equiv₁ f).apply_eq_iff_eq_symm_apply.1 (fun_like.congr_fun this x).symm },
+end
+
+/-- A permutation `σ` equals `sort f` if and only if `f ∘ σ` is monotone and whenever `i < j`
+and `f (σ i) = f (σ j)`, then `σ i < σ j`. This means that `sort f` is the lexicographically
+smallest permutation `σ` such that `f ∘ σ` is monotone. -/
+lemma eq_sort_iff : σ = sort f ↔ monotone (f ∘ σ) ∧ ∀ i j, i < j → f (σ i) = f (σ j) → σ i < σ j :=
+begin
+  rw eq_sort_iff',
+  refine ⟨λ h, ⟨(monotone_proj f).comp h.monotone, λ i j hij hfij, _⟩, λ h i j hij, _⟩,
+  { exact (((prod.lex.lt_iff _ _).1 $ h hij).resolve_left hfij.not_lt).2 },
+  { obtain he|hl := (h.1 hij.le).eq_or_lt; apply (prod.lex.lt_iff _ _).2,
+    exacts [or.inr ⟨he, h.2 i j hij he⟩, or.inl hl] },
+end
+
+/-- The permutation that sorts `f` is the identity if and only if `f` is monotone. -/
+lemma sort_eq_refl_iff_monotone : sort f = equiv.refl _ ↔ monotone f :=
+begin
+  rw [eq_comm, eq_sort_iff, equiv.coe_refl, function.comp.right_id],
+  simp only [id.def, and_iff_left_iff_imp],
+  exact λ _ _ _ hij _, hij,
+end
+
+/-- A permutation of a tuple `f` is `f` sorted if and only if it is monotone. -/
+lemma comp_sort_eq_comp_iff_monotone : f ∘ σ = f ∘ sort f ↔ monotone (f ∘ σ) :=
+⟨λ h, h.symm ▸ monotone_sort f, λ h, unique_monotone h (monotone_sort f)⟩
+
+/-- The sorted versions of a tuple `f` and of any permutation of `f` agree. -/
+lemma comp_perm_comp_sort_eq_comp_sort : (f ∘ σ) ∘ (sort (f ∘ σ)) = f ∘ sort f :=
+begin
+  rw [function.comp.assoc, ← equiv.perm.coe_mul],
+  exact unique_monotone (monotone_sort (f ∘ σ)) (monotone_sort f),
+end
+
+/-- If a permutation `f ∘ σ` of the tuple `f` is not the same as `f ∘ sort f`, then `f ∘ σ`
+has a pair of strictly decreasing entries. -/
+lemma antitone_pair_of_not_sorted' (h : f ∘ σ ≠ f ∘ sort f) :
+  ∃ i j, i < j ∧ (f ∘ σ) j < (f ∘ σ) i :=
+by { contrapose! h, exact comp_sort_eq_comp_iff_monotone.mpr (monotone_iff_forall_lt.mpr h) }
+
+/-- If the tuple `f` is not the same as `f ∘ sort f`, then `f` has a pair of strictly decreasing
+entries. -/
+lemma antitone_pair_of_not_sorted (h : f ≠ f ∘ sort f) : ∃ i j, i < j ∧ f j < f i :=
+antitone_pair_of_not_sorted' (id h : f ∘ equiv.refl _ ≠ _)
+
+end tuple

src/data/list/perm.lean

@@ -1393,3 +1393,21 @@ end
 end permutations
 
 end list
+
+open list
+
+lemma equiv.perm.map_fin_range_perm {n : ℕ} (σ : equiv.perm (fin n)) :
+  map σ (fin_range n) ~ fin_range n :=
+begin
+  rw [perm_ext ((nodup_fin_range n).map σ.injective) $ nodup_fin_range n],
+  simpa only [mem_map, mem_fin_range, true_and, iff_true] using σ.surjective
+end
+
+/-- The list obtained from a permutation of a tuple `f` is permutation equivalent to
+the list obtained from `f`. -/
+lemma equiv.perm.of_fn_comp_perm {n : ℕ} {α : Type uu} (σ : equiv.perm (fin n)) (f : fin n → α) :
+  of_fn (f ∘ σ) ~ of_fn f :=
+begin
+  rw [of_fn_eq_map, of_fn_eq_map, ←map_map],
+  exact σ.map_fin_range_perm.map f,
+end

src/data/list/sort.lean

@@ -104,6 +104,23 @@ end
 
 end sorted
 
+section monotone
+
+variables {n : ℕ} {α : Type uu} [preorder α] {f : fin n → α}
+
+/-- A tuple is monotone if and only if the list obtained from it is sorted. -/
+lemma monotone_iff_of_fn_sorted : monotone f ↔ (of_fn f).sorted (≤) :=
+begin
+  simp_rw [sorted, pairwise_iff_nth_le, length_of_fn, nth_le_of_fn', monotone_iff_forall_lt],
+  exact ⟨λ h i j hj hij, h $ fin.mk_lt_mk.mpr hij, λ h ⟨i, _⟩ ⟨j, hj⟩ hij, h i j hj hij⟩,
+end
+
+/-- The list obtained from a monotone tuple is sorted. -/
+lemma monotone.of_fn_sorted (h : monotone f) : (of_fn f).sorted (≤) :=
+monotone_iff_of_fn_sorted.1 h
+
+end monotone
+
 section sort
 variables {α : Type uu} (r : α → α → Prop) [decidable_rel r]
 local infix ` ≼ ` : 50 := r

src/data/pi/lex.lean

@@ -127,4 +127,12 @@ instance lex.ordered_comm_group [linear_order ι] [∀ a, ordered_comm_group (β
   ..pi.lex.partial_order,
   ..pi.comm_group }
 
+/-- If we swap two strictly decreasing values in a function, then the result is lexicographically
+smaller than the original function. -/
+lemma lex_desc {α} [preorder ι] [decidable_eq ι] [preorder α] {f : ι → α} {i j : ι}
+  (h₁ : i < j) (h₂ : f j < f i) :
+  to_lex (f ∘ equiv.swap i j) < to_lex f :=
+⟨i, λ k hik, congr_arg f (equiv.swap_apply_of_ne_of_ne hik.ne (hik.trans h₁).ne),
+  by simpa only [pi.to_lex_apply, function.comp_app, equiv.swap_apply_left] using h₂⟩
+
 end pi

src/order/well_founded.lean

@@ -14,7 +14,8 @@ implies `P x`. Well-founded relations can be used for induction and recursion, i
 construction of fixed points in the space of dependent functions `Π x : α , β x`.
 
 The predicate `well_founded` is defined in the core library. In this file we prove some extra lemmas
-and provide a few new definitions: `well_founded.min`, `well_founded.sup`, and `well_founded.succ`.
+and provide a few new definitions: `well_founded.min`, `well_founded.sup`, and `well_founded.succ`,
+and an induction principle `well_founded.induction_bot`.
 -/
 
 variables {α : Type*}
@@ -211,3 +212,48 @@ not_lt.mp $ not_lt_argmin_on f h s ha hs
 end linear_order
 
 end function
+
+section induction
+
+/-- Let `r` be a relation on `α`, let `f : α → β` be a function, let `C : β → Prop`, and
+let `bot : α`. This induction principle shows that `C (f bot)` holds, given that
+* some `a` that is accessible by `r` satisfies `C (f a)`, and
+* for each `b` such that `f b ≠ f bot` and `C (f b)` holds, there is `c`
+  satisfying `r c b` and `C (f c)`. -/
+lemma acc.induction_bot' {α β} {r : α → α → Prop} {a bot : α} (ha : acc r a) {C : β → Prop}
+  {f : α → β} (ih : ∀ b, f b ≠ f bot → C (f b) → ∃ c, r c b ∧ C (f c)) : C (f a) → C (f bot) :=
+@acc.rec_on _ _ (λ x, C (f x) → C (f bot)) _ ha $ λ x ac ih' hC,
+  (eq_or_ne (f x) (f bot)).elim (λ h, h ▸ hC)
+    (λ h, let ⟨y, hy₁, hy₂⟩ := ih x h hC in ih' y hy₁ hy₂)
+
+/-- Let `r` be a relation on `α`, let `C : α → Prop` and let `bot : α`.
+This induction principle shows that `C bot` holds, given that
+* some `a` that is accessible by `r` satisfies `C a`, and
+* for each `b ≠ bot` such that `C b` holds, there is `c` satisfying `r c b` and `C c`. -/
+lemma acc.induction_bot {α} {r : α → α → Prop} {a bot : α} (ha : acc r a)
+  {C : α → Prop} (ih : ∀ b, b ≠ bot → C b → ∃ c, r c b ∧ C c) : C a → C bot :=
+ha.induction_bot' ih
+
+/-- Let `r` be a well-founded relation on `α`, let `f : α → β` be a function,
+let `C : β → Prop`, and  let `bot : α`.
+This induction principle shows that `C (f bot)` holds, given that
+* some `a` satisfies `C (f a)`, and
+* for each `b` such that `f b ≠ f bot` and `C (f b)` holds, there is `c`
+  satisfying `r c b` and `C (f c)`. -/
+lemma well_founded.induction_bot' {α β} {r : α → α → Prop} (hwf : well_founded r) {a bot : α}
+  {C : β → Prop} {f : α → β} (ih : ∀ b, f b ≠ f bot → C (f b) → ∃ c, r c b ∧ C (f c)) :
+  C (f a) → C (f bot) :=
+(hwf.apply a).induction_bot' ih
+
+/-- Let `r` be a well-founded relation on `α`, let `C : α → Prop`, and let `bot : α`.
+This induction principle shows that `C bot` holds, given that
+* some `a` satisfies `C a`, and
+* for each `b` that satisfies `C b`, there is `c` satisfying `r c b` and `C c`.
+
+The naming is inspired by the fact that when `r` is transitive, it follows that `bot` is
+the smallest element w.r.t. `r` that satisfies `C`. -/
+lemma well_founded.induction_bot {α} {r : α → α → Prop} (hwf : well_founded r) {a bot : α}
+  {C : α → Prop} (ih : ∀ b, b ≠ bot → C b → ∃ c, r c b ∧ C c) : C a → C bot :=
+hwf.induction_bot' ih
+
+end induction