The Coq mailing list

[AUGER Cedric <Cedric.Auger AT lri.fr>]

Le Mon, 27 Jun 2011 16:52:55 +0800,
"Ly Kim Quyen (Gwenhael)" 
<lykimq AT gmail.com>
 a écrit :

> 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

I guess that what you want is rather a function poly_cast of type:
∀ n, poly n → ∀ m, n = m → poly m.

for which you can prove that:
∀ n m, n = m → ∀ p, JMeq.jmeq p (poly_cast p).
(or if you prefer:
∀ n m (H: n = m) (p: poly m),
 match H in _=n0 return poly n0 → Prop with
 | h => fun p0 => p = p0
 end p)

Given this hint, I hope you can find one.

Don't forget, that you can create your functions using tactics, end
them with Defined, and eventually print them to understand how Coq
builds them.

When I want to experiment these features, I often do a:

Goal forall p, p = [my_tactically_built_function].
 unfold [my_tactically_built_function].
 …

… being often a sequence of "unfold [coq_term]", "simpl",
"cbv delta/iota/zeta/beta [args]" and so on.

For instance, with poly_cast using my specification, you can do:

Definition poly_cast n (p: poly n) m (Heq:n=m): poly m.
 rewrite <- Heq.
 assumption.
Defined.

I let you explore what it does (I really don't like the use of eq_ind
in generated proof terms, but I found that the vo file is shorter for
a definition using eq_ind than for a definition using "match with").