Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coq

CHANGELOG.md

@@ -17,13 +17,15 @@ Changes in and extensions of the theory:
 * [#] Add weakest preconditions for total program correctness.
 * [#] "(Potentially) stuck" weakest preconditions are no longer considered
   experimental.
+* [#] The adequacy statement for weakest preconditions now also involves the
+  final state.
 * [#] The Löb rule is now a derived rule; it follows from later-intro, later
   being contractive and the fact that we can take fixpoints of contractive
   functions.
 * [#] Add atomic updates and logically atomic triples, including tactic support.
   See `heap_lang/lib/increment.v` for an example.
-* [#] HeapLang now uses right-to-left evaluation order. This makes easier to
-  write specifications of curried functions.
+* [#] heap_lang now uses right-to-left evaluation order. This makes it
+  significantly easier to write specifications of curried functions.
 
 Changes in Coq:
 
@@ -76,6 +78,7 @@ Changes in Coq:
 * `namespaces` has been moved to std++.
 * Changed `IntoVal` to be directly usable for rewriting `e` into `of_val v`, and
   changed `AsVal` to be usable for rewriting via the `[v <-]` destruct pattern.
+* `wp_fork` is now written in curried form.
 
 ## Iris 3.1.0 (released 2017-12-19)
 

theories/algebra/cmra.v

@@ -1395,6 +1395,10 @@ Section option.
       by eapply (cmra_validN_le n); last lia.
     - done.
   Qed.
+
+  Global Instance option_cancelable (ma : option A) :
+    (∀ a : A, IdFree a) → (∀ a : A, Cancelable a) → Cancelable ma.
+  Proof. destruct ma; apply _. Qed.
 End option.
 
 Arguments optionR : clear implicits.

theories/algebra/gmap.v

@@ -288,6 +288,12 @@ Proof.
   - by rewrite lookup_singleton_ne // !(left_id None _).
 Qed.
 
+Global Instance gmap_cancelable (m : gmap K A) :
+  (∀ x : A, IdFree x) → (∀ x : A, Cancelable x) → Cancelable m.
+Proof.
+  intros ?? n m1 m2 ?? i. apply (cancelableN (m !! i)); by rewrite -!lookup_op.
+Qed.
+
 Lemma insert_op m1 m2 i x y :
   <[i:=x ⋅ y]>(m1 ⋅ m2) =  <[i:=x]>m1 ⋅ <[i:=y]>m2.
 Proof. by rewrite (insert_merge (⋅) m1 m2 i (x ⋅ y) x y). Qed.

theories/heap_lang/lang.v

@@ -4,6 +4,17 @@ From stdpp Require Export strings.
 From stdpp Require Import gmap.
 Set Default Proof Using "Type".
 
+(** heap_lang.  A fairly simple language used for common Iris examples.
+
+- This is a right-to-left evaluated language, like CakeML and OCaml.  The reason
+  for this is that it makes curried functions usable: Given a WP for [f a b], we
+  know that any effects [f] might have to not matter until after *both* [a] and
+  [b] are evaluated.  With left-to-right evaluation, that triple is basically
+  useless the user let-expands [b].
+
+*)
+
+
 Delimit Scope expr_scope with E.
 Delimit Scope val_scope with V.