Zulip Chat Archive

Stream: new members

Topic: 23trees


view this post on Zulip Edward Ayers (Aug 09 2018 at 23:14):

Dear all, I am writing a tactic and I want to keep a set of things in a datastructure for quick access. In other languages you would use a 23tree or similar. Is there something like this in the Lean library? Otherwise I am fine just keeping a list of objects and removing the dupes but I thought I'd check if the datastructure is in there.

view this post on Zulip Simon Hudon (Aug 09 2018 at 23:17):

Yes there's the rbmap which should be available without imports

view this post on Zulip Edward Ayers (Aug 09 2018 at 23:17):

perhaps I can just use set and lean will magically figure it out?

view this post on Zulip Simon Hudon (Aug 09 2018 at 23:17):

You can see the api here: https://github.com/leanprover/lean/blob/a666c7f04eb77ecfd29f253b7fc389a4507404f1/library/init/data/rbmap/basic.lean

view this post on Zulip Simon Hudon (Aug 09 2018 at 23:18):

perhaps I can just use set and lean will magically figure it out?

Unfortunately, not yet.

view this post on Zulip Edward Ayers (Aug 09 2018 at 23:18):

thanks

view this post on Zulip Simon Hudon (Aug 09 2018 at 23:19):

No problems :)

view this post on Zulip Edward Ayers (Aug 09 2018 at 23:20):

If I want to write my own helper methods for list, is it correct to write in the form def list.myextension ...?

view this post on Zulip Simon Hudon (Aug 09 2018 at 23:26):

Yes, sure. You can also put it in namespace list ... end list so that, inside the namespace, you don't have to specify list. everywhere but outside, you can still use my_list.myextension to call it with argument my_list

view this post on Zulip Edward Ayers (Aug 09 2018 at 23:41):

Is there a better way of listing all of the local constants which appear in an expr other than recursion over expr?

view this post on Zulip Simon Hudon (Aug 09 2018 at 23:43):

you can use expr.fold.

view this post on Zulip Simon Hudon (Aug 09 2018 at 23:45):

But if you use mathlib, you can import meta.exprand use expr.list_local_const

view this post on Zulip Edward Ayers (Aug 09 2018 at 23:52):

fab

view this post on Zulip Edward Ayers (Aug 09 2018 at 23:57):

What is the difference between import and open?

view this post on Zulip Simon Hudon (Aug 09 2018 at 23:58):

import is about modules i.e. source files and open is about namespaces which can span multiple files.

view this post on Zulip Edward Ayers (Aug 10 2018 at 00:00):

if I import a source file, is that effectively the same as pasting it above my code?

view this post on Zulip Simon Hudon (Aug 10 2018 at 00:02):

You could say that. But it's a smart paste: it does not paste the same module more than once.

view this post on Zulip Mario Carneiro (Aug 10 2018 at 01:54):

perhaps I can just use set and lean will magically figure it out?

Is that a thing people want? It is conceivable that we could associate data to a typeclass on set, basically the same as fintype s currently but with a tree-like data structure. Currently you have to use explicit data structures like rbmap or hash_map or finmap

view this post on Zulip Simon Hudon (Aug 10 2018 at 01:59):

What would the type class be applied to? The element type?

view this post on Zulip Mario Carneiro (Aug 10 2018 at 02:09):

the set

view this post on Zulip Simon Hudon (Aug 10 2018 at 02:10):

I'm not eager to go down that rabbit hole. In Haskell, a similar situation has created multiple types for strings and multiple solutions to simplify the situation once and for all with unclear consequences.

view this post on Zulip Mario Carneiro (Aug 10 2018 at 02:11):

in some ways it seems appealing, similar to decidability of a prop, you have representability of a set

view this post on Zulip Mario Carneiro (Aug 10 2018 at 02:12):

but it's probably not good if the typeclass is not a subsingleton, meaning you have to hide a lot of structure

view this post on Zulip Simon Hudon (Aug 10 2018 at 02:12):

Yeah but with prop and decidability, the representation is unique.

