Restricted well-foundedness of docs#prod.lex

Stream: Is there code for X?

[Yaël Dillies]

I need a version of docs#prod.lex_wf where I don't need to check well-foundedness of the second relation on the entire domain (because it doesn't hold in my case), but only on fibers of the first relation.

import order.well_founded_set

variables {α β γ : Type*} {rα : α  → α → Prop} {rβ : β → β → Prop} {f : γ → α} {g : γ → β}

lemma well_founded.prod_lex (hα : well_founded (rα on f))
  (hβ : ∀ a, (f ⁻¹' {a}).well_founded_on (rβ on g)) :
  well_founded (prod.lex rα rβ on λ c, (f c, g c)) :=

[Yaël Dillies]

Surely @Junyan Xu can't resist a good well-foundedness puzzle? :grinning_face_with_smiling_eyes:

[Junyan Xu]

@Yaël Dillies Here's one proof (by reducing to docs#psigma.lex_wf); I try to do a direct proof with acc but am not successful yet.

import order.well_founded_set
import data.sigma.lex

variables {α β γ : Type*} {rα : α → α → Prop} {rβ : β → β → Prop} {f : γ → α} {g : γ → β}

theorem well_founded_on_range : (set.range f).well_founded_on rα ↔ well_founded (rα on f) :=
begin
  let f' : γ → set.range f := λ c, ⟨f c, c, rfl⟩,
  refine ⟨λ h, subrelation.wf (λ c c', _) (inv_image.wf f' h), λ h, ⟨_⟩⟩,
  { exact id },
  rintro ⟨_, c, rfl⟩,
  apply acc.of_downward_closed f',
  { rintro _ ⟨_, c', rfl⟩ -, exact ⟨c', rfl⟩ },
  { apply h.apply },
end

lemma well_founded.prod_lex (hα : well_founded (rα on f))
  (hβ : ∀ a, (f ⁻¹' {a}).well_founded_on (rβ on g)) :
  well_founded (prod.lex rα rβ on λ c, (f c, g c)) :=
begin
  let p : γ → Σ' a : set.range f, f⁻¹' {a} := λ c, ⟨⟨_, c, rfl⟩, c, rfl⟩,
  refine subrelation.wf _ (inv_image.wf p $ psigma.lex_wf (well_founded_on_range.2 hα) $ λ a, hβ a),
  intros c c' h,
  obtain h' | h' := prod.lex_iff.1 h,
  { exact psigma.lex.left _ _ h' },
  { dsimp only [inv_image, p, (on)] at h' ⊢,
    convert psigma.lex.right (⟨_, c', rfl⟩ : set.range f) _ using 1, swap,
    exacts [⟨c, h'.1⟩, psigma.subtype_ext (subtype.ext h'.1) rfl, h'.2] },
end

[Yaël Dillies]

Thank you, that's tremendously useful! I am now only two sorries away from Cauchy-Davenport.