Verified Commit 4d6d497a authored by Tej Chajed's avatar Tej Chajed

Explicitly use core hint database

Adding a hint without a database now triggers a deprecation warning in
Coq master (https://github.com/coq/coq/pull/8987).
parent f5e00ce3
......@@ -20,7 +20,7 @@ Notation "(⋅)" := op (only parsing) : stdpp_scope.
Definition included `{Equiv A, Op A} (x y : A) := z, y x z.
Infix "≼" := included (at level 70) : stdpp_scope.
Notation "(≼)" := included (only parsing) : stdpp_scope.
Hint Extern 0 (_ _) => reflexivity.
Hint Extern 0 (_ _) => reflexivity : core.
Instance: Params (@included) 3.
Class ValidN (A : Type) := validN : nat A Prop.
......@@ -38,7 +38,7 @@ Definition includedN `{Dist A, Op A} (n : nat) (x y : A) := ∃ z, y ≡{n}≡ x
Notation "x ≼{ n } y" := (includedN n x y)
(at level 70, n at next level, format "x ≼{ n } y") : stdpp_scope.
Instance: Params (@includedN) 4.
Hint Extern 0 (_ {_} _) => reflexivity.
Hint Extern 0 (_ {_} _) => reflexivity : core.
Section mixin.
Local Set Primitive Projections.
......@@ -644,7 +644,7 @@ Section ucmra.
Global Instance cmra_monoid : Monoid (@op A _) := {| monoid_unit := ε |}.
End ucmra.
Hint Immediate cmra_unit_cmra_total.
Hint Immediate cmra_unit_cmra_total : core.
(** * Properties about CMRAs with Leibniz equality *)
Section cmra_leibniz.
......
......@@ -140,11 +140,11 @@ Proof.
intros; symmetry; rewrite dra_comm; eauto using dra_disjoint_rl.
apply dra_disjoint_move_l; auto; by rewrite dra_comm.
Qed.
Hint Immediate dra_disjoint_move_l dra_disjoint_move_r.
Hint Immediate dra_disjoint_move_l dra_disjoint_move_r : core.
Lemma validity_valid_car_valid z : z validity_car z.
Proof. apply validity_prf. Qed.
Hint Resolve validity_valid_car_valid.
Hint Resolve validity_valid_car_valid : core.
Program Instance validity_pcore : PCore (validity A) := λ x,
Some (Validity (core (validity_car x)) ( x) _).
Solve Obligations with naive_solver eauto using dra_core_valid.
......
......@@ -16,8 +16,8 @@ Class Dist A := dist : nat → relation A.
Instance: Params (@dist) 3.
Notation "x ≡{ n }≡ y" := (dist n x y)
(at level 70, n at next level, format "x ≡{ n }≡ y").
Hint Extern 0 (_ {_} _) => reflexivity.
Hint Extern 0 (_ {_} _) => symmetry; assumption.
Hint Extern 0 (_ {_} _) => reflexivity : core.
Hint Extern 0 (_ {_} _) => symmetry; assumption : core.
Notation NonExpansive f := ( n, Proper (dist n ==> dist n) f).
Notation NonExpansive2 f := ( n, Proper (dist n ==> dist n ==> dist n) f).
......@@ -93,7 +93,7 @@ Section ofe_mixin.
Proof. apply (mixin_dist_S _ (ofe_mixin A)). Qed.
End ofe_mixin.
Hint Extern 1 (_ {_} _) => apply equiv_dist; assumption.
Hint Extern 1 (_ {_} _) => apply equiv_dist; assumption : core.
(** Discrete OFEs and discrete OFE elements *)
Class Discrete {A : ofeT} (x : A) := discrete y : x {0} y x y.
......
......@@ -48,7 +48,7 @@ Definition up_set (S : states sts) (T : tokens sts) : states sts :=
S = λ s, up s T.
(** Tactic setup *)
Hint Resolve Step.
Hint Resolve Step : core.
Hint Extern 50 (equiv (A:=set _) _ _) => set_solver : sts.
Hint Extern 50 (¬equiv (A:=set _) _ _) => set_solver : sts.
Hint Extern 50 (_ _) => set_solver : sts.
......
......@@ -148,7 +148,7 @@ Global Instance uPred_affine M : BiAffine (uPredI M) | 0.
Proof. intros P. exact: pure_intro. Qed.
(* Also add this to the global hint database, otherwise [eauto] won't work for
many lemmas that have [BiAffine] as a premise. *)
Hint Immediate uPred_affine.
Hint Immediate uPred_affine : core.
Global Instance uPred_plainly_exist_1 M : BiPlainlyExist (uPredSI M).
Proof. exact: @plainly_exist_1. Qed.
......
......@@ -3,9 +3,9 @@ From iris.bi Require Import notation.
From stdpp Require Import finite.
From Coq.Init Require Import Nat.
Set Default Proof Using "Type".
Local Hint Extern 1 (_ _) => etrans; [eassumption|].
Local Hint Extern 1 (_ _) => etrans; [|eassumption].
Local Hint Extern 10 (_ _) => lia.
Local Hint Extern 1 (_ _) => etrans; [eassumption|] : core.
Local Hint Extern 1 (_ _) => etrans; [|eassumption] : core.
Local Hint Extern 10 (_ _) => lia : core.
(** The basic definition of the uPred type, its metric and functor laws.
You probably do not want to import this file. Instead, import
......@@ -358,7 +358,7 @@ Implicit Types φ : Prop.
Implicit Types P Q : uPred M.
Implicit Types A : Type.
Arguments uPred_holds {_} !_ _ _ /.
Hint Immediate uPred_in_entails.
Hint Immediate uPred_in_entails : core.
Notation "P ⊢ Q" := (@uPred_entails M P%I Q%I) : stdpp_scope.
Notation "(⊢)" := (@uPred_entails M) (only parsing) : stdpp_scope.
......
......@@ -17,7 +17,7 @@ Implicit Types P Q R : PROP.
Implicit Types Ps : list PROP.
Implicit Types A : Type.
Hint Extern 100 (NonExpansive _) => solve_proper.
Hint Extern 100 (NonExpansive _) => solve_proper : core.
(* Force implicit argument PROP *)
Notation "P ⊢ Q" := (P @{PROP} Q).
......@@ -91,9 +91,9 @@ Proof. intros ->; apply exist_intro. Qed.
Lemma forall_elim' {A} P (Ψ : A PROP) : (P a, Ψ a) a, P Ψ a.
Proof. move=> HP a. by rewrite HP forall_elim. Qed.
Hint Resolve pure_intro forall_intro.
Hint Resolve or_elim or_intro_l' or_intro_r'.
Hint Resolve and_intro and_elim_l' and_elim_r'.
Hint Resolve pure_intro forall_intro : core.
Hint Resolve or_elim or_intro_l' or_intro_r' : core.
Hint Resolve and_intro and_elim_l' and_elim_r' : core.
Lemma impl_intro_l P Q R : (Q P R) P Q R.
Proof. intros HR; apply impl_intro_r; rewrite -HR; auto. Qed.
......@@ -110,7 +110,7 @@ Lemma False_elim P : False ⊢ P.
Proof. by apply (pure_elim' False). Qed.
Lemma True_intro P : P True.
Proof. by apply pure_intro. Qed.
Hint Immediate False_elim.
Hint Immediate False_elim : core.
Lemma entails_eq_True P Q : (P Q) ((P Q)%I True%I).
Proof.
......@@ -303,7 +303,7 @@ Proof. rewrite /bi_iff; apply and_intro; apply impl_intro_l; auto. Qed.
(* BI Stuff *)
Hint Resolve sep_mono.
Hint Resolve sep_mono : core.
Lemma sep_mono_l P P' Q : (P Q) P P' Q P'.
Proof. by intros; apply sep_mono. Qed.
Lemma sep_mono_r P P' Q' : (P' Q') P P' P Q'.
......@@ -758,7 +758,7 @@ Section bi_affine.
End bi_affine.
(* Properties of the persistence modality *)
Hint Resolve persistently_mono.
Hint Resolve persistently_mono : core.
Global Instance persistently_mono' : Proper (() ==> ()) (@bi_persistently PROP).
Proof. intros P Q; apply persistently_mono. Qed.
Global Instance persistently_flip_mono' :
......
......@@ -15,8 +15,8 @@ Implicit Types A : Type.
Notation "P ⊢ Q" := (P @{PROP} Q).
Notation "P ⊣⊢ Q" := (P @{PROP} Q).
Hint Resolve or_elim or_intro_l' or_intro_r' True_intro False_elim.
Hint Resolve and_elim_l' and_elim_r' and_intro forall_intro.
Hint Resolve or_elim or_intro_l' or_intro_r' True_intro False_elim : core.
Hint Resolve and_elim_l' and_elim_r' and_intro forall_intro : core.
Global Instance internal_eq_proper (A : ofeT) :
Proper (() ==> () ==> ()) (@sbi_internal_eq PROP A) := ne_proper_2 _.
......@@ -24,8 +24,8 @@ Global Instance later_proper :
Proper (() ==> ()) (@sbi_later PROP) := ne_proper _.
(* Equality *)
Hint Resolve internal_eq_refl.
Hint Extern 100 (NonExpansive _) => solve_proper.
Hint Resolve internal_eq_refl : core.
Hint Extern 100 (NonExpansive _) => solve_proper : core.
Lemma equiv_internal_eq {A : ofeT} P (a b : A) : a b P a b.
Proof. intros ->. auto. Qed.
......@@ -150,7 +150,7 @@ Lemma later_equivI {A : ofeT} (x y : A) : Next x ≡ Next y ⊣⊢ ▷ (x ≡ y)
Proof. apply (anti_symm _); auto using later_eq_1, later_eq_2. Qed.
(* Later derived *)
Hint Resolve later_mono.
Hint Resolve later_mono : core.
Global Instance later_mono' : Proper (() ==> ()) (@sbi_later PROP).
Proof. intros P Q; apply later_mono. Qed.
Global Instance later_flip_mono' :
......
......@@ -255,7 +255,7 @@ Arguments sbi_persistently {PROP} _%I : simpl never, rename.
Arguments sbi_internal_eq {PROP _} _ _ : simpl never, rename.
Arguments sbi_later {PROP} _%I : simpl never, rename.
Hint Extern 0 (bi_entails _ _) => reflexivity.
Hint Extern 0 (bi_entails _ _) => reflexivity : core.
Instance bi_rewrite_relation (PROP : bi) : RewriteRelation (@bi_entails PROP).
Instance bi_inhabited {PROP : bi} : Inhabited PROP := populate (bi_pure True).
......
......@@ -119,7 +119,7 @@ Implicit Types P Q : monPred.
Inductive monPred_entails (P1 P2 : monPred) : Prop :=
{ monPred_in_entails i : P1 i P2 i }.
Hint Immediate monPred_in_entails.
Hint Immediate monPred_in_entails : core.
Program Definition monPred_upclosed (Φ : I PROP) : monPred :=
MonPred (λ i, ( j, i j Φ j)%I) _.
......
......@@ -102,9 +102,9 @@ Section plainly_derived.
Context `{BiPlainly PROP}.
Implicit Types P : PROP.
Hint Resolve pure_intro forall_intro.
Hint Resolve or_elim or_intro_l' or_intro_r'.
Hint Resolve and_intro and_elim_l' and_elim_r'.
Hint Resolve pure_intro forall_intro : core.
Hint Resolve or_elim or_intro_l' or_intro_r' : core.
Hint Resolve and_intro and_elim_l' and_elim_r' : core.
Global Instance plainly_proper :
Proper (() ==> ()) (@plainly PROP _) := ne_proper _.
......
......@@ -45,16 +45,16 @@ Ltac inv_head_step :=
inversion H; subst; clear H
end.
Local Hint Extern 0 (head_reducible _ _) => eexists _, _, _, _; simpl.
Local Hint Extern 0 (head_reducible_no_obs _ _) => eexists _, _, _; simpl.
Local Hint Extern 0 (head_reducible _ _) => eexists _, _, _, _; simpl : core.
Local Hint Extern 0 (head_reducible_no_obs _ _) => eexists _, _, _; simpl : core.
(* [simpl apply] is too stupid, so we need extern hints here. *)
Local Hint Extern 1 (head_step _ _ _ _ _ _) => econstructor.
Local Hint Extern 0 (head_step (CAS _ _ _) _ _ _ _ _) => eapply CasSucS.
Local Hint Extern 0 (head_step (CAS _ _ _) _ _ _ _ _) => eapply CasFailS.
Local Hint Extern 0 (head_step (Alloc _) _ _ _ _ _) => apply alloc_fresh.
Local Hint Extern 0 (head_step NewProph _ _ _ _ _) => apply new_proph_id_fresh.
Local Hint Resolve to_of_val.
Local Hint Extern 1 (head_step _ _ _ _ _ _) => econstructor : core.
Local Hint Extern 0 (head_step (CAS _ _ _) _ _ _ _ _) => eapply CasSucS : core.
Local Hint Extern 0 (head_step (CAS _ _ _) _ _ _ _ _) => eapply CasFailS : core.
Local Hint Extern 0 (head_step (Alloc _) _ _ _ _ _) => apply alloc_fresh : core.
Local Hint Extern 0 (head_step NewProph _ _ _ _ _) => apply new_proph_id_fresh : core.
Local Hint Resolve to_of_val : core.
Instance into_val_val v : IntoVal (Val v) v.
Proof. done. Qed.
......
......@@ -10,9 +10,9 @@ Implicit Types P : iProp Σ.
Implicit Types Φ : val Λ iProp Σ.
Implicit Types v : val Λ.
Implicit Types e : expr Λ.
Hint Resolve head_prim_reducible head_reducible_prim_step.
Hint Resolve (reducible_not_val _ inhabitant).
Hint Resolve head_stuck_stuck.
Hint Resolve head_prim_reducible head_reducible_prim_step : core.
Hint Resolve (reducible_not_val _ inhabitant) : core.
Hint Resolve head_stuck_stuck : core.
Lemma wp_lift_head_step_fupd {s E Φ} e1 :
to_val e1 = None
......
......@@ -103,7 +103,7 @@ Section language.
ρ2 = (t1 ++ e2 :: t2 ++ efs, σ2)
prim_step e1 σ1 κ e2 σ2 efs
step ρ1 κ ρ2.
Hint Constructors step.
Hint Constructors step : core.
Inductive nsteps : nat cfg Λ list (observation Λ) cfg Λ Prop :=
| nsteps_refl ρ :
......@@ -112,7 +112,7 @@ Section language.
step ρ1 κ ρ2
nsteps n ρ2 κs ρ3
nsteps (S n) ρ1 (κ ++ κs) ρ3.
Hint Constructors nsteps.
Hint Constructors nsteps : core.
Definition erased_step (ρ1 ρ2 : cfg Λ) := κ, step ρ1 κ ρ2.
......
......@@ -11,7 +11,7 @@ Implicit Types σ : state Λ.
Implicit Types P Q : iProp Σ.
Implicit Types Φ : val Λ iProp Σ.
Hint Resolve reducible_no_obs_reducible.
Hint Resolve reducible_no_obs_reducible : core.
Lemma wp_lift_step_fupd s E Φ e1 :
to_val e1 = None
......
......@@ -199,9 +199,9 @@ Section ectx_lifting.
Implicit Types s : stuckness.
Implicit Types Φ : val Λ iProp Σ.
Implicit Types e : expr Λ.
Hint Resolve head_prim_reducible head_reducible_prim_step.
Hint Resolve (reducible_not_val _ inhabitant).
Hint Resolve head_stuck_stuck.
Hint Resolve head_prim_reducible head_reducible_prim_step : core.
Hint Resolve (reducible_not_val _ inhabitant) : core.
Hint Resolve head_stuck_stuck : core.
Lemma ownP_lift_head_step s E Φ e1 :
(|={E,}=> σ1, head_reducible e1 σ1 (ownP σ1)
......
......@@ -11,7 +11,7 @@ Implicit Types Φ : val Λ → iProp Σ.
Implicit Types v : val Λ.
Implicit Types e : expr Λ.
Hint Resolve head_prim_reducible_no_obs head_reducible_prim_step
head_reducible_no_obs_reducible.
head_reducible_no_obs_reducible : core.
Lemma twp_lift_head_step {s E Φ} e1 :
to_val e1 = None
......
......@@ -11,7 +11,7 @@ Implicit Types σ : state Λ.
Implicit Types P Q : iProp Σ.
Implicit Types Φ : val Λ iProp Σ.
Hint Resolve reducible_no_obs_reducible.
Hint Resolve reducible_no_obs_reducible : core.
Lemma twp_lift_step s E Φ e1 :
to_val e1 = None
......
......@@ -92,7 +92,7 @@ Context {A : Type}.
Implicit Types Γ : env A.
Implicit Types i : ident.
Implicit Types x : A.
Hint Resolve Esnoc_wf Enil_wf.
Hint Resolve Esnoc_wf Enil_wf : core.
Ltac simplify :=
repeat match goal with
......
......@@ -2263,50 +2263,50 @@ Tactic Notation "iAccu" :=
iStartProof; eapply tac_accu; [pm_reflexivity || fail "iAccu: not an evar"].
(** Automation *)
Hint Extern 0 (_ _) => iStartProof.
Hint Extern 0 (_ _) => iStartProof : core.
(* Make sure that by and done solve trivial things in proof mode *)
Hint Extern 0 (envs_entails _ _) => iPureIntro; try done.
Hint Extern 0 (envs_entails _ _) => iPureIntro; try done : core.
Hint Extern 0 (envs_entails _ ?Q) =>
first [is_evar Q; fail 1|iAssumption].
Hint Extern 0 (envs_entails _ emp) => iEmpIntro.
first [is_evar Q; fail 1|iAssumption] : core.
Hint Extern 0 (envs_entails _ emp) => iEmpIntro : core.
(* TODO: look for a more principled way of adding trivial hints like those
below; see the discussion in !75 for further details. *)
Hint Extern 0 (envs_entails _ (_ _)) =>
rewrite envs_entails_eq; apply bi.internal_eq_refl.
rewrite envs_entails_eq; apply bi.internal_eq_refl : core.
Hint Extern 0 (envs_entails _ (big_opL _ _ _)) =>
rewrite envs_entails_eq; apply big_sepL_nil'.
rewrite envs_entails_eq; apply big_sepL_nil' : core.
Hint Extern 0 (envs_entails _ (big_sepL2 _ _ _)) =>
rewrite envs_entails_eq; apply big_sepL2_nil'.
rewrite envs_entails_eq; apply big_sepL2_nil' : core.
Hint Extern 0 (envs_entails _ (big_opM _ _ _)) =>
rewrite envs_entails_eq; apply big_sepM_empty'.
rewrite envs_entails_eq; apply big_sepM_empty' : core.
Hint Extern 0 (envs_entails _ (big_opS _ _ _)) =>
rewrite envs_entails_eq; apply big_sepS_empty'.
rewrite envs_entails_eq; apply big_sepS_empty' : core.
Hint Extern 0 (envs_entails _ (big_opMS _ _ _)) =>
rewrite envs_entails_eq; apply big_sepMS_empty'.
rewrite envs_entails_eq; apply big_sepMS_empty' : core.
(* These introduce as much as possible at once, for better performance. *)
Hint Extern 0 (envs_entails _ ( _, _)) => iIntros.
Hint Extern 0 (envs_entails _ (_ _)) => iIntros.
Hint Extern 0 (envs_entails _ (_ - _)) => iIntros.
Hint Extern 0 (envs_entails _ ( _, _)) => iIntros : core.
Hint Extern 0 (envs_entails _ (_ _)) => iIntros : core.
Hint Extern 0 (envs_entails _ (_ - _)) => iIntros : core.
(* Multi-intro doesn't work for custom binders. *)
Hint Extern 0 (envs_entails _ (.. _, _)) => iIntros (?).
Hint Extern 1 (envs_entails _ (_ _)) => iSplit.
Hint Extern 1 (envs_entails _ (_ _)) => iSplit.
Hint Extern 1 (envs_entails _ ( _)) => iNext.
Hint Extern 1 (envs_entails _ ( _)) => iAlways.
Hint Extern 1 (envs_entails _ (<pers> _)) => iAlways.
Hint Extern 1 (envs_entails _ (<affine> _)) => iAlways.
Hint Extern 1 (envs_entails _ ( _)) => iAlways.
Hint Extern 1 (envs_entails _ ( _, _)) => iExists _.
Hint Extern 1 (envs_entails _ (.. _, _)) => iExists _.
Hint Extern 1 (envs_entails _ ( _)) => iModIntro.
Hint Extern 1 (envs_entails _ (_ _)) => iLeft.
Hint Extern 1 (envs_entails _ (_ _)) => iRight.
Hint Extern 1 (envs_entails _ (|==> _)) => iModIntro.
Hint Extern 1 (envs_entails _ (<absorb> _)) => iModIntro.
Hint Extern 2 (envs_entails _ (|={_}=> _)) => iModIntro.
Hint Extern 0 (envs_entails _ (.. _, _)) => iIntros (?) : core.
Hint Extern 1 (envs_entails _ (_ _)) => iSplit : core.
Hint Extern 1 (envs_entails _ (_ _)) => iSplit : core.
Hint Extern 1 (envs_entails _ ( _)) => iNext : core.
Hint Extern 1 (envs_entails _ ( _)) => iAlways : core.
Hint Extern 1 (envs_entails _ (<pers> _)) => iAlways : core.
Hint Extern 1 (envs_entails _ (<affine> _)) => iAlways : core.
Hint Extern 1 (envs_entails _ ( _)) => iAlways : core.
Hint Extern 1 (envs_entails _ ( _, _)) => iExists _ : core.
Hint Extern 1 (envs_entails _ (.. _, _)) => iExists _ : core.
Hint Extern 1 (envs_entails _ ( _)) => iModIntro : core.
Hint Extern 1 (envs_entails _ (_ _)) => iLeft : core.
Hint Extern 1 (envs_entails _ (_ _)) => iRight : core.
Hint Extern 1 (envs_entails _ (|==> _)) => iModIntro : core.
Hint Extern 1 (envs_entails _ (<absorb> _)) => iModIntro : core.
Hint Extern 2 (envs_entails _ (|={_}=> _)) => iModIntro : core.
Hint Extern 2 (envs_entails _ (_ _)) => progress iFrame : iFrame.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment