Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] problem with dependant types

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] problem with dependant types


chronological Thread 
  • 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,

I 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.

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 that
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?

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

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





Archive powered by MhonArc 2.6.16.

Top of Page