Zulip Chat Archive

Stream: Is there code for X?

Topic: Lean, show me the first 5 elements in the set of natural num


view this post on Zulip Bassem Safieldeen (Jul 04 2020 at 19:18):

When I think about the set of natural numbers its icon in my mind's file system looks something like this: {1, 2, 3, 4, 5, ...}.
When I think about the set of integers its icon looks something like this: {..., -3, -2 -1, 0, 1, 2, 3, ...}.

Is there an easy way to ask Lean to do the same -- to generate a few "nice" elements of a set and show them to me so that I can picture the set better? I would like to apply this to see what the elements of the 2ℤ ideal that I have defined look like.

view this post on Zulip Johan Commelin (Jul 04 2020 at 19:20):

At the moment there is not really a machine for doing that.

view this post on Zulip Johan Commelin (Jul 04 2020 at 19:20):

I've been thinking a while ago that it would be nice to have "examples" of terms in given types. And tactics could try to combine those.

view this post on Zulip Johan Commelin (Jul 04 2020 at 19:21):

But we don't have any framework for this atm.
(Note that example is not the kind of thing I was thinking of.)

view this post on Zulip Chris Hughes (Jul 04 2020 at 19:21):

Potentially if you provided a decidable instance for being in the ideal, then there is a proof that the integers are enumerable and that subsets of enumerable types are enumerable so you could use that to show you some elements.

view this post on Zulip Bassem Safieldeen (Jul 04 2020 at 19:25):

Chris Hughes said:

Potentially if you provided a decidable instance for being in the ideal, then there is a proof that the integers are enumerable and that subsets of enumerable types are enumerable so you could use that to show you some elements.

Sorry, I don't understand "a decidable instance for being in the ideal".

view this post on Zulip Johan Commelin (Jul 04 2020 at 19:26):

It means that you need to write an algorithm that decides whether a given integer is element of the ideal.

view this post on Zulip Mario Carneiro (Jul 04 2020 at 20:01):

This sounds kind of like quickcheck, which uses typeclasses for generating representative elements of a variety of types

view this post on Zulip Simon Hudon (Jul 04 2020 at 20:11):

It's in the pipes

view this post on Zulip Simon Hudon (Jul 04 2020 at 20:11):

I just need write tutorials and documentation for it to be merged


Last updated: May 07 2021 at 19:12 UTC