The Coq mailing list

[Marcus Ramos <marcus.ramos AT univasf.edu.br>]

Thanks Emilio.

2014-08-19 0:58 GMT-03:00 Emilio Jesús Gallego Arias <emilioga AT cis.upenn.edu>:

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