diff --git a/tests/notation.v b/tests/notation.v index 41fe94e9cea8db3335688669f0386d3c196390a7..b1b3df82c80ce8f08a768e8be791365b1f6e7106 100644 --- a/tests/notation.v +++ b/tests/notation.v @@ -18,7 +18,7 @@ Section map_notations. Definition test_4 : M (M nat) := {[ 10 := {[ 10 := 1 ]}; 20 := {[ 20 := 2]}; 30 := {[ 30 := 3]}; 40 := {[ 40 := 4 ]} ]}. - Definition test_op_2 : M (M nat) := {[ 10 := {[pow 10 2 := 99]}; + Definition test_op_2 : M (M nat) := {[ 10 := {[Nat.pow 10 2 := 99]}; 10 + 1 := {[ 10 - 100 := 42 * 1337 ]} ]}. Definition test_op_3 : M (M (list nat)) := {[ 10 := {[ 20 - 2 := [11]; 1 := [22] ]}; @@ -48,4 +48,4 @@ Section multiset_notations. Print test_gmultiset_2. Print test_gmultiset_3. Print test_gmultiset_4. -End multiset_notations. \ No newline at end of file +End multiset_notations. diff --git a/theories/fin_maps.v b/theories/fin_maps.v index b5d8197dc23d328e13ee23bf42ba3f508320a6b9..6cb16d4ea5bf867750440e3962959d8bb18c7164 100644 --- a/theories/fin_maps.v +++ b/theories/fin_maps.v @@ -1156,7 +1156,7 @@ Lemma map_to_list_length {A} (m1 m2 : M A) : Proof. revert m2. induction m1 as [|i x m ? IH] using map_ind. { intros m2 Hm2. rewrite map_to_list_empty. simpl. - apply neq_0_lt. intros Hlen. symmetry in Hlen. + apply Nat.neq_0_lt_0, Nat.neq_sym. intros Hlen. symmetry in Hlen. apply nil_length_inv, map_to_list_empty_iff in Hlen. rewrite Hlen in Hm2. destruct (irreflexivity (⊂) ∅ Hm2). } intros m2 Hm2. diff --git a/theories/list.v b/theories/list.v index a884e8d2d732090937ee93484dea44e8f6b55569..ef0d56691bfaaedc05ea59a8b80f12b2dfc4947b 100644 --- a/theories/list.v +++ b/theories/list.v @@ -1204,13 +1204,13 @@ Proof. revert n. induction l; intros [|?] ?; f_equal/=; auto with lia. Qed. Lemma take_take l n m : take n (take m l) = take (min n m) l. Proof. revert n m. induction l; intros [|?] [|?]; f_equal/=; auto. Qed. Lemma take_idemp l n : take n (take n l) = take n l. -Proof. by rewrite take_take, Min.min_idempotent. Qed. +Proof. by rewrite take_take, Nat.min_id. Qed. Lemma take_length l n : length (take n l) = min n (length l). Proof. revert n. induction l; intros [|?]; f_equal/=; done. Qed. Lemma take_length_le l n : n ≤ length l → length (take n l) = n. -Proof. rewrite take_length. apply Min.min_l. Qed. +Proof. rewrite take_length. apply Nat.min_l. Qed. Lemma take_length_ge l n : length l ≤ n → length (take n l) = length l. -Proof. rewrite take_length. apply Min.min_r. Qed. +Proof. rewrite take_length. apply Nat.min_r. Qed. Lemma take_drop_commute l n m : take n (drop m l) = drop m (take (m + n) l). Proof. revert n m. induction l; intros [|?][|?]; simpl; auto using take_nil with lia. @@ -1483,9 +1483,9 @@ Proof. revert n m. induction l; intros [|?][|?]; f_equal/=; auto using take_replicate. Qed. Lemma take_resize_le l n m x : n ≤ m → take n (resize m x l) = resize n x l. -Proof. intros. by rewrite take_resize, Min.min_l. Qed. +Proof. intros. by rewrite take_resize, Nat.min_l. Qed. Lemma take_resize_eq l n x : take n (resize n x l) = resize n x l. -Proof. intros. by rewrite take_resize, Min.min_l. Qed. +Proof. intros. by rewrite take_resize, Nat.min_l. Qed. Lemma take_resize_plus l n m x : take n (resize (n + m) x l) = resize n x l. Proof. by rewrite take_resize, min_l by lia. Qed. Lemma drop_resize_le l n m x : @@ -1699,7 +1699,7 @@ Proof. repeat match goal with | H : _ ≤ length _ |- _ => rewrite take_length, drop_length in H end; rewrite ?take_drop_commute, ?drop_drop, ?take_take, - ?Min.min_l, Nat.add_assoc by lia; auto with lia. + ?Nat.min_l, Nat.add_assoc by lia; auto with lia. Qed. Lemma sublist_alter_length f l i n k : sublist_lookup i n l = Some k → length (f k) = n → @@ -3256,7 +3256,7 @@ Section Forall2. { rewrite <-(resize_resize l m n) by done. by apply Forall2_resize. } intros. assert (n = length k); subst. { by rewrite <-(Forall2_length (resize n x l) k), resize_length. } - rewrite (le_plus_minus (length k) m), !resize_plus, + rewrite (nat_le_plus_minus (length k) m), !resize_plus, resize_all, drop_all, resize_nil by lia. auto using Forall2_app, Forall2_replicate_r, Forall_resize, Forall_drop, resize_length. @@ -3269,7 +3269,7 @@ Section Forall2. { rewrite <-(resize_resize k m n) by done. by apply Forall2_resize. } assert (n = length l); subst. { by rewrite (Forall2_length l (resize n y k)), resize_length. } - rewrite (le_plus_minus (length l) m), !resize_plus, + rewrite (nat_le_plus_minus (length l) m), !resize_plus, resize_all, drop_all, resize_nil by lia. auto using Forall2_app, Forall2_replicate_l, Forall_resize, Forall_drop, resize_length. @@ -3318,7 +3318,7 @@ Section Forall2. apply Forall2_app_l; rewrite ?take_length_le by lia; auto using Forall2_take. apply Forall2_app_l; erewrite Forall2_length, take_length, - drop_length, <-Forall2_length, Min.min_l by eauto with lia; [done|]. + drop_length, <-Forall2_length, Nat.min_l by eauto with lia; [done|]. rewrite drop_drop; auto using Forall2_drop. Qed. @@ -3652,7 +3652,7 @@ Section find. naive_solver eauto using lookup_app_l_Some with lia. } apply list_find_Some. split_and!; [done..|]. intros j z ??. eapply (Hleast (length l1 + j)); [|lia]. - by rewrite lookup_app_r, minus_plus by lia. + by rewrite lookup_app_r, nat_minus_plus by lia. - intros [(?&?&Hleast)%list_find_Some|(?&Hl1&(?&?&Hleast)%list_find_Some)]. + apply list_find_Some. split_and!; [by auto using lookup_app_l_Some..|]. assert (i < length l1) by eauto using lookup_lt_Some. diff --git a/theories/numbers.v b/theories/numbers.v index 4acc4adf9dc0a68ba9a8e1de202a109041294494..4f72314302e0bfea69cae39fd9fda484d4e258cc 100644 --- a/theories/numbers.v +++ b/theories/numbers.v @@ -65,6 +65,13 @@ Proof. unfold lt. apply _. Qed. Lemma nat_le_sum (x y : nat) : x ≤ y ↔ ∃ z, y = x + z. Proof. split; [exists (y - x); lia | intros [z ->]; lia]. Qed. +(** [Arith.Minus.minus_plus] is deprecated starting in 8.16 *) +Lemma nat_minus_plus n m : n + m - n = m. +Proof. lia. Qed. +(** [Arith.Minus.le_plus_minus] is deprecated starting in 8.16 *) +Lemma nat_le_plus_minus n m : n ≤ m → m = n + (m - n). +Proof. lia. Qed. + Lemma Nat_lt_succ_succ n : n < S (S n). Proof. auto with arith. Qed. Lemma Nat_mul_split_l n x1 x2 y1 y2 : @@ -1371,7 +1378,7 @@ Lemma rotate_nat_add_add base offset len n: Proof. intros ?. unfold rotate_nat_add. rewrite !Z2Nat_inj_mod, !Z2Nat.inj_add, !Nat2Z.id by lia. - by rewrite plus_assoc, Nat.add_mod_idemp_l by lia. + by rewrite Nat.add_assoc, Nat.add_mod_idemp_l by lia. Qed. Lemma rotate_nat_add_S base offset len: diff --git a/theories/relations.v b/theories/relations.v index 3403317828aa1170e807642e277179f733e04028..c09ae6b9c940961879d4f7a7cee513d3cb9a7a82 100644 --- a/theories/relations.v +++ b/theories/relations.v @@ -177,7 +177,7 @@ Section general. Lemma bsteps_weaken n m x y : n ≤ m → bsteps R n x y → bsteps R m x y. Proof. - intros. rewrite (Minus.le_plus_minus n m); auto using bsteps_plus_r. + intros. rewrite (nat_le_plus_minus n m); auto using bsteps_plus_r. Qed. Lemma bsteps_plus_l n m x y : bsteps R n x y → bsteps R (m + n) x y.