Merge branch 'no-implicit-core' into 'master'

Explicitly use core hint database

See merge request FP/iris-coq!191

theories/algebra/cmra.v

@@ -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.

theories/algebra/dra.v

@@ -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.

theories/algebra/ofe.v

@@ -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.

theories/algebra/sts.v

@@ -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.

theories/base_logic/bi.v

@@ -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.

theories/base_logic/upred.v

@@ -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.

theories/bi/derived_laws_bi.v

@@ -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' :

theories/bi/derived_laws_sbi.v

@@ -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' :

theories/bi/interface.v

@@ -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).
 

theories/bi/monpred.v

@@ -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) _.

theories/bi/plainly.v

@@ -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 _.

theories/heap_lang/lifting.v

@@ -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.

theories/program_logic/ectx_lifting.v

@@ -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 →

theories/program_logic/language.v

@@ -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.
 

theories/program_logic/lifting.v

@@ -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 →

theories/program_logic/ownp.v

@@ -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) ∗

theories/program_logic/total_ectx_lifting.v

@@ -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 →

theories/program_logic/total_lifting.v

@@ -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 →

theories/proofmode/environments.v

@@ -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

theories/proofmode/ltac_tactics.v

@@ -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.