{"action":"created","issue":{"url":"https://api.github.com/repos/leanprover/lean/issues/650","labels_url":"https://api.github.com/repos/leanprover/lean/issues/650/labels{/name}","comments_url":"https://api.github.com/repos/leanprover/lean/issues/650/comments","events_url":"https://api.github.com/repos/leanprover/lean/issues/650/events","html_url":"https://github.com/leanprover/lean/issues/650","id":84221577,"number":650,"title":"Relationship between set and finset","user":{"login":"dselsam","id":4520285,"avatar_url":"https://avatars.githubusercontent.com/u/4520285?v=3","gravatar_id":"","url":"https://api.github.com/users/dselsam","html_url":"https://github.com/dselsam","followers_url":"https://api.github.com/users/dselsam/followers","following_url":"https://api.github.com/users/dselsam/following{/other_user}","gists_url":"https://api.github.com/users/dselsam/gists{/gist_id}","starred_url":"https://api.github.com/users/dselsam/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/dselsam/subscriptions","organizations_url":"https://api.github.com/users/dselsam/orgs","repos_url":"https://api.github.com/users/dselsam/repos","events_url":"https://api.github.com/users/dselsam/events{/privacy}","received_events_url":"https://api.github.com/users/dselsam/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"milestone":null,"comments":2,"created_at":"2015-06-02T21:36:15Z","updated_at":"2015-06-03T01:34:55Z","closed_at":null,"body":"Hi,\r\n\r\nI 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.\r\n\r\nCould 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.\r\n\r\n    inductive finite_set [class] (xs : set T) := \r\n    | mk : ∀ (fxs : finset T), to_set fxs = xs → finite_set xs\r\n\r\nWe could then use the lemmas in the `finset` library to propagate the `finite_set` property, with instances such as:\r\n\r\n    definition finite_set_empty [instance] : finite_set ∅\r\n    definition finite_set_finset [instance] (fxs : finset T) : finite_set (to_set fxs)\r\n    definition finite_set_insert [instance] (xs : set T) [fxs : finite_set xs] (x : T) : finite_set (insert x xs)\r\n    definition finite_set_union [instance] (xs : set T) [fxs : finite_set xs] (ys : set T) [fys : finite_set ys] : finite_set (xs ∪ ys)\r\n    definition finite_set_inter1 [instance] (xs : set T) [fxs : finite_set xs] (ys : set T) [ys_dec : decidable_pred ys] : finite_set (xs ∩ ys)\r\n    definition finite_set_inter2 [instance] (xs : set T) [fxs : finite_set xs] (ys : set T) [ys_dec : decidable_pred ys] : finite_set (ys ∩ xs)\r\n    definition finite_set_set_of [instance] (xs : set T) [fxs : finite_set xs] : finite_set (set.set_of xs)\r\n\r\n    definition finite_set_bounded_nats [instance] (ub : nat) : finite_set (λ n:ℕ, n < ub)\r\n\r\nWe could then define versions of all functions that only make sense on finite sets in terms of the type class, e.g.:\r\n\r\n    definition card (xs : set T) [fxs : finite_set xs] := finset.card (get_finset fxs)\r\n\r\nThe 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:\r\n\r\n    eval card { n : ℕ | n < 10 ∧ odd n }\r\n\r\nIf this approach seems appealing, I would be happy to write a draft of it.\r\n\r\nThanks,\r\n\r\nDaniel\r\n"},"comment":{"url":"https://api.github.com/repos/leanprover/lean/issues/comments/108152769","html_url":"https://github.com/leanprover/lean/issues/650#issuecomment-108152769","issue_url":"https://api.github.com/repos/leanprover/lean/issues/650","id":108152769,"user":{"login":"htzh","id":5956967,"avatar_url":"https://avatars.githubusercontent.com/u/5956967?v=3","gravatar_id":"","url":"https://api.github.com/users/htzh","html_url":"https://github.com/htzh","followers_url":"https://api.github.com/users/htzh/followers","following_url":"https://api.github.com/users/htzh/following{/other_user}","gists_url":"https://api.github.com/users/htzh/gists{/gist_id}","starred_url":"https://api.github.com/users/htzh/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/htzh/subscriptions","organizations_url":"https://api.github.com/users/htzh/orgs","repos_url":"https://api.github.com/users/htzh/repos","events_url":"https://api.github.com/users/htzh/events{/privacy}","received_events_url":"https://api.github.com/users/htzh/received_events","type":"User","site_admin":false},"created_at":"2015-06-03T01:34:55Z","updated_at":"2015-06-03T01:34:55Z","body":"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.\r\n"}}