Commit 5f519f56 authored by Robbert Krebbers's avatar Robbert Krebbers

Get rid of IntoAssert class.

parent 8e126e96
......@@ -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.
......@@ -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.
......
......@@ -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.
......
......@@ -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"
......
......@@ -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 *)
......
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