lexicographic ordering on lists

Stream: maths

[Johan Commelin]

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]

Yeah, that is pretty bad.

[Scott Morrison]

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]

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

[Johan Commelin]

@Scott Morrison Thanks!

[Pedro Minicz]

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]

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

[Pedro Minicz]

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

[Pedro Minicz]

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]

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

[Johan Commelin]

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

[Johan Commelin]

Yup, you are right about nil_lt.

[Pedro Minicz]

Oops, my bad. Mistyped that.

[Johan Commelin]

No worries (-;

[Kevin Buzzard]

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