Commit 655c9011 authored by Robbert Krebbers's avatar Robbert Krebbers

Make compile with last version of Iris.

parent 8156cf85
......@@ -205,12 +205,12 @@ Section lang_rules.
l {q1} v1 l {q2} v2 ⊣⊢ v1 = v2 l {q1+q2} v1.
Proof.
destruct (decide (v1 = v2)) as [->|].
{ by rewrite heap_mapsto_op_eq const_equiv // left_id. }
{ by rewrite heap_mapsto_op_eq pure_equiv // left_id. }
rewrite -auth_own_op op_singleton pair_op dec_agree_ne //.
apply (anti_symm ()); last by apply const_elim_l.
apply (anti_symm ()); last by apply pure_elim_l.
rewrite auth_own_valid gmap_validI (forall_elim l) lookup_singleton.
rewrite option_validI prod_validI frac_validI discrete_valid.
by apply const_elim_r.
by apply pure_elim_r.
Qed.
Lemma heap_mapsto_op_split l q v : (l {q} v)%I (l {q/2} v l {q/2} v)%I.
......@@ -231,8 +231,8 @@ Section lang_rules.
apply wand_intro_l.
rewrite always_and_sep_l -assoc -always_and_sep_l.
cbn; rewrite to_of_val.
apply const_elim_l=>-[l [-> [-Heq [-> ?]]]]; inversion Heq; subst.
by rewrite (forall_elim l) right_id const_equiv // left_id wand_elim_r.
apply pure_elim_l=>-[l [-> [-Heq [-> ?]]]]; inversion Heq; subst.
by rewrite (forall_elim l) right_id pure_equiv // left_id wand_elim_r.
cbn; rewrite H; eauto.
Qed.
......
......@@ -218,12 +218,12 @@ Section lang_rules.
l ↦ᵢ{q1} v1 l ↦ᵢ{q2} v2 ⊣⊢ v1 = v2 l ↦ᵢ{q1+q2} v1.
Proof.
destruct (decide (v1 = v2)) as [->|].
{ by rewrite heap_mapsto_op_eq const_equiv // left_id. }
{ by rewrite heap_mapsto_op_eq pure_equiv // left_id. }
rewrite -auth_own_op op_singleton pair_op dec_agree_ne //.
apply (anti_symm ()); last by apply const_elim_l.
apply (anti_symm ()); last by apply pure_elim_l.
rewrite auth_own_valid gmap_validI (forall_elim l) lookup_singleton.
rewrite option_validI prod_validI frac_validI discrete_valid.
by apply const_elim_r.
by apply pure_elim_r.
Qed.
Lemma heap_mapsto_dup_invalid l v1 v2 : l ↦ᵢ v1 l ↦ᵢ v2 False%I.
......@@ -246,15 +246,14 @@ Section lang_rules.
l, ef = @None expr
(to_val e') = (Some (LocV l)) σ' = <[l:=v]>σ σ !! l = None).
rewrite -(wp_lift_atomic_step (Alloc e) φ σ) // /φ;
last by intros; inv_step; eauto.
[|cbn; rewrite H; eauto|by intros; inv_step; eauto].
apply sep_mono, later_mono; first done.
apply forall_intro=>e2; apply forall_intro=>σ2; apply forall_intro=>ef.
apply wand_intro_l.
rewrite always_and_sep_l -assoc -always_and_sep_l.
cbn; rewrite to_of_val.
apply const_elim_l=>-[l [-> [-Heq [-> ?]]]]; inversion Heq; subst.
by rewrite (forall_elim l) right_id const_equiv // left_id wand_elim_r.
cbn; rewrite H; eauto.
apply pure_elim_l=>-[l [-> [-Heq [-> ?]]]]; inversion Heq; subst.
by rewrite (forall_elim l) right_id pure_equiv // left_id wand_elim_r.
Qed.
Lemma wp_load_pst E σ l v Φ :
......
......@@ -41,7 +41,7 @@ Section Soundness.
iAssert (@auth.auth_inv _ Σ _ _ γ (Spec_inv ([e'], )))
with "[Hcfg1]" as "Hinv".
{ iExists _; iFrame "Hcfg1".
apply const_intro. rewrite from_to_cfg; constructor.
iPureIntro. rewrite from_to_cfg; constructor.
}
iPvs (inv_alloc (nroot .@ "Fμ,ref,par" .@ 3) with "[Hinv]") as "#Hcfg";
trivial.
......@@ -66,7 +66,7 @@ Section Soundness.
iDestruct "Ha'" as {ρ'} "Ha'"; iDestruct "Ha'" as %Ha'.
rewrite ->(right_id _ _) in Ha'; setoid_subst.
iPvsIntro; iSplitL.
- iExists _. rewrite own_op. iDestruct "Hown" as "[Ho1 Ho2]".
- iDestruct "Hown" as "[Ho1 Ho2]". iExists _.
iSplitL; trivial.
- iPureIntro.
destruct ρ' as [th hp]; unfold op, cmra_op in *; simpl in *.
......
......@@ -4,4 +4,4 @@ This version is known to compile with:
- Coq 8.5pl1
- Ssreflect 1.6
- Iris dc6db28b
- Iris version https://gitlab.mpi-sws.org/FP/iris-coq/commit/b3d2ff9b
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