The Coq mailing list

[Abhishek Anand <abhishek.anand.iitg AT gmail.com>]

Here something close to what you want (0 based indexing instead of 1 based).

You might want to search the archives about how to write programs as proofs in Coq and the pros, cons and pitfalls of doing that.

In my short and possibly biased summary, when you do that, avoid using complicated tactics like omega and  if the computation gets stuck, you might want to make the lemmas involved in the stuck part transparent (end with Defined instead of Qed). 

Lemma element0BaseIndex : forall {A : Type} (l:list A)(n:nat),

not (nil=l)

 -> lt n (length l) -> A.

Proof.

induction l as [ | lh ltl Hind].

 - intros n Hn. assert (False); [apply Hn; reflexivity| contradiction].

 - intros n Hl Hn. destruct n as [| m].

   + exact lh.

   + destruct ltl.

     * assert False;[| contradiction]. inversion Hn. inversion H0.

     * simpl in Hn. apply (Hind m);[discriminate |]. simpl.

       unfold lt. unfold lt in Hn. apply le_S_n. trivial.

Defined.

(** Let's test that the above definition does not get stuck due to opacity *)

Require Export List.

Lemma arg1 : not (nil = 1::2::nil ).

discriminate.

Defined.

Require Export Omega.

Lemma arg2 : lt 1 (length (1::2::nil)).

simpl. omega.

Defined.

Eval simpl in (element0BaseIndex (1::2::nil) 1 arg1 arg2).

(* computes to 2 *)

-- Abhishek

http://www.cs.cornell.edu/~aa755/

On Fri, Nov 28, 2014 at 12:25 PM, psperatto AT adinet.com.uy <psperatto AT adinet.com.uy> wrote:

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.