WellFoundedRelation of a lexicographic order

Stream: new members

[ZHAO Jiecheng]

I think lexicographic order is wellfounded and we may have something like instance [WellFoundedRelation α] : WellFoundedRelation (List α) where to imply it. Does anyone know if we have this and where it is?
Or just use measure but how can I map strings with different length to a number ?

[ZHAO Jiecheng]

found at https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/List/Chain.html#WellFounded.list_chain' but it only works on r-decreasing chains .

[Notification Bot]

ZHAO Jiecheng has marked this topic as resolved.

[Notification Bot]

ZHAO Jiecheng has marked this topic as unresolved.

[ZHAO Jiecheng]

I guess lexicographic order is not well founded maybe.

[Timo Carlin-Burns]

The default < relation on lists is actually already defined to be the lexicographic order (assuming you import Mathlib.Data.List.Lex). All that's missing is an instance of

import Mathlib.Data.List.Lex

instance List.instWellFoundedLT {α : Type*} [LT α] [WellFoundedLT α] : WellFoundedLT (List α) where
  wf := sorry

[ZHAO Jiecheng]

Timo Carlin-Burns said:

The default < relation on lists is actually already defined to be the lexicographic order (assuming you import Mathlib.Data.List.Lex). All that's missing is an instance of

import Mathlib.Data.List.Lex

instance List.instWellFoundedLT {α : Type*} [LT α] [WellFoundedLT α] : WellFoundedLT (List α) where
  wf := sorry

Do you have any suggestions on how to prove it? Is there a quick lemma that might be useful, or should I start from the very beginning if I want to use it?

[ZHAO Jiecheng]

I think isStrictTotalOrder should be very helpful when prove WellFoundedLT. How can I find lemmas connect them?

[ZHAO Jiecheng]

I found Mathlib.Data.Finsupp.Lex and there is WellFoundedLT.

[Timo Carlin-Burns]

I actually am not sure whether it is well founded. I think maybe not. I'm working on a counterexample now

[Timo Carlin-Burns]

Here is an infinite strictly decreasing sequence of List (Fin 2) under the lexicographic order

import Mathlib.Data.List.Lex

def mySeq (n : Nat) : List (Fin 2) :=
  List.replicate n 0 ++ [1]

theorem mySeq_lt (n : Nat) : mySeq (n + 1) < mySeq n := by
  simp only [mySeq, List.replicate_succ', List.append_assoc]
  apply List.Lex.append_left
  decide

[ZHAO Jiecheng]

Timo Carlin-Burns said:

Here is an infinite strictly decreasing sequence of List (Fin 2) under the lexicographic order

import Mathlib.Data.List.Lex

def mySeq (n : Nat) : List (Fin 2) :=
  List.replicate n 0 ++ [1]

theorem mySeq_lt (n : Nat) : mySeq (n + 1) < mySeq n := by
  simp only [mySeq, List.replicate_succ', List.append_assoc]
  apply List.Lex.append_left
  decide

Thank you very much. It is not well founded. Then I guess for all the List that is shorter than a certain length, it is well founded on lexicographic order. This should be enough from my problem. Let me see if I can prove it.

[ZHAO Jiecheng]

It's hard to prove a general lemma. The best way to use it in practice is to use a limited character set and a limited length of List, and map the string to a Nat to prove termination.