diff --git a/proofmode/classes.v b/proofmode/classes.v
index 5963a454d84c700a54cae6f9001ed87ff77cac32..224b1e48338410d8a3088648ce4c3d66d133c7ca 100644
--- a/proofmode/classes.v
+++ b/proofmode/classes.v
@@ -73,5 +73,8 @@ Global Arguments from_vs : clear implicits.
Class ElimVs (P P' : uPred M) (Q Q' : uPred M) :=
elim_vs : P ★ (P' -★ Q') ⊢ Q.
-Arguments elim_vs _ _ _ _ {_}.
+Global Arguments elim_vs _ _ _ _ {_}.
+
+Lemma elim_vs_dummy P Q : ElimVs P P Q Q.
+Proof. by rewrite /ElimVs wand_elim_r. Qed.
End classes.
diff --git a/proofmode/coq_tactics.v b/proofmode/coq_tactics.v
index 867ba424ed222514fcc2cf314090897927488c7e..4c270ef4083e38d2349d006ce65963e43641060d 100644
--- a/proofmode/coq_tactics.v
+++ b/proofmode/coq_tactics.v
@@ -531,17 +531,9 @@ Proof.
by rewrite right_id assoc (into_wand R) always_if_elim wand_elim_r wand_elim_r.
Qed.
-Class IntoAssert (P : uPred M) (Q : uPred M) (R : uPred M) :=
- into_assert : R ★ (P -★ Q) ⊢ Q.
-Global Arguments into_assert _ _ _ {_}.
-Lemma into_assert_default P Q : IntoAssert P Q P.
-Proof. by rewrite /IntoAssert wand_elim_r. Qed.
-Global Instance to_assert_rvs P Q : IntoAssert P (|=r=> Q) (|=r=> P).
-Proof. by rewrite /IntoAssert rvs_frame_r wand_elim_r rvs_trans. Qed.
-
Lemma tac_specialize_assert Δ Δ' Δ1 Δ2' j q lr js R P1 P2 P1' Q :
envs_lookup_delete j Δ = Some (q, R, Δ') →
- IntoWand R P1 P2 → IntoAssert P1 Q P1' →
+ IntoWand R P1 P2 → ElimVs P1' P1 Q Q →
('(Δ1,Δ2) ↠envs_split lr js Δ';
Δ2' ↠envs_app false (Esnoc Enil j P2) Δ2;
Some (Δ1,Δ2')) = Some (Δ1,Δ2') → (* does not preserve position of [j] *)
@@ -553,7 +545,7 @@ Proof.
rewrite envs_lookup_sound // envs_split_sound //.
rewrite (envs_app_sound Δ2) //; simpl.
rewrite right_id (into_wand R) HP1 assoc -(comm _ P1') -assoc.
- rewrite -(into_assert P1 Q); apply sep_mono_r, wand_intro_l.
+ rewrite -(elim_vs P1' P1 Q Q). apply sep_mono_r, wand_intro_l.
by rewrite always_if_elim assoc !wand_elim_r.
Qed.
@@ -614,11 +606,11 @@ Proof.
by rewrite -(idemp uPred_and Δ) {1}(persistentP Δ) {1}HP HPQ impl_elim_r.
Qed.
-Lemma tac_assert Δ Δ1 Δ2 Δ2' lr js j P Q R :
- IntoAssert P Q R →
+Lemma tac_assert Δ Δ1 Δ2 Δ2' lr js j P P' Q :
+ ElimVs P' P Q Q →
envs_split lr js Δ = Some (Δ1,Δ2) →
envs_app false (Esnoc Enil j P) Δ2 = Some Δ2' →
- (Δ1 ⊢ R) → (Δ2' ⊢ Q) → Δ ⊢ Q.
+ (Δ1 ⊢ P') → (Δ2' ⊢ Q) → Δ ⊢ Q.
Proof.
intros ??? HP HQ. rewrite envs_split_sound //.
rewrite (envs_app_sound Δ2) //; simpl.
diff --git a/proofmode/pviewshifts.v b/proofmode/pviewshifts.v
index ecdc794a5e363a601bcd071abc5292d00f6ecdb1..599068a754f469cc9a7ee300932133511831c944 100644
--- a/proofmode/pviewshifts.v
+++ b/proofmode/pviewshifts.v
@@ -36,10 +36,6 @@ Global Instance frame_pvs E1 E2 R P Q :
Frame R P Q → Frame R (|={E1,E2}=> P) (|={E1,E2}=> Q).
Proof. rewrite /Frame=><-. by rewrite pvs_frame_l. Qed.
-Global Instance to_assert_pvs E1 E2 P Q :
- IntoAssert P (|={E1,E2}=> Q) (|={E1}=> P).
-Proof. intros. by rewrite /IntoAssert pvs_frame_r wand_elim_r pvs_trans. Qed.
-
Global Instance is_except_last_pvs E1 E2 P : IsExceptLast (|={E1,E2}=> P).
Proof. by rewrite /IsExceptLast except_last_pvs. Qed.
@@ -47,10 +43,10 @@ Global Instance from_vs_pvs E P : FromVs (|={E}=> P) P.
Proof. by rewrite /FromVs -rvs_pvs. Qed.
Global Instance elim_vs_rvs_pvs E1 E2 P Q :
- ElimVs (|=r=> P) P (|={E1,E2}=> Q) (|={E1,E2}=> Q).
+ ElimVs (|=r=> P) P (|={E1,E2}=> Q) (|={E1,E2}=> Q) | 2.
Proof. by rewrite /ElimVs (rvs_pvs E1) pvs_frame_r wand_elim_r pvs_trans. Qed.
Global Instance elim_vs_pvs_pvs E1 E2 E3 P Q :
- ElimVs (|={E1,E2}=> P) P (|={E1,E3}=> Q) (|={E2,E3}=> Q).
+ ElimVs (|={E1,E2}=> P) P (|={E1,E3}=> Q) (|={E2,E3}=> Q) | 1.
Proof. by rewrite /ElimVs pvs_frame_r wand_elim_r pvs_trans. Qed.
End pvs.
diff --git a/proofmode/tactics.v b/proofmode/tactics.v
index 217ec83a62041863e05ce6cbaff8d83bedaa694c..0d692fd63aedc8280a1898ddc4bae66b8e14b749 100644
--- a/proofmode/tactics.v
+++ b/proofmode/tactics.v
@@ -312,7 +312,7 @@ Local Tactic Notation "iSpecializePat" constr(H) constr(pat) :=
[env_cbv; reflexivity || fail "iSpecialize:" H1 "not found"
|solve_to_wand H1
|match vs with
- | false => apply into_assert_default
+ | false => apply elim_vs_dummy
| true => apply _ || fail "iSpecialize: cannot generate view shifted goal"
end
|env_cbv; reflexivity || fail "iSpecialize:" Hs "not found"
@@ -1099,7 +1099,7 @@ Tactic Notation "iAssertCore" open_constr(Q) "with" constr(Hs) "as" tactic(tac)
| [SGoal (SpecGoal ?vs ?lr ?Hs_frame ?Hs)] =>
eapply tac_assert with _ _ _ lr (Hs_frame ++ Hs) H Q _;
[match vs with
- | false => apply into_assert_default
+ | false => apply elim_vs_dummy
| true => apply _ || fail "iAssert: cannot generate view shifted goal"
end
|env_cbv; reflexivity || fail "iAssert:" Hs "not found"
diff --git a/proofmode/weakestpre.v b/proofmode/weakestpre.v
index 90b01fb5c434365d6abef7081b09ff403f679f74..09e31c181241524e5cc1780d1e5cdb742ca16b77 100644
--- a/proofmode/weakestpre.v
+++ b/proofmode/weakestpre.v
@@ -12,19 +12,15 @@ Global Instance frame_wp E e R Φ Ψ :
(∀ v, Frame R (Φ v) (Ψ v)) → Frame R (WP e @ E {{ Φ }}) (WP e @ E {{ Ψ }}).
Proof. rewrite /Frame=> HR. rewrite wp_frame_l. apply wp_mono, HR. Qed.
-Global Instance to_assert_wp E e P Φ :
- IntoAssert P (WP e @ E {{ Ψ }}) (|={E}=> P).
-Proof. intros. by rewrite /IntoAssert pvs_frame_r wand_elim_r pvs_wp. Qed.
-
Global Instance is_except_last_wp E e Φ : IsExceptLast (WP e @ E {{ Φ }}).
Proof. by rewrite /IsExceptLast -{2}pvs_wp -except_last_pvs -pvs_intro. Qed.
Global Instance elim_vs_rvs_wp E e P Φ :
- ElimVs (|=r=> P) P (WP e @ E {{ Φ }}) (WP e @ E {{ Φ }}).
+ ElimVs (|=r=> P) P (WP e @ E {{ Φ }}) (WP e @ E {{ Φ }}) | 2.
Proof. by rewrite /ElimVs (rvs_pvs E) pvs_frame_r wand_elim_r pvs_wp. Qed.
Global Instance elim_vs_pvs_wp E e P Φ :
- ElimVs (|={E}=> P) P (WP e @ E {{ Φ }}) (WP e @ E {{ Φ }}).
+ ElimVs (|={E}=> P) P (WP e @ E {{ Φ }}) (WP e @ E {{ Φ }}) | 1.
Proof. by rewrite /ElimVs pvs_frame_r wand_elim_r pvs_wp. Qed.
(* lower precedence, if possible, it should always pick elim_vs_pvs_wp *)