Help proving well_foundedness

Stream: Is there code for X?

[Paul Rowe]

I could use a little help understanding how to use the relevant lemmas surrounding well-foundedness. I want to prove something like the following:

example {α : Type*} [preorder α] (f : α → ℕ × ℕ) {a1 a2 : α}
(hf : ∀ a1 a2, a1 < a2 → prod.lex (<) (<) (f a1) (f a2)) :
well_founded ((<) : α → α → Prop) := sorry

On paper, I would rely on the descending chain condition. That is, it should be sufficient to say that there is no infinite descending chain a1 > a2 > a3 > ... in α. Given I have f above, and that the lexicographic order on ℕ × ℕ is well-founded, such an infinite descending chain in α would result in an infinite descending chain in ℕ × ℕ, contradicting its well-foundedness.

What theorems exist in mathlib to support this style of argument? I see docs#rel_embedding.well_founded_iff_no_descending_seq but I'm not sure how to leverage it.

[Aaron Anderson]

You could certainly use that lemma to formalize the contradiction setup you've described. If you use that lemma, that changes the goal to is_empty (gt ↪r r), which is essentially (gt ↪r r) → false. To prove this goal, you need to show that for every rel_embedding (a monotone injective function) between the appropriate orders, you get a contradiction.

[Aaron Anderson]

That rel_embedding would basically be the descending chain you're talking about.

[Aaron Anderson]

However, to actually get that contradiction, you'd probably want to use that rel_embedding together with hf to create a rel_embedding representing a descending chain in ℕ × ℕ, at which point you'd refer to the well-foundedness of ℕ × ℕ.

[Junyan Xu]

(deleted)

[Aaron Anderson]

You can shortcut some of this argument with docs#rel_embedding.well_founded , which allows you to reduce the well-foundedness of α directly to the well-foundedness of ℕ × ℕ, if you can construct a rel_embedding from f and hf.

[Paul Rowe]

That sounds promising. I think that's the theorem I was looking for.

[Junyan Xu]

example {α : Type*} [preorder α] (f : α → ℕ × ℕ) {a1 a2 : α}
  (hf : ∀ a1 a2, a1 < a2 → prod.lex (<) (<) (f a1) (f a2)) :
  well_founded ((<) : α → α → Prop) :=
subrelation.wf hf $ inv_image.wf f $ prod.lex_wf nat.lt_wf nat.lt_wf

[Paul Rowe]

What's the tactic mode version of this?

[Aaron Anderson]

The shortest tactic mode version of that would be exact subrelation.wf hf $ inv_image.wf f $ prod.lex_wf nat.lt_wf nat.lt_wf,, or more parenthetically, exact subrelation.wf hf (inv_image.wf f (prod.lex_wf nat.lt_wf nat.lt_wf)), but you could always whittle it down step by step, starting with refine subrelation.wf hf _,

[Aaron Anderson]

or refine rel_embedding.well_founded _ _,

[Paul Rowe]

Aaron Anderson said:

The shortest tactic mode version of that would be exact subrelation.wf hf $ inv_image.wf f $ prod.lex_wf nat.lt_wf nat.lt_wf,

Well, yes, if you have a term you can always exact that term. I just always work in tactic mode so I was not familiar with the $ .

Thank you both for your help. I think this should give me a path forward.

[Paul Rowe]

Ok now I see that @Junyan Xu 's proof is really the one I had in mind when I first started. I abandoned it when I started to get confused. I can't actually start with rel_embedding.well_founded because my f is not a rel_embedding (it's not injective).

Now I'm surprised a more general version of this isn't already in mathlib somewhere. This is a standard approach for showing well-foundedness: map a given <-relation into a well-founded one in such a way that < is preserved. So something like:

example {α β : Type*}  [preorder α] [preorder β] (f : α → β)
(wf : well_founded ((<) : β → β → Prop))
(hf : ∀ a1 a2, a1 < a2 → f a1 < f a2) :
well_founded ((<) : α → α → Prop) :=
subrelation.wf hf $ inv_image.wf f $ wf