Commit 2fb90ca6 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Better framing support for disjunctions.

For example, framing `P` in `(P ∨ Q) ∗ R` now succeeds and turns the goal into `R`.
parent d328e59e
......@@ -92,7 +92,7 @@ Section proof.
wp_load. destruct (decide (x = o)) as [->|Hneq].
- iDestruct "Ha" as "[Hainv [[Ho HR] | Haown]]".
+ iMod ("Hclose" with "[Hlo Hln Hainv Ht]") as "_".
{ iNext. iExists o, n. iFrame. eauto. }
{ iNext. iExists o, n. iFrame. }
iModIntro. wp_let. wp_op. case_bool_decide; [|done].
wp_if.
iApply ("HΦ" with "[-]"). rewrite /locked. iFrame. eauto.
......
......@@ -532,8 +532,8 @@ Proof. by rewrite /MakeSep right_id. Qed.
Global Instance make_sep_default P Q : MakeSep P Q (P Q) | 100.
Proof. done. Qed.
Global Instance frame_sep_persistent_l R P1 P2 Q1 Q2 Q' :
Frame true R P1 Q1 MaybeFrame true R P2 Q2 MakeSep Q1 Q2 Q'
Global Instance frame_sep_persistent_l progress R P1 P2 Q1 Q2 Q' :
Frame true R P1 Q1 MaybeFrame true R P2 Q2 progress MakeSep Q1 Q2 Q'
Frame true R (P1 P2) Q' | 9.
Proof.
rewrite /Frame /MaybeFrame /MakeSep /= => <- <- <-.
......@@ -580,20 +580,33 @@ Proof. by rewrite /MakeOr right_absorb. Qed.
Global Instance make_or_default P Q : MakeOr P Q (P Q) | 100.
Proof. done. Qed.
Global Instance frame_or_persistent_l R P1 P2 Q1 Q2 Q :
Frame true R P1 Q1 MaybeFrame true R P2 Q2 MakeOr Q1 Q2 Q
Frame true R (P1 P2) Q | 9.
Proof. rewrite /Frame /MakeOr => <- <- <-. by rewrite -sep_or_l. Qed.
Global Instance frame_or_persistent_r R P1 P2 Q1 Q2 Q :
MaybeFrame true R P2 Q2 MakeOr P1 Q2 Q
Frame true R (P1 P2) Q | 10.
Proof.
rewrite /Frame /MaybeFrame /MakeOr => <- <-. by rewrite sep_or_l sep_elim_r.
Qed.
Global Instance frame_or R P1 P2 Q1 Q2 Q :
Frame false R P1 Q1 Frame false R P2 Q2 MakeOr Q1 Q2 Q
Frame false R (P1 P2) Q.
Proof. rewrite /Frame /MakeOr => <- <- <-. by rewrite -sep_or_l. Qed.
(* We could in principle write the instance [frame_or_spatial] by a bunch of
instances, i.e. (omitting the parameter [p = false]):
Frame R P1 Q1 → Frame R P2 Q2 → Frame R (P1 ∨ P2) (Q1 ∨ Q2)
Frame R P1 True → Frame R (P1 ∨ P2) P2
Frame R P2 True → Frame R (P1 ∨ P2) P1
The problem here is that Coq will try to infer [Frame R P1 ?] and [Frame R P2 ?]
multiple times, whereas the current solution makes sure that said inference
appears at most once.
If Coq would memorize the results of type class resolution, the solution with
multiple instances would be preferred (and more Prolog-like). *)
Global Instance frame_or_spatial progress1 progress2 R P1 P2 Q1 Q2 Q :
MaybeFrame false R P1 Q1 progress1 MaybeFrame false R P2 Q2 progress2
TCOr (TCEq (progress1 && progress2) true) (TCOr
(TCAnd (TCEq progress1 true) (TCEq Q1 True%I))
(TCAnd (TCEq progress2 true) (TCEq Q2 True%I)))
MakeOr Q1 Q2 Q
Frame false R (P1 P2) Q | 9.
Proof. rewrite /Frame /MakeOr => <- <- _ <-. by rewrite -sep_or_l. Qed.
Global Instance frame_or_persistent progress1 progress2 R P1 P2 Q1 Q2 Q :
MaybeFrame true R P1 Q1 progress1 MaybeFrame true R P2 Q2 progress2
TCEq (progress1 || progress2) true
MakeOr Q1 Q2 Q Frame true R (P1 P2) Q | 9.
Proof. rewrite /Frame /MakeOr => <- <- _ <-. by rewrite -sep_or_l. Qed.
Global Instance frame_wand p R P1 P2 Q2 :
Frame p R P2 Q2 Frame p R (P1 - P2) (P1 - Q2).
......
......@@ -190,14 +190,19 @@ Class Frame {M} (p : bool) (R P Q : uPred M) := frame : □?p R ∗ Q ⊢ P.
Arguments frame {_ _} _ _ _ {_}.
Hint Mode Frame + + ! ! - : typeclass_instances.
Class MaybeFrame {M} (p : bool) (R P Q : uPred M) := maybe_frame : ?p R Q P.
(* The boolean [progress] indicates whether actual framing has been performed.
If it is [false], then the default instance [maybe_frame_default] below has been
used. *)
Class MaybeFrame {M} (p : bool) (R P Q : uPred M) (progress : bool) :=
maybe_frame : ?p R Q P.
Arguments maybe_frame {_} _ _ _ {_}.
Hint Mode MaybeFrame + + ! ! - : typeclass_instances.
Hint Mode MaybeFrame + + ! ! - - : typeclass_instances.
Instance maybe_frame_frame {M} p (R P Q : uPred M) :
Frame p R P Q MaybeFrame p R P Q.
Frame p R P Q MaybeFrame p R P Q true.
Proof. done. Qed.
Instance maybe_frame_default {M} p (R P : uPred M) : MaybeFrame p R P P | 100.
Instance maybe_frame_default {M} p (R P : uPred M) :
MaybeFrame p R P P false | 100.
Proof. apply sep_elim_r. Qed.
Class FromOr {M} (P Q1 Q2 : uPred M) := from_or : Q1 Q2 P.
......
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