coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: AUGER Cedric <Cedric.Auger AT lri.fr>
- To: "Ly Kim Quyen (Gwenhael)" <lykimq AT gmail.com>
- Cc: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Asking about dependence type
- Date: Mon, 27 Jun 2011 12:46:52 +0200
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").
- [Coq-Club] Asking about dependence type, Ly Kim Quyen (Gwenhael)
- Re: [Coq-Club] Asking about dependence type, gallais @ ensl.org
- Re: [Coq-Club] Asking about dependence type, AUGER Cedric
- Re: [Coq-Club] Asking about dependence type, Ly Kim Quyen (Gwenhael)
Archive powered by MhonArc 2.6.16.