Vector reversal in a couple lines.

vec_rev.v

From Stdlib Require Import Vector.
Notation vec := Vector.t.
Arguments nil {A}.
Arguments cons {A} _ {n}.

(* For some reason cons has the length argument after the head argument, which
will be cumbersome here. *)
Definition cons' {A} n (x : A) (xs : vec A n) : vec A (S n) := cons x xs.
Arguments cons' {_} _ _ _ /.

(** 1: Standard naive vector reversal *)

(* First define extension on the right.. *)
Fixpoint snoc {A n} (vs : vec A n) (a : A) : vec A (S n) :=
  match vs with
  | nil       => cons a nil
  | cons v vs => cons v (snoc vs a)
  end.

(* ..then iterate. *)
Fixpoint slow_rev {A n} (vs : vec A n) : vec A n :=
  match vs with
  | nil       => nil
  | cons v vs => snoc (slow_rev vs) v
  end.

(* Laws are direct inductions. *)
Lemma slow_rev_snoc {A n} (a : A) (vs : vec A n)
  : slow_rev (snoc vs a) = cons a (slow_rev vs) .
Proof.
  induction vs; auto.
  cbn; now rewrite IHvs.
Qed.
  
Lemma slow_rev_invol {A n} (vs : vec A n) : slow_rev (slow_rev vs) = vs .
Proof.
  induction vs; auto.
  cbn; rewrite slow_rev_snoc; now f_equal.
Qed.

(** 2: Tail-recursive vector reverse _without rewriting_!

See "A well-known representation of monoids and its application to the
function ‘vector reverse’", Wouter Swierstra, JFP 2022. *)

(* Lets start with the strictified natural numbers. *)
Definition strict_nat := nat -> nat.
Definition sO : strict_nat := fun x => x .
Definition sS : strict_nat -> strict_nat := fun m x => m (S x) .

(* Next define the tail-recursive generalization of reverse:
‘reverse append’ and deduce the fast reverse. The trick is to have the
second argument indexed by a strictified natural number. *)
Fixpoint strict_rev_app {A n} (xs : vec A n) 
  m (c : forall k, A -> vec A (m k) -> vec A (sS m k))
  (ys : vec A (m O)) : vec A (m n) :=
  match xs with
  | nil => ys
  | cons x xs => strict_rev_app xs (sS m) (fun k => c _) (c _ x ys)
  end .

Definition fast_rev {A m} (xs : vec A m) : vec A m
  := strict_rev_app xs sO cons' nil .

(* To reason on this we will need vector concatenation.. *)
Fixpoint strict_app {A m n}
  (c : forall k, A -> vec A (m k) -> vec A (sS m k))
  (xs : vec A n) (ys : vec A (m O)) : vec A (m n) :=
  match xs with
  | nil => ys
  | cons x xs => c _ x (strict_app c xs ys)
  end .

(* ..as well as a modicum of theory. *)
Lemma strict_app_nil_r {A n} (xs : vec A n)
  : strict_app (m := sO) cons' xs nil = xs .
Proof.
  induction xs; auto; cbn; now f_equal.
Qed.

Lemma strict_app_snoc {A m n}
  (c : forall k, A -> vec A (m k) -> vec A (sS m k))
  (xs : vec A n) (ys : vec A (m O)) (x : A)
  : strict_app c (snoc xs x) ys = strict_app (fun k => c (S k)) xs (c _ x ys) . 
Proof.
  induction xs; auto.
  cbn; now f_equal.
Qed.

(* We can now give the specification for ‘reverse append’.. *)
Lemma strict_rev_app_spec {A n} (xs : vec A n)
  : forall m (c : forall k, A -> vec A (m k) -> vec A (sS m k))
  (ys : vec A (m O)),
  strict_rev_app xs m c ys = strict_app c (slow_rev xs) ys .
Proof.
  induction xs; intros; auto.
  cbn; now rewrite IHxs, strict_app_snoc.
Qed.

(* ..the specification for fast reverse.. *)
Lemma fast_rev_spec {A n} (xs : vec A n) : fast_rev xs = slow_rev xs .
Proof.
  unfold fast_rev.
  now rewrite strict_rev_app_spec, strict_app_nil_r.
Qed.  

(* ..and deduce the usual theory on fast reverse. *)
Lemma fast_rev_snoc {A n} (a : A) (vs : vec A n)
  : fast_rev (snoc vs a) = cons a (fast_rev vs) .
Proof.
  now rewrite 2 fast_rev_spec, slow_rev_snoc.
Qed.

Lemma fast_rev_invol {A n} (a : A) (vs : vec A n)
  : fast_rev (fast_rev vs) = vs.
Proof.
  now rewrite 2 fast_rev_spec, slow_rev_invol.
Qed.