feat(order/extension/well): Extend a well-founded order (#17054)

A well-founded order can be extended to a well order.

For this, we need the rank of an an element of a well-founded order.

Also rename `order.extension` to `order.extension.linear`.

Co-authored-by: Junyan Xu <junyanxumath@gmail.com>

src/order/extension/well.lean

@@ -0,0 +1,75 @@
+/-
+Copyright (c) 2022 Yaël Dillies, Junyan Xu. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yaël Dillies, Junyan Xu
+-/
+import data.prod.lex
+import set_theory.ordinal.arithmetic
+
+/-!
+# Extend a well-founded order to a well-order
+
+This file constructs a well-order (linear well-founded order) which is an extension of a given
+well-founded order.
+
+## Proof idea
+
+We can map our order into two well-orders:
+* the first map respects the order but isn't necessarily injective. Namely, this is the *rank*
+  function `rank : α → ordinal`.
+* the second map is injective but doesn't necessarily respect the order. This is an arbitrary
+  well-order on `α`.
+
+Then their lexicographic product is a well-founded linear order which our original order injects in.
+-/
+
+universe u
+
+variables {α : Type u} {r : α → α → Prop}
+
+namespace well_founded
+variable (hwf : well_founded r)
+include hwf
+
+/-- An arbitrary well order on `α` that extends `r`.
+
+The construction maps `r` into two well-orders: the first map is `well_founded.rank`, which is not
+necessarily injective but respects the order `r`; the other map is the identity (with an arbitrarily
+chosen well-order on `α`), which is injective but doesn't respect `r`.
+
+By taking the lexicographic product of the two, we get both properties, so we can pull it back and
+get an well-order that extend our original order `r`. Another way to view this is that we choose an
+arbitrary well-order to serve as a tiebreak between two elements of same rank.
+-/
+noncomputable def well_order_extension : linear_order α :=
+let l : linear_order α := is_well_order.linear_order well_ordering_rel in by exactI
+  @linear_order.lift' α (ordinal ×ₗ α) _
+    (λ a : α, (well_founded.rank.{u u} hwf a, a)) (λ _ _, congr_arg prod.snd)
+
+instance well_order_extension.is_well_founded_lt : is_well_founded α hwf.well_order_extension.lt :=
+⟨inv_image.wf _ $ prod.lex_wf ordinal.well_founded_lt.wf well_ordering_rel.is_well_order.wf⟩
+
+/-- Any well-founded relation can be extended to a well-ordering on that type. -/
+lemma exists_well_order_ge : ∃ s, r ≤ s ∧ is_well_order α s :=
+⟨hwf.well_order_extension.lt, λ a b h, prod.lex.left _ _ (hwf.rank_lt_of_rel h), by split⟩
+
+end well_founded
+
+/-- A type alias for `α`, intended to extend a well-founded order on `α` to a well-order. -/
+def well_order_extension (α) : Type* := α
+
+instance [inhabited α] : inhabited (well_order_extension α) := ‹inhabited (well_order_extension α)›
+
+/-- "Identity" equivalence between a well-founded order and its well-order extension. -/
+def to_well_order_extension : α ≃ well_order_extension α := equiv.refl _
+
+noncomputable instance [has_lt α] [well_founded_lt α] : linear_order (well_order_extension α) :=
+(is_well_founded.wf : @well_founded α (<)).well_order_extension
+
+instance well_order_extension.well_founded_lt [has_lt α] [well_founded_lt α] :
+  well_founded_lt (well_order_extension α) :=
+well_founded.well_order_extension.is_well_founded_lt _
+
+lemma to_well_order_extension_strict_mono [preorder α] [well_founded_lt α] :
+  strict_mono (to_well_order_extension : α → well_order_extension α) :=
+λ a b h, prod.lex.left _ _ $ well_founded.rank_lt_of_rel _ h

src/set_theory/ordinal/arithmetic.lean

@@ -2400,3 +2400,48 @@ meta def positivity_opow : expr → tactic strictness
 | _ := failed
 
 end tactic
+
+namespace acc
+variables {a b : α}
+
+/-- The rank of an element `a` accessible under a relation `r` is defined inductively as the
+smallest ordinal greater than the ranks of all elements below it (i.e. elements `b` such that
+`r b a`). -/
+noncomputable def rank (h : acc r a) : ordinal :=
+acc.rec_on h $ λ a h ih, ordinal.sup $ λ b : {b // r b a}, order.succ $ ih b b.2
+
+lemma rank_eq (h : acc r a) :
+  h.rank = ordinal.sup (λ b : {b // r b a}, order.succ (h.inv b.2).rank) :=
+by { change (acc.intro a $ λ _, h.inv).rank = _, refl }
+
+/-- if `r a b` then the rank of `a` is less than the rank of `b`. -/
+lemma rank_lt_of_rel (hb : acc r b) (h : r a b) : (hb.inv h).rank < hb.rank :=
+(order.lt_succ _).trans_le $ by { rw hb.rank_eq, refine le_trans _ (ordinal.le_sup _ ⟨a, h⟩), refl }
+
+end acc
+
+namespace well_founded
+variables (hwf : well_founded r) {a b : α}
+include hwf
+
+/-- The rank of an element `a` under a well-founded relation `r` is defined inductively as the
+smallest ordinal greater than the ranks of all elements below it (i.e. elements `b` such that
+`r b a`). -/
+noncomputable def rank (a : α) : ordinal := (hwf.apply a).rank
+
+lemma rank_eq : hwf.rank a = ordinal.sup (λ b : {b // r b a}, order.succ $ hwf.rank b) :=
+by { rw [rank, acc.rank_eq], refl }
+
+lemma rank_lt_of_rel (h : r a b) : hwf.rank a < hwf.rank b := acc.rank_lt_of_rel _ h
+
+omit hwf
+
+lemma rank_strict_mono [preorder α] [well_founded_lt α] :
+  strict_mono (rank $ @is_well_founded.wf α (<) _) :=
+λ _ _, rank_lt_of_rel _
+
+lemma rank_strict_anti [preorder α] [well_founded_gt α] :
+  strict_anti (rank $ @is_well_founded.wf α (>) _) :=
+λ _ _, rank_lt_of_rel $ @is_well_founded.wf α (>) _
+
+end well_founded