finset of divisors of pnat

Stream: general

[Johan Commelin]

I've got a n : pnat and I want the finset pnat consisting of the divisors of n. I've already made an instance has_dvd pnat (woot!). What is now the cleanest way to get this finset?
Of course... ... { d | d \| n } will not work... ... ... :expressionless:

[Johan Commelin]

And finset.range lives in finset nat.

[Chris Hughes]

(range (n : nat).succ).filter (\| n) gives the correct finset in nat.

[Chris Hughes]

I guess you want a version of range for pnat?

[Chris Hughes]

I used this finset in data.nat.totient

[Johan Commelin]

Did you give it a name?

[Johan Commelin]

I really don't like the idea of duplicating all the range and Ico, etc... definitions and all their lemmas for nat and pnat and int... etc...

[Johan Commelin]

I think I might do

def pnat.divisors (n : ℕ+) : set ℕ+ :=
{d | d ∣ n}

and then provide a fintype instance

[Chris Hughes]

It depends what you want to do with it, but you almost certainly want a finset.

[Scott Morrison]

Perhaps a good project would be to make list.range, list.Ico, and finset.Ico type polymorphic.

[Scott Morrison]

I'm not sure we yet have an appropriate typeclass describing the behaviour of succ that makes this possible in nat, pnat, int, and friends.

[Chris Hughes]

I guess it's just an ordered type where intervals are always finite. The order on finset has this property as well.

[Scott Morrison]

Well, you need some mechanism to actually list the elements in order, don't you? Merely asserting there's an order, and intervals are finite, doesn't let you make a list. I was imagining some sort of has_succ typeclass.

[Mario Carneiro]

It does let you make a finset though

[Johan Commelin]

There was some talk about enumerable on this chat, some time ago.