Stream: math-comp users

Topic: Missing coercion from {fset C} to finType


view this post on Zulip Ricardo (Nov 15 2022 at 22:41):

Why is there no coercion from {fset C} (given C : choiceType) to finType in mathcomp.finmap?

view this post on Zulip Ricardo (Nov 16 2022 at 00:18):

Wait. I'm not sure there's no coercion. In the following code it coerces in one situation and not in the other.

From mathcomp Require Import ssreflect ssrbool ssrnat ssrfun eqtype choice fintype seq finfun finmap.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Module X.
Definition symb (T : finType) (R : rel T) :=
  [forall x, forall y, R x y == R y x].
Definition rel0 (T : Type) (_ _ : T) := false.
Variable (C : choiceType) (f : {fset C}).
Set Printing Coercions. Set Printing Implicit.
Check symb (@rel0 f). (* here the coercion works *)
Definition g (T : finType) := tt.
Check g f. (* here it doesn't *)
Check g (@fset_sub_finType C f). (* here no problem again *)

view this post on Zulip Paolo Giarrusso (Nov 16 2022 at 00:21):

The working case is coercing to Type not finType?

view this post on Zulip Ricardo (Nov 16 2022 at 00:22):

The output of Check symb (@rel0 f) is

@symb (@fset_sub_finType C f)
  (@rel0 (@fset_sub_type C f))
     : bool

view this post on Zulip Paolo Giarrusso (Nov 16 2022 at 00:22):

rel0 takes a Type, so the coercion is inserted. The only finType is symb's argument, which is not generated by a coercion but by canonical structure inference.

view this post on Zulip Paolo Giarrusso (Nov 16 2022 at 00:24):

does that help / make sense?

view this post on Zulip Paolo Giarrusso (Nov 16 2022 at 00:26):

double-checked and https://github.com/math-comp/finmap/blob/master/finmap.v shows indeed

Canonical fset_sub_finType := Eval hnf in FinType fset_sub_type fset_sub_finMixin.
...
Coercion fset_sub_type : finSet >-> predArgType.

view this post on Zulip Paolo Giarrusso (Nov 16 2022 at 00:27):

I guess you'd try g [finType of f], as needed when you need Coq to infer extra structure?

view this post on Zulip Ricardo (Nov 16 2022 at 00:58):

Shouldn't that coercion in the second line help with g f?

view this post on Zulip Ricardo (Nov 16 2022 at 00:58):

Or would it have to be Coercion fset_sub_type : finSet >-> finType for it to work as I expect?

view this post on Zulip Ricardo (Nov 16 2022 at 01:07):

I was mixing up fset_sub_type with fset_sub_finType. The former is a coercion in mathcomp.finmap but not the latter. If I make fset_sub_finType a coercion then g f works as expected.

Coercion fset_sub_finType : finSet >-> finType.
Check g f. (* no problem *)

Are there good reasons why fset_sub_finType isn't made a coercion in mathcomp.finmap?

view this post on Zulip Paolo Giarrusso (Nov 16 2022 at 01:11):

I'll leave this to the actual math-comp experts :-)

view this post on Zulip Cyril Cohen (Nov 16 2022 at 08:20):

Ricardo said:

I was mixing up fset_sub_type with fset_sub_finType. The former is a coercion in mathcomp.finmap but not the latter. If I make fset_sub_finType a coercion then g f works as expected.

Coercion fset_sub_finType : finSet >-> finType.
Check g f. (* no problem *)

Are there good reasons why fset_sub_finType isn't made a coercion in mathcomp.finmap?

That would make sense indeed.

view this post on Zulip Ricardo (Nov 17 2022 at 23:09):

@Cyril Cohen, I see on the github page of mathcomp.finmap that you're one of the contributors. Would you like to add this coercion to a possible next release?

view this post on Zulip Cyril Cohen (Nov 18 2022 at 08:52):

Yes, let's do this. Could you open an issue or submit a PR?

view this post on Zulip Ricardo (Nov 18 2022 at 18:48):

I can open an issue. Here it is https://github.com/math-comp/finmap/issues/102


Last updated: Mar 28 2024 at 23:01 UTC