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`. --- x86/Conventions1.v | 28 ++++++++++++++-------------- 1 file changed, 14 insertions(+), 14 deletions(-) (limited to 'x86/Conventions1.v') diff --git a/x86/Conventions1.v b/x86/Conventions1.v index 645aae90..803d162a 100644 --- a/x86/Conventions1.v +++ b/x86/Conventions1.v @@ -302,14 +302,14 @@ Remark loc_arguments_32_charact: In p (loc_arguments_32 tyl ofs) -> forall_rpair (loc_argument_32_charact ofs) p. Proof. assert (X: forall ofs1 ofs2 l, loc_argument_32_charact ofs2 l -> ofs1 <= ofs2 -> loc_argument_32_charact ofs1 l). - { destruct l; simpl; intros; auto. destruct sl; auto. intuition omega. } + { destruct l; simpl; intros; auto. destruct sl; auto. intuition lia. } induction tyl as [ | ty tyl]; simpl loc_arguments_32; intros. - contradiction. - destruct H. -+ destruct ty; subst p; simpl; omega. ++ destruct ty; subst p; simpl; lia. + apply IHtyl in H. generalize (typesize_pos ty); intros. destruct p; simpl in *. -* eapply X; eauto; omega. -* destruct H; split; eapply X; eauto; omega. +* eapply X; eauto; lia. +* destruct H; split; eapply X; eauto; lia. Qed. Remark loc_arguments_elf64_charact: @@ -317,7 +317,7 @@ Remark loc_arguments_elf64_charact: In p (loc_arguments_elf64 tyl ir fr ofs) -> (2 | ofs) -> forall_rpair (loc_argument_elf64_charact ofs) p. Proof. assert (X: forall ofs1 ofs2 l, loc_argument_elf64_charact ofs2 l -> ofs1 <= ofs2 -> loc_argument_elf64_charact ofs1 l). - { destruct l; simpl; intros; auto. destruct sl; auto. intuition omega. } + { destruct l; simpl; intros; auto. destruct sl; auto. intuition lia. } assert (Y: forall ofs1 ofs2 p, forall_rpair (loc_argument_elf64_charact ofs2) p -> ofs1 <= ofs2 -> forall_rpair (loc_argument_elf64_charact ofs1) p). { destruct p; simpl; intuition eauto. } assert (Z: forall ofs, (2 | ofs) -> (2 | ofs + 2)). @@ -334,8 +334,8 @@ Opaque list_nth_z. { intros. destruct (list_nth_z int_param_regs_elf64 ir) as [r|] eqn:E; destruct H1. subst. left. eapply list_nth_z_in; eauto. eapply IHtyl; eauto. - subst. split. omega. assumption. - eapply Y; eauto. omega. } + subst. split. lia. assumption. + eapply Y; eauto. lia. } assert (B: forall ty, In p match list_nth_z float_param_regs_elf64 fr with | Some ireg => One (R ireg) :: loc_arguments_elf64 tyl ir (fr + 1) ofs @@ -345,8 +345,8 @@ Opaque list_nth_z. { intros. destruct (list_nth_z float_param_regs_elf64 fr) as [r|] eqn:E; destruct H1. subst. right. eapply list_nth_z_in; eauto. eapply IHtyl; eauto. - subst. split. omega. assumption. - eapply Y; eauto. omega. } + subst. split. lia. assumption. + eapply Y; eauto. lia. } destruct a; eauto. Qed. @@ -355,7 +355,7 @@ Remark loc_arguments_win64_charact: In p (loc_arguments_win64 tyl r ofs) -> (2 | ofs) -> forall_rpair (loc_argument_win64_charact ofs) p. Proof. assert (X: forall ofs1 ofs2 l, loc_argument_win64_charact ofs2 l -> ofs1 <= ofs2 -> loc_argument_win64_charact ofs1 l). - { destruct l; simpl; intros; auto. destruct sl; auto. intuition omega. } + { destruct l; simpl; intros; auto. destruct sl; auto. intuition lia. } assert (Y: forall ofs1 ofs2 p, forall_rpair (loc_argument_win64_charact ofs2) p -> ofs1 <= ofs2 -> forall_rpair (loc_argument_win64_charact ofs1) p). { destruct p; simpl; intuition eauto. } assert (Z: forall ofs, (2 | ofs) -> (2 | ofs + 2)). @@ -372,8 +372,8 @@ Opaque list_nth_z. { intros. destruct (list_nth_z int_param_regs_win64 r) as [r'|] eqn:E; destruct H1. subst. left. eapply list_nth_z_in; eauto. eapply IHtyl; eauto. - subst. split. omega. assumption. - eapply Y; eauto. omega. } + subst. split. lia. assumption. + eapply Y; eauto. lia. } assert (B: forall ty, In p match list_nth_z float_param_regs_win64 r with | Some ireg => One (R ireg) :: loc_arguments_win64 tyl (r + 1) ofs @@ -383,8 +383,8 @@ Opaque list_nth_z. { intros. destruct (list_nth_z float_param_regs_win64 r) as [r'|] eqn:E; destruct H1. subst. right. eapply list_nth_z_in; eauto. eapply IHtyl; eauto. - subst. split. omega. assumption. - eapply Y; eauto. omega. } + subst. split. lia. assumption. + eapply Y; eauto. lia. } destruct a; eauto. Qed. -- cgit