Commit d59fa2f7 authored by Robbert Krebbers's avatar Robbert Krebbers

Use type classes instead of option hack to remove Trues while framing.

parent 4c27fb0a
Pipeline #1609 passed with stage
......@@ -796,65 +796,77 @@ Proof.
Qed.
(** * Framing *)
(** The [option] is to account for formulas that can be framed entirely, so
we do not end up with [True]s everywhere. *)
Class Frame (R P : uPred M) (mQ : option (uPred M)) :=
frame : R from_option id True mQ P.
Class Frame (R P Q : uPred M) := frame : R Q P.
Arguments frame : clear implicits.
Global Instance frame_here R : Frame R R None.
Global Instance frame_here R : Frame R R True.
Proof. by rewrite /Frame right_id. Qed.
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 | 9.
Proof. rewrite /Frame => <-. destruct mQ; simpl; solve_sep_entails. Qed.
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 | 10.
Proof. rewrite /Frame => <-. destruct mQ; simpl; solve_sep_entails. Qed.
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 | 9.
Proof. rewrite /Frame => <-. destruct mQ; simpl; eauto 10 with I. Qed.
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 | 10.
Proof. rewrite /Frame => <-. destruct mQ; simpl; eauto 10 with I. Qed.
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
end).
Proof.
rewrite /Frame=> <- <-.
destruct mQ1 as [Q1|], mQ2 as [Q2|]; simpl; auto with I.
by rewrite -sep_or_l.
Qed.
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.
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.
Class MakeSep (P Q PQ : uPred M) := make_sep : P Q ⊣⊢ PQ.
Global Instance make_sep_true_l P : MakeSep True P P.
Proof. by rewrite /MakeSep left_id. Qed.
Global Instance make_sep_true_r P : MakeSep P True P.
Proof. by rewrite /MakeSep right_id. Qed.
Global Instance make_sep_fallthrough P Q : MakeSep P Q (P Q) | 100.
Proof. done. Qed.
Global Instance frame_sep_l R P1 P2 Q Q' :
Frame R P1 Q MakeSep Q P2 Q' Frame R (P1 P2) Q' | 9.
Proof. rewrite /Frame /MakeSep => <- <-. by rewrite assoc. Qed.
Global Instance frame_sep_r R P1 P2 Q Q' :
Frame R P2 Q MakeSep P1 Q Q' Frame R (P1 P2) Q' | 10.
Proof. rewrite /Frame /MakeSep => <- <-. solve_sep_entails. Qed.
Class MakeAnd (P Q PQ : uPred M) := make_and : P Q ⊣⊢ PQ.
Global Instance make_and_true_l P : MakeAnd True P P.
Proof. by rewrite /MakeAnd left_id. Qed.
Global Instance make_and_true_r P : MakeAnd P True P.
Proof. by rewrite /MakeAnd right_id. Qed.
Global Instance make_and_fallthrough P Q : MakeSep P Q (P Q) | 100.
Proof. done. Qed.
Global Instance frame_and_l R P1 P2 Q Q' :
Frame R P1 Q MakeAnd Q P2 Q' Frame R (P1 P2) Q' | 9.
Proof. rewrite /Frame /MakeAnd => <- <-; eauto 10 with I. Qed.
Global Instance frame_and_r R P1 P2 Q Q' :
Frame R P2 Q MakeAnd P1 Q Q' Frame R (P1 P2) Q' | 10.
Proof. rewrite /Frame /MakeAnd => <- <-; eauto 10 with I. Qed.
Class MakeOr (P Q PQ : uPred M) := make_or : P Q ⊣⊢ PQ.
Global Instance make_or_true_l P : MakeOr True P True.
Proof. by rewrite /MakeOr left_absorb. Qed.
Global Instance make_or_true_r P : MakeOr P True True.
Proof. by rewrite /MakeOr right_absorb. Qed.
Global Instance make_or_fallthrough P Q : MakeOr P Q (P Q) | 100.
Proof. done. Qed.
Global Instance frame_or R P1 P2 Q1 Q2 Q :
Frame R P1 Q1 Frame R P2 Q2 MakeOr Q1 Q2 Q Frame R (P1 P2) Q.
Proof. rewrite /Frame /MakeOr => <- <- <-. by rewrite -sep_or_l. Qed.
Class MakeLater (P lP : uPred M) := make_later : P ⊣⊢ lP.
Global Instance make_later_true : MakeLater True True.
Proof. by rewrite /MakeLater later_True. Qed.
Global Instance make_later_fallthrough P : MakeLater P ( P) | 100.
Proof. done. Qed.
Global Instance frame_later R P Q Q' :
Frame R P Q MakeLater Q Q' Frame R ( P) Q'.
Proof.
rewrite /Frame /MakeLater=><- <-. by rewrite later_sep -(later_intro R).
Qed.
Global Instance frame_exist {A} R (Φ Ψ : A uPred M) :
( a, Frame R (Φ a) (Ψ a)) Frame R ( x, Φ x) ( x, Ψ x).
Proof. rewrite /Frame=> ?. by rewrite sep_exist_l; apply exist_mono. Qed.
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.
Global Instance frame_forall {A} R (Φ Ψ : A uPred M) :
( a, Frame R (Φ a) (Ψ a)) Frame R ( x, Φ x) ( x, Ψ x).
Proof. rewrite /Frame=> ?. by rewrite sep_forall_l; apply forall_mono. Qed.
Lemma tac_frame Δ Δ' i p R P mQ :
envs_lookup_delete i Δ = Some (p, R, Δ') Frame R P mQ
(if mQ is Some Q then (if p then Δ else Δ') Q else True)
Δ P.
Lemma tac_frame Δ Δ' i p R P Q :
envs_lookup_delete i Δ = Some (p, R, Δ') Frame R P Q
((if p then Δ else Δ') Q) Δ P.
Proof.
intros [? ->]%envs_lookup_delete_Some ? HQ. destruct p.
- rewrite envs_lookup_persistent_sound // always_elim.
rewrite -(frame R P). destruct mQ as [Q|]; rewrite ?HQ /=; auto with I.
- rewrite envs_lookup_sound //; simpl.
rewrite -(frame R P). destruct mQ as [Q|]; rewrite ?HQ /=; auto with I.
- by rewrite envs_lookup_persistent_sound // always_elim -(frame R P) HQ.
- rewrite envs_lookup_sound //; simpl. by rewrite -(frame R P) HQ.
Qed.
(** * Disjunction *)
......
......@@ -21,9 +21,8 @@ Global Instance exists_split_pvs {A} E1 E2 P (Φ : A → iProp Λ Σ) :
Proof.
rewrite /ExistSplit=><-. apply exist_elim=> a. by rewrite -(exist_intro a).
Qed.
Global Instance frame_pvs E1 E2 R P mQ :
Frame R P mQ
Frame R (|={E1,E2}=> P) (Some (|={E1,E2}=> if mQ is Some Q then Q else True))%I.
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_wand_pvs E1 E2 R P Q :
ToWand R P Q ToWand R (|={E1,E2}=> P) (|={E1,E2}=> Q) | 100.
......
......@@ -8,10 +8,8 @@ Context {Λ : language} {Σ : iFunctor}.
Implicit Types P Q : iProp Λ Σ.
Implicit Types Φ : val Λ iProp Λ Σ.
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.
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 fsa_split_wp E e Φ :
FSASplit (WP e @ E {{ Φ }})%I E (wp_fsa e) (language.atomic e) Φ.
......
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