Xiaokun Luan (Mar 25 2021 at 12:04): 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.
Kazuhiko Sakaguchi (Mar 25 2021 at 12:08):Did you import choice?
Xiaokun Luan (Mar 25 2021 at 12:11):Yes, I import all_reflect, which includes choice.
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].
It seems to me that there is a bug in the [fmap _ => _] notation or with the coercion from fsets to Sortclass. @Cyril Cohen
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.)
Cyril Cohen (Mar 25 2021 at 12:45):The domain S is supposed to be a fset not a type.
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].
BTW, this is a mathcomp question, so I'm moving this to the mathcomp stream.
Notification Bot (Mar 25 2021 at 12:58):This topic was moved here from #Miscellaneous > Finmap construction by Cyril Cohen
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!
Cyril Cohen (Mar 25 2021 at 14:59):Maybe you are looking for fsfun instead then...
Xiaokun Luan (Mar 25 2021 at 15:06):Ok, thanks for your advice!
Last updated: Feb 08 2023 at 07:02 UTC