## Stream: maths

### Topic: lexicographic ordering on lists

#### Johan Commelin (Jun 12 2020 at 12:36):

mathlib gives a lex ordering on lists. But I don't know how to use it.

import data.list.basic

example (l : list ℕ) (n : ℕ) (h : l.length = n) :
list.repeat 0 n ≤ l :=
_


#### Scott Morrison (Jun 12 2020 at 14:07):

We are missing

lemma list.nil_le {α : Type*} [linear_order α] (L : list α) : [] ≤ L :=
sorry

lemma list.nil_lt {α : Type*} [linear_order α] (a : α) (L : list α) : [] < a :: L :=
sorry

lemma list.cons_le_iff {α : Type*} [linear_order α] (a a' : α) (L L' : list α) :
a :: L ≤ a' :: L' ↔ (a < a') ∨ (a = a' ∧ L ≤ L') :=
sorry


which would make it usable.

#### Scott Morrison (Jun 12 2020 at 14:14):

I am very sleepy, so these are pessimal proofs, but proofs.

#### Johan Commelin (Jun 12 2020 at 14:19):

@Scott Morrison Thanks!

#### Pedro Minicz (Jun 12 2020 at 14:28):

list.nil_le already exists on mathlib as list.nil_lt_cons:

import data.list.basic

variables {α : Type*} [linear_order α]

lemma list.nil_lt (a : α) (l : list α) : [] < a :: l := list.nil_lt_cons a l


#### Johan Commelin (Jun 12 2020 at 15:28):

@Pedro Minicz It's not exactly the same, right.

#### Pedro Minicz (Jun 12 2020 at 15:53):

Well, the only difference I could see in the previous example was that list.nil_lt needed [linear_order α].

#### Pedro Minicz (Jun 12 2020 at 15:53):

As far as I can see, in the following they are the exact same:

import data.list.basic

variables {α : Type*} [has_lt α]

lemma list.nil_lt (a : α) (l : list α) : [] < a :: l := list.nil_lt_cons a l
-- lemma list.nil_lt : ∀ (a : α) (l : list α), [] < a :: l := list.nil_lt_cons

#check @list.nil_lt
#check @list.nil_lt_cons


#### Pedro Minicz (Jun 12 2020 at 15:56):

As expected, the commented out eta-reduced form gives the same results.

#### Johan Commelin (Jun 12 2020 at 15:56):

Ooh, sorry, you are talking about nil_lt. In your previous post you mentioned nil_le.

#### Johan Commelin (Jun 12 2020 at 15:57):

Yup, you are right about nil_lt.

#### Pedro Minicz (Jun 12 2020 at 15:57):

Aah, lt on lists, reminds me of one of my favourite Zulip posts ever