Merge commit '6b6c1265' into gen_proofmode

Editor.md

+Here we collect some information on how to set up your editor to properly input
+and output the unicode characters used throughout Iris.
+
+## General: Unicode Fonts
+
+Most editors will just use system fonts for rendering unicode characters and do
+not need furhter configuration once the fonts are installed.  Here are some
+combinations of fonts that are known to give readable results (i.e., each of
+these sets of fonts covers all the required characters):
+
+* Fira Mono, DejaVu Mono, Symbola
+
+## Emacs
+
+### Unicode Input
+
+First, install `math-symbol-lists` by doing `M-x package-install math-symbol-lists`.
+
+Next, add the following to your `~/.emacs` to configure an input method based on the math symbol list, and with some custom aliases for symbols used a lot in Iris:
+```
+;; Input of unicode symbols
+(require 'math-symbol-lists)
+; Automatically use math input method for Coq files
+(add-hook 'coq-mode-hook (lambda () (set-input-method "math")))
+; Input method for the minibuffer
+(defun my-inherit-input-method ()
+  "Inherit input method from `minibuffer-selected-window'."
+  (let* ((win (minibuffer-selected-window))
+         (buf (and win (window-buffer win))))
+    (when buf
+      (activate-input-method (buffer-local-value 'current-input-method buf)))))
+(add-hook 'minibuffer-setup-hook #'my-inherit-input-method)
+; Define the actual input method
+(quail-define-package "math" "UTF-8" "Ω" t)
+(quail-define-rules ; add whatever extra rules you want to define here...
+ ("\\mult"   ?⋅)
+ ("\\ent"    ?⊢)
+ ("\\valid"  ?✓)
+ ("\\box"    ?□)
+ ("\\later"  ?▷)
+ ("\\pred"   ?φ)
+ ("\\and"    ?∧)
+ ("\\or"     ?∨)
+ ("\\comp"   ?∘)
+ ("\\ccomp"  ?◎)
+ ("\\all"    ?∀)
+ ("\\ex"     ?∃)
+ ("\\to"     ?→)
+ ("\\sep"    ?∗)
+ ("\\lc"     ?⌜)
+ ("\\rc"     ?⌝)
+ ("\\lam"    ?λ)
+ ("\\empty"  ?∅)
+ ("\\Lam"    ?Λ)
+ ("\\Sig"    ?Σ)
+ ("\\-"      ?∖)
+ ("\\aa"     ?●)
+ ("\\af"     ?◯)
+ ("\\iff"    ?↔)
+ ("\\gname"  ?γ)
+ ("\\incl"   ?≼)
+ ("\\latert" ?▶)
+)
+(mapc (lambda (x)
+        (if (cddr x)
+            (quail-defrule (cadr x) (car (cddr x)))))
+      (append math-symbol-list-basic math-symbol-list-extended))
+```
+
+### Font Configuration
+
+Even when usable fonts are installed, Emacs tends to pick bad fonts for some
+symbols like universal and existential quantifiers.  The following configuration
+results in a decent choice for the symbols used in Iris:
+
+```
+;; Fonts
+(set-face-attribute 'default nil :height 110) ; height is in 1/10pt
+(dolist (ft (fontset-list))
+  ; Main font
+  (set-fontset-font ft 'unicode (font-spec :name "Monospace"))
+  ; Fallback font
+  ; Appending to the 'unicode list makes emacs unbearably slow.
+  ;(set-fontset-font ft 'unicode (font-spec :name "DejaVu Sans Mono") nil 'append)
+  (set-fontset-font ft nil (font-spec :name "DejaVu Sans Mono"))
+)
+; Fallback-fallback font
+; If we 'append this to all fontsets, it picks Symbola even for some cases where DejaVu could
+; be used. Adding it only to the "t" table makes it Do The Right Thing (TM).
+(set-fontset-font t nil (font-spec :name "Symbola"))
+```

README.md

@@ -75,11 +75,14 @@ followed by `make build-dep`.
   infrastructure. Users of the Iris Coq library should *not* depend on these
   modules; they may change or disappear without any notice.
 
-## Documentation
-
-A LaTeX version of the core logic definitions and some derived forms is
-available in [docs/iris.tex](docs/iris.tex).  A compiled PDF version of this
-document is [available online](http://plv.mpi-sws.org/iris/appendix-3.1.pdf).
+## Further Documentation
+
+* A LaTeX version of the core logic definitions and some derived forms is
+  available in [docs/iris.tex](docs/iris.tex).  A compiled PDF version of this
+  document is [available online](http://plv.mpi-sws.org/iris/appendix-3.1.pdf).
+* Information on how to set up your editor for unicode input and output is
+  collected in [Editor.md](Editor.md).
+* The Iris Proof Mode (IPM) is documented at [ProofMode.md](ProofMode.md)
 
 ## Case Studies
 

docs/base-logic.tex

@@ -179,7 +179,7 @@ In writing $\vctx, x:\type$, we presuppose that $x$ is not already declared in $
 	\infer{
 		\vctx, \var:\type \proves \wtt{\term}{\type} \and
 		\text{$\var$ is guarded in $\term$} \and
-		\text{$\type$ is complete}
+		\text{$\type$ is complete and inhabited}
 	}{
 		\vctx \proves \wtt{\MU \var:\type. \term}{\type}
 	}

theories/base_logic/lib/invariants.v

@@ -7,7 +7,7 @@ Import uPred.
 
 (** Derived forms and lemmas about them. *)
 Definition inv_def `{invG Σ} (N : namespace) (P : iProp Σ) : iProp Σ :=
-  (∃ i, ⌜i ∈ (↑N:coPset)⌝ ∧ ownI i P)%I.
+  (∃ i P', ⌜i ∈ (↑N:coPset)⌝ ∧ ▷ □ (P' ↔ P) ∧ ownI i P')%I.
 Definition inv_aux : seal (@inv_def). by eexists. Qed.
 Definition inv {Σ i} := unseal inv_aux Σ i.
 Definition inv_eq : @inv = @inv_def := seal_eq inv_aux.
@@ -21,19 +21,25 @@ Implicit Types N : namespace.
 Implicit Types P Q R : iProp Σ.
 
 Global Instance inv_contractive N : Contractive (inv N).
-Proof.
-  rewrite inv_eq=> n ???. apply exist_ne=>i. by apply and_ne, ownI_contractive.
-Qed.
+Proof. rewrite inv_eq. solve_contractive. Qed.
 
 Global Instance inv_ne N : NonExpansive (inv N).
 Proof. apply contractive_ne, _. Qed.
 
-Global Instance inv_Proper N : Proper ((⊣⊢) ==> (⊣⊢)) (inv N).
+Global Instance inv_proper N : Proper ((⊣⊢) ==> (⊣⊢)) (inv N).
 Proof. apply ne_proper, _. Qed.
 
 Global Instance inv_persistent N P : Persistent (inv N P).
 Proof. rewrite inv_eq /inv; apply _. Qed.
 
+Lemma inv_iff N P Q : ▷ □ (P ↔ Q) -∗ inv N P -∗ inv N Q.
+Proof.
+  iIntros "#HPQ". rewrite inv_eq. iDestruct 1 as (i P') "(?&#HP&?)".
+  iExists i, P'. iFrame. iNext; iAlways; iSplit.
+  - iIntros "HP'". iApply "HPQ". by iApply "HP".
+  - iIntros "HQ". iApply "HP". by iApply "HPQ".
+Qed.
+
 Lemma fresh_inv_name (E : gset positive) N : ∃ i, i ∉ E ∧ i ∈ (↑N:coPset).
 Proof.
   exists (coPpick (↑ N ∖ coPset.of_gset E)).
@@ -48,6 +54,7 @@ Proof.
   rewrite inv_eq /inv_def uPred_fupd_eq. iIntros "HP [Hw $]".
   iMod (ownI_alloc (∈ (↑N : coPset)) P with "[$HP $Hw]")
     as (i ?) "[$ ?]"; auto using fresh_inv_name.
+  do 2 iModIntro. iExists i, P. rewrite -(iff_refl True%I). auto.
 Qed.
 
 Lemma inv_alloc_open N E P :
@@ -61,7 +68,9 @@ Proof.
   { rewrite -?ownE_op; [|set_solver..].
     rewrite assoc_L -!union_difference_L //. set_solver. }
   do 2 iModIntro. iFrame "HE\N". iSplitL "Hw HEi"; first by iApply "Hw".
-  iSplitL "Hi"; first by eauto. iIntros "HP [Hw HE\N]".
+  iSplitL "Hi".
+  { iExists i, P. rewrite -(iff_refl True%I). auto. }
+  iIntros "HP [Hw HE\N]".
   iDestruct (ownI_close with "[$Hw $Hi $HP $HD]") as "[$ HEi]".
   do 2 iModIntro. iSplitL; [|done].
   iCombine "HEi HEN\i HE\N" as "HEN".
@@ -72,13 +81,16 @@ Qed.
 Lemma inv_open E N P :
   ↑N ⊆ E → inv N P ={E,E∖↑N}=∗ ▷ P ∗ (▷ P ={E∖↑N,E}=∗ True).
 Proof.
-  rewrite inv_eq /inv_def uPred_fupd_eq /uPred_fupd_def; iDestruct 1 as (i) "[Hi #HiP]".
+  rewrite inv_eq /inv_def uPred_fupd_eq /uPred_fupd_def.
+  iDestruct 1 as (i P') "(Hi & #HP' & #HiP)".
   iDestruct "Hi" as % ?%elem_of_subseteq_singleton.
   rewrite {1 4}(union_difference_L (↑ N) E) // ownE_op; last set_solver.
   rewrite {1 5}(union_difference_L {[ i ]} (↑ N)) // ownE_op; last set_solver.
   iIntros "(Hw & [HE $] & $) !> !>".
-  iDestruct (ownI_open i P with "[$Hw $HE $HiP]") as "($ & $ & HD)".
-  iIntros "HP [Hw $] !> !>". iApply ownI_close; by iFrame.
+  iDestruct (ownI_open i with "[$Hw $HE $HiP]") as "($ & HP & HD)".
+  iDestruct ("HP'" with "HP") as "$".
+  iIntros "HP [Hw $] !> !>". iApply (ownI_close _ P'). iFrame "HD Hw HiP".
+  iApply "HP'". iFrame.
 Qed.
 
 Lemma inv_open_timeless E N P `{!Timeless P} :

theories/base_logic/lib/na_invariants.v

@@ -43,6 +43,14 @@ Section proofs.
   Global Instance na_inv_persistent p N P : Persistent (na_inv p N P).
   Proof. rewrite /na_inv; apply _. Qed.
 
+  Lemma na_inv_iff p N P Q : ▷ □ (P ↔ Q) -∗ na_inv p N P -∗ na_inv p N Q.
+  Proof.
+    iIntros "#HPQ". rewrite /na_inv. iDestruct 1 as (i ?) "#Hinv".
+    iExists i. iSplit; first done. iApply (inv_iff with "[] Hinv").
+    iNext. iAlways. iSplit; (iIntros "[[? Ho]|?]";
+      [iLeft; iFrame "Ho"; by iApply "HPQ"|by iRight]).
+  Qed.
+
   Lemma na_alloc : (|==> ∃ p, na_own p ⊤)%I.
   Proof. by apply own_alloc. Qed.