coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- [Coq-Club] Help on list lemmas, Marcus Ramos, 08/17/2014
- Re: [Coq-Club] Help on list lemmas, Arthur Azevedo de Amorim, 08/17/2014
- Re: [Coq-Club] Help on list lemmas, Marcus Ramos, 08/17/2014
- Re: [Coq-Club] Help on list lemmas, John Wiegley, 08/18/2014
- Re: [Coq-Club] Help on list lemmas, Marcus Ramos, 08/21/2014
- Re: [Coq-Club] Help on list lemmas, John Wiegley, 08/18/2014
- Re: [Coq-Club] Help on list lemmas, Gabriel Scherer, 08/17/2014
- Re: [Coq-Club] Help on list lemmas, Marcus Ramos, 08/17/2014
- Re: [Coq-Club] Help on list lemmas, Cédric, 08/17/2014
- Re: [Coq-Club] Help on list lemmas, Marcus Ramos, 08/21/2014
- Re: [Coq-Club] Help on list lemmas, Cédric, 08/17/2014
- Re: [Coq-Club] Help on list lemmas, Marcus Ramos, 08/17/2014
- Re: [Coq-Club] Help on list lemmas, Marcus Ramos, 08/17/2014
- Re: [Coq-Club] Help on list lemmas, Emilio Jesús Gallego Arias, 08/19/2014
- Re: [Coq-Club] Help on list lemmas, Marcus Ramos, 08/21/2014
- Re: [Coq-Club] Help on list lemmas, Arthur Azevedo de Amorim, 08/17/2014
Archive powered by MHonArc 2.6.18.