The Coq mailing list

["psperatto AT adinet.com.uy" <psperatto AT adinet.com.uy>]

I have send an email past wednesday.

I have problema with a match definition.

I have written the definition that I adjoin 
below,

I use arguments smaller in the
recursive call but Coq does not accept
it.

I explain what has happen in comments
inside the definition.

(* I have written the definitions below:*)
(*-------------------------------------------*)

Variable A:Type.
Parameter R: A -> A -> bool.

Lemma not_le_2(a:A)(m:nat) : 
       not (le (S (S m)) 
               (length (cons a nil))).
unfold length.
apply gt_not_le.
apply gt_n_S.
apply gt_Sn_O.
Qed.

Lemma zero_succ (n:nat) : not(O=(S n)).
intro.
apply (le_Sn_0 n).
rewrite H.
apply le_n.
Qed.

Lemma nil_cons (x:A)(l:list A) 
: not (nil=cons x l).
intro.
discriminate.
Qed.

(* I want to define a function element that given a list
l and a natural number n returns the element in the
list at the n-th position. I have put the preconditions
to the function as hypothesis of function types. *)

(* I get the following error message : 
Recursive definition of element is ill-formed. 

I don't understand why does not accept the recursive
call since it is applied to elements smaller *)


Fixpoint element (l:list A)(n:nat){struct l}:
not (nil=l) ->  not (O=n) 
 -> le n (length l) -> A:=
match l, n with
| nil, _ => (fun q => 
            fun p =>
            fun r => (False_rec
                      A
                     (q (refl_equal nil))))
| _, O => (fun q => 
          fun p =>
          fun r => (False_rec
                    A
                    (p (refl_equal O))))
| (cons x l1),(S O) => 
           (fun q => 
            fun p =>
            fun r => x)
| (cons x nil), (S (S m)) => (fun q => 
      fun p =>
      fun r => (False_rec
                A
                ((not_le_2 x m) r)))
| (cons x (cons y l1)), (S (S m)) =>
            (fun q =>
             fun p =>
             fun r => 
(element (cons y l1) (S m)
(nil_cons y l1)
(zero_succ m)
(le_S_n (S m) 
(length (cons y l1)) r)))
end.
                      
(* ----------------------------------------------------------------*)

Regards, Patricia.