Extending well-founded relation to well-order

Stream: Is there code for X?

[Yaël Dillies]

Do we have this somewhere?

import order.zorn

/-- Any well-founded relation can be extended to a well-ordering on that type. -/
lemma well_founded.exists_well_order_ge {α : Type*} {r : α → α → Prop} (wf : well_founded r) :
  ∃ s, r ≤ s ∧ is_well_order α s := sorry

[Junyan Xu]

I've formalized the proof at https://math.stackexchange.com/a/4124696/12932

import set_theory.ordinal.arithmetic
import data.prod.lex

universe u

variables {α : Type u} {r : α → α → Prop}

/-- This definition is probably unconventional and doesn't agree with ordinal.typein:
  there is no need to take successor if the sup is a limit ordinal,
  but this definition satisfies rank_lt_of_rel and therefore suffices for our current purpose. -/
noncomputable def acc.rank {a : α} (h : acc r a) : ordinal.{u} :=
acc.rec_on h $ λ a h ih, order.succ (ordinal.sup.{u u} $ λ b : {b // r b a}, ih b b.2)

lemma acc.rank_eq {a : α} (h : acc r a) :
  h.rank = order.succ (ordinal.sup.{u u} $ λ b : {b // r b a}, (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 acc.rank_lt_of_rel {a b : α} (hb : acc r b) (h : r a b) : (hb.inv h).rank < hb.rank :=
begin
  rw hb.rank_eq,
  rw order.lt_succ_iff,
  convert ordinal.le_sup.{u u} _ _,
  swap, { exact ⟨a, h⟩ }, { refl },
end

namespace well_founded

variable (hwf : well_founded r)
include hwf

noncomputable def rank (a : α) : ordinal.{u} := (hwf.apply a).rank

lemma rank_lt_of_rel {a b : α} (h : r a b) : hwf.rank a < hwf.rank b := acc.rank_lt_of_rel _ h

noncomputable def linear_extension : linear_order α :=
let l : linear_order α := is_well_order.linear_order well_ordering_rel in by exactI
  @linear_order.lift' α (ordinal ×ₗ α) _ (λ a : α, (hwf.rank a, a)) (λ _ _, congr_arg prod.snd)

lemma linear_extension_lt_eq :
  hwf.linear_extension.lt = inv_image (prod.lex (<) well_ordering_rel) (λ a, (hwf.rank a, a)) := rfl

instance linear_extension_is_well_founded : is_well_founded α hwf.linear_extension.lt :=
⟨inv_image.wf _ $ prod.lex_wf ordinal.well_founded_lt.wf well_ordering_rel.is_well_order.wf⟩

lemma exists_well_order_ge : ∃ s, r ≤ s ∧ is_well_order α s :=
⟨hwf.linear_extension.lt, λ a b h, prod.lex.left _ _ (hwf.rank_lt_of_rel h), by split⟩

end well_founded

[Junyan Xu]

Does mathlib even have that every partial order extends to a linear order?

[Matt Diamond]

docs#as_linear_order.linear_order?

[Matt Diamond]

it's from a total partial order, not sure if that's what you meant

[Junyan Xu]

That's mathematically trivial; I'm thinking about https://en.wikipedia.org/wiki/Linear_extension#Order-extension_principle

[Matt Diamond]

ah whoops, I see

[Junyan Xu]

Hmm docs#linear_extension.linear_order is what I was looking for...

[Junyan Xu]

That proof uses Zorn's lemma; I tried to use Zorn's lemma for this well-founded version as well, but it doesn't work: (<) restricted {x : ℤ | x > n} is well-founded, and for different n it forms a chain, but the union is (<) on ℤ which is not well-founded.

[Yaël Dillies]

Bhavik told me that at https://math.stackexchange.com/a/4124696/12932 was just Zorn in disguise and that you could basically copy-paste the proof of docs#linear_extension.linear_order to ensure well-foundedness too.

[Junyan Xu]

If you extend arbitrarily you may not get a well order, for example the empty relation on ℕ can be extended to (>) which is not well-founded, and I'm not sure how you take care of that possibility if you're gonna adapt the src#extend_partial_order proof. In fact, if all linear extensions of a well-founded partial order are well-founded, then the partial order has no infinite antichain (docs#set.is_pwo), and vice versa; I learned the fact from https://arxiv.org/abs/1503.06514v6 but it's easy to come up with a proof once you know the theorem.

[Yaël Dillies]

Maybe Bhavik is just wrong :shrug:

[Yaël Dillies]

For reference, here is our current proof idea: https://github.com/leanprover-community/con-nf/blob/main/src/phase2/strong_support.lean#L406

[Bhavik Mehta]

Junyan Xu said:

If you extend arbitrarily you may not get a well order, for example the empty relation on ℕ can be extended to (>) which is not well-founded, and I'm not sure how you take care of that possibility if you're gonna adapt the src#extend_partial_order proof. In fact, if all linear extensions of a well-founded partial order are well-founded, then the partial order has no infinite antichain (docs#set.is_pwo), and vice versa; I learned the fact from https://arxiv.org/abs/1503.06514v6 but it's easy to come up with a proof once you know the theorem.

I don't claim that extending arbitrarily gives you a well order, instead that the proof idea is the same thing - a proof by well-founded recursion on ordinals can always be translated to a proof by Zorn. I agree picking an arbitrary extension won't work, but the Zorn proof works directly instead

[Gabriel Ebner]

AFAICT using the Zorn proof directly doesn't work. A chain of well-founded relations does not necessarily have a well-founded upper bound. (If you complete the empty relation on Nat, you could devillishly go 1 < 0, 2 < 1 < 0, etc.)

(EDIT: which is apparently exactly what Junyan is saying.)

[Gabriel Ebner]

I'm kind of surprised that we do not have the rank function on well-founded relations yet.

[Junyan Xu]

We do have docs#pgame.birthday which is the rank function for the relation docs#pgame.is_option.