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`. --- cfrontend/Initializersproof.v | 36 ++++++++++++++++++------------------ 1 file changed, 18 insertions(+), 18 deletions(-) (limited to 'cfrontend/Initializersproof.v') diff --git a/cfrontend/Initializersproof.v b/cfrontend/Initializersproof.v index 272b929f..10ccbeff 100644 --- a/cfrontend/Initializersproof.v +++ b/cfrontend/Initializersproof.v @@ -561,7 +561,7 @@ Local Opaque sizeof. + destruct (zeq sz 0). inv TR. exists (@nil init_data); split; auto. constructor. destruct (zle 0 sz). - inv TR. econstructor; split. constructor. omega. auto. + inv TR. econstructor; split. constructor. lia. auto. discriminate. + monadInv TR. destruct (transl_init_rec_spec _ _ _ _ EQ) as (d1 & A1 & B1). @@ -672,8 +672,8 @@ Remark padding_size: forall frm to, frm <= to -> idlsize (tr_padding frm to) = to - frm. Proof. unfold tr_padding; intros. destruct (zlt frm to). - simpl. xomega. - simpl. omega. + simpl. extlia. + simpl. lia. Qed. Remark idlsize_app: @@ -681,7 +681,7 @@ Remark idlsize_app: Proof. induction d1; simpl; intros. auto. - rewrite IHd1. omega. + rewrite IHd1. lia. Qed. Remark union_field_size: @@ -690,8 +690,8 @@ Proof. induction fl as [|[i t]]; simpl; intros. - inv H. - destruct (ident_eq f i). - + inv H. xomega. - + specialize (IHfl H). xomega. + + inv H. extlia. + + specialize (IHfl H). extlia. Qed. Hypothesis ce_consistent: composite_env_consistent ge. @@ -712,16 +712,16 @@ with tr_init_struct_size: Proof. Local Opaque sizeof. - destruct 1; simpl. -+ erewrite transl_init_single_size by eauto. omega. ++ erewrite transl_init_single_size by eauto. lia. + Local Transparent sizeof. simpl. eapply tr_init_array_size; eauto. -+ replace (idlsize d) with (idlsize d + 0) by omega. ++ replace (idlsize d) with (idlsize d + 0) by lia. eapply tr_init_struct_size; eauto. simpl. unfold lookup_composite in H. destruct (ge.(genv_cenv)!id) as [co'|] eqn:?; inv H. erewrite co_consistent_sizeof by (eapply ce_consistent; eauto). unfold sizeof_composite. rewrite H0. apply align_le. destruct (co_alignof_two_p co) as [n EQ]. rewrite EQ. apply two_power_nat_pos. + rewrite idlsize_app, padding_size. - exploit tr_init_size; eauto. intros EQ; rewrite EQ. omega. + exploit tr_init_size; eauto. intros EQ; rewrite EQ. lia. simpl. unfold lookup_composite in H. destruct (ge.(genv_cenv)!id) as [co'|] eqn:?; inv H. apply Z.le_trans with (sizeof_union ge (co_members co)). eapply union_field_size; eauto. @@ -730,21 +730,21 @@ Local Opaque sizeof. destruct (co_alignof_two_p co) as [n EQ]. rewrite EQ. apply two_power_nat_pos. - destruct 1; simpl. -+ omega. ++ lia. + rewrite Z.mul_comm. assert (0 <= sizeof ge ty * sz). - { apply Zmult_gt_0_le_0_compat. omega. generalize (sizeof_pos ge ty); omega. } - xomega. + { apply Zmult_gt_0_le_0_compat. lia. generalize (sizeof_pos ge ty); lia. } + extlia. + rewrite idlsize_app. erewrite tr_init_size by eauto. erewrite tr_init_array_size by eauto. ring. - destruct 1; simpl; intros. -+ rewrite padding_size by auto. omega. ++ rewrite padding_size by auto. lia. + rewrite ! idlsize_app, padding_size. erewrite tr_init_size by eauto. - rewrite <- (tr_init_struct_size _ _ _ _ _ H0 H1). omega. + rewrite <- (tr_init_struct_size _ _ _ _ _ H0 H1). lia. unfold pos1. apply align_le. apply alignof_pos. Qed. @@ -806,7 +806,7 @@ Remark exec_init_array_length: forall m b ofs ty sz il m', exec_init_array m b ofs ty sz il m' -> sz >= 0. Proof. - induction 1; omega. + induction 1; lia. Qed. Lemma store_init_data_list_app: @@ -847,10 +847,10 @@ Local Opaque sizeof. inv H3. simpl. erewrite transl_init_single_steps by eauto. auto. - (* array *) inv H1. replace (Z.max 0 sz) with sz in H7. eauto. - assert (sz >= 0) by (eapply exec_init_array_length; eauto). xomega. + assert (sz >= 0) by (eapply exec_init_array_length; eauto). extlia. - (* struct *) inv H3. unfold lookup_composite in H7. rewrite H in H7. inv H7. - replace ofs with (ofs + 0) by omega. eauto. + replace ofs with (ofs + 0) by lia. eauto. - (* union *) inv H4. unfold lookup_composite in H9. rewrite H in H9. inv H9. rewrite H1 in H12; inv H12. eapply store_init_data_list_app. eauto. @@ -870,7 +870,7 @@ Local Opaque sizeof. inv H4. simpl in H3; inv H3. eapply store_init_data_list_app. apply store_init_data_list_padding. rewrite padding_size. - replace (ofs + pos0 + (pos2 - pos0)) with (ofs + pos2) by omega. + replace (ofs + pos0 + (pos2 - pos0)) with (ofs + pos2) by lia. eapply store_init_data_list_app. eauto. rewrite (tr_init_size _ _ _ H9). -- cgit