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`. --- riscV/Asmgenproof1.v | 20 ++++++++++---------- 1 file changed, 10 insertions(+), 10 deletions(-) (limited to 'riscV/Asmgenproof1.v') diff --git a/riscV/Asmgenproof1.v b/riscV/Asmgenproof1.v index c20c4e49..253e769f 100644 --- a/riscV/Asmgenproof1.v +++ b/riscV/Asmgenproof1.v @@ -35,7 +35,7 @@ Proof. - set (m := Int.sub n lo). assert (A: eqmod (two_p 12) (Int.unsigned lo) (Int.unsigned n)) by (apply Int.eqmod_sign_ext'; compute; auto). assert (B: eqmod (two_p 12) (Int.unsigned n - Int.unsigned lo) 0). - { replace 0 with (Int.unsigned n - Int.unsigned n) by omega. + { replace 0 with (Int.unsigned n - Int.unsigned n) by lia. auto using eqmod_sub, eqmod_refl. } assert (C: eqmod (two_p 12) (Int.unsigned m) 0). { apply eqmod_trans with (Int.unsigned n - Int.unsigned lo); auto. @@ -45,7 +45,7 @@ Proof. { apply eqmod_mod_eq in C. unfold Int.modu. change (Int.unsigned (Int.repr 4096)) with (two_p 12). rewrite C. reflexivity. - apply two_p_gt_ZERO; omega. } + apply two_p_gt_ZERO; lia. } rewrite <- (Int.divu_pow2 m (Int.repr 4096) (Int.repr 12)) by auto. rewrite Int.shl_mul_two_p. change (two_p (Int.unsigned (Int.repr 12))) with 4096. @@ -684,18 +684,18 @@ Proof. unfold Val.cmp; destruct (rs#r1); simpl; auto. rewrite B1. unfold Int.lt. rewrite zlt_false. auto. change (Int.signed (Int.repr Int.max_signed)) with Int.max_signed. - generalize (Int.signed_range i); omega. + generalize (Int.signed_range i); lia. * exploit (opimm32_correct Psltw Psltiw (Val.cmp Clt)); eauto. intros (rs1 & A1 & B1 & C1). exists rs1; split. eexact A1. split; auto. rewrite B1. unfold Val.cmp; simpl; destruct (rs#r1); simpl; auto. unfold Int.lt. replace (Int.signed (Int.add n Int.one)) with (Int.signed n + 1). destruct (zlt (Int.signed n) (Int.signed i)). - rewrite zlt_false by omega. auto. - rewrite zlt_true by omega. auto. + rewrite zlt_false by lia. auto. + rewrite zlt_true by lia. auto. rewrite Int.add_signed. symmetry; apply Int.signed_repr. assert (Int.signed n <> Int.max_signed). { red; intros E. elim H1. rewrite <- (Int.repr_signed n). rewrite E. auto. } - generalize (Int.signed_range n); omega. + generalize (Int.signed_range n); lia. + apply DFL. + apply DFL. Qed. @@ -782,18 +782,18 @@ Proof. unfold Val.cmpl; destruct (rs#r1); simpl; auto. rewrite B1. unfold Int64.lt. rewrite zlt_false. auto. change (Int64.signed (Int64.repr Int64.max_signed)) with Int64.max_signed. - generalize (Int64.signed_range i); omega. + generalize (Int64.signed_range i); lia. * exploit (opimm64_correct Psltl Psltil (fun v1 v2 => Val.maketotal (Val.cmpl Clt v1 v2))); eauto. intros (rs1 & A1 & B1 & C1). exists rs1; split. eexact A1. split; auto. rewrite B1. unfold Val.cmpl; simpl; destruct (rs#r1); simpl; auto. unfold Int64.lt. replace (Int64.signed (Int64.add n Int64.one)) with (Int64.signed n + 1). destruct (zlt (Int64.signed n) (Int64.signed i)). - rewrite zlt_false by omega. auto. - rewrite zlt_true by omega. auto. + rewrite zlt_false by lia. auto. + rewrite zlt_true by lia. auto. rewrite Int64.add_signed. symmetry; apply Int64.signed_repr. assert (Int64.signed n <> Int64.max_signed). { red; intros E. elim H1. rewrite <- (Int64.repr_signed n). rewrite E. auto. } - generalize (Int64.signed_range n); omega. + generalize (Int64.signed_range n); lia. + apply DFL. + apply DFL. Qed. -- cgit