The Coq mailing list

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

Thanks John.

2014-08-18 2:12 GMT-03:00 John Wiegley <johnw AT newartisans.com>:

>>>>> Marcus Ramos <marcus.ramos AT univasf.edu.br> writes:

> Thanks a lot!

Not sure if this is still of interest, but here's another way of getting to
skip_last without omega:

  Lemma big_enough : forall {X} n l,
    S n <= length l -> exists (x : X) xs, l = x :: xs.
  Proof.
    intros X n l.
    induction l; intros.
      inversion H.
    eauto.
  Qed.

  Lemma skip_last: forall (i: nat) (A: Type) (d: A) (l: list A),

    i < length l -> last (skipn i l) d = last l d.
  Proof.

    intros i A d l.
    generalize dependent i.
    induction l; intros.
      inversion H.
    destruct i; auto.
    simpl in *.
    apply Le.le_S_n in H.
    rewrite IHl.
      apply big_enough in H.
      destruct H. destruct H.
      rewrite H. reflexivity.
    apply H.
  Qed.

John