The Coq mailing list

[Cédric <sedrikov AT gmail.com>]

If you want yet another way to do skip_last (without using omega):

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.
Proof.
intros i A d; induction i; simpl; intros [|h l]; simpl; auto.
Qed.

Fixpoint lt2 (m n : nat) : Prop :=
match n with
| O => False
| S n => match m with O => True | S m => lt2 m n end
end.

Lemma lt_to_lt2 (m n : nat) : m < n -> lt2 m n.
Proof.
intros H; induction H.
+ induction m; simpl; auto.
+ revert IHle; clear; revert m; induction m0; intros [|x]; simpl; auto.
intros [].
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 l H.
generalize (lt_to_lt2 _ _ H); clear H.
revert l; induction i; simpl; auto.
intros [|h l]; simpl; auto.
intros H; case (IHi l H); clear - H.
destruct l; auto.
destruct i; destruct H.
Qed.

Le Sun, 17 Aug 2014 21:36:14 +0200, Marcus Ramos <marcus.ramos AT univasf.edu.br> a écrit:

Hi Gabriel,

Very helpful and very kind of you. Thanks.

Best Regards,

Marcus.

2014-08-17 16:24 GMT-03:00 Gabriel Scherer <gabriel.scherer AT gmail.com>:

I tried to solve the first lemma (in fact solved it), recording my
process as a comment at each step. (I also included the goal in the
comment so that you wouldn't have to replay it to follow it, but it's
still nicer with a replay. I'm only an intermediate user of Coq, so
I'm sure people may have more direct proofs -- although this case is
simple enough that there are not many different solutions.

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.

  (* step 1: let's look at the List documentation
     http://coq.inria.fr/library/Coq.Lists.List.html

     Notice that 'skpin' is defined by induction on 'i', while 'nth'
     matches over both 'i' and 'l'. To reason about them, it's natural
     to do induction on 'i' as well, but we may need to then destruct
     'l' so that the pattern-matching of 'nth' fires.
   *)
  induction i.
  - (* Goal: forall (A : Type) (d : A) (l : list A), hd d (skipn 0 l)
= nth 0 l d *)
    (* (skipn 0 l) should simplify; instead of calling 'simpl' now,
i'll undo 'induction' and call 'simpl' in in both
       induction branches (can't hurt) *)
  Undo.
  induction i; simpl.
  - (* Goal: forall (A : Type) (d : A) (l : list A), hd d l = nth 0 l d *)
    (* I need 'nth 0 l d' to simplify as well;
       as seen in 'nth' code, I need to expose the structure of 'l'
for this to happen *)
    destruct l; simpl.
    (* Now both goals look trivially solvable. Let's undo and do them
at once. *)
    Undo.
    destruct l; simpl; auto.
  - (* Goal:
  i : nat
  IHi : forall (A : Type) (d : A) (l : list A), hd d (skipn i l) = nth i l d
  ============================
   forall (A : Type) (d : A) (l : list A),
   hd d match l with
        | nil => nil
        | _ :: l0 => skipn i l0
        end = nth (S i) l d
     *)
    destruct l; simpl.
    + (* Goal: d = d *) auto.
    + (* Goal: hd d (skipn i l) = nth i l d *)
      (* my only chance is to try the induction hypothesis *)
      apply IHi.
      (* "No more subgoals."
         I didn't know it would work *that* well *)

   (* notice how I applied the same 'destruct l' step in both case?
   Let's start at the beginning again to factorize this. *)
   Restart.

   induction i; destruct l; auto.
   (* only the induction case left. *)
   apply IHi.
Qed.

On Sun, Aug 17, 2014 at 9:16 PM, Arthur Azevedo de Amorim
<arthur.aa AT gmail.com> wrote:
> 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

--

---
Cédric AUGER