From aba0e740f25ffa5c338dfa76cab71144802cebc2 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sun, 21 Jun 2020 18:22:00 +0200 Subject: Replace `omega` tactic with `lia` Since Coq 8.12, `omega` is flagged as deprecated and scheduled for removal. Also replace CompCert's homemade tactics `omegaContradiction`, `xomega`, and `xomegaContradiction` with `lia` and `extlia`. Turn back on the deprecation warning for uses of `omega`. Make the proof of `Ctypes.sizeof_pos` more robust to variations in `lia`. --- common/AST.v | 6 +- common/Events.v | 54 ++++----- common/Globalenvs.v | 72 +++++------ common/Linking.v | 2 +- common/Memdata.v | 62 +++++----- common/Memory.v | 338 ++++++++++++++++++++++++++-------------------------- common/Separation.v | 66 +++++----- common/Smallstep.v | 20 ++-- common/Subtyping.v | 56 ++++----- common/Switch.v | 38 +++--- common/Unityping.v | 16 +-- common/Values.v | 34 +++--- 12 files changed, 382 insertions(+), 382 deletions(-) (limited to 'common') diff --git a/common/AST.v b/common/AST.v index 4f954c5c..7ccbb6cc 100644 --- a/common/AST.v +++ b/common/AST.v @@ -61,7 +61,7 @@ Definition typesize (ty: typ) : Z := end. Lemma typesize_pos: forall ty, typesize ty > 0. -Proof. destruct ty; simpl; omega. Qed. +Proof. destruct ty; simpl; lia. Qed. Lemma typesize_Tptr: typesize Tptr = if Archi.ptr64 then 8 else 4. Proof. unfold Tptr; destruct Archi.ptr64; auto. Qed. @@ -265,13 +265,13 @@ Fixpoint init_data_list_size (il: list init_data) {struct il} : Z := Lemma init_data_size_pos: forall i, init_data_size i >= 0. Proof. - destruct i; simpl; try xomega. destruct Archi.ptr64; omega. + destruct i; simpl; try extlia. destruct Archi.ptr64; lia. Qed. Lemma init_data_list_size_pos: forall il, init_data_list_size il >= 0. Proof. - induction il; simpl. omega. generalize (init_data_size_pos a); omega. + induction il; simpl. lia. generalize (init_data_size_pos a); lia. Qed. (** Information attached to global variables. *) diff --git a/common/Events.v b/common/Events.v index 28bb992a..ee2d529d 100644 --- a/common/Events.v +++ b/common/Events.v @@ -798,7 +798,7 @@ Proof. exists f; exists v'; exists m1'; intuition. constructor; auto. red; intros. congruence. (* trace length *) -- inv H; inv H0; simpl; omega. +- inv H; inv H0; simpl; lia. (* receptive *) - inv H. exploit volatile_load_receptive; eauto. intros [v2 A]. exists v2; exists m1; constructor; auto. @@ -925,7 +925,7 @@ Proof. eelim H3; eauto. exploit Mem.store_valid_access_3. eexact H0. intros [X Y]. apply Mem.perm_cur_max. apply Mem.perm_implies with Writable; auto with mem. - apply X. omega. + apply X. lia. Qed. Lemma volatile_store_receptive: @@ -960,7 +960,7 @@ Proof. exploit volatile_store_inject; eauto. intros [m2' [A [B [C D]]]]. exists f; exists Vundef; exists m2'; intuition. constructor; auto. red; intros; congruence. (* trace length *) -- inv H; inv H0; simpl; omega. +- inv H; inv H0; simpl; lia. (* receptive *) - assert (t1 = t2). inv H. eapply volatile_store_receptive; eauto. subst t2; exists vres1; exists m1; auto. @@ -1042,7 +1042,7 @@ Proof. subst b1. rewrite C in H2. inv H2. eauto with mem. rewrite D in H2 by auto. congruence. (* trace length *) -- inv H; simpl; omega. +- inv H; simpl; lia. (* receptive *) - assert (t1 = t2). inv H; inv H0; auto. subst t2. exists vres1; exists m1; auto. @@ -1122,21 +1122,21 @@ Proof. exploit Mem.address_inject; eauto. apply Mem.perm_implies with Freeable; auto with mem. apply P. instantiate (1 := lo). - generalize (size_chunk_pos Mptr); omega. + generalize (size_chunk_pos Mptr); lia. intro EQ. exploit Mem.free_parallel_inject; eauto. intros (m2' & C & D). exists f, Vundef, m2'; split. apply extcall_free_sem_ptr with (sz := sz) (m' := m2'). - rewrite EQ. rewrite <- A. f_equal. omega. + rewrite EQ. rewrite <- A. f_equal. lia. auto. auto. - rewrite ! EQ. rewrite <- C. f_equal; omega. + rewrite ! EQ. rewrite <- C. f_equal; lia. split. auto. split. auto. split. eapply Mem.free_unchanged_on; eauto. unfold loc_unmapped. intros; congruence. split. eapply Mem.free_unchanged_on; eauto. unfold loc_out_of_reach. intros. red; intros. eelim H2; eauto. apply Mem.perm_cur_max. apply Mem.perm_implies with Freeable; auto with mem. - apply P. omega. + apply P. lia. split. auto. red; intros. congruence. + inv H2. inv H6. replace v' with Vnullptr. @@ -1145,7 +1145,7 @@ Proof. red; intros; congruence. unfold Vnullptr in *; destruct Archi.ptr64; inv H4; auto. (* trace length *) -- inv H; simpl; omega. +- inv H; simpl; lia. (* receptive *) - assert (t1 = t2) by (inv H; inv H0; auto). subst t2. exists vres1; exists m1; auto. @@ -1217,23 +1217,23 @@ Proof. destruct (zeq sz 0). + (* special case sz = 0 *) assert (bytes = nil). - { exploit (Mem.loadbytes_empty m1 bsrc (Ptrofs.unsigned osrc) sz). omega. congruence. } + { exploit (Mem.loadbytes_empty m1 bsrc (Ptrofs.unsigned osrc) sz). lia. congruence. } subst. destruct (Mem.range_perm_storebytes m1' b0 (Ptrofs.unsigned (Ptrofs.add odst (Ptrofs.repr delta0))) nil) as [m2' SB]. - simpl. red; intros; omegaContradiction. + simpl. red; intros; extlia. exists f, Vundef, m2'. split. econstructor; eauto. - intros; omegaContradiction. - intros; omegaContradiction. - right; omega. - apply Mem.loadbytes_empty. omega. + intros; extlia. + intros; extlia. + right; lia. + apply Mem.loadbytes_empty. lia. split. auto. split. eapply Mem.storebytes_empty_inject; eauto. split. eapply Mem.storebytes_unchanged_on; eauto. unfold loc_unmapped; intros. congruence. split. eapply Mem.storebytes_unchanged_on; eauto. - simpl; intros; omegaContradiction. + simpl; intros; extlia. split. apply inject_incr_refl. red; intros; congruence. + (* general case sz > 0 *) @@ -1243,11 +1243,11 @@ Proof. assert (RPDST: Mem.range_perm m1 bdst (Ptrofs.unsigned odst) (Ptrofs.unsigned odst + sz) Cur Nonempty). replace sz with (Z.of_nat (length bytes)). eapply Mem.range_perm_implies. eapply Mem.storebytes_range_perm; eauto. auto with mem. - rewrite LEN. apply Z2Nat.id. omega. + rewrite LEN. apply Z2Nat.id. lia. assert (PSRC: Mem.perm m1 bsrc (Ptrofs.unsigned osrc) Cur Nonempty). - apply RPSRC. omega. + apply RPSRC. lia. assert (PDST: Mem.perm m1 bdst (Ptrofs.unsigned odst) Cur Nonempty). - apply RPDST. omega. + apply RPDST. lia. exploit Mem.address_inject. eauto. eexact PSRC. eauto. intros EQ1. exploit Mem.address_inject. eauto. eexact PDST. eauto. intros EQ2. exploit Mem.loadbytes_inject; eauto. intros [bytes2 [A B]]. @@ -1258,7 +1258,7 @@ Proof. intros; eapply Mem.aligned_area_inject with (m := m1); eauto. eapply Mem.disjoint_or_equal_inject with (m := m1); eauto. apply Mem.range_perm_max with Cur; auto. - apply Mem.range_perm_max with Cur; auto. omega. + apply Mem.range_perm_max with Cur; auto. lia. split. constructor. split. auto. split. eapply Mem.storebytes_unchanged_on; eauto. unfold loc_unmapped; intros. @@ -1268,11 +1268,11 @@ Proof. apply Mem.perm_cur_max. apply Mem.perm_implies with Writable; auto with mem. eapply Mem.storebytes_range_perm; eauto. erewrite list_forall2_length; eauto. - omega. + lia. split. apply inject_incr_refl. red; intros; congruence. - (* trace length *) - intros; inv H. simpl; omega. + intros; inv H. simpl; lia. - (* receptive *) intros. assert (t1 = t2). inv H; inv H0; auto. subst t2. @@ -1318,7 +1318,7 @@ Proof. eapply eventval_list_match_inject; eauto. red; intros; congruence. (* trace length *) -- inv H; simpl; omega. +- inv H; simpl; lia. (* receptive *) - assert (t1 = t2). inv H; inv H0; auto. exists vres1; exists m1; congruence. @@ -1363,7 +1363,7 @@ Proof. eapply eventval_match_inject; eauto. red; intros; congruence. (* trace length *) -- inv H; simpl; omega. +- inv H; simpl; lia. (* receptive *) - assert (t1 = t2). inv H; inv H0; auto. subst t2. exists vres1; exists m1; auto. @@ -1404,7 +1404,7 @@ Proof. econstructor; eauto. red; intros; congruence. (* trace length *) -- inv H; simpl; omega. +- inv H; simpl; lia. (* receptive *) - inv H; inv H0. exists Vundef, m1; constructor. (* determ *) @@ -1458,7 +1458,7 @@ Proof. constructor; auto. red; intros; congruence. (* trace length *) -- inv H; simpl; omega. +- inv H; simpl; lia. (* receptive *) - inv H; inv H0. exists vres1, m1; constructor; auto. (* determ *) @@ -1582,7 +1582,7 @@ Proof. intros. destruct (plt (Mem.nextblock m2) (Mem.nextblock m1)). exploit external_call_valid_block; eauto. intros. eelim Plt_strict; eauto. - unfold Plt, Ple in *; zify; omega. + unfold Plt, Ple in *; zify; lia. Qed. (** Special case of [external_call_mem_inject_gen] (for backward compatibility) *) diff --git a/common/Globalenvs.v b/common/Globalenvs.v index d37fbd46..40496044 100644 --- a/common/Globalenvs.v +++ b/common/Globalenvs.v @@ -55,7 +55,7 @@ Function store_zeros (m: mem) (b: block) (p: Z) (n: Z) {wf (Zwf 0) n}: option me | None => None end. Proof. - intros. red. omega. + intros. red. lia. apply Zwf_well_founded. Qed. @@ -849,8 +849,8 @@ Proof. intros until n. functional induction (store_zeros m b p n); intros. - inv H; apply Mem.unchanged_on_refl. - apply Mem.unchanged_on_trans with m'. -+ eapply Mem.store_unchanged_on; eauto. simpl. intros. apply H0. omega. -+ apply IHo; auto. intros; apply H0; omega. ++ eapply Mem.store_unchanged_on; eauto. simpl. intros. apply H0. lia. ++ apply IHo; auto. intros; apply H0; lia. - discriminate. Qed. @@ -879,7 +879,7 @@ Proof. - destruct (store_init_data m b p a) as [m1|] eqn:?; try congruence. apply Mem.unchanged_on_trans with m1. eapply store_init_data_unchanged; eauto. intros; apply H0; tauto. - eapply IHil; eauto. intros; apply H0. generalize (init_data_size_pos a); omega. + eapply IHil; eauto. intros; apply H0. generalize (init_data_size_pos a); lia. Qed. (** Properties related to [loadbytes] *) @@ -895,24 +895,24 @@ Lemma store_zeros_loadbytes: readbytes_as_zero m' b p n. Proof. intros until n; functional induction (store_zeros m b p n); red; intros. -- destruct n0. simpl. apply Mem.loadbytes_empty. omega. - rewrite Nat2Z.inj_succ in H1. omegaContradiction. +- destruct n0. simpl. apply Mem.loadbytes_empty. lia. + rewrite Nat2Z.inj_succ in H1. extlia. - destruct (zeq p0 p). - + subst p0. destruct n0. simpl. apply Mem.loadbytes_empty. omega. + + subst p0. destruct n0. simpl. apply Mem.loadbytes_empty. lia. rewrite Nat2Z.inj_succ in H1. rewrite Nat2Z.inj_succ. - replace (Z.succ (Z.of_nat n0)) with (1 + Z.of_nat n0) by omega. + replace (Z.succ (Z.of_nat n0)) with (1 + Z.of_nat n0) by lia. change (list_repeat (S n0) (Byte Byte.zero)) with ((Byte Byte.zero :: nil) ++ list_repeat n0 (Byte Byte.zero)). apply Mem.loadbytes_concat. eapply Mem.loadbytes_unchanged_on with (P := fun b1 ofs1 => ofs1 = p). - eapply store_zeros_unchanged; eauto. intros; omega. - intros; omega. + eapply store_zeros_unchanged; eauto. intros; lia. + intros; lia. replace (Byte Byte.zero :: nil) with (encode_val Mint8unsigned Vzero). change 1 with (size_chunk Mint8unsigned). eapply Mem.loadbytes_store_same; eauto. unfold encode_val; unfold encode_int; unfold rev_if_be; destruct Archi.big_endian; reflexivity. - eapply IHo; eauto. omega. omega. omega. omega. - + eapply IHo; eauto. omega. omega. + eapply IHo; eauto. lia. lia. lia. lia. + + eapply IHo; eauto. lia. lia. - discriminate. Qed. @@ -947,8 +947,8 @@ Proof. intros; destruct i; simpl in H; try apply (Mem.loadbytes_store_same _ _ _ _ _ _ H). - inv H. simpl. assert (EQ: Z.of_nat (Z.to_nat z) = Z.max z 0). - { destruct (zle 0 z). rewrite Z2Nat.id; xomega. destruct z; try discriminate. simpl. xomega. } - rewrite <- EQ. apply H0. omega. simpl. omega. + { destruct (zle 0 z). rewrite Z2Nat.id; extlia. destruct z; try discriminate. simpl. extlia. } + rewrite <- EQ. apply H0. lia. simpl. lia. - rewrite init_data_size_addrof. simpl. destruct (find_symbol ge i) as [b'|]; try discriminate. rewrite (Mem.loadbytes_store_same _ _ _ _ _ _ H). @@ -968,23 +968,23 @@ Lemma store_init_data_list_loadbytes: Mem.loadbytes m' b p (init_data_list_size il) = Some (bytes_of_init_data_list il). Proof. induction il as [ | i1 il]; simpl; intros. -- apply Mem.loadbytes_empty. omega. +- apply Mem.loadbytes_empty. lia. - generalize (init_data_size_pos i1) (init_data_list_size_pos il); intros P1 PL. destruct (store_init_data m b p i1) as [m1|] eqn:S; try discriminate. apply Mem.loadbytes_concat. eapply Mem.loadbytes_unchanged_on with (P := fun b1 ofs1 => ofs1 < p + init_data_size i1). eapply store_init_data_list_unchanged; eauto. - intros; omega. - intros; omega. + intros; lia. + intros; lia. eapply store_init_data_loadbytes; eauto. - red; intros; apply H0. omega. omega. + red; intros; apply H0. lia. lia. apply IHil with m1; auto. red; intros. eapply Mem.loadbytes_unchanged_on with (P := fun b1 ofs1 => p + init_data_size i1 <= ofs1). eapply store_init_data_unchanged; eauto. - intros; omega. - intros; omega. - apply H0. omega. omega. + intros; lia. + intros; lia. + apply H0. lia. lia. auto. auto. Qed. @@ -1011,7 +1011,7 @@ Remark read_as_zero_unchanged: read_as_zero m' b ofs len. Proof. intros; red; intros. eapply Mem.load_unchanged_on; eauto. - intros; apply H1. omega. + intros; apply H1. lia. Qed. Lemma store_zeros_read_as_zero: @@ -1068,7 +1068,7 @@ Proof. { intros. eapply Mem.load_unchanged_on with (P := fun b' ofs' => ofs' < p + size_chunk chunk). - eapply store_init_data_list_unchanged; eauto. intros; omega. + eapply store_init_data_list_unchanged; eauto. intros; lia. intros; tauto. eapply Mem.load_store_same; eauto. } @@ -1078,10 +1078,10 @@ Proof. exploit IHil; eauto. set (P := fun (b': block) ofs' => p + init_data_size a <= ofs'). apply read_as_zero_unchanged with (m := m) (P := P). - red; intros; apply H0; auto. generalize (init_data_size_pos a); omega. omega. + red; intros; apply H0; auto. generalize (init_data_size_pos a); lia. lia. eapply store_init_data_unchanged with (P := P); eauto. - intros; unfold P. omega. - intros; unfold P. omega. + intros; unfold P. lia. + intros; unfold P. lia. intro D. destruct a; simpl in Heqo. + split; auto. eapply (A Mint8unsigned (Vint i)); eauto. @@ -1093,10 +1093,10 @@ Proof. + split; auto. set (P := fun (b': block) ofs' => ofs' < p + init_data_size (Init_space z)). inv Heqo. apply read_as_zero_unchanged with (m := m1) (P := P). - red; intros. apply H0; auto. simpl. generalize (init_data_list_size_pos il); xomega. + red; intros. apply H0; auto. simpl. generalize (init_data_list_size_pos il); extlia. eapply store_init_data_list_unchanged; eauto. - intros; unfold P. omega. - intros; unfold P. simpl; xomega. + intros; unfold P. lia. + intros; unfold P. simpl; extlia. + rewrite init_data_size_addrof in *. split; auto. destruct (find_symbol ge i); try congruence. @@ -1195,11 +1195,11 @@ Proof. * destruct (Mem.alloc m 0 1) as [m1 b] eqn:ALLOC. exploit Mem.alloc_result; eauto. intros RES. rewrite H, <- RES. split. - eapply Mem.perm_drop_1; eauto. omega. + eapply Mem.perm_drop_1; eauto. lia. intros. assert (0 <= ofs < 1). { eapply Mem.perm_alloc_3; eauto. eapply Mem.perm_drop_4; eauto. } exploit Mem.perm_drop_2; eauto. intros ORD. - split. omega. inv ORD; auto. + split. lia. inv ORD; auto. * set (init := gvar_init v) in *. set (sz := init_data_list_size init) in *. destruct (Mem.alloc m 0 sz) as [m1 b] eqn:?. @@ -1442,7 +1442,7 @@ Proof. exploit alloc_global_neutral; eauto. assert (Ple (Pos.succ (Mem.nextblock m)) (Mem.nextblock m')). { rewrite EQ. apply advance_next_le. } - unfold Plt, Ple in *; zify; omega. + unfold Plt, Ple in *; zify; lia. Qed. End INITMEM_INJ. @@ -1563,9 +1563,9 @@ Lemma store_zeros_exists: Proof. intros until n. functional induction (store_zeros m b p n); intros PERM. - exists m; auto. -- apply IHo. red; intros. eapply Mem.perm_store_1; eauto. apply PERM. omega. +- apply IHo. red; intros. eapply Mem.perm_store_1; eauto. apply PERM. lia. - destruct (Mem.valid_access_store m Mint8unsigned b p Vzero) as (m' & STORE). - split. red; intros. apply Mem.perm_cur. apply PERM. simpl in H. omega. + split. red; intros. apply Mem.perm_cur. apply PERM. simpl in H. lia. simpl. apply Z.divide_1_l. congruence. Qed. @@ -1603,10 +1603,10 @@ Proof. - exists m; auto. - destruct H0. destruct (@store_init_data_exists m b p i1) as (m1 & S1); eauto. - red; intros. apply H. generalize (init_data_list_size_pos il); omega. + red; intros. apply H. generalize (init_data_list_size_pos il); lia. rewrite S1. apply IHil; eauto. - red; intros. erewrite <- store_init_data_perm by eauto. apply H. generalize (init_data_size_pos i1); omega. + red; intros. erewrite <- store_init_data_perm by eauto. apply H. generalize (init_data_size_pos i1); lia. Qed. Lemma alloc_global_exists: diff --git a/common/Linking.v b/common/Linking.v index ec828ea4..a5cf0a4a 100644 --- a/common/Linking.v +++ b/common/Linking.v @@ -123,7 +123,7 @@ Defined. Next Obligation. inv H; inv H0; constructor; auto. congruence. - simpl. generalize (init_data_list_size_pos z). xomega. + simpl. generalize (init_data_list_size_pos z). extlia. Defined. Next Obligation. revert H; unfold link_varinit. diff --git a/common/Memdata.v b/common/Memdata.v index f3016efe..05a3d4ed 100644 --- a/common/Memdata.v +++ b/common/Memdata.v @@ -47,7 +47,7 @@ Definition size_chunk (chunk: memory_chunk) : Z := Lemma size_chunk_pos: forall chunk, size_chunk chunk > 0. Proof. - intros. destruct chunk; simpl; omega. + intros. destruct chunk; simpl; lia. Qed. Definition size_chunk_nat (chunk: memory_chunk) : nat := @@ -65,7 +65,7 @@ Proof. intros. generalize (size_chunk_pos chunk). rewrite size_chunk_conv. destruct (size_chunk_nat chunk). - simpl; intros; omegaContradiction. + simpl; intros; extlia. intros; exists n; auto. Qed. @@ -101,7 +101,7 @@ Definition align_chunk (chunk: memory_chunk) : Z := Lemma align_chunk_pos: forall chunk, align_chunk chunk > 0. Proof. - intro. destruct chunk; simpl; omega. + intro. destruct chunk; simpl; lia. Qed. Lemma align_chunk_Mptr: align_chunk Mptr = if Archi.ptr64 then 8 else 4. @@ -120,7 +120,7 @@ Lemma align_le_divides: align_chunk chunk1 <= align_chunk chunk2 -> (align_chunk chunk1 | align_chunk chunk2). Proof. intros. destruct chunk1; destruct chunk2; simpl in *; - solve [ omegaContradiction + solve [ extlia | apply Z.divide_refl | exists 2; reflexivity | exists 4; reflexivity @@ -216,12 +216,12 @@ Proof. simpl. rewrite Zmod_1_r. auto. Opaque Byte.wordsize. rewrite Nat2Z.inj_succ. simpl. - replace (Z.succ (Z.of_nat n) * 8) with (Z.of_nat n * 8 + 8) by omega. - rewrite two_p_is_exp; try omega. + replace (Z.succ (Z.of_nat n) * 8) with (Z.of_nat n * 8 + 8) by lia. + rewrite two_p_is_exp; try lia. rewrite Zmod_recombine. rewrite IHn. rewrite Z.add_comm. change (Byte.unsigned (Byte.repr x)) with (Byte.Z_mod_modulus x). rewrite Byte.Z_mod_modulus_eq. reflexivity. - apply two_p_gt_ZERO. omega. apply two_p_gt_ZERO. omega. + apply two_p_gt_ZERO. lia. apply two_p_gt_ZERO. lia. Qed. Lemma rev_if_be_involutive: @@ -280,15 +280,15 @@ Proof. intros; simpl; auto. intros until y. rewrite Nat2Z.inj_succ. - replace (Z.succ (Z.of_nat n) * 8) with (Z.of_nat n * 8 + 8) by omega. - rewrite two_p_is_exp; try omega. + replace (Z.succ (Z.of_nat n) * 8) with (Z.of_nat n * 8 + 8) by lia. + rewrite two_p_is_exp; try lia. intro EQM. simpl; decEq. apply Byte.eqm_samerepr. red. eapply eqmod_divides; eauto. apply Z.divide_factor_r. apply IHn. destruct EQM as [k EQ]. exists k. rewrite EQ. - rewrite <- Z_div_plus_full_l. decEq. change (two_p 8) with 256. ring. omega. + rewrite <- Z_div_plus_full_l. decEq. change (two_p 8) with 256. ring. lia. Qed. Lemma encode_int_8_mod: @@ -517,9 +517,9 @@ Ltac solve_decode_encode_val_general := | |- context [ Int.repr(decode_int (encode_int 2 (Int.unsigned _))) ] => rewrite decode_encode_int_2 | |- context [ Int.repr(decode_int (encode_int 4 (Int.unsigned _))) ] => rewrite decode_encode_int_4 | |- context [ Int64.repr(decode_int (encode_int 8 (Int64.unsigned _))) ] => rewrite decode_encode_int_8 - | |- Vint (Int.sign_ext _ (Int.sign_ext _ _)) = Vint _ => f_equal; apply Int.sign_ext_idem; omega - | |- Vint (Int.zero_ext _ (Int.zero_ext _ _)) = Vint _ => f_equal; apply Int.zero_ext_idem; omega - | |- Vint (Int.sign_ext _ (Int.zero_ext _ _)) = Vint _ => f_equal; apply Int.sign_ext_zero_ext; omega + | |- Vint (Int.sign_ext _ (Int.sign_ext _ _)) = Vint _ => f_equal; apply Int.sign_ext_idem; lia + | |- Vint (Int.zero_ext _ (Int.zero_ext _ _)) = Vint _ => f_equal; apply Int.zero_ext_idem; lia + | |- Vint (Int.sign_ext _ (Int.zero_ext _ _)) = Vint _ => f_equal; apply Int.sign_ext_zero_ext; lia end. Lemma decode_encode_val_general: @@ -543,7 +543,7 @@ Lemma decode_encode_val_similar: v2 = Val.load_result chunk2 v1. Proof. intros until v2; intros TY SZ DE. - destruct chunk1; destruct chunk2; simpl in TY; try discriminate; simpl in SZ; try omegaContradiction; + destruct chunk1; destruct chunk2; simpl in TY; try discriminate; simpl in SZ; try extlia; destruct v1; auto. Qed. @@ -553,7 +553,7 @@ Lemma decode_val_rettype: Proof. intros. unfold decode_val. destruct (proj_bytes cl). -- destruct chunk; simpl; rewrite ? Int.sign_ext_idem, ? Int.zero_ext_idem by omega; auto. +- destruct chunk; simpl; rewrite ? Int.sign_ext_idem, ? Int.zero_ext_idem by lia; auto. - Local Opaque Val.load_result. destruct chunk; simpl; (exact I || apply Val.load_result_type || destruct Archi.ptr64; (exact I || apply Val.load_result_type)). @@ -653,7 +653,7 @@ Proof. exists j, mv = Fragment v q j /\ S j <> size_quantity_nat q). { induction n; simpl; intros. contradiction. destruct H0. - exists n; split; auto. omega. apply IHn; auto. omega. + exists n; split; auto. lia. apply IHn; auto. lia. } assert (B: forall q, q = quantity_chunk chunk -> @@ -663,7 +663,7 @@ Proof. Local Transparent inj_value. intros. unfold inj_value. destruct (size_quantity_nat_pos q) as [sz' EQ']. rewrite EQ'. simpl. constructor; auto. - intros; eapply A; eauto. omega. + intros; eapply A; eauto. lia. } assert (C: forall bl, match v with Vint _ => True | Vlong _ => True | Vfloat _ => True | Vsingle _ => True | _ => False end -> @@ -719,8 +719,8 @@ Proof. induction n; destruct mvs; simpl; intros; try discriminate. contradiction. destruct m; try discriminate. InvBooleans. apply beq_nat_true in H4. subst. - destruct H0. subst mv. exists n0; split; auto. omega. - eapply IHn; eauto. omega. + destruct H0. subst mv. exists n0; split; auto. lia. + eapply IHn; eauto. lia. } assert (U: forall mvs, shape_decoding chunk mvs (Val.load_result chunk Vundef)). { @@ -740,7 +740,7 @@ Proof. simpl. apply beq_nat_true in EQN. subst n q0. constructor. auto. destruct H0 as [E|[E|[E|E]]]; subst chunk; destruct q; auto || discriminate. congruence. - intros. eapply B; eauto. omega. + intros. eapply B; eauto. lia. } unfold decode_val. destruct (proj_bytes (mv1 :: mvl)) as [bl|] eqn:PB. @@ -955,22 +955,22 @@ Proof. induction l1; simpl int_of_bytes; intros. simpl. ring. simpl length. rewrite Nat2Z.inj_succ. - replace (Z.succ (Z.of_nat (length l1)) * 8) with (Z.of_nat (length l1) * 8 + 8) by omega. + replace (Z.succ (Z.of_nat (length l1)) * 8) with (Z.of_nat (length l1) * 8 + 8) by lia. rewrite two_p_is_exp. change (two_p 8) with 256. rewrite IHl1. ring. - omega. omega. + lia. lia. Qed. Lemma int_of_bytes_range: forall l, 0 <= int_of_bytes l < two_p (Z.of_nat (length l) * 8). Proof. induction l; intros. - simpl. omega. + simpl. lia. simpl length. rewrite Nat2Z.inj_succ. - replace (Z.succ (Z.of_nat (length l)) * 8) with (Z.of_nat (length l) * 8 + 8) by omega. + replace (Z.succ (Z.of_nat (length l)) * 8) with (Z.of_nat (length l) * 8 + 8) by lia. rewrite two_p_is_exp. change (two_p 8) with 256. simpl int_of_bytes. generalize (Byte.unsigned_range a). - change Byte.modulus with 256. omega. - omega. omega. + change Byte.modulus with 256. lia. + lia. lia. Qed. Lemma length_proj_bytes: @@ -1014,7 +1014,7 @@ Proof. intros. apply Int.unsigned_repr. generalize (int_of_bytes_range l). rewrite H2. change (two_p (Z.of_nat 4 * 8)) with (Int.max_unsigned + 1). - omega. + lia. apply Val.lessdef_same. unfold decode_int, rev_if_be. destruct Archi.big_endian; rewrite B1; rewrite B2. + rewrite <- (rev_length b1) in L1. @@ -1036,18 +1036,18 @@ Lemma bytes_of_int_append: bytes_of_int n1 x1 ++ bytes_of_int n2 x2. Proof. induction n1; intros. -- simpl in *. f_equal. omega. +- simpl in *. f_equal. lia. - assert (E: two_p (Z.of_nat (S n1) * 8) = two_p (Z.of_nat n1 * 8) * 256). { rewrite Nat2Z.inj_succ. change 256 with (two_p 8). rewrite <- two_p_is_exp. - f_equal. omega. omega. omega. + f_equal. lia. lia. lia. } rewrite E in *. simpl. f_equal. apply Byte.eqm_samerepr. exists (x2 * two_p (Z.of_nat n1 * 8)). change Byte.modulus with 256. ring. rewrite Z.mul_assoc. rewrite Z_div_plus. apply IHn1. - apply Zdiv_interval_1. omega. apply two_p_gt_ZERO; omega. omega. - assumption. omega. + apply Zdiv_interval_1. lia. apply two_p_gt_ZERO; lia. lia. + assumption. lia. Qed. Lemma bytes_of_int64: diff --git a/common/Memory.v b/common/Memory.v index 9f9934c2..641a9243 100644 --- a/common/Memory.v +++ b/common/Memory.v @@ -208,11 +208,11 @@ Proof. induction lo using (well_founded_induction_type (Zwf_up_well_founded hi)). destruct (zlt lo hi). destruct (perm_dec m b lo k p). - destruct (H (lo + 1)). red. omega. - left; red; intros. destruct (zeq lo ofs). congruence. apply r. omega. - right; red; intros. elim n. red; intros; apply H0; omega. - right; red; intros. elim n. apply H0. omega. - left; red; intros. omegaContradiction. + destruct (H (lo + 1)). red. lia. + left; red; intros. destruct (zeq lo ofs). congruence. apply r. lia. + right; red; intros. elim n. red; intros; apply H0; lia. + right; red; intros. elim n. apply H0. lia. + left; red; intros. extlia. Defined. (** [valid_access m chunk b ofs p] holds if a memory access @@ -253,7 +253,7 @@ Theorem valid_access_valid_block: Proof. intros. destruct H. assert (perm m b ofs Cur Nonempty). - apply H. generalize (size_chunk_pos chunk). omega. + apply H. generalize (size_chunk_pos chunk). lia. eauto with mem. Qed. @@ -264,7 +264,7 @@ Lemma valid_access_perm: valid_access m chunk b ofs p -> perm m b ofs k p. Proof. - intros. destruct H. apply perm_cur. apply H. generalize (size_chunk_pos chunk). omega. + intros. destruct H. apply perm_cur. apply H. generalize (size_chunk_pos chunk). lia. Qed. Lemma valid_access_compat: @@ -310,9 +310,9 @@ Theorem valid_pointer_valid_access: Proof. intros. rewrite valid_pointer_nonempty_perm. split; intros. - split. simpl; red; intros. replace ofs0 with ofs by omega. auto. + split. simpl; red; intros. replace ofs0 with ofs by lia. auto. simpl. apply Z.divide_1_l. - destruct H. apply H. simpl. omega. + destruct H. apply H. simpl. lia. Qed. (** C allows pointers one past the last element of an array. These are not @@ -482,8 +482,8 @@ Proof. auto. simpl length in H. rewrite Nat2Z.inj_succ in H. transitivity (ZMap.get q (ZMap.set p a c)). - apply IHvl. intros. apply H. omega. - apply ZMap.gso. apply not_eq_sym. apply H. omega. + apply IHvl. intros. apply H. lia. + apply ZMap.gso. apply not_eq_sym. apply H. lia. Qed. Remark setN_outside: @@ -492,7 +492,7 @@ Remark setN_outside: ZMap.get q (setN vl p c) = ZMap.get q c. Proof. intros. apply setN_other. - intros. omega. + intros. lia. Qed. Remark getN_setN_same: @@ -502,7 +502,7 @@ Proof. induction vl; intros; simpl. auto. decEq. - rewrite setN_outside. apply ZMap.gss. omega. + rewrite setN_outside. apply ZMap.gss. lia. apply IHvl. Qed. @@ -512,7 +512,7 @@ Remark getN_exten: getN n p c1 = getN n p c2. Proof. induction n; intros. auto. rewrite Nat2Z.inj_succ in H. simpl. decEq. - apply H. omega. apply IHn. intros. apply H. omega. + apply H. lia. apply IHn. intros. apply H. lia. Qed. Remark getN_setN_disjoint: @@ -636,7 +636,7 @@ Qed. Theorem valid_access_empty: forall chunk b ofs p, ~valid_access empty chunk b ofs p. Proof. intros. red; intros. elim (perm_empty b ofs Cur p). apply H. - generalize (size_chunk_pos chunk); omega. + generalize (size_chunk_pos chunk); lia. Qed. (** ** Properties related to [load] *) @@ -801,7 +801,7 @@ Theorem loadbytes_empty: n <= 0 -> loadbytes m b ofs n = Some nil. Proof. intros. unfold loadbytes. rewrite pred_dec_true. rewrite Z_to_nat_neg; auto. - red; intros. omegaContradiction. + red; intros. extlia. Qed. Lemma getN_concat: @@ -809,9 +809,9 @@ Lemma getN_concat: getN (n1 + n2)%nat p c = getN n1 p c ++ getN n2 (p + Z.of_nat n1) c. Proof. induction n1; intros. - simpl. decEq. omega. + simpl. decEq. lia. rewrite Nat2Z.inj_succ. simpl. decEq. - replace (p + Z.succ (Z.of_nat n1)) with ((p + 1) + Z.of_nat n1) by omega. + replace (p + Z.succ (Z.of_nat n1)) with ((p + 1) + Z.of_nat n1) by lia. auto. Qed. @@ -825,12 +825,12 @@ Proof. unfold loadbytes; intros. destruct (range_perm_dec m b ofs (ofs + n1) Cur Readable); try congruence. destruct (range_perm_dec m b (ofs + n1) (ofs + n1 + n2) Cur Readable); try congruence. - rewrite pred_dec_true. rewrite Z2Nat.inj_add by omega. - rewrite getN_concat. rewrite Z2Nat.id by omega. + rewrite pred_dec_true. rewrite Z2Nat.inj_add by lia. + rewrite getN_concat. rewrite Z2Nat.id by lia. congruence. red; intros. - assert (ofs0 < ofs + n1 \/ ofs0 >= ofs + n1) by omega. - destruct H4. apply r; omega. apply r0; omega. + assert (ofs0 < ofs + n1 \/ ofs0 >= ofs + n1) by lia. + destruct H4. apply r; lia. apply r0; lia. Qed. Theorem loadbytes_split: @@ -845,13 +845,13 @@ Proof. unfold loadbytes; intros. destruct (range_perm_dec m b ofs (ofs + (n1 + n2)) Cur Readable); try congruence. - rewrite Z2Nat.inj_add in H by omega. rewrite getN_concat in H. - rewrite Z2Nat.id in H by omega. + rewrite Z2Nat.inj_add in H by lia. rewrite getN_concat in H. + rewrite Z2Nat.id in H by lia. repeat rewrite pred_dec_true. econstructor; econstructor. split. reflexivity. split. reflexivity. congruence. - red; intros; apply r; omega. - red; intros; apply r; omega. + red; intros; apply r; lia. + red; intros; apply r; lia. Qed. Theorem load_rep: @@ -871,13 +871,13 @@ Proof. revert ofs H; induction n; intros; simpl; auto. f_equal. rewrite Nat2Z.inj_succ in H. - replace ofs with (ofs+0) by omega. - apply H; omega. + replace ofs with (ofs+0) by lia. + apply H; lia. apply IHn. intros. rewrite <- Z.add_assoc. apply H. - rewrite Nat2Z.inj_succ. omega. + rewrite Nat2Z.inj_succ. lia. Qed. Theorem load_int64_split: @@ -892,7 +892,7 @@ Proof. exploit load_valid_access; eauto. intros [A B]. simpl in *. exploit load_loadbytes. eexact H. simpl. intros [bytes [LB EQ]]. change 8 with (4 + 4) in LB. - exploit loadbytes_split. eexact LB. omega. omega. + exploit loadbytes_split. eexact LB. lia. lia. intros (bytes1 & bytes2 & LB1 & LB2 & APP). change 4 with (size_chunk Mint32) in LB1. exploit loadbytes_load. eexact LB1. @@ -924,11 +924,11 @@ Proof. change (Int.unsigned (Int.repr 4)) with 4. apply Ptrofs.unsigned_repr. exploit (Zdivide_interval (Ptrofs.unsigned i) Ptrofs.modulus 8). - omega. apply Ptrofs.unsigned_range. auto. + lia. apply Ptrofs.unsigned_range. auto. exists (two_p (Ptrofs.zwordsize - 3)). unfold Ptrofs.modulus, Ptrofs.zwordsize, Ptrofs.wordsize. unfold Wordsize_Ptrofs.wordsize. destruct Archi.ptr64; reflexivity. - unfold Ptrofs.max_unsigned. omega. + unfold Ptrofs.max_unsigned. lia. Qed. Theorem loadv_int64_split: @@ -1085,7 +1085,7 @@ Qed. Theorem load_store_same: load chunk m2 b ofs = Some (Val.load_result chunk v). Proof. - apply load_store_similar_2; auto. omega. + apply load_store_similar_2; auto. lia. Qed. Theorem load_store_other: @@ -1137,9 +1137,9 @@ Proof. destruct H. congruence. destruct (zle n 0) as [z | n0]. rewrite (Z_to_nat_neg _ z). auto. - destruct H. omegaContradiction. + destruct H. extlia. apply getN_setN_outside. rewrite encode_val_length. rewrite <- size_chunk_conv. - rewrite Z2Nat.id. auto. omega. + rewrite Z2Nat.id. auto. lia. auto. red; intros. eauto with mem. rewrite pred_dec_false. auto. @@ -1152,11 +1152,11 @@ Lemma setN_in: In (ZMap.get q (setN vl p c)) vl. Proof. induction vl; intros. - simpl in H. omegaContradiction. + simpl in H. extlia. simpl length in H. rewrite Nat2Z.inj_succ in H. simpl. destruct (zeq p q). subst q. rewrite setN_outside. rewrite ZMap.gss. - auto with coqlib. omega. - right. apply IHvl. omega. + auto with coqlib. lia. + right. apply IHvl. lia. Qed. Lemma getN_in: @@ -1165,10 +1165,10 @@ Lemma getN_in: In (ZMap.get q c) (getN n p c). Proof. induction n; intros. - simpl in H; omegaContradiction. + simpl in H; extlia. rewrite Nat2Z.inj_succ in H. simpl. destruct (zeq p q). subst q. auto. - right. apply IHn. omega. + right. apply IHn. lia. Qed. End STORE. @@ -1205,28 +1205,28 @@ Proof. split. rewrite V', SIZE'. apply decode_val_shape. destruct (zeq ofs' ofs). - subst ofs'. left; split. auto. unfold c'. simpl. - rewrite setN_outside by omega. apply ZMap.gss. + rewrite setN_outside by lia. apply ZMap.gss. - right. destruct (zlt ofs ofs'). (* If ofs < ofs': the load reads (at ofs') a continuation byte from the write. ofs ofs' ofs+|chunk| [-------------------] write [-------------------] read *) -+ left; split. omega. unfold c'. simpl. apply setN_in. ++ left; split. lia. unfold c'. simpl. apply setN_in. assert (Z.of_nat (length (mv1 :: mvl)) = size_chunk chunk). { rewrite <- ENC; rewrite encode_val_length. rewrite size_chunk_conv; auto. } - simpl length in H3. rewrite Nat2Z.inj_succ in H3. omega. + simpl length in H3. rewrite Nat2Z.inj_succ in H3. lia. (* If ofs > ofs': the load reads (at ofs) the first byte from the write. ofs' ofs ofs'+|chunk'| [-------------------] write [----------------] read *) -+ right; split. omega. replace mv1 with (ZMap.get ofs c'). ++ right; split. lia. replace mv1 with (ZMap.get ofs c'). apply getN_in. assert (size_chunk chunk' = Z.succ (Z.of_nat sz')). { rewrite size_chunk_conv. rewrite SIZE'. rewrite Nat2Z.inj_succ; auto. } - omega. - unfold c'. simpl. rewrite setN_outside by omega. apply ZMap.gss. + lia. + unfold c'. simpl. rewrite setN_outside by lia. apply ZMap.gss. Qed. Definition compat_pointer_chunks (chunk1 chunk2: memory_chunk) : Prop := @@ -1313,10 +1313,10 @@ Theorem load_store_pointer_mismatch: Proof. intros. exploit load_store_overlap; eauto. - generalize (size_chunk_pos chunk'); omega. - generalize (size_chunk_pos chunk); omega. + generalize (size_chunk_pos chunk'); lia. + generalize (size_chunk_pos chunk); lia. intros (mv1 & mvl & mv1' & mvl' & ENC & DEC & CASES). - destruct CASES as [(A & B) | [(A & B) | (A & B)]]; try omegaContradiction. + destruct CASES as [(A & B) | [(A & B) | (A & B)]]; try extlia. inv ENC; inv DEC; auto. - elim H1. apply compat_pointer_chunks_true; auto. - contradiction. @@ -1338,8 +1338,8 @@ Proof. destruct (valid_access_dec m chunk1 b ofs Writable); destruct (valid_access_dec m chunk2 b ofs Writable); auto. f_equal. apply mkmem_ext; auto. congruence. - elim n. apply valid_access_compat with chunk1; auto. omega. - elim n. apply valid_access_compat with chunk2; auto. omega. + elim n. apply valid_access_compat with chunk1; auto. lia. + elim n. apply valid_access_compat with chunk2; auto. lia. Qed. Theorem store_signed_unsigned_8: @@ -1385,7 +1385,7 @@ Proof. destruct (valid_access_dec m Mfloat64 b ofs Writable); try discriminate. destruct (valid_access_dec m Mfloat64al32 b ofs Writable). rewrite <- H. f_equal. apply mkmem_ext; auto. - elim n. apply valid_access_compat with Mfloat64; auto. simpl; omega. + elim n. apply valid_access_compat with Mfloat64; auto. simpl; lia. Qed. Theorem storev_float64al32: @@ -1548,7 +1548,7 @@ Proof. rewrite pred_dec_true. rewrite storebytes_mem_contents. decEq. rewrite PMap.gsspec. destruct (peq b' b). subst b'. - apply getN_setN_disjoint. rewrite Z2Nat.id by omega. intuition congruence. + apply getN_setN_disjoint. rewrite Z2Nat.id by lia. intuition congruence. auto. red; auto with mem. apply pred_dec_false. @@ -1593,8 +1593,8 @@ Lemma setN_concat: setN (bytes1 ++ bytes2) ofs c = setN bytes2 (ofs + Z.of_nat (length bytes1)) (setN bytes1 ofs c). Proof. induction bytes1; intros. - simpl. decEq. omega. - simpl length. rewrite Nat2Z.inj_succ. simpl. rewrite IHbytes1. decEq. omega. + simpl. decEq. lia. + simpl length. rewrite Nat2Z.inj_succ. simpl. rewrite IHbytes1. decEq. lia. Qed. Theorem storebytes_concat: @@ -1613,8 +1613,8 @@ Proof. elim n. rewrite app_length. rewrite Nat2Z.inj_add. red; intros. destruct (zlt ofs0 (ofs + Z.of_nat(length bytes1))). - apply r. omega. - eapply perm_storebytes_2; eauto. apply r0. omega. + apply r. lia. + eapply perm_storebytes_2; eauto. apply r0. lia. Qed. Theorem storebytes_split: @@ -1627,10 +1627,10 @@ Proof. intros. destruct (range_perm_storebytes m b ofs bytes1) as [m1 ST1]. red; intros. exploit storebytes_range_perm; eauto. rewrite app_length. - rewrite Nat2Z.inj_add. omega. + rewrite Nat2Z.inj_add. lia. destruct (range_perm_storebytes m1 b (ofs + Z.of_nat (length bytes1)) bytes2) as [m2' ST2]. red; intros. eapply perm_storebytes_1; eauto. exploit storebytes_range_perm. - eexact H. instantiate (1 := ofs0). rewrite app_length. rewrite Nat2Z.inj_add. omega. + eexact H. instantiate (1 := ofs0). rewrite app_length. rewrite Nat2Z.inj_add. lia. auto. assert (Some m2 = Some m2'). rewrite <- H. eapply storebytes_concat; eauto. @@ -1738,7 +1738,7 @@ Theorem perm_alloc_2: Proof. unfold perm; intros. injection ALLOC; intros. rewrite <- H1; simpl. subst b. rewrite PMap.gss. unfold proj_sumbool. rewrite zle_true. - rewrite zlt_true. simpl. auto with mem. omega. omega. + rewrite zlt_true. simpl. auto with mem. lia. lia. Qed. Theorem perm_alloc_inv: @@ -1782,7 +1782,7 @@ Theorem valid_access_alloc_same: valid_access m2 chunk b ofs Freeable. Proof. intros. constructor; auto with mem. - red; intros. apply perm_alloc_2. omega. + red; intros. apply perm_alloc_2. lia. Qed. Local Hint Resolve valid_access_alloc_other valid_access_alloc_same: mem. @@ -1797,11 +1797,11 @@ Proof. intros. inv H. generalize (size_chunk_pos chunk); intro. destruct (eq_block b' b). subst b'. - assert (perm m2 b ofs Cur p). apply H0. omega. - assert (perm m2 b (ofs + size_chunk chunk - 1) Cur p). apply H0. omega. + assert (perm m2 b ofs Cur p). apply H0. lia. + assert (perm m2 b (ofs + size_chunk chunk - 1) Cur p). apply H0. lia. exploit perm_alloc_inv. eexact H2. rewrite dec_eq_true. intro. exploit perm_alloc_inv. eexact H3. rewrite dec_eq_true. intro. - intuition omega. + intuition lia. split; auto. red; intros. exploit perm_alloc_inv. apply H0. eauto. rewrite dec_eq_false; auto. Qed. @@ -1848,7 +1848,7 @@ Theorem load_alloc_same': Proof. intros. assert (exists v, load chunk m2 b ofs = Some v). apply valid_access_load. constructor; auto. - red; intros. eapply perm_implies. apply perm_alloc_2. omega. auto with mem. + red; intros. eapply perm_implies. apply perm_alloc_2. lia. auto with mem. destruct H2 as [v LOAD]. rewrite LOAD. decEq. eapply load_alloc_same; eauto. Qed. @@ -1958,7 +1958,7 @@ Theorem perm_free_2: Proof. intros. rewrite free_result. unfold perm, unchecked_free; simpl. rewrite PMap.gss. unfold proj_sumbool. rewrite zle_true. rewrite zlt_true. - simpl. tauto. omega. omega. + simpl. tauto. lia. lia. Qed. Theorem perm_free_3: @@ -1991,7 +1991,7 @@ Theorem valid_access_free_1: Proof. intros. inv H. constructor; auto with mem. red; intros. eapply perm_free_1; eauto. - destruct (zlt lo hi). intuition. right. omega. + destruct (zlt lo hi). intuition. right. lia. Qed. Theorem valid_access_free_2: @@ -2003,9 +2003,9 @@ Proof. generalize (size_chunk_pos chunk); intros. destruct (zlt ofs lo). elim (perm_free_2 lo Cur p). - omega. apply H3. omega. + lia. apply H3. lia. elim (perm_free_2 ofs Cur p). - omega. apply H3. omega. + lia. apply H3. lia. Qed. Theorem valid_access_free_inv_1: @@ -2031,7 +2031,7 @@ Proof. destruct (zlt lo hi); auto. destruct (zle (ofs + size_chunk chunk) lo); auto. destruct (zle hi ofs); auto. - elim (valid_access_free_2 chunk ofs p); auto. omega. + elim (valid_access_free_2 chunk ofs p); auto. lia. Qed. Theorem load_free: @@ -2069,7 +2069,7 @@ Proof. red; intros. eapply perm_free_3; eauto. rewrite pred_dec_false; auto. red; intros. elim n0; red; intros. - eapply perm_free_1; eauto. destruct H; auto. right; omega. + eapply perm_free_1; eauto. destruct H; auto. right; lia. Qed. Theorem loadbytes_free_2: @@ -2139,7 +2139,7 @@ Proof. unfold drop_perm in DROP. destruct (range_perm_dec m b lo hi Cur Freeable); inv DROP. unfold perm. simpl. rewrite PMap.gss. unfold proj_sumbool. rewrite zle_true. rewrite zlt_true. simpl. constructor. - omega. omega. + lia. lia. Qed. Theorem perm_drop_2: @@ -2149,7 +2149,7 @@ Proof. unfold drop_perm in DROP. destruct (range_perm_dec m b lo hi Cur Freeable); inv DROP. revert H0. unfold perm; simpl. rewrite PMap.gss. unfold proj_sumbool. rewrite zle_true. rewrite zlt_true. simpl. auto. - omega. omega. + lia. lia. Qed. Theorem perm_drop_3: @@ -2159,7 +2159,7 @@ Proof. unfold drop_perm in DROP. destruct (range_perm_dec m b lo hi Cur Freeable); inv DROP. unfold perm; simpl. rewrite PMap.gsspec. destruct (peq b' b). subst b'. unfold proj_sumbool. destruct (zle lo ofs). destruct (zlt ofs hi). - byContradiction. intuition omega. + byContradiction. intuition lia. auto. auto. auto. Qed. @@ -2185,7 +2185,7 @@ Proof. destruct (eq_block b' b). subst b'. destruct (zlt ofs0 lo). eapply perm_drop_3; eauto. destruct (zle hi ofs0). eapply perm_drop_3; eauto. - apply perm_implies with p. eapply perm_drop_1; eauto. omega. + apply perm_implies with p. eapply perm_drop_1; eauto. lia. generalize (size_chunk_pos chunk); intros. intuition. eapply perm_drop_3; eauto. Qed. @@ -2227,7 +2227,7 @@ Proof. destruct (eq_block b' b). subst b'. destruct (zlt ofs0 lo). eapply perm_drop_3; eauto. destruct (zle hi ofs0). eapply perm_drop_3; eauto. - apply perm_implies with p. eapply perm_drop_1; eauto. omega. intuition. + apply perm_implies with p. eapply perm_drop_1; eauto. lia. intuition. eapply perm_drop_3; eauto. rewrite pred_dec_false; eauto. red; intros; elim n0; red; intros. @@ -2285,8 +2285,8 @@ Lemma range_perm_inj: range_perm m2 b2 (lo + delta) (hi + delta) k p. Proof. intros; red; intros. - replace ofs with ((ofs - delta) + delta) by omega. - eapply perm_inj; eauto. apply H0. omega. + replace ofs with ((ofs - delta) + delta) by lia. + eapply perm_inj; eauto. apply H0. lia. Qed. Lemma valid_access_inj: @@ -2298,7 +2298,7 @@ Lemma valid_access_inj: Proof. intros. destruct H1 as [A B]. constructor. replace (ofs + delta + size_chunk chunk) - with ((ofs + size_chunk chunk) + delta) by omega. + with ((ofs + size_chunk chunk) + delta) by lia. eapply range_perm_inj; eauto. apply Z.divide_add_r; auto. eapply mi_align; eauto with mem. Qed. @@ -2320,9 +2320,9 @@ Proof. rewrite Nat2Z.inj_succ in H1. constructor. eapply mi_memval; eauto. - apply H1. omega. - replace (ofs + delta + 1) with ((ofs + 1) + delta) by omega. - apply IHn. red; intros; apply H1; omega. + apply H1. lia. + replace (ofs + delta + 1) with ((ofs + 1) + delta) by lia. + apply IHn. red; intros; apply H1; lia. Qed. Lemma load_inj: @@ -2353,11 +2353,11 @@ Proof. destruct (range_perm_dec m1 b1 ofs (ofs + len) Cur Readable); inv H0. exists (getN (Z.to_nat len) (ofs + delta) (m2.(mem_contents)#b2)). split. apply pred_dec_true. - replace (ofs + delta + len) with ((ofs + len) + delta) by omega. + replace (ofs + delta + len) with ((ofs + len) + delta) by lia. eapply range_perm_inj; eauto with mem. apply getN_inj; auto. - destruct (zle 0 len). rewrite Z2Nat.id by omega. auto. - rewrite Z_to_nat_neg by omega. simpl. red; intros; omegaContradiction. + destruct (zle 0 len). rewrite Z2Nat.id by lia. auto. + rewrite Z_to_nat_neg by lia. simpl. red; intros; extlia. Qed. (** Preservation of stores. *) @@ -2372,11 +2372,11 @@ Lemma setN_inj: Proof. induction 1; intros; simpl. auto. - replace (p + delta + 1) with ((p + 1) + delta) by omega. + replace (p + delta + 1) with ((p + 1) + delta) by lia. apply IHlist_forall2; auto. intros. rewrite ZMap.gsspec at 1. destruct (ZIndexed.eq q0 p). subst q0. rewrite ZMap.gss. auto. - rewrite ZMap.gso. auto. unfold ZIndexed.t in *. omega. + rewrite ZMap.gso. auto. unfold ZIndexed.t in *. lia. Qed. Definition meminj_no_overlap (f: meminj) (m: mem) : Prop := @@ -2431,8 +2431,8 @@ Proof. assert (b2 <> b2 \/ ofs0 + delta0 <> (r - delta) + delta). eapply H1; eauto. eauto 6 with mem. exploit store_valid_access_3. eexact H0. intros [A B]. - eapply perm_implies. apply perm_cur_max. apply A. omega. auto with mem. - destruct H8. congruence. omega. + eapply perm_implies. apply perm_cur_max. apply A. lia. auto with mem. + destruct H8. congruence. lia. (* block <> b1, block <> b2 *) eapply mi_memval; eauto. eauto with mem. Qed. @@ -2479,8 +2479,8 @@ Proof. rewrite setN_outside. auto. rewrite encode_val_length. rewrite <- size_chunk_conv. destruct (zlt (ofs0 + delta) ofs); auto. - destruct (zle (ofs + size_chunk chunk) (ofs0 + delta)). omega. - byContradiction. eapply H0; eauto. omega. + destruct (zle (ofs + size_chunk chunk) (ofs0 + delta)). lia. + byContradiction. eapply H0; eauto. lia. eauto with mem. Qed. @@ -2501,7 +2501,7 @@ Proof. with ((ofs + Z.of_nat (length bytes1)) + delta). eapply range_perm_inj; eauto with mem. eapply storebytes_range_perm; eauto. - rewrite (list_forall2_length H3). omega. + rewrite (list_forall2_length H3). lia. destruct (range_perm_storebytes _ _ _ _ H4) as [n2 STORE]. exists n2; split. eauto. constructor. @@ -2532,9 +2532,9 @@ Proof. eapply H1; eauto 6 with mem. exploit storebytes_range_perm. eexact H0. instantiate (1 := r - delta). - rewrite (list_forall2_length H3). omega. + rewrite (list_forall2_length H3). lia. eauto 6 with mem. - destruct H9. congruence. omega. + destruct H9. congruence. lia. (* block <> b1, block <> b2 *) eauto. Qed. @@ -2581,8 +2581,8 @@ Proof. rewrite PMap.gsspec. destruct (peq b2 b). subst b2. rewrite setN_outside. auto. destruct (zlt (ofs0 + delta) ofs); auto. - destruct (zle (ofs + Z.of_nat (length bytes2)) (ofs0 + delta)). omega. - byContradiction. eapply H0; eauto. omega. + destruct (zle (ofs + Z.of_nat (length bytes2)) (ofs0 + delta)). lia. + byContradiction. eapply H0; eauto. lia. eauto with mem. Qed. @@ -2679,10 +2679,10 @@ Proof. intros. destruct (eq_block b0 b1). subst b0. assert (delta0 = delta) by congruence. subst delta0. assert (lo <= ofs < hi). - { eapply perm_alloc_3; eauto. apply H6. generalize (size_chunk_pos chunk); omega. } + { eapply perm_alloc_3; eauto. apply H6. generalize (size_chunk_pos chunk); lia. } assert (lo <= ofs + size_chunk chunk - 1 < hi). - { eapply perm_alloc_3; eauto. apply H6. generalize (size_chunk_pos chunk); omega. } - apply H2. omega. + { eapply perm_alloc_3; eauto. apply H6. generalize (size_chunk_pos chunk); lia. } + apply H2. lia. eapply mi_align0 with (ofs := ofs) (p := p); eauto. red; intros. eapply perm_alloc_4; eauto. (* mem_contents *) @@ -2727,7 +2727,7 @@ Proof. intros. eapply perm_free_1; eauto. destruct (eq_block b2 b); auto. subst b. right. assert (~ (lo <= ofs + delta < hi)). red; intros; eapply H1; eauto. - omega. + lia. constructor. (* perm *) auto. @@ -2772,8 +2772,8 @@ Proof. intros. assert ({ m2' | drop_perm m2 b2 (lo + delta) (hi + delta) p = Some m2' }). apply range_perm_drop_2. red; intros. - replace ofs with ((ofs - delta) + delta) by omega. - eapply perm_inj; eauto. eapply range_perm_drop_1; eauto. omega. + replace ofs with ((ofs - delta) + delta) by lia. + eapply perm_inj; eauto. eapply range_perm_drop_1; eauto. lia. destruct X as [m2' DROP]. exists m2'; split; auto. inv H. constructor. @@ -2787,9 +2787,9 @@ Proof. destruct (zlt (ofs + delta0) (lo + delta0)). eapply perm_drop_3; eauto. destruct (zle (hi + delta0) (ofs + delta0)). eapply perm_drop_3; eauto. assert (perm_order p p0). - eapply perm_drop_2. eexact H0. instantiate (1 := ofs). omega. eauto. + eapply perm_drop_2. eexact H0. instantiate (1 := ofs). lia. eauto. apply perm_implies with p; auto. - eapply perm_drop_1. eauto. omega. + eapply perm_drop_1. eauto. lia. (* b1 <> b0 *) eapply perm_drop_3; eauto. destruct (eq_block b3 b2); auto. @@ -2798,7 +2798,7 @@ Proof. exploit H1; eauto. instantiate (1 := ofs + delta0 - delta). apply perm_cur_max. apply perm_implies with Freeable. - eapply range_perm_drop_1; eauto. omega. auto with mem. + eapply range_perm_drop_1; eauto. lia. auto with mem. eapply perm_drop_4; eauto. eapply perm_max. apply perm_implies with p0. eauto. eauto with mem. intuition. @@ -2829,7 +2829,7 @@ Proof. destruct (eq_block b2 b); auto. subst b2. right. destruct (zlt (ofs + delta) lo); auto. destruct (zle hi (ofs + delta)); auto. - byContradiction. exploit H1; eauto. omega. + byContradiction. exploit H1; eauto. lia. (* align *) eapply mi_align0; eauto. (* contents *) @@ -2862,9 +2862,9 @@ Theorem extends_refl: forall m, extends m m. Proof. intros. constructor. auto. constructor. - intros. unfold inject_id in H; inv H. replace (ofs + 0) with ofs by omega. auto. + intros. unfold inject_id in H; inv H. replace (ofs + 0) with ofs by lia. auto. intros. unfold inject_id in H; inv H. apply Z.divide_0_r. - intros. unfold inject_id in H; inv H. replace (ofs + 0) with ofs by omega. + intros. unfold inject_id in H; inv H. replace (ofs + 0) with ofs by lia. apply memval_lessdef_refl. tauto. Qed. @@ -2877,7 +2877,7 @@ Theorem load_extends: Proof. intros. inv H. exploit load_inj; eauto. unfold inject_id; reflexivity. intros [v2 [A B]]. exists v2; split. - replace (ofs + 0) with ofs in A by omega. auto. + replace (ofs + 0) with ofs in A by lia. auto. rewrite val_inject_id in B. auto. Qed. @@ -2901,7 +2901,7 @@ Theorem loadbytes_extends: /\ list_forall2 memval_lessdef bytes1 bytes2. Proof. intros. inv H. - replace ofs with (ofs + 0) by omega. eapply loadbytes_inj; eauto. + replace ofs with (ofs + 0) by lia. eapply loadbytes_inj; eauto. Qed. Theorem store_within_extends: @@ -2920,7 +2920,7 @@ Proof. rewrite val_inject_id. eauto. intros [m2' [A B]]. exists m2'; split. - replace (ofs + 0) with ofs in A by omega. auto. + replace (ofs + 0) with ofs in A by lia. auto. constructor; auto. rewrite (nextblock_store _ _ _ _ _ _ H0). rewrite (nextblock_store _ _ _ _ _ _ A). @@ -2938,7 +2938,7 @@ Proof. intros. inversion H. constructor. rewrite (nextblock_store _ _ _ _ _ _ H0). auto. eapply store_outside_inj; eauto. - unfold inject_id; intros. inv H2. eapply H1; eauto. omega. + unfold inject_id; intros. inv H2. eapply H1; eauto. lia. intros. eauto using perm_store_2. Qed. @@ -2972,7 +2972,7 @@ Proof. unfold inject_id; reflexivity. intros [m2' [A B]]. exists m2'; split. - replace (ofs + 0) with ofs in A by omega. auto. + replace (ofs + 0) with ofs in A by lia. auto. constructor; auto. rewrite (nextblock_storebytes _ _ _ _ _ H0). rewrite (nextblock_storebytes _ _ _ _ _ A). @@ -2990,7 +2990,7 @@ Proof. intros. inversion H. constructor. rewrite (nextblock_storebytes _ _ _ _ _ H0). auto. eapply storebytes_outside_inj; eauto. - unfold inject_id; intros. inv H2. eapply H1; eauto. omega. + unfold inject_id; intros. inv H2. eapply H1; eauto. lia. intros. eauto using perm_storebytes_2. Qed. @@ -3022,12 +3022,12 @@ Proof. intros. eapply perm_implies with Freeable; auto with mem. eapply perm_alloc_2; eauto. - omega. + lia. intros. eapply perm_alloc_inv in H; eauto. generalize (perm_alloc_inv _ _ _ _ _ H0 b0 ofs Max Nonempty); intros PERM. destruct (eq_block b0 b). subst b0. - assert (EITHER: lo1 <= ofs < hi1 \/ ~(lo1 <= ofs < hi1)) by omega. + assert (EITHER: lo1 <= ofs < hi1 \/ ~(lo1 <= ofs < hi1)) by lia. destruct EITHER. left. apply perm_implies with Freeable; auto with mem. eapply perm_alloc_2; eauto. right; tauto. @@ -3059,7 +3059,7 @@ Proof. intros. inv H. constructor. rewrite (nextblock_free _ _ _ _ _ H0). auto. eapply free_right_inj; eauto. - unfold inject_id; intros. inv H. eapply H1; eauto. omega. + unfold inject_id; intros. inv H. eapply H1; eauto. lia. intros. eauto using perm_free_3. Qed. @@ -3074,7 +3074,7 @@ Proof. intros. inversion H. assert ({ m2': mem | free m2 b lo hi = Some m2' }). apply range_perm_free. red; intros. - replace ofs with (ofs + 0) by omega. + replace ofs with (ofs + 0) by lia. eapply perm_inj with (b1 := b); eauto. eapply free_range_perm; eauto. destruct X as [m2' FREE]. exists m2'; split; auto. @@ -3084,7 +3084,7 @@ Proof. eapply free_right_inj with (m1 := m1'); eauto. eapply free_left_inj; eauto. unfold inject_id; intros. inv H1. - eapply perm_free_2. eexact H0. instantiate (1 := ofs); omega. eauto. + eapply perm_free_2. eexact H0. instantiate (1 := ofs); lia. eauto. intros. exploit mext_perm_inv0; eauto using perm_free_3. intros [A|A]. eapply perm_free_inv in A; eauto. destruct A as [[A B]|A]; auto. subst b0. right; eapply perm_free_2; eauto. @@ -3103,7 +3103,7 @@ Theorem perm_extends: forall m1 m2 b ofs k p, extends m1 m2 -> perm m1 b ofs k p -> perm m2 b ofs k p. Proof. - intros. inv H. replace ofs with (ofs + 0) by omega. + intros. inv H. replace ofs with (ofs + 0) by lia. eapply perm_inj; eauto. Qed. @@ -3118,7 +3118,7 @@ Theorem valid_access_extends: forall m1 m2 chunk b ofs p, extends m1 m2 -> valid_access m1 chunk b ofs p -> valid_access m2 chunk b ofs p. Proof. - intros. inv H. replace ofs with (ofs + 0) by omega. + intros. inv H. replace ofs with (ofs + 0) by lia. eapply valid_access_inj; eauto. auto. Qed. @@ -3263,7 +3263,7 @@ Theorem weak_valid_pointer_inject: weak_valid_pointer m2 b2 (ofs + delta) = true. Proof. intros until 2. unfold weak_valid_pointer. rewrite !orb_true_iff. - replace (ofs + delta - 1) with ((ofs - 1) + delta) by omega. + replace (ofs + delta - 1) with ((ofs - 1) + delta) by lia. intros []; eauto using valid_pointer_inject. Qed. @@ -3281,8 +3281,8 @@ Proof. assert (perm m1 b1 (Ptrofs.unsigned ofs1) Max Nonempty) by eauto with mem. exploit mi_representable; eauto. intros [A B]. assert (0 <= delta <= Ptrofs.max_unsigned). - generalize (Ptrofs.unsigned_range ofs1). omega. - unfold Ptrofs.add. repeat rewrite Ptrofs.unsigned_repr; omega. + generalize (Ptrofs.unsigned_range ofs1). lia. + unfold Ptrofs.add. repeat rewrite Ptrofs.unsigned_repr; lia. Qed. Lemma address_inject': @@ -3293,7 +3293,7 @@ Lemma address_inject': Ptrofs.unsigned (Ptrofs.add ofs1 (Ptrofs.repr delta)) = Ptrofs.unsigned ofs1 + delta. Proof. intros. destruct H0. eapply address_inject; eauto. - apply H0. generalize (size_chunk_pos chunk). omega. + apply H0. generalize (size_chunk_pos chunk). lia. Qed. Theorem weak_valid_pointer_inject_no_overflow: @@ -3308,7 +3308,7 @@ Proof. exploit mi_representable; eauto. destruct H0; eauto with mem. intros [A B]. pose proof (Ptrofs.unsigned_range ofs). - rewrite Ptrofs.unsigned_repr; omega. + rewrite Ptrofs.unsigned_repr; lia. Qed. Theorem valid_pointer_inject_no_overflow: @@ -3348,7 +3348,7 @@ Proof. exploit mi_representable; eauto. destruct H0; eauto with mem. intros [A B]. pose proof (Ptrofs.unsigned_range ofs). - unfold Ptrofs.add. repeat rewrite Ptrofs.unsigned_repr; auto; omega. + unfold Ptrofs.add. repeat rewrite Ptrofs.unsigned_repr; auto; lia. Qed. Theorem inject_no_overlap: @@ -3383,8 +3383,8 @@ Proof. rewrite (address_inject' _ _ _ _ _ _ _ _ H H2 H4). inv H1. simpl in H5. inv H2. simpl in H1. eapply mi_no_overlap; eauto. - apply perm_cur_max. apply (H5 (Ptrofs.unsigned ofs1)). omega. - apply perm_cur_max. apply (H1 (Ptrofs.unsigned ofs2)). omega. + apply perm_cur_max. apply (H5 (Ptrofs.unsigned ofs1)). lia. + apply perm_cur_max. apply (H1 (Ptrofs.unsigned ofs2)). lia. Qed. Theorem disjoint_or_equal_inject: @@ -3403,16 +3403,16 @@ Proof. intros. destruct (eq_block b1 b2). assert (b1' = b2') by congruence. assert (delta1 = delta2) by congruence. subst. - destruct H5. congruence. right. destruct H5. left; congruence. right. omega. + destruct H5. congruence. right. destruct H5. left; congruence. right. lia. destruct (eq_block b1' b2'); auto. subst. right. right. set (i1 := (ofs1 + delta1, ofs1 + delta1 + sz)). set (i2 := (ofs2 + delta2, ofs2 + delta2 + sz)). change (snd i1 <= fst i2 \/ snd i2 <= fst i1). - apply Intv.range_disjoint'; simpl; try omega. + apply Intv.range_disjoint'; simpl; try lia. unfold Intv.disjoint, Intv.In; simpl; intros. red; intros. exploit mi_no_overlap; eauto. - instantiate (1 := x - delta1). apply H2. omega. - instantiate (1 := x - delta2). apply H3. omega. + instantiate (1 := x - delta1). apply H2. lia. + instantiate (1 := x - delta2). apply H3. lia. intuition. Qed. @@ -3427,9 +3427,9 @@ Theorem aligned_area_inject: (al | ofs + delta). Proof. intros. - assert (P: al > 0) by omega. - assert (Q: Z.abs al <= Z.abs sz). apply Zdivide_bounds; auto. omega. - rewrite Z.abs_eq in Q; try omega. rewrite Z.abs_eq in Q; try omega. + assert (P: al > 0) by lia. + assert (Q: Z.abs al <= Z.abs sz). apply Zdivide_bounds; auto. lia. + rewrite Z.abs_eq in Q; try lia. rewrite Z.abs_eq in Q; try lia. assert (R: exists chunk, al = align_chunk chunk /\ al = size_chunk chunk). destruct H0. subst; exists Mint8unsigned; auto. destruct H0. subst; exists Mint16unsigned; auto. @@ -3437,7 +3437,7 @@ Proof. subst; exists Mint64; auto. destruct R as [chunk [A B]]. assert (valid_access m chunk b ofs Nonempty). - split. red; intros; apply H3. omega. congruence. + split. red; intros; apply H3. lia. congruence. exploit valid_access_inject; eauto. intros [C D]. congruence. Qed. @@ -3794,7 +3794,7 @@ Proof. unfold f'; intros. destruct (eq_block b0 b1). inversion H8. subst b0 b3 delta0. elim (fresh_block_alloc _ _ _ _ _ H0). - eapply perm_valid_block with (ofs := ofs). apply H9. generalize (size_chunk_pos chunk); omega. + eapply perm_valid_block with (ofs := ofs). apply H9. generalize (size_chunk_pos chunk); lia. eauto. unfold f'; intros. destruct (eq_block b0 b1). inversion H8. subst b0 b3 delta0. @@ -3817,10 +3817,10 @@ Proof. congruence. inversion H10; subst b0 b1' delta1. destruct (eq_block b2 b2'); auto. subst b2'. right; red; intros. - eapply H6; eauto. omega. + eapply H6; eauto. lia. inversion H11; subst b3 b2' delta2. destruct (eq_block b1' b2); auto. subst b1'. right; red; intros. - eapply H6; eauto. omega. + eapply H6; eauto. lia. eauto. (* representable *) unfold f'; intros. @@ -3828,16 +3828,16 @@ Proof. subst. injection H9; intros; subst b' delta0. destruct H10. exploit perm_alloc_inv; eauto; rewrite dec_eq_true; intro. exploit H3. apply H4 with (k := Max) (p := Nonempty); eauto. - generalize (Ptrofs.unsigned_range_2 ofs). omega. + generalize (Ptrofs.unsigned_range_2 ofs). lia. exploit perm_alloc_inv; eauto; rewrite dec_eq_true; intro. exploit H3. apply H4 with (k := Max) (p := Nonempty); eauto. - generalize (Ptrofs.unsigned_range_2 ofs). omega. + generalize (Ptrofs.unsigned_range_2 ofs). lia. eapply mi_representable0; try eassumption. destruct H10; eauto using perm_alloc_4. (* perm inv *) intros. unfold f' in H9; destruct (eq_block b0 b1). inversion H9; clear H9; subst b0 b3 delta0. - assert (EITHER: lo <= ofs < hi \/ ~(lo <= ofs < hi)) by omega. + assert (EITHER: lo <= ofs < hi \/ ~(lo <= ofs < hi)) by lia. destruct EITHER. left. apply perm_implies with Freeable; auto with mem. eapply perm_alloc_2; eauto. right; intros A. eapply perm_alloc_inv in A; eauto. rewrite dec_eq_true in A. tauto. @@ -3868,10 +3868,10 @@ Proof. eapply alloc_right_inject; eauto. eauto. instantiate (1 := b2). eauto with mem. - instantiate (1 := 0). unfold Ptrofs.max_unsigned. generalize Ptrofs.modulus_pos; omega. + instantiate (1 := 0). unfold Ptrofs.max_unsigned. generalize Ptrofs.modulus_pos; lia. auto. intros. apply perm_implies with Freeable; auto with mem. - eapply perm_alloc_2; eauto. omega. + eapply perm_alloc_2; eauto. lia. red; intros. apply Z.divide_0_r. intros. apply (valid_not_valid_diff m2 b2 b2); eauto with mem. intros [f' [A [B [C D]]]]. @@ -3994,13 +3994,13 @@ Proof. simpl; rewrite H0; auto. intros. destruct (eq_block b1 b). subst b1. rewrite H1 in H2; inv H2. - exists lo, hi; split; auto with coqlib. omega. + exists lo, hi; split; auto with coqlib. lia. exploit mi_no_overlap. eexact H. eexact n. eauto. eauto. eapply perm_max. eapply perm_implies. eauto. auto with mem. instantiate (1 := ofs + delta0 - delta). apply perm_cur_max. apply perm_implies with Freeable; auto with mem. - eapply free_range_perm; eauto. omega. - intros [A|A]. congruence. omega. + eapply free_range_perm; eauto. lia. + intros [A|A]. congruence. lia. Qed. Lemma drop_outside_inject: forall f m1 m2 b lo hi p m2', @@ -4027,7 +4027,7 @@ Proof. (* perm *) destruct (f b1) as [[b' delta'] |] eqn:?; try discriminate. destruct (f' b') as [[b'' delta''] |] eqn:?; inv H. - replace (ofs + (delta' + delta'')) with ((ofs + delta') + delta'') by omega. + replace (ofs + (delta' + delta'')) with ((ofs + delta') + delta'') by lia. eauto. (* align *) destruct (f b1) as [[b' delta'] |] eqn:?; try discriminate. @@ -4035,12 +4035,12 @@ Proof. apply Z.divide_add_r. eapply mi_align0; eauto. eapply mi_align1 with (ofs := ofs + delta') (p := p); eauto. - red; intros. replace ofs0 with ((ofs0 - delta') + delta') by omega. - eapply mi_perm0; eauto. apply H0. omega. + red; intros. replace ofs0 with ((ofs0 - delta') + delta') by lia. + eapply mi_perm0; eauto. apply H0. lia. (* memval *) destruct (f b1) as [[b' delta'] |] eqn:?; try discriminate. destruct (f' b') as [[b'' delta''] |] eqn:?; inv H. - replace (ofs + (delta' + delta'')) with ((ofs + delta') + delta'') by omega. + replace (ofs + (delta' + delta'')) with ((ofs + delta') + delta'') by lia. eapply memval_inject_compose; eauto. Qed. @@ -4069,11 +4069,11 @@ Proof. exploit mi_no_overlap0; eauto. intros A. destruct (eq_block b1x b2x). subst b1x. destruct A. congruence. - assert (delta1y = delta2y) by congruence. right; omega. + assert (delta1y = delta2y) by congruence. right; lia. exploit mi_no_overlap1. eauto. eauto. eauto. eapply perm_inj. eauto. eexact H2. eauto. eapply perm_inj. eauto. eexact H3. eauto. - intuition omega. + intuition lia. (* representable *) intros. destruct (f b) as [[b1 delta1] |] eqn:?; try discriminate. @@ -4085,15 +4085,15 @@ Proof. exploit mi_representable1. eauto. instantiate (1 := ofs'). rewrite H. replace (Ptrofs.unsigned ofs + delta1 - 1) with - ((Ptrofs.unsigned ofs - 1) + delta1) by omega. + ((Ptrofs.unsigned ofs - 1) + delta1) by lia. destruct H0; eauto using perm_inj. - rewrite H. omega. + rewrite H. lia. (* perm inv *) intros. destruct (f b1) as [[b' delta'] |] eqn:?; try discriminate. destruct (f' b') as [[b'' delta''] |] eqn:?; try discriminate. inversion H; clear H; subst b'' delta. - replace (ofs + (delta' + delta'')) with ((ofs + delta') + delta'') in H0 by omega. + replace (ofs + (delta' + delta'')) with ((ofs + delta') + delta'') in H0 by lia. exploit mi_perm_inv1; eauto. intros [A|A]. eapply mi_perm_inv0; eauto. right; red; intros. elim A. eapply perm_inj; eauto. @@ -4145,7 +4145,7 @@ Proof. (* inj *) replace f with (compose_meminj f inject_id). eapply mem_inj_compose; eauto. apply extensionality; intros. unfold compose_meminj, inject_id. - destruct (f x) as [[y delta] | ]; auto. decEq. decEq. omega. + destruct (f x) as [[y delta] | ]; auto. decEq. decEq. lia. (* unmapped *) eauto. (* mapped *) @@ -4210,7 +4210,7 @@ Proof. apply flat_inj_no_overlap. (* range *) unfold flat_inj; intros. - destruct (plt b (nextblock m)); inv H0. generalize (Ptrofs.unsigned_range_2 ofs); omega. + destruct (plt b (nextblock m)); inv H0. generalize (Ptrofs.unsigned_range_2 ofs); lia. (* perm inv *) unfold flat_inj; intros. destruct (plt b1 (nextblock m)); inv H0. @@ -4223,7 +4223,7 @@ Proof. intros; red; constructor. (* perm *) unfold flat_inj; intros. destruct (plt b1 thr); inv H. - replace (ofs + 0) with ofs by omega; auto. + replace (ofs + 0) with ofs by lia; auto. (* align *) unfold flat_inj; intros. destruct (plt b1 thr); inv H. apply Z.divide_0_r. (* mem_contents *) @@ -4243,7 +4243,7 @@ Proof. red. intros. apply Z.divide_0_r. intros. apply perm_implies with Freeable; auto with mem. - eapply perm_alloc_2; eauto. omega. + eapply perm_alloc_2; eauto. lia. unfold flat_inj. apply pred_dec_true. rewrite (alloc_result _ _ _ _ _ H). auto. Qed. @@ -4259,7 +4259,7 @@ Proof. intros; red. exploit store_mapped_inj. eauto. eauto. apply flat_inj_no_overlap. unfold flat_inj. apply pred_dec_true; auto. eauto. - replace (ofs + 0) with ofs by omega. + replace (ofs + 0) with ofs by lia. intros [m'' [A B]]. congruence. Qed. @@ -4306,7 +4306,7 @@ Lemma valid_block_unchanged_on: forall m m' b, unchanged_on m m' -> valid_block m b -> valid_block m' b. Proof. - unfold valid_block; intros. apply unchanged_on_nextblock in H. xomega. + unfold valid_block; intros. apply unchanged_on_nextblock in H. extlia. Qed. Lemma perm_unchanged_on: @@ -4349,7 +4349,7 @@ Proof. + unfold loadbytes. destruct H. destruct (range_perm_dec m b ofs (ofs + n) Cur Readable). rewrite pred_dec_true. f_equal. - apply getN_exten. intros. rewrite Z2Nat.id in H by omega. + apply getN_exten. intros. rewrite Z2Nat.id in H by lia. apply unchanged_on_contents0; auto. red; intros. apply unchanged_on_perm0; auto. rewrite pred_dec_false. auto. @@ -4367,7 +4367,7 @@ Proof. destruct (zle n 0). + erewrite loadbytes_empty in * by assumption. auto. + rewrite <- H1. apply loadbytes_unchanged_on_1; auto. - exploit loadbytes_range_perm; eauto. instantiate (1 := ofs). omega. + exploit loadbytes_range_perm; eauto. instantiate (1 := ofs). lia. intros. eauto with mem. Qed. @@ -4410,7 +4410,7 @@ Proof. rewrite encode_val_length. rewrite <- size_chunk_conv. destruct (zlt ofs0 ofs); auto. destruct (zlt ofs0 (ofs + size_chunk chunk)); auto. - elim (H0 ofs0). omega. auto. + elim (H0 ofs0). lia. auto. Qed. Lemma storebytes_unchanged_on: @@ -4426,7 +4426,7 @@ Proof. destruct (peq b0 b); auto. subst b0. apply setN_outside. destruct (zlt ofs0 ofs); auto. destruct (zlt ofs0 (ofs + Z.of_nat (length bytes))); auto. - elim (H0 ofs0). omega. auto. + elim (H0 ofs0). lia. auto. Qed. Lemma alloc_unchanged_on: @@ -4455,7 +4455,7 @@ Proof. - split; intros. eapply perm_free_1; eauto. destruct (eq_block b0 b); auto. destruct (zlt ofs lo); auto. destruct (zle hi ofs); auto. - subst b0. elim (H0 ofs). omega. auto. + subst b0. elim (H0 ofs). lia. auto. eapply perm_free_3; eauto. - unfold free in H. destruct (range_perm_dec m b lo hi Cur Freeable); inv H. simpl. auto. @@ -4473,7 +4473,7 @@ Proof. destruct (eq_block b0 b); auto. subst b0. assert (~ (lo <= ofs < hi)). { red; intros; eelim H0; eauto. } - right; omega. + right; lia. eapply perm_drop_4; eauto. - unfold drop_perm in H. destruct (range_perm_dec m b lo hi Cur Freeable); inv H; simpl. auto. diff --git a/common/Separation.v b/common/Separation.v index 27065d1f..0357b2bf 100644 --- a/common/Separation.v +++ b/common/Separation.v @@ -355,12 +355,12 @@ Proof. intros. rewrite <- sep_assoc. eapply sep_imp; eauto. split; simpl; intros. - intuition auto. -+ omega. -+ apply H5; omega. -+ omega. -+ apply H5; omega. -+ red; simpl; intros; omega. -- intuition omega. ++ lia. ++ apply H5; lia. ++ lia. ++ apply H5; lia. ++ red; simpl; intros; lia. +- intuition lia. Qed. Lemma range_drop_left: @@ -392,12 +392,12 @@ Proof. assert (mid <= align mid al) by (apply align_le; auto). split; simpl; intros. - intuition auto. -+ omega. -+ apply H7; omega. -+ omega. -+ apply H7; omega. -+ red; simpl; intros; omega. -- intuition omega. ++ lia. ++ apply H7; lia. ++ lia. ++ apply H7; lia. ++ red; simpl; intros; lia. +- intuition lia. Qed. Lemma range_preserved: @@ -493,7 +493,7 @@ Proof. split; [|split]. - assert (Mem.valid_access m chunk b ofs Freeable). { split; auto. red; auto. } - split. generalize (size_chunk_pos chunk). unfold Ptrofs.max_unsigned. omega. + split. generalize (size_chunk_pos chunk). unfold Ptrofs.max_unsigned. lia. split. auto. + destruct (Mem.valid_access_load m chunk b ofs) as [v LOAD]. eauto with mem. @@ -616,7 +616,7 @@ Next Obligation. assert (IMG: forall b1 b2 delta ofs k p, j b1 = Some (b2, delta) -> Mem.perm m0 b1 ofs k p -> img b2 (ofs + delta)). { intros. red. exists b1, delta; split; auto. - replace (ofs + delta - delta) with ofs by omega. + replace (ofs + delta - delta) with ofs by lia. eauto with mem. } destruct H. constructor. - destruct mi_inj. constructor; intros. @@ -668,7 +668,7 @@ Proof. intros; red; intros. eelim C; eauto. simpl. exists b1, delta; split; auto. destruct VALID as [V1 V2]. apply Mem.perm_cur_max. apply Mem.perm_implies with Writable; auto with mem. - apply V1. omega. + apply V1. lia. - red; simpl; intros. destruct H1 as (b0 & delta0 & U & V). eelim C; eauto. simpl. exists b0, delta0; eauto with mem. Qed. @@ -690,7 +690,7 @@ Lemma alloc_parallel_rule: /\ (forall b, b <> b1 -> j' b = j b). Proof. intros until delta; intros SEP ALLOC1 ALLOC2 ALIGN LO HI RANGE1 RANGE2 RANGE3. - assert (RANGE4: lo <= hi) by xomega. + assert (RANGE4: lo <= hi) by extlia. assert (FRESH1: ~Mem.valid_block m1 b1) by (eapply Mem.fresh_block_alloc; eauto). assert (FRESH2: ~Mem.valid_block m2 b2) by (eapply Mem.fresh_block_alloc; eauto). destruct SEP as (INJ & SP & DISJ). simpl in INJ. @@ -698,10 +698,10 @@ Proof. - eapply Mem.alloc_right_inject; eauto. - eexact ALLOC1. - instantiate (1 := b2). eauto with mem. -- instantiate (1 := delta). xomega. -- intros. assert (0 <= ofs < sz2) by (eapply Mem.perm_alloc_3; eauto). omega. +- instantiate (1 := delta). extlia. +- intros. assert (0 <= ofs < sz2) by (eapply Mem.perm_alloc_3; eauto). lia. - intros. apply Mem.perm_implies with Freeable; auto with mem. - eapply Mem.perm_alloc_2; eauto. xomega. + eapply Mem.perm_alloc_2; eauto. extlia. - red; intros. apply Z.divide_trans with 8; auto. exists (8 / align_chunk chunk). destruct chunk; reflexivity. - intros. elim FRESH2. eapply Mem.valid_block_inject_2; eauto. @@ -709,19 +709,19 @@ Proof. exists j'; split; auto. rewrite <- ! sep_assoc. split; [|split]. -+ simpl. intuition auto; try (unfold Ptrofs.max_unsigned in *; omega). ++ simpl. intuition auto; try (unfold Ptrofs.max_unsigned in *; lia). * apply Mem.perm_implies with Freeable; auto with mem. - eapply Mem.perm_alloc_2; eauto. omega. + eapply Mem.perm_alloc_2; eauto. lia. * apply Mem.perm_implies with Freeable; auto with mem. - eapply Mem.perm_alloc_2; eauto. omega. -* red; simpl; intros. destruct H1, H2. omega. + eapply Mem.perm_alloc_2; eauto. lia. +* red; simpl; intros. destruct H1, H2. lia. * red; simpl; intros. assert (b = b2) by tauto. subst b. assert (0 <= ofs < lo \/ hi <= ofs < sz2) by tauto. clear H1. destruct H2 as (b0 & delta0 & D & E). eapply Mem.perm_alloc_inv in E; eauto. destruct (eq_block b0 b1). - subst b0. rewrite J2 in D. inversion D; clear D; subst delta0. xomega. + subst b0. rewrite J2 in D. inversion D; clear D; subst delta0. extlia. rewrite J3 in D by auto. elim FRESH2. eapply Mem.valid_block_inject_2; eauto. + apply (m_invar P) with m2; auto. eapply Mem.alloc_unchanged_on; eauto. + red; simpl; intros. @@ -753,11 +753,11 @@ Proof. simpl in E. assert (PERM: Mem.range_perm m2 b2 0 sz2 Cur Freeable). { red; intros. - destruct (zlt ofs lo). apply J; omega. - destruct (zle hi ofs). apply K; omega. - replace ofs with ((ofs - delta) + delta) by omega. + destruct (zlt ofs lo). apply J; lia. + destruct (zle hi ofs). apply K; lia. + replace ofs with ((ofs - delta) + delta) by lia. eapply Mem.perm_inject; eauto. - eapply Mem.free_range_perm; eauto. xomega. + eapply Mem.free_range_perm; eauto. extlia. } destruct (Mem.range_perm_free _ _ _ _ PERM) as [m2' FREE]. exists m2'; split; auto. split; [|split]. @@ -768,16 +768,16 @@ Proof. destruct (zle hi (ofs + delta0)). intuition auto. destruct (eq_block b0 b1). * subst b0. rewrite H1 in H; inversion H; clear H; subst delta0. - eelim (Mem.perm_free_2 m1); eauto. xomega. + eelim (Mem.perm_free_2 m1); eauto. extlia. * exploit Mem.mi_no_overlap; eauto. apply Mem.perm_max with k. apply Mem.perm_implies with p; auto with mem. eapply Mem.perm_free_3; eauto. apply Mem.perm_cur_max. apply Mem.perm_implies with Freeable; auto with mem. eapply (Mem.free_range_perm m1); eauto. - instantiate (1 := ofs + delta0 - delta). xomega. - intros [X|X]. congruence. omega. + instantiate (1 := ofs + delta0 - delta). extlia. + intros [X|X]. congruence. lia. + simpl. exists b0, delta0; split; auto. - replace (ofs + delta0 - delta0) with ofs by omega. + replace (ofs + delta0 - delta0) with ofs by lia. apply Mem.perm_max with k. apply Mem.perm_implies with p; auto with mem. eapply Mem.perm_free_3; eauto. - apply (m_invar P) with m2; auto. @@ -787,7 +787,7 @@ Proof. destruct (zle hi i). intuition auto. right; exists b1, delta; split; auto. apply Mem.perm_cur_max. apply Mem.perm_implies with Freeable; auto with mem. - eapply Mem.free_range_perm; eauto. xomega. + eapply Mem.free_range_perm; eauto. extlia. - red; simpl; intros. eelim C; eauto. simpl. right. destruct H as (b0 & delta0 & U & V). exists b0, delta0; split; auto. diff --git a/common/Smallstep.v b/common/Smallstep.v index 27ad0a2d..5ac67c96 100644 --- a/common/Smallstep.v +++ b/common/Smallstep.v @@ -893,8 +893,8 @@ Proof. exploit (sd_traces DET). eexact H3. intros L2. assert (t1 = t0 /\ t2 = t3). destruct t1. inv MT. auto. - destruct t1; simpl in L1; try omegaContradiction. - destruct t0. inv MT. destruct t0; simpl in L2; try omegaContradiction. + destruct t1; simpl in L1; try extlia. + destruct t0. inv MT. destruct t0; simpl in L2; try extlia. simpl in H5. split. congruence. congruence. destruct H1; subst. assert (s2 = s4) by (eapply sd_determ_2; eauto). subst s4. @@ -974,7 +974,7 @@ Proof. destruct C as [P | [P Q]]; auto using lex_ord_left. + exploit sd_determ_3. eauto. eexact A. eauto. intros [P Q]; subst t s1'0. exists (i, n), s2; split; auto. - right; split. apply star_refl. apply lex_ord_right. omega. + right; split. apply star_refl. apply lex_ord_right. lia. - exact public_preserved. Qed. @@ -1256,7 +1256,7 @@ Proof. subst t. assert (EITHER: t1 = E0 \/ t2 = E0). unfold Eapp in H2; rewrite app_length in H2. - destruct t1; auto. destruct t2; auto. simpl in H2; omegaContradiction. + destruct t1; auto. destruct t2; auto. simpl in H2; extlia. destruct EITHER; subst. exploit IHstar; eauto. intros [s2x [s2y [A [B C]]]]. exists s2x; exists s2y; intuition. eapply star_left; eauto. @@ -1305,7 +1305,7 @@ Proof. - (* 1 L2 makes one or several transitions *) assert (EITHER: t = E0 \/ (length t = 1)%nat). { exploit L3_single_events; eauto. - destruct t; auto. destruct t; auto. simpl. intros. omegaContradiction. } + destruct t; auto. destruct t; auto. simpl. intros. extlia. } destruct EITHER. + (* 1.1 these are silent transitions *) subst t. exploit (bsim_E0_plus S12); eauto. @@ -1473,7 +1473,7 @@ Remark not_silent_length: forall t1 t2, (length (t1 ** t2) <= 1)%nat -> t1 = E0 \/ t2 = E0. Proof. unfold Eapp, E0; intros. rewrite app_length in H. - destruct t1; destruct t2; auto. simpl in H. omegaContradiction. + destruct t1; destruct t2; auto. simpl in H. extlia. Qed. Lemma f2b_determinacy_inv: @@ -1622,7 +1622,7 @@ Proof. intros [[EQ1 [EQ2 EQ3]] | [NOT1 [NOT2 MT]]]. + (* 2.1 L2 makes a silent transition: remain in "before" state *) subst. simpl in *. exists (F2BI_before n0); exists s1; split. - right; split. apply star_refl. constructor. omega. + right; split. apply star_refl. constructor. lia. econstructor; eauto. eapply star_right; eauto. + (* 2.2 L2 make a non-silent transition *) exploit not_silent_length. eapply (sr_traces L1_receptive); eauto. intros [EQ | EQ]. @@ -1650,7 +1650,7 @@ Proof. exploit f2b_determinacy_inv. eexact H2. eexact STEP2. intros [[EQ1 [EQ2 EQ3]] | [NOT1 [NOT2 MT]]]. subst. exists (F2BI_after n); exists s1; split. - right; split. apply star_refl. constructor; omega. + right; split. apply star_refl. constructor; lia. eapply f2b_match_after'; eauto. congruence. Qed. @@ -1763,7 +1763,7 @@ Proof. destruct IHstar as [s2x [A B]]. exists s2x; split; auto. eapply plus_left. eauto. apply plus_star; eauto. auto. destruct t1. simpl in *. subst t. exists s2; split; auto. apply plus_one; auto. - simpl in LEN. omegaContradiction. + simpl in LEN. extlia. Qed. Lemma ffs_simulation: @@ -1955,7 +1955,7 @@ Proof. assert (t2 = ev :: nil). inv H1; simpl in H0; tauto. subst t2. exists (t, s0). constructor; auto. simpl; auto. (* single-event *) - red. intros. inv H0; simpl; omega. + red. intros. inv H0; simpl; lia. Qed. (** * Connections with big-step semantics *) diff --git a/common/Subtyping.v b/common/Subtyping.v index 26b282e0..f1047d45 100644 --- a/common/Subtyping.v +++ b/common/Subtyping.v @@ -222,7 +222,7 @@ Definition weight_bounds (ob: option bounds) : nat := Lemma weight_bounds_1: forall lo hi s, weight_bounds (Some (B lo hi s)) < weight_bounds None. Proof. - intros; simpl. generalize (T.weight_range hi); omega. + intros; simpl. generalize (T.weight_range hi); lia. Qed. Lemma weight_bounds_2: @@ -233,8 +233,8 @@ Proof. intros; simpl. generalize (T.weight_sub _ _ s1) (T.weight_sub _ _ s2) (T.weight_sub _ _ H) (T.weight_sub _ _ H0); intros. destruct H1. - assert (T.weight lo2 < T.weight lo1) by (apply T.weight_sub_strict; auto). omega. - assert (T.weight hi1 < T.weight hi2) by (apply T.weight_sub_strict; auto). omega. + assert (T.weight lo2 < T.weight lo1) by (apply T.weight_sub_strict; auto). lia. + assert (T.weight hi1 < T.weight hi2) by (apply T.weight_sub_strict; auto). lia. Qed. Hint Resolve T.sub_refl: ty. @@ -250,11 +250,11 @@ Lemma weight_type_move: Proof. unfold type_move; intros. destruct (peq r1 r2). - inv H. split; auto. split; intros. omega. discriminate. + inv H. split; auto. split; intros. lia. discriminate. destruct (te_typ e)!r1 as [[lo1 hi1 s1]|] eqn:E1; destruct (te_typ e)!r2 as [[lo2 hi2 s2]|] eqn:E2. - destruct (T.sub_dec hi1 lo2). - inv H. split; auto. split; intros. omega. discriminate. + inv H. split; auto. split; intros. lia. discriminate. destruct (T.sub_dec lo1 hi2); try discriminate. set (lo2' := T.lub lo1 lo2) in *. set (hi1' := T.glb hi1 hi2) in *. @@ -264,45 +264,45 @@ Proof. set (b2 := B lo2' hi2 (T.lub_min lo1 lo2 hi2 s s2)) in *. Local Opaque weight_bounds. destruct (T.eq lo2 lo2'); destruct (T.eq hi1 hi1'); inversion H; clear H; subst changed e'; simpl. -+ split; auto. split; intros. omega. discriminate. ++ split; auto. split; intros. lia. discriminate. + assert (weight_bounds (Some b1) < weight_bounds (Some (B lo1 hi1 s1))) by (apply weight_bounds_2; auto with ty). split; auto. split; intros. - rewrite PTree.gsspec. destruct (peq r r1). subst r. rewrite E1. omega. omega. - rewrite PTree.gss. rewrite PTree.gso by auto. rewrite E2. omega. + rewrite PTree.gsspec. destruct (peq r r1). subst r. rewrite E1. lia. lia. + rewrite PTree.gss. rewrite PTree.gso by auto. rewrite E2. lia. + assert (weight_bounds (Some b2) < weight_bounds (Some (B lo2 hi2 s2))) by (apply weight_bounds_2; auto with ty). split; auto. split; intros. - rewrite PTree.gsspec. destruct (peq r r2). subst r. rewrite E2. omega. omega. - rewrite PTree.gss. rewrite PTree.gso by auto. rewrite E1. omega. + rewrite PTree.gsspec. destruct (peq r r2). subst r. rewrite E2. lia. lia. + rewrite PTree.gss. rewrite PTree.gso by auto. rewrite E1. lia. + assert (weight_bounds (Some b1) < weight_bounds (Some (B lo1 hi1 s1))) by (apply weight_bounds_2; auto with ty). assert (weight_bounds (Some b2) < weight_bounds (Some (B lo2 hi2 s2))) by (apply weight_bounds_2; auto with ty). split; auto. split; intros. rewrite ! PTree.gsspec. - destruct (peq r r2). subst r. rewrite E2. omega. - destruct (peq r r1). subst r. rewrite E1. omega. - omega. - rewrite PTree.gss. rewrite PTree.gso by auto. rewrite PTree.gss. omega. + destruct (peq r r2). subst r. rewrite E2. lia. + destruct (peq r r1). subst r. rewrite E1. lia. + lia. + rewrite PTree.gss. rewrite PTree.gso by auto. rewrite PTree.gss. lia. - set (b2 := B lo1 (T.high_bound lo1) (T.high_bound_sub lo1)) in *. assert (weight_bounds (Some b2) < weight_bounds None) by (apply weight_bounds_1). inv H; simpl. split. destruct (T.sub_dec hi1 lo1); auto. split; intros. - rewrite PTree.gsspec. destruct (peq r r2). subst r; rewrite E2; omega. omega. - rewrite PTree.gss. rewrite PTree.gso by auto. rewrite E1. omega. + rewrite PTree.gsspec. destruct (peq r r2). subst r; rewrite E2; lia. lia. + rewrite PTree.gss. rewrite PTree.gso by auto. rewrite E1. lia. - set (b1 := B (T.low_bound hi2) hi2 (T.low_bound_sub hi2)) in *. assert (weight_bounds (Some b1) < weight_bounds None) by (apply weight_bounds_1). inv H; simpl. split. destruct (T.sub_dec hi2 lo2); auto. split; intros. - rewrite PTree.gsspec. destruct (peq r r1). subst r; rewrite E1; omega. omega. - rewrite PTree.gss. rewrite PTree.gso by auto. rewrite E2. omega. + rewrite PTree.gsspec. destruct (peq r r1). subst r; rewrite E1; lia. lia. + rewrite PTree.gss. rewrite PTree.gso by auto. rewrite E2. lia. -- inv H. split; auto. simpl; split; intros. omega. congruence. +- inv H. split; auto. simpl; split; intros. lia. congruence. Qed. Definition weight_constraints (b: PTree.t bounds) (cstr: list constraint) : nat := @@ -312,7 +312,7 @@ Remark weight_constraints_tighter: forall b1 b2, (forall r, weight_bounds b1!r <= weight_bounds b2!r) -> forall q, weight_constraints b1 q <= weight_constraints b2 q. Proof. - induction q; simpl. omega. generalize (H (fst a)) (H (snd a)); omega. + induction q; simpl. lia. generalize (H (fst a)) (H (snd a)); lia. Qed. Lemma weight_solve_rec: @@ -323,8 +323,8 @@ Lemma weight_solve_rec: <= weight_constraints e.(te_typ) e.(te_sub) + weight_constraints e.(te_typ) q. Proof. induction q; simpl; intros. -- inv H. split. intros; omega. replace (changed' && negb changed') with false. - omega. destruct changed'; auto. +- inv H. split. intros; lia. replace (changed' && negb changed') with false. + lia. destruct changed'; auto. - destruct a as [r1 r2]; monadInv H; simpl. rename x into changed1. rename x0 into e1. exploit weight_type_move; eauto. intros [A [B C]]. @@ -336,7 +336,7 @@ Proof. assert (Q: weight_constraints (te_typ e1) (te_sub e1) <= weight_constraints (te_typ e1) (te_sub e) + weight_bounds (te_typ e1)!r1 + weight_bounds (te_typ e1)!r2). - { destruct A as [Q|Q]; rewrite Q. omega. simpl. omega. } + { destruct A as [Q|Q]; rewrite Q. lia. simpl. lia. } assert (R: weight_constraints (te_typ e1) q <= weight_constraints (te_typ e) q) by (apply weight_constraints_tighter; auto). set (ch1 := if changed' && negb (changed || changed1) then 1 else 0) in *. @@ -344,11 +344,11 @@ Proof. destruct changed1. assert (ch2 <= ch1 + 1). { unfold ch2, ch1. rewrite orb_true_r. simpl. rewrite andb_false_r. - destruct (changed' && negb changed); omega. } - exploit C; eauto. omega. + destruct (changed' && negb changed); lia. } + exploit C; eauto. lia. assert (ch2 <= ch1). - { unfold ch2, ch1. rewrite orb_false_r. omega. } - generalize (B r1) (B r2); omega. + { unfold ch2, ch1. rewrite orb_false_r. lia. } + generalize (B r1) (B r2); lia. Qed. Definition weight_typenv (e: typenv) : nat := @@ -364,7 +364,7 @@ Function solve_constraints (e: typenv) {measure weight_typenv e}: res typenv := end. Proof. intros. exploit weight_solve_rec; eauto. simpl. intros [A B]. - unfold weight_typenv. omega. + unfold weight_typenv. lia. Qed. Definition typassign := positive -> T.t. diff --git a/common/Switch.v b/common/Switch.v index 5a6d4c63..748aa459 100644 --- a/common/Switch.v +++ b/common/Switch.v @@ -235,8 +235,8 @@ Proof. destruct (split_lt n cases) as [lc rc] eqn:SEQ. rewrite (IHcases lc rc) by auto. destruct (zlt key n); intros EQ; inv EQ; simpl. -+ destruct (zeq v key). rewrite zlt_true by omega. auto. auto. -+ destruct (zeq v key). rewrite zlt_false by omega. auto. auto. ++ destruct (zeq v key). rewrite zlt_true by lia. auto. auto. ++ destruct (zeq v key). rewrite zlt_false by lia. auto. auto. Qed. Lemma split_between_prop: @@ -269,12 +269,12 @@ Lemma validate_jumptable_correct_rec: list_nth_z tbl v = Some(ZMap.get (base + v) cases). Proof. induction tbl; simpl; intros. -- unfold list_length_z in H0. simpl in H0. omegaContradiction. +- unfold list_length_z in H0. simpl in H0. extlia. - InvBooleans. rewrite list_length_z_cons in H0. apply beq_nat_true in H1. destruct (zeq v 0). - + replace (base + v) with base by omega. congruence. - + replace (base + v) with (Z.succ base + Z.pred v) by omega. - apply IHtbl. auto. omega. + + replace (base + v) with base by lia. congruence. + + replace (base + v) with (Z.succ base + Z.pred v) by lia. + apply IHtbl. auto. lia. Qed. Lemma validate_jumptable_correct: @@ -288,12 +288,12 @@ Lemma validate_jumptable_correct: Proof. intros. rewrite (validate_jumptable_correct_rec cases tbl ofs); auto. -- f_equal. f_equal. rewrite Z.mod_small. omega. - destruct (zle ofs v). omega. +- f_equal. f_equal. rewrite Z.mod_small. lia. + destruct (zle ofs v). lia. assert (M: ((v - ofs) + 1 * modulus) mod modulus = (v - ofs) + modulus). - { rewrite Z.mod_small. omega. omega. } - rewrite Z_mod_plus in M by auto. rewrite M in H0. omega. -- generalize (Z_mod_lt (v - ofs) modulus modulus_pos). omega. + { rewrite Z.mod_small. lia. lia. } + rewrite Z_mod_plus in M by auto. rewrite M in H0. lia. +- generalize (Z_mod_lt (v - ofs) modulus modulus_pos). lia. Qed. Lemma validate_correct_rec: @@ -309,7 +309,7 @@ Proof. destruct cases as [ | [key1 act1] cases1]; intros. + apply beq_nat_true in H. subst act. reflexivity. + InvBooleans. apply beq_nat_true in H2. subst. simpl. - destruct (zeq v hi). auto. omegaContradiction. + destruct (zeq v hi). auto. extlia. - (* eq node *) destruct (split_eq key cases) as [optact others] eqn:EQ. intros. destruct optact as [act1|]; InvBooleans; try discriminate. @@ -319,19 +319,19 @@ Proof. + congruence. + eapply IHt; eauto. unfold refine_low_bound, refine_high_bound. split. - destruct (zeq key lo); omega. - destruct (zeq key hi); omega. + destruct (zeq key lo); lia. + destruct (zeq key hi); lia. - (* lt node *) destruct (split_lt key cases) as [lcases rcases] eqn:EQ; intros; InvBooleans. rewrite (split_lt_prop v default _ _ _ _ EQ). destruct (zlt v key). - eapply IHt1. eauto. omega. - eapply IHt2. eauto. omega. + eapply IHt1. eauto. lia. + eapply IHt2. eauto. lia. - (* jumptable node *) destruct (split_between default ofs sz cases) as [ins outs] eqn:EQ; intros; InvBooleans. rewrite (split_between_prop v _ _ _ _ _ _ EQ). - assert (0 <= (v - ofs) mod modulus < modulus) by (apply Z_mod_lt; omega). + assert (0 <= (v - ofs) mod modulus < modulus) by (apply Z_mod_lt; lia). destruct (zlt ((v - ofs) mod modulus) sz). - rewrite Z.mod_small by omega. eapply validate_jumptable_correct; eauto. + rewrite Z.mod_small by lia. eapply validate_jumptable_correct; eauto. eapply IHt; eauto. Qed. @@ -346,7 +346,7 @@ Theorem validate_switch_correct: Proof. unfold validate_switch, table_tree_agree; split. eapply validate_wf; eauto. - intros; eapply validate_correct_rec; eauto. omega. + intros; eapply validate_correct_rec; eauto. lia. Qed. End COMPTREE. diff --git a/common/Unityping.v b/common/Unityping.v index 28bcfb5c..878e5943 100644 --- a/common/Unityping.v +++ b/common/Unityping.v @@ -126,12 +126,12 @@ Lemma length_move: length e'.(te_equ) + (if changed then 1 else 0) <= S(length e.(te_equ)). Proof. unfold move; intros. - destruct (peq r1 r2). inv H. omega. + destruct (peq r1 r2). inv H. lia. destruct e.(te_typ)!r1 as [ty1|]; destruct e.(te_typ)!r2 as [ty2|]; inv H; simpl. - destruct (T.eq ty1 ty2); inv H1. omega. - omega. - omega. - omega. + destruct (T.eq ty1 ty2); inv H1. lia. + lia. + lia. + lia. Qed. Lemma length_solve_rec: @@ -140,14 +140,14 @@ Lemma length_solve_rec: length e'.(te_equ) + (if ch' && negb ch then 1 else 0) <= length e.(te_equ) + length q. Proof. induction q; simpl; intros. -- inv H. replace (ch' && negb ch') with false. omega. destruct ch'; auto. +- inv H. replace (ch' && negb ch') with false. lia. destruct ch'; auto. - destruct a as [r1 r2]; monadInv H. rename x0 into e0. rename x into ch0. exploit IHq; eauto. intros A. exploit length_move; eauto. intros B. set (X := (if ch' && negb (ch || ch0) then 1 else 0)) in *. set (Y := (if ch0 then 1 else 0)) in *. set (Z := (if ch' && negb ch then 1 else 0)) in *. - cut (Z <= X + Y). intros. omega. + cut (Z <= X + Y). intros. lia. unfold X, Y, Z. destruct ch'; destruct ch; destruct ch0; simpl; auto. Qed. @@ -164,7 +164,7 @@ Function solve_constraints (e: typenv) {measure weight_typenv e}: res typenv := end. Proof. intros. exploit length_solve_rec; eauto. simpl. intros. - unfold weight_typenv. omega. + unfold weight_typenv. lia. Qed. Definition typassign := positive -> T.t. diff --git a/common/Values.v b/common/Values.v index 68a2054b..c5b07e2f 100644 --- a/common/Values.v +++ b/common/Values.v @@ -1024,10 +1024,10 @@ Lemma load_result_rettype: forall chunk v, has_rettype (load_result chunk v) (rettype_of_chunk chunk). Proof. intros. unfold has_rettype; destruct chunk; destruct v; simpl; auto. -- rewrite Int.sign_ext_idem by omega; auto. -- rewrite Int.zero_ext_idem by omega; auto. -- rewrite Int.sign_ext_idem by omega; auto. -- rewrite Int.zero_ext_idem by omega; auto. +- rewrite Int.sign_ext_idem by lia; auto. +- rewrite Int.zero_ext_idem by lia; auto. +- rewrite Int.sign_ext_idem by lia; auto. +- rewrite Int.zero_ext_idem by lia; auto. - destruct Archi.ptr64 eqn:SF; simpl; auto. - destruct Archi.ptr64 eqn:SF; simpl; auto. - destruct Archi.ptr64 eqn:SF; simpl; auto. @@ -1053,14 +1053,14 @@ Theorem cast8unsigned_and: forall x, zero_ext 8 x = and x (Vint(Int.repr 255)). Proof. destruct x; simpl; auto. decEq. - change 255 with (two_p 8 - 1). apply Int.zero_ext_and. omega. + change 255 with (two_p 8 - 1). apply Int.zero_ext_and. lia. Qed. Theorem cast16unsigned_and: forall x, zero_ext 16 x = and x (Vint(Int.repr 65535)). Proof. destruct x; simpl; auto. decEq. - change 65535 with (two_p 16 - 1). apply Int.zero_ext_and. omega. + change 65535 with (two_p 16 - 1). apply Int.zero_ext_and. lia. Qed. Theorem bool_of_val_of_bool: @@ -1297,7 +1297,7 @@ Proof. unfold divs. rewrite Int.eq_false; try discriminate. simpl. rewrite (Int.eq_false Int.one Int.mone); try discriminate. rewrite andb_false_intro2; auto. f_equal. f_equal. - rewrite Int.divs_one; auto. replace Int.zwordsize with 32; auto. omega. + rewrite Int.divs_one; auto. replace Int.zwordsize with 32; auto. lia. Qed. Theorem divu_pow2: @@ -1424,7 +1424,7 @@ Proof. destruct (Int.ltu i0 (Int.repr 31)) eqn:?; inv H1. exploit Int.ltu_inv; eauto. change (Int.unsigned (Int.repr 31)) with 31. intros. assert (Int.ltu i0 Int.iwordsize = true). - unfold Int.ltu. apply zlt_true. change (Int.unsigned Int.iwordsize) with 32. omega. + unfold Int.ltu. apply zlt_true. change (Int.unsigned Int.iwordsize) with 32. lia. simpl. rewrite H0. simpl. decEq. rewrite Int.shrx_carry; auto. Qed. @@ -1439,7 +1439,7 @@ Proof. destruct (Int.ltu i0 (Int.repr 31)) eqn:?; inv H1. exploit Int.ltu_inv; eauto. change (Int.unsigned (Int.repr 31)) with 31. intros. assert (Int.ltu i0 Int.iwordsize = true). - unfold Int.ltu. apply zlt_true. change (Int.unsigned Int.iwordsize) with 32. omega. + unfold Int.ltu. apply zlt_true. change (Int.unsigned Int.iwordsize) with 32. lia. exists i; exists i0; intuition. rewrite Int.shrx_shr; auto. destruct (Int.lt i Int.zero); simpl; rewrite H0; auto. Qed. @@ -1462,12 +1462,12 @@ Proof. replace (Int.ltu (Int.sub (Int.repr 32) n) Int.iwordsize) with true. simpl. replace (Int.ltu n Int.iwordsize) with true. f_equal; apply Int.shrx_shr_2; assumption. - symmetry; apply zlt_true. change (Int.unsigned n < 32); omega. + symmetry; apply zlt_true. change (Int.unsigned n < 32); lia. symmetry; apply zlt_true. unfold Int.sub. change (Int.unsigned (Int.repr 32)) with 32. assert (Int.unsigned n <> 0). { red; intros; elim H. rewrite <- (Int.repr_unsigned n), H0. auto. } rewrite Int.unsigned_repr. - change (Int.unsigned Int.iwordsize) with 32; omega. - assert (32 < Int.max_unsigned) by reflexivity. omega. + change (Int.unsigned Int.iwordsize) with 32; lia. + assert (32 < Int.max_unsigned) by reflexivity. lia. Qed. Theorem or_rolm: @@ -1657,7 +1657,7 @@ Proof. rewrite (Int64.eq_false Int64.one Int64.mone); try discriminate. rewrite andb_false_intro2; auto. simpl. f_equal. f_equal. apply Int64.divs_one. - replace Int64.zwordsize with 64; auto. omega. + replace Int64.zwordsize with 64; auto. lia. Qed. Theorem divlu_pow2: @@ -1700,7 +1700,7 @@ Proof. destruct (Int.ltu i0 (Int.repr 63)) eqn:?; inv H1. exploit Int.ltu_inv; eauto. change (Int.unsigned (Int.repr 63)) with 63. intros. assert (Int.ltu i0 Int64.iwordsize' = true). - unfold Int.ltu. apply zlt_true. change (Int.unsigned Int64.iwordsize') with 64. omega. + unfold Int.ltu. apply zlt_true. change (Int.unsigned Int64.iwordsize') with 64. lia. simpl. rewrite H0. simpl. decEq. rewrite Int64.shrx'_carry; auto. Qed. @@ -1721,12 +1721,12 @@ Proof. replace (Int.ltu (Int.sub (Int.repr 64) n) Int64.iwordsize') with true. simpl. replace (Int.ltu n Int64.iwordsize') with true. f_equal; apply Int64.shrx'_shr_2; assumption. - symmetry; apply zlt_true. change (Int.unsigned n < 64); omega. + symmetry; apply zlt_true. change (Int.unsigned n < 64); lia. symmetry; apply zlt_true. unfold Int.sub. change (Int.unsigned (Int.repr 64)) with 64. assert (Int.unsigned n <> 0). { red; intros; elim H. rewrite <- (Int.repr_unsigned n), H0. auto. } rewrite Int.unsigned_repr. - change (Int.unsigned Int64.iwordsize') with 64; omega. - assert (64 < Int.max_unsigned) by reflexivity. omega. + change (Int.unsigned Int64.iwordsize') with 64; lia. + assert (64 < Int.max_unsigned) by reflexivity. lia. Qed. Theorem negate_cmp_bool: -- cgit