Commit a1171d02 by Robbert Krebbers

### Use simpl more to get rid of %V scopes following 6d038c53.

parent 24be0361
Pipeline #2648 passed with stage
in 9 minutes and 4 seconds
 ... @@ -94,7 +94,7 @@ Lemma newcounter_spec N : ... @@ -94,7 +94,7 @@ Lemma newcounter_spec N : heapN ⊥ N → heapN ⊥ N → heap_ctx ⊢ {{ True }} newcounter #() {{ v, ∃ l, v = #l ∧ C l 0 }}. heap_ctx ⊢ {{ True }} newcounter #() {{ v, ∃ l, v = #l ∧ C l 0 }}. Proof. Proof. iIntros (?) "#Hh !# _ /=". rewrite /newcounter. wp_seq. wp_alloc l as "Hl". iIntros (?) "#Hh !# _ /=". rewrite /newcounter /=. wp_seq. wp_alloc l as "Hl". iVs (own_alloc (Auth 0)) as (γ) "Hγ"; first done. iVs (own_alloc (Auth 0)) as (γ) "Hγ"; first done. rewrite (auth_frag_op 0 0) //; iDestruct "Hγ" as "[Hγ Hγf]". rewrite (auth_frag_op 0 0) //; iDestruct "Hγ" as "[Hγ Hγf]". iVs (inv_alloc N _ (I γ l) with "[Hl Hγ]") as "#?". iVs (inv_alloc N _ (I γ l) with "[Hl Hγ]") as "#?". ... @@ -128,7 +128,7 @@ Lemma read_spec l n : ... @@ -128,7 +128,7 @@ Lemma read_spec l n : {{ C l n }} read #l {{ v, ∃ m : nat, ■ (v = #m ∧ n ≤ m) ∧ C l m }}. {{ C l n }} read #l {{ v, ∃ m : nat, ■ (v = #m ∧ n ≤ m) ∧ C l m }}. Proof. Proof. iIntros "!# Hl /=". iDestruct "Hl" as (N γ) "(% & #Hh & #Hinv & Hγf)". iIntros "!# Hl /=". iDestruct "Hl" as (N γ) "(% & #Hh & #Hinv & Hγf)". rewrite /read. wp_let. iInv N as (c) "[Hl Hγ]" "Hclose". wp_load. rewrite /read /=. wp_let. iInv N as (c) "[Hl Hγ]" "Hclose". wp_load. iDestruct (own_valid γ (Frag n ⋅ Auth c) with "[#]") as % ?%auth_frag_valid. iDestruct (own_valid γ (Frag n ⋅ Auth c) with "[#]") as % ?%auth_frag_valid. { iApply own_op. by iFrame. } { iApply own_op. by iFrame. } rewrite (auth_frag_op c c); last lia; iDestruct "Hγ" as "[Hγ Hγf']". rewrite (auth_frag_op c c); last lia; iDestruct "Hγ" as "[Hγ Hγf']". ... ...
 ... @@ -42,7 +42,7 @@ Lemma wp_one_shot (Φ : val → iProp Σ) : ... @@ -42,7 +42,7 @@ Lemma wp_one_shot (Φ : val → iProp Σ) : ⊢ WP one_shot_example #() {{ Φ }}. ⊢ WP one_shot_example #() {{ Φ }}. Proof. Proof. iIntros "[#? Hf] /=". iIntros "[#? Hf] /=". rewrite /one_shot_example. wp_seq. wp_alloc l as "Hl". wp_let. rewrite /one_shot_example /=. wp_seq. wp_alloc l as "Hl". wp_let. iVs (own_alloc Pending) as (γ) "Hγ"; first done. iVs (own_alloc Pending) as (γ) "Hγ"; first done. iVs (inv_alloc N _ (one_shot_inv γ l) with "[Hl Hγ]") as "#HN". iVs (inv_alloc N _ (one_shot_inv γ l) with "[Hl Hγ]") as "#HN". { iNext. iLeft. by iSplitL "Hl". } { iNext. iLeft. by iSplitL "Hl". } ... ...
 ... @@ -60,7 +60,7 @@ Lemma sum_wp `{!heapG Σ} v t Φ : ... @@ -60,7 +60,7 @@ Lemma sum_wp `{!heapG Σ} v t Φ : heap_ctx ★ is_tree v t ★ (is_tree v t -★ Φ #(sum t)) heap_ctx ★ is_tree v t ★ (is_tree v t -★ Φ #(sum t)) ⊢ WP sum' v {{ Φ }}. ⊢ WP sum' v {{ Φ }}. Proof. Proof. iIntros "(#Hh & Ht & HΦ)". rewrite /sum'. iIntros "(#Hh & Ht & HΦ)". rewrite /sum' /=. wp_let. wp_alloc l as "Hl". wp_let. wp_let. wp_alloc l as "Hl". wp_let. wp_apply sum_loop_wp; iFrame "Hh Ht Hl". wp_apply sum_loop_wp; iFrame "Hh Ht Hl". rewrite Z.add_0_r. rewrite Z.add_0_r. ... ...
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!