From 91fae00ccdd17e48826bd2e9614d46c8dac2c74d Mon Sep 17 00:00:00 2001 From: Ralf Jung <jung@mpi-sws.org> Date: Thu, 29 Apr 2021 11:40:33 +0200 Subject: [PATCH] make Z.of_nat not a coercion inside the prelude implementation --- theories/list_numbers.v | 16 ++++++++-------- theories/numbers.v | 30 ++++++++++++++++-------------- theories/prelude.v | 4 ++++ 3 files changed, 28 insertions(+), 22 deletions(-) diff --git a/theories/list_numbers.v b/theories/list_numbers.v index 1bb5a816..43e5d06c 100644 --- a/theories/list_numbers.v +++ b/theories/list_numbers.v @@ -7,7 +7,7 @@ From stdpp Require Import options. (** [seqZ m n] generates the sequence [m], [m + 1], ..., [m + n - 1] over integers, provided [0 ≤ n]. If [n < 0], then the range is empty. **) Definition seqZ (m len: Z) : list Z := - (λ i: nat, Z.add i m) <$> (seq 0 (Z.to_nat len)). + (λ i: nat, Z.add (Z.of_nat i) m) <$> (seq 0 (Z.to_nat len)). Global Arguments seqZ : simpl never. Definition sum_list_with {A} (f : A → nat) : list A → nat := @@ -107,7 +107,7 @@ Section seqZ. f_equal/=. rewrite Z.pred_succ, IH; simpl. f_equal; lia. - by rewrite !seqZ_nil by lia. Qed. - Lemma lookup_seqZ_lt m n i : i < n → seqZ m n !! i = Some (m + i). + Lemma lookup_seqZ_lt m n i : Z.of_nat i < n → seqZ m n !! i = Some (m + Z.of_nat i). Proof. revert m i. induction n as [|n ? IH|] using (Z_succ_pred_induction 0); intros m i Hi; [lia| |lia]. @@ -115,9 +115,9 @@ Section seqZ. - f_equal; lia. - rewrite Z.pred_succ, IH by lia. f_equal; lia. Qed. - Lemma lookup_total_seqZ_lt m n i : i < n → seqZ m n !!! i = m + i. + Lemma lookup_total_seqZ_lt m n i : Z.of_nat i < n → seqZ m n !!! i = m + Z.of_nat i. Proof. intros. by rewrite !list_lookup_total_alt, lookup_seqZ_lt. Qed. - Lemma lookup_seqZ_ge m n i : n ≤ i → seqZ m n !! i = None. + Lemma lookup_seqZ_ge m n i : n ≤ Z.of_nat i → seqZ m n !! i = None. Proof. revert m i. induction n as [|n ? IH|] using (Z_succ_pred_induction 0); intros m i Hi; try lia. @@ -126,11 +126,11 @@ Section seqZ. destruct i as [|i]; simpl; [lia|]. by rewrite Z.pred_succ, IH by lia. - by rewrite seqZ_nil by lia. Qed. - Lemma lookup_total_seqZ_ge m n i : n ≤ i → seqZ m n !!! i = inhabitant. + Lemma lookup_total_seqZ_ge m n i : n ≤ Z.of_nat i → seqZ m n !!! i = inhabitant. Proof. intros. by rewrite !list_lookup_total_alt, lookup_seqZ_ge. Qed. - Lemma lookup_seqZ m n i m' : seqZ m n !! i = Some m' ↔ m' = m + i ∧ i < n. + Lemma lookup_seqZ m n i m' : seqZ m n !! i = Some m' ↔ m' = m + Z.of_nat i ∧ Z.of_nat i < n. Proof. - destruct (Z_le_gt_dec n i). + destruct (Z_le_gt_dec n (Z.of_nat i)). - rewrite lookup_seqZ_ge by lia. naive_solver lia. - rewrite lookup_seqZ_lt by lia. naive_solver lia. Qed. @@ -148,7 +148,7 @@ Section seqZ. rewrite Nat2Z.inj_add, Z2Nat.id by done. lia. Qed. - Lemma seqZ_S m i : seqZ m (S i) = seqZ m i ++ [m + i]. + Lemma seqZ_S m i : seqZ m (Z.of_nat (S i)) = seqZ m (Z.of_nat i) ++ [m + Z.of_nat i]. Proof. unfold seqZ. rewrite !Nat2Z.id, seq_S, fmap_app. simpl. by rewrite Z.add_comm. diff --git a/theories/numbers.v b/theories/numbers.v index 67009522..bce80ceb 100644 --- a/theories/numbers.v +++ b/theories/numbers.v @@ -7,7 +7,6 @@ From stdpp Require Export base decidable option. From stdpp Require Import options. Local Open Scope nat_scope. -Coercion Z.of_nat : nat >-> Z. Global Instance comparison_eq_dec : EqDecision comparison. Proof. solve_decision. Defined. @@ -425,7 +424,7 @@ Global Hint Extern 1000 => lia : zpos. Lemma Z_to_nat_nonpos x : x ≤ 0 → Z.to_nat x = 0%nat. Proof. destruct x; simpl; auto using Z2Nat.inj_neg. by intros []. Qed. -Lemma Z2Nat_inj_pow (x y : nat) : Z.of_nat (x ^ y) = x ^ y. +Lemma Z2Nat_inj_pow (x y : nat) : Z.of_nat (x ^ y) = (Z.of_nat x) ^ (Z.of_nat y). Proof. induction y as [|y IH]; [by rewrite Z.pow_0_r, Nat.pow_0_r|]. by rewrite Nat.pow_succ_r, Nat2Z.inj_succ, Z.pow_succ_r, @@ -443,18 +442,18 @@ Qed. Lemma Z2Nat_divide n m : 0 ≤ n → 0 ≤ m → (Z.to_nat n | Z.to_nat m)%nat ↔ (n | m). Proof. intros. by rewrite <-Nat2Z_divide, !Z2Nat.id by done. Qed. -Lemma Nat2Z_inj_div x y : Z.of_nat (x `div` y) = x `div` y. +Lemma Nat2Z_inj_div x y : Z.of_nat (x `div` y) = (Z.of_nat x) `div` (Z.of_nat y). Proof. destruct (decide (y = 0%nat)); [by subst; destruct x |]. - apply Z.div_unique with (x `mod` y)%nat. + apply Z.div_unique with (Z.of_nat $ x `mod` y)%nat. { left. rewrite <-(Nat2Z.inj_le 0), <-Nat2Z.inj_lt. apply Nat.mod_bound_pos; lia. } by rewrite <-Nat2Z.inj_mul, <-Nat2Z.inj_add, <-Nat.div_mod. Qed. -Lemma Nat2Z_inj_mod x y : Z.of_nat (x `mod` y) = x `mod` y. +Lemma Nat2Z_inj_mod x y : Z.of_nat (x `mod` y) = (Z.of_nat x) `mod` (Z.of_nat y). Proof. destruct (decide (y = 0%nat)); [by subst; destruct x |]. - apply Z.mod_unique with (x `div` y)%nat. + apply Z.mod_unique with (Z.of_nat $ x `div` y)%nat. { left. rewrite <-(Nat2Z.inj_le 0), <-Nat2Z.inj_lt. apply Nat.mod_bound_pos; lia. } by rewrite <-Nat2Z.inj_mul, <-Nat2Z.inj_add, <-Nat.div_mod. @@ -463,7 +462,7 @@ Lemma Z2Nat_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|]. + intros. destruct (decide (y = Z.of_nat 0%nat)); [by subst; destruct x|]. pose proof (Z.div_pos x y). apply (inj Z.of_nat). by rewrite Nat2Z_inj_div, !Z2Nat.id by lia. Qed. @@ -471,7 +470,7 @@ Lemma Z2Nat_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|]. + intros. destruct (decide (y = Z.of_nat 0%nat)); [by subst; destruct x|]. pose proof (Z_mod_pos x y). apply (inj Z.of_nat). by rewrite Nat2Z_inj_mod, !Z2Nat.id by lia. Qed. @@ -1243,13 +1242,13 @@ 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. + Z.to_nat ((Z.of_nat base + Z.of_nat offset) `mod` Z.of_nat 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. + Z.to_nat ((Z.of_nat len + Z.of_nat offset - Z.of_nat base) `mod` Z.of_nat len)%Z. Lemma rotate_nat_add_add_mod base offset len: rotate_nat_add base offset len = @@ -1299,7 +1298,7 @@ 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). + pose proof (Z_mod_lt (Z.of_nat len + Z.of_nat offset - Z.of_nat base) (Z.of_nat len)). apply Nat2Z.inj_lt. rewrite Z2Nat.id; lia. Qed. @@ -1309,7 +1308,8 @@ Lemma rotate_nat_add_sub base 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. + replace (Z.of_nat base + (Z.of_nat len + Z.of_nat offset - Z.of_nat base))%Z + with (Z.of_nat len + Z.of_nat 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. @@ -1320,9 +1320,11 @@ Lemma rotate_nat_sub_add base 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. + assert (∀ n, (Z.of_nat len + n - Z.of_nat base) = ((Z.of_nat len - Z.of_nat 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. + replace (Z.of_nat len - Z.of_nat base + (Z.of_nat base + Z.of_nat offset))%Z with + (Z.of_nat len + Z.of_nat 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. diff --git a/theories/prelude.v b/theories/prelude.v index 9c18d5ee..826a080d 100644 --- a/theories/prelude.v +++ b/theories/prelude.v @@ -13,3 +13,7 @@ From stdpp Require Export list_numbers lexico. From stdpp Require Import options. + +(** We are phasing out this coercion inside std++, but currently +keep it enabled for users to ensure backwards compatibility. *) +Coercion Z.of_nat : nat >-> Z. -- GitLab