view this post on Zulip Mario Carneiro (Aug 10 2018 at 02:13):

you can always perform a suitable quotient to make it a subsingleton

view this post on Zulip Mario Carneiro (Aug 10 2018 at 02:14):

but you need more than decidable_eq if you want to have any representation better than an association list (which you already get with fintype s)

view this post on Zulip Simon Hudon (Aug 10 2018 at 02:14):

That creates another mess: if you take two sets as parameters, you have to anticipate that they have vastly different representations.

view this post on Zulip Mario Carneiro (Aug 10 2018 at 02:15):

what do you mean? If it is a binary tree structure the only representation ambiguity is wrt tree rotations

view this post on Zulip Simon Hudon (Aug 10 2018 at 02:16):

No I mean if you have a function that takes two sets as a parameter, one might be a binary search tree, the other may be represented as an assoc list (if I understand your quotient idea properly). That makes taking their union needlessly complicated.

view this post on Zulip Mario Carneiro (Aug 10 2018 at 02:16):

oh, no I wasn't thinking that

view this post on Zulip Mario Carneiro (Aug 10 2018 at 02:17):

if you have two data structures which are both applicable here you have two typeclasses

view this post on Zulip Mario Carneiro (Aug 10 2018 at 02:17):

I'm not even sure how to implement type ambiguity of that kind

view this post on Zulip Simon Hudon (Aug 10 2018 at 02:18):

Actually, I think existential types would be the best way to go. But I don't advise trying it at home.

view this post on Zulip Mario Carneiro (Aug 10 2018 at 02:18):

existential types don't really work in lean though

view this post on Zulip Mario Carneiro (Aug 10 2018 at 02:18):

because of predicativity

view this post on Zulip Simon Hudon (Aug 10 2018 at 02:19):

Really? But if you have structure where one of the field is a type and the next is a type class assumption, doesn't that work?

view this post on Zulip Mario Carneiro (Aug 10 2018 at 02:19):

It's possible but it will live in a higher universe

view this post on Zulip Simon Hudon (Aug 10 2018 at 02:20):

Yeah, it is annoying to say the least

view this post on Zulip Mario Carneiro (Aug 10 2018 at 02:20):

I guess it might work if it acts a bit like monad or traversable-type typeclasses

view this post on Zulip Simon Hudon (Aug 10 2018 at 02:20):

What kind of type classes do you have in mind? Do they including operations like union, intersection, empty set?

view this post on Zulip Mario Carneiro (Aug 10 2018 at 02:21):

At the very least

view this post on Zulip Mario Carneiro (Aug 10 2018 at 02:21):

Indeed there probably isn't much else they can support

view this post on Zulip Simon Hudon (Aug 10 2018 at 02:21):

I found curious wrinkle about finset and traversable by the way but I think it's a different conversation.

view this post on Zulip Mario Carneiro (Aug 10 2018 at 02:22):

that sounds ominous

view this post on Zulip Mario Carneiro (Aug 10 2018 at 02:22):

I recall Johannes having difficulty defining the BNF instance for multiset because of quotients, I assume the issue is similar here

view this post on Zulip Simon Hudon (Aug 10 2018 at 02:23):

I think having that kind of type class would be useful but it should be a last resort of generalization. You should probably stick to concrete types of set representations in the type of your computable functions as much as possible.

view this post on Zulip Mario Carneiro (Aug 10 2018 at 02:24):

Does haskell have a typeclass for finite maps? Or is it just traversable

view this post on Zulip Simon Hudon (Aug 10 2018 at 02:25):

As for the wrinkle. I managed to make multiset sort-of traversable -- sort-of because in traverse (not its laws) I require the applicative to be lawful and commutative. In finset, I didn't manage to make it sort-of traversable because I would need seq to be idempotent. That's not a big wrinkle but our conversation reminded me of that.

view this post on Zulip Simon Hudon (Aug 10 2018 at 02:26):

Officially, it's mostly just traversable and the like. Some packages have classes for that but they aren't very useable and don't simplify much.

view this post on Zulip Simon Hudon (Aug 10 2018 at 02:27):

