The Coq mailing list

["gallais @ ensl.org" <guillaume.allais AT ens-lyon.org>]

Hi Gwen,

I think that you are looking for:

f_equal
     : forall (A B : Type) (f : A -> B) (x y : A), x = y -> f x = f y

You can have a look at its code (which is quite similar to what you wanted
to do) by typing [Print f_equal.]

cheers,

--
guillaume



On 27 June 2011 10:52, Ly Kim Quyen (Gwenhael) 
<lykimq AT gmail.com>
 wrote:
> Hello,
>
> I have a question about an dependent type.
>
> I have a function poly_symbol is:
>
> Fixpoint poly_symbol ( l : list {g: symbol & poly (arity g)}) : poly (arity
> f) :=
>    match l with
>    | existT g p :: l' =>
>                  match eq_symb_dec f g with
>                      | left h => poly_cast h p
>                      | right _ => poly_symbol l'
>                   end
>    | nil => default_poly (arity f)
>   end.
>
> where eq_symb_dec:  forall f g : symbol, {f = g} + {f <> g}
> arity : symbol -> nat.
> poly: nat -> Set.
>
> I want to define the function poly_cast which a specification is:
>
> poly_cast: forall n m : nat, if n = m then poly n = poly m.
>
> Here is my definition :
>
> Definition poly_cast {n : nat} {m : nat} (x : n = m) :=
>      match x with
>         | h => poly n = poly m
>      end.
>
> I know it is not good function of what I want because when I apply it to the
> function poly_symbol it gives me an error at : poly_cast h
>
> The term "h" has type "f = g" while it is expected to have type  "?3478 =
> ?3479".
>
> Could you please give me some suggestion how to build the function
> poly_cast?
> I would like to learn more about how to build a function and dependence type
> function.
>
> Thank you very much,
>
> Gwen
>