coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Venanzio Capretta <Venanzio.Capretta AT mathstat.uottawa.ca>
- To: Conor McBride <conor AT cs.rhul.ac.uk>
- Cc: Nicolas Magaud <nmagaud AT cse.unsw.edu.au>, casteran AT labri.fr, june andronick <jandronick AT axalto.com>, coq-club AT pauillac.inria.fr
- Subject: Re: [Coq-Club] problem with dependant types
- Date: Thu, 18 Nov 2004 10:48:07 -0500
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
Hi Conor,
Of course my challenge was to do it in Coq (with no axioms). Epigram seems to be better at dealing with dependent induction. Specifically, it is nice how it can automatically deduce thatI challenge you to do the same using the inductive Vector (or listn) definition!
See attached Epigram file, which I offer as evidence of what's possible
with a bit more automation.
if v:Vec (suc n) X, then when I do pattern matching on it I have to consider only the vcons case.
In Coq we have to consider the vnil case also, introduce an extra equality in the domain predicate etc... How does Epigram do it? Is its type theory different and nicer, or is there an automathic translation that does the dirty work for you?
Nice idea of making a vector of copies of the function, anyway: it should make things easier in Coq too.
By the way, you didn't beat the challenge yet! To do so you have to define a function like my tuple_n_map, that is:
given f: A -> ... -> A -> B (k copies of A),
a0, ..., ak: Vector A n
compute <f (a{0,0},...,a{0,k-1}), ...., f (a{n-1,0},...,a{n-1,k-1})> : Vector B n
But probably it's not too hard in Epigram.
Or go even further: define finite
sets (either inductively, or by iterated coproducts) and represent vectors
functionally: this makes all sorts of operations even easier (eg transpose),
at the cost of making vector equality extensional.
I actually used this definition in past formalizations and it seems to be the easiest to use. The fact that equality is extensional didn't seem to be a problem.
What's so bad about K anyway?I don't have anything in particular agains K, but in general I don't like axioms. When you are forced to use an axiom it means that your type theory is not doing the job. One should rather rething the system so that the desired properties are "structural" rather that axiomatic.
Dependent pattern matching is currently difficult in Coq, but it doesn't
have to be that way. The question is what to do about it.
On conna\^it la chanson...
In the case under study, Pierre Casteran showed how to do things without assuming axioms, if you can do without them you should.
A part from this philosophical point, I have no objection: go ahead and use K!
Venanzio
- [Coq-Club] problem with dependant types, june andronick
- Re: [Coq-Club] problem with dependant types,
casteran
- Re: [Coq-Club] problem with dependant types,
casteran
- Re: [Coq-Club] problem with dependant types,
Nicolas Magaud
- Re: [Coq-Club] problem with dependant types,
Venanzio Capretta
- Re: [Coq-Club] problem with dependant types,
Conor McBride
- Re: [Coq-Club] problem with dependant types, Venanzio Capretta
- Re: [Coq-Club] problem with dependant types, Cuihtlauac ALVARADO
- Re: [Coq-Club] problem with dependant types, Conor McBride
- Re: [Coq-Club] problem with dependant types, Venanzio Capretta
- Re: [Coq-Club] problem with dependant types, Venanzio Capretta
- Re: [Coq-Club] problem with dependant types, James McKinna
- Re: [Coq-Club] problem with dependant types,
Conor McBride
- Re: [Coq-Club] problem with dependant types,
Venanzio Capretta
- Re: [Coq-Club] problem with dependant types,
Nicolas Magaud
- Re: [Coq-Club] problem with dependant types,
casteran
- Re: [Coq-Club] problem with dependant types,
casteran
- Re: [Coq-Club] problem with dependant types, Boris Yakobowski
- Re: [Coq-Club] problem with dependant types, casteran
- <Possible follow-ups>
- Re: [Coq-Club] problem with dependant types, june andronick
Archive powered by MhonArc 2.6.16.