2.7 Implicit Coercions
Coercions can be used to implicitly inject terms from one ``class'' in which they reside into another one. A class is either a sort (denoted by the keyword SORTCLASS), a product type (denoted by the keyword FUNCLASS) or an inductive type (denoted by its name).2.7.1 Class ident.
Declares the name ident as a new class.Variant:
-
Class Local ident.
Declares the name ident as a new local class to the current section.
2.7.2 Coercion ident : ident1 >-> ident2.
Declares the name ident as a coercion between ident1 and ident2. The classes ident1 and ident2 are first declared if necessary.Variants:
-
Coercion Local ident : ident1 >-> ident2.
Declares the name ident as a coercion local to the current section.
- Identity Coercion ident:ident1 >-> ident2.
Coerce an inductive type to a subtype of it.
- Identity Coercion Local ident:ident1 >-> ident2.
Idem but locally to the current section.
2.7.3 Displaying available coercions
Print Classes.
Print the list of declared classes in the current context.Print Coercions.
Print the list of declared coercions in the current context.Print Graph.
Print the list of valid path coercions in the current context.2.7.4 Examples
-
Coercion between inductive types
Coq < Definition bool_in_nat := [b:bool]if b then O else (S O).
bool_in_nat is defined
Coq < Coercion bool_in_nat : bool >-> nat.
bool_in_nat is now a coercion
Coq < Check O=true.
O=(true)
: Prop
Warnings:-
Check true=O.fails. This is ``normal'' behaviour of coercions. To validatetrue=O, the coercion is searched fromnattobool. There is not one.
-
- Coercion to a sort
Coq < Variable Graph : Type.
Graph is assumed
Coq < Variable Node : Graph -> Type.
Node is assumed
Coq < Coercion Node : Graph >-> SORTCLASS.
Node is now a coercion
Coq < Variable G : Graph.
G is assumed
Coq < Variable Arrows : G -> G -> Type.
Arrows is assumed
Coq < Check Arrows.
Arrows
: (G)->(G)->Type
Coq < Variable fg : G -> G.
fg is assumed
Coq < Check fg.
fg
: (G)->(G)
- Coercion to a function
Coq < Variable bij : Set -> Set -> Set.
bij is assumed
Coq < Variable ap : (A,B:Set)(bij A B) -> A -> B.
ap is assumed
Coq < Coercion ap : bij >-> FUNCLASS.
ap is now a coercion
Coq < Variable b : (bij nat nat).
b is assumed
Coq < Check (b O).
(ap nat nat b O)
: nat
- Transitivity of coercion
Coq < Variables C : nat -> Set; D : nat -> bool -> Set; E : bool -> Set.
C is assumed
D is assumed
E is assumed
Coq < Variable f : (n:nat)(C n) -> (D (S n) true).
f is assumed
Coq < Coercion f : C >-> D.
f is now a coercion
Coq < Variable g : (n:nat)(b:bool)(D n b) -> (E b).
g is assumed
Coq < Coercion g : D >-> E.
g is now a coercion
Coq < Variable c : (C O).
c is assumed
Coq < Variable T : (E true) -> nat.
T is assumed
Coq < Check (T c).
(T c)
: nat
- Identity coercion
Coq < Definition D' := [b:bool](D (S O) b).
D' is defined
Coq < Identity Coercion IdD'D : D' >-> D.
IdD'D is now a coercion
Coq < Print IdD'D.
IdD'D = [b:bool][x:(D' b)]x
: (b:bool)(D' b)->(D (S O) b)
Coq < Variable d' : (D' true).
d' is assumed
Coq < Check (T d').
(T d')
: nat
See also: the technical chapter 14 on coercions.