The Coq mailing list

[Martijn Vermaat <martijn AT vermaat.name>]

Hi Adam,

>         But unfortunately, we cannot deconstruct the proof of n <= m
>         since it
>         lives in Prop.
>   Why would you want to de-construct such a proof?

You're right, indeed, I don't. (See for example other Adam's answer.)

> You may want to take a look at the CoLoR library [1], which has a rich
> set of functions/results on vectors [2].

Actually, CoLoR is quite related to our project, which aims at a
formalisation of infinitary rewriting.

The main difference (as far as vector representations are concerned) is
that our term type is coinductive, which quickly leads to problems with
the guardednes restriction if we used a standard inductive vector type.

Instead, Adam Chlipala suggested the recursive type, which seems to work
quite nice so fare. Of course, we miss out on a lot of re-use
opportunities from CoLoR.

See also our original question:
  http://logical.saclay.inria.fr/coq-puma/messages/9978d9af68461f02

cheers,
Martijn