Verified Commit 247db01f authored by Tej Chajed's avatar Tej Chajed
Browse files

Add explicit Local to non-Global hints

parent e8d341be
......@@ -141,11 +141,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 : core.
Local 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 : core.
Local 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.
......
......@@ -54,12 +54,12 @@ Definition up_set (S : states sts) (T : tokens sts) : states sts :=
S = λ s, up s T.
(** Tactic setup *)
Hint Resolve Step : core.
Hint Extern 50 (equiv (A:=propset _) _ _) => set_solver : sts.
Hint Extern 50 (¬equiv (A:=propset _) _ _) => set_solver : sts.
Hint Extern 50 (_ _) => set_solver : sts.
Hint Extern 50 (_ _) => set_solver : sts.
Hint Extern 50 (_ ## _) => set_solver : sts.
Local Hint Resolve Step : core.
Local Hint Extern 50 (equiv (A:=propset _) _ _) => set_solver : sts.
Local Hint Extern 50 (¬equiv (A:=propset _) _ _) => set_solver : sts.
Local Hint Extern 50 (_ _) => set_solver : sts.
Local Hint Extern 50 (_ _) => set_solver : sts.
Local Hint Extern 50 (_ ## _) => set_solver : sts.
(** ** Setoids *)
Instance frame_step_mono : Proper (flip () ==> (=) ==> (=) ==> impl) frame_step.
......@@ -221,11 +221,11 @@ Instance sts_op : Op (car sts) := λ x1 x2,
| auth s T1, auth _ T2 => auth s (T1 T2)(* never happens *)
end.
Hint Extern 50 (equiv (A:=propset _) _ _) => set_solver : sts.
Hint Extern 50 ( s : state sts, _) => set_solver : sts.
Hint Extern 50 (_ _) => set_solver : sts.
Hint Extern 50 (_ _) => set_solver : sts.
Hint Extern 50 (_ ## _) => set_solver : sts.
Local Hint Extern 50 (equiv (A:=propset _) _ _) => set_solver : sts.
Local Hint Extern 50 ( s : state sts, _) => set_solver : sts.
Local Hint Extern 50 (_ _) => set_solver : sts.
Local Hint Extern 50 (_ _) => set_solver : sts.
Local Hint Extern 50 (_ ## _) => set_solver : sts.
Global Instance auth_proper s : Proper (() ==> ()) (@auth sts s).
Proof. by constructor. Qed.
......
......@@ -429,7 +429,7 @@ Implicit Types φ : Prop.
Implicit Types P Q : uPred M.
Implicit Types A : Type.
Arguments uPred_holds {_} !_ _ _ /.
Hint Immediate uPred_in_entails : core.
Local 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.
......
......@@ -21,7 +21,7 @@ Implicit Types P Q R : PROP.
Implicit Types Ps : list PROP.
Implicit Types A : Type.
Hint Extern 100 (NonExpansive _) => solve_proper : core.
Local Hint Extern 100 (NonExpansive _) => solve_proper : core.
(* Force implicit argument PROP *)
Notation "P ⊢ Q" := (P @{PROP} Q).
......@@ -95,9 +95,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 : core.
Hint Resolve or_elim or_intro_l' or_intro_r' : core.
Hint Resolve and_intro and_elim_l' and_elim_r' : core.
Local Hint Resolve pure_intro forall_intro : core.
Local Hint Resolve or_elim or_intro_l' or_intro_r' : core.
Local 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.
......@@ -114,7 +114,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 : core.
Local Hint Immediate False_elim : core.
Lemma entails_eq_True P Q : (P Q) ((P Q)%I True%I).
Proof.
......@@ -337,7 +337,7 @@ Proof. rewrite /bi_iff; apply and_intro; apply impl_intro_l; auto. Qed.
(* BI Stuff *)
Hint Resolve sep_mono : core.
Local 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'.
......@@ -810,7 +810,7 @@ Section bi_affine.
End bi_affine.
(* Properties of the persistence modality *)
Hint Resolve persistently_mono : core.
Local 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' :
......
......@@ -17,14 +17,14 @@ 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 : core.
Hint Resolve and_elim_l' and_elim_r' and_intro forall_intro : core.
Local Hint Resolve or_elim or_intro_l' or_intro_r' True_intro False_elim : core.
Local Hint Resolve and_elim_l' and_elim_r' and_intro forall_intro : core.
Global Instance later_proper :
Proper (() ==> ()) (@bi_later PROP) := ne_proper _.
(* Later derived *)
Hint Resolve later_mono : core.
Local Hint Resolve later_mono : core.
Global Instance later_mono' : Proper (() ==> ()) (@bi_later PROP).
Proof. intros P Q; apply later_mono. Qed.
Global Instance later_flip_mono' :
......
......@@ -85,10 +85,10 @@ Global Instance internal_eq_proper (A : ofeT) :
Proper (() ==> () ==> ()) (@internal_eq PROP _ A) := ne_proper_2 _.
(* Equality *)
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.
Hint Resolve internal_eq_refl : core.
Hint Extern 100 (NonExpansive _) => solve_proper : core.
Local Hint Resolve or_elim or_intro_l' or_intro_r' True_intro False_elim : core.
Local Hint Resolve and_elim_l' and_elim_r' and_intro forall_intro : core.
Local Hint Resolve internal_eq_refl : core.
Local 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.
......
......@@ -121,7 +121,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 : core.
Local Hint Immediate monPred_in_entails : core.
Program Definition monPred_upclosed (Φ : I PROP) : monPred :=
MonPred (λ i, ( j, i j Φ j)%I) _.
......
......@@ -110,9 +110,9 @@ Section plainly_derived.
Context `{BiPlainly PROP}.
Implicit Types P : PROP.
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.
Local Hint Resolve pure_intro forall_intro : core.
Local Hint Resolve or_elim or_intro_l' or_intro_r' : core.
Local Hint Resolve and_intro and_elim_l' and_elim_r' : core.
Global Instance plainly_proper :
Proper (() ==> ()) (@plainly PROP _) := ne_proper _.
......
......@@ -10,10 +10,10 @@ 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 : core.
Local Hint Resolve head_prim_reducible head_reducible_prim_step : core.
Local Definition reducible_not_val_inhabitant e := reducible_not_val e inhabitant.
Hint Resolve reducible_not_val_inhabitant : core.
Hint Resolve head_stuck_stuck : core.
Local Hint Resolve reducible_not_val_inhabitant : core.
Local Hint Resolve head_stuck_stuck : core.
Lemma wp_lift_head_step_fupd {s E Φ} e1 :
to_val e1 = None
......
......@@ -109,7 +109,7 @@ Section language.
ρ2 = (t1 ++ e2 :: t2 ++ efs, σ2)
prim_step e1 σ1 κ e2 σ2 efs
step ρ1 κ ρ2.
Hint Constructors step : core.
Local Hint Constructors step : core.
Inductive nsteps : nat cfg Λ list (observation Λ) cfg Λ Prop :=
| nsteps_refl ρ :
......@@ -118,7 +118,7 @@ Section language.
step ρ1 κ ρ2
nsteps n ρ2 κs ρ3
nsteps (S n) ρ1 (κ ++ κs) ρ3.
Hint Constructors nsteps : core.
Local Hint Constructors nsteps : core.
Definition erased_step (ρ1 ρ2 : cfg Λ) := κ, step ρ1 κ ρ2.
......
......@@ -14,7 +14,7 @@ Implicit Types σ : state Λ.
Implicit Types P Q : iProp Σ.
Implicit Types Φ : val Λ iProp Σ.
Hint Resolve reducible_no_obs_reducible : core.
Local Hint Resolve reducible_no_obs_reducible : core.
Lemma wp_lift_step_fupd s E Φ e1 :
to_val e1 = None
......
......@@ -210,10 +210,10 @@ Section ectx_lifting.
Implicit Types s : stuckness.
Implicit Types Φ : val Λ iProp Σ.
Implicit Types e : expr Λ.
Hint Resolve head_prim_reducible head_reducible_prim_step : core.
Local Hint Resolve head_prim_reducible head_reducible_prim_step : core.
Local Definition reducible_not_val_inhabitant e := reducible_not_val e inhabitant.
Hint Resolve reducible_not_val_inhabitant : core.
Hint Resolve head_stuck_stuck : core.
Local Hint Resolve reducible_not_val_inhabitant : core.
Local Hint Resolve head_stuck_stuck : core.
Lemma ownP_lift_head_step s E Φ e1 :
(|={E,}=> σ1, head_reducible e1 σ1 (ownP σ1)
......
......@@ -9,7 +9,7 @@ Implicit Types P : iProp Σ.
Implicit Types Φ : val Λ iProp Σ.
Implicit Types v : val Λ.
Implicit Types e : expr Λ.
Hint Resolve head_prim_reducible_no_obs head_reducible_prim_step
Local Hint Resolve head_prim_reducible_no_obs head_reducible_prim_step
head_reducible_no_obs_reducible : core.
Lemma twp_lift_head_step {s E Φ} e1 :
......
......@@ -11,7 +11,7 @@ Implicit Types σ : state Λ.
Implicit Types P Q : iProp Σ.
Implicit Types Φ : val Λ iProp Σ.
Hint Resolve reducible_no_obs_reducible : core.
Local Hint Resolve reducible_no_obs_reducible : core.
Lemma twp_lift_step s E Φ e1 :
to_val e1 = None
......
......@@ -90,7 +90,7 @@ Context {A : Type}.
Implicit Types Γ : env A.
Implicit Types i : ident.
Implicit Types x : A.
Hint Resolve Esnoc_wf Enil_wf : core.
Local Hint Resolve Esnoc_wf Enil_wf : core.
Ltac simplify :=
repeat match goal with
......
Supports Markdown
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