The Coq mailing list

[Yves Bertot <Yves.Bertot AT sophia.inria.fr>]

Adam Koprowski wrote:
> > In the definitions of functions on vectors such as take, drop, and nth,
> > we would use proofs of 'le' ord 'lt', e.g.:
> >
> >  Definition vtake (n m : nat) : n <= m -> vector m -> vector n.
> >
> > 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 may want to take a
> look at the CoLoR library [1], which has a rich set of functions/results on
> vectors [2].
>
>    Best,
>    Adam
>
> [1] http://color.inria.fr/
> [2] http://color.inria.fr/doc/CoLoR.Util.Vector.VecUtil.html
>
>   
Pattern-matching on proofs while constructing data is not allowed for 
good reasons (or at least for reasons you can understand and get 
accustomed to).  Very often, you think you need it to justify that some 
case is irrelevant, but you can do this because the statement "there is 
a contradiction" (namely False) is in sort Prop.  To see a commented 
example, look at section 15.4 of the Coq'Art, where pattern-matching on 
the proof of "log_domain x" is performed while computing a logarithm, to 
show that the 0 case is not possible (using log_domain_non_0).

Yves