The Coq mailing list

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

Hi Arthur,

Thanks a lot!

Best Regards,

Marcus.

2014-08-17 16:16 GMT-03:00 Arthur Azevedo de Amorim <arthur.aa AT gmail.com>:

One possible source of difficulty is that you need to do induction
over one argument (say, i), but generalize over the other (l in this
case), otherwise your induction hypothesis will be too weak. Here are
possible solutions.

Require Import List.
Require Import Omega.
Import ListNotations.

Lemma skip_hd:
forall i: nat,
forall A: Type,
forall d: A,
forall l: list A,
hd d (skipn i l) = nth i l d.

Proof.
  intros i A d.
  induction i as [|i IH]; intros [|a l]; trivial.
  simpl.
  now rewrite IH.
Qed.

Lemma skip_last:
forall i: nat,
forall A: Type,
forall d: A,
forall l: list A,
i < length l -> last (skipn i l) d = last l d.

Proof.
  intros i A d.
  induction i as [|i IH]; intros [|a l]; trivial.
  simpl. intros Hl.
  assert (Hl' : i < length l) by omega.
  rewrite IH; trivial.
  destruct l; trivial.
  simpl in Hl'. omega.
Qed.

2014-08-17 20:57 GMT+02:00 Marcus Ramos <marcus.ramos AT univasf.edu.br>:

> Hi,
>
> 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.
>
> Require Import List.
>
> Lemma skip_hd:
> forall i: nat,
> forall A: Type,
> forall d: A,
> forall l: list A,
> hd d (skipn i l) = nth i l d.
>
> Lemma skip_last:
> forall i: nat,
> forall A: Type,
> forall d: A,
> forall l: list A,
> i < length l -> last (skipn i l) d = last l d.
>
> Thanks in advance,
> Marcus.

--
Arthur Azevedo de Amorim