The Coq mailing list

[Abhishek Anand <abhishek.anand.iitg AT gmail.com>]

Theorem list_of_nats_nth  {k n} len default (p: k <= n): nth k (list_of_nats n len) default = len + k - n.

Proof.

generalize dependent k.

generalize dependent len.

generalize dependent default.

generalize dependent n.

induction n; intros def l k Hleq.

- assert (k=0) by omega. subst. simpl. omega. 

- inversion Hleq;subst.

  + assert (n <= n) as XX by omega. simpl.  eapply (IHn def l) in XX; eauto. rewrite XX. omega.

  + simpl. destruct k; try omega. assert (l + S k - S n =  l +  k -  n) as XR by omega.

    rewrite XR. eapply IHn; eauto. omega.

Qed.

-- Abhishek

http://www.cs.cornell.edu/~aa755/

On Wed, Dec 11, 2013 at 6:21 PM, Ilmārs Cīrulis <ilmars.cirulis AT gmail.com> wrote:

Fixpoint list_of_nats n len: list nat :=

 match n with O => cons len nil | S m => cons (len - n) (list_of_nats m len) end.

Theorem list_of_nats_nth {k n} len default (p: k <= n): nth k (list_of_nats n len) default = len + k - n.

Admitted.

I can't prove it for long time already. Any hints are very appreciated.