Stream: math-comp users

Topic: countType in finmap

view this post on Zulip Evgeniy Moiseenko (Nov 12 2021 at 09:55):

Is there any reason why {fset K}, {fmap K -> V}, and {fsfun K -> V for dflt} from finmap library have instances of choiceType, but no countType? Or is it just by accident (or wasn't needed before)?

view this post on Zulip Pierre-Yves Strub (Nov 12 2021 at 10:42):

countType would be more restrictive, no?

view this post on Zulip Evgeniy Moiseenko (Nov 12 2021 at 11:21):

I mean, if we have that K : countType then we can derive {fset K} : countType.

I actually implemented the required instances in my project, e.g for fset:

Section FSetCount.
Variable (K : countType).
Definition fset_countMixin := Eval hnf in [countMixin of {fset K} by <:].
Canonical fset_countType := Eval hnf in CountType {fset K} fset_countMixin.
End FSetCount.

Just what to know if those instances were missing for some reason.
Perhaps, there are some hidden undesirable consequences which I just don't see?

view this post on Zulip Ana de Almeida Borges (Nov 12 2021 at 11:36):

{fset K} has an instance of finType, right? That implies it's a countType as well. Coq doesn't complain about this:

Variable K : choiceType.
Variable s : {fset K}.
Check [countType of s].

view this post on Zulip Karl Palmskog (Nov 12 2021 at 11:40):

from what I can recall, one can get a countType from a choiceType nearly automatically at any point, and I don't think any finType is involved

view this post on Zulip Ana de Almeida Borges (Nov 12 2021 at 11:46):

But... isn't it possible to have a choiceType that is not countable?

view this post on Zulip Evgeniy Moiseenko (Nov 12 2021 at 12:01):

Ana de Almeida Borges said:

{fset K} has an instance of finType, right? That implies it's a countType as well. Coq doesn't complain about this:

Variable K : choiceType.
Variable s : {fset K}.
Check [countType of s].

Is {fset K} has an instance of finType though?
One can have an infinite amount of finite sets over some infinite type K.

Still your code snippet confuses me, I can't understand where from countType instance comes.

view this post on Zulip Evgeniy Moiseenko (Nov 12 2021 at 12:04):

Ahh, I think in your example [countType of s] actually derives countType for the type of keys of s, which is finite indeed.

Variable K : choiceType.
Variable s : {fset K}.

Let T := [countType of s].

Lemma test : Countable.sort T = (s : Type).
Proof. done. Qed.

view this post on Zulip Ana de Almeida Borges (Nov 12 2021 at 12:06):

Ok, maybe we are talking about different things and I just didn't read your original post with enough attention. You are asking about the statement {fset K} : countType and not the statement s : countType, is that it?

view this post on Zulip Evgeniy Moiseenko (Nov 12 2021 at 12:07):

Yes, I need countType instance for the type of finite sets themselves, not for the type of keys of some particular finite set.

view this post on Zulip Ana de Almeida Borges (Nov 12 2021 at 12:09):

Ok, sorry for the detour then. In that case I don't know, perhaps it was indeed never needed.

view this post on Zulip Evgeniy Moiseenko (Nov 13 2021 at 21:13):

I made a PR for this issue https://github.com/math-comp/finmap/pull/87
Everyone interested is welcome to continue the discussion there.

Last updated: Nov 29 2023 at 05:01 UTC