Stream: math-comp users

Topic: Finmap construction


view this post on Zulip Xiaokun Luan (Mar 25 2021 at 12:04):

Hi everyone. I want to use finmap in a project, but I am having trouble using it.
The doc on Github says that a finmap can be constructed by using [fmap x : S => E]. But this doesn't work for me.
For example, when I use the command Check [fmap x : bool => ~~ x]%fmap. to check the type of this term, I got the following error:

Error: The term "[ffun x => ~~ x]" has type "{ffun bool_finType -> bool"}, while it is expected to have type "{ffun ?domf -> ?V".

I have checked that the library version (1.5.0) and Coq version (8.12.0) are both ok, I don't know why Coq cannot unify these two types. Can someone help me? Any suggestions would be appreciated.

view this post on Zulip Kazuhiko Sakaguchi (Mar 25 2021 at 12:08):

Did you import choice?

view this post on Zulip Xiaokun Luan (Mar 25 2021 at 12:11):

Yes, I import all_reflect, which includes choice.

view this post on Zulip Xiaokun Luan (Mar 25 2021 at 12:12):

Here is a minimal example.

From mathcomp Require Import finmap.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.


Check [fmap x : bool => ~~ x].

view this post on Zulip Kazuhiko Sakaguchi (Mar 25 2021 at 12:34):

It seems to me that there is a bug in the [fmap _ => _] notation or with the coercion from fsets to Sortclass. @Cyril Cohen

view this post on Zulip Kazuhiko Sakaguchi (Mar 25 2021 at 12:39):

(If I understand correctly, the problem is that the domain of a fmap is a fset rather than a Type, and there should be a coercion from fset to Type, but somehow this does not work. But I'm not familiar with this part of the library and might be wrong.)

view this post on Zulip Cyril Cohen (Mar 25 2021 at 12:45):

The domain S is supposed to be a fset not a type.

view this post on Zulip Cyril Cohen (Mar 25 2021 at 12:57):

I'm wondering why you are using a fmap here, since the domain is a fintype, a finfun is better...

Check [ffun x => ~~ x].

If you are insisting on using (mathcomp) finmap, then you would have to write

Check [fmap x : [fset b : bool | true] => ~~ val x].

view this post on Zulip Cyril Cohen (Mar 25 2021 at 12:57):

BTW, this is a mathcomp question, so I'm moving this to the mathcomp stream.

view this post on Zulip Notification Bot (Mar 25 2021 at 12:58):

This topic was moved here from #Miscellaneous > Finmap construction by Cyril Cohen

view this post on Zulip Xiaokun Luan (Mar 25 2021 at 14:58):

Well, this simple example here is a simplified version of the problem I actually have. What I actually want to do is to initialize a fmap {fmap K -> V} using a function of type K -> V, and this fmap may be changed afterward.
Anyway, thanks a lot for your help!

view this post on Zulip Cyril Cohen (Mar 25 2021 at 14:59):

Maybe you are looking for fsfun instead then...

view this post on Zulip Xiaokun Luan (Mar 25 2021 at 15:06):

Ok, thanks for your advice!


Last updated: Feb 08 2023 at 07:02 UTC