From a613b693a68ac6d5511eae0961f38947b6923085 Mon Sep 17 00:00:00 2001
From: Michael Sammler <noreply@sammler.me>
Date: Wed, 8 Apr 2020 10:29:05 +0200
Subject: [PATCH] Added rotate_nat_add, rotate_nat_sub, rotate and rotate_take
 functions

---
 CHANGELOG.md       |   3 +
 theories/list.v    | 126 ++++++++++++++++++++++++++++++++++++++++++
 theories/numbers.v | 135 +++++++++++++++++++++++++++++++++++++++++++++
 theories/sets.v    |   4 ++
 4 files changed, 268 insertions(+)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 0881670f..29542846 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -3,6 +3,9 @@ API-breaking change is listed.
 
 ## std++ master
 
+- Added `rotate` and `rotate_take` functions for accessing a list with
+  wrap-around. Also added `rotate_nat_add` and `rotate_nat_sub` for
+  computing indicies into a rotated list.
 - Added the `select` and `revert select` tactics for selecting and
   reverting a hypothesis based on a pattern.
 - Extracted `list_numbers.v` from `list.v` and `numbers.v` for
diff --git a/theories/list.v b/theories/list.v
index bf29b3ce..0dfd1471 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -143,6 +143,20 @@ Fixpoint replicate {A} (n : nat) (x : A) : list A :=
   match n with 0 => [] | S n => x :: replicate n x end.
 Instance: Params (@replicate) 2 := {}.
 
+(** The function [rotate n l] rotates the list [l] by [n], e.g., [rotate 1
+[x0; x1; ...; xm]] becomes [x1; ...; xm; x0]. Rotating by a multiple of
+[length l] is the identity function. **)
+Definition rotate {A} (n : nat) (l : list A) : list A :=
+  drop (Z.to_nat (n `mod` length l)%Z) l ++ take (Z.to_nat (n `mod` length l)%Z) l.
+Instance: Params (@rotate) 2 := {}.
+
+(** The function [rotate_take s e l] returns the range between the
+indices [s] (inclusive) and [e] (exclusive) of [l]. If [e ≤ s], all
+elements after [s] and before [e] are returned. *)
+Definition rotate_take {A} (s e : nat) (l : list A) : list A :=
+  take (rotate_nat_sub s e (length l)) (rotate s l).
+Instance: Params (@rotate_take) 3 := {}.
+
 (** The function [reverse l] returns the elements of [l] in reverse order. *)
 Definition reverse {A} (l : list A) : list A := rev_append l [].
 Instance: Params (@reverse) 1 := {}.