I think I just understood why you talked of monad and traversable. I think you're right. You might also need a lattice or a monoid

view this post on Zulip Mario Carneiro (Aug 10 2018 at 02:34):

Why does seq have to be idempotent? Seems like the finset traverse should just refer to multiset traverse

view this post on Zulip Simon Hudon (Aug 10 2018 at 02:35):

Because somewhere in the laws, you need to prove the equivalence between pruning duplicates before and after a traversal with pruning them only after.

view this post on Zulip Simon Hudon (Aug 10 2018 at 02:38):

That's for a lawful traversable instance. The traverse implementation itself works for finset

view this post on Zulip Mario Carneiro (Aug 10 2018 at 02:40):

I just noticed that there are five axioms in is_lawful_traversable. Are none of them redundant?

view this post on Zulip Simon Hudon (Aug 10 2018 at 02:40):

I suspect one might be but I haven't managed to prove it.

view this post on Zulip Simon Hudon (Aug 10 2018 at 02:41):

Two of them look really similar and it's odd that I can't prove one from the other.

view this post on Zulip Mario Carneiro (Aug 10 2018 at 02:43):

do you know any category theoretic treatment of traversable?

view this post on Zulip Simon Hudon (Aug 10 2018 at 02:44):

I know of a few papers that I still need to read. I don't know how far they go into category theory

view this post on Zulip Mario Carneiro (Aug 10 2018 at 02:47):

Haskell only mentions axioms 1,2,5

view this post on Zulip Mario Carneiro (Aug 10 2018 at 02:47):

the map_traverse and traverse_map axioms aren't mentioned

view this post on Zulip Simon Hudon (Aug 10 2018 at 02:51):

That's right but the laws it does mention do not connect map and traverse. In the case of finset, the trouble comes from proving comp_traverse anyway.

view this post on Zulip Simon Hudon (Aug 10 2018 at 02:52):

(the map of t, not f)

view this post on Zulip Mario Carneiro (Aug 10 2018 at 02:58):

Lol @ "origami programming"

In the origami style of programming (Meijer et al. , 1991; Gibbons, 2002; Gibbons, 2003), the structure of programs is captured by higher-order recursion operators such as map, fold and unfold. [from http://www.cs.ox.ac.uk/jeremy.gibbons/publications/iterator.pdf ]

view this post on Zulip Simon Hudon (Aug 10 2018 at 02:58):

:laughing:

view this post on Zulip Simon Hudon (Aug 10 2018 at 02:59):

I guess you now know that bifunctor and bitraversable are coming

view this post on Zulip Simon Hudon (Aug 10 2018 at 03:00):

Also: monotraversable to use traversable-like techniques on monomorphic structures like strings

view this post on Zulip Mario Carneiro (Aug 10 2018 at 03:13):

what does that mean? What is the type of traverse in this case?

view this post on Zulip Simon Hudon (Aug 10 2018 at 03:16):

that would look like

class mono_traversable (t a : Type u) :=
(traverse : Π {m : Type u  Type u} [applicative m],
   (a  m a)  t  m t)

view this post on Zulip Johan Commelin (Aug 10 2018 at 04:50):

Lean has chosen to handle modules and namespaces orthogonally. A nice choice, I think. It means that if you need to prove something about lists, it doesn't need to go into the file list.lean, you can just prove list.foobar in your own file. Or you write

namespace list

lemma foobar : ....

end list

Of course, that also means that you don't get access to list.foobar by just import data.list. You will also have to import the file where list.foobar is stated.

open list means that inside the section/file where you issued the open command, you can just write foobar instead of list.foobar. If you already had a foobar, this would lead to ambiguity. You can close one of them with close. The root namespace is called _root_.

view this post on Zulip Johan Commelin (Aug 10 2018 at 07:11):

But if you use mathlib, you can import meta.exprand use expr.list_local_const

I really think that it is a pity that there is group theory in core, and stuff like this in mathlib... I wish it was the other way round (-;


Last updated: May 11 2021 at 00:31 UTC