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/Events.v | 54 +++++++++++++++++++++++++++--------------------------- 1 file changed, 27 insertions(+), 27 deletions(-) (limited to 'common/Events.v') 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) *) -- cgit From fc82b6c80fd3feeb4ef9478e6faa16b5b1104593 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Thu, 21 Jan 2021 15:44:09 +0100 Subject: Qualify `Hint` as `Global Hint` where appropriate This avoids a new warning of Coq 8.13. Eventually these `Global Hint` should become `#[export] Hint`, with a cleaner but different meaning than `Global Hint`. --- common/Events.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'common/Events.v') diff --git a/common/Events.v b/common/Events.v index ee2d529d..aae0662c 100644 --- a/common/Events.v +++ b/common/Events.v @@ -1697,7 +1697,7 @@ Qed. End EVAL_BUILTIN_ARG. -Hint Constructors eval_builtin_arg: barg. +Global Hint Constructors eval_builtin_arg: barg. (** Invariance by change of global environment. *) -- cgit