Relationship between set and finset

[dselsam]

Hi,

I apologize in advance if this is not the appropriate place for questions like this. Please feel free to ignore if it is off-topic or just generally not helpful.

Could somebody please explain the envisioned interactions between the set library and the finset library? In particular, is finset designed to be user-facing? I fear it might get confusing to deal with both types of sets at the same time, especially when the notation means slightly different things in different places. Another option might be to use the finset library to support a finite_set type class.

inductive finite_set [class] (xs : set T) := 
| mk : ∀ (fxs : finset T), to_set fxs = xs → finite_set xs

We could then use the lemmas in the finset library to propagate the finite_set property, with instances such as:

definition finite_set_empty [instance] : finite_set ∅
definition finite_set_finset [instance] (fxs : finset T) : finite_set (to_set fxs)
definition finite_set_insert [instance] (xs : set T) [fxs : finite_set xs] (x : T) : finite_set (insert x xs)
definition finite_set_union [instance] (xs : set T) [fxs : finite_set xs] (ys : set T) [fys : finite_set ys] : finite_set (xs ∪ ys)
definition finite_set_inter1 [instance] (xs : set T) [fxs : finite_set xs] (ys : set T) [ys_dec : decidable_pred ys] : finite_set (xs ∩ ys)
definition finite_set_inter2 [instance] (xs : set T) [fxs : finite_set xs] (ys : set T) [ys_dec : decidable_pred ys] : finite_set (ys ∩ xs)
definition finite_set_set_of [instance] (xs : set T) [fxs : finite_set xs] : finite_set (set.set_of xs)

definition finite_set_bounded_nats [instance] (ub : nat) : finite_set (λ n:ℕ, n < ub)

We could then define versions of all functions that only make sense on finite sets in terms of the type class, e.g.:

definition card (xs : set T) [fxs : finite_set xs] := finset.card (get_finset fxs)

The net result is that users could use traditional set-theoretic notation everywhere, have it always mean the same thing, and still make use of finiteness when necessary without needing to track it explicitly. For example, one could write:

eval card { n : ℕ | n < 10 ∧ odd n }

If this approach seems appealing, I would be happy to write a draft of it.

Thanks,

Daniel

[avigad]

Dear Daniel,

Thanks for this posting -- it is perfectly appropriate, and most helpful. There is also a Google-groups mailing list, lean-discuss, that we have been using internally for more open-ended discussions. I will send you an invitation to that as well.

About a month ago, I lost a lot of sleep over the issues regarding sets and finsets and exchanged some overwrought e-mails with @leodemoura and @htzh. As you have probably gathered, the root of the problem is that, constructively, they are very different sorts of objects: finsets are lists up to permutation, and sets are arbitrary predicates. In general, they support different operations, and although finsets can be cast to sets, we still need to define separate operations on both.

I thought about a solution like the one you are suggesting. I think the problem is that an expression like card s means more than you think it means: there is a hidden argument for a proof-relevant piece of data that has been inferred. So that it is possible that in one part of a proof we have foo1 = card s, somewhere else we have foo2 = card s, and yet we can prove foo1 ≠ foo2.

I don't think this is science fiction. Suppose you are doing a calculation, and you rewrite card (a ∩ b) to card (b ∩ a). Then suppose you try to combine that with another equation card (b ∩ a) = t. The inference is likely to fail, because you have different witnesses to the finiteness of b ∩ a. On the right-hand side, it is probably inferred from the intersection rule, given that b and a are finite. On the left-hand side, it is instead inferred by rewriting a ∩ b to b ∩ a in the proof that the latter is finite. And now we are stuck is a surreal type theory nightmare where card (b ∩ a) is no longer equal to card (b ∩ a).

What do you think? I am not sure about any of this, and your thoughts are welcome.

The conclusion I eventually reached is that we need parallel libraries and a theory that bridge the two. The message for constructive users is this: if you are working with finite sets, use finsets; if you are working with general sets, use sets; if you find yourself in need of both, for example to apply a general theorem about sets to instances that are finsets, convert the finset to the set.

I am hoping that the latter can be made palatable. The procedure to "translate" a universal theorem like forall (s : set A), P s is to instantiate s to finset.to_set t, and then use the rewrite rules in data/finset/to_set to rewrite the set operations in P to finset operations. That is something we can automate.

Also, in the classical library, we can make a solution like yours work. We define the predicate finite s to say that there exists a finset representative, and we can define a classical version of card that either infers finiteness or returns a default value of 0 if the set is not finite. Since Lean has proof irrelevance in the kernel, the "finiteness" predicate doesn't get in the way like it does in your proposal. So, in the classical library, we can just use sets and the finiteness predicate, at the expense of giving up computational behavior for finite sets.

[htzh]

Mathematically finiteness (cardinality) of a set is established through the existence of a bijection to a finite ordinal. The finset design internalized the bijection to a nodup list and the quot over the permutation is the equivalent of the existence operator. I agree with Jeremy that finset is a different animal from set. We can think of of it as a set s with the additional property that ∃ f n, bij_on f s (ord n). Could this second representation be more convenient? I haven't tried and couldn't say, but I can say that my experience with finset so far has been very positive, although the cast to set should definitely be made automatic one day so everything proved for a set can be directly used for a finset.

[avigad]

Let me add a small friendly amendment: constructively (at least in the formal framework adopted by Lean), there is a difference between saying "there exists" and having the object asserted to exist. So even given f, n, and H : ∃ f n, bij_on f s (ord n), we can't in general recover a finset representation of s. On the other hand, given the data f, n, and H' : bij_on f s (ord n), we can.

I find it helpful to keep in mind the distinction between "data" and "facts". Representing things as facts can be helpful, because it washes out distinctions between data (e.g. any two elements H1 H2 : bij_on f s (ord n) are definitionally equal in Lean). But then you can't cheat and turn a fact back into a piece of data (except in special circumstances where is possible to find the data elsewhere).

That said, Haitao's general point is correct: coding finsets as lists up to permutation or coding them as tuples s, n, f, H : bij_on f s (ord n) are essentially equivalent.

[htzh]

@avigad If you start with finset A can you get a listing of the elements (in the original order or any order)? This is something I have wondered about. If not I think it is more like the ∃ version. If you start with an enumeration list you can lift what you prove to the corresponding finset; just like if you have the bijection you can present it as the evidence for introducing the existence quantifier. Still the distinction you made between "data" and "facts" has been very helpful in thinking about how to set up a constructive proof.

[leodemoura]

If you start with finset A can you get a listing of the elements (in the original order or any order)?

In general, we cannot. We can implement finset A to list A in some special cases: 1- When there is an order on A: we return a sorted list 2- A is encodable

[avigad]

Good point: in general, you can't. You could can do it, though, for finsets of natural numbers. The quotient mechanism works as follows: if you can define a function on the underlying representations, and show that it respects the equivalence relation, you can lift that to a function on the quotient. So, for example, you can define the function which maps any finset of natural numbers to the list of elements in nondecreasing order. You can do something similar for any encodable type.

