lexicographic ordering on tuples

Stream: new members

[Scott Morrison]

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

[Scott Morrison]

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

[Kevin Buzzard]

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.

[Kevin Buzzard]

https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/string_lt.20doesn't.20match.20its.20spec/near/128392824 yeah it was lists.

[Gabriel Ebner]

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]

preorder on product:
https://github.com/leanprover-community/mathlib/blob/fb8001d6fd786a67e01d022241f01b7017ae0825/src/order/basic.lean#L217

[Sebastien Gouezel]

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

[Scott Morrison]

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]

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

[Scott Morrison]

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

[Kenny Lau]

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

[Kevin Buzzard]

Where is it?

[Kenny Lau]

It's in core

[Kenny Lau]

prod.lex

[Kevin Buzzard]

That's a good name for it

[Scott Morrison]

Are you talking about the one in wf.lean?

[Kenny Lau]

yes

[Scott Morrison]

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

[Scott Morrison]

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

[Kenny Lau]

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

[Kenny Lau]

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

[Kenny Lau]

(sadly it uses the other hierarchy)

[Scott Morrison]

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

[Scott Morrison]

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

[Kenny Lau]

lex.

[Scott Morrison]

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]

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]

tactic.find

[Patrick Massot]

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

[Kevin Buzzard]

And find doesn't work very well

[Scott Morrison]

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]

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]

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