The Coq mailing list

[Conor McBride <conor AT strictlypositive.org>]

Hi

Just for purposes of comparison, here's a treatment in Agda 2.

On 20 Aug 2008, at 14:17, 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.

First the key data structures, defined inductively:

  data Vec (X : Set) : Nat -> Set where
    [] : Vec X zero
    _::_ : {n : Nat} -> X -> Vec X n -> Vec X (suc n)

  data Fin : Nat -> Set where
    fz : {n : Nat} -> Fin (suc n)
    fs : {n : Nat} -> Fin n -> Fin (suc n)

Then the forgetful map...

  fog : {n : Nat} -> Fin n -> Nat
  fog fz = zero
  fog (fs i) = suc (fog i)

...and the prefix function.

  pref : {X : Set}{n : Nat}(i : Fin (suc n)) -> Vec X n -> Vec X  
(fog i)
  pref fz     xs         = []
  pref (fs ()) []
  pref (fs i) (x :: xs)  = x :: pref i xs

The Agda typechecker is doing all Samuel's equational reasoning
(effectively first-order unification by hand) externally to the
type theory and just accepting that this function is ok. Of course,
it's possible to automate the equational reasoning inside the type
theory: aren't there new dependent induction/inversion tactics
which do that in Coq? Perhaps they might tidy up Samuel's proof.
If anyone can point me to a beta of Coq 8.2 for a G4 mac, I'll
happily try it out.

Once you actually have reasonable dependent inversion technology,
the advantages of recursive vectors over inductive vectors aren't
so strong. With recursive vectors, you pretty much have to keep
the length information in the foreground; the inductive presentation
allows length management to be much quieter (provided, of course,
that the machine is doing it). Also, you sometimes get slightly
more inferred by implicit syntax with the inductive version --- why
should the machine *infer* that some pair (x, xs) happens to be in
particular a nonempty vector?

But there really isn't that much difference. Agda / Epigram
programmers tend to prefer the inductive version, partly from habit,
partly from the joy of seeing the analysis of list and length in
unison, where the recursive version separates them and requires us
to keep them in step. This gets even more fun if you have families
indexed by indexed data...

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

Now that's a very nice way of looking the problem! Channelling
James McKinna, I'd suggest going one step further and writing
vec_split as a view, proving that every vector of length m+n
is the concatenation of an m-vector and an n-vector. In Agda 2,
this goes as follows:

  _++_ : {X : Set}{m n : Nat} -> Vec X m -> Vec X n -> Vec X (m + n)
  []         ++ ys  = ys
  (x :: xs)  ++ ys  = x :: (xs ++ ys)

  data Split {X : Set}(m n : Nat) : Vec X (m + n) -> Set where
    append : (xs : Vec X m)(ys : Vec X n) -> Split m n (xs ++ ys)

  split : {X : Set}(m n : Nat)(xs : Vec X (m + n)) -> Split m n xs
  split zero    n xs                                 = append [] xs
  split (suc m) n (x :: xs)       with split m n xs
  split (suc m) n (x :: .(xs ++ ys)) | append xs ys  = append (x ::  
xs) ys

As you can see in the analysis of the recursive call, you not
only get vectors of the right lengths, you also get the guarantee
that they are the prefix and suffix of the original. The mechanism
is pretty much the same as Venanzio's, but the type tells you more,
if you're interested.

I'm sure the same story can be told with recursive vectors, and here
the length information is in the foreground anyway, so I'd expect
no difference given dependent inversion.

I'm sorry I have such an old computer or I'd have tried it already.

Fun stuff

Conor