Merge branch 'master' into gen_proofmode

opam

@@ -11,5 +11,5 @@ install: [make "install"]
 remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris"]
 depends: [
   "coq" { (>= "8.7.1" & < "8.9~") | (= "dev") }
-  "coq-stdpp" { (= "dev.2018-04-27.1.32c8182a") | (= "dev") }
+  "coq-stdpp" { (= "dev.2018-05-14.0.8fdeb77f") | (= "dev") }
 ]

theories/algebra/frac_auth.v

@@ -105,4 +105,17 @@ Section frac_auth.
   Proof.
     intros. by apply auth_update, option_local_update, prod_local_update_2.
   Qed.
+
+  Lemma frac_auth_update_alloc q a b c :
+    (∀ n : nat, ✓{n} a → ✓{n} (c ⋅ a)) →
+    ●! a ⋅ ◯!{q} b ~~> ●! (c ⋅ a) ⋅ ◯!{q} (c ⋅ b).
+  Proof. intros ?. by apply frac_auth_update, op_local_update. Qed.
+
+  Lemma frac_auth_dealloc q a b c `{!Cancelable c} :
+    ●! (c ⋅ a) ⋅ ◯!{q} (c ⋅ b) ~~> ●! a ⋅ ◯!{q} b.
+  Proof.
+    apply frac_auth_update.
+    move=> n [x|] /= Hvalid Heq; split; eauto using cmra_validN_op_r.
+    eapply (cancelableN c); by rewrite ?assoc.
+  Qed.
 End frac_auth.

theories/algebra/gmultiset.v

@@ -50,6 +50,11 @@ Section gmultiset.
   Proof. split. done. intros X. by rewrite gmultiset_op_union left_id_L. done. Qed.
   Canonical Structure gmultisetUR := UcmraT (gmultiset K) gmultiset_ucmra_mixin.
 
+  Global Instance gmultiset_cancelable X : Cancelable X.
+  Proof.
+    apply: discrete_cancelable=> Y Z _ ?. fold_leibniz. by apply (inj (X ∪)).
+  Qed.
+
   Lemma gmultiset_opM X mY : X ⋅? mY = X ∪ from_option id ∅ mY.
   Proof. destruct mY; by rewrite /= ?right_id_L. Qed.
 
@@ -71,7 +76,6 @@ Section gmultiset.
     repeat (rewrite multiplicity_difference || rewrite multiplicity_union).
     omega.
   Qed.
-
 End gmultiset.
 
 Arguments gmultisetC _ {_ _}.

theories/program_logic/ectx_language.v

@@ -101,7 +101,7 @@ Section ectx_language.
   Definition head_irreducible (e : expr Λ) (σ : state Λ) :=
     ∀ e' σ' efs, ¬head_step e σ e' σ' efs.
   Definition head_stuck (e : expr Λ) (σ : state Λ) :=
-    to_val e = None ∧ ∀ K e', e = fill K e' → head_irreducible e' σ.
+    to_val e = None ∧ head_irreducible e σ.
 
   (* All non-value redexes are at the root.  In other words, all sub-redexes are
      values. *)
@@ -168,9 +168,8 @@ Section ectx_language.
   Lemma head_stuck_stuck e σ :
     head_stuck e σ → sub_redexes_are_values e → stuck e σ.
   Proof.
-    move=>[] ? Hirr ?. split; first done.
-    apply prim_head_irreducible; last done.
-    apply (Hirr empty_ectx). by rewrite fill_empty.
+    intros [] ?. split; first done.
+    by apply prim_head_irreducible.
   Qed.
 
   Lemma ectx_language_atomic a e :