Zulip Chat Archive

Stream: maths

Topic: lexicographic ordering on lists


view this post on Zulip 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 :=
_

view this post on Zulip Scott Morrison (Jun 12 2020 at 14:02):

Yeah, that is pretty bad.

view this post on Zulip 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.

view this post on Zulip Scott Morrison (Jun 12 2020 at 14:14):

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

view this post on Zulip Johan Commelin (Jun 12 2020 at 14:19):

@Scott Morrison Thanks!

view this post on Zulip 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

view this post on Zulip Johan Commelin (Jun 12 2020 at 15:28):

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

view this post on Zulip 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 α].

view this post on Zulip 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

view this post on Zulip Pedro Minicz (Jun 12 2020 at 15:56):

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

view this post on Zulip Johan Commelin (Jun 12 2020 at 15:56):

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

view this post on Zulip Johan Commelin (Jun 12 2020 at 15:57):

Yup, you are right about nil_lt.

view this post on Zulip Pedro Minicz (Jun 12 2020 at 15:57):

Oops, my bad. Mistyped that.

view this post on Zulip Johan Commelin (Jun 12 2020 at 15:58):

No worries (-;

view this post on Zulip Kevin Buzzard (Jun 12 2020 at 17:34):

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


Last updated: May 14 2021 at 19:21 UTC