Ssreflect Users Discussion List

[Georges Gonthier <>]

   Hi Tim,

  First, there are a few things that are a bit off in your query; I'll try to 
correct a few, but please ask again if I've misinterpreted something.
To be able to "coerce" type A to type B, you need to supply a function AtoB 
from A to B, and then declare it to the type inference engine with the line
Coercion AtoB : A >-> B.

The A and the B here should be type constructors -- parameters are omitted in 
the Coercion declaration. Type reconstruction uses coercions to fix what 
would otherwise by type errors - specifically, if it encounters an expression 
whose inferred type is A (or A a1 a2 a3...) in a context where type B is 
expected, and these are incompatible (even with conversion, canonical 
structures, etc), then it will attempt to fix the typing by inserting a call 
to AtoB. Because type checking proceeds eagerly, this is only attempted once; 
type reconstruction does not backtrack to try to change expressions it has 
already typechecked, in order to make things go better elsewhere.

Note that A and B must be real type constructors, not structures that coerce 
to Type. You can't go wrong if you write the Coercion declaration separately, 
but you should beware if you use the convenient shorthand to define a 
function and declare it simultaneously as a coercion. For instance, if you 
wrote
   Coercion AtoB : A -> B := ....
in your context where A B : eqType, you would be in fact trying to declare
  Coercion AtoB : Equality.sort >-> Equality.sort
and since this is circular it would be ignored by Coq.

As a rule, you should only use structures to declare interfaces, and never 
(or as little as possible) in the application part of your development. This 
is actually why the structure constructors have such awkward names -- it's a 
precaution against their accidental misuse.
  For example, in you code below, the declaration for f should read
Variable f : {ffun D -> A * B}.
The prod_eqType structure will be generated automatically when it's needed.
Similarly, subD should be defined as a Type, e.g.,
Definition subD := {z : D | p z}.
Indeed, if you do this subD will automatically get the eqType, subtype, 
choiceType, countType and finType structures that are defined for "sig" (the 
type constructor hiding behind the {  | } notation). Coq will however need to 
expand you nice abbreviation in order to figure them out. If you want to 
avoid this, you can use the "cloning" forms to grab your own copy of those 
structures, as in
Canonical subD_eqType := [eqType of subD].
Canonical subD_choiceType :=[choiceType of subD].
....
Now that subD is a proper type, you can declare a coercion from it -- but not 
to D, because that's not a proper type. If you tried to define
Coercion subDtoD (u : subD) : D := sval u.
you would in effect be declaring a coercion subD >-> Finite.sort.
This would appear to work locally in your test file, but it would actually 
corrupt the Coercion graph of every file that would import your code, because 
it would now tell Coq that it should not expand Finite.sort when looking for 
the "head constructor" of a type. This would for example break the ordinal 
>-> nat coercion when the finType structure of ordinals is used. 

    If D were a proper type (say, some type of container) then you could 
indeed declare a subD >-> D coercion. However, you should make sure the type 
annotations that are intended to trigger the coercion insertion are close 
enough.
Declaring
   Let f : {ffun 'I_n -> nat} := [ffun i -> i]
won't work, because Coq has already decided that you wrote an identity 
function by the time it takes the constraint into account.
You need to write
  Let f := [ffun i : 'I_n -> i : nat].
to keep the system happy.

     I hope this helps a bit...
Georges


-----Original Message-----
From: T.G. Griffin [] On Behalf Of Timothy G. 
Griffin
Sent: 22 May 2012 11:30
To: 
Subject: [ssreflect] a question about coercion

Consider the following context: 

Require Import ssreflect ssrbool eqtype seq fintype finfun. 
Variable A : eqType. 
Variable B : eqType. 
Variable  D : finType. 
Variable  f : {ffun D -> prod_eqType A B}. 
Variable p : pred D. 
(* subD is perhaps a clumsy encoding of "{z in Z | p z = true}" *) Definition 
subD : finType := seq_sub_finType (filter p (enum D)). 

Now suppose I want to define a function "g (z : subD) = (f z).1". 
Doing the "obvious" thing does not work: 

Definition g : {ffun subD -> A} := [ffun z => (f z).1]. 

This does not type check: 
    Error: The term "[ffun z => (f z).1]" has type "{ffun D -> A}"
    while it is expected to have type "{ffun subD -> A}".

My question : what is the trick to get this kind of coercion to work? 

thanks,
tim
http://www.cl.cam.ac.uk/~tgg22/