Commit 59ae6b91 by Robbert Krebbers

### Remove a FIXME in barrier.lifting.

```Remarks:
* eauto needs more fuel to automatically solve the side-conditions.
* ssreflect rewrite works if we do a set (φ ..) first. No idea why.```
parent 9b141597
 ... @@ -21,21 +21,14 @@ Lemma wp_alloc_pst E σ e v Q : ... @@ -21,21 +21,14 @@ Lemma wp_alloc_pst E σ e v Q : (ownP σ ★ ▷ (∀ l, ■(σ !! l = None) ∧ ownP (<[l:=v]>σ) -★ Q (LocV l))) (ownP σ ★ ▷ (∀ l, ■(σ !! l = None) ∧ ownP (<[l:=v]>σ) -★ Q (LocV l))) ⊑ wp E (Alloc e) Q. ⊑ wp E (Alloc e) Q. Proof. Proof. intros. intros. set (φ v' σ' := ∃ l, v' = LocV l ∧ σ' = <[l:=v]>σ ∧ σ !! l = None). (* FIXME RJ: ssreflect rewrite does not work. *) rewrite -(wp_lift_atomic_step (Alloc e) φ σ) // /φ; rewrite <-(wp_lift_atomic_step (Alloc e) last by intros; inv_step; eauto 10. (λ v' σ', ∃ l, v' = LocV l ∧ σ' = <[l:=v]>σ ∧ σ !! l = None) σ)=> //; last first. { (* TODO RJ: Somehow automation used to kill all this...?? *) intros. inv_step. eexists; split_ands; try done; []. eexists; done. } apply sep_mono, later_mono; first done. apply sep_mono, later_mono; first done. apply forall_intro=>e2; apply forall_intro=>σ2. apply forall_intro=>e2; apply forall_intro=>σ2; apply wand_intro_l. apply wand_intro_l. rewrite always_and_sep_l' -associative -always_and_sep_l'. rewrite always_and_sep_l' -associative -always_and_sep_l'. apply const_elim_l=>-[l [-> [-> ?]]]. apply const_elim_l=>-[l [-> [-> ?]]]. rewrite (forall_elim l) const_equiv //. by rewrite (forall_elim l) const_equiv // left_id wand_elim_r. by rewrite left_id wand_elim_r. Qed. Qed. Lemma wp_load_pst E σ l v Q : Lemma wp_load_pst E σ l v Q : ... ...
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!