Programming with sets

Stream: new members

[Mike Hamburg]

Hi all, I'm new-ish to Lean, and I'm looking to use it as a general-purpose programming language where I can write some code and later prove correctness properties about it.

[Mike Hamburg]

One thing I've been struggling with is how to program with sets. (Edit: by this of course I mean finite sets, such as Python's frozenset or Haskell's Data.Set.) I have some inductive type T (e.g. a basic algebraic datatype), and I can derive BEq and Ord on T, and then I can make TreeSet T. But TreeSet doesn't expose some pretty basic operations such as intersection, and also doesn't have particularly many lemmas about it, especially compared to Finset T. But Finset T depends on having a LinearOrder. The automatically derived Ord instance ought to be a LinearOrder, but as far as I can tell the compiler won't derive LinearOrder for that type and it's a pain to prove for an inductive type with a few constructors.

[Mike Hamburg]

Also it seems to me that Finset, since it's based on unordered lists, will be quite slow. Eg it ought to take quadratic time for union and intersection, unless I'm missing something

[Mike Hamburg]

Is there a set type that makes this easy, where I get the usual set operations like \cap, \cup, \in etc, and can prove theorems about them, without having to write a lot of boilerplate?

[Matthew Ballard]

The only other "set" I can remember off the top of my head is docs#Std.HashSet

[Mario Carneiro]

Finset doesn't depend on linear orders, it only needs equality on the type

[Mario Carneiro]

If you want better performance you need either a linear order (give or take) or a hash function on the key type

[Mario Carneiro]

You can use RBSet as an alternative to TreeSet, it has more lemmas

[Mike Hamburg]

Yeah, RBTree could be another option, seems pretty similar to TreeSet. Finset doesn't need linear orders by itself, but to get the answer out as a list, without running into noncomputable, you have to sort it which requires linear orders unless I'm missing something.

[Mike Hamburg]

Out of curiosity, none of these "practical" sets implement Inter or have named intersection or disjointness functions, do they? Only Finset does?

[Mike Hamburg]

Also is there a way to derive a LinearOrder for inductive types? The derived Ord ought to induce a LinearOrder (if this is true for all of the fields, but it's true for common ones like Nat and Bool and String) and proving this should be more or less mechanical but also kind of a pain to do by hand

[Kenny Lau]

@Mike Hamburg I mean, you can't have everything, lol

[Robin Arnez]

Mike Hamburg schrieb:

derive a LinearOrder for inductive types

That would need deriving Std.TransOrd and deriving Std.LawfulEqOrd which doesn't exist yet and also it's very weird to induce a linear order on a type that is not like, linear

[Robin Arnez]

Intersection would be s1.filter s2.contains btw and I would use Std.ExtHashSet instead Std.TreeSet for having filter lemmas and extensionality

[Robin Arnez]

e.g.

import Std.Data.ExtHashSet

theorem inter_comm [BEq α] [Hashable α] [LawfulBEq α] (s₁ s₂ : Std.ExtHashSet α) :
    s₁.filter s₂.contains = s₂.filter s₁.contains := by
  ext k
  simp [and_comm]

although we don't specifically have intersection on these as a function or operator

[Mike Hamburg]

ah ok, that's not too bad for the inter_comm lemma.

I'm not sure what you mean about inducing a linear order on a type that's not linear?

[Kenny Lau]

@Mike Hamburg it might be worth asking this, what are you planning to do with sets?

[Robin Arnez]

I mean you usually have a linear order when ≤ "makes sense", e.g. for natural numbers, rationals, reals. Notably α × β has an ≤ which doesn't form a linear order (x.1 ≤ y.1 ∧ x.2 ≤ y.2). For the purposes described you would certainly use Ord instead which has a lot of lemmas under e.g. Std.TransCmp but no deriving handler currently (but I mean LinearOrder is not different in that regard).

[Mike Hamburg]

Oh hey Kenny! Long time no see, unless you're a different Kenny Lau. Basically code generation, which uses sets for various analysis purposes. The code generation doesn't have to be particularly fast, but being gratuitously quadratic would be a bummer

[Mike Hamburg]

@Robin Arnez I see. I was thinking of using a lexicographic order for the types in question, as Ord does. I guess that's why Lean doesn't auto-derive Ord for product types unless you use Lex... I was wondering why that would be the case

[Robin Arnez]

You can find it under the name lexOrd. Not sure why it's not an instance but if you need it:
attribute [instance] lexOrd

[Kevin Buzzard]

My guess is that it's not an instance because making it an instance would be tantamount to saying "this is the only order you are allowed on a product" which is certainly not true in general.

[Aaron Liu]

Products already have an order instance (the product order), it's just not a linear order for most of the time

[Robin Arnez]

Yeah right but there is no reason to make Ord compatible with LE. I'd say Ord is the programming order and LE is the mathematical order.

[Aaron Liu]

Robin Arnez said:

You can find it under the name lexOrd. Not sure why it's not an instance but if you need it:
attribute [instance] lexOrd

Since it would conflict with the usual order instance. If you want it as an instance there is docs#Prod.Lex.instOrdLexProd

[Aaron Liu]

Robin Arnez said:

Yeah right but there is no reason to make Ord compatible with LE. I'd say Ord is the programming order and LE is the mathematical order.

docs#LinearOrder bundles a compatible Ord instance

[Robin Arnez]

Yeah but the usual product order is not a linear order so there are no instance diamonds to worry about

[Robin Arnez]

I understand why you'd want LE and LT to be lexicograhical only on Lex but Ord?

[Aaron Liu]

Robin Arnez said:

Yeah but the usual product order is not a linear order so there are no instance diamonds to worry about

If either of the components is a subsingleton you get a linear order

[Robin Arnez]

Then it's equivalent to the lexicograhical order though..?

[Robin Arnez]

Also, we don't have that as an instance, do we?