Verified Commit 4201c413 authored by Tej Chajed's avatar Tej Chajed
Browse files

Avoid using Arith libraries deprecated in v8.16

parent db60d211
Pipeline #58393 passed with stage
in 12 minutes
......@@ -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] ]};
......
......@@ -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.
......
......@@ -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,8 +3256,9 @@ 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,
resize_all, drop_all, resize_nil by lia.
replace m with (length k + (m - length k)) by lia.
rewrite !resize_plus, resize_all,
drop_all, resize_nil by lia.
auto using Forall2_app, Forall2_replicate_r,
Forall_resize, Forall_drop, resize_length.
Qed.
......@@ -3269,8 +3270,9 @@ 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,
resize_all, drop_all, resize_nil by lia.
replace m with (length l + (m - length l)) by lia.
rewrite !resize_plus, resize_all,
drop_all, resize_nil by lia.
auto using Forall2_app, Forall2_replicate_l,
Forall_resize, Forall_drop, resize_length.
Qed.
......@@ -3318,7 +3320,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 +3654,8 @@ 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.
rewrite lookup_app_r by lia.
by replace (length l1 + j - length l1) with j 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.
......
......@@ -1371,7 +1371,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:
......
......@@ -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. replace m with (n + (m - n)) by lia; 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.
......
Supports Markdown
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