The Coq mailing list

[Line Jakubiec-Jamet <jakubiec AT lif.univ-mrs.fr>]

  Hello,

I have two questions about coercions in Coq.

* My first problem is illustrated by the following declarations:

Parameters (A B C :Prop).
Parameter Z:{A}+{B}->{A}+{C}.
Coercion  Z:{A}+{B}>->{A}+{C}. (*Syntax error: *)


But we can write:

Parameters (A B C :Prop).
Definition X:={A}+{B}.
Definition Y:={A}+{C}.
Parameter Z:X->Y.
Coercion  Z:X>->Y. (* Ok*)

I don't understand why it is different?


* Secondly, suppose we have :

Parameters (A B C :Prop).
Definition X:={A}+{B}.
Definition Y:={A}+{C}.
Parameter Z:X->Y.
Coercion  Z:X>->Y.

Parameter F:Y->Prop.
Definition f := exists v:B, F (Z (right A v)).

Why we have to use Z in the definition f to make the conversion between
an object of type X to an object of type Y ?
(it should be introduced by the coercion Z?).


Thanks for your help,


  Line

--
(**********************************************************)
(* Line Jakubiec-Jamet                                    *)
(* Laboratoire d'Informatique Fondamentale de Marseille   *)
(* Université de la Méditerranée (Aix-Marseille II)       *)
(* Faculté des Sciences de Luminy                         *)
(* 163, Avenue de Luminy                                  *)
(* 13288 - MARSEILLE Cedex 9                              *)
(**********************************************************)