Commit 3466bb6e authored by Robbert Krebbers's avatar Robbert Krebbers

Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coq

parents b92a75d3 b0ec18bc
This diff is collapsed.
...@@ -104,20 +104,48 @@ Lemma ht_frame_r E P Φ R e : ...@@ -104,20 +104,48 @@ Lemma ht_frame_r E P Φ R e :
{{ P }} e @ E {{ Φ }} {{ P R }} e @ E {{ v, Φ v R }}. {{ P }} e @ E {{ Φ }} {{ P R }} e @ E {{ v, Φ v R }}.
Proof. setoid_rewrite (comm _ _ R); apply ht_frame_l. Qed. Proof. setoid_rewrite (comm _ _ R); apply ht_frame_l. Qed.
Lemma ht_frame_step_l E P R e Φ : Lemma ht_frame_step_l E E1 E2 P R1 R2 R3 e Φ :
to_val e = None E E1 E2 E1
((R1 ={E1,E2}=> R2) (R2 ={E2,E1}=> R3) {{ P }} e @ E {{ Φ }})
{{ R1 P }} e @ (E E1) {{ λ v, R3 Φ v }}.
Proof.
iIntros {???} "[#Hvs1 [#Hvs2 #Hwp]] ! [HR HP]".
iApply (wp_frame_step_l E E1 E2); try done.
iSplitL "HR".
- (* TODO: Is there a way to do "apply Hvs1 in Hr"? *)
iPvs "Hvs1" "HR"; first by set_solver.
(* TODO: iApply pvs_intro? *)
rewrite -pvs_intro.
iNext. iPvs "Hvs2" "Hvs1"; first by set_solver.
rewrite -pvs_intro. done.
- iApply "Hwp". done.
Qed.
Lemma ht_frame_step_r E E1 E2 P R1 R2 R3 e Φ :
to_val e = None E E1 E2 E1
((R1 ={E1,E2}=> R2) (R2 ={E2,E1}=> R3) {{ P }} e @ E {{ Φ }})
{{ R1 P }} e @ (E E1) {{ λ v, Φ v R3 }}.
Proof.
iIntros {???} "[#Hvs1 [#Hvs2 #Hwp]]".
setoid_rewrite (comm _ _ R3).
iApply ht_frame_step_l; try eassumption. iSplit; last iSplit;
iIntros "!"; done.
Qed.
Lemma ht_frame_step_l' E P R e Φ :
to_val e = None to_val e = None
{{ P }} e @ E {{ Φ }} {{ R P }} e @ E {{ v, R Φ v }}. {{ P }} e @ E {{ Φ }} {{ R P }} e @ E {{ v, R Φ v }}.
Proof. Proof.
iIntros {?} "#Hwp ! [HR HP]". iIntros {?} "#Hwp ! [HR HP]".
iApply wp_frame_step_l; try done. iFrame "HR". by iApply "Hwp". iApply wp_frame_step_l'; try done. iFrame "HR". by iApply "Hwp".
Qed. Qed.
Lemma ht_frame_step_r E P Φ R e : Lemma ht_frame_step_r' E P Φ R e :
to_val e = None to_val e = None
{{ P }} e @ E {{ Φ }} {{ P R }} e @ E {{ v, Φ v R }}. {{ P }} e @ E {{ Φ }} {{ P R }} e @ E {{ v, Φ v R }}.
Proof. Proof.
iIntros {?} "#Hwp ! [HP HR]". iIntros {?} "#Hwp ! [HP HR]".
iApply wp_frame_step_r; try done. iFrame "HR". by iApply "Hwp". iApply wp_frame_step_r'; try done. iFrame "HR". by iApply "Hwp".
Qed. Qed.
Lemma ht_inv N E P Φ R e : Lemma ht_inv N E P Φ R e :
......
...@@ -196,22 +196,36 @@ Proof. ...@@ -196,22 +196,36 @@ Proof.
- by rewrite -(assoc _ r2) (comm _ rR) !assoc -(assoc _ _ rR). - by rewrite -(assoc _ r2) (comm _ rR) !assoc -(assoc _ _ rR).
- apply IH; eauto using uPred_weaken. - apply IH; eauto using uPred_weaken.
Qed. Qed.
Lemma wp_frame_step_r E e Φ R : Lemma wp_frame_step_r E E1 E2 e Φ R :
to_val e = None (WP e @ E {{ Φ }} R) WP e @ E {{ v, Φ v R }}. to_val e = None E E1 E2 E1
Proof. (WP e @ E {{ Φ }} |={E1,E2}=> |={E2,E1}=> R)
rewrite wp_eq. WP e @ (E E1) {{ v, Φ v R }}.
intros He; uPred.unseal; split; intros n r' Hvalid (r&rR&Hr&Hwp&?). rewrite wp_eq pvs_eq=> He ??.
revert Hvalid; rewrite Hr; clear Hr. uPred.unseal; split; intros n r' Hvalid (r&rR&Hr&Hwp&HR); cofe_subst.
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|].
constructor; [done|]=>rf k Ef σ1 ???; destruct n as [|n]; first omega. (* "execute" HR *)
destruct (Hgo (rRrf) k Ef σ1) as [Hsafe Hstep];rewrite ?assoc;auto. edestruct (HR (r rf) (S k) (E Ef) σ1) as [s [Hvs Hws2]]; [omega|set_solver| |].
{ eapply wsat_change, Hws1; first by set_solver+.
rewrite assoc [rR _]comm. done. } clear Hws1 HR.
(* Take a step *)
destruct (Hgo (srf) k (E2 Ef) σ1) as [Hsafe Hstep]; [done|set_solver| |].
{ eapply wsat_change, Hws2; first by set_solver+.
rewrite !assoc [s _]comm. done. } clear Hgo.
split; [done|intros e2 σ2 ef ?]. split; [done|intros e2 σ2 ef ?].
destruct (Hstep e2 σ2 ef) as (r2&r2'&?&?&?); auto. destruct (Hstep e2 σ2 ef) as (r2&r2'&Hws3&?&?); auto. clear Hws2.
exists (r2 rR), r2'; split_and?; auto. (* Execute 2nd part of the view shift *)
- by rewrite -(assoc _ r2) (comm _ rR) !assoc -(assoc _ _ rR). edestruct (Hvs (r2 r2' rf) k (E Ef) σ2) as [t [HR Hws4]]; [omega|set_solver| |].
{ eapply wsat_change, Hws3; first by set_solver+.
rewrite !assoc [_ s]comm !assoc. done. } clear Hvs Hws3.
(* Execute the rest of e *)
exists (r2 t), r2'. split_and?; auto.
- eapply wsat_change, Hws4; first by set_solver+.
rewrite !assoc [_ t]comm. done.
- 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; [auto|uPred.unseal; exists r2, rR; split_and?; auto]. apply Hframe; first by auto. uPred.unseal; exists r2, t; split_and?; auto.
eapply uPred_weaken with n rR; eauto. move:(wp_mask_frame_mono). rewrite wp_eq=>Hmask.
eapply (Hmask E); by auto.
Qed. Qed.
Lemma wp_bind `{LanguageCtx Λ K} E e Φ : Lemma wp_bind `{LanguageCtx Λ K} E e Φ :
WP e @ E {{ v, WP K (of_val v) @ E {{ Φ }} }} WP K e @ E {{ Φ }}. WP e @ E {{ v, WP K (of_val v) @ E {{ Φ }} }} WP K e @ E {{ Φ }}.
...@@ -248,11 +262,26 @@ Lemma wp_value_pvs E Φ e v : ...@@ -248,11 +262,26 @@ Lemma wp_value_pvs E Φ e v :
Proof. intros. rewrite -wp_pvs. rewrite -wp_value //. Qed. Proof. intros. rewrite -wp_pvs. rewrite -wp_value //. Qed.
Lemma wp_frame_l E e Φ R : (R WP e @ E {{ Φ }}) WP e @ E {{ v, R Φ v }}. Lemma wp_frame_l E e Φ R : (R WP e @ E {{ Φ }}) WP e @ E {{ v, R Φ v }}.
Proof. setoid_rewrite (comm _ R); apply wp_frame_r. Qed. Proof. setoid_rewrite (comm _ R); apply wp_frame_r. Qed.
Lemma wp_frame_step_l E e Φ R : Lemma wp_frame_step_r' E e Φ R :
to_val e = None (WP e @ E {{ Φ }} R) WP e @ E {{ v, Φ v R }}.
Proof.
intros. rewrite {2}(_ : E = E ); last by set_solver.
rewrite -(wp_frame_step_r E ); [|auto|set_solver..].
apply sep_mono_r. rewrite -!pvs_intro. done.
Qed.
Lemma wp_frame_step_l E E1 E2 e Φ R :
to_val e = None E E1 E2 E1
((|={E1,E2}=> |={E2,E1}=> R) WP e @ E {{ Φ }})
WP e @ (E E1) {{ v, R Φ v }}.
Proof.
rewrite [((|={E1,E2}=> _) _)%I]comm; setoid_rewrite (comm _ R).
apply wp_frame_step_r.
Qed.
Lemma wp_frame_step_l' E e Φ R :
to_val e = None ( R WP e @ E {{ Φ }}) WP e @ E {{ v, R Φ v }}. to_val e = None ( R WP e @ E {{ Φ }}) WP e @ E {{ v, R Φ v }}.
Proof. Proof.
rewrite (comm _ ( R)%I); setoid_rewrite (comm _ R). rewrite (comm _ ( R)%I); setoid_rewrite (comm _ R).
apply wp_frame_step_r. apply wp_frame_step_r'.
Qed. Qed.
Lemma wp_always_l E e Φ R `{!PersistentP R} : Lemma wp_always_l E e Φ R `{!PersistentP R} :
(R WP e @ E {{ Φ }}) WP e @ E {{ v, R Φ v }}. (R WP e @ E {{ Φ }}) WP e @ E {{ v, R Φ v }}.
......
...@@ -44,6 +44,9 @@ Global Instance wsat_ne n : Proper (dist n ==> iff) (@wsat Λ Σ n E σ) | 1. ...@@ -44,6 +44,9 @@ 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 :
E1 = E2 r1 r2 wsat n E1 σ r1 wsat n E2 σ r2.
Proof. move=>->->. done. 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