The Coq mailing list

[David Monniaux <monniaux AT clipper.ens.fr>]

Hi,

I'm a beginner in Coq. I started implementing some canonical examples such
as lists etc... I wanted to implement a projection function; that is, a
function taking a list l with items of type X, an integer i so that 0 <= i
< (length l) and giving the i-th item in the list.

This "extract" function would thus be of type:
(l: list) {i: nat | (lt i (length l))} -> X, X being the set from which
the items of the list are taken.

* ABSURD CASE
Here some problems arise: when programming the definition of this function
as an inductive definition, there is one case ((proj1 i) = (S n) and l =
Nil) that is prevented by the condition in i. The question is: how am I
supposed to take advantage of it?

There's surely a way to draw a contradiction from this case. What is the
correct way, from this contradiction, to extract a "anything" value, in a
similar fashion that we can extract "any proposition" from the "absurd"
value?

* CRYPTIC ERROR MESSAGE
Also, why is the following code incorrect?
Fixpoint extract [l: list] : {i: nat | (lt i (length l))} -> nat :=
  [ii: {i: nat | (lt i (length l))}]
    Cases ii of (exist i _) =>
      Cases l of
        Nil => O
      | (Cons h t) =>
        Cases i of
          O => O
        | (S j) => O
        end
      end
    end.

Error message : Illegal application (Non-functional construction) : 
In environment: 
X : Set
extract : (l:list){i:nat | (lt i (length l))}->nat
l : list
ii : {i:nat | (lt i (length l))}
i : nat
<> : ([i0:nat](lt i0 (length l)) i)
The term nat : Set cannot be applied to the terms
(length l)
: nat

I must admit I'm not too familiar with implicit syntax....

* CONSTRAINED TYPES
 
My experience with PVS (another prover) is that constrained parameters are
easy to use because they are automatically cast into less constrained
parameters (more accurately, a TCC [type-checking condition] is generated
for this cast, and trivial ones are thrown out by the system before being
submitted to the user); the automatic generation of TCCs when casting an
less constrained value into a constrained type is also very useful.

As far as I know, there's no equivalent in Coq to this ease of use of
typechecking conditions: constrained values are written as dependent
products, whose second parameter is the proof of the satisfaction of the
constraint. Proof terms are tedious to write directly; thus one would have
to write an explicit intermediary lemma and instanciate it in the code of
the function... In the reverse way, one has to project the dependent
product, maybe using an implicit coercion.

Are there easier ways?

Sorry for asking such trivial questions...

-- David Monniaux