rotate_by_reversing.v

Require Import Coq.Lists.List. Import ListNotations.
Require Import Lia.

Lemma skipn_skipn {A} n m (xs : list A) : skipn n (skipn m xs) = skipn (n+m) xs. Admitted.

Section __.
  Context {A : Type}. Implicit Types xs : list A.

  Definition rot' n xs := skipn n xs ++ firstn n xs.
  Lemma rot'_0 xs : rot' 0 xs = xs.
  Proof. cbv [rot']; simpl; rewrite app_nil_r; trivial. Qed.
  Lemma rot'_length xs : rot' (length xs) xs = xs.
  Proof. cbv [rot']; rewrite skipn_all, firstn_all; trivial. Qed.
  Lemma rot'_nil n : rot' n [] = [].
  Proof. cbv [rot']; rewrite skipn_all2, firstn_all2; auto with arith. Qed.
  Lemma rot'_S n xs (H : S n <= length xs) : rot' 1 (rot' n xs) = rot' (S n) xs.
  Proof.
    cbv [rot'].
    repeat rewrite ?skipn_app, ?firstn_app, ?skipn_length.
    unshelve erewrite (_ : _ - _ = O); [Lia.lia|].
    simpl (firstn 0); simpl (skipn 0); cbv beta.
    rewrite app_nil_r, <-app_assoc, skipn_skipn.
    f_equal.
    rewrite <-(firstn_skipn n xs) at 3; rewrite firstn_app.
    rewrite firstn_length.
    unshelve erewrite (_ : _ - _ = 1); [Lia.lia|].
    f_equal.
    rewrite (firstn_all2 (n:=S n)); trivial.
    rewrite firstn_length; Lia.lia.
  Qed.

  Definition rot n := Nat.iter n (rot' 1).
  Lemma rot_small xs n (H : n <= length xs) : rot n xs = rot' n xs.
  Proof. induction n; simpl; rewrite ?IHn,?rot'_0,?rot'_S; auto with arith. Qed.
  Lemma rot_length xs : rot (length xs) xs = xs.
  Proof. rewrite rot_small, rot'_length; trivial. Qed.
  Lemma rot_rot n m xs : rot n (rot m xs) = rot (n + m) xs.
  Proof. induction n; simpl; congruence. Qed.
  Lemma rot_nil n : rot n [] = [].
  Proof. induction n; simpl; rewrite ?IHn, ?rot'_nil; trivial. Qed.
  Lemma rot_length_times_plus n m xs : rot (length xs * n + m) xs = rot m xs.
  Proof.
    rewrite PeanoNat.Nat.mul_comm; induction n; simpl; trivial.
    rewrite <-PeanoNat.Nat.add_assoc, PeanoNat.Nat.add_comm.
    rewrite <-rot_rot, rot_length; trivial.
  Qed.
  Lemma rot_by_rot' n xs (m := Nat.modulo n (length xs))
    : rot n xs = rot' m xs.
  Proof.
    case xs as [|x xs'] eqn:? in |-; [subst xs; simpl; apply rot_nil|].
    assert (length xs <> 0) by (subst xs; discriminate); clear Heql x xs'.
    rewrite (PeanoNat.Nat.div_mod n (length xs)) by trivial.
    rewrite rot_length_times_plus, rot_small; trivial.
    apply PeanoNat.Nat.lt_le_incl, PeanoNat.Nat.mod_upper_bound; trivial.
  Qed.

  Lemma rot'_by_rev n xs
    : rot' n xs = rev (rev (firstn n xs) ++ rev (skipn n xs)).
  Proof. rewrite rev_app_distr, 2rev_involutive; trivial. Qed.

  Lemma rot_by_rev n xs (m := Nat.modulo n (length xs))
    : rot n xs = rev (rev (firstn m xs) ++ rev (skipn m xs)).
  Proof.  rewrite rot_by_rot', rot'_by_rev; trivial. Qed.
End __.