Redo heap_lang/heap lemmas using proofmode.

heap_lang/heap.v

@@ -120,8 +120,7 @@ Section heap.
   Global Instance heap_mapsto_timeless l q v : TimelessP (l ↦{q} v).
   Proof. rewrite /heap_mapsto. apply _. Qed.
 
-  Lemma heap_mapsto_op_eq l q1 q2 v :
-    (l ↦{q1} v ★ l ↦{q2} v) ⊣⊢ (l ↦{q1+q2} v).
+  Lemma heap_mapsto_op_eq l q1 q2 v : (l ↦{q1} v ★ l ↦{q2} v) ⊣⊢ l ↦{q1+q2} v.
   Proof. by rewrite -auth_own_op op_singleton Frac_op dec_agree_idemp. Qed.
 
   Lemma heap_mapsto_op l q1 q2 v1 v2 :
@@ -135,8 +134,7 @@ Section heap.
     rewrite option_validI frac_validI discrete_valid. by apply const_elim_r.
   Qed.
 
-  Lemma heap_mapsto_op_split l q v :
-    (l ↦{q} v) ⊣⊢ (l ↦{q/2} v ★ l ↦{q/2} v).
+  Lemma heap_mapsto_op_split l q v : l ↦{q} v ⊣⊢ (l ↦{q/2} v ★ l ↦{q/2} v).
   Proof. by rewrite heap_mapsto_op_eq Qp_div_2. Qed.
 
   (** Weakest precondition *)
@@ -162,66 +160,57 @@ Section heap.
 
   Lemma wp_load N E l q v Φ :
     nclose N ⊆ E →
-    (heap_ctx N ★ ▷ l ↦{q} v ★ ▷ (l ↦{q} v -★ Φ v)) ⊢ WP Load (Lit (LitLoc l)) @ E {{ Φ }}.
+    (heap_ctx N ★ ▷ l ↦{q} v ★ ▷ (l ↦{q} v -★ Φ v))
+    ⊢ WP Load (Lit (LitLoc l)) @ E {{ Φ }}.
   Proof.
