The Coq mailing list

[emilioga AT cis.upenn.edu (Emilio Jesús Gallego Arias)]

Hi Marcus,

Marcus Ramos 
<marcus.ramos AT univasf.edu.br>
 writes:

> I guess the following two list lemmas are correct, however I am not able to
> finish their proofs by myself. In case you have any hints or comments, I
> would be glad to hear about them.

Another possibility in addition to the excellent solutions that have
been posted is to use the ssreflect library that I have found useful
when doing certain proofs similar to the ones you sent.

Find my solution, but keep in mind that I am a total newbie:

Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq.
Set Implicit Arguments.

Require Import List.

Lemma skip_hd A d :
  forall (i : nat) (l : list A),
    hd d (skipn i l) = nth i l d.
Proof.
  by elim=> [ [] | n IH []].
Qed.

Lemma skip_last A d :
  forall (i : nat) (l : list A),
    i < length l ->
    last (skipn i l) d = last l d.
Proof.
  elim=> // n IH [|x [|y l]] // Hlt.
  by rewrite IH.
Qed.

Best,
Emilio