From 352f18651189c448a98c3ba7d9c78b3308ac794e Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 3 May 2016 11:30:11 +0200
Subject: [PATCH] No longer define Frame instances using Hint Extern.
We now give frame_here priority 0, so it is used immediately when an
evar occurs. This thus avoids loops in the presence of evars.
---
proofmode/coq_tactics.v | 41 +++++++++++++----------------------------
proofmode/pviewshifts.v | 5 +----
proofmode/weakestpre.v | 5 +----
3 files changed, 15 insertions(+), 36 deletions(-)
diff --git a/proofmode/coq_tactics.v b/proofmode/coq_tactics.v
index ae98291a5..29882b430 100644
--- a/proofmode/coq_tactics.v
+++ b/proofmode/coq_tactics.v
@@ -731,25 +731,25 @@ Class Frame (R P : uPred M) (mQ : option (uPred M)) :=
frame : (R ★ from_option True mQ) ⊢ P.
Arguments frame : clear implicits.
-Instance frame_here R : Frame R R None | 1.
+Global Instance frame_here R : Frame R R None.
Proof. by rewrite /Frame right_id. Qed.
-Instance frame_sep_l R P1 P2 mQ :
+Global Instance frame_sep_l R P1 P2 mQ :
Frame R P1 mQ →
- Frame R (P1 ★ P2) (Some $ if mQ is Some Q then Q ★ P2 else P2)%I.
+ Frame R (P1 ★ P2) (Some $ if mQ is Some Q then Q ★ P2 else P2)%I | 9.
Proof. rewrite /Frame => <-. destruct mQ; simpl; solve_sep_entails. Qed.
-Instance frame_sep_r R P1 P2 mQ :
+Global Instance frame_sep_r R P1 P2 mQ :
Frame R P2 mQ →
- Frame R (P1 ★ P2) (Some $ if mQ is Some Q then P1 ★ Q else P1)%I.
+ Frame R (P1 ★ P2) (Some $ if mQ is Some Q then P1 ★ Q else P1)%I | 10.
Proof. rewrite /Frame => <-. destruct mQ; simpl; solve_sep_entails. Qed.
-Instance frame_and_l R P1 P2 mQ :
+Global Instance frame_and_l R P1 P2 mQ :
Frame R P1 mQ →
- Frame R (P1 ∧ P2) (Some $ if mQ is Some Q then Q ∧ P2 else P2)%I.
+ Frame R (P1 ∧ P2) (Some $ if mQ is Some Q then Q ∧ P2 else P2)%I | 9.
Proof. rewrite /Frame => <-. destruct mQ; simpl; eauto 10 with I. Qed.
-Instance frame_and_r R P1 P2 mQ :
+Global Instance frame_and_r R P1 P2 mQ :
Frame R P2 mQ →
- Frame R (P1 ∧ P2) (Some $ if mQ is Some Q then P1 ∧ Q else P1)%I.
+ Frame R (P1 ∧ P2) (Some $ if mQ is Some Q then P1 ∧ Q else P1)%I | 10.
Proof. rewrite /Frame => <-. destruct mQ; simpl; eauto 10 with I. Qed.
-Instance frame_or R P1 P2 mQ1 mQ2 :
+Global Instance frame_or R P1 P2 mQ1 mQ2 :
Frame R P1 mQ1 → Frame R P2 mQ2 →
Frame R (P1 ∨ P2) (match mQ1, mQ2 with
| Some Q1, Some Q2 => Some (Q1 ∨ Q2)%I | _, _ => None
@@ -759,17 +759,17 @@ Proof.
destruct mQ1 as [Q1|], mQ2 as [Q2|]; simpl; auto with I.
by rewrite -sep_or_l.
Qed.
-Instance frame_later R P mQ :
+Global Instance frame_later R P mQ :
Frame R P mQ → Frame R (▷ P) (if mQ is Some Q then Some (▷ Q) else None)%I.
Proof.
rewrite /Frame=><-.
by destruct mQ; rewrite /= later_sep -(later_intro R) ?later_True.
Qed.
-Instance frame_exist {A} R (Φ : A → uPred M) mΨ :
+Global Instance frame_exist {A} R (Φ : A → uPred M) mΨ :
(∀ a, Frame R (Φ a) (mΨ a)) →
Frame R (∃ x, Φ x) (Some (∃ x, if mΨ x is Some Q then Q else True))%I.
Proof. rewrite /Frame=> ?. by rewrite sep_exist_l; apply exist_mono. Qed.
-Instance frame_forall {A} R (Φ : A → uPred M) mΨ :
+Global Instance frame_forall {A} R (Φ : A → uPred M) mΨ :
(∀ a, Frame R (Φ a) (mΨ a)) →
Frame R (∀ x, Φ x) (Some (∀ x, if mΨ x is Some Q then Q else True))%I.
Proof. rewrite /Frame=> ?. by rewrite sep_forall_l; apply forall_mono. Qed.
@@ -895,18 +895,3 @@ End tactics.
Hint Extern 0 (ToPosedProof True _ _) =>
class_apply @to_posed_proof_True : typeclass_instances.
-(** Make sure we can frame in the presence of evars without making Coq loop due
-to it applying these rules too eager.
-
-Note: that [Hint Mode Frame - + + - : typeclass_instances] would disable framing
-with evars entirely.
-Note: we give presence to framing on the left. *)
-Hint Extern 0 (Frame _ ?R _) => class_apply @frame_here : typeclass_instances.
-Hint Extern 9 (Frame _ (_ ★ _) _) => class_apply @frame_sep_l : typeclass_instances.
-Hint Extern 10 (Frame _ (_ ★ _) _) => class_apply @frame_sep_r : typeclass_instances.
-Hint Extern 9 (Frame _ (_ ∧ _) _) => class_apply @frame_and_l : typeclass_instances.
-Hint Extern 10 (Frame _ (_ ∧ _) _) => class_apply @frame_and_r : typeclass_instances.
-Hint Extern 10 (Frame _ (_ ∨ _) _) => class_apply @frame_or : typeclass_instances.
-Hint Extern 10 (Frame _ (â–· _) _) => class_apply @frame_later : typeclass_instances.
-Hint Extern 10 (Frame _ (∃ _, _) _) => class_apply @frame_exist : typeclass_instances.
-Hint Extern 10 (Frame _ (∀ _, _) _) => class_apply @frame_forall : typeclass_instances.
diff --git a/proofmode/pviewshifts.v b/proofmode/pviewshifts.v
index 8a47eec7d..f99165ba0 100644
--- a/proofmode/pviewshifts.v
+++ b/proofmode/pviewshifts.v
@@ -21,7 +21,7 @@ Global Instance exists_split_pvs {A} E1 E2 P (Φ : A → iProp Λ Σ) :
Proof.
rewrite /ExistSplit=><-. apply exist_elim=> a. by rewrite -(exist_intro a).
Qed.
-Instance frame_pvs E1 E2 R P mQ :
+Global Instance frame_pvs E1 E2 R P mQ :
Frame R P mQ →
Frame R (|={E1,E2}=> P) (Some (|={E1,E2}=> from_option True mQ))%I.
Proof. rewrite /Frame=><-. by rewrite pvs_frame_l. Qed.
@@ -97,9 +97,6 @@ Proof.
Qed.
End pvs.
-Hint Extern 10 (Frame _ (|={_,_}=> _) _) =>
- class_apply frame_pvs : typeclass_instances.
-
Tactic Notation "iPvsIntro" := apply tac_pvs_intro.
Tactic Notation "iPvsCore" constr(H) :=
diff --git a/proofmode/weakestpre.v b/proofmode/weakestpre.v
index 36ecbd2cd..ab3d1f0ea 100644
--- a/proofmode/weakestpre.v
+++ b/proofmode/weakestpre.v
@@ -8,7 +8,7 @@ Context {Λ : language} {Σ : iFunctor}.
Implicit Types P Q : iProp Λ Σ.
Implicit Types Φ : val Λ → iProp Λ Σ.
-Instance frame_wp E e R Φ mΨ :
+Global Instance frame_wp E e R Φ mΨ :
(∀ v, Frame R (Φ v) (mΨ v)) →
Frame R (WP e @ E {{ Φ }})
(Some (WP e @ E {{ v, if mΨ v is Some Q then Q else True }}))%I.
@@ -17,6 +17,3 @@ Global Instance fsa_split_wp E e Φ :
FSASplit (WP e @ E {{ Φ }})%I E (wp_fsa e) (language.atomic e) Φ.
Proof. split. done. apply _. Qed.
End weakestpre.
-
-Hint Extern 10 (Frame _ (WP _ @ _ {{ _ }}) _) =>
- class_apply frame_wp : typeclass_instances.
\ No newline at end of file
--
GitLab