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/Memdata.v | 62 ++++++++++++++++++++++++++++---------------------------- 1 file changed, 31 insertions(+), 31 deletions(-) (limited to 'common/Memdata.v') diff --git a/common/Memdata.v b/common/Memdata.v index f3016efe..05a3d4ed 100644 --- a/common/Memdata.v +++ b/common/Memdata.v @@ -47,7 +47,7 @@ Definition size_chunk (chunk: memory_chunk) : Z := Lemma size_chunk_pos: forall chunk, size_chunk chunk > 0. Proof. - intros. destruct chunk; simpl; omega. + intros. destruct chunk; simpl; lia. Qed. Definition size_chunk_nat (chunk: memory_chunk) : nat := @@ -65,7 +65,7 @@ Proof. intros. generalize (size_chunk_pos chunk). rewrite size_chunk_conv. destruct (size_chunk_nat chunk). - simpl; intros; omegaContradiction. + simpl; intros; extlia. intros; exists n; auto. Qed. @@ -101,7 +101,7 @@ Definition align_chunk (chunk: memory_chunk) : Z := Lemma align_chunk_pos: forall chunk, align_chunk chunk > 0. Proof. - intro. destruct chunk; simpl; omega. + intro. destruct chunk; simpl; lia. Qed. Lemma align_chunk_Mptr: align_chunk Mptr = if Archi.ptr64 then 8 else 4. @@ -120,7 +120,7 @@ Lemma align_le_divides: align_chunk chunk1 <= align_chunk chunk2 -> (align_chunk chunk1 | align_chunk chunk2). Proof. intros. destruct chunk1; destruct chunk2; simpl in *; - solve [ omegaContradiction + solve [ extlia | apply Z.divide_refl | exists 2; reflexivity | exists 4; reflexivity @@ -216,12 +216,12 @@ Proof. simpl. rewrite Zmod_1_r. auto. Opaque Byte.wordsize. rewrite Nat2Z.inj_succ. simpl. - replace (Z.succ (Z.of_nat n) * 8) with (Z.of_nat n * 8 + 8) by omega. - rewrite two_p_is_exp; try omega. + replace (Z.succ (Z.of_nat n) * 8) with (Z.of_nat n * 8 + 8) by lia. + rewrite two_p_is_exp; try lia. rewrite Zmod_recombine. rewrite IHn. rewrite Z.add_comm. change (Byte.unsigned (Byte.repr x)) with (Byte.Z_mod_modulus x). rewrite Byte.Z_mod_modulus_eq. reflexivity. - apply two_p_gt_ZERO. omega. apply two_p_gt_ZERO. omega. + apply two_p_gt_ZERO. lia. apply two_p_gt_ZERO. lia. Qed. Lemma rev_if_be_involutive: @@ -280,15 +280,15 @@ Proof. intros; simpl; auto. intros until y. rewrite Nat2Z.inj_succ. - replace (Z.succ (Z.of_nat n) * 8) with (Z.of_nat n * 8 + 8) by omega. - rewrite two_p_is_exp; try omega. + replace (Z.succ (Z.of_nat n) * 8) with (Z.of_nat n * 8 + 8) by lia. + rewrite two_p_is_exp; try lia. intro EQM. simpl; decEq. apply Byte.eqm_samerepr. red. eapply eqmod_divides; eauto. apply Z.divide_factor_r. apply IHn. destruct EQM as [k EQ]. exists k. rewrite EQ. - rewrite <- Z_div_plus_full_l. decEq. change (two_p 8) with 256. ring. omega. + rewrite <- Z_div_plus_full_l. decEq. change (two_p 8) with 256. ring. lia. Qed. Lemma encode_int_8_mod: @@ -517,9 +517,9 @@ Ltac solve_decode_encode_val_general := | |- context [ Int.repr(decode_int (encode_int 2 (Int.unsigned _))) ] => rewrite decode_encode_int_2 | |- context [ Int.repr(decode_int (encode_int 4 (Int.unsigned _))) ] => rewrite decode_encode_int_4 | |- context [ Int64.repr(decode_int (encode_int 8 (Int64.unsigned _))) ] => rewrite decode_encode_int_8 - | |- Vint (Int.sign_ext _ (Int.sign_ext _ _)) = Vint _ => f_equal; apply Int.sign_ext_idem; omega - | |- Vint (Int.zero_ext _ (Int.zero_ext _ _)) = Vint _ => f_equal; apply Int.zero_ext_idem; omega - | |- Vint (Int.sign_ext _ (Int.zero_ext _ _)) = Vint _ => f_equal; apply Int.sign_ext_zero_ext; omega + | |- Vint (Int.sign_ext _ (Int.sign_ext _ _)) = Vint _ => f_equal; apply Int.sign_ext_idem; lia + | |- Vint (Int.zero_ext _ (Int.zero_ext _ _)) = Vint _ => f_equal; apply Int.zero_ext_idem; lia + | |- Vint (Int.sign_ext _ (Int.zero_ext _ _)) = Vint _ => f_equal; apply Int.sign_ext_zero_ext; lia end. Lemma decode_encode_val_general: @@ -543,7 +543,7 @@ Lemma decode_encode_val_similar: v2 = Val.load_result chunk2 v1. Proof. intros until v2; intros TY SZ DE. - destruct chunk1; destruct chunk2; simpl in TY; try discriminate; simpl in SZ; try omegaContradiction; + destruct chunk1; destruct chunk2; simpl in TY; try discriminate; simpl in SZ; try extlia; destruct v1; auto. Qed. @@ -553,7 +553,7 @@ Lemma decode_val_rettype: Proof. intros. unfold decode_val. destruct (proj_bytes cl). -- destruct chunk; simpl; rewrite ? Int.sign_ext_idem, ? Int.zero_ext_idem by omega; auto. +- destruct chunk; simpl; rewrite ? Int.sign_ext_idem, ? Int.zero_ext_idem by lia; auto. - Local Opaque Val.load_result. destruct chunk; simpl; (exact I || apply Val.load_result_type || destruct Archi.ptr64; (exact I || apply Val.load_result_type)). @@ -653,7 +653,7 @@ Proof. exists j, mv = Fragment v q j /\ S j <> size_quantity_nat q). { induction n; simpl; intros. contradiction. destruct H0. - exists n; split; auto. omega. apply IHn; auto. omega. + exists n; split; auto. lia. apply IHn; auto. lia. } assert (B: forall q, q = quantity_chunk chunk -> @@ -663,7 +663,7 @@ Proof. Local Transparent inj_value. intros. unfold inj_value. destruct (size_quantity_nat_pos q) as [sz' EQ']. rewrite EQ'. simpl. constructor; auto. - intros; eapply A; eauto. omega. + intros; eapply A; eauto. lia. } assert (C: forall bl, match v with Vint _ => True | Vlong _ => True | Vfloat _ => True | Vsingle _ => True | _ => False end -> @@ -719,8 +719,8 @@ Proof. induction n; destruct mvs; simpl; intros; try discriminate. contradiction. destruct m; try discriminate. InvBooleans. apply beq_nat_true in H4. subst. - destruct H0. subst mv. exists n0; split; auto. omega. - eapply IHn; eauto. omega. + destruct H0. subst mv. exists n0; split; auto. lia. + eapply IHn; eauto. lia. } assert (U: forall mvs, shape_decoding chunk mvs (Val.load_result chunk Vundef)). { @@ -740,7 +740,7 @@ Proof. simpl. apply beq_nat_true in EQN. subst n q0. constructor. auto. destruct H0 as [E|[E|[E|E]]]; subst chunk; destruct q; auto || discriminate. congruence. - intros. eapply B; eauto. omega. + intros. eapply B; eauto. lia. } unfold decode_val. destruct (proj_bytes (mv1 :: mvl)) as [bl|] eqn:PB. @@ -955,22 +955,22 @@ Proof. induction l1; simpl int_of_bytes; intros. simpl. ring. simpl length. rewrite Nat2Z.inj_succ. - replace (Z.succ (Z.of_nat (length l1)) * 8) with (Z.of_nat (length l1) * 8 + 8) by omega. + replace (Z.succ (Z.of_nat (length l1)) * 8) with (Z.of_nat (length l1) * 8 + 8) by lia. rewrite two_p_is_exp. change (two_p 8) with 256. rewrite IHl1. ring. - omega. omega. + lia. lia. Qed. Lemma int_of_bytes_range: forall l, 0 <= int_of_bytes l < two_p (Z.of_nat (length l) * 8). Proof. induction l; intros. - simpl. omega. + simpl. lia. simpl length. rewrite Nat2Z.inj_succ. - replace (Z.succ (Z.of_nat (length l)) * 8) with (Z.of_nat (length l) * 8 + 8) by omega. + replace (Z.succ (Z.of_nat (length l)) * 8) with (Z.of_nat (length l) * 8 + 8) by lia. rewrite two_p_is_exp. change (two_p 8) with 256. simpl int_of_bytes. generalize (Byte.unsigned_range a). - change Byte.modulus with 256. omega. - omega. omega. + change Byte.modulus with 256. lia. + lia. lia. Qed. Lemma length_proj_bytes: @@ -1014,7 +1014,7 @@ Proof. intros. apply Int.unsigned_repr. generalize (int_of_bytes_range l). rewrite H2. change (two_p (Z.of_nat 4 * 8)) with (Int.max_unsigned + 1). - omega. + lia. apply Val.lessdef_same. unfold decode_int, rev_if_be. destruct Archi.big_endian; rewrite B1; rewrite B2. + rewrite <- (rev_length b1) in L1. @@ -1036,18 +1036,18 @@ Lemma bytes_of_int_append: bytes_of_int n1 x1 ++ bytes_of_int n2 x2. Proof. induction n1; intros. -- simpl in *. f_equal. omega. +- simpl in *. f_equal. lia. - assert (E: two_p (Z.of_nat (S n1) * 8) = two_p (Z.of_nat n1 * 8) * 256). { rewrite Nat2Z.inj_succ. change 256 with (two_p 8). rewrite <- two_p_is_exp. - f_equal. omega. omega. omega. + f_equal. lia. lia. lia. } rewrite E in *. simpl. f_equal. apply Byte.eqm_samerepr. exists (x2 * two_p (Z.of_nat n1 * 8)). change Byte.modulus with 256. ring. rewrite Z.mul_assoc. rewrite Z_div_plus. apply IHn1. - apply Zdiv_interval_1. omega. apply two_p_gt_ZERO; omega. omega. - assumption. omega. + apply Zdiv_interval_1. lia. apply two_p_gt_ZERO; lia. lia. + assumption. lia. Qed. Lemma bytes_of_int64: -- cgit