-    iIntros {?} "[#Hinv [Hmapsto HΦ]]". rewrite /heap_ctx /heap_mapsto.
+    iIntros {?} "[#Hh [Hl HΦ]]". rewrite /heap_ctx /heap_mapsto.
     apply (auth_fsa' heap_inv (wp_fsa _) id)
-      with N heap_name {[ l := Frac q (DecAgree v) ]}; simpl; eauto with I.
-    iFrame "Hmapsto". iIntros {h} "[% Hheap]". rewrite /heap_inv.
+      with N heap_name {[ l := Frac q (DecAgree v) ]}; simpl; eauto.
+    iFrame "Hl". iIntros {h} "[% Hl]". rewrite /heap_inv.
     iApply (wp_load_pst _ (<[l:=v]>(of_heap h)));first by rewrite lookup_insert.
-    rewrite of_heap_singleton_op //. iFrame "Hheap". iNext.
+    rewrite of_heap_singleton_op //. iFrame "Hl". iNext.
     iIntros "$". by iSplit.
   Qed.
 
-  Lemma wp_store N E l v' e v P Φ :
-    to_val e = Some v →
-    P ⊢ heap_ctx N → nclose N ⊆ E →
-    P ⊢ (▷ l ↦ v' ★ ▷ (l ↦ v -★ Φ (LitV LitUnit))) →
-    P ⊢ WP Store (Lit (LitLoc l)) e @ E {{ Φ }}.
+  Lemma wp_store N E l v' e v Φ :
+    to_val e = Some v → nclose N ⊆ E →
+    (heap_ctx N ★ ▷ l ↦ v' ★ ▷ (l ↦ v -★ Φ (LitV LitUnit)))
+    ⊢ WP Store (Lit (LitLoc l)) e @ E {{ Φ }}.
   Proof.
-    rewrite /heap_ctx /heap_inv=> ??? HPΦ.
+    iIntros {??} "[#Hh [Hl HΦ]]". rewrite /heap_ctx /heap_mapsto.
     apply (auth_fsa' heap_inv (wp_fsa _) (alter (λ _, Frac 1 (DecAgree v)) l))
       with N heap_name {[ l := Frac 1 (DecAgree v') ]}; simpl; eauto with I.
-    rewrite HPΦ{HPΦ}; apply sep_mono_r, forall_intro=> h; apply wand_intro_l.
-    rewrite -assoc; apply const_elim_sep_l=> ?.
-    rewrite -(wp_store_pst _ (<[l:=v']>(of_heap h))) ?lookup_insert //.
-    rewrite /heap_inv alter_singleton insert_insert !of_heap_singleton_op; eauto.
-    rewrite const_equiv; last naive_solver.
-    apply sep_mono_r, later_mono, wand_intro_l. by rewrite left_id -later_intro.
+    iFrame "Hl". iIntros {h} "[% Hl]". rewrite /heap_inv.
+    iApply (wp_store_pst _ (<[l:=v']>(of_heap h))); rewrite ?lookup_insert //.
+    rewrite alter_singleton insert_insert !of_heap_singleton_op; eauto.
+    iFrame "Hl". iNext. iIntros "$". iFrame "HΦ". iPureIntro; naive_solver.
   Qed.
 
-  Lemma wp_cas_fail N E l q v' e1 v1 e2 v2 P Φ :
-    to_val e1 = Some v1 → to_val e2 = Some v2 → v' ≠ v1 →
-    P ⊢ heap_ctx N → nclose N ⊆ E →
-    P ⊢ (▷ l ↦{q} v' ★ ▷ (l ↦{q} v' -★ Φ (LitV (LitBool false)))) →
-    P ⊢ WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
+  Lemma wp_cas_fail N E l q v' e1 v1 e2 v2 Φ :
+    to_val e1 = Some v1 → to_val e2 = Some v2 → v' ≠ v1 → nclose N ⊆ E →
+    (heap_ctx N ★ ▷ l ↦{q} v' ★ ▷ (l ↦{q} v' -★ Φ (LitV (LitBool false))))
+    ⊢ WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
   Proof.
-    rewrite /heap_ctx /heap_inv=>????? HPΦ.
+    iIntros {????} "[#Hh [Hl HΦ]]". rewrite /heap_ctx /heap_mapsto.
     apply (auth_fsa' heap_inv (wp_fsa _) id)
-      with N heap_name {[ l := Frac q (DecAgree v') ]}; simpl; eauto 10 with I.
-    rewrite HPΦ{HPΦ}; apply sep_mono_r, forall_intro=> h; apply wand_intro_l.
-    rewrite -assoc; apply const_elim_sep_l=> ?.
-    rewrite -(wp_cas_fail_pst _ (<[l:=v']>(of_heap h))) ?lookup_insert //.
-    rewrite const_equiv // left_id.
-    rewrite /heap_inv !of_heap_singleton_op //.
-    apply sep_mono_r, later_mono, wand_intro_l. by rewrite -later_intro.
+      with N heap_name {[ l := Frac q (DecAgree v') ]}; simpl; eauto 10.
+    iFrame "Hl". iIntros {h} "[% Hl]". rewrite /heap_inv.
+    iApply (wp_cas_fail_pst _ (<[l:=v']>(of_heap h))); rewrite ?lookup_insert //.
+    rewrite of_heap_singleton_op //. iFrame "Hl". iNext.
+    iIntros "$". by iSplit.
   Qed.
 
-  Lemma wp_cas_suc N E l e1 v1 e2 v2 P Φ :
-    to_val e1 = Some v1 → to_val e2 = Some v2 →
-    P ⊢ heap_ctx N → nclose N ⊆ E →
-    P ⊢ (▷ l ↦ v1 ★ ▷ (l ↦ v2 -★ Φ (LitV (LitBool true)))) →
-    P ⊢ WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
+  Lemma wp_cas_suc N E l e1 v1 e2 v2 Φ :
+    to_val e1 = Some v1 → to_val e2 = Some v2 → nclose N ⊆ E →
+    (heap_ctx N ★ ▷ l ↦ v1 ★ ▷ (l ↦ v2 -★ Φ (LitV (LitBool true))))
+    ⊢ WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
   Proof.
-    rewrite /heap_ctx /heap_inv=> ???? HPΦ.
+    iIntros {???} "[#Hh [Hl HΦ]]". rewrite /heap_ctx /heap_mapsto.
     apply (auth_fsa' heap_inv (wp_fsa _) (alter (λ _, Frac 1 (DecAgree v2)) l))
-      with N heap_name {[ l := Frac 1 (DecAgree v1) ]}; simpl; eauto 10 with I.
-    rewrite HPΦ{HPΦ}; apply sep_mono_r, forall_intro=> h; apply wand_intro_l.
-    rewrite -assoc; apply const_elim_sep_l=> ?.
-    rewrite -(wp_cas_suc_pst _ (<[l:=v1]>(of_heap h))) //;
-      last by rewrite lookup_insert.
-    rewrite /heap_inv alter_singleton insert_insert !of_heap_singleton_op; eauto.
-    rewrite lookup_insert const_equiv; last naive_solver.
-    apply sep_mono_r, later_mono, wand_intro_l. by rewrite left_id -later_intro.
+      with N heap_name {[ l := Frac 1 (DecAgree v1) ]}; simpl; eauto 10.
+    iFrame "Hl". iIntros {h} "[% Hl]". rewrite /heap_inv.
+    iApply (wp_cas_suc_pst _ (<[l:=v1]>(of_heap h))); rewrite ?lookup_insert //.
+    rewrite alter_singleton insert_insert !of_heap_singleton_op; eauto.
+    iFrame "Hl". iNext. iIntros "$". iFrame "HΦ". iPureIntro; naive_solver.
   Qed.
 End heap.

heap_lang/proofmode.v

@@ -52,7 +52,7 @@ Lemma tac_wp_store Δ Δ' Δ'' N E i l v e v' Φ :
   envs_simple_replace i false (Esnoc Enil i (l ↦ v')) Δ' = Some Δ'' →
   Δ'' ⊢ Φ (LitV LitUnit) → Δ ⊢ WP Store (Lit (LitLoc l)) e @ E {{ Φ }}.
 Proof.
-  intros. eapply wp_store; eauto.
+  intros. rewrite -wp_store // -always_and_sep_l. apply and_intro; first done.
   rewrite strip_later_env_sound -later_sep envs_simple_replace_sound //; simpl.
   rewrite right_id. by apply later_mono, sep_mono_r, wand_mono.
 Qed.
@@ -65,7 +65,7 @@ Lemma tac_wp_cas_fail Δ Δ' N E i l q v e1 v1 e2 v2 Φ :
   Δ' ⊢ Φ (LitV (LitBool false)) →
   Δ ⊢ WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
 Proof.
-  intros. eapply wp_cas_fail; eauto.
+  intros. rewrite -wp_cas_fail // -always_and_sep_l. apply and_intro; first done.
   rewrite strip_later_env_sound -later_sep envs_lookup_split //; simpl.
   by apply later_mono, sep_mono_r, wand_mono.
 Qed.
@@ -78,7 +78,7 @@ Lemma tac_wp_cas_suc Δ Δ' Δ'' N E i l e1 v1 e2 v2 Φ :
   envs_simple_replace i false (Esnoc Enil i (l ↦ v2)) Δ' = Some Δ'' →
   Δ'' ⊢ Φ (LitV (LitBool true)) → Δ ⊢ WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
 Proof.
-  intros. eapply wp_cas_suc; eauto.
+  intros. rewrite -wp_cas_suc // -always_and_sep_l. apply and_intro; first done.
   rewrite strip_later_env_sound -later_sep envs_simple_replace_sound //; simpl.
   rewrite right_id. by apply later_mono, sep_mono_r, wand_mono.
 Qed.