diff options
125 files changed, 752 insertions, 0 deletions
diff --git a/theories/Arith/Between.v b/theories/Arith/Between.v index 74d1e391c4..71c8f10755 100644 --- a/theories/Arith/Between.v +++ b/theories/Arith/Between.v @@ -24,6 +24,7 @@ Section Between. | bet_emp : between k k | bet_S : forall l, between k l -> P l -> between k (S l). + #[local] Hint Constructors between: arith. Lemma bet_eq : forall k l, l = k -> between k l. @@ -31,18 +32,21 @@ Section Between. intros * ->; auto with arith. Qed. + #[local] Hint Resolve bet_eq: arith. Lemma between_le : forall k l, between k l -> k <= l. Proof. induction 1; auto with arith. Qed. + #[local] Hint Immediate between_le: arith. Lemma between_Sk_l : forall k l, between k l -> S k <= l -> between (S k) l. Proof. induction 1 as [|* [|]]; auto with arith. Qed. + #[local] Hint Resolve between_Sk_l: arith. Lemma between_restr : @@ -57,6 +61,7 @@ Section Between. | exists_S : forall l, exists_between k l -> exists_between k (S l) | exists_le : forall l, k <= l -> Q l -> exists_between k (S l). + #[local] Hint Constructors exists_between: arith. Lemma exists_le_S : forall k l, exists_between k l -> S k <= l. @@ -66,12 +71,14 @@ Section Between. Lemma exists_lt : forall k l, exists_between k l -> k < l. Proof exists_le_S. + #[local] Hint Immediate exists_le_S exists_lt: arith. Lemma exists_S_le : forall k l, exists_between k (S l) -> k <= l. Proof. intros; apply le_S_n; auto with arith. Qed. + #[local] Hint Immediate exists_S_le: arith. Definition in_int p q r := p <= r /\ r < q. @@ -80,6 +87,7 @@ Section Between. Proof. split; assumption. Qed. + #[local] Hint Resolve in_int_intro: arith. Lemma in_int_lt : forall p q r, in_int p q r -> p < q. @@ -99,12 +107,14 @@ Section Between. Proof. intros * []; auto with arith. Qed. + #[local] Hint Resolve in_int_S: arith. Lemma in_int_Sp_q : forall p q r, in_int (S p) q r -> in_int p q r. Proof. intros * []; auto with arith. Qed. + #[local] Hint Immediate in_int_Sp_q: arith. Lemma between_in_int : @@ -188,6 +198,8 @@ Section Between. End Between. +#[global] Hint Resolve nth_O bet_S bet_emp bet_eq between_Sk_l exists_S exists_le in_int_S in_int_intro: arith. +#[global] Hint Immediate in_int_Sp_q exists_le_S exists_S_le: arith. diff --git a/theories/Arith/Div2.v b/theories/Arith/Div2.v index 2d34412908..c52edf9994 100644 --- a/theories/Arith/Div2.v +++ b/theories/Arith/Div2.v @@ -42,6 +42,7 @@ Qed. Lemma lt_div2 n : 0 < n -> div2 n < n. Proof. apply Nat.lt_div2. Qed. +#[global] Hint Resolve lt_div2: arith. (** Properties related to the parity *) @@ -73,6 +74,7 @@ Proof. symmetry in Ev'. elim (n_Sn _ Ev'). Qed. +#[global] Hint Resolve even_div2 div2_even odd_div2 div2_odd: arith. Lemma even_odd_div2 n : @@ -88,6 +90,7 @@ Qed. Notation double := Nat.double (only parsing). +#[global] Hint Unfold double Nat.double: arith. Lemma double_S n : double (S n) = S (S (double n)). @@ -100,6 +103,7 @@ Proof. apply Nat.add_shuffle1. Qed. +#[global] Hint Resolve double_S: arith. Lemma even_odd_double n : @@ -133,6 +137,7 @@ Proof proj1 (proj2 (even_odd_double n)). Lemma double_odd n : n = S (double (div2 n)) -> odd n. Proof proj2 (proj2 (even_odd_double n)). +#[global] Hint Resolve even_double double_even odd_double double_odd: arith. (** Application: diff --git a/theories/Arith/EqNat.v b/theories/Arith/EqNat.v index 593d8c5934..66678b24f8 100644 --- a/theories/Arith/EqNat.v +++ b/theories/Arith/EqNat.v @@ -27,6 +27,7 @@ Theorem eq_nat_refl n : eq_nat n n. Proof. induction n; simpl; auto. Qed. +#[global] Hint Resolve eq_nat_refl: arith. (** [eq] restricted to [nat] and [eq_nat] are equivalent *) @@ -48,6 +49,7 @@ Proof. apply eq_nat_is_eq. Qed. +#[global] Hint Immediate eq_eq_nat eq_nat_eq: arith. Theorem eq_nat_elim : diff --git a/theories/Arith/Even.v b/theories/Arith/Even.v index 3422596818..87d6a6ee64 100644 --- a/theories/Arith/Even.v +++ b/theories/Arith/Even.v @@ -31,7 +31,9 @@ Inductive even : nat -> Prop := with odd : nat -> Prop := odd_S : forall n, even n -> odd (S n). +#[global] Hint Constructors even: arith. +#[global] Hint Constructors odd: arith. (** * Equivalence with predicates [Nat.Even] and [Nat.odd] *) @@ -178,6 +180,7 @@ Proof. parity_binop. Qed. Lemma odd_mult_inv_r n m : odd (n * m) -> odd m. Proof. parity_binop. Qed. +#[global] Hint Resolve even_even_plus odd_even_plus odd_plus_l odd_plus_r even_mult_l even_mult_r even_mult_l even_mult_r odd_mult : arith. diff --git a/theories/Arith/Gt.v b/theories/Arith/Gt.v index 05d585b9a2..492aeba66b 100644 --- a/theories/Arith/Gt.v +++ b/theories/Arith/Gt.v @@ -135,13 +135,21 @@ Qed. (** * Hints *) +#[global] Hint Resolve gt_Sn_O gt_Sn_n gt_n_S : arith. +#[global] Hint Immediate gt_S_n gt_pred : arith. +#[global] Hint Resolve gt_irrefl gt_asym : arith. +#[global] Hint Resolve le_not_gt gt_not_le : arith. +#[global] Hint Immediate le_S_gt gt_S_le : arith. +#[global] Hint Resolve gt_le_S le_gt_S : arith. +#[global] Hint Resolve gt_trans_S le_gt_trans gt_le_trans: arith. +#[global] Hint Resolve plus_gt_compat_l: arith. (* begin hide *) diff --git a/theories/Arith/Le.v b/theories/Arith/Le.v index 4e71465452..3d176fb644 100644 --- a/theories/Arith/Le.v +++ b/theories/Arith/Le.v @@ -32,7 +32,9 @@ Notation le_refl := Nat.le_refl (only parsing). Notation le_trans := Nat.le_trans (only parsing). Notation le_antisym := Nat.le_antisymm (only parsing). +#[global] Hint Resolve le_trans: arith. +#[global] Hint Immediate le_antisym: arith. (** * Properties of [le] w.r.t 0 *) @@ -61,8 +63,11 @@ Notation le_Sn_n := Nat.nle_succ_diag_l (only parsing). (* ~ S n <= n *) Theorem le_Sn_le : forall n m, S n <= m -> n <= m. Proof Nat.lt_le_incl. +#[global] Hint Resolve le_0_n le_Sn_0: arith. +#[global] Hint Resolve le_n_S le_n_Sn le_Sn_n : arith. +#[global] Hint Immediate le_n_0_eq le_Sn_le le_S_n : arith. (** * Properties of [le] w.r.t predecessor *) @@ -70,6 +75,7 @@ Hint Immediate le_n_0_eq le_Sn_le le_S_n : arith. Notation le_pred_n := Nat.le_pred_l (only parsing). (* pred n <= n *) Notation le_pred := Nat.pred_le_mono (only parsing). (* n<=m -> pred n <= pred m *) +#[global] Hint Resolve le_pred_n: arith. (** * A different elimination principle for the order on natural numbers *) diff --git a/theories/Arith/Lt.v b/theories/Arith/Lt.v index 60cc361e35..467420afb3 100644 --- a/theories/Arith/Lt.v +++ b/theories/Arith/Lt.v @@ -27,6 +27,7 @@ Local Open Scope nat_scope. Notation lt_irrefl := Nat.lt_irrefl (only parsing). (* ~ x < x *) +#[global] Hint Resolve lt_irrefl: arith. (** * Relationship between [le] and [lt] *) @@ -50,8 +51,11 @@ Qed. Register le_lt_n_Sm as num.nat.le_lt_n_Sm. +#[global] Hint Immediate lt_le_S: arith. +#[global] Hint Immediate lt_n_Sm_le: arith. +#[global] Hint Immediate le_lt_n_Sm: arith. Theorem le_not_lt n m : n <= m -> ~ m < n. @@ -64,6 +68,7 @@ Proof. apply Nat.lt_nge. Qed. +#[global] Hint Immediate le_not_lt lt_not_le: arith. (** * Asymmetry *) @@ -85,7 +90,9 @@ Proof. intros. now apply Nat.neq_sym, Nat.neq_0_lt_0. Qed. +#[global] Hint Resolve lt_0_Sn lt_n_0 : arith. +#[global] Hint Immediate neq_0_lt lt_0_neq: arith. (** * Order and successor *) @@ -105,7 +112,9 @@ Qed. Register lt_S_n as num.nat.lt_S_n. +#[global] Hint Resolve lt_n_Sn lt_S lt_n_S : arith. +#[global] Hint Immediate lt_S_n : arith. (** * Predecessor *) @@ -130,7 +139,9 @@ Proof. intros. now apply Nat.lt_pred_l, Nat.neq_0_lt_0. Qed. +#[global] Hint Immediate lt_pred: arith. +#[global] Hint Resolve lt_pred_n_n: arith. (** * Transitivity properties *) @@ -141,6 +152,7 @@ Notation le_lt_trans := Nat.le_lt_trans (only parsing). Register le_lt_trans as num.nat.le_lt_trans. +#[global] Hint Resolve lt_trans lt_le_trans le_lt_trans: arith. (** * Large = strict or equal *) @@ -154,6 +166,7 @@ Qed. Notation lt_le_weak := Nat.lt_le_incl (only parsing). +#[global] Hint Immediate lt_le_weak: arith. (** * Dichotomy *) diff --git a/theories/Arith/Max.v b/theories/Arith/Max.v index 28fe51f9af..863b02ef2e 100644 --- a/theories/Arith/Max.v +++ b/theories/Arith/Max.v @@ -43,8 +43,10 @@ Notation max_case2 := max_case (only parsing). Notation max_SS := Nat.succ_max_distr (only parsing). (* end hide *) +#[global] Hint Resolve Nat.max_l Nat.max_r Nat.le_max_l Nat.le_max_r : arith. +#[global] Hint Resolve Nat.min_l Nat.min_r Nat.le_min_l Nat.le_min_r : arith. diff --git a/theories/Arith/Minus.v b/theories/Arith/Minus.v index b8c7ac147a..6cbba63e1a 100644 --- a/theories/Arith/Minus.v +++ b/theories/Arith/Minus.v @@ -111,13 +111,23 @@ Qed. (** * Hints *) +#[global] Hint Resolve minus_n_O: arith. +#[global] Hint Resolve minus_Sn_m: arith. +#[global] Hint Resolve minus_diag_reverse: arith. +#[global] Hint Resolve minus_plus_simpl_l_reverse: arith. +#[global] Hint Immediate plus_minus: arith. +#[global] Hint Resolve minus_plus: arith. +#[global] Hint Resolve le_plus_minus: arith. +#[global] Hint Resolve le_plus_minus_r: arith. +#[global] Hint Resolve lt_minus: arith. +#[global] Hint Immediate lt_O_minus_lt: arith. diff --git a/theories/Arith/Mult.v b/theories/Arith/Mult.v index d7f703e6e4..584b282f4d 100644 --- a/theories/Arith/Mult.v +++ b/theories/Arith/Mult.v @@ -33,12 +33,14 @@ Notation mult_0_r := Nat.mul_0_r (only parsing). (* n * 0 = 0 *) Notation mult_1_l := Nat.mul_1_l (only parsing). (* 1 * n = n *) Notation mult_1_r := Nat.mul_1_r (only parsing). (* n * 1 = n *) +#[global] Hint Resolve mult_1_l mult_1_r: arith. (** ** Commutativity *) Notation mult_comm := Nat.mul_comm (only parsing). (* n * m = m * n *) +#[global] Hint Resolve mult_comm: arith. (** ** Distributivity *) @@ -55,8 +57,11 @@ Notation mult_minus_distr_r := Notation mult_minus_distr_l := Nat.mul_sub_distr_l (only parsing). (* n*(m-p) = n*m - n*p *) +#[global] Hint Resolve mult_plus_distr_r: arith. +#[global] Hint Resolve mult_minus_distr_r: arith. +#[global] Hint Resolve mult_minus_distr_l: arith. (** ** Associativity *) @@ -68,7 +73,9 @@ Proof. symmetry. apply Nat.mul_assoc. Qed. +#[global] Hint Resolve mult_assoc_reverse: arith. +#[global] Hint Resolve mult_assoc: arith. (** ** Inversion lemmas *) @@ -94,12 +101,14 @@ Lemma mult_O_le n m : m = 0 \/ n <= m * n. Proof. destruct m; [left|right]; simpl; trivial using Nat.le_add_r. Qed. +#[global] Hint Resolve mult_O_le: arith. Lemma mult_le_compat_l n m p : n <= m -> p * n <= p * m. Proof. apply Nat.mul_le_mono_nonneg_l, Nat.le_0_l. (* TODO : get rid of 0<=n hyp *) Qed. +#[global] Hint Resolve mult_le_compat_l: arith. Lemma mult_le_compat_r n m p : n <= m -> n * p <= m * p. @@ -117,6 +126,7 @@ Proof. apply Nat.mul_lt_mono_pos_l, Nat.lt_0_succ. Qed. +#[global] Hint Resolve mult_S_lt_compat_l: arith. Lemma mult_lt_compat_l n m p : n < m -> 0 < p -> p * n < p * m. diff --git a/theories/Arith/PeanoNat.v b/theories/Arith/PeanoNat.v index 37704704a0..8d3b1b318a 100644 --- a/theories/Arith/PeanoNat.v +++ b/theories/Arith/PeanoNat.v @@ -765,7 +765,9 @@ Infix "?=" := Nat.compare (at level 70) : nat_scope. Infix "/" := Nat.div : nat_scope. Infix "mod" := Nat.modulo (at level 40, no associativity) : nat_scope. +#[global] Hint Unfold Nat.le : core. +#[global] Hint Unfold Nat.lt : core. Register Nat.le_trans as num.nat.le_trans. diff --git a/theories/Arith/Peano_dec.v b/theories/Arith/Peano_dec.v index 9a7a397023..2fc44ba592 100644 --- a/theories/Arith/Peano_dec.v +++ b/theories/Arith/Peano_dec.v @@ -23,6 +23,7 @@ Defined. Notation eq_nat_dec := Nat.eq_dec (only parsing). +#[global] Hint Resolve O_or_S eq_nat_dec: arith. Theorem dec_eq_nat n m : decidable (n = m). diff --git a/theories/Arith/Plus.v b/theories/Arith/Plus.v index 5da7738adc..49e242276e 100644 --- a/theories/Arith/Plus.v +++ b/theories/Arith/Plus.v @@ -179,11 +179,17 @@ Proof (succ_plus_discr n 3). (** * Compatibility Hints *) +#[global] Hint Immediate plus_comm : arith. +#[global] Hint Resolve plus_assoc plus_assoc_reverse : arith. +#[global] Hint Resolve plus_le_compat_l plus_le_compat_r : arith. +#[global] Hint Resolve le_plus_l le_plus_r le_plus_trans : arith. +#[global] Hint Immediate lt_plus_trans : arith. +#[global] Hint Resolve plus_lt_compat_l plus_lt_compat_r : arith. (** For compatibility, we "Require" the same files as before *) diff --git a/theories/Arith/Wf_nat.v b/theories/Arith/Wf_nat.v index ebd909c1dc..a87eeba9b1 100644 --- a/theories/Arith/Wf_nat.v +++ b/theories/Arith/Wf_nat.v @@ -197,7 +197,9 @@ Proof. intros n H q; pattern q; apply lt_wf_ind; auto with arith. Qed. +#[global] Hint Resolve lt_wf: arith. +#[global] Hint Resolve well_founded_lt_compat: arith. Section LT_WF_REL. diff --git a/theories/Bool/Bool.v b/theories/Bool/Bool.v index 0f62db42cf..8039c96efe 100644 --- a/theories/Bool/Bool.v +++ b/theories/Bool/Bool.v @@ -44,13 +44,16 @@ Lemma diff_true_false : true <> false. Proof. discriminate. Qed. +#[global] Hint Resolve diff_true_false : bool. Lemma diff_false_true : false <> true. Proof. discriminate. Qed. +#[global] Hint Resolve diff_false_true : bool. +#[global] Hint Extern 1 (false <> true) => exact diff_false_true : core. Lemma eq_true_false_abs : forall b:bool, b = true -> b = false -> False. @@ -87,6 +90,7 @@ Qed. | true => b2 = true | false => True end. +#[global] Hint Unfold le: bool. Lemma le_implb : forall b1 b2, le b1 b2 <-> implb b1 b2 = true. @@ -104,6 +108,7 @@ Notation leb_implb := le_implb (only parsing). | true => False | false => b2 = true end. +#[global] Hint Unfold lt: bool. #[ local ] Definition compare (b1 b2 : bool) := @@ -271,6 +276,7 @@ Lemma orb_true_intro : Proof. intros; apply orb_true_iff; trivial. Qed. +#[global] Hint Resolve orb_true_intro: bool. Lemma orb_false_intro : @@ -278,6 +284,7 @@ Lemma orb_false_intro : Proof. intros. subst. reflexivity. Qed. +#[global] Hint Resolve orb_false_intro: bool. Lemma orb_false_elim : @@ -297,6 +304,7 @@ Lemma orb_true_r : forall b:bool, b || true = true. Proof. destr_bool. Qed. +#[global] Hint Resolve orb_true_r: bool. Lemma orb_true_l : forall b:bool, true || b = true. @@ -313,12 +321,14 @@ Lemma orb_false_r : forall b:bool, b || false = b. Proof. destr_bool. Qed. +#[global] Hint Resolve orb_false_r: bool. Lemma orb_false_l : forall b:bool, false || b = b. Proof. destr_bool. Qed. +#[global] Hint Resolve orb_false_l: bool. Notation orb_b_false := orb_false_r (only parsing). @@ -330,6 +340,7 @@ Lemma orb_negb_r : forall b:bool, b || negb b = true. Proof. destr_bool. Qed. +#[global] Hint Resolve orb_negb_r: bool. Lemma orb_negb_l : forall b:bool, negb b || b = true. @@ -352,6 +363,7 @@ Lemma orb_assoc : forall b1 b2 b3:bool, b1 || (b2 || b3) = b1 || b2 || b3. Proof. destr_bool. Qed. +#[global] Hint Resolve orb_comm orb_assoc: bool. (***************************) @@ -426,6 +438,7 @@ Lemma andb_false_elim : Proof. intro b1; destruct b1; simpl; auto. Defined. +#[global] Hint Resolve andb_false_elim: bool. (** Complementation *) @@ -434,6 +447,7 @@ Lemma andb_negb_r : forall b:bool, b && negb b = false. Proof. destr_bool. Qed. +#[global] Hint Resolve andb_negb_r: bool. Lemma andb_negb_l : forall b:bool, negb b && b = false. @@ -457,6 +471,7 @@ Proof. destr_bool. Qed. +#[global] Hint Resolve andb_comm andb_assoc: bool. (*****************************************) @@ -722,6 +737,7 @@ Qed. Notation bool_6 := eq_true_not_negb (only parsing). (* Compatibility *) +#[global] Hint Resolve eq_true_not_negb : bool. (* An interesting lemma for auto but too strong to keep compatibility *) @@ -737,6 +753,7 @@ Lemma absurd_eq_true : forall b, False -> b = true. Proof. contradiction. Qed. +#[global] Hint Resolve absurd_eq_true : core. (* A specific instance of eq_trans that preserves compatibility with @@ -746,6 +763,7 @@ Lemma trans_eq_bool : forall x y z:bool, x = y -> y = z -> x = z. Proof. apply eq_trans. Qed. +#[global] Hint Resolve trans_eq_bool : core. (***************************************) @@ -754,6 +772,7 @@ Hint Resolve trans_eq_bool : core. (** [Is_true] and equality *) +#[global] Hint Unfold Is_true: bool. Lemma Is_true_eq_true : forall x:bool, Is_true x -> x = true. @@ -773,6 +792,7 @@ Qed. Notation Is_true_eq_true2 := Is_true_eq_right (only parsing). +#[global] Hint Immediate Is_true_eq_right Is_true_eq_left: bool. Lemma eqb_refl : forall x:bool, Is_true (eqb x x). @@ -806,6 +826,7 @@ Lemma andb_prop_intro : Proof. destr_bool; tauto. Qed. +#[global] Hint Resolve andb_prop_intro: bool. Notation andb_true_intro2 := @@ -817,6 +838,7 @@ Lemma andb_prop_elim : Proof. destr_bool; auto. Qed. +#[global] Hint Resolve andb_prop_elim: bool. Notation andb_prop2 := andb_prop_elim (only parsing). @@ -901,6 +923,7 @@ Qed. Inductive reflect (P : Prop) : bool -> Set := | ReflectT : P -> reflect P true | ReflectF : ~ P -> reflect P false. +#[global] Hint Constructors reflect : bool. (** Interest: a case on a reflect lemma or hyp performs clever diff --git a/theories/Bool/IfProp.v b/theories/Bool/IfProp.v index 1a41eb6bb5..7e9087c377 100644 --- a/theories/Bool/IfProp.v +++ b/theories/Bool/IfProp.v @@ -14,6 +14,7 @@ Inductive IfProp (A B:Prop) : bool -> Prop := | Iftrue : A -> IfProp A B true | Iffalse : B -> IfProp A B false. +#[global] Hint Resolve Iftrue Iffalse: bool. Lemma Iftrue_inv : forall (A B:Prop) (b:bool), IfProp A B b -> b = true -> A. diff --git a/theories/Bool/Sumbool.v b/theories/Bool/Sumbool.v index 52605a4667..49feda15ea 100644 --- a/theories/Bool/Sumbool.v +++ b/theories/Bool/Sumbool.v @@ -19,6 +19,7 @@ Definition sumbool_of_bool : forall b:bool, {b = true} + {b = false}. intros b; destruct b; auto. Defined. +#[global] Hint Resolve sumbool_of_bool: bool. Definition bool_eq_rec : @@ -57,7 +58,9 @@ Section connectives. End connectives. +#[global] Hint Resolve sumbool_and sumbool_or: core. +#[global] Hint Immediate sumbool_not : core. (** Any decidability function in type [sumbool] can be turned into a function diff --git a/theories/Bool/Zerob.v b/theories/Bool/Zerob.v index 3665a8c78d..aff5008410 100644 --- a/theories/Bool/Zerob.v +++ b/theories/Bool/Zerob.v @@ -23,6 +23,7 @@ Lemma zerob_true_intro : forall n:nat, n = 0 -> zerob n = true. Proof. destruct n; [ trivial with bool | inversion 1 ]. Qed. +#[global] Hint Resolve zerob_true_intro: bool. Lemma zerob_true_elim : forall n:nat, zerob n = true -> n = 0. @@ -34,6 +35,7 @@ Lemma zerob_false_intro : forall n:nat, n <> 0 -> zerob n = false. Proof. destruct n; [ destruct 1; auto with bool | trivial with bool ]. Qed. +#[global] Hint Resolve zerob_false_intro: bool. Lemma zerob_false_elim : forall n:nat, zerob n = false -> n <> 0. diff --git a/theories/Classes/CMorphisms.v b/theories/Classes/CMorphisms.v index 9a3a1d3709..892568c3d8 100644 --- a/theories/Classes/CMorphisms.v +++ b/theories/Classes/CMorphisms.v @@ -80,9 +80,11 @@ End Proper. (** We favor the use of Leibniz equality or a declared reflexive crelation when resolving [ProperProxy], otherwise, if the crelation is given (not an evar), we fall back to [Proper]. *) +#[global] Hint Extern 1 (ProperProxy _ _) => class_apply @eq_proper_proxy || class_apply @reflexive_proper_proxy : typeclass_instances. +#[global] Hint Extern 2 (ProperProxy ?R _) => not_evar R; class_apply @proper_proper_proxy : typeclass_instances. @@ -215,8 +217,11 @@ Typeclasses Opaque respectful pointwise_relation forall_relation. Arguments forall_relation {A P}%type sig%signature _ _. Arguments pointwise_relation A%type {B}%type R%signature _ _. +#[global] Hint Unfold Reflexive : core. +#[global] Hint Unfold Symmetric : core. +#[global] Hint Unfold Transitive : core. (** Resolution with subrelation: favor decomposing products over applying reflexivity @@ -225,6 +230,7 @@ Ltac subrelation_tac T U := (is_ground T ; is_ground U ; class_apply @subrelation_refl) || class_apply @subrelation_respectful || class_apply @subrelation_refl. +#[global] Hint Extern 3 (@subrelation _ ?T ?U) => subrelation_tac T U : typeclass_instances. CoInductive apply_subrelation : Prop := do_subrelation. @@ -234,6 +240,7 @@ Ltac proper_subrelation := [ H : apply_subrelation |- _ ] => clear H ; class_apply @subrelation_proper end. +#[global] Hint Extern 5 (@Proper _ ?H _) => proper_subrelation : typeclass_instances. (** Essential subrelation instances for [iff], [impl] and [pointwise_relation]. *) @@ -254,6 +261,7 @@ Proof. firstorder. Qed. (** We use an extern hint to help unification. *) +#[global] Hint Extern 4 (subrelation (@forall_relation ?A ?B ?R) (@forall_relation _ _ ?S)) => apply (@forall_subrelation A B R S) ; intro : typeclass_instances. @@ -526,17 +534,23 @@ Ltac proper_reflexive := end. +#[global] Hint Extern 1 (subrelation (flip _) _) => class_apply @flip1 : typeclass_instances. +#[global] Hint Extern 1 (subrelation _ (flip _)) => class_apply @flip2 : typeclass_instances. (* Hint Extern 1 (Proper _ (complement _)) => apply @complement_proper *) (* : typeclass_instances. *) +#[global] Hint Extern 1 (Proper _ (flip _)) => apply @flip_proper : typeclass_instances. +#[global] Hint Extern 2 (@Proper _ (flip _) _) => class_apply @proper_flip_proper : typeclass_instances. +#[global] Hint Extern 4 (@Proper _ _ _) => partial_application_tactic : typeclass_instances. +#[global] Hint Extern 7 (@Proper _ _ _) => proper_reflexive : typeclass_instances. @@ -586,7 +600,9 @@ Ltac proper_normalization := set(H:=did_normalization) ; class_apply @proper_normalizes_proper end. +#[global] Hint Extern 1 (Normalizes _ _ _) => normalizes : typeclass_instances. +#[global] Hint Extern 6 (@Proper _ _ _) => proper_normalization : typeclass_instances. @@ -690,6 +706,7 @@ split. + right. transitivity y; auto. Qed. +#[global] Hint Extern 4 (PreOrder (relation_disjunction _ _)) => class_apply StrictOrder_PreOrder : typeclass_instances. @@ -702,8 +719,10 @@ elim (StrictOrder_Irreflexive x). transitivity y; auto. Qed. +#[global] Hint Extern 4 (StrictOrder (relation_conjunction _ _)) => class_apply PartialOrder_StrictOrder : typeclass_instances. +#[global] Hint Extern 4 (PartialOrder _ (relation_disjunction _ _)) => class_apply StrictOrder_PartialOrder : typeclass_instances. diff --git a/theories/Classes/CRelationClasses.v b/theories/Classes/CRelationClasses.v index 72a196ca7a..236d35b68e 100644 --- a/theories/Classes/CRelationClasses.v +++ b/theories/Classes/CRelationClasses.v @@ -203,22 +203,35 @@ Defined. (** Hints to drive the typeclass resolution avoiding loops due to the use of full unification. *) +#[global] Hint Extern 1 (Reflexive (complement _)) => class_apply @irreflexivity : typeclass_instances. +#[global] Hint Extern 3 (Symmetric (complement _)) => class_apply complement_Symmetric : typeclass_instances. +#[global] Hint Extern 3 (Irreflexive (complement _)) => class_apply complement_Irreflexive : typeclass_instances. +#[global] Hint Extern 3 (Reflexive (flip _)) => apply flip_Reflexive : typeclass_instances. +#[global] Hint Extern 3 (Irreflexive (flip _)) => class_apply flip_Irreflexive : typeclass_instances. +#[global] Hint Extern 3 (Symmetric (flip _)) => class_apply flip_Symmetric : typeclass_instances. +#[global] Hint Extern 3 (Asymmetric (flip _)) => class_apply flip_Asymmetric : typeclass_instances. +#[global] Hint Extern 3 (Antisymmetric (flip _)) => class_apply flip_Antisymmetric : typeclass_instances. +#[global] Hint Extern 3 (Transitive (flip _)) => class_apply flip_Transitive : typeclass_instances. +#[global] Hint Extern 3 (StrictOrder (flip _)) => class_apply flip_StrictOrder : typeclass_instances. +#[global] Hint Extern 3 (PreOrder (flip _)) => class_apply flip_PreOrder : typeclass_instances. +#[global] Hint Extern 4 (subrelation (flip _) _) => class_apply @subrelation_symmetric : typeclass_instances. +#[global] Hint Resolve irreflexivity : ord. Unset Implicit Arguments. @@ -231,6 +244,7 @@ Ltac solve_crelation := | [ H : ?R ?x ?y |- ?R ?y ?x ] => symmetry ; exact H end. +#[global] Hint Extern 4 => solve_crelation : crelations. (** We can already dualize all these properties. *) @@ -351,6 +365,7 @@ Section Binary. Qed. End Binary. +#[global] Hint Extern 3 (PartialOrder (flip _)) => class_apply PartialOrder_inverse : typeclass_instances. (** The partial order defined by subrelation and crelation equivalence. *) diff --git a/theories/Classes/Init.v b/theories/Classes/Init.v index 394f5dc4de..9ca465bbfd 100644 --- a/theories/Classes/Init.v +++ b/theories/Classes/Init.v @@ -36,4 +36,5 @@ Ltac unconvertible := | |- _ => exact tt end. +#[global] Hint Extern 0 (@Unconvertible _ _ _) => unconvertible : typeclass_instances. diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v index c70e3fe478..ffbea7dddf 100644 --- a/theories/Classes/Morphisms.v +++ b/theories/Classes/Morphisms.v @@ -81,9 +81,11 @@ End Proper. (** We favor the use of Leibniz equality or a declared reflexive relation when resolving [ProperProxy], otherwise, if the relation is given (not an evar), we fall back to [Proper]. *) +#[global] Hint Extern 1 (ProperProxy _ _) => class_apply @eq_proper_proxy || class_apply @reflexive_proper_proxy : typeclass_instances. +#[global] Hint Extern 2 (ProperProxy ?R _) => not_evar R; class_apply @proper_proper_proxy : typeclass_instances. @@ -213,8 +215,11 @@ Typeclasses Opaque respectful pointwise_relation forall_relation. Arguments forall_relation {A P}%type sig%signature _ _. Arguments pointwise_relation A%type {B}%type R%signature _ _. +#[global] Hint Unfold Reflexive : core. +#[global] Hint Unfold Symmetric : core. +#[global] Hint Unfold Transitive : core. (** Resolution with subrelation: favor decomposing products over applying reflexivity @@ -223,6 +228,7 @@ Ltac subrelation_tac T U := (is_ground T ; is_ground U ; class_apply @subrelation_refl) || class_apply @subrelation_respectful || class_apply @subrelation_refl. +#[global] Hint Extern 3 (@subrelation _ ?T ?U) => subrelation_tac T U : typeclass_instances. CoInductive apply_subrelation : Prop := do_subrelation. @@ -232,6 +238,7 @@ Ltac proper_subrelation := [ H : apply_subrelation |- _ ] => clear H ; class_apply @subrelation_proper end. +#[global] Hint Extern 5 (@Proper _ ?H _) => proper_subrelation : typeclass_instances. (** Essential subrelation instances for [iff], [impl] and [pointwise_relation]. *) @@ -244,6 +251,7 @@ Proof. firstorder. Qed. (** We use an extern hint to help unification. *) +#[global] Hint Extern 4 (subrelation (@forall_relation ?A ?B ?R) (@forall_relation _ _ ?S)) => apply (@forall_subrelation A B R S) ; intro : typeclass_instances. @@ -538,17 +546,24 @@ Ltac proper_reflexive := end. +#[global] Hint Extern 1 (subrelation (flip _) _) => class_apply @flip1 : typeclass_instances. +#[global] Hint Extern 1 (subrelation _ (flip _)) => class_apply @flip2 : typeclass_instances. +#[global] Hint Extern 1 (Proper _ (complement _)) => apply @complement_proper : typeclass_instances. +#[global] Hint Extern 1 (Proper _ (flip _)) => apply @flip_proper : typeclass_instances. +#[global] Hint Extern 2 (@Proper _ (flip _) _) => class_apply @proper_flip_proper : typeclass_instances. +#[global] Hint Extern 4 (@Proper _ _ _) => partial_application_tactic : typeclass_instances. +#[global] Hint Extern 7 (@Proper _ _ _) => proper_reflexive : typeclass_instances. @@ -603,7 +618,9 @@ Ltac proper_normalization := set(H:=did_normalization) ; class_apply @proper_normalizes_proper end. +#[global] Hint Extern 1 (Normalizes _ _ _) => normalizes : typeclass_instances. +#[global] Hint Extern 6 (@Proper _ _ _) => proper_normalization : typeclass_instances. @@ -693,6 +710,7 @@ split. + right. transitivity y; auto. Qed. +#[global] Hint Extern 4 (PreOrder (relation_disjunction _ _)) => class_apply StrictOrder_PreOrder : typeclass_instances. @@ -705,8 +723,10 @@ elim (StrictOrder_Irreflexive x). transitivity y; auto. Qed. +#[global] Hint Extern 4 (StrictOrder (relation_conjunction _ _)) => class_apply PartialOrder_StrictOrder : typeclass_instances. +#[global] Hint Extern 4 (PartialOrder _ (relation_disjunction _ _)) => class_apply StrictOrder_PartialOrder : typeclass_instances. diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v index 5381e91997..d8246c22e1 100644 --- a/theories/Classes/RelationClasses.v +++ b/theories/Classes/RelationClasses.v @@ -196,19 +196,31 @@ Defined. (** Hints to drive the typeclass resolution avoiding loops due to the use of full unification. *) +#[global] Hint Extern 1 (Reflexive (complement _)) => class_apply @irreflexivity : typeclass_instances. +#[global] Hint Extern 3 (Symmetric (complement _)) => class_apply complement_Symmetric : typeclass_instances. +#[global] Hint Extern 3 (Irreflexive (complement _)) => class_apply complement_Irreflexive : typeclass_instances. +#[global] Hint Extern 3 (Reflexive (flip _)) => apply flip_Reflexive : typeclass_instances. +#[global] Hint Extern 3 (Irreflexive (flip _)) => class_apply flip_Irreflexive : typeclass_instances. +#[global] Hint Extern 3 (Symmetric (flip _)) => class_apply flip_Symmetric : typeclass_instances. +#[global] Hint Extern 3 (Asymmetric (flip _)) => class_apply flip_Asymmetric : typeclass_instances. +#[global] Hint Extern 3 (Antisymmetric (flip _)) => class_apply flip_Antisymmetric : typeclass_instances. +#[global] Hint Extern 3 (Transitive (flip _)) => class_apply flip_Transitive : typeclass_instances. +#[global] Hint Extern 3 (StrictOrder (flip _)) => class_apply flip_StrictOrder : typeclass_instances. +#[global] Hint Extern 3 (PreOrder (flip _)) => class_apply flip_PreOrder : typeclass_instances. +#[global] Hint Extern 4 (subrelation (flip _) _) => class_apply @subrelation_symmetric : typeclass_instances. @@ -218,6 +230,7 @@ Arguments asymmetry {A} {R} {_} [x] [y] _ _. Arguments transitivity {A} {R} {_} [x] [y] [z] _ _. Arguments Antisymmetric A eqA {_} _. +#[global] Hint Resolve irreflexivity : ord. Unset Implicit Arguments. @@ -230,6 +243,7 @@ Ltac solve_relation := | [ H : ?R ?x ?y |- ?R ?y ?x ] => symmetry ; exact H end. +#[global] Hint Extern 4 => solve_relation : relations. (** We can already dualize all these properties. *) @@ -476,6 +490,7 @@ Section Binary. Proof. firstorder. Qed. End Binary. +#[global] Hint Extern 3 (PartialOrder (flip _)) => class_apply PartialOrder_inverse : typeclass_instances. (** The partial order defined by subrelation and relation equivalence. *) diff --git a/theories/Classes/RelationPairs.v b/theories/Classes/RelationPairs.v index b4034b9cf9..afe69cae7f 100644 --- a/theories/Classes/RelationPairs.v +++ b/theories/Classes/RelationPairs.v @@ -160,6 +160,8 @@ Section RelProd_Instances. Proof. unfold RelCompFun; firstorder. Qed. End RelProd_Instances. +#[global] Hint Unfold RelProd RelCompFun : core. +#[global] Hint Extern 2 (RelProd _ _ _ _) => split : core. diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v index ad0124db6d..bfa50d7fae 100644 --- a/theories/FSets/FMapAVL.v +++ b/theories/FSets/FMapAVL.v @@ -41,6 +41,7 @@ Local Open Scope Int_scope. Local Notation int := I.t. Definition key := X.t. +#[global] Hint Transparent key : core. (** * Trees *) @@ -495,7 +496,9 @@ Functional Scheme map2_opt_ind := Induction for map2_opt Sort Prop. (** * Automation and dedicated tactics. *) +#[global] Hint Constructors tree MapsTo In bst : core. +#[global] Hint Unfold lt_tree gt_tree : core. Tactic Notation "factornode" ident(l) ident(x) ident(d) ident(r) ident(h) @@ -576,6 +579,7 @@ Lemma MapsTo_In : forall k e m, MapsTo k e m -> In k m. Proof. induction 1; auto. Qed. +#[local] Hint Resolve MapsTo_In : core. Lemma In_MapsTo : forall k m, In k m -> exists e, MapsTo k e m. @@ -595,6 +599,7 @@ Lemma MapsTo_1 : Proof. induction m; simpl; intuition_in; eauto with ordered_type. Qed. +#[local] Hint Immediate MapsTo_1 : core. Lemma In_1 : @@ -634,6 +639,7 @@ Proof. unfold gt_tree in *; intuition_in; order. Qed. +#[local] Hint Resolve lt_leaf gt_leaf lt_tree_node gt_tree_node : core. Lemma lt_left : forall x y l r e h, @@ -660,6 +666,7 @@ Proof. intuition_in. Qed. +#[local] Hint Resolve lt_left lt_right gt_left gt_right : core. Lemma lt_tree_not_in : @@ -686,6 +693,7 @@ Proof. eauto with ordered_type. Qed. +#[local] Hint Resolve lt_tree_not_in lt_tree_trans gt_tree_not_in gt_tree_trans : core. (** * Empty map *) @@ -818,6 +826,7 @@ Lemma create_bst : Proof. unfold create; auto. Qed. +#[local] Hint Resolve create_bst : core. Lemma create_in : @@ -835,6 +844,7 @@ Proof. (apply lt_tree_node || apply gt_tree_node); auto with ordered_type; (eapply lt_tree_trans || eapply gt_tree_trans); eauto with ordered_type. Qed. +#[local] Hint Resolve bal_bst : core. Lemma bal_in : forall l x e r y, @@ -876,6 +886,7 @@ Proof. apply MX.eq_lt with x; auto. apply MX.lt_eq with x; auto with ordered_type. Qed. +#[local] Hint Resolve add_bst : core. Lemma add_1 : forall m x y e, X.eq x y -> MapsTo y e (add x e m). @@ -956,6 +967,7 @@ Proof. destruct 1. apply H2; intuition. Qed. +#[local] Hint Resolve remove_min_bst : core. Lemma remove_min_gt_tree : forall l x e r h, @@ -975,6 +987,7 @@ Proof. assert (X.lt m#1 x) by order. decompose [or] H; order. Qed. +#[local] Hint Resolve remove_min_gt_tree : core. Lemma remove_min_find : forall l x e r h y, @@ -1127,6 +1140,7 @@ Proof. intuition; [ apply MX.lt_eq with x | ]; eauto with ordered_type. intuition; [ apply MX.eq_lt with x | ]; eauto with ordered_type. Qed. +#[local] Hint Resolve join_bst : core. Lemma join_find : forall l x d r y, @@ -1263,6 +1277,7 @@ Proof. rewrite remove_min_in, e1; simpl; auto with ordered_type. change (gt_tree (m2',xd)#2#1 (m2',xd)#1). rewrite <-e1; eauto. Qed. +#[local] Hint Resolve concat_bst : core. Lemma concat_find : forall m1 m2 y, bst m1 -> bst m2 -> @@ -1351,6 +1366,7 @@ Proof. intros; unfold elements; apply elements_aux_sort; auto. intros; inversion H0. Qed. +#[local] Hint Resolve elements_sort : core. Lemma elements_nodup : forall s : t elt, bst s -> NoDupA eqk (elements s). @@ -1620,6 +1636,7 @@ destruct (map_option_2 H) as (d0 & ? & ?). destruct (map_option_2 H') as (d0' & ? & ?). eapply X.lt_trans with x; eauto using MapsTo_In. Qed. +#[local] Hint Resolve map_option_bst : core. Ltac nonify e := @@ -1719,6 +1736,7 @@ apply X.lt_trans with x1. destruct (map2_opt_2 H1 H6 Hy); intuition. destruct (map2_opt_2 H2 H7 Hy'); intuition. Qed. +#[local] Hint Resolve map2_opt_bst : core. Ltac map2_aux := @@ -2075,6 +2093,7 @@ Module IntMake_ord (I:Int)(X: OrderedType)(D : OrderedType) <: Proof. destruct c; simpl; intros; P.MX.elim_comp; auto with ordered_type. Qed. + #[global] Hint Resolve cons_Cmp : core. Lemma compare_end_Cmp : diff --git a/theories/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v index 2001201ec3..bb52166ca7 100644 --- a/theories/FSets/FMapFacts.v +++ b/theories/FSets/FMapFacts.v @@ -20,6 +20,7 @@ Require Export FMapInterface. Set Implicit Arguments. Unset Strict Implicit. +#[global] Hint Extern 1 (Equivalence _) => constructor; congruence : core. (** * Facts about weak maps *) @@ -371,6 +372,7 @@ Proof. intros. rewrite eq_option_alt. intro e'. rewrite <- 2 find_mapsto_iff. apply add_neq_mapsto_iff; auto. Qed. +#[local] Hint Resolve add_neq_o : map. Lemma add_o : forall m x y e, @@ -404,6 +406,7 @@ Proof. intros. rewrite eq_option_alt. intro e. rewrite <- find_mapsto_iff, remove_mapsto_iff; now intuition. Qed. +#[local] Hint Resolve remove_eq_o : map. Lemma remove_neq_o : forall m x y, @@ -412,6 +415,7 @@ Proof. intros. rewrite eq_option_alt. intro e. rewrite <- find_mapsto_iff, remove_neq_mapsto_iff; now intuition. Qed. +#[local] Hint Resolve remove_neq_o : map. Lemma remove_o : forall m x y, @@ -1100,6 +1104,7 @@ Module WProperties_fun (E:DecidableType)(M:WSfun E). contradict Hnotin; rewrite <- Hnotin; exists e0; auto. Qed. + #[local] Hint Resolve NoDupA_eqk_eqke NoDupA_rev elements_3w : map. Lemma fold_Equal : forall m1 m2 i, Equal m1 m2 -> @@ -1232,6 +1237,7 @@ Module WProperties_fun (E:DecidableType)(M:WSfun E). Proof. intros; rewrite cardinal_Empty; auto. Qed. + #[local] Hint Resolve cardinal_inv_1 : map. Lemma cardinal_inv_2 : @@ -1846,6 +1852,7 @@ Module OrdProperties (M:S). unfold leb; f_equal; apply gtb_compat; auto. Qed. + #[local] Hint Resolve gtb_compat leb_compat elements_3 : map. Lemma elements_split : forall p m, diff --git a/theories/FSets/FMapFullAVL.v b/theories/FSets/FMapFullAVL.v index 03e8d270e9..d26510ab9d 100644 --- a/theories/FSets/FMapFullAVL.v +++ b/theories/FSets/FMapFullAVL.v @@ -63,6 +63,7 @@ Inductive avl : t elt -> Prop := (** * Automation and dedicated tactics about [avl]. *) +#[local] Hint Constructors avl : core. Lemma height_non_negative : forall (s : t elt), avl s -> @@ -100,6 +101,7 @@ Lemma avl_node : forall x e l r, avl l -> avl r -> Proof. intros; auto. Qed. +#[local] Hint Resolve avl_node : core. (** Results about [height] *) @@ -193,6 +195,7 @@ Lemma add_avl : forall m x e, avl m -> avl (add x e m). Proof. intros; generalize (add_avl_1 x e H); intuition. Qed. +#[local] Hint Resolve add_avl : core. (** * Extraction of minimum binding *) @@ -274,6 +277,7 @@ Lemma remove_avl : forall m x, avl m -> avl (remove x m). Proof. intros; generalize (remove_avl_1 x H); intuition. Qed. +#[local] Hint Resolve remove_avl : core. @@ -331,6 +335,7 @@ Lemma join_avl : forall l x d r, avl l -> avl r -> avl (join l x d r). Proof. intros; destruct (join_avl_1 x d H H0); auto. Qed. +#[local] Hint Resolve join_avl : core. (** concat *) @@ -341,6 +346,7 @@ Proof. intros; apply join_avl; auto. generalize (remove_min_avl H0); rewrite e1; simpl; auto. Qed. +#[local] Hint Resolve concat_avl : core. (** split *) @@ -355,6 +361,7 @@ Proof. Qed. End Elt. +#[global] Hint Constructors avl : core. Section Map. @@ -714,6 +721,7 @@ Module IntMake_ord (I:Int)(X: OrderedType)(D : OrderedType) <: Proof. destruct c; simpl; intros; MX.elim_comp; auto with ordered_type. Qed. + #[global] Hint Resolve cons_Cmp : core. Lemma compare_aux_Cmp : forall e, diff --git a/theories/FSets/FMapInterface.v b/theories/FSets/FMapInterface.v index ab87ba9722..77ce76721e 100644 --- a/theories/FSets/FMapInterface.v +++ b/theories/FSets/FMapInterface.v @@ -58,6 +58,7 @@ Definition Cmp (elt:Type)(cmp:elt->elt->bool) e1 e2 := cmp e1 e2 = true. Module Type WSfun (E : DecidableType). Definition key := E.t. + #[global] Hint Transparent key : core. Parameter t : Type -> Type. @@ -243,9 +244,11 @@ Module Type WSfun (E : DecidableType). (x:key)(f:option elt->option elt'->option elt''), In x (map2 f m m') -> In x m \/ In x m'. + #[global] Hint Immediate MapsTo_1 mem_2 is_empty_2 map_2 mapi_2 add_3 remove_3 find_2 : map. + #[global] Hint Resolve mem_1 is_empty_1 is_empty_2 add_1 add_2 remove_1 remove_2 find_1 fold_1 map_1 mapi_1 mapi_2 : map. diff --git a/theories/FSets/FMapList.v b/theories/FSets/FMapList.v index a5c00189c4..204e8d0199 100644 --- a/theories/FSets/FMapList.v +++ b/theories/FSets/FMapList.v @@ -51,6 +51,7 @@ Proof. intro abs. inversion abs. Qed. +#[local] Hint Resolve empty_1 : core. Lemma empty_sorted : Sort empty. @@ -216,6 +217,7 @@ Proof. compute in H0,H1. simpl; case (X.compare x x''); intuition. Qed. +#[local] Hint Resolve add_Inf : core. Lemma add_sorted : forall m (Hm:Sort m) x e, Sort (add x e m). @@ -302,6 +304,7 @@ Proof. inversion_clear Hm. apply Inf_lt with (x'',e''); auto. Qed. +#[local] Hint Resolve remove_Inf : core. Lemma remove_sorted : forall m (Hm:Sort m) x, Sort (remove x m). @@ -586,6 +589,7 @@ Proof. inversion_clear H; auto. Qed. +#[local] Hint Resolve map_lelistA : core. Lemma map_sorted : forall (m: t elt)(Hm : sort (@ltk elt) m)(f:elt -> elt'), @@ -655,6 +659,7 @@ Proof. inversion_clear H; auto. Qed. +#[local] Hint Resolve mapi_lelistA : core. Lemma mapi_sorted : forall m (Hm : sort (@ltk elt) m)(f: key ->elt -> elt'), @@ -782,6 +787,7 @@ Proof. inversion_clear H; auto. inversion_clear H0; auto. Qed. +#[local] Hint Resolve combine_lelistA : core. Lemma combine_sorted : diff --git a/theories/FSets/FMapWeakList.v b/theories/FSets/FMapWeakList.v index c4bb67a52c..78e7ab69d8 100644 --- a/theories/FSets/FMapWeakList.v +++ b/theories/FSets/FMapWeakList.v @@ -49,6 +49,7 @@ Proof. inversion abs. Qed. +#[local] Hint Resolve empty_1 : core. Lemma empty_NoDup : NoDupA empty. @@ -621,6 +622,7 @@ Proof. inversion_clear 1. intros; apply add_NoDup; auto. Qed. +#[local] Hint Resolve fold_right_pair_NoDup : core. Lemma combine_NoDup : diff --git a/theories/FSets/FSetBridge.v b/theories/FSets/FSetBridge.v index 73021a84a3..4917fcb5fd 100644 --- a/theories/FSets/FSetBridge.v +++ b/theories/FSets/FSetBridge.v @@ -137,6 +137,7 @@ Module DepOfNodep (Import M: S) <: Sdep with Module E := M.E. generalize (E.eq_sym H0); case (Pdec x); case (Pdec y); firstorder. Qed. + #[global] Hint Resolve compat_P_aux : core. Definition filter : @@ -467,6 +468,7 @@ Module NodepOfDep (M: Sdep) <: S with Module E := M.E. Proof. intros; unfold elements; case (M.elements s); firstorder. Qed. + #[global] Hint Resolve elements_3 : core. Lemma elements_3w : forall s : t, NoDupA E.eq (elements s). @@ -666,6 +668,7 @@ Module NodepOfDep (M: Sdep) <: S with Module E := M.E. rewrite <- H1; firstorder. Qed. + #[global] Hint Resolve compat_P_aux : core. Definition filter (f : elt -> bool) (s : t) : t := diff --git a/theories/FSets/FSetDecide.v b/theories/FSets/FSetDecide.v index 8a217a752a..d597c0404a 100644 --- a/theories/FSets/FSetDecide.v +++ b/theories/FSets/FSetDecide.v @@ -466,6 +466,7 @@ the above form: (** Here is the tactic that will throw away hypotheses that are not useful (for the intended scope of the [fsetdec] tactic). *) + #[global] Hint Constructors FSet_elt_Prop FSet_Prop : FSet_Prop. Ltac discard_nonFSet := repeat ( @@ -518,6 +519,7 @@ the above form: (** The hint database [FSet_decidability] will be given to the [push_neg] tactic from the module [Negation]. *) + #[global] Hint Resolve dec_In dec_eq : FSet_decidability. (** ** Normalizing Propositions About Equality diff --git a/theories/FSets/FSetEqProperties.v b/theories/FSets/FSetEqProperties.v index ac08351ad9..7618880bd2 100644 --- a/theories/FSets/FSetEqProperties.v +++ b/theories/FSets/FSetEqProperties.v @@ -460,9 +460,11 @@ Qed. End BasicProperties. +#[global] Hint Immediate empty_mem is_empty_equal_empty add_mem_1 remove_mem_1 singleton_equal_add union_mem inter_mem diff_mem equal_sym add_remove remove_add : set. +#[global] Hint Resolve equal_mem_1 subset_mem_1 choose_mem_1 choose_mem_2 add_mem_2 remove_mem_2 equal_refl equal_equal subset_refl subset_equal subset_antisym diff --git a/theories/FSets/FSetInterface.v b/theories/FSets/FSetInterface.v index dfe22b7831..848c27cba1 100644 --- a/theories/FSets/FSetInterface.v +++ b/theories/FSets/FSetInterface.v @@ -253,13 +253,16 @@ Module Type WSfun (E : DecidableType). End Spec. + #[global] Hint Transparent elt : core. + #[global] Hint Resolve mem_1 equal_1 subset_1 empty_1 is_empty_1 choose_1 choose_2 add_1 add_2 remove_1 remove_2 singleton_2 union_1 union_2 union_3 inter_3 diff_3 fold_1 filter_3 for_all_1 exists_1 partition_1 partition_2 elements_1 elements_3w : set. + #[global] Hint Immediate In_1 mem_2 equal_2 subset_2 is_empty_2 add_3 remove_3 singleton_1 inter_1 inter_2 diff_1 diff_2 filter_1 filter_2 for_all_2 exists_2 elements_2 @@ -336,7 +339,9 @@ Module Type Sfun (E : OrderedType). End Spec. + #[global] Hint Resolve elements_3 : set. + #[global] Hint Immediate min_elt_1 min_elt_2 min_elt_3 max_elt_1 max_elt_2 max_elt_3 : set. diff --git a/theories/FSets/FSetProperties.v b/theories/FSets/FSetProperties.v index 98b445580b..af034bbdd5 100644 --- a/theories/FSets/FSetProperties.v +++ b/theories/FSets/FSetProperties.v @@ -21,7 +21,9 @@ Require Import DecidableTypeEx FSetFacts FSetDecide. Set Implicit Arguments. Unset Strict Implicit. +#[global] Hint Unfold transpose compat_op Proper respectful : fset. +#[global] Hint Extern 1 (Equivalence _) => constructor; congruence : fset. (** First, a functor for Weak Sets in functorial version. *) @@ -269,7 +271,9 @@ Module WProperties_fun (Import E : DecidableType)(M : WSfun E). End BasicProperties. + #[global] Hint Immediate equal_sym add_remove remove_add union_sym inter_sym: set. + #[global] Hint Resolve equal_refl equal_trans subset_refl subset_equal subset_antisym subset_trans subset_empty subset_remove_3 subset_diff subset_add_3 subset_add_2 in_subset empty_is_empty_1 empty_is_empty_2 add_equal @@ -732,6 +736,7 @@ Module WProperties_fun (Import E : DecidableType)(M : WSfun E). Proof. intros; rewrite cardinal_Empty; auto. Qed. + #[global] Hint Resolve cardinal_inv_1 : fset. Lemma cardinal_inv_2 : @@ -769,6 +774,7 @@ Module WProperties_fun (Import E : DecidableType)(M : WSfun E). exact Equal_cardinal. Qed. + #[global] Hint Resolve Add_add Add_remove Equal_remove cardinal_inv_1 Equal_cardinal : fset. (** ** Cardinal and set operators *) @@ -778,6 +784,7 @@ Module WProperties_fun (Import E : DecidableType)(M : WSfun E). rewrite cardinal_fold; apply fold_1; auto with set fset. Qed. + #[global] Hint Immediate empty_cardinal cardinal_1 : set. Lemma singleton_cardinal : forall x, cardinal (singleton x) = 1. @@ -788,6 +795,7 @@ Module WProperties_fun (Import E : DecidableType)(M : WSfun E). apply cardinal_2 with x; auto with set. Qed. + #[global] Hint Resolve singleton_cardinal: set. Lemma diff_inter_cardinal : @@ -887,6 +895,7 @@ Module WProperties_fun (Import E : DecidableType)(M : WSfun E). auto with set fset. Qed. + #[global] Hint Resolve subset_cardinal union_cardinal add_cardinal_1 add_cardinal_2 : fset. End WProperties_fun. @@ -952,6 +961,7 @@ Module OrdProperties (M:S). red; intros x a b H; unfold leb. f_equal; apply gtb_compat; auto. Qed. + #[global] Hint Resolve gtb_compat leb_compat : fset. Lemma elements_split : forall x s, diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v index 9984bff0c2..f013c857ea 100644 --- a/theories/Init/Datatypes.v +++ b/theories/Init/Datatypes.v @@ -83,6 +83,7 @@ Lemma andb_prop (a b:bool) : andb a b = true -> a = true /\ b = true. Proof. destruct a, b; repeat split; assumption. Qed. +#[global] Hint Resolve andb_prop: bool. Register andb_prop as core.bool.andb_prop. @@ -92,6 +93,7 @@ Lemma andb_true_intro (b1 b2:bool) : Proof. destruct b1; destruct b2; simpl; intros [? ?]; assumption. Qed. +#[global] Hint Resolve andb_true_intro: bool. Register andb_true_intro as core.bool.andb_true_intro. @@ -100,6 +102,7 @@ Register andb_true_intro as core.bool.andb_true_intro. Inductive eq_true : bool -> Prop := is_eq_true : eq_true true. +#[global] Hint Constructors eq_true : eq_true. Register eq_true as core.eq_true.type. @@ -142,6 +145,7 @@ Defined. Inductive BoolSpec (P Q : Prop) : bool -> Prop := | BoolSpecT : P -> BoolSpec P Q true | BoolSpecF : Q -> BoolSpec P Q false. +#[global] Hint Constructors BoolSpec : core. Register BoolSpec as core.BoolSpec.type. @@ -243,6 +247,7 @@ Section projections. End projections. +#[global] Hint Resolve pair inl inr: core. Lemma surjective_pairing (A B:Type) (p:A * B) : p = (fst p, snd p). @@ -380,6 +385,7 @@ Inductive CompareSpec (Peq Plt Pgt : Prop) : comparison -> Prop := | CompEq : Peq -> CompareSpec Peq Plt Pgt Eq | CompLt : Plt -> CompareSpec Peq Plt Pgt Lt | CompGt : Pgt -> CompareSpec Peq Plt Pgt Gt. +#[global] Hint Constructors CompareSpec : core. Register CompareSpec as core.CompareSpec.type. @@ -395,6 +401,7 @@ Inductive CompareSpecT (Peq Plt Pgt : Prop) : comparison -> Type := | CompEqT : Peq -> CompareSpecT Peq Plt Pgt Eq | CompLtT : Plt -> CompareSpecT Peq Plt Pgt Lt | CompGtT : Pgt -> CompareSpecT Peq Plt Pgt Gt. +#[global] Hint Constructors CompareSpecT : core. Register CompareSpecT as core.CompareSpecT.type. @@ -417,6 +424,7 @@ Definition CompSpec {A} (eq lt : A->A->Prop)(x y:A) : comparison -> Prop := Definition CompSpecT {A} (eq lt : A->A->Prop)(x y:A) : comparison -> Type := CompareSpecT (eq x y) (lt x y) (lt y x). +#[global] Hint Unfold CompSpec CompSpecT : core. Lemma CompSpec2Type : forall A (eq lt:A->A->Prop) x y c, @@ -435,6 +443,7 @@ Proof. intros. apply CompareSpec2Type; assumption. Defined. Inductive identity (A:Type) (a:A) : A -> Type := identity_refl : identity a a. +#[global] Hint Resolve identity_refl: core. Arguments identity_ind [A] a P f y i. diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v index 8012235143..023705e169 100644 --- a/theories/Init/Logic.v +++ b/theories/Init/Logic.v @@ -41,9 +41,12 @@ Register not as core.not.type. variables and constants explicitly. *) Create HintDb core. +#[global] Hint Variables Opaque : core. +#[global] Hint Constants Opaque : core. +#[global] Hint Unfold not: core. (** [and A B], written [A /\ B], is the conjunction of [A] and [B] @@ -119,6 +122,7 @@ Theorem iff_sym : forall A B:Prop, (A <-> B) -> (B <-> A). End Equivalence. +#[global] Hint Unfold iff: extcore. (** Backward direction of the equivalences above does not need assumptions *) @@ -364,8 +368,11 @@ Notation "x = y" := (eq x y) : type_scope. Notation "x <> y :> T" := (~ x = y :>T) : type_scope. Notation "x <> y" := (~ (x = y)) : type_scope. +#[global] Hint Resolve I conj or_introl or_intror : core. +#[global] Hint Resolve eq_refl: core. +#[global] Hint Resolve ex_intro ex_intro2: core. Register eq as core.eq.type. @@ -733,6 +740,7 @@ Notation sym_equal := eq_sym (only parsing). Notation trans_equal := eq_trans (only parsing). Notation sym_not_equal := not_eq_sym (only parsing). +#[global] Hint Immediate eq_sym not_eq_sym: core. (** Basic definitions about relations and properties *) @@ -801,6 +809,7 @@ Qed. Inductive inhabited (A:Type) : Prop := inhabits : A -> inhabited A. +#[global] Hint Resolve inhabits: core. Lemma exists_inhabited : forall (A:Type) (P:A->Prop), diff --git a/theories/Init/Logic_Type.v b/theories/Init/Logic_Type.v index 3d9937ae89..f8869615cd 100644 --- a/theories/Init/Logic_Type.v +++ b/theories/Init/Logic_Type.v @@ -72,6 +72,7 @@ Definition identity_rect_r : intros A x P H y H0; case identity_sym with (1 := H0); trivial. Defined. +#[global] Hint Immediate identity_sym not_identity_sym: core. Notation refl_id := identity_refl (only parsing). diff --git a/theories/Init/Peano.v b/theories/Init/Peano.v index 98fd52f351..fb2a7a57fe 100644 --- a/theories/Init/Peano.v +++ b/theories/Init/Peano.v @@ -37,6 +37,7 @@ Local Notation "0" := O. Definition eq_S := f_equal S. Definition f_equal_nat := f_equal (A:=nat). +#[global] Hint Resolve f_equal_nat: core. (** The predecessor function *) @@ -53,12 +54,14 @@ Qed. (** Injectivity of successor *) Definition eq_add_S n m (H: S n = S m): n = m := f_equal pred H. +#[global] Hint Immediate eq_add_S: core. Theorem not_eq_S : forall n m:nat, n <> m -> S n <> S m. Proof. red; auto. Qed. +#[global] Hint Resolve not_eq_S: core. Definition IsSucc (n:nat) : Prop := @@ -73,12 +76,14 @@ Theorem O_S : forall n:nat, 0 <> S n. Proof. discriminate. Qed. +#[global] Hint Resolve O_S: core. Theorem n_Sn : forall n:nat, n <> S n. Proof. intro n; induction n; auto. Qed. +#[global] Hint Resolve n_Sn: core. (** Addition *) @@ -88,6 +93,7 @@ Infix "+" := Nat.add : nat_scope. Definition f_equal2_plus := f_equal2 plus. Definition f_equal2_nat := f_equal2 (A1:=nat) (A2:=nat). +#[global] Hint Resolve f_equal2_nat: core. Lemma plus_n_O : forall n:nat, n = n + 0. @@ -95,7 +101,9 @@ Proof. intro n; induction n; simpl; auto. Qed. +#[global] Remove Hints eq_refl : core. +#[global] Hint Resolve plus_n_O eq_refl: core. (* We want eq_refl to have higher priority than plus_n_O *) Lemma plus_O_n : forall n:nat, 0 + n = n. @@ -107,6 +115,7 @@ Lemma plus_n_Sm : forall n m:nat, S (n + m) = n + S m. Proof. intros n m; induction n; simpl; auto. Qed. +#[global] Hint Resolve plus_n_Sm: core. Lemma plus_Sn_m : forall n m:nat, S n + m = S (n + m). @@ -125,12 +134,14 @@ Notation mult := Nat.mul (only parsing). Infix "*" := Nat.mul : nat_scope. Definition f_equal2_mult := f_equal2 mult. +#[global] Hint Resolve f_equal2_mult: core. Lemma mult_n_O : forall n:nat, 0 = n * 0. Proof. intro n; induction n; simpl; auto. Qed. +#[global] Hint Resolve mult_n_O: core. Lemma mult_n_Sm : forall n m:nat, n * m + n = n * S m. @@ -139,6 +150,7 @@ Proof. destruct H; rewrite <- plus_n_Sm; apply eq_S. pattern m at 1 3; elim m; simpl; auto. Qed. +#[global] Hint Resolve mult_n_Sm: core. (** Standard associated names *) @@ -162,20 +174,24 @@ where "n <= m" := (le n m) : nat_scope. Register le_n as num.nat.le_n. +#[global] Hint Constructors le: core. (*i equivalent to : "Hints Resolve le_n le_S : core." i*) Definition lt (n m:nat) := S n <= m. +#[global] Hint Unfold lt: core. Infix "<" := lt : nat_scope. Definition ge (n m:nat) := m <= n. +#[global] Hint Unfold ge: core. Infix ">=" := ge : nat_scope. Definition gt (n m:nat) := m < n. +#[global] Hint Unfold gt: core. Infix ">" := gt : nat_scope. diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v index 1fb6dabe6f..5d759f3234 100644 --- a/theories/Init/Specif.v +++ b/theories/Init/Specif.v @@ -797,5 +797,7 @@ Proof. apply (h2 h1). Defined. +#[global] Hint Resolve left right inleft inright: core. +#[global] Hint Resolve exist exist2 existT existT2: core. diff --git a/theories/Init/Tactics.v b/theories/Init/Tactics.v index 35bab1021e..8721b7c797 100644 --- a/theories/Init/Tactics.v +++ b/theories/Init/Tactics.v @@ -339,5 +339,6 @@ Tactic Notation "assert_fails" tactic3(tac) := assert_fails tac. Create HintDb rewrite discriminated. +#[global] Hint Variables Opaque : rewrite. Create HintDb typeclass_instances discriminated. diff --git a/theories/Lists/List.v b/theories/Lists/List.v index 4cc3597029..115c7cb365 100644 --- a/theories/Lists/List.v +++ b/theories/Lists/List.v @@ -163,6 +163,7 @@ Section Facts. Proof. auto using app_assoc. Qed. + #[local] Hint Resolve app_assoc_reverse : core. (* end hide *) @@ -385,10 +386,15 @@ Section Facts. End Facts. +#[global] Hint Resolve app_assoc app_assoc_reverse: datatypes. +#[global] Hint Resolve app_comm_cons app_cons_not_nil: datatypes. +#[global] Hint Immediate app_eq_nil: datatypes. +#[global] Hint Resolve app_eq_unit app_inj_tail: datatypes. +#[global] Hint Resolve in_eq in_cons in_inv in_nil in_app_or in_or_app: datatypes. @@ -1928,6 +1934,7 @@ Section length_order. Qed. End length_order. +#[global] Hint Resolve lel_refl lel_cons_cons lel_cons lel_nil lel_nil nil_cons: datatypes. @@ -1941,6 +1948,7 @@ Section SetIncl. Variable A : Type. Definition incl (l m:list A) := forall a:A, In a l -> In a m. + #[local] Hint Unfold incl : core. Lemma incl_nil_l : forall l, incl nil l. @@ -1959,12 +1967,14 @@ Section SetIncl. Proof. auto. Qed. + #[local] Hint Resolve incl_refl : core. Lemma incl_tl : forall (a:A) (l m:list A), incl l m -> incl l (a :: m). Proof. auto with datatypes. Qed. + #[local] Hint Immediate incl_tl : core. Lemma incl_tran : forall l m n:list A, incl l m -> incl m n -> incl l n. @@ -1976,12 +1986,14 @@ Section SetIncl. Proof. auto with datatypes. Qed. + #[local] Hint Immediate incl_appl : core. Lemma incl_appr : forall l m n:list A, incl l n -> incl l (m ++ n). Proof. auto with datatypes. Qed. + #[local] Hint Immediate incl_appr : core. Lemma incl_cons : @@ -1997,6 +2009,7 @@ Section SetIncl. now_show (In a0 l -> In a0 m). auto. Qed. + #[local] Hint Resolve incl_cons : core. Lemma incl_cons_inv : forall (a:A) (l m:list A), @@ -2012,6 +2025,7 @@ Section SetIncl. now_show (In a n). elim (in_app_or _ _ _ H1); auto. Qed. + #[local] Hint Resolve incl_app : core. Lemma incl_app_app : forall l1 l2 m1 m2:list A, @@ -2054,6 +2068,7 @@ Proof. apply in_map; intuition. Qed. +#[global] Hint Resolve incl_refl incl_tl incl_tran incl_appl incl_appr incl_cons incl_app incl_map: datatypes. @@ -2738,6 +2753,7 @@ Section Exists_Forall. | Exists_cons_hd : forall x l, P x -> Exists (x::l) | Exists_cons_tl : forall x l, Exists l -> Exists (x::l). + #[local] Hint Constructors Exists : core. Lemma Exists_exists (l:list A) : @@ -2815,6 +2831,7 @@ Section Exists_Forall. | Forall_nil : Forall nil | Forall_cons : forall x l, P x -> Forall l -> Forall (x::l). + #[local] Hint Constructors Forall : core. Lemma Forall_forall (l:list A): @@ -2999,7 +3016,9 @@ Section Exists_Forall. End Exists_Forall. +#[global] Hint Constructors Exists : core. +#[global] Hint Constructors Forall : core. Lemma exists_Forall A B : forall (P : A -> B -> Prop) l, @@ -3064,6 +3083,7 @@ Section Forall2. | Forall2_cons : forall x y l l', R x y -> Forall2 l l' -> Forall2 (x::l) (y::l'). + #[local] Hint Constructors Forall2 : core. Theorem Forall2_refl : Forall2 [] []. @@ -3098,6 +3118,7 @@ Section Forall2. Qed. End Forall2. +#[global] Hint Constructors Forall2 : core. Section ForallPairs. @@ -3119,6 +3140,7 @@ Section ForallPairs. | FOP_cons : forall a l, Forall (R a) l -> ForallOrdPairs l -> ForallOrdPairs (a::l). + #[local] Hint Constructors ForallOrdPairs : core. Lemma ForallOrdPairs_In : forall l, @@ -3344,6 +3366,7 @@ Notation rev_acc := rev_append (only parsing). Notation rev_acc_rev := rev_append_rev (only parsing). Notation AllS := Forall (only parsing). (* was formerly in TheoryList *) +#[global] Hint Resolve app_nil_end : datatypes. (* end hide *) diff --git a/theories/Lists/ListSet.v b/theories/Lists/ListSet.v index 7f5148d0dd..458d08ccb9 100644 --- a/theories/Lists/ListSet.v +++ b/theories/Lists/ListSet.v @@ -193,6 +193,7 @@ Section first_definitions. | auto with datatypes ]. Qed. + #[local] Hint Resolve set_add_intro1 set_add_intro2 : core. Lemma set_add_intro : @@ -224,6 +225,7 @@ Section first_definitions. case H1; trivial. Qed. + #[local] Hint Resolve set_add_intro set_add_elim set_add_elim2 : core. Lemma set_add_not_empty : forall (a:A) (x:set), set_add a x <> empty_set. @@ -310,6 +312,7 @@ Section first_definitions. intros; elim H0; auto with datatypes. Qed. + #[local] Hint Resolve set_union_intro2 set_union_intro1 : core. Lemma set_union_intro : @@ -393,6 +396,7 @@ Section first_definitions. eauto with datatypes. Qed. + #[local] Hint Resolve set_inter_elim1 set_inter_elim2 : core. Lemma set_inter_elim : @@ -471,6 +475,7 @@ Section first_definitions. apply (set_diff_elim1 _ _ _ H). Qed. +#[local] Hint Resolve set_diff_intro set_diff_trivial : core. diff --git a/theories/Lists/SetoidList.v b/theories/Lists/SetoidList.v index 48e9f992fd..826815410a 100644 --- a/theories/Lists/SetoidList.v +++ b/theories/Lists/SetoidList.v @@ -30,6 +30,7 @@ Inductive InA (x : A) : list A -> Prop := | InA_cons_hd : forall y l, eqA x y -> InA x (y :: l) | InA_cons_tl : forall y l, InA x l -> InA x (y :: l). +#[local] Hint Constructors InA : core. (** TODO: it would be nice to have a generic definition instead @@ -62,6 +63,7 @@ Inductive NoDupA : list A -> Prop := | NoDupA_nil : NoDupA nil | NoDupA_cons : forall x l, ~ InA x l -> NoDupA l -> NoDupA (x::l). +#[local] Hint Constructors NoDupA : core. (** An alternative definition of [NoDupA] based on [ForallOrdPairs] *) @@ -84,6 +86,7 @@ Definition equivlistA l l' := forall x, InA x l <-> InA x l'. Lemma incl_nil l : inclA nil l. Proof. intro. intros. inversion H. Qed. +#[local] Hint Resolve incl_nil : list. (** lists with same elements modulo [eqA] at the same place *) @@ -93,6 +96,7 @@ Inductive eqlistA : list A -> list A -> Prop := | eqlistA_cons : forall x x' l l', eqA x x' -> eqlistA l l' -> eqlistA (x::l) (x'::l'). +#[local] Hint Constructors eqlistA : core. (** We could also have written [eqlistA = Forall2 eqA]. *) @@ -107,7 +111,9 @@ Definition eqarefl := (@Equivalence_Reflexive _ _ eqA_equiv). Definition eqatrans := (@Equivalence_Transitive _ _ eqA_equiv). Definition eqasym := (@Equivalence_Symmetric _ _ eqA_equiv). +#[local] Hint Resolve eqarefl eqatrans : core. +#[local] Hint Immediate eqasym : core. Ltac inv := invlist InA; invlist sort; invlist lelistA; invlist NoDupA. @@ -154,6 +160,7 @@ Lemma InA_eqA : forall l x y, eqA x y -> InA x l -> InA y l. Proof. intros l x y H H'. rewrite <- H. auto. Qed. +#[local] Hint Immediate InA_eqA : core. Lemma In_InA : forall l x, In x l -> InA x l. @@ -161,6 +168,7 @@ Proof. simple induction l; simpl; intuition. subst; auto. Qed. +#[local] Hint Resolve In_InA : core. Lemma InA_split : forall l x, InA x l -> @@ -786,11 +794,13 @@ Hypothesis ltA_compat : Proper (eqA==>eqA==>iff) ltA. Let sotrans := (@StrictOrder_Transitive _ _ ltA_strorder). +#[local] Hint Resolve sotrans : core. Notation InfA:=(lelistA ltA). Notation SortA:=(sort ltA). +#[local] Hint Constructors lelistA sort : core. Lemma InfA_ltA : @@ -814,6 +824,7 @@ Lemma InfA_eqA l x y : eqA x y -> InfA y l -> InfA x l. Proof using eqA_equiv ltA_compat. intros H; now rewrite H. Qed. +#[local] Hint Immediate InfA_ltA InfA_eqA : core. Lemma SortA_InfA_InA : @@ -1005,6 +1016,7 @@ Qed. End Filter. End Type_with_equality. +#[global] Hint Constructors InA eqlistA NoDupA sort lelistA : core. Arguments equivlistA_cons_nil {A} eqA {eqA_equiv} x l _. diff --git a/theories/Lists/Streams.v b/theories/Lists/Streams.v index 7a275a8231..f16d70a4c2 100644 --- a/theories/Lists/Streams.v +++ b/theories/Lists/Streams.v @@ -54,6 +54,7 @@ Lemma tl_nth_tl : Proof. simple induction n; simpl; auto. Qed. +#[local] Hint Resolve tl_nth_tl: datatypes. Lemma Str_nth_tl_plus : diff --git a/theories/Logic/Classical_Prop.v b/theories/Logic/Classical_Prop.v index e5d364297d..b2b5985ff1 100644 --- a/theories/Logic/Classical_Prop.v +++ b/theories/Logic/Classical_Prop.v @@ -16,6 +16,7 @@ Require Import ClassicalFacts. +#[global] Hint Unfold not: core. Axiom classic : forall P:Prop, P \/ ~ P. diff --git a/theories/Logic/Decidable.v b/theories/Logic/Decidable.v index 998497f13e..5fb6bb3907 100644 --- a/theories/Logic/Decidable.v +++ b/theories/Logic/Decidable.v @@ -206,6 +206,7 @@ Qed. (** With the following hint database, we can leverage [auto] to check decidability of propositions. *) +#[global] Hint Resolve dec_True dec_False dec_or dec_and dec_imp dec_not dec_iff : decidable_prop. diff --git a/theories/Logic/Eqdep.v b/theories/Logic/Eqdep.v index f2e15c9abb..934806de93 100644 --- a/theories/Logic/Eqdep.v +++ b/theories/Logic/Eqdep.v @@ -35,5 +35,7 @@ Export EqdepTheory. (** Exported hints *) +#[global] Hint Resolve eq_dep_eq: eqdep. +#[global] Hint Resolve inj_pair2 inj_pairT2: eqdep. diff --git a/theories/Logic/EqdepFacts.v b/theories/Logic/EqdepFacts.v index a918d1ecd7..6589e75289 100644 --- a/theories/Logic/EqdepFacts.v +++ b/theories/Logic/EqdepFacts.v @@ -65,6 +65,7 @@ Section Dependent_Equality. Inductive eq_dep (p:U) (x:P p) : forall q:U, P q -> Prop := eq_dep_intro : eq_dep p x p x. + #[local] Hint Constructors eq_dep: core. Lemma eq_dep_refl : forall (p:U) (x:P p), eq_dep p x p x. @@ -75,6 +76,7 @@ Section Dependent_Equality. Proof. destruct 1; auto. Qed. + #[local] Hint Immediate eq_dep_sym: core. Lemma eq_dep_trans : @@ -221,7 +223,9 @@ Unset Implicit Arguments. (** Exported hints *) +#[global] Hint Resolve eq_dep_intro: core. +#[global] Hint Immediate eq_dep_sym: core. (************************************************************************) diff --git a/theories/Logic/JMeq.v b/theories/Logic/JMeq.v index ccd7db177c..7ee3a99d60 100644 --- a/theories/Logic/JMeq.v +++ b/theories/Logic/JMeq.v @@ -31,6 +31,7 @@ Arguments JMeq_refl {A x} , [A] x. Register JMeq as core.JMeq.type. Register JMeq_refl as core.JMeq.refl. +#[global] Hint Resolve JMeq_refl : core. Definition JMeq_hom {A : Type} (x y : A) := JMeq x y. @@ -42,6 +43,7 @@ Proof. intros; destruct H; trivial. Qed. +#[global] Hint Immediate JMeq_sym : core. Register JMeq_sym as core.JMeq.sym. diff --git a/theories/MSets/MSetDecide.v b/theories/MSets/MSetDecide.v index 0f62a9419b..aa0c419f0e 100644 --- a/theories/MSets/MSetDecide.v +++ b/theories/MSets/MSetDecide.v @@ -466,6 +466,7 @@ the above form: (** Here is the tactic that will throw away hypotheses that are not useful (for the intended scope of the [fsetdec] tactic). *) + #[global] Hint Constructors MSet_elt_Prop MSet_Prop : MSet_Prop. Ltac discard_nonMSet := repeat ( @@ -518,6 +519,7 @@ the above form: (** The hint database [MSet_decidability] will be given to the [push_neg] tactic from the module [Negation]. *) + #[global] Hint Resolve dec_In dec_eq : MSet_decidability. (** ** Normalizing Propositions About Equality diff --git a/theories/MSets/MSetEqProperties.v b/theories/MSets/MSetEqProperties.v index dc22af4948..b439be9b3f 100644 --- a/theories/MSets/MSetEqProperties.v +++ b/theories/MSets/MSetEqProperties.v @@ -462,9 +462,11 @@ Qed. End BasicProperties. +#[global] Hint Immediate empty_mem is_empty_equal_empty add_mem_1 remove_mem_1 singleton_equal_add union_mem inter_mem diff_mem equal_sym add_remove remove_add : set. +#[global] Hint Resolve equal_mem_1 subset_mem_1 choose_mem_1 choose_mem_2 add_mem_2 remove_mem_2 equal_refl equal_equal subset_refl subset_equal subset_antisym diff --git a/theories/MSets/MSetFacts.v b/theories/MSets/MSetFacts.v index 7dbb658e46..ea86c7a4d7 100644 --- a/theories/MSets/MSetFacts.v +++ b/theories/MSets/MSetFacts.v @@ -139,12 +139,14 @@ Notation choose_1 := choose_spec1 (only parsing). Notation choose_2 := choose_spec2 (only parsing). Notation elements_3w := elements_spec2w (only parsing). +#[global] Hint Resolve mem_1 equal_1 subset_1 empty_1 is_empty_1 choose_1 choose_2 add_1 add_2 remove_1 remove_2 singleton_2 union_1 union_2 union_3 inter_3 diff_3 fold_1 filter_3 for_all_1 exists_1 partition_1 partition_2 elements_1 elements_3w : set. +#[global] Hint Immediate In_1 mem_2 equal_2 subset_2 is_empty_2 add_3 remove_3 singleton_1 inter_1 inter_2 diff_1 diff_2 filter_1 filter_2 for_all_2 exists_2 elements_2 diff --git a/theories/MSets/MSetGenTree.v b/theories/MSets/MSetGenTree.v index 58656b666e..37d20bffad 100644 --- a/theories/MSets/MSetGenTree.v +++ b/theories/MSets/MSetGenTree.v @@ -46,6 +46,7 @@ End InfoTyp. Module Type Ops (X:OrderedType)(Info:InfoTyp). Definition elt := X.t. +#[global] Hint Transparent elt : core. Inductive tree : Type := diff --git a/theories/MSets/MSetInterface.v b/theories/MSets/MSetInterface.v index fe5d721ffa..c0567f9ef1 100644 --- a/theories/MSets/MSetInterface.v +++ b/theories/MSets/MSetInterface.v @@ -442,6 +442,7 @@ Module WRaw2SetsOn (E:DecidableType)(M:WRawSets E) <: WSetsOn E. Record t_ := Mkt {this :> M.t; is_ok : M.Ok this}. Definition t := t_. Arguments Mkt this {is_ok}. + #[global] Hint Resolve is_ok : typeclass_instances. Definition In (x : elt)(s : t) := M.In x (this s). @@ -884,9 +885,11 @@ Module MakeListOrdering (O:OrderedType). O.lt x y -> lt_list (x :: s) (y :: s') | lt_cons_eq : forall x y s s', O.eq x y -> lt_list s s' -> lt_list (x :: s) (y :: s'). + #[global] Hint Constructors lt_list : core. Definition lt := lt_list. + #[global] Hint Unfold lt : core. Instance lt_strorder : StrictOrder lt. @@ -933,6 +936,7 @@ Module MakeListOrdering (O:OrderedType). left; MO.order. right; rewrite <- E12; auto. left; MO.order. right; rewrite E12; auto. Qed. + #[global] Hint Resolve eq_cons : core. Lemma cons_CompSpec : forall c x1 x2 l1 l2, O.eq x1 x2 -> @@ -940,6 +944,7 @@ Module MakeListOrdering (O:OrderedType). Proof. destruct c; simpl; inversion_clear 2; auto with relations. Qed. + #[global] Hint Resolve cons_CompSpec : core. End MakeListOrdering. diff --git a/theories/MSets/MSetList.v b/theories/MSets/MSetList.v index d2878b4710..84cf620474 100644 --- a/theories/MSets/MSetList.v +++ b/theories/MSets/MSetList.v @@ -231,13 +231,16 @@ Module MakeRaw (X: OrderedType) <: RawSets X. Notation In := (InA X.eq). Existing Instance X.eq_equiv. + #[local] Hint Extern 20 => solve [order] : core. Definition IsOk s := Sort s. Class Ok (s:t) : Prop := ok : Sort s. + #[local] Hint Resolve ok : core. + #[local] Hint Unfold Ok : core. Instance Sort_Ok s `(Hs : Sort s) : Ok s := { ok := Hs }. @@ -276,6 +279,7 @@ Module MakeRaw (X: OrderedType) <: RawSets X. destruct H; constructor; tauto. Qed. + #[local] Hint Extern 1 (Ok _) => rewrite <- isok_iff : core. Ltac inv_ok := match goal with @@ -326,6 +330,7 @@ Module MakeRaw (X: OrderedType) <: RawSets X. intuition. intros; elim_compare x a; inv; intuition. Qed. + #[local] Hint Resolve add_inf : core. Global Instance add_ok s x : forall `(Ok s), Ok (add x s). @@ -353,6 +358,7 @@ Module MakeRaw (X: OrderedType) <: RawSets X. intros; elim_compare x a; inv; auto. apply Inf_lt with a; auto. Qed. + #[local] Hint Resolve remove_inf : core. Global Instance remove_ok s x : forall `(Ok s), Ok (remove x s). @@ -396,6 +402,7 @@ Module MakeRaw (X: OrderedType) <: RawSets X. Proof. induction2. Qed. + #[local] Hint Resolve union_inf : core. Global Instance union_ok s s' : forall `(Ok s, Ok s'), Ok (union s s'). @@ -422,6 +429,7 @@ Module MakeRaw (X: OrderedType) <: RawSets X. apply Hrec'; auto. apply Inf_lt with x'; auto. Qed. + #[local] Hint Resolve inter_inf : core. Global Instance inter_ok s s' : forall `(Ok s, Ok s'), Ok (inter s s'). @@ -452,6 +460,7 @@ Module MakeRaw (X: OrderedType) <: RawSets X. apply Hrec'; auto. apply Inf_lt with x'; auto. Qed. + #[local] Hint Resolve diff_inf : core. Global Instance diff_ok s s' : forall `(Ok s, Ok s'), Ok (diff s s'). diff --git a/theories/MSets/MSetProperties.v b/theories/MSets/MSetProperties.v index 51807e5cda..b49a91ed14 100644 --- a/theories/MSets/MSetProperties.v +++ b/theories/MSets/MSetProperties.v @@ -21,6 +21,7 @@ Require Import DecidableTypeEx OrdersLists MSetFacts MSetDecide. Set Implicit Arguments. Unset Strict Implicit. +#[global] Hint Unfold transpose : core. (** First, a functor for Weak Sets in functorial version. *) @@ -268,7 +269,9 @@ Module WPropertiesOn (Import E : DecidableType)(M : WSetsOn E). End BasicProperties. + #[global] Hint Immediate equal_sym add_remove remove_add union_sym inter_sym: set. + #[global] Hint Resolve equal_refl equal_trans subset_refl subset_equal subset_antisym subset_trans subset_empty subset_remove_3 subset_diff subset_add_3 subset_add_2 in_subset empty_is_empty_1 empty_is_empty_2 add_equal @@ -735,6 +738,7 @@ Module WPropertiesOn (Import E : DecidableType)(M : WSetsOn E). Proof. intros; rewrite cardinal_Empty; auto. Qed. + #[global] Hint Resolve cardinal_inv_1 : core. Lemma cardinal_inv_2 : @@ -774,6 +778,7 @@ Module WPropertiesOn (Import E : DecidableType)(M : WSetsOn E). exact Equal_cardinal. Qed. + #[global] Hint Resolve Add_add Add_remove Equal_remove cardinal_inv_1 Equal_cardinal : core. (** ** Cardinal and set operators *) @@ -783,6 +788,7 @@ Module WPropertiesOn (Import E : DecidableType)(M : WSetsOn E). rewrite cardinal_fold; apply fold_1; auto with *. Qed. + #[global] Hint Immediate empty_cardinal cardinal_1 : set. Lemma singleton_cardinal : forall x, cardinal (singleton x) = 1. @@ -793,6 +799,7 @@ Module WPropertiesOn (Import E : DecidableType)(M : WSetsOn E). apply cardinal_2 with x; auto with set. Qed. + #[global] Hint Resolve singleton_cardinal: set. Lemma diff_inter_cardinal : @@ -898,6 +905,7 @@ Module WPropertiesOn (Import E : DecidableType)(M : WSetsOn E). auto with set. Qed. + #[global] Hint Resolve subset_cardinal union_cardinal add_cardinal_1 add_cardinal_2 : core. End WPropertiesOn. @@ -922,7 +930,9 @@ Module OrdProperties (M:Sets). Import M.E. Import M. + #[global] Hint Resolve elements_spec2 : core. + #[global] Hint Immediate min_elt_spec1 min_elt_spec2 min_elt_spec3 max_elt_spec1 max_elt_spec2 max_elt_spec3 : set. @@ -961,6 +971,7 @@ Module OrdProperties (M:Sets). Proof. intros a b H; unfold leb. rewrite H; auto. Qed. + #[global] Hint Resolve gtb_compat leb_compat : core. Lemma elements_split : forall x s, diff --git a/theories/MSets/MSetWeakList.v b/theories/MSets/MSetWeakList.v index 2498d82889..8a5ba2d80f 100644 --- a/theories/MSets/MSetWeakList.v +++ b/theories/MSets/MSetWeakList.v @@ -123,14 +123,18 @@ Module MakeRaw (X:DecidableType) <: WRawSets X. Let eqr:= (@Equivalence_Reflexive _ _ X.eq_equiv). Let eqsym:= (@Equivalence_Symmetric _ _ X.eq_equiv). Let eqtrans:= (@Equivalence_Transitive _ _ X.eq_equiv). + #[local] Hint Resolve eqr eqtrans : core. + #[local] Hint Immediate eqsym : core. Definition IsOk := NoDup. Class Ok (s:t) : Prop := ok : NoDup s. + #[local] Hint Unfold Ok : core. + #[local] Hint Resolve ok : core. Instance NoDup_Ok s (nd : NoDup s) : Ok s := { ok := nd }. diff --git a/theories/Numbers/Cyclic/Int31/Cyclic31.v b/theories/Numbers/Cyclic/Int31/Cyclic31.v index f6b2544b6e..c5c75fc17a 100644 --- a/theories/Numbers/Cyclic/Int31/Cyclic31.v +++ b/theories/Numbers/Cyclic/Int31/Cyclic31.v @@ -467,6 +467,7 @@ Section Basics. apply phibis_aux_pos. Qed. + #[local] Hint Resolve phi_nonneg : zarith. Lemma phi_bounded : forall x, (0 <= phi x < 2 ^ (Z.of_nat size))%Z. diff --git a/theories/Numbers/Cyclic/Int63/Int63.v b/theories/Numbers/Cyclic/Int63/Int63.v index 383c0aff3a..dbca2f0947 100644 --- a/theories/Numbers/Cyclic/Int63/Int63.v +++ b/theories/Numbers/Cyclic/Int63/Int63.v @@ -290,6 +290,7 @@ Proof. intros h; apply Z.lt_gt, Zpower_gt_0; lia. Qed. Lemma pow2_nz n : 0 <= n → 2 ^ n ≠ 0. Proof. intros h; generalize (pow2_pos _ h); lia. Qed. +#[global] Hint Resolve pow2_pos pow2_nz : zarith. (* =================================================== *) diff --git a/theories/Numbers/Cyclic/ZModulo/ZModulo.v b/theories/Numbers/Cyclic/ZModulo/ZModulo.v index 5e486333b2..6aad65899a 100644 --- a/theories/Numbers/Cyclic/ZModulo/ZModulo.v +++ b/theories/Numbers/Cyclic/ZModulo/ZModulo.v @@ -61,6 +61,7 @@ Section ZModulo. apply Z.lt_gt. unfold wB, base; auto with zarith. Qed. + #[local] Hint Resolve wB_pos : core. Lemma spec_to_Z_1 : forall x, 0 <= [|x|]. @@ -72,6 +73,7 @@ Section ZModulo. Proof. unfold to_Z; intros; destruct (Z_mod_lt x wB wB_pos); auto. Qed. + #[local] Hint Resolve spec_to_Z_1 spec_to_Z_2 : core. Lemma spec_to_Z : forall x, 0 <= [|x|] < wB. @@ -706,6 +708,7 @@ Section ZModulo. Proof. induction p; simpl; auto with zarith. Qed. + #[local] Hint Resolve Ptail_pos : core. Lemma Ptail_bounded : forall p d, Zpos p < 2^(Zpos d) -> Ptail p < Zpos d. diff --git a/theories/Numbers/Natural/Abstract/NDefOps.v b/theories/Numbers/Natural/Abstract/NDefOps.v index 019b138b4d..2f8fcc7290 100644 --- a/theories/Numbers/Natural/Abstract/NDefOps.v +++ b/theories/Numbers/Natural/Abstract/NDefOps.v @@ -383,6 +383,7 @@ f_equiv. apply E, half_decrease. rewrite two_succ, <- not_true_iff_false, ltb_lt, nlt_ge, le_succ_l in H. order'. Qed. +#[global] Hint Resolve log_good_step : core. Theorem log_init : forall n, n < 2 -> log n == 0. diff --git a/theories/Program/Basics.v b/theories/Program/Basics.v index 3e282f696a..3ecb5a5a61 100644 --- a/theories/Program/Basics.v +++ b/theories/Program/Basics.v @@ -26,6 +26,7 @@ Arguments id {A} x. Definition compose {A B C} (g : B -> C) (f : A -> B) := fun x : A => g (f x). +#[global] Hint Unfold compose : core. Declare Scope program_scope. diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v index 5862a08838..25af2d5ffb 100644 --- a/theories/Program/Equality.v +++ b/theories/Program/Equality.v @@ -21,6 +21,7 @@ Ltac is_ground_goal := (** Try to find a contradiction. *) +#[global] Hint Extern 10 => is_ground_goal ; progress exfalso : exfalso. (** We will use the [block] definition to separate the goal from the @@ -308,6 +309,7 @@ Proof. intros. rewrite (UIP_refl A). assumption. Defined. (** This hint database and the following tactic can be used with [autounfold] to unfold everything to [eq_rect]s. *) +#[global] Hint Unfold solution_left solution_right deletion simplification_heq simplification_existT1 simplification_existT2 simplification_K eq_rect_r eq_rec eq_ind : dep_elim. diff --git a/theories/Program/Wf.v b/theories/Program/Wf.v index 688db8b812..d1be8812e9 100644 --- a/theories/Program/Wf.v +++ b/theories/Program/Wf.v @@ -108,6 +108,7 @@ Section Measure_well_founded. End Measure_well_founded. +#[global] Hint Resolve measure_wf : core. Section Fix_rects. diff --git a/theories/QArith/QArith_base.v b/theories/QArith/QArith_base.v index fa4f9134cc..b008c6c2aa 100644 --- a/theories/QArith/QArith_base.v +++ b/theories/QArith/QArith_base.v @@ -95,7 +95,9 @@ Proof. symmetry. apply Z.ge_le_iff. Qed. +#[global] Hint Unfold Qeq Qlt Qle : qarith. +#[global] Hint Extern 5 (?X1 <> ?X2) => intro; discriminate: qarith. Lemma Qcompare_antisym x y : CompOpp (x ?= y) = (y ?= x). @@ -127,7 +129,9 @@ apply Z.mul_reg_r with (QDen y); [auto with qarith|]. now rewrite Z.mul_shuffle0, XY, Z.mul_shuffle0, YZ, Z.mul_shuffle0. Qed. +#[global] Hint Immediate Qeq_sym : qarith. +#[global] Hint Resolve Qeq_refl Qeq_trans : qarith. (** In a word, [Qeq] is a setoid equality. *) @@ -203,6 +207,7 @@ Proof. rewrite !Qeq_bool_iff; apply Qeq_trans. Qed. +#[global] Hint Resolve Qnot_eq_sym : qarith. (** * Addition, multiplication and opposite *) @@ -783,6 +788,7 @@ Proof. Close Scope Z_scope. Qed. +#[global] Hint Resolve Qle_trans : qarith. Lemma Qlt_irrefl x : ~x<x. @@ -863,6 +869,7 @@ Proof. unfold Qle, Qlt, Qeq; intros; now apply Z.lt_eq_cases. Qed. +#[global] Hint Resolve Qle_not_lt Qlt_not_le Qnot_le_lt Qnot_lt_le Qlt_le_weak Qlt_not_eq Qle_antisym Qle_refl: qarith. @@ -904,6 +911,7 @@ Proof. Qed. +#[global] Hint Resolve Qopp_le_compat : qarith. Lemma Qle_minus_iff : forall p q, p <= q <-> 0 <= q+-p. diff --git a/theories/QArith/Qabs.v b/theories/QArith/Qabs.v index 13e88fc093..d1ff1fc794 100644 --- a/theories/QArith/Qabs.v +++ b/theories/QArith/Qabs.v @@ -11,6 +11,7 @@ Require Export QArith. Require Export Qreduction. +#[global] Hint Resolve Qlt_le_weak : qarith. Definition Qabs (x:Q) := let (n,d):=x in (Z.abs n#d). diff --git a/theories/QArith/Qcanon.v b/theories/QArith/Qcanon.v index 63b0a5afb7..bd43f901bb 100644 --- a/theories/QArith/Qcanon.v +++ b/theories/QArith/Qcanon.v @@ -66,6 +66,7 @@ Proof. rewrite hq, hq' in H'. subst q'. f_equal. apply eq_proofs_unicity. intros. repeat decide equality. Qed. +#[global] Hint Resolve Qc_is_canon : core. Theorem Qc_decomp: forall q q': Qc, (q:Q) = q' -> q = q'. diff --git a/theories/QArith/Qreals.v b/theories/QArith/Qreals.v index 20b5cb236b..5a23a20811 100644 --- a/theories/QArith/Qreals.v +++ b/theories/QArith/Qreals.v @@ -19,6 +19,7 @@ intros. now apply not_O_IZR. Qed. +#[global] Hint Resolve IZR_nz Rmult_integral_contrapositive : core. Lemma eqR_Qeq : forall x y : Q, Q2R x = Q2R y -> x==y. diff --git a/theories/QArith/Qround.v b/theories/QArith/Qround.v index 8fd342ab15..06f4ca02d1 100644 --- a/theories/QArith/Qround.v +++ b/theories/QArith/Qround.v @@ -18,6 +18,7 @@ rewrite !Z.mul_opp_l. apply Z.opp_lt_mono. Qed. +#[global] Hint Resolve Qopp_lt_compat : qarith. (************) @@ -54,6 +55,7 @@ rewrite Z.mul_comm. now apply Z.mul_div_le. Qed. +#[global] Hint Resolve Qfloor_le : qarith. Lemma Qle_ceiling : forall x, x <= Qceiling x. @@ -66,6 +68,7 @@ change (Qceiling x:Q) with (-(Qfloor(-x))). auto with *. Qed. +#[global] Hint Resolve Qle_ceiling : qarith. Lemma Qle_floor_ceiling : forall x, Qfloor x <= Qceiling x. @@ -88,6 +91,7 @@ rewrite <- Z.lt_add_lt_sub_r. destruct (Z_mod_lt n (Zpos d)); auto with *. Qed. +#[global] Hint Resolve Qlt_floor : qarith. Lemma Qceiling_lt : forall x, (Qceiling x-1)%Z < x. @@ -101,6 +105,7 @@ rewrite Qopp_involutive. auto with *. Qed. +#[global] Hint Resolve Qceiling_lt : qarith. Lemma Qfloor_resp_le : forall x y, x <= y -> (Qfloor x <= Qfloor y)%Z. @@ -114,6 +119,7 @@ rewrite (Z.mul_comm (Zpos yd) (Zpos xd)). apply Z_div_le; auto with *. Qed. +#[global] Hint Resolve Qfloor_resp_le : qarith. Lemma Qceiling_resp_le : forall x y, x <= y -> (Qceiling x <= Qceiling y)%Z. @@ -123,6 +129,7 @@ unfold Qceiling. rewrite <- Z.opp_le_mono; auto with qarith. Qed. +#[global] Hint Resolve Qceiling_resp_le : qarith. Add Morphism Qfloor with signature Qeq ==> eq as Qfloor_comp. diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v index 993b7b3ec4..fd8acf481a 100644 --- a/theories/Reals/RIneq.v +++ b/theories/Reals/RIneq.v @@ -37,10 +37,12 @@ Lemma Rle_refl : forall r, r <= r. Proof. intro; right; reflexivity. Qed. +#[global] Hint Immediate Rle_refl: rorders. Lemma Rge_refl : forall r, r <= r. Proof. exact Rle_refl. Qed. +#[global] Hint Immediate Rge_refl: rorders. (** Irreflexivity of the strict order *) @@ -49,6 +51,7 @@ Lemma Rlt_irrefl : forall r, ~ r < r. Proof. intros r H; eapply Rlt_asym; eauto. Qed. +#[global] Hint Resolve Rlt_irrefl: real. Lemma Rgt_irrefl : forall r, ~ r > r. @@ -72,6 +75,7 @@ Proof. - apply Rlt_not_eq in H1. eauto. - apply Rgt_not_eq in H1. eauto. Qed. +#[global] Hint Resolve Rlt_dichotomy_converse: real. (** Reasoning by case on equality and order *) @@ -82,6 +86,7 @@ Proof. intros; generalize (total_order_T r1 r2) Rlt_dichotomy_converse; unfold not; intuition eauto 3. Qed. +#[global] Hint Resolve Req_dec: real. (**********) @@ -110,6 +115,7 @@ Lemma Rlt_le : forall r1 r2, r1 < r2 -> r1 <= r2. Proof. intros; red; tauto. Qed. +#[global] Hint Resolve Rlt_le: real. Lemma Rgt_ge : forall r1 r2, r1 > r2 -> r1 >= r2. @@ -122,14 +128,18 @@ Lemma Rle_ge : forall r1 r2, r1 <= r2 -> r2 >= r1. Proof. destruct 1; red; auto with real. Qed. +#[global] Hint Immediate Rle_ge: real. +#[global] Hint Resolve Rle_ge: rorders. Lemma Rge_le : forall r1 r2, r1 >= r2 -> r2 <= r1. Proof. destruct 1; red; auto with real. Qed. +#[global] Hint Resolve Rge_le: real. +#[global] Hint Immediate Rge_le: rorders. (**********) @@ -137,12 +147,14 @@ Lemma Rlt_gt : forall r1 r2, r1 < r2 -> r2 > r1. Proof. trivial. Qed. +#[global] Hint Resolve Rlt_gt: rorders. Lemma Rgt_lt : forall r1 r2, r1 > r2 -> r2 < r1. Proof. trivial. Qed. +#[global] Hint Immediate Rgt_lt: rorders. (**********) @@ -151,6 +163,7 @@ Lemma Rnot_le_lt : forall r1 r2, ~ r1 <= r2 -> r2 < r1. Proof. intros r1 r2; generalize (Rtotal_order r1 r2); unfold Rle; tauto. Qed. +#[global] Hint Immediate Rnot_le_lt: real. Lemma Rnot_ge_gt : forall r1 r2, ~ r1 >= r2 -> r2 > r1. @@ -183,6 +196,7 @@ Proof. generalize Rlt_asym Rlt_dichotomy_converse; unfold Rle. unfold not; intuition eauto 3. Qed. +#[global] Hint Immediate Rlt_not_le: real. Lemma Rgt_not_le : forall r1 r2, r1 > r2 -> ~ r1 <= r2. @@ -190,6 +204,7 @@ Proof. exact Rlt_not_le. Qed. Lemma Rlt_not_ge : forall r1 r2, r1 < r2 -> ~ r1 >= r2. Proof. red; intros; eapply Rlt_not_le; eauto with real. Qed. +#[global] Hint Immediate Rlt_not_ge: real. Lemma Rgt_not_ge : forall r1 r2, r2 > r1 -> ~ r1 >= r2. @@ -215,24 +230,28 @@ Lemma Req_le : forall r1 r2, r1 = r2 -> r1 <= r2. Proof. unfold Rle; tauto. Qed. +#[global] Hint Immediate Req_le: real. Lemma Req_ge : forall r1 r2, r1 = r2 -> r1 >= r2. Proof. unfold Rge; tauto. Qed. +#[global] Hint Immediate Req_ge: real. Lemma Req_le_sym : forall r1 r2, r2 = r1 -> r1 <= r2. Proof. unfold Rle; auto. Qed. +#[global] Hint Immediate Req_le_sym: real. Lemma Req_ge_sym : forall r1 r2, r2 = r1 -> r1 >= r2. Proof. unfold Rge; auto. Qed. +#[global] Hint Immediate Req_ge_sym: real. (** *** Asymmetry *) @@ -248,6 +267,7 @@ Lemma Rle_antisym : forall r1 r2, r1 <= r2 -> r2 <= r1 -> r1 = r2. Proof. intros r1 r2; generalize (Rlt_asym r1 r2); unfold Rle; intuition. Qed. +#[global] Hint Resolve Rle_antisym: real. Lemma Rge_antisym : forall r1 r2, r1 >= r2 -> r2 >= r1 -> r1 = r2. @@ -387,12 +407,14 @@ Lemma Rplus_0_r : forall r, r + 0 = r. Proof. intro; ring. Qed. +#[global] Hint Resolve Rplus_0_r: real. Lemma Rplus_ne : forall r, r + 0 = r /\ 0 + r = r. Proof. split; ring. Qed. +#[global] Hint Resolve Rplus_ne: real. (**********) @@ -403,6 +425,7 @@ Lemma Rplus_opp_l : forall r, - r + r = 0. Proof. intro; ring. Qed. +#[global] Hint Resolve Rplus_opp_l: real. (**********) @@ -415,6 +438,7 @@ Qed. Definition f_equal_R := (f_equal (A:=R)). +#[global] Hint Resolve f_equal_R : real. Lemma Rplus_eq_compat_l : forall r r1 r2, r1 = r2 -> r + r1 = r + r2. @@ -439,6 +463,7 @@ Proof. repeat rewrite Rplus_assoc; rewrite <- H; reflexivity. ring. Qed. +#[global] Hint Resolve Rplus_eq_reg_l: real. Lemma Rplus_eq_reg_r : forall r r1 r2, r1 + r = r2 + r -> r1 = r2. @@ -485,18 +510,21 @@ Lemma Rinv_r : forall r, r <> 0 -> r * / r = 1. Proof. intros; field; trivial. Qed. +#[global] Hint Resolve Rinv_r: real. Lemma Rinv_l_sym : forall r, r <> 0 -> 1 = / r * r. Proof. intros; field; trivial. Qed. +#[global] Hint Resolve Rinv_l_sym: real. Lemma Rinv_r_sym : forall r, r <> 0 -> 1 = r * / r. Proof. intros; field; trivial. Qed. +#[global] Hint Resolve Rinv_r_sym: real. (**********) @@ -504,6 +532,7 @@ Lemma Rmult_0_r : forall r, r * 0 = 0. Proof. intro; ring. Qed. +#[global] Hint Resolve Rmult_0_r: real. (**********) @@ -511,6 +540,7 @@ Lemma Rmult_0_l : forall r, 0 * r = 0. Proof. intro; ring. Qed. +#[global] Hint Resolve Rmult_0_l: real. (**********) @@ -518,6 +548,7 @@ Lemma Rmult_ne : forall r, r * 1 = r /\ 1 * r = r. Proof. intro; split; ring. Qed. +#[global] Hint Resolve Rmult_ne: real. (**********) @@ -525,6 +556,7 @@ Lemma Rmult_1_r : forall r, r * 1 = r. Proof. intro; ring. Qed. +#[global] Hint Resolve Rmult_1_r: real. (**********) @@ -572,6 +604,7 @@ Proof. intros r1 r2 [H| H]; rewrite H; auto with real. Qed. +#[global] Hint Resolve Rmult_eq_0_compat: real. (**********) @@ -599,6 +632,7 @@ Proof. red; intros r1 r2 [H1 H2] H. case (Rmult_integral r1 r2); auto with real. Qed. +#[global] Hint Resolve Rmult_integral_contrapositive: real. Lemma Rmult_integral_contrapositive_currified : @@ -640,6 +674,7 @@ Lemma Ropp_eq_compat : forall r1 r2, r1 = r2 -> - r1 = - r2. Proof. auto with real. Qed. +#[global] Hint Resolve Ropp_eq_compat: real. (**********) @@ -647,6 +682,7 @@ Lemma Ropp_0 : -0 = 0. Proof. ring. Qed. +#[global] Hint Resolve Ropp_0: real. (**********) @@ -654,6 +690,7 @@ Lemma Ropp_eq_0_compat : forall r, r = 0 -> - r = 0. Proof. intros; rewrite H; auto with real. Qed. +#[global] Hint Resolve Ropp_eq_0_compat: real. (**********) @@ -661,6 +698,7 @@ Lemma Ropp_involutive : forall r, - - r = r. Proof. intro; ring. Qed. +#[global] Hint Resolve Ropp_involutive: real. (*********) @@ -670,6 +708,7 @@ Proof. apply H. transitivity (- - r); auto with real. Qed. +#[global] Hint Resolve Ropp_neq_0_compat: real. (**********) @@ -677,6 +716,7 @@ Lemma Ropp_plus_distr : forall r1 r2, - (r1 + r2) = - r1 + - r2. Proof. intros; ring. Qed. +#[global] Hint Resolve Ropp_plus_distr: real. (*********************************************************) @@ -692,6 +732,7 @@ Lemma Ropp_mult_distr_l_reverse : forall r1 r2, - r1 * r2 = - (r1 * r2). Proof. intros; ring. Qed. +#[global] Hint Resolve Ropp_mult_distr_l_reverse: real. (**********) @@ -699,6 +740,7 @@ Lemma Rmult_opp_opp : forall r1 r2, - r1 * - r2 = r1 * r2. Proof. intros; ring. Qed. +#[global] Hint Resolve Rmult_opp_opp: real. Lemma Ropp_mult_distr_r : forall r1 r2, - (r1 * r2) = r1 * - r2. @@ -719,12 +761,14 @@ Lemma Rminus_0_r : forall r, r - 0 = r. Proof. intro; ring. Qed. +#[global] Hint Resolve Rminus_0_r: real. Lemma Rminus_0_l : forall r, 0 - r = - r. Proof. intro; ring. Qed. +#[global] Hint Resolve Rminus_0_l: real. (**********) @@ -732,6 +776,7 @@ Lemma Ropp_minus_distr : forall r1 r2, - (r1 - r2) = r2 - r1. Proof. intros; ring. Qed. +#[global] Hint Resolve Ropp_minus_distr: real. Lemma Ropp_minus_distr' : forall r1 r2, - (r2 - r1) = r1 - r2. @@ -744,6 +789,7 @@ Lemma Rminus_diag_eq : forall r1 r2, r1 = r2 -> r1 - r2 = 0. Proof. intros; rewrite H; ring. Qed. +#[global] Hint Resolve Rminus_diag_eq: real. Lemma Rminus_eq_0 x : x - x = 0. @@ -755,6 +801,7 @@ Proof. intros r1 r2; unfold Rminus; rewrite Rplus_comm; intro. rewrite <- (Ropp_involutive r2); apply (Rplus_opp_r_uniq (- r2) r1 H). Qed. +#[global] Hint Immediate Rminus_diag_uniq: real. Lemma Rminus_diag_uniq_sym : forall r1 r2, r2 - r1 = 0 -> r1 = r2. @@ -762,12 +809,14 @@ Proof. intros; generalize (Rminus_diag_uniq r2 r1 H); clear H; intro H; rewrite H; ring. Qed. +#[global] Hint Immediate Rminus_diag_uniq_sym: real. Lemma Rplus_minus : forall r1 r2, r1 + (r2 - r1) = r2. Proof. intros; ring. Qed. +#[global] Hint Resolve Rplus_minus: real. (**********) @@ -776,18 +825,21 @@ Proof. red; intros r1 r2 H H0. apply H; auto with real. Qed. +#[global] Hint Resolve Rminus_eq_contra: real. Lemma Rminus_not_eq : forall r1 r2, r1 - r2 <> 0 -> r1 <> r2. Proof. red; intros; elim H; apply Rminus_diag_eq; auto. Qed. +#[global] Hint Resolve Rminus_not_eq: real. Lemma Rminus_not_eq_right : forall r1 r2, r2 - r1 <> 0 -> r1 <> r2. Proof. red; intros; elim H; rewrite H0; ring. Qed. +#[global] Hint Resolve Rminus_not_eq_right: real. (**********) @@ -809,6 +861,7 @@ Lemma Rinv_1 : / 1 = 1. Proof. field. Qed. +#[global] Hint Resolve Rinv_1: real. (*********) @@ -817,6 +870,7 @@ Proof. red; intros; apply R1_neq_R0. replace 1 with (/ r * r); auto with real. Qed. +#[global] Hint Resolve Rinv_neq_0_compat: real. (*********) @@ -824,6 +878,7 @@ Lemma Rinv_involutive : forall r, r <> 0 -> / / r = r. Proof. intros; field; trivial. Qed. +#[global] Hint Resolve Rinv_involutive: real. (*********) @@ -857,6 +912,7 @@ Proof. transitivity (r2 * (r1 * / r1)); auto with real. ring. Qed. +#[global] Hint Resolve Rinv_r_simpl_l Rinv_r_simpl_r Rinv_r_simpl_m: real. (*********) @@ -878,6 +934,7 @@ Qed. Lemma Rplus_gt_compat_l : forall r r1 r2, r1 > r2 -> r + r1 > r + r2. Proof. eauto using Rplus_lt_compat_l with rorders. Qed. +#[global] Hint Resolve Rplus_gt_compat_l: real. (**********) @@ -886,6 +943,7 @@ Proof. intros. rewrite (Rplus_comm r1 r); rewrite (Rplus_comm r2 r); auto with real. Qed. +#[global] Hint Resolve Rplus_lt_compat_r: real. Lemma Rplus_gt_compat_r : forall r r1 r2, r1 > r2 -> r1 + r > r2 + r. @@ -901,6 +959,7 @@ Qed. Lemma Rplus_ge_compat_l : forall r r1 r2, r1 >= r2 -> r + r1 >= r + r2. Proof. auto using Rplus_le_compat_l with rorders. Qed. +#[global] Hint Resolve Rplus_ge_compat_l: real. (**********) @@ -911,6 +970,7 @@ Proof. right; rewrite <- H0; auto with real. Qed. +#[global] Hint Resolve Rplus_le_compat_l Rplus_le_compat_r: real. Lemma Rplus_ge_compat_r : forall r r1 r2, r1 >= r2 -> r1 + r >= r2 + r. @@ -922,6 +982,7 @@ Lemma Rplus_lt_compat : Proof. intros; apply Rlt_trans with (r2 + r3); auto with real. Qed. +#[global] Hint Immediate Rplus_lt_compat: real. Lemma Rplus_le_compat : @@ -929,6 +990,7 @@ Lemma Rplus_le_compat : Proof. intros; apply Rle_trans with (r2 + r3); auto with real. Qed. +#[global] Hint Immediate Rplus_le_compat: real. Lemma Rplus_gt_compat : @@ -952,6 +1014,7 @@ Proof. intros; apply Rle_lt_trans with (r2 + r3); auto with real. Qed. +#[global] Hint Immediate Rplus_lt_le_compat Rplus_le_lt_compat: real. Lemma Rplus_gt_ge_compat : @@ -1091,6 +1154,7 @@ Proof. apply CReal_opp_gt_lt_contravar. unfold Rgt in H. rewrite Rlt_def in H. apply CRealLtEpsilon. exact H. Qed. +#[global] Hint Resolve Ropp_gt_lt_contravar : core. Lemma Ropp_lt_gt_contravar : forall r1 r2, r1 < r2 -> - r1 > - r2. @@ -1100,6 +1164,7 @@ Proof. apply CReal_opp_gt_lt_contravar. rewrite Rlt_def in H. apply CRealLtEpsilon. exact H. Qed. +#[global] Hint Resolve Ropp_lt_gt_contravar: real. (**********) @@ -1107,6 +1172,7 @@ Lemma Ropp_lt_contravar : forall r1 r2, r2 < r1 -> - r1 < - r2. Proof. auto with real. Qed. +#[global] Hint Resolve Ropp_lt_contravar: real. Lemma Ropp_gt_contravar : forall r1 r2, r2 > r1 -> - r1 > - r2. @@ -1117,12 +1183,14 @@ Lemma Ropp_le_ge_contravar : forall r1 r2, r1 <= r2 -> - r1 >= - r2. Proof. unfold Rge; intros r1 r2 [H| H]; auto with real. Qed. +#[global] Hint Resolve Ropp_le_ge_contravar: real. Lemma Ropp_ge_le_contravar : forall r1 r2, r1 >= r2 -> - r1 <= - r2. Proof. unfold Rle; intros r1 r2 [H| H]; auto with real. Qed. +#[global] Hint Resolve Ropp_ge_le_contravar: real. (**********) @@ -1130,6 +1198,7 @@ Lemma Ropp_le_contravar : forall r1 r2, r2 <= r1 -> - r1 <= - r2. Proof. intros r1 r2 H; elim H; auto with real. Qed. +#[global] Hint Resolve Ropp_le_contravar: real. Lemma Ropp_ge_contravar : forall r1 r2, r2 >= r1 -> - r1 >= - r2. @@ -1140,12 +1209,14 @@ Lemma Ropp_0_lt_gt_contravar : forall r, 0 < r -> 0 > - r. Proof. intros; replace 0 with (-0); auto with real. Qed. +#[global] Hint Resolve Ropp_0_lt_gt_contravar: real. Lemma Ropp_0_gt_lt_contravar : forall r, 0 > r -> 0 < - r. Proof. intros; replace 0 with (-0); auto with real. Qed. +#[global] Hint Resolve Ropp_0_gt_lt_contravar: real. (**********) @@ -1153,12 +1224,14 @@ Lemma Ropp_lt_gt_0_contravar : forall r, r > 0 -> - r < 0. Proof. intros; rewrite <- Ropp_0; auto with real. Qed. +#[global] Hint Resolve Ropp_lt_gt_0_contravar: real. Lemma Ropp_gt_lt_0_contravar : forall r, r < 0 -> - r > 0. Proof. intros; rewrite <- Ropp_0; auto with real. Qed. +#[global] Hint Resolve Ropp_gt_lt_0_contravar: real. (**********) @@ -1166,12 +1239,14 @@ Lemma Ropp_0_le_ge_contravar : forall r, 0 <= r -> 0 >= - r. Proof. intros; replace 0 with (-0); auto with real. Qed. +#[global] Hint Resolve Ropp_0_le_ge_contravar: real. Lemma Ropp_0_ge_le_contravar : forall r, 0 >= r -> 0 <= - r. Proof. intros; replace 0 with (-0); auto with real. Qed. +#[global] Hint Resolve Ropp_0_ge_le_contravar: real. (** *** Cancellation *) @@ -1182,6 +1257,7 @@ Proof. rewrite <- (Ropp_involutive x); rewrite <- (Ropp_involutive y); auto with real. Qed. +#[global] Hint Immediate Ropp_lt_cancel: real. Lemma Ropp_gt_cancel : forall r1 r2, - r2 > - r1 -> r1 > r2. @@ -1194,6 +1270,7 @@ Proof. intro H1; rewrite <- (Ropp_involutive x); rewrite <- (Ropp_involutive y); rewrite H1; auto with real. Qed. +#[global] Hint Immediate Ropp_le_cancel: real. Lemma Ropp_ge_cancel : forall r1 r2, - r2 >= - r1 -> r1 >= r2. @@ -1211,6 +1288,7 @@ Lemma Rmult_lt_compat_r : forall r r1 r2, 0 < r -> r1 < r2 -> r1 * r < r2 * r. Proof. intros; rewrite (Rmult_comm r1 r); rewrite (Rmult_comm r2 r); auto with real. Qed. +#[global] Hint Resolve Rmult_lt_compat_r : core. Lemma Rmult_gt_compat_r : forall r r1 r2, r > 0 -> r1 > r2 -> r1 * r > r2 * r. @@ -1227,6 +1305,7 @@ Proof. auto with real. right; rewrite <- H; do 2 rewrite Rmult_0_l; reflexivity. Qed. +#[global] Hint Resolve Rmult_le_compat_l: real. Lemma Rmult_le_compat_r : @@ -1235,6 +1314,7 @@ Proof. intros r r1 r2 H; rewrite (Rmult_comm r1 r); rewrite (Rmult_comm r2 r); auto with real. Qed. +#[global] Hint Resolve Rmult_le_compat_r: real. Lemma Rmult_ge_compat_l : @@ -1256,6 +1336,7 @@ Proof. apply Rmult_le_compat_l; auto. apply Rle_trans with z; auto. Qed. +#[global] Hint Resolve Rmult_le_compat: real. Lemma Rmult_ge_compat : @@ -1297,6 +1378,7 @@ Proof. do 2 rewrite (Ropp_mult_distr_l_reverse (- r)). apply Ropp_le_contravar; auto with real. Qed. +#[global] Hint Resolve Rmult_le_compat_neg_l: real. Lemma Rmult_le_ge_compat_neg_l : @@ -1304,6 +1386,7 @@ Lemma Rmult_le_ge_compat_neg_l : Proof. intros; apply Rle_ge; auto with real. Qed. +#[global] Hint Resolve Rmult_le_ge_compat_neg_l: real. Lemma Rmult_lt_gt_compat_neg_l : @@ -1368,6 +1451,7 @@ Proof. replace (r2 + (r1 - r2)) with r1 by ring. now rewrite Rplus_0_r. Qed. +#[global] Hint Resolve Rlt_minus: real. Lemma Rgt_minus : forall r1 r2, r1 > r2 -> r1 - r2 > 0. @@ -1436,6 +1520,7 @@ Proof. intros; apply not_eq_sym; apply Rlt_not_eq. rewrite Rplus_comm; replace 0 with (0 + 0); auto with real. Qed. +#[global] Hint Immediate tech_Rplus: real. (*********************************************************) @@ -1458,6 +1543,7 @@ Proof. replace 0 with (- r * 0); auto with real. replace 0 with (0 * r); auto with real. Qed. +#[global] Hint Resolve Rle_0_sqr Rlt_0_sqr: real. (***********) @@ -1485,6 +1571,7 @@ Proof. replace 1 with (Rsqr 1); auto with real. unfold Rsqr; auto with real. Qed. +#[global] Hint Resolve Rlt_0_1: real. Lemma Rle_0_1 : 0 <= 1. @@ -1504,6 +1591,7 @@ Proof. replace 1 with (r * / r); auto with real. replace 0 with (r * 0); auto with real. Qed. +#[global] Hint Resolve Rinv_0_lt_compat: real. (*********) @@ -1514,6 +1602,7 @@ Proof. replace 1 with (r * / r); auto with real. replace 0 with (r * 0); auto with real. Qed. +#[global] Hint Resolve Rinv_lt_0_compat: real. (*********) @@ -1543,6 +1632,7 @@ Proof. apply Rlt_dichotomy_converse; right. red; apply Rlt_trans with (r2 := x); auto with real. Qed. +#[global] Hint Resolve Rinv_1_lt_contravar: real. (*********************************************************) @@ -1556,6 +1646,7 @@ Proof. apply Rlt_le_trans with 1; auto with real. pattern 1 at 1; replace 1 with (0 + 1); auto with real. Qed. +#[global] Hint Resolve Rle_lt_0_plus_1: real. (**********) @@ -1564,6 +1655,7 @@ Proof. intros. pattern r at 1; replace r with (r + 0); auto with real. Qed. +#[global] Hint Resolve Rlt_plus_1: real. (**********) @@ -1598,6 +1690,7 @@ Proof. repeat rewrite S_INR. rewrite Hrecn; ring. Qed. +#[global] Hint Resolve plus_INR: real. (**********) @@ -1608,6 +1701,7 @@ Proof. intros; repeat rewrite S_INR; simpl. rewrite H0; ring. Qed. +#[global] Hint Resolve minus_INR: real. (*********) @@ -1618,6 +1712,7 @@ Proof. intros; repeat rewrite S_INR; simpl. rewrite plus_INR; rewrite Hrecn; ring. Qed. +#[global] Hint Resolve mult_INR: real. Lemma pow_INR (m n: nat) : INR (m ^ n) = pow (INR m) n. @@ -1629,6 +1724,7 @@ Proof. simple induction 1; intros; auto with real. rewrite S_INR; auto with real. Qed. +#[global] Hint Resolve lt_0_INR: real. Lemma lt_INR : forall n m:nat, (n < m)%nat -> INR n < INR m. @@ -1637,12 +1733,14 @@ Proof. rewrite S_INR; auto with real. rewrite S_INR; apply Rlt_trans with (INR m0); auto with real. Qed. +#[global] Hint Resolve lt_INR: real. Lemma lt_1_INR : forall n:nat, (1 < n)%nat -> 1 < INR n. Proof. apply lt_INR. Qed. +#[global] Hint Resolve lt_1_INR: real. (**********) @@ -1652,6 +1750,7 @@ Proof. simpl; auto with real. apply Pos2Nat.is_pos. Qed. +#[global] Hint Resolve pos_INR_nat_of_P: real. (**********) @@ -1661,6 +1760,7 @@ Proof. simpl; auto with real. auto with arith real. Qed. +#[global] Hint Resolve pos_INR: real. Lemma INR_lt : forall n m:nat, INR n < INR m -> (n < m)%nat. @@ -1676,6 +1776,7 @@ Proof. rewrite 2!S_INR in H. apply Rplus_lt_reg_r with (1 := H). Qed. +#[global] Hint Resolve INR_lt: real. (*********) @@ -1685,6 +1786,7 @@ Proof. rewrite S_INR. apply Rle_trans with (INR m0); auto with real. Qed. +#[global] Hint Resolve le_INR: real. (**********) @@ -1694,6 +1796,7 @@ Proof. apply H. rewrite H1; trivial. Qed. +#[global] Hint Immediate INR_not_0: real. (**********) @@ -1704,6 +1807,7 @@ Proof. intros; rewrite S_INR. apply Rgt_not_eq; red; auto with real. Qed. +#[global] Hint Resolve not_0_INR: real. Lemma not_INR : forall n m:nat, n <> m -> INR n <> INR m. @@ -1714,6 +1818,7 @@ Proof. exfalso; auto. apply not_eq_sym; apply Rlt_dichotomy_converse; auto with real. Qed. +#[global] Hint Resolve not_INR: real. Lemma INR_eq : forall n m:nat, INR n = INR m -> n = m. @@ -1730,6 +1835,7 @@ Proof. generalize (INR_lt n m H0); intro; auto with arith. generalize (INR_eq n m H0); intro; rewrite H1; auto. Qed. +#[global] Hint Resolve INR_le: real. Lemma not_1_INR : forall n:nat, n <> 1%nat -> INR n <> 1. @@ -1737,6 +1843,7 @@ Proof. intros n. apply not_INR. Qed. +#[global] Hint Resolve not_1_INR: real. (*********************************************************) @@ -1967,10 +2074,15 @@ Proof. intros; red; intro; elim H; apply eq_IZR; assumption. Qed. +#[global] Hint Extern 0 (IZR _ <= IZR _) => apply IZR_le, Zle_bool_imp_le, eq_refl : real. +#[global] Hint Extern 0 (IZR _ >= IZR _) => apply Rle_ge, IZR_le, Zle_bool_imp_le, eq_refl : real. +#[global] Hint Extern 0 (IZR _ < IZR _) => apply IZR_lt, eq_refl : real. +#[global] Hint Extern 0 (IZR _ > IZR _) => apply IZR_lt, eq_refl : real. +#[global] Hint Extern 0 (IZR _ <> IZR _) => apply IZR_neq, Zeq_bool_neq, eq_refl : real. Lemma one_IZR_lt1 : forall n:Z, -1 < IZR n < 1 -> n = 0%Z. diff --git a/theories/Reals/Raxioms.v b/theories/Reals/Raxioms.v index 338c939a06..f1c9eb8eee 100644 --- a/theories/Reals/Raxioms.v +++ b/theories/Reals/Raxioms.v @@ -119,6 +119,7 @@ Lemma Rplus_comm : forall r1 r2:R, r1 + r2 = r2 + r1. Proof. intros. apply Rquot1. do 2 rewrite Rrepr_plus. apply CReal_plus_comm. Qed. +#[global] Hint Resolve Rplus_comm: real. (**********) @@ -127,6 +128,7 @@ Proof. intros. apply Rquot1. repeat rewrite Rrepr_plus. apply CReal_plus_assoc. Qed. +#[global] Hint Resolve Rplus_assoc: real. (**********) @@ -135,6 +137,7 @@ Proof. intros. apply Rquot1. rewrite Rrepr_plus, Rrepr_opp, Rrepr_0. apply CReal_plus_opp_r. Qed. +#[global] Hint Resolve Rplus_opp_r: real. (**********) @@ -143,6 +146,7 @@ Proof. intros. apply Rquot1. rewrite Rrepr_plus, Rrepr_0. apply CReal_plus_0_l. Qed. +#[global] Hint Resolve Rplus_0_l: real. (***********************************************************) @@ -154,6 +158,7 @@ Lemma Rmult_comm : forall r1 r2:R, r1 * r2 = r2 * r1. Proof. intros. apply Rquot1. do 2 rewrite Rrepr_mult. apply CReal_mult_comm. Qed. +#[global] Hint Resolve Rmult_comm: real. (**********) @@ -162,6 +167,7 @@ Proof. intros. apply Rquot1. repeat rewrite Rrepr_mult. apply CReal_mult_assoc. Qed. +#[global] Hint Resolve Rmult_assoc: real. (**********) @@ -171,6 +177,7 @@ Proof. - contradiction. - apply Rquot1. rewrite Rrepr_mult, Rquot2, Rrepr_1. apply CReal_inv_l. Qed. +#[global] Hint Resolve Rinv_l: real. (**********) @@ -179,6 +186,7 @@ Proof. intros. apply Rquot1. rewrite Rrepr_mult, Rrepr_1. apply CReal_mult_1_l. Qed. +#[global] Hint Resolve Rmult_1_l: real. (**********) @@ -197,6 +205,7 @@ Proof. pose proof (CRealLt_morph 0%CReal 0%CReal (CRealEq_refl _) 1%CReal 0%CReal H). apply (CRealLt_irrefl 0%CReal). apply H0. apply CRealLt_0_1. Qed. +#[global] Hint Resolve R1_neq_R0: real. (*********************************************************) @@ -211,6 +220,7 @@ Proof. rewrite Rrepr_mult, Rrepr_plus, Rrepr_plus, Rrepr_mult, Rrepr_mult. apply CReal_mult_plus_distr_l. Qed. +#[global] Hint Resolve Rmult_plus_distr_l: real. (*********************************************************) @@ -256,6 +266,7 @@ Proof. rewrite RbaseSymbolsImpl.Rlt_def in H0. apply CRealLtEpsilon. exact H0. Qed. +#[global] Hint Resolve Rlt_asym Rplus_lt_compat_l Rmult_lt_compat_l: real. (**********************************************************) diff --git a/theories/Reals/Rfunctions.v b/theories/Reals/Rfunctions.v index d64e635d0f..4aa6edb2c4 100644 --- a/theories/Reals/Rfunctions.v +++ b/theories/Reals/Rfunctions.v @@ -102,6 +102,7 @@ Proof. apply H; assumption. Qed. +#[global] Hint Resolve pow_O pow_1 pow_add pow_nonzero: real. Lemma pow_RN_plus : @@ -117,6 +118,7 @@ Proof. intros x n; elim n; simpl; auto with real. intros n0 H' H'0; replace 0 with (x * 0); auto with real. Qed. +#[global] Hint Resolve pow_lt: real. Lemma Rlt_pow_R1 : forall (x:R) (n:nat), 1 < x -> (0 < n)%nat -> 1 < x ^ n. @@ -132,6 +134,7 @@ Proof. apply Rlt_trans with (r2 := 1); auto with real. apply H'; auto with arith. Qed. +#[global] Hint Resolve Rlt_pow_R1: real. Lemma Rlt_pow : forall (x:R) (n m:nat), 1 < x -> (n < m)%nat -> x ^ n < x ^ m. @@ -153,6 +156,7 @@ Proof. rewrite le_plus_minus_r; auto with arith; rewrite <- plus_n_O; auto. rewrite plus_comm; auto with arith. Qed. +#[global] Hint Resolve Rlt_pow: real. (*********) @@ -628,6 +632,7 @@ Proof. rewrite pow_add; auto with real. apply Rinv_mult_distr; apply pow_nonzero; auto. Qed. +#[local] Hint Resolve powerRZ_O powerRZ_1 powerRZ_NOR powerRZ_add: real. Lemma Zpower_nat_powerRZ : @@ -661,12 +666,14 @@ Lemma powerRZ_lt : forall (x:R) (z:Z), 0 < x -> 0 < x ^Z z. Proof. intros x z; case z; simpl; auto with real. Qed. +#[local] Hint Resolve powerRZ_lt: real. Lemma powerRZ_le : forall (x:R) (z:Z), 0 < x -> 0 <= x ^Z z. Proof. intros x z H'; apply Rlt_le; auto with real. Qed. +#[local] Hint Resolve powerRZ_le: real. Lemma Zpower_nat_powerRZ_absolu : diff --git a/theories/Relations/Relation_Definitions.v b/theories/Relations/Relation_Definitions.v index 7d0dffdd00..d0d633a0c4 100644 --- a/theories/Relations/Relation_Definitions.v +++ b/theories/Relations/Relation_Definitions.v @@ -68,10 +68,13 @@ Section Relation_Definition. End Relation_Definition. +#[global] Hint Unfold reflexive transitive antisymmetric symmetric: sets. +#[global] Hint Resolve Build_preorder Build_order Build_equivalence Build_PER preord_refl preord_trans ord_refl ord_trans ord_antisym equiv_refl equiv_trans equiv_sym per_sym per_trans: sets. +#[global] Hint Unfold inclusion same_relation commut: sets. diff --git a/theories/Relations/Relation_Operators.v b/theories/Relations/Relation_Operators.v index f0f36149d1..520333332a 100644 --- a/theories/Relations/Relation_Operators.v +++ b/theories/Relations/Relation_Operators.v @@ -228,8 +228,11 @@ Section Lexicographic_Exponentiation. End Lexicographic_Exponentiation. +#[global] Hint Unfold transp union: sets. +#[global] Hint Resolve t_step rt_step rt_refl rst_step rst_refl: sets. +#[global] Hint Immediate rst_sym: sets. (* begin hide *) diff --git a/theories/Sets/Classical_sets.v b/theories/Sets/Classical_sets.v index 68d200e189..430f35eecb 100644 --- a/theories/Sets/Classical_sets.v +++ b/theories/Sets/Classical_sets.v @@ -77,6 +77,7 @@ Section Ensembles_classical. Proof. unfold Subtract at 1; auto with sets. Qed. + #[local] Hint Resolve Subtract_intro : sets. Lemma Subtract_inv : @@ -123,5 +124,6 @@ Section Ensembles_classical. End Ensembles_classical. + #[global] Hint Resolve Strict_super_set_contains_new_element Subtract_intro not_SIncl_empty: sets. diff --git a/theories/Sets/Constructive_sets.v b/theories/Sets/Constructive_sets.v index 5027679266..ae7cdc9a0f 100644 --- a/theories/Sets/Constructive_sets.v +++ b/theories/Sets/Constructive_sets.v @@ -140,6 +140,7 @@ Section Ensembles_facts. End Ensembles_facts. +#[global] Hint Resolve Singleton_inv Singleton_intro Add_intro1 Add_intro2 Intersection_inv Couple_inv Setminus_intro Strict_Included_intro Strict_Included_strict Noone_in_empty Inhabited_not_empty Add_not_Empty diff --git a/theories/Sets/Cpo.v b/theories/Sets/Cpo.v index face010746..581c16778d 100644 --- a/theories/Sets/Cpo.v +++ b/theories/Sets/Cpo.v @@ -92,6 +92,7 @@ Section Bounds. exists bsup : _, Lub X bsup) -> Conditionally_complete. End Bounds. +#[global] Hint Resolve Totally_ordered_definition Upper_Bound_definition Lower_Bound_definition Lub_definition Glb_definition Bottom_definition Definition_of_Complete Definition_of_Complete diff --git a/theories/Sets/Ensembles.v b/theories/Sets/Ensembles.v index fb33f7834c..96fb070071 100644 --- a/theories/Sets/Ensembles.v +++ b/theories/Sets/Ensembles.v @@ -92,8 +92,10 @@ Section Ensembles. End Ensembles. +#[global] Hint Unfold In Included Same_set Strict_Included Add Setminus Subtract: sets. +#[global] Hint Resolve Union_introl Union_intror Intersection_intro In_singleton Couple_l Couple_r Triple_l Triple_m Triple_r Disjoint_intro Extensionality_Ensembles: sets. diff --git a/theories/Sets/Finite_sets.v b/theories/Sets/Finite_sets.v index e8e2a66e98..683979be74 100644 --- a/theories/Sets/Finite_sets.v +++ b/theories/Sets/Finite_sets.v @@ -45,7 +45,9 @@ Section Ensembles_finis. End Ensembles_finis. +#[global] Hint Resolve Empty_is_finite Union_is_finite: sets. +#[global] Hint Resolve card_empty card_add: sets. Require Import Constructive_sets. diff --git a/theories/Sets/Image.v b/theories/Sets/Image.v index 023eeaac9d..e83ff223f3 100644 --- a/theories/Sets/Image.v +++ b/theories/Sets/Image.v @@ -202,4 +202,5 @@ Section Image. End Image. +#[global] Hint Resolve Im_def image_empty finite_image: sets. diff --git a/theories/Sets/Infinite_sets.v b/theories/Sets/Infinite_sets.v index b3d7ed0b7b..766f62af45 100644 --- a/theories/Sets/Infinite_sets.v +++ b/theories/Sets/Infinite_sets.v @@ -46,6 +46,7 @@ Section Approx. Defn_of_Approximant : Finite U X -> Included U X A -> Approximant A X. End Approx. +#[global] Hint Resolve Defn_of_Approximant : core. Section Infinite_sets. diff --git a/theories/Sets/Multiset.v b/theories/Sets/Multiset.v index 4d0cd1174c..3f3cade37d 100644 --- a/theories/Sets/Multiset.v +++ b/theories/Sets/Multiset.v @@ -187,7 +187,10 @@ End multiset_defs. Unset Implicit Arguments. +#[global] Hint Unfold meq multiplicity: datatypes. +#[global] Hint Resolve munion_empty_right munion_comm munion_ass meq_left meq_right munion_empty_left: datatypes. +#[global] Hint Immediate meq_sym: datatypes. diff --git a/theories/Sets/Partial_Order.v b/theories/Sets/Partial_Order.v index 875afe3f44..879a7df608 100644 --- a/theories/Sets/Partial_Order.v +++ b/theories/Sets/Partial_Order.v @@ -53,7 +53,9 @@ Section Partial_orders. End Partial_orders. +#[global] Hint Unfold Carrier_of Rel_of Strict_Rel_of: sets. +#[global] Hint Resolve Definition_of_covers: sets. diff --git a/theories/Sets/Powerset.v b/theories/Sets/Powerset.v index 96d04100b9..617836225c 100644 --- a/theories/Sets/Powerset.v +++ b/theories/Sets/Powerset.v @@ -38,12 +38,14 @@ Variable U : Type. Inductive Power_set (A:Ensemble U) : Ensemble (Ensemble U) := Definition_of_Power_set : forall X:Ensemble U, Included U X A -> In (Ensemble U) (Power_set A) X. +#[local] Hint Resolve Definition_of_Power_set : core. Theorem Empty_set_minimal : forall X:Ensemble U, Included U (Empty_set U) X. intro X; red. intros x H'; elim H'. Qed. +#[local] Hint Resolve Empty_set_minimal : core. Theorem Power_set_Inhabited : @@ -51,22 +53,26 @@ Theorem Power_set_Inhabited : intro X. apply Inhabited_intro with (Empty_set U); auto with sets. Qed. +#[local] Hint Resolve Power_set_Inhabited : core. Theorem Inclusion_is_an_order : Order (Ensemble U) (Included U). auto 6 with sets. Qed. +#[local] Hint Resolve Inclusion_is_an_order : core. Theorem Inclusion_is_transitive : Transitive (Ensemble U) (Included U). elim Inclusion_is_an_order; auto with sets. Qed. +#[local] Hint Resolve Inclusion_is_transitive : core. Definition Power_set_PO : Ensemble U -> PO (Ensemble U). intro A; try assumption. apply Definition_of_PO with (Power_set A) (Included U); auto with sets. Defined. +#[local] Hint Unfold Power_set_PO : core. Theorem Strict_Rel_is_Strict_Included : @@ -74,6 +80,7 @@ Theorem Strict_Rel_is_Strict_Included : (Strict_Rel_of (Ensemble U) (Power_set_PO (Full_set U))). auto with sets. Qed. +#[local] Hint Resolve Strict_Rel_Transitive Strict_Rel_is_Strict_Included : core. Lemma Strict_inclusion_is_transitive_with_inclusion : @@ -109,6 +116,7 @@ Theorem Empty_set_is_Bottom : forall A:Ensemble U, Bottom (Ensemble U) (Power_set_PO A) (Empty_set U). intro A; apply Bottom_definition; simpl; auto with sets. Qed. +#[local] Hint Resolve Empty_set_is_Bottom : core. Theorem Union_minimal : @@ -117,6 +125,7 @@ Theorem Union_minimal : intros a b X H' H'0; red. intros x H'1; elim H'1; auto with sets. Qed. +#[local] Hint Resolve Union_minimal : core. Theorem Intersection_maximal : @@ -144,6 +153,7 @@ Theorem Intersection_decreases_r : intros a b; red. intros x H'; elim H'; auto with sets. Qed. +#[local] Hint Resolve Union_increases_l Union_increases_r Intersection_decreases_l Intersection_decreases_r : core. @@ -177,14 +187,25 @@ Qed. End The_power_set_partial_order. +#[global] Hint Resolve Empty_set_minimal: sets. +#[global] Hint Resolve Power_set_Inhabited: sets. +#[global] Hint Resolve Inclusion_is_an_order: sets. +#[global] Hint Resolve Inclusion_is_transitive: sets. +#[global] Hint Resolve Union_minimal: sets. +#[global] Hint Resolve Union_increases_l: sets. +#[global] Hint Resolve Union_increases_r: sets. +#[global] Hint Resolve Intersection_decreases_l: sets. +#[global] Hint Resolve Intersection_decreases_r: sets. +#[global] Hint Resolve Empty_set_is_Bottom: sets. +#[global] Hint Resolve Strict_inclusion_is_transitive: sets. diff --git a/theories/Sets/Powerset_Classical_facts.v b/theories/Sets/Powerset_Classical_facts.v index b83485bbf3..0fe63c5b66 100644 --- a/theories/Sets/Powerset_Classical_facts.v +++ b/theories/Sets/Powerset_Classical_facts.v @@ -92,6 +92,7 @@ Section Sets_as_an_algebra. apply Subtract_intro; auto with sets. red; intro H'1; apply H'; rewrite H'1; auto with sets. Qed. + #[local] Hint Resolve incl_soustr_add_r: sets. Lemma add_soustr_2 : @@ -330,9 +331,15 @@ Section Sets_as_an_algebra. End Sets_as_an_algebra. +#[global] Hint Resolve incl_soustr_in: sets. +#[global] Hint Resolve incl_soustr: sets. +#[global] Hint Resolve incl_soustr_add_l: sets. +#[global] Hint Resolve incl_soustr_add_r: sets. +#[global] Hint Resolve add_soustr_1 add_soustr_2: sets. +#[global] Hint Resolve add_soustr_xy: sets. diff --git a/theories/Sets/Powerset_facts.v b/theories/Sets/Powerset_facts.v index 69b28f14e4..b21c48d305 100644 --- a/theories/Sets/Powerset_facts.v +++ b/theories/Sets/Powerset_facts.v @@ -348,6 +348,7 @@ Section Sets_as_an_algebra. End Sets_as_an_algebra. +#[global] Hint Resolve Empty_set_zero Empty_set_zero' Union_associative Union_add singlx incl_add: sets. diff --git a/theories/Sets/Relations_1.v b/theories/Sets/Relations_1.v index 42755b551f..1167ad36bf 100644 --- a/theories/Sets/Relations_1.v +++ b/theories/Sets/Relations_1.v @@ -61,7 +61,9 @@ Section Relations_1. Definition_of_PER : Symmetric -> Transitive -> PER. End Relations_1. +#[global] Hint Unfold Reflexive Transitive Antisymmetric Symmetric contains same_relation: sets. +#[global] Hint Resolve Definition_of_preorder Definition_of_order Definition_of_equivalence Definition_of_PER: sets. diff --git a/theories/Sets/Relations_1_facts.v b/theories/Sets/Relations_1_facts.v index 21fc7ceaf2..6d7b837b63 100644 --- a/theories/Sets/Relations_1_facts.v +++ b/theories/Sets/Relations_1_facts.v @@ -52,6 +52,7 @@ apply Definition_of_equivalence. split; apply H'1 with y; auto 10 with sets. - red; intros x y h; elim h; intros H'3 H'4; auto 10 with sets. Qed. +#[global] Hint Resolve Equiv_from_preorder : core. Theorem Equiv_from_order : @@ -60,6 +61,7 @@ Theorem Equiv_from_order : Proof. intros U R H'; elim H'; auto 10 with sets. Qed. +#[global] Hint Resolve Equiv_from_order : core. Theorem contains_is_preorder : @@ -67,6 +69,7 @@ Theorem contains_is_preorder : Proof. auto 10 with sets. Qed. +#[global] Hint Resolve contains_is_preorder : core. Theorem same_relation_is_equivalence : @@ -74,6 +77,7 @@ Theorem same_relation_is_equivalence : Proof. unfold same_relation at 1; auto 10 with sets. Qed. +#[global] Hint Resolve same_relation_is_equivalence : core. Theorem cong_reflexive_same_relation : diff --git a/theories/Sets/Relations_2.v b/theories/Sets/Relations_2.v index 5e3206dd9b..e180798d1f 100644 --- a/theories/Sets/Relations_2.v +++ b/theories/Sets/Relations_2.v @@ -50,7 +50,11 @@ Definition Strongly_confluent : Prop := End Relations_2. +#[global] Hint Resolve Rstar_0: sets. +#[global] Hint Resolve Rstar1_0: sets. +#[global] Hint Resolve Rstar1_1: sets. +#[global] Hint Resolve Rplus_0: sets. diff --git a/theories/Sets/Relations_3.v b/theories/Sets/Relations_3.v index 9ebbba485c..d5c4040033 100644 --- a/theories/Sets/Relations_3.v +++ b/theories/Sets/Relations_3.v @@ -53,10 +53,16 @@ Section Relations_3. Definition Noetherian : Prop := forall x:U, noetherian x. End Relations_3. +#[global] Hint Unfold coherent: sets. +#[global] Hint Unfold locally_confluent: sets. +#[global] Hint Unfold confluent: sets. +#[global] Hint Unfold Confluent: sets. +#[global] Hint Resolve definition_of_noetherian: sets. +#[global] Hint Unfold Noetherian: sets. diff --git a/theories/Sets/Relations_3_facts.v b/theories/Sets/Relations_3_facts.v index db51186ef1..9f4869a625 100644 --- a/theories/Sets/Relations_3_facts.v +++ b/theories/Sets/Relations_3_facts.v @@ -38,6 +38,7 @@ Proof. intros U R x y H'; red. exists y; auto with sets. Qed. +#[global] Hint Resolve Rstar_imp_coherent : core. Theorem coherent_symmetric : diff --git a/theories/Sets/Uniset.v b/theories/Sets/Uniset.v index 474b417e8e..d8fe7f6dbe 100644 --- a/theories/Sets/Uniset.v +++ b/theories/Sets/Uniset.v @@ -41,20 +41,24 @@ Definition Singleton (a:A) := end). Definition In (s:uniset) (a:A) : Prop := charac s a = true. +#[local] Hint Unfold In : core. (** uniset inclusion *) Definition incl (s1 s2:uniset) := forall a:A, Bool.le (charac s1 a) (charac s2 a). +#[local] Hint Unfold incl : core. (** uniset equality *) Definition seq (s1 s2:uniset) := forall a:A, charac s1 a = charac s2 a. +#[local] Hint Unfold seq : core. Lemma le_refl : forall b, Bool.le b b. Proof. destruct b; simpl; auto. Qed. +#[local] Hint Resolve le_refl : core. Lemma incl_left : forall s1 s2:uniset, seq s1 s2 -> incl s1 s2. @@ -71,6 +75,7 @@ Lemma seq_refl : forall x:uniset, seq x x. Proof. destruct x; unfold seq; auto. Qed. +#[local] Hint Resolve seq_refl : core. Lemma seq_trans : forall x y z:uniset, seq x y -> seq y z -> seq x z. @@ -94,6 +99,7 @@ Lemma union_empty_left : forall x:uniset, seq x (union Emptyset x). Proof. unfold seq; unfold union; simpl; auto. Qed. +#[local] Hint Resolve union_empty_left : core. Lemma union_empty_right : forall x:uniset, seq x (union x Emptyset). @@ -101,6 +107,7 @@ Proof. unfold seq; unfold union; simpl. intros x a; rewrite (orb_b_false (charac x a)); auto. Qed. +#[local] Hint Resolve union_empty_right : core. Lemma union_comm : forall x y:uniset, seq (union x y) (union y x). @@ -108,6 +115,7 @@ Proof. unfold seq; unfold charac; unfold union. destruct x; destruct y; auto with bool. Qed. +#[local] Hint Resolve union_comm : core. Lemma union_ass : @@ -116,6 +124,7 @@ Proof. unfold seq; unfold union; unfold charac. destruct x; destruct y; destruct z; auto with bool. Qed. +#[local] Hint Resolve union_ass : core. Lemma seq_left : forall x y z:uniset, seq x y -> seq (union x z) (union y z). @@ -124,6 +133,7 @@ unfold seq; unfold union; unfold charac. destruct x; destruct y; destruct z. intros; elim H; auto. Qed. +#[local] Hint Resolve seq_left : core. Lemma seq_right : forall x y z:uniset, seq x y -> seq (union z x) (union z y). @@ -132,6 +142,7 @@ unfold seq; unfold union; unfold charac. destruct x; destruct y; destruct z. intros; elim H; auto. Qed. +#[local] Hint Resolve seq_right : core. diff --git a/theories/Sorting/CPermutation.v b/theories/Sorting/CPermutation.v index 31d9f7f0ed..cebb0c808c 100644 --- a/theories/Sorting/CPermutation.v +++ b/theories/Sorting/CPermutation.v @@ -96,6 +96,7 @@ Qed. End CPermutation. +#[global] Hint Resolve CPermutation_refl : core. (* These hints do not reduce the size of the problem to solve and they diff --git a/theories/Sorting/Heap.v b/theories/Sorting/Heap.v index 1130c9dd76..05a21620b7 100644 --- a/theories/Sorting/Heap.v +++ b/theories/Sorting/Heap.v @@ -36,7 +36,9 @@ Section defs. Hypothesis leA_trans : forall x y z:A, leA x y -> leA y z -> leA x z. Hypothesis leA_antisym : forall x y:A, leA x y -> leA y x -> eqA x y. + #[local] Hint Resolve leA_refl : core. + #[local] Hint Immediate eqA_dec leA_dec leA_antisym : core. Let emptyBag := EmptyBag A. diff --git a/theories/Sorting/Permutation.v b/theories/Sorting/Permutation.v index 2f445c341a..45fb48ad5d 100644 --- a/theories/Sorting/Permutation.v +++ b/theories/Sorting/Permutation.v @@ -76,6 +76,7 @@ Qed. End Permutation. +#[global] Hint Resolve Permutation_refl perm_nil perm_skip : core. (* These hints do not reduce the size of the problem to solve and they diff --git a/theories/Sorting/Sorted.v b/theories/Sorting/Sorted.v index 8cba461082..206eb606d2 100644 --- a/theories/Sorting/Sorted.v +++ b/theories/Sorting/Sorted.v @@ -137,7 +137,9 @@ Section defs. End defs. +#[global] Hint Constructors HdRel : core. +#[global] Hint Constructors Sorted : core. (* begin hide *) diff --git a/theories/Structures/DecidableType.v b/theories/Structures/DecidableType.v index 0c3bd9393b..c923b503a7 100644 --- a/theories/Structures/DecidableType.v +++ b/theories/Structures/DecidableType.v @@ -38,7 +38,9 @@ Module KeyDecidableType(D:DecidableType). Definition eqke (p p':key*elt) := eq (fst p) (fst p') /\ (snd p) = (snd p'). + #[local] Hint Unfold eqk eqke : core. + #[local] Hint Extern 2 (eqke ?a ?b) => split : core. (* eqke is stricter than eqk *) @@ -70,7 +72,9 @@ Module KeyDecidableType(D:DecidableType). unfold eqke; intuition; [ eauto | congruence ]. Qed. + #[local] Hint Resolve eqk_trans eqke_trans eqk_refl eqke_refl : core. + #[local] Hint Immediate eqk_sym eqke_sym : core. Global Instance eqk_equiv : Equivalence eqk. @@ -84,6 +88,7 @@ Module KeyDecidableType(D:DecidableType). Proof. unfold eqke; induction 1; intuition. Qed. + #[local] Hint Resolve InA_eqke_eqk : core. Lemma InA_eqk : forall p q m, eqk p q -> InA eqk p m -> InA eqk q m. @@ -94,6 +99,7 @@ Module KeyDecidableType(D:DecidableType). Definition MapsTo (k:key)(e:elt):= InA eqke (k,e). Definition In k m := exists e:elt, MapsTo k e m. + #[local] Hint Unfold MapsTo In : core. (* An alternative formulation for [In k l] is [exists e, InA eqk (k,e) l] *) @@ -140,12 +146,19 @@ Module KeyDecidableType(D:DecidableType). End Elt. + #[global] Hint Unfold eqk eqke : core. + #[global] Hint Extern 2 (eqke ?a ?b) => split : core. + #[global] Hint Resolve eqk_trans eqke_trans eqk_refl eqke_refl : core. + #[global] Hint Immediate eqk_sym eqke_sym : core. + #[global] Hint Resolve InA_eqke_eqk : core. + #[global] Hint Unfold MapsTo In : core. + #[global] Hint Resolve In_inv_2 In_inv_3 : core. End KeyDecidableType. diff --git a/theories/Structures/Equalities.v b/theories/Structures/Equalities.v index 914361d718..7cd5943a3f 100644 --- a/theories/Structures/Equalities.v +++ b/theories/Structures/Equalities.v @@ -53,7 +53,9 @@ Module Type IsEqOrig (Import E:Eq'). Axiom eq_refl : forall x : t, x==x. Axiom eq_sym : forall x y : t, x==y -> y==x. Axiom eq_trans : forall x y z : t, x==y -> y==z -> x==z. + #[global] Hint Immediate eq_sym : core. + #[global] Hint Resolve eq_refl eq_trans : core. End IsEqOrig. diff --git a/theories/Structures/EqualitiesFacts.v b/theories/Structures/EqualitiesFacts.v index fe9794de8a..523240065d 100644 --- a/theories/Structures/EqualitiesFacts.v +++ b/theories/Structures/EqualitiesFacts.v @@ -22,6 +22,7 @@ Module KeyDecidableType(D:DecidableType). Definition eqk {elt} : relation (key*elt) := D.eq @@1. Definition eqke {elt} : relation (key*elt) := D.eq * Logic.eq. + #[global] Hint Unfold eqk eqke : core. (** eqk, eqke are equalities *) @@ -60,6 +61,7 @@ Module KeyDecidableType(D:DecidableType). Lemma eqk_1 {elt} k k' (e e':elt) : eqk (k,e) (k',e') -> D.eq k k'. Proof. trivial. Qed. + #[global] Hint Resolve eqke_1 eqke_2 eqk_1 : core. (* Additional facts *) @@ -69,6 +71,7 @@ Module KeyDecidableType(D:DecidableType). Proof. induction 1; firstorder. Qed. + #[global] Hint Resolve InA_eqke_eqk : core. Lemma InA_eqk_eqke {elt} p (m:list (key*elt)) : @@ -86,6 +89,7 @@ Module KeyDecidableType(D:DecidableType). Definition MapsTo {elt} (k:key)(e:elt):= InA eqke (k,e). Definition In {elt} k m := exists e:elt, MapsTo k e m. + #[global] Hint Unfold MapsTo In : core. (* Alternative formulations for [In k l] *) @@ -167,8 +171,11 @@ Module KeyDecidableType(D:DecidableType). eauto with *. Qed. + #[global] Hint Extern 2 (eqke ?a ?b) => split : core. + #[global] Hint Resolve InA_eqke_eqk : core. + #[global] Hint Resolve In_inv_2 In_inv_3 : core. End KeyDecidableType. diff --git a/theories/Structures/OrderedType.v b/theories/Structures/OrderedType.v index ecf0706a4f..dc7a48cd6b 100644 --- a/theories/Structures/OrderedType.v +++ b/theories/Structures/OrderedType.v @@ -44,7 +44,9 @@ Module Type MiniOrderedType. Parameter compare : forall x y : t, Compare lt eq x y. + #[global] Hint Immediate eq_sym : ordered_type. + #[global] Hint Resolve eq_refl eq_trans lt_not_eq lt_trans : ordered_type. End MiniOrderedType. @@ -144,8 +146,11 @@ Module OrderedTypeFacts (Import O: OrderedType). Lemma eq_not_gt x y : eq x y -> ~ lt y x. Proof. order. Qed. Lemma lt_not_gt x y : lt x y -> ~ lt y x. Proof. order. Qed. + #[global] Hint Resolve gt_not_eq eq_not_lt : ordered_type. + #[global] Hint Immediate eq_lt lt_eq le_eq eq_le neq_eq eq_neq : ordered_type. + #[global] Hint Resolve eq_not_gt lt_antirefl lt_not_gt : ordered_type. Lemma elim_compare_eq : @@ -248,7 +253,9 @@ Proof. exact (SortA_NoDupA eq_equiv lt_strorder lt_compat). Qed. End ForNotations. +#[global] Hint Resolve ListIn_In Sort_NoDup Inf_lt : ordered_type. +#[global] Hint Immediate In_eq Inf_lt : ordered_type. End OrderedTypeFacts. @@ -267,7 +274,9 @@ Module KeyOrderedType(O:OrderedType). eq (fst p) (fst p') /\ (snd p) = (snd p'). Definition ltk (p p':key*elt) := lt (fst p) (fst p'). + #[local] Hint Unfold eqk eqke ltk : ordered_type. + #[local] Hint Extern 2 (eqke ?a ?b) => split : ordered_type. (* eqke is stricter than eqk *) @@ -284,6 +293,7 @@ Module KeyOrderedType(O:OrderedType). Lemma ltk_right_l : forall x k e e', ltk (k,e) x -> ltk (k,e') x. Proof. auto. Qed. + #[local] Hint Immediate ltk_right_r ltk_right_l : ordered_type. (* eqk, eqke are equalities, ltk is a strict order *) @@ -320,8 +330,11 @@ Module KeyOrderedType(O:OrderedType). exact (lt_not_eq H H1). Qed. + #[local] Hint Resolve eqk_trans eqke_trans eqk_refl eqke_refl : ordered_type. + #[local] Hint Resolve ltk_trans ltk_not_eqk ltk_not_eqke : ordered_type. + #[local] Hint Immediate eqk_sym eqke_sym : ordered_type. Global Instance eqk_equiv : Equivalence eqk. @@ -360,7 +373,9 @@ Module KeyOrderedType(O:OrderedType). intros (k,e) (k',e') (k'',e''). unfold ltk, eqk; simpl; eauto with ordered_type. Qed. + #[local] Hint Resolve eqk_not_ltk : ordered_type. + #[local] Hint Immediate ltk_eqk eqk_ltk : ordered_type. Lemma InA_eqke_eqk : @@ -368,6 +383,7 @@ Module KeyOrderedType(O:OrderedType). Proof. unfold eqke; induction 1; intuition. Qed. + #[local] Hint Resolve InA_eqke_eqk : ordered_type. Definition MapsTo (k:key)(e:elt):= InA eqke (k,e). @@ -375,6 +391,7 @@ Module KeyOrderedType(O:OrderedType). Notation Sort := (sort ltk). Notation Inf := (lelistA ltk). + #[local] Hint Unfold MapsTo In : ordered_type. (* An alternative formulation for [In k l] is [exists e, InA eqk (k,e) l] *) @@ -406,7 +423,9 @@ Module KeyOrderedType(O:OrderedType). Lemma Inf_lt : forall l x x', ltk x x' -> Inf x' l -> Inf x l. Proof. exact (InfA_ltA ltk_strorder). Qed. + #[local] Hint Immediate Inf_eq : ordered_type. + #[local] Hint Resolve Inf_lt : ordered_type. Lemma Sort_Inf_In : @@ -470,18 +489,31 @@ Module KeyOrderedType(O:OrderedType). End Elt. + #[global] Hint Unfold eqk eqke ltk : ordered_type. + #[global] Hint Extern 2 (eqke ?a ?b) => split : ordered_type. + #[global] Hint Resolve eqk_trans eqke_trans eqk_refl eqke_refl : ordered_type. + #[global] Hint Resolve ltk_trans ltk_not_eqk ltk_not_eqke : ordered_type. + #[global] Hint Immediate eqk_sym eqke_sym : ordered_type. + #[global] Hint Resolve eqk_not_ltk : ordered_type. + #[global] Hint Immediate ltk_eqk eqk_ltk : ordered_type. + #[global] Hint Resolve InA_eqke_eqk : ordered_type. + #[global] Hint Unfold MapsTo In : ordered_type. + #[global] Hint Immediate Inf_eq : ordered_type. + #[global] Hint Resolve Inf_lt : ordered_type. + #[global] Hint Resolve Sort_Inf_NotIn : ordered_type. + #[global] Hint Resolve In_inv_2 In_inv_3 : ordered_type. End KeyOrderedType. diff --git a/theories/Structures/Orders.v b/theories/Structures/Orders.v index b3e3b6e853..b4ddd0b262 100644 --- a/theories/Structures/Orders.v +++ b/theories/Structures/Orders.v @@ -181,6 +181,7 @@ Module OTF_to_TotalOrder (O:OrderedTypeFull) <: TotalOrder we coerce [bool] into [Prop]. *) Local Coercion is_true : bool >-> Sortclass. +#[global] Hint Unfold is_true : core. Module Type HasLeb (Import T:Typ). diff --git a/theories/Structures/OrdersLists.v b/theories/Structures/OrdersLists.v index 3a5dbc2f88..bace70cbee 100644 --- a/theories/Structures/OrdersLists.v +++ b/theories/Structures/OrdersLists.v @@ -50,7 +50,9 @@ Proof. exact (InfA_alt O.eq_equiv O.lt_strorder O.lt_compat). Qed. Lemma Sort_NoDup : forall l, Sort l -> NoDup l. Proof. exact (SortA_NoDupA O.eq_equiv O.lt_strorder O.lt_compat) . Qed. +#[global] Hint Resolve ListIn_In Sort_NoDup Inf_lt : core. +#[global] Hint Immediate In_eq Inf_lt : core. End OrderedTypeLists. @@ -66,6 +68,7 @@ Module KeyOrderedType(O:OrderedType). Definition ltk {elt} : relation (key*elt) := O.lt @@1. + #[global] Hint Unfold ltk : core. (* ltk is a strict order *) @@ -109,7 +112,9 @@ Module KeyOrderedType(O:OrderedType). Lemma Inf_lt l x x' : ltk x x' -> Inf x' l -> Inf x l. Proof. apply InfA_ltA; auto with *. Qed. + #[local] Hint Immediate Inf_eq : core. + #[local] Hint Resolve Inf_lt : core. Lemma Sort_Inf_In l p q : Sort l -> Inf q l -> InA eqk p l -> ltk q p. @@ -148,9 +153,13 @@ Module KeyOrderedType(O:OrderedType). End Elt. + #[global] Hint Resolve ltk_not_eqk ltk_not_eqke : core. + #[global] Hint Immediate Inf_eq : core. + #[global] Hint Resolve Inf_lt : core. + #[global] Hint Resolve Sort_Inf_NotIn : core. End KeyOrderedType. diff --git a/theories/Vectors/VectorDef.v b/theories/Vectors/VectorDef.v index a154a2b269..3799ffaca9 100644 --- a/theories/Vectors/VectorDef.v +++ b/theories/Vectors/VectorDef.v @@ -279,27 +279,32 @@ Section SCANNING. Inductive Forall {A} (P: A -> Prop): forall {n} (v: t A n), Prop := |Forall_nil: Forall P [] |Forall_cons {n} x (v: t A n): P x -> Forall P v -> Forall P (x::v). +#[local] Hint Constructors Forall : core. Inductive Exists {A} (P:A->Prop): forall {n}, t A n -> Prop := |Exists_cons_hd {m} x (v: t A m): P x -> Exists P (x::v) |Exists_cons_tl {m} x (v: t A m): Exists P v -> Exists P (x::v). +#[local] Hint Constructors Exists : core. Inductive In {A} (a:A): forall {n}, t A n -> Prop := |In_cons_hd {m} (v: t A m): In a (a::v) |In_cons_tl {m} x (v: t A m): In a v -> In a (x::v). +#[local] Hint Constructors In : core. Inductive Forall2 {A B} (P:A->B->Prop): forall {n}, t A n -> t B n -> Prop := |Forall2_nil: Forall2 P [] [] |Forall2_cons {m} x1 x2 (v1:t A m) v2: P x1 x2 -> Forall2 P v1 v2 -> Forall2 P (x1::v1) (x2::v2). +#[local] Hint Constructors Forall2 : core. Inductive Exists2 {A B} (P:A->B->Prop): forall {n}, t A n -> t B n -> Prop := |Exists2_cons_hd {m} x1 x2 (v1: t A m) (v2: t B m): P x1 x2 -> Exists2 P (x1::v1) (x2::v2) |Exists2_cons_tl {m} x1 x2 (v1:t A m) v2: Exists2 P v1 v2 -> Exists2 P (x1::v1) (x2::v2). +#[local] Hint Constructors Exists2 : core. End SCANNING. diff --git a/theories/Wellfounded/Inclusion.v b/theories/Wellfounded/Inclusion.v index 474836d53d..cafa849b1b 100644 --- a/theories/Wellfounded/Inclusion.v +++ b/theories/Wellfounded/Inclusion.v @@ -22,6 +22,7 @@ Section WfInclusion. apply Acc_intro; auto with sets. Qed. + #[local] Hint Resolve Acc_incl : core. Theorem wf_incl : inclusion A R1 R2 -> well_founded R2 -> well_founded R1. diff --git a/theories/Wellfounded/Transitive_Closure.v b/theories/Wellfounded/Transitive_Closure.v index 2d139504f3..49c2dd8602 100644 --- a/theories/Wellfounded/Transitive_Closure.v +++ b/theories/Wellfounded/Transitive_Closure.v @@ -31,6 +31,7 @@ Section Wf_Transitive_Closure. apply Acc_inv with y; auto with sets. Defined. + #[local] Hint Resolve Acc_clos_trans : core. Lemma Acc_inv_trans : forall x y:A, trans_clos y x -> Acc R x -> Acc R y. diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v index 52998c8b95..47137414dc 100644 --- a/theories/ZArith/BinInt.v +++ b/theories/ZArith/BinInt.v @@ -1754,6 +1754,7 @@ Proof. congruence. Qed. Lemma Zpos_eq_iff : forall p q, p = q <-> Z.pos p = Z.pos q. Proof (fun p q => iff_sym (Pos2Z.inj_iff p q)). +#[global] Hint Immediate Zsucc_pred: zarith. (* Not kept : diff --git a/theories/ZArith/ZArith_base.v b/theories/ZArith/ZArith_base.v index 26cd3e1e4d..cae918b4b6 100644 --- a/theories/ZArith/ZArith_base.v +++ b/theories/ZArith/ZArith_base.v @@ -30,6 +30,7 @@ Require Export Zbool. Require Export Zmisc. Require Export Wf_Z. +#[global] Hint Resolve Z.le_refl Z.add_comm Z.add_assoc Z.mul_comm Z.mul_assoc Z.add_0_l Z.add_0_r Z.mul_1_l Z.add_opp_diag_l Z.add_opp_diag_r Z.mul_add_distr_l Z.mul_add_distr_r: zarith. diff --git a/theories/ZArith/Zdiv.v b/theories/ZArith/Zdiv.v index 2039dc0bee..13adda412d 100644 --- a/theories/ZArith/Zdiv.v +++ b/theories/ZArith/Zdiv.v @@ -75,6 +75,7 @@ Proof. + apply Pos2Z.neg_is_nonpos. Qed. +#[global] Hint Unfold Remainder : core. (** Now comes the fully general result about Euclidean division. *) @@ -203,6 +204,7 @@ Proof. intros a. zero_or_not a. apply Z.mod_1_r. Qed. Lemma Zdiv_1_r: forall a, a/1 = a. Proof. intros a. zero_or_not a. apply Z.div_1_r. Qed. +#[global] Hint Resolve Zmod_0_l Zmod_0_r Zdiv_0_l Zdiv_0_r Zdiv_1_r Zmod_1_r : zarith. diff --git a/theories/ZArith/Zeven.v b/theories/ZArith/Zeven.v index 0448bcf41b..d3a9d7baac 100644 --- a/theories/ZArith/Zeven.v +++ b/theories/ZArith/Zeven.v @@ -130,6 +130,7 @@ Proof. boolify_even_odd. now rewrite Z.odd_pred. Qed. +#[global] Hint Unfold Zeven Zodd: zarith. Notation Zeven_bool_succ := Z.even_succ (only parsing). diff --git a/theories/ZArith/Zhints.v b/theories/ZArith/Zhints.v index 95266186eb..80073bdbdf 100644 --- a/theories/ZArith/Zhints.v +++ b/theories/ZArith/Zhints.v @@ -40,6 +40,7 @@ Require Import Wf_Z. (** No subgoal or smaller subgoals *) +#[global] Hint Resolve (** ** Reversible simplification lemmas (no loss of information) *) (** Should clearly be declared as hints *) diff --git a/theories/ZArith/Znumtheory.v b/theories/ZArith/Znumtheory.v index cad9454906..861c204ab8 100644 --- a/theories/ZArith/Znumtheory.v +++ b/theories/ZArith/Znumtheory.v @@ -65,8 +65,11 @@ Proof. apply Z.divide_abs_l. Qed. Theorem Zdivide_Zabs_inv_l a b : (a | b) -> (Z.abs a | b). Proof. apply Z.divide_abs_l. Qed. +#[global] Hint Resolve Z.divide_refl Z.divide_1_l Z.divide_0_r: zarith. +#[global] Hint Resolve Z.mul_divide_mono_l Z.mul_divide_mono_r: zarith. +#[global] Hint Resolve Z.divide_add_r Zdivide_opp_r Zdivide_opp_r_rev Zdivide_opp_l Zdivide_opp_l_rev Z.divide_sub_r Z.divide_mul_l Z.divide_mul_r Z.divide_factor_l Z.divide_factor_r: zarith. @@ -236,6 +239,7 @@ Proof. intros; apply Zis_gcd_opp; apply Zis_gcd_0; auto. Qed. +#[global] Hint Resolve Zis_gcd_sym Zis_gcd_0 Zis_gcd_minus Zis_gcd_opp: zarith. Theorem Zis_gcd_unique: forall a b c d : Z, @@ -646,6 +650,7 @@ Proof. - absurd (p | a); intuition. Qed. +#[global] Hint Resolve prime_rel_prime: zarith. (** As a consequence, a prime number is relatively prime with smaller numbers *) @@ -866,6 +871,7 @@ Notation Zgcd_Zabs := Z.gcd_abs_l (only parsing). Notation Zgcd_0 := Z.gcd_0_r (only parsing). Notation Zgcd_1 := Z.gcd_1_r (only parsing). +#[global] Hint Resolve Z.gcd_0_r Z.gcd_1_r : zarith. Theorem Zgcd_1_rel_prime : forall a b, diff --git a/theories/ZArith/Zorder.v b/theories/ZArith/Zorder.v index 949a01860f..4c533ac458 100644 --- a/theories/ZArith/Zorder.v +++ b/theories/ZArith/Zorder.v @@ -132,6 +132,7 @@ Register not_Zne as plugins.omega.not_Zne. Notation Zeq_le := Z.eq_le_incl (only parsing). +#[global] Hint Resolve Z.le_refl: zarith. (** Antisymmetry *) @@ -196,6 +197,7 @@ Proof. Z.swap_greater. Z.order. Qed. +#[global] Hint Resolve Z.le_trans: zarith. (** * Compatibility of order and operations on Z *) @@ -219,6 +221,7 @@ Proof. Z.swap_greater. apply Z.succ_lt_mono. Qed. +#[global] Hint Resolve Zsucc_le_compat: zarith. (** Simplification of successor wrt to order *) @@ -302,7 +305,9 @@ Proof. intros. now apply Z.lt_le_incl, Z.le_succ_l. Qed. +#[global] Hint Resolve Z.le_succ_diag_r: zarith. +#[global] Hint Resolve Z.le_le_succ_r: zarith. (** Relating order wrt successor and order wrt predecessor *) @@ -357,6 +362,7 @@ Proof. intros n; induction n; simpl; intros. apply Z.le_refl. easy. Qed. +#[global] Hint Immediate Z.eq_le_incl: zarith. (** Derived lemma *) diff --git a/theories/ZArith/Zpow_facts.v b/theories/ZArith/Zpow_facts.v index c36ddad823..b69af424b1 100644 --- a/theories/ZArith/Zpow_facts.v +++ b/theories/ZArith/Zpow_facts.v @@ -57,6 +57,7 @@ Proof. apply Z.pow_gt_1. Qed. Theorem Zmult_power p q r : 0 <= r -> (p*q)^r = p^r * q^r. Proof. intros. apply Z.pow_mul_l. Qed. +#[global] Hint Resolve Z.pow_nonneg Z.pow_pos_nonneg : zarith. Theorem Zpower_le_monotone3 a b c : diff --git a/theories/ZArith/Zpower.v b/theories/ZArith/Zpower.v index ae12295ca4..6f464d89bb 100644 --- a/theories/ZArith/Zpower.v +++ b/theories/ZArith/Zpower.v @@ -79,7 +79,9 @@ Proof. now apply (Z.pow_add_r z (Zpos n) (Zpos m)). Qed. +#[global] Hint Immediate Zpower_nat_is_exp Zpower_pos_is_exp : zarith. +#[global] Hint Unfold Z.pow_pos Zpower_nat: zarith. Theorem Zpower_exp x n m : @@ -226,7 +228,9 @@ Section Powers_of_2. End Powers_of_2. +#[global] Hint Resolve two_p_gt_ZERO: zarith. +#[global] Hint Immediate two_p_pred two_p_S: zarith. Section power_div_with_rest. diff --git a/theories/ZArith/Zquot.v b/theories/ZArith/Zquot.v index f95831436a..943376ecfd 100644 --- a/theories/ZArith/Zquot.v +++ b/theories/ZArith/Zquot.v @@ -57,6 +57,7 @@ Proof. now destruct a. Qed. Lemma Zquot_0_l a : 0÷a = 0. Proof. now destruct a. Qed. +#[global] Hint Resolve Zrem_0_l Zrem_0_r Zquot_0_l Zquot_0_r Z.quot_1_r Z.rem_1_r : zarith. diff --git a/theories/ZArith/Zwf.v b/theories/ZArith/Zwf.v index 2ff6805c78..81d2a2d70d 100644 --- a/theories/ZArith/Zwf.v +++ b/theories/ZArith/Zwf.v @@ -57,6 +57,7 @@ Section wf_proof. End wf_proof. +#[global] Hint Resolve Zwf_well_founded: datatypes. @@ -87,4 +88,5 @@ Section wf_proof_up. End wf_proof_up. +#[global] Hint Resolve Zwf_up_well_founded: datatypes. diff --git a/theories/btauto/Algebra.v b/theories/btauto/Algebra.v index 4a603f2c52..08bb49a449 100644 --- a/theories/btauto/Algebra.v +++ b/theories/btauto/Algebra.v @@ -10,6 +10,7 @@ end. Arguments decide P /H. +#[global] Hint Extern 5 => progress bool : core. Ltac define t x H := @@ -147,6 +148,7 @@ Qed. (** * The core reflexive part. *) +#[local] Hint Constructors valid : core. Fixpoint beq_poly pl pr := @@ -315,6 +317,7 @@ Section Validity. (* Decision procedure of validity *) +#[local] Hint Constructors valid linear : core. Lemma valid_le_compat : forall k l p, valid k p -> (k <= l)%positive -> valid l p. @@ -414,6 +417,7 @@ intros pl; induction pl; intros pr var; simpl. rewrite poly_add_compat, poly_mul_mon_compat, IHpl1, IHpl2; ring. Qed. +#[local] Hint Extern 5 => match goal with | [ |- (Pos.max ?x ?y <= ?z)%positive ] => @@ -426,8 +430,10 @@ match goal with apply Pos.max_case_strong; intros; lia | _ => lia end : core. +#[local] Hint Resolve Pos.le_max_r Pos.le_max_l : core. +#[local] Hint Constructors valid linear : core. (* Compatibility of validity w.r.t algebraic operations *) diff --git a/theories/btauto/Reflect.v b/theories/btauto/Reflect.v index 867fe69550..a653b94d1c 100644 --- a/theories/btauto/Reflect.v +++ b/theories/btauto/Reflect.v @@ -77,9 +77,11 @@ intros var f; induction f; simpl poly_of_formula; simpl formula_eval; auto. end. Qed. +#[local] Hint Extern 5 => change 0 with (min 0 0) : core. Local Hint Resolve poly_add_valid_compat poly_mul_valid_compat : core. Local Hint Constructors valid : core. +#[local] Hint Extern 5 => lia : core. (* Compatibility with validity *) diff --git a/theories/micromega/Tauto.v b/theories/micromega/Tauto.v index 99af214396..ce12b02359 100644 --- a/theories/micromega/Tauto.v +++ b/theories/micromega/Tauto.v @@ -1562,6 +1562,7 @@ Section S. auto. Qed. + #[local] Hint Resolve no_middle_eval_tt : tauto. Lemma or_clause_correct : forall cl cl' env, eval_opt_clause env (or_clause cl cl') <-> eval_clause env cl \/ eval_clause env cl'. @@ -1702,6 +1703,7 @@ Section S. intros k; destruct k ; simpl; auto. Qed. + #[local] Hint Resolve hold_eTT : tauto. Lemma hold_eFF : forall k, @@ -1710,6 +1712,7 @@ Section S. intros k; destruct k ; simpl;auto. Qed. + #[local] Hint Resolve hold_eFF : tauto. Lemma hold_eAND : forall k r1 r2, diff --git a/theories/micromega/ZArith_hints.v b/theories/micromega/ZArith_hints.v index a6d3d92a99..3545e8b218 100644 --- a/theories/micromega/ZArith_hints.v +++ b/theories/micromega/ZArith_hints.v @@ -10,34 +10,56 @@ Require Import Lia. Import ZArith_base. +#[global] Hint Resolve Z.le_refl Z.add_comm Z.add_assoc Z.mul_comm Z.mul_assoc Z.add_0_l Z.add_0_r Z.mul_1_l Z.add_opp_diag_l Z.add_opp_diag_r Z.mul_add_distr_r Z.mul_add_distr_l: zarith. Require Export Zhints. +#[global] Hint Extern 10 (_ = _ :>nat) => abstract lia: zarith. +#[global] Hint Extern 10 (_ <= _) => abstract lia: zarith. +#[global] Hint Extern 10 (_ < _) => abstract lia: zarith. +#[global] Hint Extern 10 (_ >= _) => abstract lia: zarith. +#[global] Hint Extern 10 (_ > _) => abstract lia: zarith. +#[global] Hint Extern 10 (_ <> _ :>nat) => abstract lia: zarith. +#[global] Hint Extern 10 (~ _ <= _) => abstract lia: zarith. +#[global] Hint Extern 10 (~ _ < _) => abstract lia: zarith. +#[global] Hint Extern 10 (~ _ >= _) => abstract lia: zarith. +#[global] Hint Extern 10 (~ _ > _) => abstract lia: zarith. +#[global] Hint Extern 10 (_ = _ :>Z) => abstract lia: zarith. +#[global] Hint Extern 10 (_ <= _)%Z => abstract lia: zarith. +#[global] Hint Extern 10 (_ < _)%Z => abstract lia: zarith. +#[global] Hint Extern 10 (_ >= _)%Z => abstract lia: zarith. +#[global] Hint Extern 10 (_ > _)%Z => abstract lia: zarith. +#[global] Hint Extern 10 (_ <> _ :>Z) => abstract lia: zarith. +#[global] Hint Extern 10 (~ (_ <= _)%Z) => abstract lia: zarith. +#[global] Hint Extern 10 (~ (_ < _)%Z) => abstract lia: zarith. +#[global] Hint Extern 10 (~ (_ >= _)%Z) => abstract lia: zarith. +#[global] Hint Extern 10 (~ (_ > _)%Z) => abstract lia: zarith. +#[global] Hint Extern 10 False => abstract lia: zarith. diff --git a/theories/nsatz/Nsatz.v b/theories/nsatz/Nsatz.v index b684775bb4..21f0f30140 100644 --- a/theories/nsatz/Nsatz.v +++ b/theories/nsatz/Nsatz.v @@ -60,6 +60,7 @@ exact Rplus_opp_r. Defined. Class can_compute_Z (z : Z) := dummy_can_compute_Z : True. +#[global] Hint Extern 0 (can_compute_Z ?v) => match isZcst v with true => exact I end : typeclass_instances. Instance reify_IZR z lvar {_ : can_compute_Z z} : reify (PEc z) lvar (IZR z). diff --git a/theories/ssr/ssrbool.v b/theories/ssr/ssrbool.v index e8a036bbb0..b205965ed1 100644 --- a/theories/ssr/ssrbool.v +++ b/theories/ssr/ssrbool.v @@ -487,6 +487,7 @@ Ltac prop_congr := apply: prop_congr. Lemma is_true_true : true. Proof. by []. Qed. Lemma not_false_is_true : ~ false. Proof. by []. Qed. Lemma is_true_locked_true : locked true. Proof. by unlock. Qed. +#[global] Hint Resolve is_true_true not_false_is_true is_true_locked_true : core. (** Shorter names. **) diff --git a/theories/ssr/ssreflect.v b/theories/ssr/ssreflect.v index 175cae8415..d0508bef2e 100644 --- a/theories/ssr/ssreflect.v +++ b/theories/ssr/ssreflect.v @@ -543,8 +543,10 @@ Proof. by move=> /(_ P); apply. Qed. Require Export ssrunder. +#[global] Hint Extern 0 (@Under_rel.Over_rel _ _ _ _) => solve [ apply: Under_rel.over_rel_done ] : core. +#[global] Hint Resolve Under_rel.over_rel_done : core. Register Under_rel.Under_rel as plugins.ssreflect.Under_rel. diff --git a/theories/ssr/ssrfun.v b/theories/ssr/ssrfun.v index 053e86dc34..e1442e1da2 100644 --- a/theories/ssr/ssrfun.v +++ b/theories/ssr/ssrfun.v @@ -450,6 +450,7 @@ End ExtensionalEquality. Typeclasses Opaque eqfun. Typeclasses Opaque eqrel. +#[global] Hint Resolve frefl rrefl : core. Notation "f1 =1 f2" := (eqfun f1 f2) : fun_scope. |