List.Lex is well founded on decreasing lists

Stream: Is there code for X?

[Dagur Asgeirsson]

I want to prove the following:

import Mathlib.Data.List.Lex

variable (α : Type _) [LinearOrder α] [IsWellFounded α (·<·)]

instance : IsWellFounded {l : List α // l.Chain' (·>·)}
    (fun l m ↦ List.Lex (·<·) l.val m.val) :=
  sorry

The mathematical proof I have in mind is the following:

Take a strictly decreasing sequence l : ℕ → {l : List α // l.Chain' (·>·)}. Then because [IsWellFounded α (·<·)], the decreasing sequence (l n).head! is eventually constant, denote its limit by a.

The sequence (l n).tail, starting from the point from which all elements of the original sequence have the same head! is again strictly decreasing, and again the sequence of head!'s is decreasing and hence eventually constant; denote its limit by b.

Then a > b because of the List.Chain' condition. We keep going like this and get a strictly decreasing sequence in α, contradiction.

This proof seems really annoying to do in Lean. Does anyone have a better idea or can point me to something useful in the library?

[Scott Morrison]

I don't know that this is in the library, but I'm not the right person to ask. :-) It ought to be.

I wouldn't mention head! and tail. Define the predicate P on a strictly decreasing sequence L (maybe worth defining a type synonym for such sequences): "forall n, there exists an M : Nat and S : List α so M ≤ m implies (L m).take n = P". Now prove three lemmas:

1. you can prove P L by proving P (L (· + k)) for some k : ℕ.
2. if ∀ m, (L m).take n = S, then fun m => (L m).drop n is strictly decreasing
3. again if ∀ m, (L m).take n = S, you can prove P L by proving P fun m => (L m).drop n.

Now P L should be amenable to proof by induction on n.
Once you have P L extracting the strictly decreasing sequence in α is hopefully not too bad. Maybe even easier if you tweak P so M depends monotonically on n, then you don't need to take any maxs at this point.

It's a bit late for writing real code here, but hopefully this will help provoke someone into writing something better!

[Yury G. Kudryashov]

Note that we usually use docs#List.Sorted instead of List.Chain' for sorted lists.

[Scott Morrison]

(I couldn't resist, and wrote down most of this proof. @Dagur Asgeirsson, if you want detailed spoilers let me know. :-)

[Scott Morrison]

The parts I didn't do are

import Mathlib.Order.Monotone.Basic

variable (α : Type _) [LinearOrder α]

lemma Antitone.eventually_constant [WellFoundedLT α] (f : ℕ → α) (h : Antitone f) :
    ∃ N a, ∀ n, N ≤ n → f n = a := by
  sorry

theorem wellFoundedLT_iff_not_strictAnti : WellFoundedLT α ↔ ∀ f : ℕ → α, ¬ StrictAnti f :=
  sorry

which perhaps are already in Mathlib?

[Scott Morrison]

#6278

[Dagur Asgeirsson]

Scott Morrison said:

#6278

Both sorries are done now

[Junyan Xu]

It turns out this can be done in 30 lines using the Acc (accessibility) primitive, i.e. directly using the definition of WellFounded without passing to the antitone sequence characterization (no need to invoke dependent choice!). In my experience (e.g. docs#WellFounded.cutExpand and docs#DFinsupp.Lex.wellFounded), proofs using Acc are usually much shorter and more elegant, which is probably why docs#RelEmbedding.wellFounded_iff_no_descending_seq is rarely used and forgotten (oh it's actually used). This proof is actually even simpler than I originally thought as it doesn't require the construction of a docs#Relation.Fibration and the self-similarity can be captured using a (slightly convoluted) double induction.

I have stated the theorem using Chain' as in Dagur's original formalization because it's more general, requiring the relation r be satisfied only by adjacent elements in the list rather than all pairs of elements. The two are equivalent via docs#List.chain'_iff_pairwise for a transitive relation.

import Mathlib.Data.List.Chain

variable (α : Type _) (r : α → α → Prop)

theorem WellFounded.list_chain' (hwf : WellFounded r) :
    @WellFounded {l : List α // l.Chain' (flip r)} (fun l m ↦ List.Lex r l.val m.val) := by
  refine ⟨fun ⟨l, hl⟩ ↦ ?_⟩
  cases' l with a l
  · apply Acc.intro; rintro ⟨_⟩ ⟨_⟩
  induction hwf.apply a generalizing l with
  | intro a _ ih =>
    have hl' := (List.chain'_cons'.1 hl).2
    let l' : {l // l.Chain' (flip r)} := ⟨l, hl'⟩
    have : Acc (fun l m ↦ List.Lex r l.val m.val) l'
    · cases' l with b l
      · apply Acc.intro; rintro ⟨_⟩ ⟨_⟩
      · apply ih b (List.chain'_cons.1 hl).1
    revert hl
    rw [(by rfl : l = l'.1)]
    clear_value l'
    induction this with
    | intro l _ ihl =>
      intro hl
      apply Acc.intro
      rintro ⟨_ | ⟨b, m⟩, hm⟩ (_ | hr | hr)
      · apply Acc.intro; rintro ⟨_⟩ ⟨_⟩
      · apply ihl ⟨m, (List.chain'_cons'.1 hm).2⟩ hr
      · apply ih b hr

instance [hwf : IsWellFounded α r] :
    IsWellFounded {l : List α // l.Chain' (flip r)} (fun l m ↦ List.Lex r l.val m.val) :=
  ⟨hwf.wf.list_chain'⟩

[Dagur Asgeirsson]

Wow, thanks!

[Dagur Asgeirsson]

Can you update the PR? Otherwise I can do it tonight. Do we still want some of the small intermediate results from Scott's proof?

[Junyan Xu]

I'd hesitate to update the PR myself as I have no idea which lemmas are just for the proof and which are of independent interest; Scott would know better. I also don't know which other forms of the theorem you'd like, e.g. do you prefer Sorted? You're welcome to update the PR with my new proof, but I could open a separate PR if you want; it would be a short one adding a theorem and an instance to Mathlib.Data.List.Chain, which would be easy to review.

[Dagur Asgeirsson]

Ok I think it’s best if you just open a new, short PR, and then I can go through the old one and see if there are any results there that we want to keep. I prefer Chain'.

[Junyan Xu]

This is now #6432

Let me add some comment about the Acc predicate (which seems inadequately addressed in major texts like TPIL and hitchhiker's guide etc.) and about my proof:

The usual mathematical definition of a well-founded relation r on a type α says that for every nonempty subset s : set α, there exists a r-minimal element in s (i.e. ∃ a ∈ s, ∀ b ∈ s, ¬ r b a, see docs#WellFounded.has_min), if we think of r a b as saying that a is less than b. Equivalently, if s doesn't have a r-minimal element, then it must be empty: ∀ s : set α, (∀ a ∈ s, ∃ b ∈ s, r b a) → s = ∅. Replacing s by its complement sᶜ, this is furthermore equivalent to ∀ s : set α, (∀ a ∉ s, ∃ b ∉ s, r b a) → s = set.univ. Taking contrapositives twice, we see that ∀ a ∉ s, ∃ b ∉ s, r b a is equivalent to ∀ a, (∀ b, r b a → b ∈ s) → a ∈ s; let's call a subset s satisfying this condition an r-inductive subset.

We define an inductive ("accessibility") predicate Acc r with a single constructor of type ∀ a, (∀ b, r b a → Acc r b) → Acc r a, then {a | Acc r a} is the smallest r-inductive subset by the way inductive predicates work (basically, the recursor of an inductive predicate states precisely this minimality). Well-foundedness says every r-inductive subset must be the whole type, which is equivalent to saying the smallest such subset, {a | Acc r a}, is the whole type. (Note: the smallest such subset exists since the intersection of any set of subsets satisfying the condition itself satisfies the condition.) Therefore, well-foundedness is equivalent to ∀ a, Acc r a, which is taken to be the definition of well-foundedness in type theory. Minimality of Acc r means that to prove ∀ a, Acc r a → p a, it suffices to show {a | p a} is an r-inductive set, i.e. ∀ a, (∀ b, r b a → p b) → p a. In other words, Acc r a allows us to assume p b for all "b < a" when proving p a.

In this particular proof, we want to show the relation rel := fun l m ↦ List.Lex r l.val m.val on {l : List α // l.Chain' (flip r)} is well-founded, i.e. every element is accessible. A list is either nil or of the form a :: l, and List.nil is rel-minimal ("bottom element") and therefore trivially accessible (such goals are solved by apply Acc.intro; rintro ⟨_⟩ ⟨_⟩ in the proof). In the a :: l case we apply r-induction on a and assume that b :: m is accessible for all "b < a", which in particular implies that l is accessible because l.head < a if it's not nil. Due to accessibility of l, we may do induction on l and assume a :: m is accessible for all m such that rel m l. Finally, to show a :: l is accessible, consider all n such that rel n (a :: l): if n ≠ nil then either n.head < a or n = a :: m for some m satisfying rel m l, and we see in both cases n is accessible by the inductive hypotheses.

The main tricky thing is that we need to do induction on l' which is l combined with a proof hl that it's a chain under flip r, and is not a free variable that we can directly do induction on. The whole have hl, revert hl, clear_value l' business has the sole purpose to massage l' := ⟨l, hl⟩ into a free variable.