Commit 8bf6270c authored by Robbert Krebbers's avatar Robbert Krebbers

Misc clean up.

parent 3466bb6e
...@@ -107,18 +107,15 @@ Proof. setoid_rewrite (comm _ _ R); apply ht_frame_l. Qed. ...@@ -107,18 +107,15 @@ Proof. setoid_rewrite (comm _ _ R); apply ht_frame_l. Qed.
Lemma ht_frame_step_l E E1 E2 P R1 R2 R3 e Φ : Lemma ht_frame_step_l E E1 E2 P R1 R2 R3 e Φ :
to_val e = None E E1 E2 E1 to_val e = None E E1 E2 E1
((R1 ={E1,E2}=> R2) (R2 ={E2,E1}=> R3) {{ P }} e @ E {{ Φ }}) ((R1 ={E1,E2}=> R2) (R2 ={E2,E1}=> R3) {{ P }} e @ E {{ Φ }})
{{ R1 P }} e @ (E E1) {{ λ v, R3 Φ v }}. {{ R1 P }} e @ E E1 {{ λ v, R3 Φ v }}.
Proof. Proof.
iIntros {???} "[#Hvs1 [#Hvs2 #Hwp]] ! [HR HP]". iIntros {???} "[#Hvs1 [#Hvs2 #Hwp]] ! [HR HP]".
iApply (wp_frame_step_l E E1 E2); try done. iApply (wp_frame_step_l E E1 E2); try done.
iSplitL "HR". iSplitL "HR"; [|by iApply "Hwp"].
- (* TODO: Is there a way to do "apply Hvs1 in Hr"? *) iPvs "Hvs1" "HR"; first by set_solver.
iPvs "Hvs1" "HR"; first by set_solver. iPvsIntro. iNext.
(* TODO: iApply pvs_intro? *) iPvs "Hvs2" "Hvs1"; first by set_solver.
rewrite -pvs_intro. by iPvsIntro.
iNext. iPvs "Hvs2" "Hvs1"; first by set_solver.
rewrite -pvs_intro. done.
- iApply "Hwp". done.
Qed. Qed.
Lemma ht_frame_step_r E E1 E2 P R1 R2 R3 e Φ : Lemma ht_frame_step_r E E1 E2 P R1 R2 R3 e Φ :
...@@ -128,8 +125,7 @@ Lemma ht_frame_step_r E E1 E2 P R1 R2 R3 e Φ : ...@@ -128,8 +125,7 @@ Lemma ht_frame_step_r E E1 E2 P R1 R2 R3 e Φ :
Proof. Proof.
iIntros {???} "[#Hvs1 [#Hvs2 #Hwp]]". iIntros {???} "[#Hvs1 [#Hvs2 #Hwp]]".
setoid_rewrite (comm _ _ R3). setoid_rewrite (comm _ _ R3).
iApply ht_frame_step_l; try eassumption. iSplit; last iSplit; iApply ht_frame_step_l; try eassumption. repeat iSplit; by iIntros "!".
iIntros "!"; done.
Qed. Qed.
Lemma ht_frame_step_l' E P R e Φ : Lemma ht_frame_step_l' E P R e Φ :
......
...@@ -198,33 +198,37 @@ Proof. ...@@ -198,33 +198,37 @@ Proof.
Qed. Qed.
Lemma wp_frame_step_r E E1 E2 e Φ R : Lemma wp_frame_step_r E E1 E2 e Φ R :
to_val e = None E E1 E2 E1 to_val e = None E E1 E2 E1
(WP e @ E {{ Φ }} |={E1,E2}=> |={E2,E1}=> R) (WP e @ E {{ Φ }} |={E1,E2}=> |={E2,E1}=> R)
WP e @ (E E1) {{ v, Φ v R }}. WP e @ E E1 {{ v, Φ v R }}.
Proof.
rewrite wp_eq pvs_eq=> He ??. rewrite wp_eq pvs_eq=> He ??.
uPred.unseal; split; intros n r' Hvalid (r&rR&Hr&Hwp&HR); cofe_subst. uPred.unseal; split; intros n r' Hvalid (r&rR&Hr&Hwp&HR); cofe_subst.
constructor; [done|]=>rf k Ef σ1 ?? Hws1. constructor; [done|]=>rf k Ef σ1 ?? Hws1.
destruct Hwp as [|n r e ? Hgo]; [by rewrite to_of_val in He|]. destruct Hwp as [|n r e ? Hgo]; [by rewrite to_of_val in He|].
(* "execute" HR *) (* "execute" HR *)
edestruct (HR (r rf) (S k) (E Ef) σ1) as [s [Hvs Hws2]]; [omega|set_solver| |]. destruct (HR (r rf) (S k) (E Ef) σ1) as (s&Hvs&Hws2); auto.
{ eapply wsat_change, Hws1; first by set_solver+. { eapply wsat_proper, Hws1; first by set_solver+.
rewrite assoc [rR _]comm. done. } clear Hws1 HR. by rewrite assoc [rR _]comm. }
clear Hws1 HR.
(* Take a step *) (* Take a step *)
destruct (Hgo (srf) k (E2 Ef) σ1) as [Hsafe Hstep]; [done|set_solver| |]. destruct (Hgo (srf) k (E2 Ef) σ1) as [Hsafe Hstep]; auto.
{ eapply wsat_change, Hws2; first by set_solver+. { eapply wsat_proper, Hws2; first by set_solver+.
rewrite !assoc [s _]comm. done. } clear Hgo. by rewrite !assoc [s _]comm. }
clear Hgo.
split; [done|intros e2 σ2 ef ?]. split; [done|intros e2 σ2 ef ?].
destruct (Hstep e2 σ2 ef) as (r2&r2'&Hws3&?&?); auto. clear Hws2. destruct (Hstep e2 σ2 ef) as (r2&r2'&Hws3&?&?); auto. clear Hws2.
(* Execute 2nd part of the view shift *) (* Execute 2nd part of the view shift *)
edestruct (Hvs (r2 r2' rf) k (E Ef) σ2) as [t [HR Hws4]]; [omega|set_solver| |]. destruct (Hvs (r2 r2' rf) k (E Ef) σ2) as (t&HR&Hws4); auto.
{ eapply wsat_change, Hws3; first by set_solver+. { eapply wsat_proper, Hws3; first by set_solver+.
rewrite !assoc [_ s]comm !assoc. done. } clear Hvs Hws3. by rewrite !assoc [_ s]comm !assoc. }
clear Hvs Hws3.
(* Execute the rest of e *) (* Execute the rest of e *)
exists (r2 t), r2'. split_and?; auto. exists (r2 t), r2'. split_and?; auto.
- eapply wsat_change, Hws4; first by set_solver+. - eapply wsat_proper, Hws4; first by set_solver+.
rewrite !assoc [_ t]comm. done. by rewrite !assoc [_ t]comm.
- rewrite -uPred_sep_eq. move:(wp_frame_r). rewrite wp_eq=>Hframe. - rewrite -uPred_sep_eq. move: wp_frame_r. rewrite wp_eq=>Hframe.
apply Hframe; first by auto. uPred.unseal; exists r2, t; split_and?; auto. apply Hframe; first by auto. uPred.unseal; exists r2, t; split_and?; auto.
move:(wp_mask_frame_mono). rewrite wp_eq=>Hmask. move: wp_mask_frame_mono. rewrite wp_eq=>Hmask.
eapply (Hmask E); by auto. eapply (Hmask E); by auto.
Qed. Qed.
Lemma wp_bind `{LanguageCtx Λ K} E e Φ : Lemma wp_bind `{LanguageCtx Λ K} E e Φ :
......
...@@ -42,11 +42,11 @@ Proof. ...@@ -42,11 +42,11 @@ Proof.
Qed. Qed.
Global Instance wsat_ne n : Proper (dist n ==> iff) (@wsat Λ Σ n E σ) | 1. Global Instance wsat_ne n : Proper (dist n ==> iff) (@wsat Λ Σ n E σ) | 1.
Proof. by intros E σ w1 w2 Hw; split; apply wsat_ne'. Qed. Proof. by intros E σ w1 w2 Hw; split; apply wsat_ne'. Qed.
Global Instance wsat_proper n : Proper (() ==> iff) (@wsat Λ Σ n E σ) | 1. Global Instance wsat_proper' n : Proper (() ==> iff) (@wsat Λ Σ n E σ) | 1.
Proof. by intros E σ w1 w2 Hw; apply wsat_ne, equiv_dist. Qed. Proof. by intros E σ w1 w2 Hw; apply wsat_ne, equiv_dist. Qed.
Lemma wsat_change n E1 E2 σ r1 r2 : Lemma wsat_proper n E1 E2 σ r1 r2 :
E1 = E2 r1 r2 wsat n E1 σ r1 wsat n E2 σ r2. E1 = E2 r1 r2 wsat n E1 σ r1 wsat n E2 σ r2.
Proof. move=>->->. done. Qed. Proof. by move=>->->. Qed.
Lemma wsat_le n n' E σ r : wsat n E σ r n' n wsat n' E σ r. Lemma wsat_le n n' E σ r : wsat n E σ r n' n wsat n' E σ r.
Proof. Proof.
destruct n as [|n], n' as [|n']; simpl; try by (auto with lia). destruct n as [|n], n' as [|n']; simpl; try by (auto with lia).
......
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