(Leo's response just arrived as I was writing this, but I will continue...)

Suppose we define the following:

structure finset' (A : Type) :=
(s : set A) (n : nat) (f : A → ?) (H : bij_on f s (ord n))

structure finset'' (A : Type) :=
(s : set A) (n : nat) (H : ∃ f, bij_on f s (ord n))

structure finset''' (A : Type) :=
(s : set A) (H : ∃ n f, bij_on f s (ord n))

(The question mark is because I am not sure how you are representing ord n.) There are maps back and forth between finset and finset', preserving the membership relation; but note that finset' is not extensional, i.e. two elements of finset' with the same members won't generally be equal (because the functions f can be different). We could quotient finset' by the relevant equality, in which case, the result would be equivalent to finset. We can map finset' -> finset'' -> finset''', but not back. On finset'', we can define card, but not the functions Leo and I have described. On finset''', we cannot even define card.

[avigad]

By the way, here is another thought I have had in the past. It might be useful to have an alternative representation of finsets, which bundles in the set that it is equivalent to:

structure finite_set (A : Type) :=
(set : set A) (finset : finset A) (eq : set = finset.to_set finset)

Then the coercion to set A simply returns the first projection. The point is that we can then define all the operations on finite_set (union, intersection, empty, ...) so that the first component returns the corresponding operation on set. The advantage is that given a b c : finite_set A, if we write ts for the coercion finite_set.to_set, we have

ts (a ∩ (b ∪ c)) = (ts a) ∩ (ts b ∪ ts c)

and this holds /definitionally/. In other words, the coercion to set does the "translation" to the set-theoretic description automatically, without any rewriting.

It would not be hard to implement finite_set on top of finset using the operations that are already present in finset.to_set, but then we would have to redo all the theorems in the finset library for finite sets, and then "hide" finset from the user (because it is too confusing to have multiple versions of finite set floating around).

Really, the right way of doing it would be to redo finset from the start to incorporate the corresponding set predicate. I don't know if it is worth the effort, just to get the nice definitional equations.

[htzh]

@avigad I think I should have said: ∃ f n, bij_on f (ord n) s instead. Classically it is equivalent to what I used but constructively this one would give us a listing of the elements if given f. With this change finset would be more similar to finset''? Good point though that lift keeps more information than ∃ in Lean formalism, for example allowing one to say card s, giving us skolemization(?).

[avigad]

No, I think the situation is the same: just knowing that such an f exists doesn't allow us to define a function to an arbitrary type that depends on such an f. Remember, exists.elim only lets us use f to prove things, i.e. to derive elements of Prop. Existence is a "fact". To build a finset, we need to /use/ f to build the list of elements, so f has to be "data".

Mike Shulman one characterized Prop as one of those parking lots you can pull into but can't back out of, at least not without severe tire damage.

[htzh]

@avigad

just knowing that such an f exists doesn't allow us to define a function to an arbitrary type that depends on such an f

I agree but in your finset' definition f is explicitly stored in the structure. Let me restate and clarify my point: knowing f and n -- that is your definition finset' is equivalent to knowing l (the pre-quot version of finset), post quot the existential form (set + exists prop) is similar to finset but the quot mechanism is more powerful by giving us skolemization card s (we should also be able to lift elt_of from nodup_list to finset so we can have elt_of s). quot corresponds to exists.intro, but we can lift to any type unlike exists.elim due to the computational nature of quot/lift.

[avigad]

Yes, that sounds right to me.

[leodemoura]

I think it would be useful to try different approaches for defining finset. The current implementation is not really general. It is implementing a special case of finite set known as "decidable finite set". Note that many operations on finset A assume that A has decidable equality.

When Jeremy and I started working on finset, we investigated how constructivists define finite sets. It seems they usually define finite sets as: a set S is finite there is a nat n and a surjection from finord n to S. That is, there is a listing of the elements of S. This definition is also problematic. For example, we cannot prove constructively that a subset of a finite set is finite.

We settled for the current finset A because it has nice computational properties. However, we know it has limitations. For example, we cannot use them for defining a finite set of functions nat -> nat.

[fpvandoorn]

So that it is possible that in one part of a proof we have foo1 = card s, somewhere else we have foo2 = card s, and yet we can prove foo1 ≠ foo2.

This sounds very strange to me. Surely we should be able to prove a theorem

theorem (xs : set T) [fxs1 fxs2 : finite_set xs] : @card T xs fxs1 = @card T xs fxs2

And now we are stuck is a surreal type theory nightmare where card (b ∩ a) is no longer equal to card (b ∩ a).

They will be equal, but not definitionally equal. True, it will be an annoyance (and confusing) that those terms are not definitionally equal, but it is not as bad as you describe.

structure finite_set (A : Type) :=
(set : set A) (finset : finset A) (eq : set = finset.to_set finset)

This looks as a very neat trick worth investigating.

[leodemoura]

quot corresponds to exists.intro, but we can lift to any type unlike exists.elim due to the computational nature of quot/lift.

This is correct, but quot.lift forces us to show that the result is the same for any two equivalent representations. For example, in finset, quot.lift allows us to "access" the list l. The same will happen if we use f and n instead of a list. There are different equivalent "listings", and we have two show the result produced by quot.lift is the same no matter which one is used. This is why we cannot define:

definition to_list {A : Type} (s : finset A) : list A :=
quot.lift_on s (λ l, elt_of l) ?M

where ?M has type ∀ (a b : nodup_list A), a ≈ b → elt_of a = elt_of b.

One possible workaround is to sort the list. In this case, we can provide the proof ?M for ∀ (a b : nodup_list A), a ≈ b → sort (elt_of a) = sort (elt_of b).

[leodemoura]

This sounds very strange to me. Surely we should be able to prove a theorem

theorem (xs : set T) [fxs1 fxs2 : finite_set xs] := @card T xs fxs1 = @card T xs fxs2

Yes, this is correct. We can prove that.

They will be equal, but not definitionally equal. True, it will be an annoyance (and confusing) that those terms are not definitionally equal, but it is not as bad as you describe.

In the current system, it would be really annoying to work with it, and it would probably confuse new users. For example, suppose we have the hypothesis h : s1 = s2, and we use rewrite h to rewrite a term containing @card T s1 fxs1. The tactic will fail because the resulting term is not type correct. The novice user will probably not understand why it failed. Note that, the pretty printer will display @card T s1 fxs1 as card s1, making the failure even more mysterious. I think we need better automation for handling a definition such as

card {T : Type} (s : set T) [h : finite_set T] : nat

We need to improve the support for definitions such as card. This is not an isolated case. A similar problem occurs with definitions that use propositions that state "pre-conditions". Example: definition last {T : Type} (l : list T) : l ≠ [] → T. I'm trying to address these issues in the new simplifier I'm working on.

This sounds as a very neat trick worth investigating.

I agree.

[fpvandoorn]

In the current system, it would be really annoying to work with it, and it would probably confuse new users.

I agree.

I'm trying to address these issues in the new simplifier I'm working on.

That sounds awesome!

[avigad]

I am sorry about the slip-up in the first post: yes, of course, the different versions of card s will be definitionally equal. But it will be really to have complicated terms that look exactly the same but are different in the implicit arguments, and I think it will be generally unworkable to calculate with them.

There are two questions here: whether to do the trick of embedding the set predicate in the definition of finset; and, following #649, whether to avoid the use of quotients. Embedding the set predicate seems worth doing -- I don't think it can hurt, and it may help.

[htzh]

For example, we cannot use them for defining a finite set of functions

Not able to enumerate functions is a bottleneck for me. We need to be able equate finite functions with lists. Right now my plan is to start with fintypes A B, first enumerate all lists of B with length of card A, use list_to_fun to obtain a function of A -> B:

definition list_to_fun [deceqA : decidable_eq A] (l : list B) (leq : length l = card A) : A → B 

then use dmap to "lift" the list of list B with length card A to the list of functions "A -> B":

definition dmap (p : A → Prop) [h : decidable_pred p] (f : Π a, p a → B) : list A → list B

then prove the list of functions is nodup and complete and thus prove fintype A -> B as well.

This is correct, but quot.lift forces us to show that the result is the same for any two equivalent representations.

Very good point. Thanks for pointing it out.

[leodemoura]

If A is a fintype, and B has decidable equality, then we can use https://github.com/leanprover/lean/blob/master/library/data/fintype.lean#L75 for creating a finite set of A -> B

Your plan is sound for showing that A -> B is a fintype when A and B are fintypes.

[dselsam]

Can't we prove that the finite sets themselves will be equal, and not just their cardinalities?

inductive finite_set [class] (xs : set T) : Type := 
| mk {} : ∀ (fxs : finset T), to_set fxs = xs → finite_set xs

lemma finite_set_irrel (xs : set T) : Π (fset1 fset2 : finite_set xs), fset1 = fset2
| (finite_set.mk fxs1 feq1) (finite_set.mk fxs2 feq2) := 
  have H1 : to_set fxs1 = to_set fxs2, from feq2⁻¹ ▸ feq1,
  have H2 : fxs1 = fxs2, from (eq_eq_to_set_eq fxs1 fxs2)⁻¹ ▸ H1,
  have H3 : eq.rec_on H1 feq1 = feq2, from eq.irrel (eq.rec_on H1 feq1) feq2,
  dcongr_arg2 finite_set.mk H2 H3

(This does not affect the problem of terms that look the same but are not definitionally equal, I just want to make sure I am not misunderstanding something basic.)

[leodemoura]

@dselsam Yes, we can. I think your approach is worth trying. However, we will need better automation in Lean to make it pleasant to use. In the current system, it would be very inconvenient to rewrite terms that contain subterms of the form @card T xs fxs. I hope the new simplifier will address this issue.

[avigad]

By the way, we can define a type of finite (partial) functions between any types A and B in the usual set-theoretic way:

{ f : finset (A × B) | ∀p1 p2, p1 ∈ f → p2 ∈ f → pr1 p1 = pr1 p2 → pr2 p1 = pr2 p2}

Here the set-builder notation is the subtype operation.

We can define a the operator of finite sets, with the property that given H : ∃! x, x ∈ s ∧ P x, the H returns the unique x. We can use that to coerce any finite function to a function (e.g. returning a default element outside for inputs outside the domain).

(This is orthgononal to showing that A -> B is a fintype in nice situations. I just thought I would mention it.)

[htzh]

Proving fintype A -> B is secondary. The question is how best to enumerate and count the number of functions satisfying certain properties, for example the number of permutations (bijective functions A -> A) is n!. I can see the way of doing it using inductions on list. If the existing finset facility can easily accommodate that I don't have to go the list route. But can one usefully start with s : finset (A -> B) and ∀ f, f ∈ s and calculate card s?

we can define a type of finite (partial) functions between any types A and B

That is a cool representation. I have to think about how to make cardinality arguments for it.

[leodemoura]

But can one usefully start with s : finset (A -> B) and ∀ f, f ∈ s and calculate card s?

Yes.

Here are the main benefits of showing that A -> B is a fintype. The "universe" finite set for A -> B would be available, and we would be able to perform computations with it. It would also allow us to easily create subsets of univ. This has many useful applications. Propositions of the form ∀ f, f ∈ s -> p f would be automatically inferred as decidable (same for exists f, f ∈ s /\ p f).

The question is how best to enumerate and count the number of functions satisfying certain properties, for example the number of permutations (bijective functions A -> A) is n!

After we show that A -> B is a fintype, we would be able to compute this number for concrete types (e.g., finord 3 -> finord 3) by just executing eval. However, we would still have to prove that for any type A with n elements the result is n!.

[leodemoura]

@htzh finfun.lean and extra.lean contain a lot of useful functionality. It would be great to move them to the standard library as soon as possible. I know you eventually plan to move the group theory module to the standard library. However, I think the support files can already be moved. They are useful for all sorts of things. For example, it is trivial to prove that a subtype of a fintype is also a fintype using the definitions and theorems from extra.lean.

[htzh]

It would be great to move them to the standard library as soon as possible.

@avigad was going to pick what he likes from extra.lean, make the necessary name/style adjustments and merge into the standard library. I plan to expand the theory of finfun as I sketched above. If you would like it as is now I suggest we have a fintype subdirectory (finfun for now resides in fintype namespace) and we put the file under fintype/function.lean like you have set/function.lean. That way I can continue to work on the file while minimizing merge conflict.

But can one usefully start with s : finset (A -> B) and ∀ f, f ∈ s and calculate card s?

Yes.

I intended the question to mean "without first developing the theory of fintype (A -> B)". Based on your answer I take it to mean you agree that the way to go is to develop the fintype (A -> B) theory based on list arguments first. There is a possibility of starting just with finset (A -> B) and argue that "two functions agreeing on a particular element" is an equivalence and partition the function space that way but it seems to me inducting on how many points two functions agree upon is likely to be less natural than the corresponding inductions on lists.

[leodemoura]

@avigad was going to pick what he likes from extra.lean, make the necessary name/style adjustments and merge into the standard library.

Great.

I plan to expand the theory of finfun as I sketched above. If you would like it as is now I suggest we have a fintype subdirectory (finfun for now resides in fintype namespace) and we put the file under fintype/function.lean like you have set/function.lean

I added the data/fintype subdirectory: https://github.com/leanprover/lean/tree/master/library/data/fintype

Based on your answer I take it to mean you agree that the way to go is to develop the fintype (A -> B) theory based on list arguments first.

Yes, this is the way I would do it. I think it is natural, and there are many other benefits.

[avigad]

I am sorry I have been so slow to get to this. I will merge in things from extras.lean soon. After that, I think it would be great if Haitao just did pull requests directly and add material once he feels comfortable with it. I'll create a "theories" folder for the group theory stuff, etc.

Haitao, the material doesn't have to be perfect -- the library is still evolving and we are still tinkering with it. But if the material is in the main repository, others can experiment with it, and we can see what effects other changes to the system and library have on those files.

[dselsam]

@avigad

What do you think? I am not sure about any of this, and your thoughts are welcome.

Looking over the "finite sets in Lean" thread on lean-discuss, I see that a lot of thought has gone into this issue already, and I don't think I have much to add at this point. I may not even be a target user, since I am mainly interested in building tools to help verify and partially automate the kind of math people already do in CS/AI, and for now I prefer representations that are as familiar and intuitive as possible even if they might not generalize to more exotic math outside the CS/AI canon. For what it is worth, the finite_set type class seems to me to model standard informal reasoning better than the alternatives, and to present a more familiar interface. This approach also seems to work smoothly in the common case where we can bypass quot and just sort the lists, so that two different inferred lists will always be definitionally equal.

I think the core issue is that an assumption about the underlying type (e.g. decidable_eq or decidable_order) can sometimes enable qualitatively different representations that a user may want to make use of, and not just additional operations on the same representation. It seems possible that over time, the finite set representations might split even further as users try to exploit additional assumptions in various ways. The beauty of informal set theory is that it abstracts away these representation decisions, and the hope is that type class inference could make the right operations available at the right time without the casual user needing to worry about which representations need to be used where.

On the other hand, the current finset library works very well and people seem to like using it. My interests are niche, my concerns are speculative, and my experience and expertise are both limited, so please take what I say with a grain of salt.

[avigad]

Thanks. Automating the kind of math the people do in CS/AI is certainly the kind of thing we'd like to do with Lean, so that is definitely a target. But even in that domain, I think the representation will become unworkable as soon as users try to carry out some simple calculations, for the reasons I described above. I'd be happy to be proved wrong, though. Please do keep us posted as you experiment with the system.

[leodemoura]

I'm closing this issue, but we can continue the discussion. Here is a summary (feel free to add more items).

• Many of us acknowledge that the finite_set type class is nice idea, and it is worth trying.
• We need better automation in Lean to be able to work with this type class in a convenient way. This is not a problem of the proposal, but a current limitation of the system. I believe the simplifier will address these issues. BTW, the new congruence tactic already minimizes the problem.
• There is also an issue regarding evaluation. Some closed terms using the finite_set type class would not evaluate to a value inside of the Lean kernel. See example in the OTT thread #654. I think this is an important issue, and I welcome others to share ideas and concerns in the OTT thread.
• Daniel is correct when he claims that: "It seems possible that over time, the finite set representations might split even further as users try to exploit additional assumptions in various ways." This is a common scenario, and we should provide support for that in Leab. In the past we talked about automatic translation of theorems between different representations; and aggressively using abstract structures. Example: int is a parametric type that can be instantiated with different implementations of nat. Same for rat and real.

[htzh]

As we now have established fintype (A -> B) we can define all sets of fintype A as A -> bool instead. We would immediately have the power sets and even card (A -> bool) = 2 ^ card A for free.

Haitao

On Sat, Jun 13, 2015 at 11:06 AM, Leonardo de Moura < notifications@github.com> wrote:

I'm closing this issue, but we can continue the discussion. Here is a summary (feel free to add more items).

-

Many of us acknowledge that the finite_set type class is nice idea, and it is worth trying.

We need better automation in Lean to be able to work with this type class in a convenient way. This is not a problem of the proposal, but a current limitation of the system. I believe the simplifier will address these issues. BTW, the new congruence tactic already minimizes the problem.

There is also an issue regarding evaluation. Some closed terms using the finite_set type class would not evaluate to a value inside of the Lean kernel. See example in the OTT thread #654 https://github.com/leanprover/lean/issues/654. I think this is an important issue, and I welcome others to share ideas and concerns in the OTT thread.

Daniel is correct when he claims that: "It seems possible that over time, the finite set representations might split even further as users try to exploit additional assumptions in various ways." This is a common scenario, and we should provide support for that in Leab. In the past we talked about automatic translation of theorems between different representations; and aggressively using abstract structures. Example: int is a parametric type that can be instantiated with different implementations of nat. Same for rat and real.

— Reply to this email directly or view it on GitHub https://github.com/leanprover/lean/issues/650#issuecomment-111737252.

[htzh]

I have noticed that with the current finset setup it is not easy to prove that a subtype based on finset membership is a fintype. The difficulty comes from what was discussed in this thread: that only for special case of base type A can we establish an enumerated list of set elements, such as when A is ordered or when A itself is fintype. This reminds me of this discussion about finite_set. What do you think of the following framework of finite_set in parallel with fintype (note complete needs to be iff for set unlike type):

section
open list set

structure finite_set (A : Type) :=
(carrier : set A) (elems : list A) (nodup : nodup elems) (complete : ∀ a, a ∈ carrier ↔ a ∈ elems)

check @finite_set.elems
definition finite_set_to_finset {A : Type} (s : finite_set A) : finset A :=
to_finset_of_nodup (finite_set.elems s) (finite_set.nodup s)

structure is_finite [class] {A : Type} (s : set A) :=
(elems : list A) (nodup : nodup elems) (complete : ∀ a, a ∈ s ↔ a ∈ elems)

definition set_to_finset {A : Type} (s : set A) [fins : is_finite s] :=
to_finset_of_nodup (is_finite.elems s) (is_finite.nodup s)

end

[htzh]

With the is_finite type class we can develop set algebra cleanly: those that don't require finiteness can be used directly instead of having to be lifted. For the finite sets we can now sort of complete the circle: set + is_finite -> finset -> set (note we lose is_finite when converted back).

[htzh]

equiv may be a better name for the complete field.

[leodemoura]

Haitao,

This is an important issue. Could you please include links to the problematic definitions? I mean the ones that are not as clean as you want because of finset.

Thanks, Leo

[avigad]

I agree that this is an important issue.

@htzh, I am not clear about your proposal. Are you suggested changing the definition of finset, or adding a new definition, finite_set? I think it will be confusing to have a third type in addition to set and finset, but I think it is worth considering changing the definition of finset if there is one that works better.

Bundling in a set and an equivalence proof has the advantage I described above that the coercion to set preserves structure, i.e. intersections coerce to intersections, etc. The main disadvantage is that the change would require work. But I think that work will be mostly localized to the finset folder, because outside most theorems use finset through the natural interface.

As to the suggestion for is_finite, I have the same concern expressed above that if this is inferred by expressions and left implicit, it will be bad for calculation. E.g. if the expression card (b ∩ a) has a hidden implicit argument is_finite, we will often have expressions card (b ∩ a) that are provably equal but not definitionally equal. It will be confusing to have calculations that fail because two instances of card (b ∩ a) are not the same. In addition, the workaround -- applying a rewrite that fixes it -- might be tedious.

Maybe there are good ways to deal with this. I am just noting the concern.

[leodemoura]

@avigad We need to address the definitional vs provable equality issue anyway. The card implicit argument is not an isolated issue. Yes, this issue affects the rewrite tactic because it is based on subst (eq.rec_on). However, it will not affect the simplifier. The simplifier will dynamically generate congruence theorems that ignore irrelevant arguments (i.e., type is a subsingleton). This feature is already available in the congruence tactic. I implemented this feature for the simplifier, I added it to the congruence tactic just to be able to test it. For example, congruence will automatically solve the goal card (b ∩ a) = card (b ∩ a) even when the implicit arguments are only provably equal. The simplifier will use the same trick.

For applying theorems that contain nested card terms, one trick is to always abstract the card implicit argument. We have (inconsciently) used this approach in many theorems in the standard library that have this kind of problem.

[htzh]

@leodemoura

Could you please include links to the problematic definitions?

Currently I have defined quotient group through quot, which requires a type. So if I want to define the quotient between two subgroups (represented as sets or finsets) I need to turn the parent group from a set into a subtype. For finite groups (represented as finsets) I would like to prove the subtype as fintype, for which I need a list of the elements. For my purpose I can live with having the base type be a fintype, in which case it is easy to prove that the subtype (through finset membership) is fintype. But this is not as general as it could be since one should be able to do this for finsets in general. I don't have definitions yet. For background see:

https://github.com/htzh/leanproved/blob/dddd41f93099fd7b9f30b344c8717e4f91705694/group_theory/finsubg.lean#L29

for the current finsubg definition.

https://github.com/htzh/leanproved/blob/dddd41f93099fd7b9f30b344c8717e4f91705694/group_theory/subgroup.lean#L359-L398

for the quotient group theory that I would like to do for a fintype that is subtyped on the finsubg.

@avigad

I am not clear about your proposal. Are you suggested changing the definition of finset, or adding a new definition, finite_set?

I am guessing it is in addition. What I am really suggesting is a facility to enumerate the elements of the finset. The easy way to achieve that is to simply carry the information along as in fintype which is the is_finite or finite_set proposal. But if we can achieve it some other way that preserves the current interface I would be happy too.

The litmus test is can we subtype a finset and prove the new type is fintype? There is incompatibility right now with the two definitions.

[htzh]

As to the suggestion for is_finite, I have the same concern expressed above that if this is inferred by expressions and left implicit, it will be bad for calculation.

Maybe this can be experimented on the group theory. There are two aspects: algebraic operations and cardinalities. is_finite may let us decouple the two for set just as fintype let us decouple the two for types. The point is that we shouldn't need to two sets of group theories as the current setup would demand. Group operations should be built on types; and subgroups would be built on sets. If cardinality is required we will need an is_finite instance to translate the set into finset (if needed) for facilities that require cardinality.

[leodemoura]

@htzh Thanks for describing the issue in detail. So, we can solve the problem if we can list the elements of a finset, right? What about a listable type class for finsets?

structure listable (A : Type) :=
(to_list : finset A → list A) (complete : ∀ a s, a ∈ s ↔ a ∈ to_list s)

We can define instances that would cover all basic cases: orderable types, encodable types, etc. Then, you add [lst : listable A] as an extra parameter to any function that needs to list the elements of a finset. For classical users, the extra parameter is not a big deal since they can use hilbert's choice to show that any type is listable.

[leodemoura]

The litmus test is can we subtype a finset and prove the new type is fintype?

The short answer is no. This sounds really bad, but I don't see a good solution for that. Finite sets are tricky to handle constructively. As I described in the previous comments, in the standard definition used for finite sets, we cannot even prove that a subset of a finite set is finite.

I thought about defining fintype using finset instead of lists. But, we would only be moving the problem to a different place. For many applications of fintype, we also want to list the elements.

Another possibility: we represent a finset as a bare list, and use ˜ instead of =, where s1 ~ s2 is defined as ∀ a, a ∈ s1 ↔ a ∈ s2. Then, we would always have access to the list, but we would be forced to use the equivalence relation ˜ instead of =. This is really annoying, and it would look quite bizarre for classical users.

[htzh]

@leodemoura

What about a listable type class for finsets?

Making it a property of the type instead of particular set seems sensible. However my requirement is not going to test the limit of this hypothesis as I could live with fintype for finite groups.

The other thing is to not develop two tracks of group theories (or at least as little redundant work as possible) with one on set one on finset. This was a question deferred from earlier, but now it is popping up again as I need to make quotient group work between two sets.

For now there are two ways to do the coset_type:

• https://github.com/htzh/leanproved/blob/dddd41f93099fd7b9f30b344c8717e4f91705694/group_theory/finsubg.lean#L137-L201 based on finset.
• And the earlier link to quot over setoid: https://github.com/htzh/leanproved/blob/dddd41f93099fd7b9f30b344c8717e4f91705694/group_theory/subgroup.lean#L359-L398

Maybe this kind of replication is unavoidable.

[avigad]

It would be great if we can work around the provable vs. definition equality issue, and calculate with card (b ∩ a) even when there is a "data relevant" implicit argument. That would simplify things a lot.

For example, in that case, I don't see why we need to have separate types for set A and finset A. We only need set A and a type

structure finite [class] {A : Type} (s : set A) :=
(list_rep : list A) (complete : ∀ x, x ∈ s ↔ x ∈ list_rep)

If it is more convenient to assume the list has no duplicates, we can do that. We also don't need special treatment for finite types. The hypothesis that A : Type is a finite type is just H : finite (@univ A).

Right now, the situation is baroque: we have set and finset and fintype and we are talking about adding more gadgets, like listable and finite as a predicate for sets in classical set theory. We have subgroups of groups and subgroups of groups on finite types and finite subgroups of groups on arbitrary types. This is a mess. It would be nice if we could simplify all this.

In ordinary mathematics, there are sets, and some sets are finite. The most natural thing is to say s : set A and H : finite s. Similarly, if G is a group, to say that G is finite we want to say H : finite (carrier G). The only reason we needed finset is that, from a constructive standpoint, we could not put finite s in Prop, because we need to compute with the data. But if it is not a problem to have finite s : Type, I see no good reason for finset.

[avigad]

By the way, the concern about contentful implicit arguments is not limited to calculation. Suppose I am trying to prove card (b ∩ a) > 1 and I have hypothesis H : prime (card (b ∩ a)). I look in the library and find the theorem foo {x : nat} : prime x → x > 1. I apply foo H and it fails. Why? Because the two instances of card (b ∩ a) are not the same.

This will be a very common occurrence. Won't we run into trouble unless every aspect of the system can learn to treat all the "instances" of card (b ∩ a) the same?

[leodemoura]

@avigad A type class such as finite is problematic. Recall the comment I made in the OTT thread https://github.com/leanprover/lean/issues/654#issuecomment-109439028

[leodemoura]

Right now, the situation is fairly baroque: we have set and finset and fintype and we are talking about adding more gadgets, like listable and finite as a predicate for sets in classical set theory. This will make the library look like a mess. It would be nice if we could simplify all this.

I don't think it is a mess. Each type class has a clear purpose. We also don't need both listable and finite. They are part of two different proposals.

[leodemoura]

I apply foo H and it fails. Why? Because the two instances of card (b ∩ a) are not the same.

This will be a very common occurrence. Won't we run into trouble unless every aspect of the system can learn to treat all the "instances" of card (b ∩ a) the same?

Yes, we may need support in some parts of the system. I don't think the problem is that big. We already have definitions such as card in the system. Example: the dependent if-then-else. https://github.com/leanprover/lean/blob/master/library/init/logic.lean#L567 It is the same problem, the argument [H : decidable c] is a subsingleton.

[avigad]

@avigad A type class such as finite is problematic. Recall the comment I made in the OTT thread

654 (comment)

Sigh. I forgot about that.

We also don't need both listable and finite. They are part of two different proposals.

In the classical library, I think we want a predicate finite on sets.

Yes, this issue affects the rewrite tactic because it is based on subst (eq.rec_on). However, it will not affect the simplifier. The simplifier will dynamically generate congruence theorems that ignore irrelevant arguments (i.e., type is a subsingleton). This feature is already available in the congruence tactic. I implemented this feature for the simplifier, I added it to the congruence tactic just to be able to test it. For example, congruence will automatically solve the goal card (b ∩ a) = card (b ∩ a) even when the implicit arguments are only provably equal. The simplifier will use the same trick.

Just to make sure I understand: where you wrote "i.e." did you mean "e.g."? In other words, we'll be able to use general congruence rules, not just for subsingletons?

Anyhow, as I understand it now, the proposal is to use listable to address Haitao's immediate concern, and there is no concrete proposal to change our current treatment of finite sets. I am o.k. with that.

[avigad]

It is the same problem, the argument [H : decidable c] is a subsingleton.

Ah, but Haitao's proposed is_finite, which is what I was initially responding to, is not a subsingleton. Or have I misunderstood?