## Stream: new members

### Topic: lexicographic ordering on tuples

#### Scott Morrison (Mar 03 2019 at 02:53):

How do I most easily summon the instance giving lexicographic ordering on a tuple? I want has_le (ℕ × ℕ × ℕ).

#### Scott Morrison (Mar 03 2019 at 04:25):

Do we not have preorder (A \times B) given preorder A and preorder B? I'm having trouble finding it.

#### Kevin Buzzard (Mar 03 2019 at 09:11):

I guess (a) preorder is a class and (b) there is probably more than one kind of preorder on A x B that one might want to consider in general, so maybe putting one in mathlib is a dangerous game :-) OTOH wasn't there a thread about this one where Sebastian posted a one-liner just saying "oops" with a link to a howler in core Lean? Maybe that was a preorder on list X given a preorder on X though.

#### Gabriel Ebner (Mar 03 2019 at 09:24):

I think the only lexicographic order in core is on psigma and not pairs: psigma.lex https://github.com/leanprover/lean/blob/cbd2b6686ddb566028f5830490fe55c0b3a9a4cb/library/init/data/sigma/lex.lean

#### Sebastien Gouezel (Mar 03 2019 at 09:36):

(found with grep -r "instance.*preorder" .)

#### Scott Morrison (Mar 03 2019 at 09:36):

Ok, so it seems the lexicographic orderings are not there. And yes, as Kevin says, there shouldn't be a global instance for them.

#### Scott Morrison (Mar 03 2019 at 09:37):

Nevertheless, it seems like they should be made available in mathlib?

#### Scott Morrison (Mar 03 2019 at 09:37):

I've since implemented it this afternoon, so I can PR it if desired.

#### Kenny Lau (Mar 03 2019 at 09:43):

of course we have lexicographic ordering, what are you talking about

Where is it?

It's in core

#### Kenny Lau (Mar 03 2019 at 09:44):

prod.lex

#### Kevin Buzzard (Mar 03 2019 at 09:44):

That's a good name for it

#### Scott Morrison (Mar 03 2019 at 09:46):

Are you talking about the one in wf.lean?

yes

#### Scott Morrison (Mar 03 2019 at 09:46):

there's not even a proof that it's a preorder?

#### Scott Morrison (Mar 03 2019 at 09:47):

I think we want a bit more than that. :-)

#### Kenny Lau (Mar 03 2019 at 09:49):

you can be sure that it's there because ordinal uses it

#### Kenny Lau (Mar 03 2019 at 09:49):

it's prod.lex.is_well_order in order.basic

#### Kenny Lau (Mar 03 2019 at 09:49):

(sadly it uses the other hierarchy)

#### Scott Morrison (Mar 03 2019 at 09:51):

Currently searching for the word "lexicographic" in mathlib points to well_founded_recursion.md, and data/list/basic.lean.

#### Scott Morrison (Mar 03 2019 at 09:51):

I'll add it to my list of things for students to do, I guess.

#### Kenny Lau (Mar 03 2019 at 09:51):

lex.

#### Scott Morrison (Mar 03 2019 at 09:53):

Knowing you need to search for arbitrarily chosen prefixes of standard mathematical terms is not really good enough. Finding stuff in mathlib is ridiculously difficult already.

#### Sebastien Gouezel (Mar 03 2019 at 10:16):

There's a very handy feature of Isabelle to find stuff, as follows. If you type a lemma, then it will search (asynchronously, so it will not slow everything down) if there is a lemma in the library that matches the statement (up to reordering of the variables), and if so it will tell you the name of the statement.

A similar handy tactic in Lean, say search_library, would try to apply all the lemmas in the library to the current goal and close all of their premises using assumption, and if it works apply this lemma and tell you its name in the trace output. So, if you don't remember the name of the lemma saying that n < m <-> n.succ <= mon nat, then just type this statement as a have:in your proof, call search_library and get the name. As I don't know anything about tactics, I don't know if it would be easy to implement, and how slow it would be...

#### Kenny Lau (Mar 03 2019 at 10:18):

tactic.find

#### Patrick Massot (Mar 03 2019 at 10:19):

find is ridiculously slow, so I guess anything smarter would be insufferably slow (in Lean 3 at least)

#### Scott Morrison (Mar 03 2019 at 10:36):

I am working on search_library right this second. (aka back) No promises that it will actually be fast enough to run on the whole library :-)

#### Neil Strickland (Mar 03 2019 at 12:04):

Fancier search tools would obviously be welcome, but I also think that it should be more standard practice to add relevant keywords as comments in mathlib so that a straightforward grep will find them. Perhaps there should be a structured syntax for this, like

/-
- @keywords: lexicographic order, dictionary order
-/


#### Scott Morrison (Mar 03 2019 at 21:09):

I'm not sure that the structured syntax adds anything, but just piles of greppable text all through mathlib would be amazing. :-)

Last updated: May 14 2021 at 04:22 UTC