Zulip Chat Archive

Stream: new members

Topic: lexicographic ordering on tuples


view this post on Zulip 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 (ℕ × ℕ × ℕ).

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

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

view this post on Zulip Kevin Buzzard (Mar 03 2019 at 09:13):

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

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

view this post on Zulip Sebastien Gouezel (Mar 03 2019 at 09:34):

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

view this post on Zulip Sebastien Gouezel (Mar 03 2019 at 09:36):

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

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

view this post on Zulip Scott Morrison (Mar 03 2019 at 09:37):

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

view this post on Zulip Scott Morrison (Mar 03 2019 at 09:37):

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

view this post on Zulip Kenny Lau (Mar 03 2019 at 09:43):

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

view this post on Zulip Kevin Buzzard (Mar 03 2019 at 09:43):

Where is it?

view this post on Zulip Kenny Lau (Mar 03 2019 at 09:44):

It's in core

view this post on Zulip Kenny Lau (Mar 03 2019 at 09:44):

prod.lex

view this post on Zulip Kevin Buzzard (Mar 03 2019 at 09:44):

That's a good name for it

view this post on Zulip Scott Morrison (Mar 03 2019 at 09:46):

Are you talking about the one in wf.lean?

view this post on Zulip Kenny Lau (Mar 03 2019 at 09:46):

yes

view this post on Zulip Scott Morrison (Mar 03 2019 at 09:46):

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

view this post on Zulip Scott Morrison (Mar 03 2019 at 09:47):

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

view this post on Zulip Kenny Lau (Mar 03 2019 at 09:49):

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

view this post on Zulip Kenny Lau (Mar 03 2019 at 09:49):

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

view this post on Zulip Kenny Lau (Mar 03 2019 at 09:49):

(sadly it uses the other hierarchy)

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

view this post on Zulip Scott Morrison (Mar 03 2019 at 09:51):

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

view this post on Zulip Kenny Lau (Mar 03 2019 at 09:51):

lex.

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

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

view this post on Zulip Kenny Lau (Mar 03 2019 at 10:18):

tactic.find

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

view this post on Zulip Kevin Buzzard (Mar 03 2019 at 10:32):

And find doesn't work very well

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

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

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