From 79f6566af9bfce269005615105f4cf5fd9033a99 Mon Sep 17 00:00:00 2001
From: Michael Sammler <noreply@sammler.me>
Date: Thu, 29 Apr 2021 15:35:59 +0200
Subject: [PATCH] Don't use Z.to_nat in definition of rotate

---
 theories/list.v    | 20 ++++++++------------
 theories/numbers.v |  9 ++-------
 2 files changed, 10 insertions(+), 19 deletions(-)

diff --git a/theories/list.v b/theories/list.v
index 4a0321ab..4468f28b 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -150,7 +150,7 @@ Instance: Params (@replicate) 2 := {}.
 [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.
+  drop (n `mod` length l) l ++ take (n `mod` length l) l.
 Instance: Params (@rotate) 2 := {}.
 
 (** The function [rotate_take s e l] returns the range between the
@@ -1404,11 +1404,9 @@ 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'.
+  intros Hlen. pose proof (Nat.mod_upper_bound n (length l)) as ?.
+  unfold rotate. rewrite rotate_nat_add_add_mod, rotate_nat_add_alt by lia.
+  remember (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).
@@ -1435,7 +1433,7 @@ 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.
+  unfold rotate. rewrite <-(take_drop (n `mod` length l) l) at 5.
   rewrite !elem_of_app. naive_solver.
 Qed.
 
@@ -1443,11 +1441,9 @@ 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'.
+  intros Hlen. pose proof (Nat.mod_upper_bound n (length l)) as ?. unfold rotate.
+  rewrite insert_length, rotate_nat_add_add_mod, rotate_nat_add_alt by lia.
+  remember (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.
diff --git a/theories/numbers.v b/theories/numbers.v
index c0c636b7..67009522 100644
--- a/theories/numbers.v
+++ b/theories/numbers.v
@@ -1253,13 +1253,8 @@ Definition rotate_nat_sub (base offset len : nat) : nat :=
 
 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.
-  (* TODO: [Z_mod_nonneg_nonneg] once that's part of all supported Coq versions *)
-  unfold rotate_nat_add. assert (0 ≤ base `mod` len)%Z.
-  { destruct len as [|i]; [rewrite Zmod_0_r|apply Z_mod_lt]; lia. }
-  by rewrite Z2Nat.id, Zplus_mod_idemp_l.
-Qed.
+  rotate_nat_add (base `mod` len) offset len.
+Proof. unfold rotate_nat_add. by rewrite Nat2Z_inj_mod, Zplus_mod_idemp_l. Qed.
 
 Lemma rotate_nat_add_alt base offset len:
   base < len → offset < len →
-- 
GitLab