Merge commit '38b6' into gen_proofmode

CHANGELOG.md

@@ -9,16 +9,16 @@ Changes in and extensions of the theory:
 
 * [#] Add new modality: ■ ("plainly").
 * [#] Camera morphisms have to be homomorphisms, not just monotone functions.
-* [#] A proof that `f` has a fixed point if `f^k` is contractive.
+* Add a proof that `f` has a fixed point if `f^k` is contractive.
 * Constructions for least and greatest fixed points over monotone predicates
   (defined in the logic of Iris using impredicative quantification).
-* A proof of the inverse of `wp_bind`.
+* Add a proof of the inverse of `wp_bind`.
 
 Changes in Coq:
 
-* Some things got renamed and notation changed:
+* Rename some things and change notation:
   - The unit of a camera: `empty` -> `unit`, `∅` -> `ε`
-  - The proof mode type class `IntoOp` -> `IsOp`
+  - A proof mode type class `IntoOp` -> `IsOp`
   - OFEs with all elements being discrete: `Discrete` -> `OfeDiscrete`
   - OFE elements whose equality is discrete: `Timeless` -> `Discrete`
   - Timeless propositions: `TimelessP` -> `Timeless`
@@ -36,7 +36,8 @@ Changes in Coq:
     + `DRAMixin` -> `DraMixin`
     + `DRAT` -> `DraT`
     + `STS` -> `Sts`
-  - Many lemmas also changed their name.  A partial list:
+  - Many lemmas also changed their name.  `always_*` became `persistently_*`,
+    and furthermore: (the following list is not complete)
     + `impl_wand` -> `impl_wand_1` (it only involves one direction of the
       equivalent)
     + `always_impl_wand` -> `impl_wand`
@@ -49,7 +50,7 @@ Changes in Coq:
       direction of this equivalence got swapped for consistency's sake)
   The following `sed` snippet should get you most of the way:
 ```
-sed 's/\bPersistentP\b/Persistent/g; s/\bTimelessP\b/Timeless/g; s/\bCMRADiscrete\b/CmraDiscrete/g; s/\bSTS\b/Sts/g' -i $(find -name "*.v")
+sed 's/\bPersistentP\b/Persistent/g; s/\bTimelessP\b/Timeless/g; s/\bCMRADiscrete\b/CmraDiscrete/g; s/\bCMRAT\b/CmraT/g; s/\bCMRAMixin\b/CmraMixin/g; s/\bUCMRAT\b/UcmraT/g; s/\bUCMRAMixin\b/UcmraMixin/g; s/\bSTS\b/Sts/g' -i $(find -name "*.v")
 ```
 * Fix a bunch of consistency issues in the proof mode, and make it overall more
   usable.  In particular:
@@ -63,21 +64,27 @@ sed 's/\bPersistentP\b/Persistent/g; s/\bTimelessP\b/Timeless/g; s/\bCMRADiscret
   - There is a new connective `tc_opaque`, which can be used to make definitions
     opaque for type classes, and thus opaque for most tactics of the proof
     mode.
-  - Many missing type class instances for distributing connectives have been
-    defined.
-* The generic `fill` operation of the `ectxi_language` construct has been
-  defined in terms of a left fold instead of a right fold. This gives rise to
-  more definitional equalities.
-* The big operators have been improved:
+  - Define Many missing type class instances for distributing connectives.
+  - Implement the tactics `iIntros (?)` and `iIntros "!#"` (i.e. `iAlways`)
+    using type classes. This makes them more generic, e.g., `iIntros (?)` also
+    works when the universal quantifier is below a modality, and `iAlways` also
+    works for the plainness modality.  A breaking change, however, is that these
+    tactics now no longer work when the universal quantifier or modality is
+    behind a type class opaque definition.  Furthermore, this can change the
+    name of anonymous identifiers introduced with the "%" pattern.
+* Define the generic `fill` operation of the `ectxi_language` construct in terms
+  of a left fold instead of a right fold. This gives rise to more definitional
+  equalities.
+* Improved big operators:
   + They are no longer tied to cameras, but work on any monoid
-  + The version of big operations over lists was redefined so that it enjoy more
-    definitional equalities.
+  + The version of big operations over lists was redefined so that it enjoys
+    more definitional equalities.
 * Various improvements to `solve_ndisj`.
 * Improve handling of pure (non-state-dependent) reductions in heap_lang.
 * Use `Hint Mode` to prevent Coq from making arbitrary guesses in the presence
   of evars, which often led to divergence. There are a few places where type
   annotations are now needed.
-* The `prelude` folder has been moved to its own project: std++
+* Move the `prelude` folder to its own project: std++
 
 ## Iris 3.0.0 (released 2017-01-11)
 

docs/algebra.tex

@@ -75,6 +75,7 @@ The function space $\ofe \nfn \cofeB$ is a COFE if $\cofeB$ is a COFE (\ie the d
 
 Completeness is necessary to take fixed-points.
 For once, every \emph{contractive function} $f : \ofe \to \cofeB$ where $\cofeB$ is a COFE and inhabited has a \emph{unique} fixed-point $\fix(f)$ such that $\fix(f) = f(\fix(f))$.
+This also holds if $f^k$ is contractive for an arbitrary $k$.
 Furthermore, by America and Rutten's theorem~\cite{America-Rutten:JCSS89,birkedal:metric-space}, every contractive (bi)functor from $\COFEs$ to $\COFEs$ has a unique\footnote{Uniqueness is not proven in Coq.} fixed-point.
 
 

opam

@@ -12,5 +12,5 @@ remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris"]
 depends: [
   "coq" { >= "8.6.1" & < "8.8~" }
   "coq-mathcomp-ssreflect" { (>= "1.6.1" & < "1.7~") | (= "dev") }
-  "coq-stdpp" { (= "dev.2017-10-16.0") | (= "dev") }
+  "coq-stdpp" { (= "dev.2017-10-28.3") | (= "dev") }
 ]

theories/proofmode/class_instances.v

@@ -591,6 +591,9 @@ Proof. by rewrite /FromForall. Qed.
 Global Instance from_forall_pure {A} (φ : A → Prop) :
   @FromForall PROP A (⌜∀ a : A, φ a⌝)%I (λ a, ⌜ φ a ⌝)%I.
 Proof. by rewrite /FromForall pure_forall. Qed.
+Global Instance from_forall_pure_not (φ : Prop) :
+  @FromForall PROP φ (⌜¬ φ⌝)%I (λ a : φ, False)%I.
+Proof. by rewrite /FromForall pure_forall. Qed.
 Global Instance from_forall_impl_pure P Q φ :
   IntoPureT P φ → FromForall (P → Q)%I (λ _ : φ, Q)%I.
 Proof.

theories/proofmode/environments.v

@@ -156,7 +156,7 @@ Proof.
 Qed.
 
 Lemma env_lookup_delete_correct Γ i :
-  env_lookup_delete i Γ = x ← Γ !! i; Some (x,env_delete i Γ).
+  env_lookup_delete i Γ = (x ← Γ !! i; Some (x,env_delete i Γ)).
 Proof. induction Γ; intros; simplify; eauto. Qed.
 Lemma env_lookup_delete_Some Γ Γ' i x :
   env_lookup_delete i Γ = Some (x,Γ') ↔ Γ !! i = Some x ∧ Γ' = env_delete i Γ.

theories/tests/proofmode.v

@@ -247,4 +247,11 @@ Lemma test_iAlways P Q R :
   □ P -∗ bi_persistently Q → R -∗ bi_persistently (bi_affinely (bi_affinely P)) ∗ □ Q.
 Proof. iIntros "#HP #HQ HR". iSplitL. iAlways. done. iAlways. done. Qed.
 
+(* TODO: This test is broken in Coq 8.6. Should be restored once we drop Coq
+8.6 support. See also issue #108. *)
+(*
+Lemma test_iIntros_pure : (⌜ ¬False ⌝ : uPred M)%I.
+Proof. by iIntros (?). Qed.
+*)
+
 End tests.