@@ -1354,6 +1368,97 @@ Lemma lookup_total_resize_old `{!Inhabited A} l n x i :
   n ≤ i → resize n x l !!! i = inhabitant.
 Proof. intros. by rewrite !list_lookup_total_alt, lookup_resize_old. Qed.
 
+(** ** Properties of the [rotate] function *)
+Lemma rotate_replicate n1 n2 x:
+  rotate n1 (replicate n2 x) = replicate n2 x.
+Proof.
+  unfold rotate. rewrite drop_replicate, take_replicate, <-replicate_plus.
+  f_equal. lia.
+Qed.
+
+Lemma rotate_length l n:
+  length (rotate n l) = length l.
+Proof. unfold rotate. rewrite app_length, drop_length, take_length. lia. Qed.
+
+Lemma lookup_rotate_r l n i:
+  i < length l →
+  rotate n l !! i = l !! rotate_nat_add n i (length l).
+Proof.
+  intros Hlen. destruct (Z_mod_lt n (length l)) as [??];[lia|].
+  assert (Z.to_nat (n `mod` length l) < length l) as Hr.
+  { apply Nat2Z.inj_lt. rewrite Z2Nat.id; lia. }
+  unfold rotate. rewrite rotate_nat_add_add_mod, rotate_nat_add_alt by done.
+  remember (Z.to_nat (n `mod` length l)) as n'.
+  case_decide.
+  - by rewrite lookup_app_l, lookup_drop by (rewrite drop_length; lia).
+  - rewrite lookup_app_r, lookup_take, drop_length by (rewrite drop_length; lia).
+    f_equal. lia.
+Qed.
+
+Lemma lookup_rotate_r_Some l n i x:
+  rotate n l !! i = Some x ↔
+  l !! rotate_nat_add n i (length l) = Some x ∧ i < length l.
+Proof.
+  split.
+  - intros Hl. pose proof (lookup_lt_Some _ _ _ Hl) as Hlen.
+    rewrite rotate_length in Hlen. by rewrite <-lookup_rotate_r.
+  - intros [??]. by rewrite lookup_rotate_r.
+Qed.
+
+Lemma lookup_rotate_l l n i:
+  i < length l → rotate n l !! rotate_nat_sub n i (length l) = l !! i.
+Proof.
+  intros ?. rewrite lookup_rotate_r, rotate_nat_add_sub;[done..|].
+  apply rotate_nat_sub_lt. lia.
+Qed.
+
+Lemma elem_of_rotate l n x:
+  x ∈ rotate n l ↔ x ∈ l.
+Proof.
+  unfold rotate. rewrite <-(take_drop (Z.to_nat (n `mod` length l)) l) at 5.
+  rewrite !elem_of_app. naive_solver.
+Qed.
+
+Lemma rotate_insert_l l n i x:
+  i < length l →
+  rotate n (<[rotate_nat_add n i (length l):=x]> l) = <[i:=x]> (rotate n l).
+Proof.
+  intros Hlen. destruct (Z_mod_lt n (length l)) as [Hn1 Hn2];[lia|].
+  assert (Z.to_nat (n `mod` length l) < length l) as Hr.
+  { apply Nat2Z.inj_lt. rewrite Z2Nat.id; lia. } unfold rotate.
+  rewrite insert_length, rotate_nat_add_add_mod, rotate_nat_add_alt by done.
+  remember (Z.to_nat (n `mod` length l)) as n'.
+  case_decide.
+  - rewrite take_insert, drop_insert_le, insert_app_l
+      by (rewrite ?drop_length; lia). do 2 f_equal. lia.
+  - rewrite take_insert_lt, drop_insert_gt, insert_app_r_alt, drop_length
+      by (rewrite ?drop_length; lia). do 2 f_equal. lia.
+Qed.
+
+Lemma rotate_insert_r l n i x:
+  i < length l →
+  rotate n (<[i:=x]> l) = <[rotate_nat_sub n i (length l):=x]> (rotate n l).
+Proof.
+  intros ?. rewrite <-rotate_insert_l, rotate_nat_add_sub;[done..|].
+  apply rotate_nat_sub_lt. lia.
+Qed.
+
+(** ** Properties of the [rotate_take] function *)
+Lemma rotate_take_insert l s e i x:
+  i < length l →
+  rotate_take s e (<[i:=x]>l) =
+  if decide (rotate_nat_sub s i (length l) < rotate_nat_sub s e (length l)) then
+    <[rotate_nat_sub s i (length l):=x]> (rotate_take s e l) else rotate_take s e l.
+Proof.
+  intros ?. unfold rotate_take. rewrite rotate_insert_r, insert_length by done.
+  case_decide; [rewrite take_insert_lt | rewrite take_insert]; naive_solver lia.
+Qed.
+
+Lemma rotate_take_add l b i :
+  i < length l →
+  rotate_take b (rotate_nat_add b i (length l)) l = take i (rotate b l).
+Proof. intros ?. unfold rotate_take. by rewrite rotate_nat_sub_add. Qed.
+
 (** ** Properties of the [reshape] function *)
 Lemma reshape_length szs l : length (reshape szs l) = length szs.
 Proof. revert l. by induction szs; intros; f_equal/=. Qed.
@@ -2793,6 +2898,19 @@ Section Forall2.
     P x y → Forall2 P (replicate n x) (replicate n y).
   Proof. induction n; simpl; constructor; auto. Qed.
 
+  Lemma Forall2_rotate n l k :
+    Forall2 P l k → Forall2 P (rotate n l) (rotate n k).
+  Proof.
+    intros HAll. unfold rotate. rewrite (Forall2_length _ _ HAll).
+    eauto using Forall2_app, Forall2_take, Forall2_drop.
+  Qed.
+  Lemma Forall2_rotate_take s e l k :
+    Forall2 P l k → Forall2 P (rotate_take s e l) (rotate_take s e k).
+  Proof.
+    intros HAll. unfold rotate_take. rewrite (Forall2_length _ _ HAll).
+    eauto using Forall2_take, Forall2_rotate.
+  Qed.
+
   Lemma Forall2_reverse l k : Forall2 P l k → Forall2 P (reverse l) (reverse k).
   Proof.
     induction 1; rewrite ?reverse_nil, ?reverse_cons; eauto using Forall2_app.
@@ -2943,6 +3061,10 @@ Section Forall2_proper.
 
   Global Instance: Proper (R ==> Forall2 R) (replicate n).
   Proof. repeat intro. eauto using Forall2_replicate. Qed.
+  Global Instance: Proper (Forall2 R ==> Forall2 R) (rotate n).
+  Proof. repeat intro. eauto using Forall2_rotate. Qed.
+  Global Instance: Proper (Forall2 R ==> Forall2 R) (rotate_take s e).
+  Proof. repeat intro. eauto using Forall2_rotate_take. Qed.
   Global Instance: Proper (Forall2 R ==> Forall2 R) reverse.
   Proof. repeat intro. eauto using Forall2_reverse. Qed.
   Global Instance: Proper (Forall2 R ==> option_Forall2 R) last.
@@ -3101,6 +3223,10 @@ Section setoid.
   Proof. intros ???. rewrite !equiv_Forall2. by apply Forall2_filter. Qed.
   Global Instance replicate_proper n : Proper ((≡@{A}) ==> (≡)) (replicate n).
   Proof. induction n; constructor; auto. Qed.
+  Global Instance rotate_proper n : Proper ((≡@{list A}) ==> (≡)) (rotate n).
+  Proof. intros ??. rewrite !equiv_Forall2. by apply Forall2_rotate. Qed.
+  Global Instance rotate_take_proper s e : Proper ((≡@{list A}) ==> (≡)) (rotate_take s e).
+  Proof. intros ??. rewrite !equiv_Forall2. by apply Forall2_rotate_take. Qed.
   Global Instance reverse_proper : Proper ((≡) ==> (≡@{list A})) reverse.
   Proof.
     induction 1; rewrite ?reverse_cons; simpl; [constructor|].
diff --git a/theories/numbers.v b/theories/numbers.v
index d0b9d29d..46805624 100644
--- a/theories/numbers.v
+++ b/theories/numbers.v
@@ -452,6 +452,22 @@ Proof.
     apply Nat.mod_bound_pos; lia. }
   by rewrite <-Nat2Z.inj_mul, <-Nat2Z.inj_add, <-Nat.div_mod.
 Qed.
+Lemma Nat2Z_inj_div x y :
+  0 ≤ x → 0 ≤ y →
+  Z.to_nat (x `div` y) = (Z.to_nat x `div` Z.to_nat y)%nat.
+Proof.
+  intros. destruct (decide (y = 0%nat)); [by subst; destruct x|].
+  pose proof (Z.div_pos x y).
+  apply (inj Z.of_nat). by rewrite Z2Nat_inj_div, !Z2Nat.id by lia.
+Qed.
+Lemma Nat2Z_inj_mod x y :
+  0 ≤ x → 0 ≤ y →
+  Z.to_nat (x `mod` y) = (Z.to_nat x `mod` Z.to_nat y)%nat.
+Proof.
+  intros. destruct (decide (y = 0%nat)); [by subst; destruct x|].
+  pose proof (Z_mod_pos x y).
+  apply (inj Z.of_nat). by rewrite Z2Nat_inj_mod, !Z2Nat.id by lia.
+Qed.
 Lemma Z_succ_pred_induction y (P : Z → Prop) :
   P y →
   (∀ x, y ≤ x → P x → P (Z.succ x)) →
@@ -808,3 +824,122 @@ Qed.
 
 Lemma Qp_ge_0 (q: Qp): (0 ≤ q)%Qc.
 Proof. apply Qclt_le_weak, Qp_prf. Qed.
+
+(** * Helper for working with accessing lists with wrap-around
+    See also [rotate] and [rotate_take] in [list.v] *)
+(** [rotate_nat_add base offset len] computes [(base + offset) `mod`
+len]. This is useful in combination with the [rotate] function on
+lists, since the index [i] of [rotate n l] corresponds to the index
+[rotate_nat_add n i (length i)] of the original list. The definition
+uses [Z] for consistency with [rotate_nat_sub]. **)
+Definition rotate_nat_add (base offset len : nat) : nat :=
+  Z.to_nat ((base + offset) `mod` len)%Z.
+(** [rotate_nat_sub base offset len] is the inverse of [rotate_nat_add
+base offset len]. The definition needs to use modulo on [Z] instead of
+on nat since otherwise we need the sidecondition [base < len] on
+[rotate_nat_sub_add]. **)
+Definition rotate_nat_sub (base offset len : nat) : nat :=
+  Z.to_nat ((len + offset - base) `mod` len)%Z.
+
+Lemma rotate_nat_add_len_0 base offset:
+  rotate_nat_add base offset 0 = 0.
+Proof. unfold rotate_nat_add. by rewrite Zmod_0_r. Qed.
+Lemma rotate_nat_sub_len_0 base offset:
+  rotate_nat_sub base offset 0 = 0.
+Proof. unfold rotate_nat_sub. by rewrite Zmod_0_r. Qed.
+
+Lemma rotate_nat_add_add_mod base offset len:
+  rotate_nat_add base offset len =
+  rotate_nat_add (Z.to_nat (base `mod` len)%Z) offset len.
+Proof.
+  destruct len as [|i];[ by rewrite !rotate_nat_add_len_0|].
+  pose proof (Z_mod_lt base (S i)) as Hlt. unfold rotate_nat_add.
+  rewrite !Z2Nat.id by lia. by rewrite Zplus_mod_idemp_l.
+Qed.
+
+Lemma rotate_nat_add_alt base offset len:
+  base < len → offset < len →
+  rotate_nat_add base offset len =
+  if decide (base + offset < len) then base + offset else base + offset - len.
+Proof.
+  unfold rotate_nat_add. intros ??. case_decide.
+  - rewrite Z.mod_small by lia. by rewrite <-Nat2Z.inj_add, Nat2Z.id.
+  - rewrite (Zmod_in_range 1) by lia.
+    by rewrite Z.mul_1_l, <-Nat2Z.inj_add, <-Nat2Z.inj_sub,Nat2Z.id by lia.
+Qed.
+Lemma rotate_nat_sub_alt base offset len:
+  base < len → offset < len →
+  rotate_nat_sub base offset len =
+  if decide (offset < base) then len + offset - base else offset - base.
+Proof.
+  unfold rotate_nat_sub. intros ??. case_decide.
+  - rewrite Z.mod_small by lia.
+    by rewrite <-Nat2Z.inj_add, <-Nat2Z.inj_sub, Nat2Z.id by lia.
+  - rewrite (Zmod_in_range 1) by lia.
+    rewrite Z.mul_1_l, <-Nat2Z.inj_add, <-!Nat2Z.inj_sub,Nat2Z.id; lia.
+Qed.
+
+Lemma rotate_nat_add_0 base len :
+  base < len → rotate_nat_add base 0 len = base.
+Proof.
+  intros ?. unfold rotate_nat_add.
+  rewrite Z.mod_small by lia. by rewrite Z.add_0_r, Nat2Z.id.
+Qed.
+Lemma rotate_nat_sub_0 base len :
+  base < len → rotate_nat_sub base base len = 0.
+Proof. intros ?. rewrite rotate_nat_sub_alt by done. case_decide; lia. Qed.
+
+Lemma rotate_nat_add_lt base offset len :
+  0 < len → rotate_nat_add base offset len < len.
+Proof.
+  unfold rotate_nat_add. intros ?.
+  pose proof (Nat.mod_upper_bound (base + offset) len).
+  rewrite Nat2Z_inj_mod, Z2Nat.inj_add, !Nat2Z.id; lia.
+Qed.
+Lemma rotate_nat_sub_lt base offset len :
+  0 < len → rotate_nat_sub base offset len < len.
+Proof.
+  unfold rotate_nat_sub. intros ?.
+  pose proof (Z_mod_lt (len + offset - base) len).
+  apply Nat2Z.inj_lt. rewrite Z2Nat.id; lia.
+Qed.
+
+Lemma rotate_nat_add_sub base len offset:
+  offset < len →
+  rotate_nat_add base (rotate_nat_sub base offset len) len = offset.
+Proof.
+  intros ?. unfold rotate_nat_add, rotate_nat_sub.
+  rewrite Z2Nat.id by (apply Z_mod_pos; lia). rewrite Zplus_mod_idemp_r.
+  replace (base + (len + offset - base))%Z with (len + offset)%Z by lia.
+  rewrite (Zmod_in_range 1) by lia.
+  rewrite Z.mul_1_l, <-Nat2Z.inj_add, <-!Nat2Z.inj_sub,Nat2Z.id; lia.
+Qed.
+
+Lemma rotate_nat_sub_add base len offset:
+  offset < len →
+  rotate_nat_sub base (rotate_nat_add base offset len) len = offset.
+Proof.
+  intros ?. unfold rotate_nat_add, rotate_nat_sub.
+  rewrite Z2Nat.id by (apply Z_mod_pos; lia).
+  assert (∀ n, (len + n - base) = ((len - base) + n))%Z as -> by naive_solver lia.
+  rewrite Zplus_mod_idemp_r.
+  replace (len - base + (base + offset))%Z with (len + offset)%Z by lia.
+  rewrite (Zmod_in_range 1) by lia.
+  rewrite Z.mul_1_l, <-Nat2Z.inj_add, <-!Nat2Z.inj_sub,Nat2Z.id; lia.
+Qed.
+
+Lemma rotate_nat_add_add base offset len n:
+  0 < len →
+  rotate_nat_add base (offset + n) len =
+  (rotate_nat_add base offset len + n) `mod` len.
+Proof.
+  intros ?. unfold rotate_nat_add.
+  rewrite !Nat2Z_inj_mod, !Z2Nat.inj_add, !Nat2Z.id by lia.
+  by rewrite plus_assoc, Nat.add_mod_idemp_l by lia.
+Qed.
+
+Lemma rotate_nat_add_S base offset len:
+  0 < len →
+  rotate_nat_add base (S offset) len =
+  S (rotate_nat_add base offset len) `mod` len.
+Proof. intros ?. by rewrite <-Nat.add_1_r, rotate_nat_add_add, Nat.add_1_r. Qed.
diff --git a/theories/sets.v b/theories/sets.v
index 3462f1ba..2a97d742 100644
--- a/theories/sets.v
+++ b/theories/sets.v
@@ -300,6 +300,10 @@ Section set_unfold_list.
     constructor. rewrite elem_of_list_fmap. f_equiv; intros y.
     by rewrite (set_unfold_elem_of y l (P y)).
   Qed.
+  Global Instance set_unfold_rotate x l P n:
+    SetUnfoldElemOf x l P → SetUnfoldElemOf x (rotate n l) P.
+  Proof. constructor. by rewrite elem_of_rotate, (set_unfold_elem_of x l P). Qed.
+
 End set_unfold_list.
 
 Tactic Notation "set_unfold" :=
-- 
GitLab