Commit 6b5ee4fa by Jacques-Henri Jourdan

### Lifting lemmas : get rid of \phi when it has became useless

parent 76a7d9a2
 ... @@ -18,19 +18,17 @@ Lemma wp_ectx_bind {E e} K Φ : ... @@ -18,19 +18,17 @@ Lemma wp_ectx_bind {E e} K Φ : WP e @ E {{ v, WP fill K (of_val v) @ E {{ Φ }} }} ⊢ WP fill K e @ E {{ Φ }}. WP e @ E {{ v, WP fill K (of_val v) @ E {{ Φ }} }} ⊢ WP fill K e @ E {{ Φ }}. Proof. apply: weakestpre.wp_bind. Qed. Proof. apply: weakestpre.wp_bind. Qed. Lemma wp_lift_head_step E1 E2 Lemma wp_lift_head_step E1 E2 Φ e1 : (φ : expr → state → option expr → Prop) Φ e1 : E2 ⊆ E1 → to_val e1 = None → E2 ⊆ E1 → to_val e1 = None → (|={E1,E2}=> ∃ σ1, (|={E1,E2}=> ∃ σ1, ■ head_reducible e1 σ1 ∧ ■ head_reducible e1 σ1 ∧ ▷ ownP σ1 ★ ▷ ∀ e2 σ2 ef, (■ head_step e1 σ1 e2 σ2 ef ∧ ownP σ2) ■ (∀ e2 σ2 ef, head_step e1 σ1 e2 σ2 ef → φ e2 σ2 ef) ∧ ={E2,E1}=★ WP e2 @ E1 {{ Φ }} ★ wp_fork ef) ▷ ownP σ1 ★ ▷ ∀ e2 σ2 ef, (■ φ e2 σ2 ef ∧ ownP σ2) ={E2,E1}=★ WP e2 @ E1 {{ Φ }} ★ wp_fork ef) ⊢ WP e1 @ E1 {{ Φ }}. ⊢ WP e1 @ E1 {{ Φ }}. Proof. Proof. iIntros {??} "H". iApply (wp_lift_step E1 E2 φ); try done. iIntros {??} "H". iApply (wp_lift_step E1 E2); try done. iPvs "H" as {σ1} "(%&%&Hσ1&?)". set_solver. iPvsIntro. iExists σ1. iPvs "H" as {σ1} "(%&Hσ1&Hwp)". set_solver. iPvsIntro. iExists σ1. repeat iSplit; eauto. by iFrame. iSplit; first by eauto. iFrame. iNext. iIntros {e2 σ2 ef} "[% ?]". iApply "Hwp". by eauto. Qed. Qed. Lemma wp_lift_pure_head_step E (φ : expr → option expr → Prop) Φ e1 : Lemma wp_lift_pure_head_step E (φ : expr → option expr → Prop) Φ e1 : ... ...
 ... @@ -18,24 +18,22 @@ Implicit Types e : expr Λ. ... @@ -18,24 +18,22 @@ Implicit Types e : expr Λ. Implicit Types P Q R : iProp Λ Σ. Implicit Types P Q R : iProp Λ Σ. Implicit Types Ψ : val Λ → iProp Λ Σ. Implicit Types Ψ : val Λ → iProp Λ Σ. Lemma ht_lift_step E1 E2 Lemma ht_lift_step E1 E2 P Pσ1 Φ1 Φ2 Ψ e1 : (φ : expr Λ → state Λ → option (expr Λ) → Prop) P P' Φ1 Φ2 Ψ e1 : E2 ⊆ E1 → to_val e1 = None → E2 ⊆ E1 → to_val e1 = None → (P ={E1,E2}=> ∃ σ1, (P ={E1,E2}=> ∃ σ1, ■ reducible e1 σ1 ∧ ■ reducible e1 σ1 ∧ ▷ ownP σ1 ★ ▷ Pσ1 σ1) ∧ ■ (∀ e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef → φ e2 σ2 ef) ∧ (∀ σ1 e2 σ2 ef, ■ prim_step e1 σ1 e2 σ2 ef ★ ownP σ2 ★ Pσ1 σ1 ▷ ownP σ1 ★ ▷ P') ∧ ={E2,E1}=> Φ1 e2 σ2 ef ★ Φ2 e2 σ2 ef) ∧ (∀ e2 σ2 ef, ■ φ e2 σ2 ef ★ ownP σ2 ★ P' ={E2,E1}=> Φ1 e2 σ2 ef ★ Φ2 e2 σ2 ef) ∧ (∀ e2 σ2 ef, {{ Φ1 e2 σ2 ef }} e2 @ E1 {{ Ψ }}) ∧ (∀ e2 σ2 ef, {{ Φ1 e2 σ2 ef }} e2 @ E1 {{ Ψ }}) ∧ (∀ e2 σ2 ef, {{ Φ2 e2 σ2 ef }} ef ?@ ⊤ {{ _, True }}) (∀ e2 σ2 ef, {{ Φ2 e2 σ2 ef }} ef ?@ ⊤ {{ _, True }}) ⊢ {{ P }} e1 @ E1 {{ Ψ }}. ⊢ {{ P }} e1 @ E1 {{ Ψ }}. Proof. Proof. iIntros {??} "#(#Hvs&HΦ&He2&Hef) ! HP". iIntros {??} "#(#Hvs&HΦ&He2&Hef) ! HP". iApply (wp_lift_step E1 E2 φ _ e1); auto. iApply (wp_lift_step E1 E2 _ e1); auto. iPvs ("Hvs" with "HP") as {σ1} "(%&%&Hσ&HP)"; first set_solver. iPvs ("Hvs" with "HP") as {σ1} "(%&Hσ&HP)"; first set_solver. iPvsIntro. iExists σ1. repeat iSplit; eauto. iFrame. iPvsIntro. iExists σ1. repeat iSplit. by eauto. iFrame. iNext. iIntros {e2 σ2 ef} "[#Hφ Hown]". iNext. iIntros {e2 σ2 ef} "[#Hφ Hown]". iSpecialize ("HΦ" $! e2 σ2 ef with "[-]"). by iFrame "Hφ HP Hown". iSpecialize ("HΦ"$! σ1 e2 σ2 ef with "[-]"). by iFrame "Hφ HP Hown". iPvs "HΦ" as "[H1 H2]"; first by set_solver. iPvsIntro. iSplitL "H1". iPvs "HΦ" as "[H1 H2]"; first by set_solver. iPvsIntro. iSplitL "H1". - by iApply "He2". - by iApply "He2". - destruct ef as [e|]; last done. by iApply ("Hef" $! _ _ (Some e)). - destruct ef as [e|]; last done. by iApply ("Hef"$! _ _ (Some e)). ... @@ -50,15 +48,15 @@ Lemma ht_lift_atomic_step ... @@ -50,15 +48,15 @@ Lemma ht_lift_atomic_step {{ ▷ ownP σ1 ★ ▷ P }} e1 @ E {{ v, ∃ σ2 ef, ownP σ2 ★ ■ φ (of_val v) σ2 ef }}. {{ ▷ ownP σ1 ★ ▷ P }} e1 @ E {{ v, ∃ σ2 ef, ownP σ2 ★ ■ φ (of_val v) σ2 ef }}. Proof. Proof. iIntros {? Hsafe Hstep} "#Hef". iIntros {? Hsafe Hstep} "#Hef". set (φ' e σ ef := is_Some (to_val e) ∧ φ e σ ef). set (φ' (_:state Λ) e σ ef := is_Some (to_val e) ∧ φ e σ ef). iApply (ht_lift_step E E φ' _ P iApply (ht_lift_step E E _ (λ σ1', P ∧ σ1 = σ1')%I (λ e2 σ2 ef, ownP σ2 ★ ■ (φ' e2 σ2 ef))%I (λ e2 σ2 ef, ■ φ e2 σ2 ef ★ P)%I); (λ e2 σ2 ef, ownP σ2 ★ ■ (φ' σ1 e2 σ2 ef))%I (λ e2 σ2 ef, ■ φ e2 σ2 ef ★ P)%I); try by (eauto using atomic_not_val). try by (eauto using atomic_not_val). repeat iSplit. repeat iSplit. - iIntros "![Hσ1 HP]". iExists σ1. iPvsIntro. unfold φ'. - iIntros "![Hσ1 HP]". iExists σ1. iPvsIntro. repeat iSplit; eauto using atomic_step. by iFrame. iSplit. by eauto using atomic_step. iFrame. by auto. - iIntros {e2 σ2 ef} "! (#Hφ&Hown&HP)"; iPvsIntro. - iIntros {? e2 σ2 ef} "! (%&Hown&HP&%)". iPvsIntro. subst. iSplitL "Hown". by iSplit. iSplit. by iDestruct "Hφ" as %[_ ?]. done. iFrame. iSplit; iPureIntro; auto. split; eauto using atomic_step. - iIntros {e2 σ2 ef} "! [Hown #Hφ]"; iDestruct "Hφ" as %[[v2 <-%of_to_val] ?]. - iIntros {e2 σ2 ef} "! [Hown #Hφ]"; iDestruct "Hφ" as %[[v2 <-%of_to_val] ?]. iApply wp_value'. iExists σ2, ef. by iSplit. iApply wp_value'. iExists σ2, ef. by iSplit. - done. - done. ... ...
 ... @@ -18,19 +18,16 @@ Implicit Types Φ : val Λ → iProp Λ Σ. ... @@ -18,19 +18,16 @@ Implicit Types Φ : val Λ → iProp Λ Σ. Notation wp_fork ef := (default True ef (flip (wp ⊤) (λ _, True)))%I. Notation wp_fork ef := (default True ef (flip (wp ⊤) (λ _, True)))%I. Lemma wp_lift_step E1 E2 Lemma wp_lift_step E1 E2 Φ e1 : (φ : expr Λ → state Λ → option (expr Λ) → Prop) Φ e1 : E2 ⊆ E1 → to_val e1 = None → E2 ⊆ E1 → to_val e1 = None → (|={E1,E2}=> ∃ σ1, (|={E1,E2}=> ∃ σ1, ■ reducible e1 σ1 ∧ ▷ ownP σ1 ★ ■ reducible e1 σ1 ∧ ▷ ∀ e2 σ2 ef, (■ prim_step e1 σ1 e2 σ2 ef ∧ ownP σ2) ■ (∀ e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef → φ e2 σ2 ef) ∧ ={E2,E1}=★ WP e2 @ E1 {{ Φ }} ★ wp_fork ef) ▷ ownP σ1 ★ ▷ ∀ e2 σ2 ef, (■ φ e2 σ2 ef ∧ ownP σ2) ={E2,E1}=★ WP e2 @ E1 {{ Φ }} ★ wp_fork ef) ⊢ WP e1 @ E1 {{ Φ }}. ⊢ WP e1 @ E1 {{ Φ }}. Proof. Proof. intros ? He. rewrite pvs_eq wp_eq. intros ? He. rewrite pvs_eq wp_eq. uPred.unseal; split=> n r ? Hvs; constructor; auto. intros k Ef σ1' rf ???. uPred.unseal; split=> n r ? Hvs; constructor; auto. intros k Ef σ1' rf ???. destruct (Hvs (S k) Ef σ1' rf) as (r'&(σ1&Hsafe&Hstep&r1&r2&?&?&Hwp)&Hws); destruct (Hvs (S k) Ef σ1' rf) as (r'&(σ1&Hsafe&r1&r2&?&?&Hwp)&Hws); auto; clear Hvs; cofe_subst r'. auto; clear Hvs; cofe_subst r'. destruct (wsat_update_pst k (E2 ∪ Ef) σ1 σ1' r1 (r2 ⋅ rf)) as [-> Hws']. destruct (wsat_update_pst k (E2 ∪ Ef) σ1 σ1' r1 (r2 ⋅ rf)) as [-> Hws']. { apply equiv_dist. rewrite -(ownP_spec k); auto. } { apply equiv_dist. rewrite -(ownP_spec k); auto. } ... @@ -38,7 +35,7 @@ Proof. ... @@ -38,7 +35,7 @@ Proof. constructor; [done|intros e2 σ2 ef ?; specialize (Hws' σ2)]. constructor; [done|intros e2 σ2 ef ?; specialize (Hws' σ2)]. destruct (λ H1 H2 H3, Hwp e2 σ2 ef k (update_pst σ2 r1) H1 H2 H3 k Ef σ2 rf) destruct (λ H1 H2 H3, Hwp e2 σ2 ef k (update_pst σ2 r1) H1 H2 H3 k Ef σ2 rf) as (r'&(r1'&r2'&?&?&?)&?); auto; cofe_subst r'. as (r'&(r1'&r2'&?&?&?)&?); auto; cofe_subst r'. { split. by eapply Hstep. apply ownP_spec; auto. } { split. done. apply ownP_spec; auto. } { rewrite (comm _ r2) -assoc; eauto using wsat_le. } { rewrite (comm _ r2) -assoc; eauto using wsat_le. } exists r1', r2'; split_and?; try done. by uPred.unseal; intros ? ->. exists r1', r2'; split_and?; try done. by uPred.unseal; intros ? ->. Qed. Qed. ... @@ -71,11 +68,10 @@ Lemma wp_lift_atomic_step {E Φ} e1 ... @@ -71,11 +68,10 @@ Lemma wp_lift_atomic_step {E Φ} e1 ■ φ (of_val v2) σ2 ef ∧ ownP σ2 -★ (|={E}=> Φ v2) ★ wp_fork ef) ■ φ (of_val v2) σ2 ef ∧ ownP σ2 -★ (|={E}=> Φ v2) ★ wp_fork ef) ⊢ WP e1 @ E {{ Φ }}. ⊢ WP e1 @ E {{ Φ }}. Proof. Proof. iIntros {???} "[Hσ1 Hwp]". iApply (wp_lift_step E E (λ e2 σ2 ef, iIntros {???} "[Hσ1 Hwp]". iApply (wp_lift_step E E _ e1); auto using atomic_not_val. is_Some (to_val e2) ∧ φ e2 σ2 ef) _ e1); auto using atomic_not_val. iPvsIntro. iExists σ1. repeat iSplit; eauto 10 using atomic_step. iApply pvs_intro. iExists σ1. repeat iSplit; eauto using atomic_step. iFrame. iNext. iIntros {e2 σ2 ef} "[% Hσ2]". iFrame. iNext. iIntros {e2 σ2 ef} "[#He2 Hσ2]". edestruct @atomic_step as [v2 Hv%of_to_val]; eauto. subst e2. iDestruct "He2" as %[[v2 Hv%of_to_val]?]. subst e2. iDestruct ("Hwp" $! v2 σ2 ef with "[Hσ2]") as "[HΦ ?]". by eauto. iDestruct ("Hwp"$! v2 σ2 ef with "[Hσ2]") as "[HΦ ?]". by eauto. iFrame. iPvs "HΦ". iPvsIntro. iApply wp_value; auto using to_of_val. iFrame. iPvs "HΦ". iPvsIntro. iApply wp_value; auto using to_of_val. Qed. Qed. ... ...
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