shttpd/coq/S/Vector/Iota.v

(* SPDX-License-Identifier: GPL-2.0 or GPL-3.0
   Copyright © 2019 Ariadne Devos *)

Require Import Coq.Lists.List.

Local Open Scope list_scope.

(* Countdown up to 0, starting from n (exclusive).
   Compare with `seq` from Coq.Lists.List *)

(* Element-wise transformations
   of a vector, without looking at neighbours,
   length ... . Except the index.

   Mostly a reiteration of lemma's in Coq's standard
   library *)

(* For the exponents of positional numbers: 1111 = 10 ** 3 + 10 ** 2 + 10 ** 1 + 1 *)
Fixpoint countdown n : list nat :=
  match n with
  | 0 => nil
  | S n' => n' :: countdown n'
  end.

Theorem countdown_length n : length (countdown n) = n.
Proof.
  induction n.
  + reflexivity.
  + cbn.
    rewrite IHn.
    reflexivity.
Qed.

Theorem countdown0 : countdown 0 = nil.
Proof. reflexivity. Qed.

Theorem countdown_peell n : countdown (S n) = n :: countdown n.
Proof. reflexivity. Qed.

(* An analogue lemma for seq exists. *)

Theorem countdown_shift n : map S (countdown n) ++ 0 :: nil = countdown (S n).
Proof.
  induction n.
  + reflexivity.
  + rewrite (countdown_peell (S n)).
    set (t := map S (countdown (S n))).
    cbn in t.
    subst t.
    rewrite <- app_comm_cons.
    rewrite IHn.
    reflexivity.
Qed.