The Coq mailing list

["Ly Kim Quyen (Gwenhael)" <lykimq AT gmail.com>]

Hello Cedric,

I have tried to define the definition poly_cast from your hint.

Definition poly_cast n m (Heq: n = m)(p: poly n) : poly m.

    rewrite <- Heq; hyp. Defined.

and also 

Definition poly_cast' {n m} {Heq: n = m} {p : poly m} := 
    match Heq in _ = n0 return poly n0 -> Prop with
      | h => fun p0 => p = p0

    end p.

From definitions above when I apply it to the function poly_symbol I get the same error at poly_cast h: 

f: symbol
p : (fun g : symbol => poly (arity g)) g
h : f = g
The term "h" has type "f = g" while it is expected to have type  "?1733 = ?1734"

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.

In my definition of poly_symbol it return the type poly (arity f), and the function poly_cast waiting the condition (h : f = g) p and return a type poly (arity f). 

If I am using the function poly_cast' which type: forall n m : nat, n = m -> poly m -> Prop how can I change the definition of poly_symbol at left h? because it will return Prop but I want it return poly (arity g) for f = g.

Thank you,
Gwen

On 27 June 2011 18:46, AUGER Cedric <Cedric.Auger AT lri.fr> wrote:

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").