From 89c50de2ab2b7a552eb80fb799b54fb9e2c4cc17 Mon Sep 17 00:00:00 2001 From: Andrej Dudenhefner <mrhaandi@gmail.com> Date: Thu, 8 Apr 2021 10:39:17 +0200 Subject: [PATCH] Future proof rotate_nat_add_add_mod for https://github.com/coq/coq/pull/14086 --- theories/numbers.v | 12 ++---------- 1 file changed, 2 insertions(+), 10 deletions(-) diff --git a/theories/numbers.v b/theories/numbers.v index 750647cd..e5a05b02 100644 --- a/theories/numbers.v +++ b/theories/numbers.v @@ -1208,20 +1208,12 @@ on nat since otherwise we need the sidecondition [base < len] on 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. + unfold rotate_nat_add. rewrite !Z2Nat.id; [by rewrite Zplus_mod_idemp_l|]. + destruct len as [|i]; [rewrite Zmod_0_r|apply Z_mod_lt]; lia. Qed. Lemma rotate_nat_add_alt base offset len: -- GitLab