Commit 91fae00c authored by Ralf Jung's avatar Ralf Jung
Browse files

make Z.of_nat not a coercion inside the prelude implementation

parent 2d7f0238
......@@ -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.
......
......@@ -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.
......
......@@ -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.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment