diff --git a/Editor.md b/Editor.md
new file mode 100644
index 0000000000000000000000000000000000000000..fd8b58fe9e67a411bc4c1688b41dff917c8cea1e
--- /dev/null
+++ b/Editor.md
@@ -0,0 +1,91 @@
+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"))
+```
diff --git a/README.md b/README.md
index 2d3fb194ff040ee27b2beb069ff01dfa63df5422..5a22285dafa5bf8c11ed59da3ac85417b4dc2a5e 100644
--- a/README.md
+++ b/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
diff --git a/docs/base-logic.tex b/docs/base-logic.tex
index 5e7d5418327fbbf5b0bf1c755fa5ba15a46c398b..450b6a6adc6c83a3e6ebbf606b6817c588daa7b2 100644
--- a/docs/base-logic.tex
+++ b/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}
}
diff --git a/theories/base_logic/lib/invariants.v b/theories/base_logic/lib/invariants.v
index 8e5b2933ab508af5c0deda33e65e97be11eb2d62..bcfe0a8f747c5e344947009c691e379ba0b977bb 100644
--- a/theories/base_logic/lib/invariants.v
+++ b/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} :
diff --git a/theories/base_logic/lib/na_invariants.v b/theories/base_logic/lib/na_invariants.v
index a86c35bcf4d736ffcd2381d3291dc7f35af3f0d5..d5f27a26100d2bf1f86d99aa9d1f1711bd4131e6 100644
--- a/theories/base_logic/lib/na_invariants.v
+++ b/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.