diff options
author | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2020-06-21 18:22:00 +0200 |
---|---|---|
committer | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2020-12-29 15:29:56 +0100 |
commit | aba0e740f25ffa5c338dfa76cab71144802cebc2 (patch) | |
tree | 746115009aa60b802a2b5369a5106a2e971eb22f /aarch64/Conventions1.v | |
parent | 2e202e2b17cc3ae909628b7b3ae0b8ede3117d82 (diff) | |
download | compcert-aba0e740f25ffa5c338dfa76cab71144802cebc2.tar.gz compcert-aba0e740f25ffa5c338dfa76cab71144802cebc2.zip |
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`.
Diffstat (limited to 'aarch64/Conventions1.v')
-rw-r--r-- | aarch64/Conventions1.v | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/aarch64/Conventions1.v b/aarch64/Conventions1.v index 4873dd91..cfcbcbf1 100644 --- a/aarch64/Conventions1.v +++ b/aarch64/Conventions1.v @@ -274,33 +274,33 @@ Proof. assert (ALP: forall ofs ty, ofs >= 0 -> align ofs (typesize ty) >= 0). { intros. assert (ofs <= align ofs (typesize ty)) by (apply align_le; apply typesize_pos). - omega. } + lia. } assert (ALD: forall ofs ty, ofs >= 0 -> (typealign ty | align ofs (typesize ty))). { intros. apply Z.divide_trans with (typesize ty). apply typealign_typesize. apply align_divides. apply typesize_pos. } assert (ALP2: forall ofs, ofs >= 0 -> align ofs 2 >= 0). { intros. - assert (ofs <= align ofs 2) by (apply align_le; omega). - omega. } + assert (ofs <= align ofs 2) by (apply align_le; lia). + lia. } assert (ALD2: forall ofs ty, ofs >= 0 -> (typealign ty | align ofs 2)). { intros. eapply Z.divide_trans with 2. exists (2 / typealign ty). destruct ty; reflexivity. - apply align_divides. omega. } + apply align_divides. lia. } assert (STK: forall tyl ofs, ofs >= 0 -> OK (loc_arguments_stack tyl ofs)). { induction tyl as [ | ty tyl]; intros ofs OO; red; simpl; intros. - contradiction. - destruct H. + subst p. split. auto. simpl. apply Z.divide_1_l. - + apply IHtyl with (ofs := ofs + 2). omega. auto. + + apply IHtyl with (ofs := ofs + 2). lia. auto. } assert (A: forall ty ri rf ofs f, OKF f -> ofs >= 0 -> OK (stack_arg ty ri rf ofs f)). { intros until f; intros OF OO; red; unfold stack_arg; intros. destruct Archi.abi; destruct H. - subst p; simpl; auto. - - eapply OF; [|eauto]. apply ALP2 in OO. omega. + - eapply OF; [|eauto]. apply ALP2 in OO. lia. - subst p; simpl; auto. - - eapply OF; [|eauto]. apply (ALP ofs ty) in OO. generalize (typesize_pos ty). omega. + - eapply OF; [|eauto]. apply (ALP ofs ty) in OO. generalize (typesize_pos ty). lia. } assert (B: forall ty ri rf ofs f, OKF f -> ofs >= 0 -> OK (int_arg ty ri rf ofs f)). @@ -332,7 +332,7 @@ Lemma loc_arguments_acceptable: In p (loc_arguments s) -> forall_rpair loc_argument_acceptable p. Proof. unfold loc_arguments; intros. - eapply loc_arguments_rec_charact; eauto. omega. + eapply loc_arguments_rec_charact; eauto. lia. Qed. Hint Resolve loc_arguments_acceptable: locs. |