Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Prefixes of a vector

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Prefixes of a vector


chronological Thread 
  • From: Adam Chlipala <adamc AT hcoop.net>
  • To: Venanzio Capretta <venanzio AT cs.ru.nl>
  • Cc: coq-club AT pauillac.inria.fr
  • Subject: Re: [Coq-Club] Prefixes of a vector
  • Date: Wed, 20 Aug 2008 09:23:17 -0400
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Venanzio Capretta wrote:
Adam Chlipala wrote:
Programs written like this with proof scripts seem hard to read and maintain. Does anyone have any arguments for writing in this style instead of in the style I used in my solution?
I agree with you: For the prefix function, it seems that your recursive implementation of vectors is much nicer that the inductive one. But is it always preferable.

I don't have a formal argument, but I think it's likely that the recursive version is never any worse than the inductive version, and we have this example where the recursive version seems much easier to work with. You can code the constructors and induction principle of the inductive version from the recursive version using very direct definitions, while going in the opposite direction seems to require some unintuitive acrobatics.

Btw: I have a little module with the equivalence of the two implementations and a third one of vectors as functions on finite types.
See http://www.cs.ru.nl/~venanzio/Coq/Vectors.v.

Using some of the definitions in there, here is another possible way is to answer Samuel's original question:

Fixpoint vec_split (A:Set)(n1 n2:nat){struct n1}:
 vector A (n1+n2) -> (vector A n1 * vector A n2)%type :=
match n1 return vector A (n1+n2) -> (vector A n1 * vector A n2)%type with
 O => fun v => (vec_nil A, v)
| (S n1') => fun v => let (w1,w2):= vec_split A n1' n2 (vec_tail v) in
                       (vec_cons (vec_head v) w1, w2)
end.

This seems like the champion solution so far. :-) It's a good example of how reordering function arguments and their type dependencies can make your life easier.





Archive powered by MhonArc 2.6.16.

Top of Page