Commit 1622b639 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan

Merge branch 'robbert/add_modal' into 'master'

Special proof mode class for adding a modality to a goal

See merge request FP/iris-coq!107
parents 1418f5db a63f256e
Pipeline #6223 passed with stages
in 9 minutes and 31 seconds
......@@ -211,17 +211,18 @@ Section proofmode_classes.
Global Instance from_modal_fupd E P : FromModal (|={E}=> P) P.
Proof. rewrite /FromModal. apply fupd_intro. Qed.
(* Put a lower priority compared to [elim_modal_fupd_fupd], so that
it is not taken when the first parameter is not specified (in
spec. patterns). *)
Global Instance elim_modal_bupd_fupd E1 E2 P Q :
ElimModal (|==> P) P (|={E1,E2}=> Q) (|={E1,E2}=> Q) | 10.
ElimModal (|==> P) P (|={E1,E2}=> Q) (|={E1,E2}=> Q).
Proof.
by rewrite /ElimModal (bupd_fupd E1) fupd_frame_r wand_elim_r fupd_trans.
Qed.
Global Instance elim_modal_fupd_fupd E1 E2 E3 P Q :
ElimModal (|={E1,E2}=> P) P (|={E1,E3}=> Q) (|={E2,E3}=> Q).
Proof. by rewrite /ElimModal fupd_frame_r wand_elim_r fupd_trans. Qed.
Global Instance add_modal_fupd E1 E2 P Q :
AddModal (|={E1}=> P) P (|={E1,E2}=> Q).
Proof. by rewrite /AddModal fupd_frame_r wand_elim_r fupd_trans. Qed.
End proofmode_classes.
Hint Extern 2 (coq_tactics.envs_entails _ (|={_}=> _)) => iModIntro.
......
......@@ -393,10 +393,13 @@ Section proofmode_classes.
ElimModal (|={E}=> P) P (WP e @ s; E {{ Φ }}) (WP e @ s; E {{ Φ }}).
Proof. by rewrite /ElimModal fupd_frame_r wand_elim_r fupd_wp. Qed.
(* lower precedence, if possible, it should persistently pick elim_upd_fupd_wp *)
Global Instance elim_modal_fupd_wp_atomic s E1 E2 e P Φ :
Atomic (stuckness_to_atomicity s) e
ElimModal (|={E1,E2}=> P) P
(WP e @ s; E1 {{ Φ }}) (WP e @ s; E2 {{ v, |={E2,E1}=> Φ v }})%I | 100.
(WP e @ s; E1 {{ Φ }}) (WP e @ s; E2 {{ v, |={E2,E1}=> Φ v }})%I.
Proof. intros. by rewrite /ElimModal fupd_frame_r wand_elim_r wp_atomic. Qed.
Global Instance add_modal_fupd_wp s E e P Φ :
AddModal (|={E}=> P) P (WP e @ s; E {{ Φ }}).
Proof. by rewrite /AddModal fupd_frame_r wand_elim_r fupd_wp. Qed.
End proofmode_classes.
......@@ -881,6 +881,22 @@ Proof.
intros _ _. by rewrite /ElimModal wand_elim_r.
Qed.
(* AddModal *)
Global Instance add_modal_wand P P' Q R :
AddModal P P' Q AddModal P P' (R - Q).
Proof.
rewrite /AddModal=> H. apply wand_intro_r.
by rewrite wand_curry -assoc (comm _ P') -wand_curry wand_elim_l.
Qed.
Global Instance add_modal_forall {A} P P' (Φ : A uPred M) :
( x, AddModal P P' (Φ x)) AddModal P P' ( x, Φ x).
Proof.
rewrite /AddModal=> H. apply forall_intro=> a. by rewrite (forall_elim a).
Qed.
Global Instance add_modal_bupd P Q : AddModal (|==> P) P (|==> Q).
Proof. by rewrite /AddModal bupd_frame_r wand_elim_r bupd_trans. Qed.
(** IsExcept0 *)
Global Instance is_except_0_except_0 P : IsExcept0 ( P).
Proof. by rewrite /IsExcept0 except_0_idemp. Qed.
Global Instance is_except_0_later P : IsExcept0 ( P).
......
......@@ -236,10 +236,16 @@ Class ElimModal {M} (P P' : uPred M) (Q Q' : uPred M) :=
elim_modal : P (P' - Q') Q.
Arguments elim_modal {_} _ _ _ _ {_}.
Hint Mode ElimModal + ! - ! - : typeclass_instances.
Hint Mode ElimModal + - ! - ! : typeclass_instances.
Lemma elim_modal_dummy {M} (P Q : uPred M) : ElimModal P P Q Q.
Proof. by rewrite /ElimModal wand_elim_r. Qed.
(* Used by the specialization pattern [ > ] in [iSpecialize] and [iAssert] to
add a modality to the goal corresponding to a premise/asserted proposition. *)
Class AddModal {M} (P P' : uPred M) (Q : uPred M) :=
add_modal : P (P' - Q) Q.
Arguments add_modal {_} _ _ _ {_}.
Hint Mode AddModal + - ! ! : typeclass_instances.
Lemma add_modal_id {M} (P Q : uPred M) : AddModal P P Q.
Proof. by rewrite /AddModal wand_elim_r. Qed.
Class IsExcept0 {M} (Q : uPred M) := is_except_0 : Q Q.
Arguments is_except_0 {_} _ {_}.
......
......@@ -644,7 +644,7 @@ Qed.
Lemma tac_specialize_assert Δ Δ' Δ1 Δ2' j q neg js R P1 P2 P1' Q :
envs_lookup_delete j Δ = Some (q, R, Δ')
IntoWand false R P1 P2 ElimModal P1' P1 Q Q
IntoWand false R P1 P2 AddModal P1' P1 Q
(''(Δ1,Δ2) envs_split (if neg is true then Right else Left) js Δ';
Δ2' envs_app false (Esnoc Enil j P2) Δ2;
Some (Δ1,Δ2')) = Some (Δ1,Δ2') (* does not preserve position of [j] *)
......@@ -656,7 +656,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 -(elim_modal P1' P1 Q Q). apply sep_mono_r, wand_intro_l.
rewrite -(add_modal P1' P1 Q). apply sep_mono_r, wand_intro_l.
by rewrite persistently_if_elim assoc !wand_elim_r.
Qed.
......@@ -666,7 +666,7 @@ Proof. by unlock. Qed.
Lemma tac_specialize_frame Δ Δ' j q R P1 P2 P1' Q Q' :
envs_lookup_delete j Δ = Some (q, R, Δ')
IntoWand false R P1 P2
ElimModal P1' P1 Q Q
AddModal P1' P1 Q
envs_entails Δ' (P1' locked Q')
Q' = (P2 - Q)%I
envs_entails Δ Q.
......@@ -674,7 +674,7 @@ Proof.
rewrite /envs_entails. intros [? ->]%envs_lookup_delete_Some ?? HPQ ->.
rewrite envs_lookup_sound //. rewrite HPQ -lock.
rewrite (into_wand _ R) assoc -(comm _ P1') -assoc persistently_if_elim.
rewrite -{2}(elim_modal P1' P1 Q Q). apply sep_mono_r, wand_intro_l.
rewrite -{2}(add_modal P1' P1 Q). apply sep_mono_r, wand_intro_l.
by rewrite assoc !wand_elim_r.
Qed.
......@@ -748,7 +748,7 @@ Proof.
Qed.
Lemma tac_assert Δ Δ1 Δ2 Δ2' neg js j P P' Q :
ElimModal P' P Q Q
AddModal P' P Q
envs_split (if neg is true then Right else Left) js Δ = Some (Δ1,Δ2)
envs_app false (Esnoc Enil j P) Δ2 = Some Δ2'
envs_entails Δ1 P' envs_entails Δ2' Q envs_entails Δ Q.
......
......@@ -456,7 +456,7 @@ Local Tactic Notation "iSpecializePat" open_constr(H) constr(pat) :=
[env_reflexivity || fail "iSpecialize:" H1 "not found"
|solve_to_wand H1
|lazymatch m with
| GSpatial => apply elim_modal_dummy
| GSpatial => apply add_modal_id
| GModal => apply _ || fail "iSpecialize: goal not a modality"
end
|env_reflexivity ||
......@@ -479,7 +479,7 @@ Local Tactic Notation "iSpecializePat" open_constr(H) constr(pat) :=
[env_reflexivity || fail "iSpecialize:" H1 "not found"
|solve_to_wand H1
|lazymatch m with
| GSpatial => apply elim_modal_dummy
| GSpatial => apply add_modal_id
| GModal => apply _ || fail "iSpecialize: goal not a modality"
end
|iFrame "∗ #"; apply tac_unlock ||
......@@ -1588,7 +1588,7 @@ Tactic Notation "iAssertCore" open_constr(Q)
| false =>
eapply tac_assert with _ _ _ lr Hs' H Q _;
[lazymatch m with
| GSpatial => apply elim_modal_dummy
| GSpatial => apply add_modal_id
| GModal => apply _ || fail "iAssert: goal not a modality"
end
|env_reflexivity ||
......
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