Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Help on list lemmas

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Help on list lemmas


Chronological Thread 
  • From: Arthur Azevedo de Amorim <arthur.aa AT gmail.com>
  • To: Coq Club <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] Help on list lemmas
  • Date: Sun, 17 Aug 2014 21:16:48 +0200

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



Archive powered by MHonArc 2.6.18.

Top of Page