From fc82b6c80fd3feeb4ef9478e6faa16b5b1104593 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Thu, 21 Jan 2021 15:44:09 +0100 Subject: Qualify `Hint` as `Global Hint` where appropriate This avoids a new warning of Coq 8.13. Eventually these `Global Hint` should become `#[export] Hint`, with a cleaner but different meaning than `Global Hint`. --- lib/Coqlib.v | 20 ++++++++++---------- lib/Integers.v | 47 +++++++++++++++++++++++++---------------------- lib/Intv.v | 2 +- 3 files changed, 36 insertions(+), 33 deletions(-) (limited to 'lib') diff --git a/lib/Coqlib.v b/lib/Coqlib.v index ae9dceec..bd52d20a 100644 --- a/lib/Coqlib.v +++ b/lib/Coqlib.v @@ -116,7 +116,7 @@ Lemma Plt_ne: Proof. unfold Plt; intros. red; intro. subst y. eelim Pos.lt_irrefl; eauto. Qed. -Hint Resolve Plt_ne: coqlib. +Global Hint Resolve Plt_ne: coqlib. Lemma Plt_trans: forall (x y z: positive), Plt x y -> Plt y z -> Plt x z. @@ -127,14 +127,14 @@ Lemma Plt_succ: Proof. unfold Plt; intros. apply Pos.lt_succ_r. apply Pos.le_refl. Qed. -Hint Resolve Plt_succ: coqlib. +Global Hint Resolve Plt_succ: coqlib. Lemma Plt_trans_succ: forall (x y: positive), Plt x y -> Plt x (Pos.succ y). Proof. intros. apply Plt_trans with y. assumption. apply Plt_succ. Qed. -Hint Resolve Plt_succ: coqlib. +Global Hint Resolve Plt_succ: coqlib. Lemma Plt_succ_inv: forall (x y: positive), Plt x (Pos.succ y) -> Plt x y \/ x = y. @@ -175,7 +175,7 @@ Proof (Pos.lt_le_trans). Lemma Plt_strict: forall p, ~ Plt p p. Proof (Pos.lt_irrefl). -Hint Resolve Ple_refl Plt_Ple Ple_succ Plt_strict: coqlib. +Global Hint Resolve Ple_refl Plt_Ple Ple_succ Plt_strict: coqlib. Ltac extlia := unfold Plt, Ple in *; lia. @@ -559,7 +559,7 @@ Definition sum_left_map (A B C: Type) (f: A -> B) (x: A + C) : B + C := (** Properties of [List.nth] (n-th element of a list). *) -Hint Resolve in_eq in_cons: coqlib. +Global Hint Resolve in_eq in_cons: coqlib. Lemma nth_error_in: forall (A: Type) (n: nat) (l: list A) (x: A), @@ -573,14 +573,14 @@ Proof. discriminate. apply in_cons. auto. Qed. -Hint Resolve nth_error_in: coqlib. +Global Hint Resolve nth_error_in: coqlib. Lemma nth_error_nil: forall (A: Type) (idx: nat), nth_error (@nil A) idx = None. Proof. induction idx; simpl; intros; reflexivity. Qed. -Hint Resolve nth_error_nil: coqlib. +Global Hint Resolve nth_error_nil: coqlib. (** Compute the length of a list, with result in [Z]. *) @@ -671,7 +671,7 @@ Lemma incl_cons_inv: Proof. unfold incl; intros. apply H. apply in_cons. auto. Qed. -Hint Resolve incl_cons_inv: coqlib. +Global Hint Resolve incl_cons_inv: coqlib. Lemma incl_app_inv_l: forall (A: Type) (l1 l2 m: list A), @@ -687,7 +687,7 @@ Proof. unfold incl; intros. apply H. apply in_or_app. right; assumption. Qed. -Hint Resolve incl_tl incl_refl incl_app_inv_l incl_app_inv_r: coqlib. +Global Hint Resolve incl_tl incl_refl incl_app_inv_l incl_app_inv_r: coqlib. Lemma incl_same_head: forall (A: Type) (x: A) (l1 l2: list A), @@ -1042,7 +1042,7 @@ Proof. constructor. constructor. constructor. auto. Qed. -Hint Resolve is_tail_refl is_tail_cons is_tail_in is_tail_cons_left: coqlib. +Global Hint Resolve is_tail_refl is_tail_cons is_tail_in is_tail_cons_left: coqlib. Lemma is_tail_incl: forall (A: Type) (l1 l2: list A), is_tail l1 l2 -> incl l1 l2. diff --git a/lib/Integers.v b/lib/Integers.v index 03f19c98..9368b531 100644 --- a/lib/Integers.v +++ b/lib/Integers.v @@ -91,7 +91,7 @@ Proof. generalize modulus_gt_one; lia. Qed. -Hint Resolve modulus_pos: ints. +Global Hint Resolve modulus_pos: ints. (** * Representation of machine integers *) @@ -400,45 +400,45 @@ Definition eqm := eqmod modulus. Lemma eqm_refl: forall x, eqm x x. Proof (eqmod_refl modulus). -Hint Resolve eqm_refl: ints. +Global Hint Resolve eqm_refl: ints. Lemma eqm_refl2: forall x y, x = y -> eqm x y. Proof (eqmod_refl2 modulus). -Hint Resolve eqm_refl2: ints. +Global Hint Resolve eqm_refl2: ints. Lemma eqm_sym: forall x y, eqm x y -> eqm y x. Proof (eqmod_sym modulus). -Hint Resolve eqm_sym: ints. +Global Hint Resolve eqm_sym: ints. Lemma eqm_trans: forall x y z, eqm x y -> eqm y z -> eqm x z. Proof (eqmod_trans modulus). -Hint Resolve eqm_trans: ints. +Global Hint Resolve eqm_trans: ints. Lemma eqm_small_eq: forall x y, eqm x y -> 0 <= x < modulus -> 0 <= y < modulus -> x = y. Proof (eqmod_small_eq modulus). -Hint Resolve eqm_small_eq: ints. +Global Hint Resolve eqm_small_eq: ints. Lemma eqm_add: forall a b c d, eqm a b -> eqm c d -> eqm (a + c) (b + d). Proof (eqmod_add modulus). -Hint Resolve eqm_add: ints. +Global Hint Resolve eqm_add: ints. Lemma eqm_neg: forall x y, eqm x y -> eqm (-x) (-y). Proof (eqmod_neg modulus). -Hint Resolve eqm_neg: ints. +Global Hint Resolve eqm_neg: ints. Lemma eqm_sub: forall a b c d, eqm a b -> eqm c d -> eqm (a - c) (b - d). Proof (eqmod_sub modulus). -Hint Resolve eqm_sub: ints. +Global Hint Resolve eqm_sub: ints. Lemma eqm_mult: forall a b c d, eqm a c -> eqm b d -> eqm (a * b) (c * d). Proof (eqmod_mult modulus). -Hint Resolve eqm_mult: ints. +Global Hint Resolve eqm_mult: ints. Lemma eqm_same_bits: forall x y, @@ -466,7 +466,7 @@ Lemma eqm_unsigned_repr: Proof. unfold eqm; intros. rewrite unsigned_repr_eq. apply eqmod_mod. auto with ints. Qed. -Hint Resolve eqm_unsigned_repr: ints. +Global Hint Resolve eqm_unsigned_repr: ints. Lemma eqm_unsigned_repr_l: forall a b, eqm a b -> eqm (unsigned (repr a)) b. @@ -474,7 +474,7 @@ Proof. intros. apply eqm_trans with a. apply eqm_sym. apply eqm_unsigned_repr. auto. Qed. -Hint Resolve eqm_unsigned_repr_l: ints. +Global Hint Resolve eqm_unsigned_repr_l: ints. Lemma eqm_unsigned_repr_r: forall a b, eqm a b -> eqm a (unsigned (repr b)). @@ -482,7 +482,7 @@ Proof. intros. apply eqm_trans with b. auto. apply eqm_unsigned_repr. Qed. -Hint Resolve eqm_unsigned_repr_r: ints. +Global Hint Resolve eqm_unsigned_repr_r: ints. Lemma eqm_signed_unsigned: forall x, eqm (signed x) (unsigned x). @@ -497,7 +497,7 @@ Theorem unsigned_range: Proof. destruct i. simpl. lia. Qed. -Hint Resolve unsigned_range: ints. +Global Hint Resolve unsigned_range: ints. Theorem unsigned_range_2: forall i, 0 <= unsigned i <= max_unsigned. @@ -505,7 +505,7 @@ Proof. intro; unfold max_unsigned. generalize (unsigned_range i). lia. Qed. -Hint Resolve unsigned_range_2: ints. +Global Hint Resolve unsigned_range_2: ints. Theorem signed_range: forall i, min_signed <= signed i <= max_signed. @@ -524,7 +524,7 @@ Proof. destruct i; simpl. unfold repr. apply mkint_eq. rewrite Z_mod_modulus_eq. apply Z.mod_small; lia. Qed. -Hint Resolve repr_unsigned: ints. +Global Hint Resolve repr_unsigned: ints. Lemma repr_signed: forall i, repr (signed i) = i. @@ -532,7 +532,7 @@ Proof. intros. transitivity (repr (unsigned i)). apply eqm_samerepr. apply eqm_signed_unsigned. auto with ints. Qed. -Hint Resolve repr_signed: ints. +Global Hint Resolve repr_signed: ints. Opaque repr. @@ -547,7 +547,7 @@ Proof. intros. rewrite unsigned_repr_eq. apply Z.mod_small. unfold max_unsigned in H. lia. Qed. -Hint Resolve unsigned_repr: ints. +Global Hint Resolve unsigned_repr: ints. Theorem signed_repr: forall z, min_signed <= z <= max_signed -> signed (repr z) = z. @@ -4802,7 +4802,7 @@ Qed. End AGREE64. -Hint Resolve +Global Hint Resolve agree32_repr agree32_of_int agree32_of_ints agree32_of_int_eq agree32_of_ints_eq agree32_to_int agree32_to_int_eq agree32_neg agree32_add agree32_sub agree32_mul agree32_divs agree64_repr agree64_of_int agree64_of_int_eq @@ -4816,19 +4816,22 @@ Notation ptrofs := Ptrofs.int. Global Opaque Ptrofs.repr. -Hint Resolve Int.modulus_pos Int.eqm_refl Int.eqm_refl2 Int.eqm_sym Int.eqm_trans +Global Hint Resolve + Int.modulus_pos Int.eqm_refl Int.eqm_refl2 Int.eqm_sym Int.eqm_trans Int.eqm_small_eq Int.eqm_add Int.eqm_neg Int.eqm_sub Int.eqm_mult Int.eqm_unsigned_repr Int.eqm_unsigned_repr_l Int.eqm_unsigned_repr_r Int.unsigned_range Int.unsigned_range_2 Int.repr_unsigned Int.repr_signed Int.unsigned_repr : ints. -Hint Resolve Int64.modulus_pos Int64.eqm_refl Int64.eqm_refl2 Int64.eqm_sym Int64.eqm_trans +Global Hint Resolve + Int64.modulus_pos Int64.eqm_refl Int64.eqm_refl2 Int64.eqm_sym Int64.eqm_trans Int64.eqm_small_eq Int64.eqm_add Int64.eqm_neg Int64.eqm_sub Int64.eqm_mult Int64.eqm_unsigned_repr Int64.eqm_unsigned_repr_l Int64.eqm_unsigned_repr_r Int64.unsigned_range Int64.unsigned_range_2 Int64.repr_unsigned Int64.repr_signed Int64.unsigned_repr : ints. -Hint Resolve Ptrofs.modulus_pos Ptrofs.eqm_refl Ptrofs.eqm_refl2 Ptrofs.eqm_sym Ptrofs.eqm_trans +Global Hint Resolve + Ptrofs.modulus_pos Ptrofs.eqm_refl Ptrofs.eqm_refl2 Ptrofs.eqm_sym Ptrofs.eqm_trans Ptrofs.eqm_small_eq Ptrofs.eqm_add Ptrofs.eqm_neg Ptrofs.eqm_sub Ptrofs.eqm_mult Ptrofs.eqm_unsigned_repr Ptrofs.eqm_unsigned_repr_l Ptrofs.eqm_unsigned_repr_r Ptrofs.unsigned_range Ptrofs.unsigned_range_2 diff --git a/lib/Intv.v b/lib/Intv.v index 19943942..82d3c751 100644 --- a/lib/Intv.v +++ b/lib/Intv.v @@ -303,7 +303,7 @@ Qed. (** Hints *) -Hint Resolve +Global Hint Resolve notin_range range_notin is_notempty empty_notin in_notempty disjoint_sym empty_disjoint_r empty_disjoint_l -- cgit