Initial commit

.gitignore

+*.vo
+*.glob
+.sconsign.dblite
+deps
+old/*
+coqidescript
+\#*\#
+*.pyc
+*~
+*.cmi
+*.cmx
+*.cmo
+*.o
+utils/coq2html
+utils/coq2html.ml
+doc/ch2o.*.html
+*.cache
+*.broken
+broken/*
+*.patch
+parser/Extracted.*
+parser/Lexer.ml
+parser/Parser.ml
+parser/Parser.mli
+parser/Include.*
+_build/
+ch2o
+*.native
+*.byte
+a.out
+*.aux
+.coq-native/

SConstruct

+# Copyright (c) 2012-2015, Robbert Krebbers.
+# This file is distributed under the terms of the BSD license.
+import os, glob, string
+
+modules = ["prelude", "iris"]
+Rs = '-R . iris'
+env = DefaultEnvironment(ENV = os.environ,tools=['default', 'Coq'], COQFLAGS=Rs)
+
+# Coq dependencies
+vs = [x for m in modules for x in glob.glob(m + '/*.v')]
+if os.system('coqdep ' + Rs + ' ' + ' '.join(map(str, vs)) + ' > deps'): Exit(2)
+ParseDepends('deps')
+
+# Coq files
+for v in vs: env.Coq(v)
+
+# Coqidescript
+env.CoqIdeScript('coqidescript', [])

iris/agree.v

+Require Export cmra.
+Local Hint Extern 10 (_ ≤ _) => omega.
+
+Record agree A `{Dist A} := Agree {
+  agree_car :> nat → A;
+  agree_is_valid : nat → Prop;
+  agree_valid_0 : agree_is_valid 0;
+  agree_valid_S n : agree_is_valid (S n) → agree_is_valid n;
+  agree_cauchy n i: n ≤ i → agree_is_valid i → agree_car n ={n}= agree_car i
+}.
+Arguments Agree {_ _} _ _ _ _ _.
+Arguments agree_car {_ _} _ _.
+Arguments agree_is_valid {_ _} _ _.
+Arguments agree_cauchy {_ _} _ _ _ _ _.
+
+Section agree.
+Context `{Cofe A}.
+
+Global Instance agree_validN : ValidN (agree A) := λ n x, agree_is_valid x n.
+Lemma agree_valid_le (x : agree A) n n' : validN n x → n' ≤ n → validN n' x.
+Proof. unfold validN, agree_validN; induction 2; eauto using agree_valid_S. Qed.
+Global Instance agree_valid : Valid (agree A) := λ x, ∀ n, validN n x.
+Global Instance agree_equiv : Equiv (agree A) := λ x y,
+  (∀ n, validN n x ↔ validN n y) ∧ (∀ n, validN n x → x n ={n}= y n).
+Global Instance agree_dist : Dist (agree A) := λ n x y,
+  (∀ n', n' ≤ n → validN n' x ↔ validN n' y) ∧
+  (∀ n', n' ≤ n → validN n' x → x n' ={n'}= y n').
+Global Program Instance agree_compl : Compl (agree A) := λ c,
+  {| agree_car n := c n n; agree_is_valid n := validN n (c n) |}.
+Next Obligation. intros; apply agree_valid_0. Qed.
+Next Obligation.
+  intros c n ?; apply (chain_cauchy c n (S n)), agree_valid_S; auto.
+Qed.
+Next Obligation.
+  intros c n i ??; simpl in *; rewrite <-(agree_cauchy (c i) n i) by done.
+  by apply (chain_cauchy c), (chain_cauchy c) with i, agree_valid_le with i.
+Qed.
+Instance agree_cofe : Cofe (agree A).
+Proof.
+  split.
+  * intros x y; split.
+    + by intros Hxy n; split; intros; apply Hxy.
+    + by intros Hxy; split; intros; apply Hxy with n.
+  * split.
+    + by split.
+    + by intros x y Hxy; split; intros; symmetry; apply Hxy; auto; apply Hxy.
+    + intros x y z Hxy Hyz; split; intros n'; intros.
+      - transitivity (validN n' y). by apply Hxy. by apply Hyz.
+      - transitivity (y n'). by apply Hxy. by apply Hyz, Hxy.
+  * intros n x y Hxy; split; intros; apply Hxy; auto.
+  * intros x y; split; intros n'; rewrite Nat.le_0_r; intros ->; [|done].
+    by split; intros; apply agree_valid_0.
+  * by intros c n; split; intros; apply (chain_cauchy c).
+Qed.
+
+Global Program Instance agree_op : Op (agree A) := λ x y,
+  {| agree_car := x; agree_is_valid n := validN n x ∧ validN n y ∧ x ={n}= y |}.
+Next Obligation. by intros; simpl; split_ands; try apply agree_valid_0. Qed.
+Next Obligation. naive_solver eauto using agree_valid_le, dist_S. Qed.
+Next Obligation. by intros x y n i ? (?&?&?); apply agree_cauchy. Qed.
+Global Instance agree_unit : Unit (agree A) := id.
+Global Instance agree_minus : Minus (agree A) := λ x y, x.
+Global Instance agree_included : Included (agree A) := λ x y, y ≡ x ⋅ y.
+Instance: Associative (≡) (@op (agree A) _).
+Proof.
+  intros x y z; split; [split|done].
+  * intros (?&(?&?&Hyz)&Hxy); repeat (intros (?&?&?) || intro || split);
+      eauto using agree_valid_le; try apply Hxy; auto.
+    etransitivity; [by apply Hxy|by apply Hyz].
+  * intros ((?&?&Hxy)&?&Hxz); repeat split;
+      try apply Hxy; eauto using agree_valid_le;
+      by etransitivity; [symmetry; apply Hxy|apply Hxz];
+       repeat (intro || split); eauto using agree_valid_le; apply Hxy; auto.
+Qed.
+Instance: Commutative (≡) (@op (agree A) _).
+Proof.
+  intros x y; split; [split|intros n (?&?&Hxy); apply Hxy; auto];
+    intros (?&?&Hxy); repeat split; eauto using agree_valid_le;
+    intros n' ??; symmetry; apply Hxy; eauto using agree_valid_le.
+Qed.
+Definition agree_idempotent (x : agree A) : x ⋅ x ≡ x.
+Proof. split; [split;[by intros (?&?&?)|done]|done]. Qed.
+Instance: ∀ x : agree A, Proper (dist n ==> dist n) (op x).
+Proof.
+  intros n x y1 y2 [Hy' Hy]; split; [|done].
+  split; intros (?&?&Hxy); repeat (intro || split);
+    try apply Hy'; eauto using agree_valid_le.
+  * etransitivity; [apply Hxy|apply Hy]; eauto using agree_valid_le.
+  * etransitivity; [apply Hxy|symmetry; apply Hy, Hy'];
+      eauto using agree_valid_le.
+Qed.
+Instance: Proper (dist n ==> dist n ==> dist n) op.
+Proof. by intros n x1 x2 Hx y1 y2 Hy; rewrite Hy,!(commutative _ _ y2), Hx. Qed.
+Global Instance agree_cmra : CMRA (agree A).
+Proof.
+  split; try (apply _ || done).
+  * by intros n x y Hxy ?; apply Hxy.
+  * by intros n x1 x2 Hx y1 y2 Hy.
+  * by intros x y1 y2 Hy ?; do 2 red; rewrite <-Hy.
+  * intros; apply agree_valid_0.
+  * intros n x ?; apply agree_valid_le with (S n); auto.
+  * intros x; apply agree_idempotent.
+  * intros x y; change (x ⋅ y ≡ x ⋅ (x ⋅ y)).
+    by rewrite (associative _), agree_idempotent.
+  * by intros x y n (?&?&?).
+  * by intros x y; do 2 red; rewrite (associative _), agree_idempotent.
+Qed.
+Program Definition to_agree (x : A) : agree A :=
+  {| agree_car n := x; agree_is_valid n := True |}.
+Solve Obligations with done.
+Global Instance to_agree_ne n : Proper (dist n ==> dist n) to_agree.
+Proof. intros x1 x2 Hx; split; naive_solver eauto using @dist_le. Qed.
+
+Lemma agree_op_inv (x y1 y2 : agree A) n :
+  validN n x → x ={n}= y1 ⋅ y2 → y1 ={n}= y2.
+Proof. by intros ? Hxy; apply Hxy. Qed.
+Global Instance agree_extend : CMRAExtend (agree A).
+Proof.
+  intros x y1 y2 n ? Hx; exists (x,x); simpl; split.
+  * by rewrite agree_idempotent.
+  * by rewrite Hx, (agree_op_inv x y1 y2), agree_idempotent by done.
+Qed.
+End agree.
+
+Canonical Structure agreeC (A : cmraT) : cmraT := CMRAT (agree A).
+
+Section agree_map.
+  Context `{Cofe A, Cofe B} (f: A → B) `{Hf: ∀ n, Proper (dist n ==> dist n) f}.
+  Program Definition agree_map (x : agree A) : agree B :=
+   {| agree_car n := f (x n); agree_is_valid n := validN n x |}.
+  Next Obligation. apply agree_valid_0. Qed.
+  Next Obligation. by intros x n ?; apply agree_valid_S. Qed.
+  Next Obligation. by intros x n i ??; simpl; rewrite (agree_cauchy x n i). Qed.
+  Global Instance agree_map_ne n : Proper (dist n ==> dist n) agree_map.
+  Proof. by intros x1 x2 Hx; split; simpl; intros; [apply Hx|apply Hf, Hx]. Qed.
+  Global Instance agree_map_preserving : CMRAPreserving agree_map.
+  Proof.
+    split; [|by intros n ?].
+    intros x y; unfold included, agree_included; intros Hy; rewrite Hy.
+    split; [split|done].
+    * by intros (?&?&Hxy); repeat (intro || split);
+        try apply Hxy; try apply Hf; eauto using @agree_valid_le.
+    * by intros (?&(?&?&Hxy)&_); repeat split;
+        try apply Hxy; eauto using agree_valid_le.
+  Qed.
+End agree_map.

iris/auth.v

+Require Export excl.
+Local Arguments disjoint _ _ !_ !_ /.
+Local Arguments included _ _ !_ !_ /.
+
+Record auth (A : Type) : Type := Auth { authorative : excl A ; own : A }.
+Arguments Auth {_} _ _.
+Arguments authorative {_} _.
+Arguments own {_} _.
+Notation "∘ x" := (Auth ExclUnit x) (at level 20).
+Notation "∙ x" := (Auth (Excl x) ∅) (at level 20).
+
+Instance auth_valid `{Valid A, Included A} : Valid (auth A) := λ x,
+  valid (authorative x) ∧ excl_above (own x) (authorative x).
+Instance auth_equiv `{Equiv A} : Equiv (auth A) := λ x y,
+  authorative x ≡ authorative y ∧ own x ≡ own y.
+Instance auth_unit `{Unit A} : Unit (auth A) := λ x,
+  Auth (unit (authorative x)) (unit (own x)).
+Instance auth_op `{Op A} : Op (auth A) := λ x y,
+  Auth (authorative x ⋅ authorative y) (own x ⋅ own y).
+Instance auth_minus `{Minus A} : Minus (auth A) := λ x y,
+  Auth (authorative x ⩪ authorative y) (own x ⩪ own y).
+Instance auth_included `{Equiv A, Included A} : Included (auth A) := λ x y,
+  authorative x ≼ authorative y ∧ own x ≼ own y.
+
+Instance auth_ra `{RA A} : RA (auth A).
+Proof.
+  split.
+  * split.
+    + by intros ?; split.
+    + by intros ?? [??]; split.
+    + intros ??? [??] [??]; split; etransitivity; eauto.
+  * by intros x y1 y2 [Hy Hy']; split; simpl; rewrite ?Hy, ?Hy'.
+  * by intros y1 y2 [Hy Hy']; split; simpl; rewrite ?Hy, ?Hy'.
+  * by intros y1 y2 [Hy Hy'] [??]; split; simpl; rewrite <-?Hy, <-?Hy'.
+  * by intros x1 x2 [Hx Hx'] y1 y2 [Hy Hy'];
+      split; simpl; rewrite ?Hy, ?Hy', ?Hx, ?Hx'.
+  * by intros x y1 y2 [Hy Hy'] [??]; split; simpl; rewrite <-?Hy, <-?Hy'.
+  * by split; simpl; rewrite (associative _).
+  * by split; simpl; rewrite (commutative _).
+  * by split; simpl; rewrite ?(ra_unit_l _).
+  * by split; simpl; rewrite ?(ra_unit_idempotent _).
+  * split; simpl; auto using ra_unit_weaken.
+  * intros ?? [??]; split; [by apply ra_valid_op_l with (authorative y)|].
+    by apply excl_above_weaken with (own x ⋅ own y)
+      (authorative x ⋅ authorative y); try apply ra_included_l.
+  * split; simpl; apply ra_included_l.
+  * by intros ?? [??]; split; simpl; apply ra_op_difference.
+Qed.
+Lemma auth_frag_op `{RA A} a b : ∘(a ⋅ b) ≡ ∘a ⋅ ∘b.
+Proof. done. Qed.
\ No newline at end of file

iris/cmra.v

+Require Export ra cofe cofe_instances.
+
+Class ValidN (A : Type) := validN : nat → A → Prop.
+Instance: Params (@validN) 3.
+
+Class CMRA A `{Equiv A, Compl A,
+    Unit A, Op A, Valid A, ValidN A, Included A, Minus A} : Prop := {
+  (* setoids *)
+  cmra_cofe :> Cofe A;
+  cmra_op_ne n x :> Proper (dist n ==> dist n) (op x);
+  cmra_unit_ne n :> Proper (dist n ==> dist n) unit;
+  cmra_valid_ne n :> Proper (dist n ==> impl) (validN n);
+  cmra_minus_ne n :> Proper (dist n ==> dist n ==> dist n) minus;
+  cmra_included_proper x : Proper ((≡) ==> impl) (included x);
+  (* valid *)
+  cmra_valid_0 x : validN 0 x;
+  cmra_valid_S n x : validN (S n) x → validN n x;
+  cmra_valid_validN x : valid x ↔ ∀ n, validN n x;
+  (* monoid *)
+  cmra_associative : Associative (≡) (⋅);
+  cmra_commutative : Commutative (≡) (⋅);
+  cmra_unit_l x : unit x ⋅ x ≡ x;
+  cmra_unit_idempotent x : unit (unit x) ≡ unit x;
+  cmra_unit_weaken x y : unit x ≼ unit (x ⋅ y);
+  cmra_valid_op_l n x y : validN n (x ⋅ y) → validN n x;
+  cmra_included_l x y : x ≼ x ⋅ y;
+  cmra_op_difference x y : x ≼ y → x ⋅ y ⩪ x ≡ y
+}.
+Class CMRAExtend A `{Equiv A, Dist A, Op A, ValidN A} :=
+  cmra_extend_op x y1 y2 n :
+    validN n x → x ={n}= y1 ⋅ y2 → { z | x ≡ z.1 ⋅ z.2 ∧ z ={n}= (y1,y2) }.
+
+Class CMRAPreserving
+    `{Included A, ValidN A, Included B, ValidN B} (f : A → B) := {
+  included_preserving x y : x ≼ y → f x ≼ f y;
+  validN_preserving n x : validN n x → validN n (f x)
+}.
+
+(** Bundeled version *)
+Structure cmraT := CMRAT {
+  cmra_car :> Type;
+  cmra_equiv : Equiv cmra_car;
+  cmra_dist : Dist cmra_car;
+  cmra_compl : Compl cmra_car;
+  cmra_unit : Unit cmra_car;
+  cmra_op : Op cmra_car;
+  cmra_valid : Valid cmra_car;
+  cmra_validN : ValidN cmra_car;
+  cmra_included : Included cmra_car;
+  cmra_minus : Minus cmra_car;
+  cmra_cmra : CMRA cmra_car;
+  cmra_extend : CMRAExtend cmra_car
+}.
+Arguments CMRAT _ {_ _ _ _ _ _ _ _ _ _ _}.
+Add Printing Constructor cmraT.
+Existing Instances cmra_equiv cmra_dist cmra_compl cmra_unit cmra_op
+  cmra_valid cmra_validN cmra_included cmra_minus cmra_cmra cmra_extend.
+Coercion cmra_cofeC (A : cmraT) : cofeT := CofeT A.
+Canonical Structure cmra_cofeC.
+
+Section cmra.
+Context `{cmra : CMRA A}.
+Implicit Types x y z : A.
+
+Global Instance cmra_valid_ne' : Proper (dist n ==> iff) (validN n).
+Proof. by split; apply cmra_valid_ne. Qed.
+Global Instance cmra_valid_proper : Proper ((≡) ==> iff) (validN n).
+Proof. by intros n x1 x2 Hx; apply cmra_valid_ne', equiv_dist. Qed.
+Global Instance cmra_ra : RA A.
+Proof.
+  split; try by (destruct cmra; eauto with typeclass_instances).
+  * by intros x1 x2 Hx; rewrite !cmra_valid_validN; intros ? n; rewrite <-Hx.
+  * intros x y; rewrite !cmra_valid_validN; intros ? n.
+    by apply cmra_valid_op_l with y.
+Qed.
+Lemma cmra_valid_op_r x y n : validN n (x ⋅ y) → validN n y.
+Proof. rewrite (commutative _ x); apply cmra_valid_op_l. Qed.
+Lemma cmra_valid_included x y n : validN n y → x ≼ y → validN n x.
+Proof.
+  rewrite ra_included_spec; intros Hvalid [z Hy]; rewrite Hy in Hvalid.
+  eauto using cmra_valid_op_l.
+Qed.
+Lemma cmra_valid_le x n n' : validN n x → n' ≤ n → validN n' x.
+Proof. induction 2; eauto using cmra_valid_S. Qed.
+Global Instance ra_op_ne n : Proper (dist n ==> dist n ==> dist n) (⋅).
+Proof.
+  intros x1 x2 Hx y1 y2 Hy.
+  by rewrite Hy, (commutative _ x1), Hx, (commutative _ y2).
+Qed.
+Lemma cmra_included_dist_l x1 x2 x1' n :
+  x1 ≼ x2 → x1' ={n}= x1 → ∃ x2', x1' ≼ x2' ∧ x2' ={n}= x2.
+Proof.
+  rewrite ra_included_spec; intros [z Hx2] Hx1; exists (x1' ⋅ z); split.
+  apply ra_included_l. by rewrite Hx1, Hx2.
+Qed.
+Lemma cmra_unit_valid x n : validN n x → validN n (unit x).
+Proof. rewrite <-(cmra_unit_l x) at 1; apply cmra_valid_op_l. Qed.
+End cmra.
+
+(* Also via [cmra_cofe; cofe_equivalence] *)
+Hint Cut [!*; ra_equivalence; cmra_ra] : typeclass_instances.

iris/cofe.v

+Require Export prelude.
+Obligation Tactic := idtac.
+
+(** Unbundeled version *)
+Class Dist A := dist : nat → relation A.
+Instance: Params (@dist) 2.
+Notation "x ={ n }= y" := (dist n x y)
+  (at level 70, n at next level, format "x  ={ n }=  y").
+Hint Extern 0 (?x ={_}= ?x) => reflexivity.
+Hint Extern 0 (_ ={_}= _) => symmetry; assumption.
+
+Record chain (A : Type) `{Dist A} := {
+  chain_car :> nat → A;
+  chain_cauchy n i : n ≤ i → chain_car n ={n}= chain_car i
+}.
+Arguments chain_car {_ _} _ _.
+Arguments chain_cauchy {_ _} _ _ _ _.
+Class Compl A `{Dist A} := compl : chain A → A.
+
+Class Cofe A `{Equiv A, Compl A} := {
+  equiv_dist x y : x ≡ y ↔ ∀ n, x ={n}= y;
+  dist_equivalence n :> Equivalence (dist n);
+  dist_S n x y : x ={S n}= y → x ={n}= y;
+  dist_0 x y : x ={0}= y;
+  conv_compl (c : chain A) n : compl c ={n}= c n
+}.
+Hint Extern 0 (_ ={0}= _) => apply dist_0.
+Class Contractive `{Dist A, Dist B} (f : A -> B) :=
+  contractive n : Proper (dist n ==> dist (S n)) f.
+
+(** Bundeled version *)
+Structure cofeT := CofeT {
+  cofe_car :> Type;
+  cofe_equiv : Equiv cofe_car;
+  cofe_dist : Dist cofe_car;
+  cofe_compl : Compl cofe_car;
+  cofe_cofe : Cofe cofe_car
+}.
+Arguments CofeT _ {_ _ _ _}.
+Add Printing Constructor cofeT.
+Existing Instances cofe_equiv cofe_dist cofe_compl cofe_cofe.
+
+(** General properties *)
+Section cofe.
+  Context `{Cofe A}.
+  Global Instance cofe_equivalence : Equivalence ((≡) : relation A).
+  Proof.
+    split.
+    * by intros x; rewrite equiv_dist.
+    * by intros x y; rewrite !equiv_dist.
+    * by intros x y z; rewrite !equiv_dist; intros; transitivity y.
+  Qed.
+  Global Instance dist_ne n : Proper (dist n ==> dist n ==> iff) (dist n).
+  Proof.
+    intros x1 x2 ? y1 y2 ?; split; intros.
+    * by transitivity x1; [done|]; transitivity y1.
+    * by transitivity x2; [done|]; transitivity y2.
+  Qed.
+  Global Instance dist_proper n : Proper ((≡) ==> (≡) ==> iff) (dist n).
+  Proof.
+    intros x1 x2 Hx y1 y2 Hy.
+    by rewrite equiv_dist in Hx, Hy; rewrite (Hx n), (Hy n).
+  Qed.
+  Global Instance dist_proper_2 n x : Proper ((≡) ==> iff) (dist n x).
+  Proof. by apply dist_proper. Qed.
+  Lemma dist_le x y n n' : x ={n}= y → n' ≤ n → x ={n'}= y.
+  Proof. induction 2; eauto using dist_S. Qed.
+  Global Instance contractive_ne `{Cofe B} (f : A → B) `{!Contractive f} n :
+    Proper (dist n ==> dist n) f | 100.
+  Proof. by intros x1 x2 ?; apply dist_S, contractive. Qed.
+  Global Instance ne_proper `{Cofe B} (f : A → B)
+    `{!∀ n, Proper (dist n ==> dist n) f} : Proper ((≡) ==> (≡)) f | 100.
+  Proof. by intros x1 x2; rewrite !equiv_dist; intros Hx n; rewrite (Hx n). Qed.
+  Global Instance ne_proper_2 `{Cofe B, Cofe C} (f : A → B → C)
+    `{!∀ n, Proper (dist n ==> dist n ==> dist n) f} :
+    Proper ((≡) ==> (≡) ==> (≡)) f | 100.
+  Proof.
+     unfold Proper, respectful; setoid_rewrite equiv_dist.
+     by intros x1 x2 Hx y1 y2 Hy n; rewrite Hx, Hy.
+  Qed.
+  Lemma compl_ne (c1 c2: chain A) n : c1 n ={n}= c2 n → compl c1 ={n}= compl c2.
+  Proof. intros. by rewrite (conv_compl c1 n), (conv_compl c2 n). Qed.
+  Lemma compl_ext (c1 c2 : chain A) : (∀ i, c1 i ≡ c2 i) → compl c1 ≡ compl c2.
+  Proof. setoid_rewrite equiv_dist; naive_solver eauto using compl_ne. Qed.
+End cofe.
+
+(** Fixpoint *)
+Program Definition fixpoint_chain `{Cofe A} (f : A → A) `{!Contractive f}
+  (x : A) : chain A := {| chain_car i := Nat.iter i f x |}.
+Next Obligation.
+  intros A ???? f ? x n; induction n as [|n IH]; intros i ?; [done|].
+  destruct i as [|i]; simpl; try lia; apply contractive, IH; auto with lia.
+Qed.
+Program Definition fixpoint `{Cofe A} (f : A → A) `{!Contractive f}
+  (x : A) : A := compl (fixpoint_chain f x).
+
+Section fixpoint.
+  Context `{Cofe A} (f : A → A) `{!Contractive f}.
+  Lemma fixpoint_unfold x : fixpoint f x ≡ f (fixpoint f x).
+  Proof.
+    apply equiv_dist; intros n; unfold fixpoint.
+    rewrite (conv_compl (fixpoint_chain f x) n).
+    by rewrite (chain_cauchy (fixpoint_chain f x) n (S n)) at 1 by lia.
+  Qed.
+  Lemma fixpoint_ne (g : A → A) `{!Contractive g} x y n :
+    (∀ z, f z ={n}= g z) → fixpoint f x ={n}= fixpoint g y.
+  Proof.
+    intros Hfg; unfold fixpoint; rewrite (conv_compl (fixpoint_chain f x) n),
+      (conv_compl (fixpoint_chain g y) n).
+    induction n as [|n IH]; simpl in *; [done|].
+    rewrite Hfg; apply contractive, IH; auto using dist_S.
+  Qed.
+  Lemma fixpoint_proper (g : A → A) `{!Contractive g} x :
+    (∀ x, f x ≡ g x) → fixpoint f x ≡ fixpoint g x.
+  Proof. setoid_rewrite equiv_dist; naive_solver eauto using fixpoint_ne. Qed.
+End fixpoint.
+
+(** Function space *)
+Structure cofeMor (A B : cofeT) : Type := CofeMor {
+  cofe_mor_car :> A → B;
+  cofe_mor_ne n : Proper (dist n ==> dist n) cofe_mor_car
+}.
+Arguments CofeMor {_ _} _ {_}.
+Add Printing Constructor cofeMor.
+Existing Instance cofe_mor_ne.
+
+Instance cofe_mor_proper `(f : cofeMor A B) : Proper ((≡) ==> (≡)) f := _.
+Instance cofe_mor_equiv {A B : cofeT} : Equiv (cofeMor A B) := λ f g,
+  ∀ x, f x ≡ g x.
+Instance cofe_mor_dist (A B : cofeT) : Dist (cofeMor A B) := λ n f g,
+  ∀ x, f x ={n}= g x.
+Program Definition fun_chain `(c : chain (cofeMor A B)) (x : A) : chain B :=
+  {| chain_car n := c n x |}.
+Next Obligation. intros A B c x n i ?. by apply (chain_cauchy c). Qed.
+Program Instance cofe_mor_compl (A B : cofeT) : Compl (cofeMor A B) := λ c,
+  {| cofe_mor_car x := compl (fun_chain c x) |}.
+Next Obligation.
+  intros A B c n x y Hxy.
+  rewrite (conv_compl (fun_chain c x) n), (conv_compl (fun_chain c y) n).
+  simpl; rewrite Hxy; apply (chain_cauchy c); lia.
+Qed.
+Instance cofe_mor_cofe (A B : cofeT) : Cofe (cofeMor A B).
+Proof.
+  split.
+  * intros X Y; split; [intros HXY n k; apply equiv_dist, HXY|].
+    intros HXY k; apply equiv_dist; intros n; apply HXY.
+  * intros n; split.
+    + by intros f x.
+    + by intros f g ? x.
+    + by intros f g h ?? x; transitivity (g x).
+  * by intros n f g ? x; apply dist_S.
+  * by intros f g x.
+  * intros c n x; simpl.
+    rewrite (conv_compl (fun_chain c x) n); apply (chain_cauchy c); lia.
+Qed.
+Instance cofe_mor_car_proper :
+  Proper ((≡) ==> (≡) ==> (≡)) (@cofe_mor_car A B).
+Proof. intros A B f g Hfg x y Hx; rewrite Hx; apply Hfg. Qed.
+Lemma cofe_mor_ext {A B} (f g : cofeMor A B) : f ≡ g ↔ ∀ x, f x ≡ g x.
+Proof. done. Qed.
+Canonical Structure cofe_mor (A B : cofeT) : cofeT := CofeT (cofeMor A B).
+Infix "-n>" := cofe_mor (at level 45, right associativity).
+
+(** Identity and composition *)
+Definition cid {A} : A -n> A := CofeMor id.
+Instance: Params (@cid) 1.
+Definition ccompose {A B C}
+  (f : B -n> C) (g : A -n> B) : A -n> C := CofeMor (f ∘ g).
+Instance: Params (@ccompose) 3.
+Infix "◎" := ccompose (at level 40, left associativity).
+Lemma ccompose_ne {A B C} (f1 f2 : B -n> C) (g1 g2 : A -n> B) n :
+  f1 ={n}= f2 → g1 ={n}= g2 → f1 ◎ g1 ={n}= f2 ◎ g2.
+Proof. by intros Hf Hg x; simpl; rewrite (Hg x), (Hf (g2 x)). Qed.
+
+(** Pre-composition as a functor *)
+Local Instance ccompose_l_ne' {A B C} (f : B -n> A) n :
+  Proper (dist n ==> dist n) (λ g : A -n> C, g ◎ f).
+Proof. by intros g1 g2 ?; apply ccompose_ne. Qed.
+Definition ccompose_l {A B C} (f : B -n> A) : (A -n> C) -n> (B -n> C) :=
+  CofeMor (λ g : A -n> C, g ◎ f).
+Instance ccompose_l_ne {A B C} : Proper (dist n ==> dist n) (@ccompose_l A B C).
+Proof. by intros n f1 f2 Hf g x; apply ccompose_ne. Qed.
+
+(** unit *)
+Instance unit_dist : Dist unit := λ _ _ _, True.
+Instance unit_compl : Compl unit := λ _, ().
+Instance unit_cofe : Cofe unit.
+Proof. by repeat split; try exists 0. Qed.
+
+(** Product *)
+Instance prod_dist `{Dist A, Dist B} : Dist (A * B) := λ n,
+  prod_relation (dist n) (dist n).
+Program Definition fst_chain `{Dist A, Dist B} (c : chain (A * B)) : chain A :=
+  {| chain_car n := fst (c n) |}.
+Next Obligation. by intros A ? B ? c n i ?; apply (chain_cauchy c n). Qed.
+Program Definition snd_chain `{Dist A, Dist B} (c : chain (A * B)) : chain B :=
+  {| chain_car n := snd (c n) |}.
+Next Obligation. by intros A ? B ? c n i ?; apply (chain_cauchy c n). Qed.
+Instance prod_compl `{Compl A, Compl B} : Compl (A * B) := λ c,
+  (compl (fst_chain c), compl (snd_chain c)).
+Instance prod_cofe `{Cofe A, Cofe B} : Cofe (A * B).
+Proof.
+  split.
+  * intros x y; unfold dist, prod_dist, equiv, prod_equiv, prod_relation.
+    rewrite !equiv_dist; naive_solver.
+  * apply _.
+  * by intros n [x1 y1] [x2 y2] [??]; split; apply dist_S.
+  * by split.
+  * intros c n; split. apply (conv_compl (fst_chain c) n).
+    apply (conv_compl (snd_chain c) n).
+Qed.
+Canonical Structure prodC (A B : cofeT) : cofeT := CofeT (A * B).
+Local Instance prod_map_ne `{Dist A, Dist A', Dist B, Dist B'} n :
+  Proper ((dist n ==> dist n) ==> (dist n ==> dist n) ==>
+           dist n ==> dist n) (@prod_map A A' B B').
+Proof. by intros f f' Hf g g' Hg ?? [??]; split; [apply Hf|apply Hg]. Qed.
+Definition prodC_map {A A' B B'} (f : A -n> A') (g : B -n> B') :
+  prodC A B -n> prodC A' B' := CofeMor (prod_map f g).
+Instance prodC_map_ne {A A' B B'} n :
+  Proper (dist n ==> dist n ==> dist n) (@prodC_map A A' B B').
+Proof. intros f f' Hf g g' Hg [??]; split; [apply Hf|apply Hg]. Qed.
+
+Instance pair_ne `{Dist A, Dist B} :
+  Proper (dist n ==> dist n ==> dist n) (@pair A B) := _.
+Instance fst_ne `{Dist A, Dist B} : Proper (dist n ==> dist n) (@fst A B) := _.
+Instance snd_ne `{Dist A, Dist B} : Proper (dist n ==> dist n) (@snd A B) := _.
+Typeclasses Opaque prod_dist.

iris/cofe_instances.v

+Require Export cofe.
+Require Import fin_maps pmap nmap zmap stringmap.
+
+(** Discrete cofe *)
+Section discrete_cofe.
+  Context `{Equiv A, @Equivalence A (≡)}.
+  Instance discrete_dist : Dist A := λ n x y,
+    match n with 0 => True | S n => x ≡ y end.
+  Instance discrete_compl `{Equiv A} : Compl A := λ c, c 1.
+  Instance discrete_cofe : Cofe A.
+  Proof.
+    split.
+    * intros x y; split; [by intros ? []|intros Hn; apply (Hn 1)].
+    * intros [|n]; [done|apply _].
+    * by intros [|n].
+    * done.
+    * intros c [|n]; [done|apply (chain_cauchy c 1 (S n)); lia].
+  Qed.
+  Definition discreteC : cofeT := CofeT A.
+End discrete_cofe.
+Arguments discreteC _ {_ _}.
+
+(** Later *)
+Inductive later (A : Type) : Type := Later { later_car : A }.
+Arguments Later {_} _.
+Arguments later_car {_} _.
+Section later.
+  Instance later_equiv `{Equiv A} : Equiv (later A) := λ x y,
+    later_car x ≡ later_car y.
+  Instance later_dist `{Dist A} : Dist (later A) := λ n x y,
+    match n with 0 => True | S n => later_car x ={n}= later_car y end.
+  Program Definition later_chain `{Dist A} (c : chain (later A)) : chain A :=
+    {| chain_car n := later_car (c (S n)) |}.
+  Next Obligation. intros A ? c n i ?; apply (chain_cauchy c (S n)); lia. Qed.
+  Instance later_compl `{Compl A} : Compl (later A) := λ c,
+    Later (compl (later_chain c)).
+  Instance later_cofe `{Cofe A} : Cofe (later A).
+  Proof.
+    split.
+    * intros x y; unfold equiv, later_equiv; rewrite !equiv_dist.
+      split. intros Hxy [|n]; [done|apply Hxy]. intros Hxy n; apply (Hxy (S n)).
+    * intros [|n]; [by split|split]; unfold dist, later_dist.
+      + by intros [x].
+      + by intros [x] [y].
+      + by intros [x] [y] [z] ??; transitivity y.
+    * intros [|n] [x] [y] ?; [done|]; unfold dist, later_dist; by apply dist_S.
+    * done.
+    * intros c [|n]; [done|by apply (conv_compl (later_chain c) n)].
+  Qed.
+  Canonical Structure laterC (A : cofeT) : cofeT := CofeT (later A).
+
+  Instance later_fmap : FMap later := λ A B f x, Later (f (later_car x)).
+  Instance later_fmap_ne `{Cofe A, Cofe B} (f : A → B) :
+    (∀ n, Proper (dist n ==> dist n) f) →
+    ∀ n, Proper (dist n ==> dist n) (fmap f : later A → later B).
+  Proof. intros Hf [|n] [x] [y] ?; do 2 red; simpl. done. by apply Hf. Qed.
+  Lemma later_fmap_id {A} (x : later A) : id <$> x = x.
+  Proof. by destruct x. Qed.
+  Lemma later_fmap_compose {A B C} (f : A → B) (g : B → C) (x : later A) :
+    g ∘ f <$> x = g <$> f <$> x.
+  Proof. by destruct x. Qed.
+  Definition laterC_map {A B} (f : A -n> B) : laterC A -n> laterC B :=
+    CofeMor (fmap f : laterC A → laterC B).
+  Instance laterC_contractive (A B : cofeT) : Contractive (@laterC_map A B).
+  Proof. intros n f g Hf n'; apply Hf. Qed.
+End later.
+
+(* Option *)
+Instance option_dist `{Dist A} : Dist (option A) := λ n o1 o2,
+  match n with 0 => True | S n => option_Forall2 (dist n) o1 o2 end.
+Program Definition option_chain `{Dist A}
+    (c : chain (option A)) (x : A) (H : c 1 = Some x) : chain A :=
+  {| chain_car n := from_option x (c (S n)) |}.
+Next Obligation.
+  intros A ? c x ? n i ?.
+  feed inversion (chain_cauchy c 1 (S i)); auto with lia congruence.
+  feed inversion (chain_cauchy c (S n) (S i)); simpl; auto with lia congruence.
+Qed.
+Instance option_compl `{Compl A} : Compl (option A) := λ c,
+  match Some_dec (c 1) with
+  | inleft (exist x H) => Some (compl (option_chain c x H))
+  | inright _ => None
+  end.
+Instance option_cofe `{Cofe A} : Cofe (option A).
+Proof.
+  split.
+  * intros mx my; split.
+    { by destruct 1; intros [|n]; constructor; apply equiv_dist. }
+    intros Hxy; feed inversion (Hxy 1); constructor; apply equiv_dist.
+    intros n. feed inversion (Hxy (S n)); congruence.
+  * intros [|n]; [by split|split].
+    + by intros [x|]; constructor.
+    + by destruct 1; constructor.
+    + by intros [x|] [y|] [z|]; do 2 inversion 1; constructor; transitivity y.
+  * by destruct n; [|destruct 1; constructor; apply dist_S].
+  * done.
+  * intros c [|n]; unfold compl, option_compl; [constructor|].
+    destruct (Some_dec (c 1)) as [[x Hx]|].
+    + assert (is_Some (c (S n))) as [y Hy].
+      { feed inversion (chain_cauchy c 1 (S n)); try congruence; eauto with lia. }
+      rewrite Hy; constructor.
+      by rewrite (conv_compl (option_chain c x Hx) n); simpl; rewrite Hy.
+    + feed inversion (chain_cauchy c 1 (S n)); auto with lia congruence.
+      by constructor.
+Qed.
+Instance Some_ne `{Cofe A} : Proper (dist n ==> dist n) Some.
+Proof. by intros [|n];[done|constructor; apply dist_S]. Qed.
+Instance option_fmap_ne `{Cofe A, Cofe B} (f : A → B) :
+  (∀ n, Proper (dist n ==> dist n) f) →
+  ∀ n, Proper (dist n ==> dist n) (fmap f : option A → option B).
+Proof. intros Hf [|n];[done|destruct 1;constructor;by apply Hf]. Qed.
+
+(** Finite maps *)
+Section map.
+  Context `{FinMap K M}.
+  Instance map_dist `{Dist A} : Dist (M A) := λ n m1 m2,
+    ∀ i, m1 !! i ={n}= m2 !! i.
+  Program Definition map_chain `{Dist A} (c : chain (M A))
+    (k : K) : chain (option A) := {| chain_car n := c n !! k |}.
+  Next Obligation. by intros A ? c k n i ?; apply (chain_cauchy c). Qed.
+  Instance map_compl `{Compl A} : Compl (M A) := λ c,
+    map_imap (λ i _, compl (map_chain c i)) (c 1).
+  Instance map_cofe `{Cofe A} : Cofe (M A).
+  Proof.
+    split.
+    * intros m1 m2; split.
+      + by intros Hm n k; apply equiv_dist.
+      + intros Hm k; apply equiv_dist; intros n; apply Hm.
+    * intros n; split.
+      + by intros m k.
+      + by intros m1 m2 ? k.
+      + by intros m1 m2 m3 ?? k; transitivity (m2 !! k).
+    * by intros n m1 m2 ? k; apply dist_S.
+    * done.
+    * intros c [|n] k; unfold compl, map_compl; [apply dist_0|].
+      rewrite lookup_imap.
+      assert ((∃ x y, c 1 !! k = Some x ∧ c (S n) !! k = Some y) ∨
+        c 1 !! k = None ∧ c (S n) !! k = None) as [(x&y&Hx&Hy)|[-> ->]]
+        by (feed inversion (λ H, chain_cauchy c 1 (S n) H k);
+          eauto with lia congruence); [|done].
+      by rewrite Hx; simpl; rewrite conv_compl; simpl; rewrite Hy.
+  Qed.
+  Instance lookup_ne `{Cofe A} n :
+    Proper ((=) ==> dist n ==> dist n) (lookup : K → M A → option A).
+  Proof. by intros k1 k2 -> m1 m2 Hm; apply Hm. Qed.
+  Instance map_fmap_ne `{Cofe A, Cofe B} (f : A → B) :
+    (∀ n, Proper (dist n ==> dist n) f) →
+    ∀ n, Proper (dist n ==> dist n) (fmap f : M A → M B).
+  Proof. by intros ? n m1 m2 Hm k; rewrite !lookup_fmap, Hm. Qed.
+  Definition mapC (A : cofeT) : cofeT := CofeT (M A).
+  Definition mapC_map {A B} (f: A -n> B) : mapC A -n> mapC B :=
+    CofeMor (fmap f : mapC A → mapC B).
+  Global Instance mapC_map_ne (A B : cofeT) :
+    Proper (dist n ==> dist n) (@mapC_map A B).
+  Proof.
+    intros [|n] f g Hf m k; simpl; rewrite !lookup_fmap; [apply dist_0|].
+    destruct (_ !! k) eqn:?; simpl; constructor; apply dist_S, Hf.
+  Qed.
+End map.
+Arguments mapC {_} _ {_ _ _ _ _ _ _ _ _} _.
+
+Canonical Structure PmapC := mapC Pmap.
+Canonical Structure NmapC := mapC Nmap.
+Canonical Structure ZmapC := mapC Zmap.
+Canonical Structure stringmapC := mapC stringmap.

iris/cofe_solver.v

+Require Export cofe.
+
+Section solver.
+Context (F : cofeT → cofeT → cofeT).
+Context (p : F (CofeT unit) (CofeT unit)).
+Context (map : ∀ {A1 A2 B1 B2 : cofeT},
+  ((A2 -n> A1) * (B1 -n> B2)) → (F A1 B1 -n> F A2 B2)).
+Arguments map {_ _ _ _} _.
+Instance: Params (@map) 4.
+Context (map_id : ∀ {A B : cofeT} (x : F A B), map (cid, cid) x ≡ x).
+Context (map_comp : ∀ {A1 A2 A3 B1 B2 B3 : cofeT}
+    (f : A2 -n> A1) (g : A3 -n> A2) (f' : B1 -n> B2) (g' : B2 -n> B3) x,
+  map (f ◎ g, g' ◎ f') x ≡ map (g,g') (map (f,f') x)).
+Context (map_contractive : ∀ {A1 A2 B1 B2}, Contractive (@map A1 A2 B1 B2)).
+
+Lemma map_ext {A1 A2 B1 B2 : cofeT}
+  (f : A2 -n> A1) (f' : A2 -n> A1) (g : B1 -n> B2) (g' : B1 -n> B2) x x' :
+  (∀ x, f x ≡ f' x) → (∀ y, g y ≡ g' y) → x ≡ x' →
+  map (f,g) x ≡ map (f',g') x'.
+Proof. by rewrite <-!cofe_mor_ext; intros Hf Hg Hx; rewrite Hf, Hg, Hx. Qed.
+
+Fixpoint A (k : nat) : cofeT :=
+  match k with 0 => CofeT unit | S k => F (A k) (A k) end.
+Fixpoint f {k} : A k -n> A (S k) :=
+  match k with 0 => CofeMor (λ _, p) | S k => map (g,f) end
+with g {k} : A (S k) -n> A k :=
+  match k with 0 => CofeMor (λ _, () : CofeT ()) | S k => map (f,g) end.
+Definition f_S k (x : A (S k)) : f x = map (g,f) x := eq_refl.
+Definition g_S k (x : A (S (S k))) : g x = map (f,g) x := eq_refl.
+Lemma gf {k} (x : A k) : g (f x) ≡ x.
+Proof.
+  induction k as [|k IH]; simpl in *; [by destruct x|].
+  rewrite <-map_comp; rewrite <-(map_id _ _ x) at 2; by apply map_ext.
+Qed.
+Lemma fg {n k} (x : A (S k)) : n ≤ k → f (g x) ={n}= x.
+Proof.
+  intros Hnk; apply dist_le with k; auto; clear Hnk.
+  induction k as [|k IH]; simpl; [apply dist_0|].
+  rewrite <-(map_id _ _ x) at 2; rewrite <-map_comp; by apply map_contractive.
+Qed.
+Arguments A _ : simpl never.
+Arguments f {_} : simpl never.
+Arguments g {_} : simpl never.
+
+Record tower := {
+  tower_car k :> A k;
+  g_tower k : g (tower_car (S k)) ≡ tower_car k
+}.
+Instance tower_equiv : Equiv tower := λ X Y, ∀ k, X k ≡ Y k.
+Instance tower_dist : Dist tower := λ n X Y, ∀ k, X k ={n}= Y k.
+Program Definition tower_chain (c : chain tower) (k : nat) : chain (A k) :=
+  {| chain_car i := c i k |}.
+Next Obligation. intros c k n i ?; apply (chain_cauchy c n); lia. Qed.
+Program Instance tower_compl : Compl tower := λ c,
+  {| tower_car n := compl (tower_chain c n) |}.
+Next Obligation.
+  intros c k; apply equiv_dist; intros n.
+  rewrite (conv_compl (tower_chain c k) n).
+  rewrite (conv_compl (tower_chain c (S k)) n); simpl.
+  by rewrite (g_tower (c n) k).
+Qed.
+Instance tower_cofe : Cofe tower.
+Proof.
+  split.
+  * intros X Y; split; [by intros HXY n k; apply equiv_dist|].
+    intros HXY k; apply equiv_dist; intros n; apply HXY.
+  * intros k; split.
+    + by intros X n.
+    + by intros X Y ? n.
+    + by intros X Y Z ?? n; transitivity (Y n).
+  * intros k X Y HXY n; apply dist_S.
+    by rewrite <-(g_tower X), (HXY (S n)), g_tower.
+  * intros X Y k; apply dist_0.
+  * intros c n k; simpl; rewrite (conv_compl (tower_chain c k) n).
+    apply (chain_cauchy c); lia.
+Qed.
+Definition T : cofeT := CofeT tower.
+
+Fixpoint ff {k} (i : nat) : A k -n> A (i + k) :=
+  match i with 0 => cid | S i => f ◎ ff i end.
+Fixpoint gg {k} (i : nat) : A (i + k) -n> A k :=
+  match i with 0 => cid | S i => gg i ◎ g end.
+Lemma ggff {k i} (x : A k) : gg i (ff i x) ≡ x.
+Proof. induction i as [|i IH]; simpl; [done|by rewrite (gf (ff i x)),IH]. Qed.
+Lemma f_tower {n k} (X : tower) : n ≤ k → f (X k) ={n}= X (S k).
+Proof. intros. by rewrite <-(fg (X (S k))), <-(g_tower X). Qed.
+Lemma ff_tower {n} k i (X : tower) : n ≤ k → ff i (X k) ={n}= X (i + k).
+Proof.
+  intros; induction i as [|i IH]; simpl; [done|].
+  by rewrite IH, (f_tower X) by lia.
+Qed.
+Lemma gg_tower k i (X : tower) : gg i (X (i + k)) ≡ X k.
+Proof. by induction i as [|i IH]; simpl; [done|rewrite g_tower, IH]. Qed.
+
+Instance tower_car_ne n k : Proper (dist n ==> dist n) (λ X, tower_car X k).
+Proof. by intros X Y HX. Qed.
+Definition project (k : nat) : T -n> A k := CofeMor (λ X : T, tower_car X k).
+
+Definition coerce {i j} (H : i = j) : A i -n> A j :=
+  eq_rect _ (λ i', A i -n> A i') cid _ H.
+Lemma coerce_id {i} (H : i = i) (x : A i) : coerce H x = x.
+Proof. unfold coerce. by rewrite (proof_irrel H (eq_refl i)). Qed.
+Lemma coerce_proper {i j} (x y : A i) (H1 H2 : i = j) :
+  x = y → coerce H1 x = coerce H2 y.
+Proof. by destruct H1; rewrite !coerce_id. Qed.
+Lemma g_coerce {k j} (H : S k = S j) (x : A (S k)) :
+  g (coerce H x) = coerce (Nat.succ_inj _ _ H) (g x).
+Proof. by assert (k = j) by lia; subst; rewrite !coerce_id. Qed.
+Lemma coerce_f {k j} (H : S k = S j) (x : A k) :
+  coerce H (f x) = f (coerce (Nat.succ_inj _ _ H) x).
+Proof. by assert (k = j) by lia; subst; rewrite !coerce_id. Qed.
+Lemma gg_gg {k i i1 i2 j} (H1 : k = i + j) (H2 : k = i2 + (i1 + j)) (x : A k) :
+  gg i (coerce H1 x) = gg i1 (gg i2 (coerce H2 x)).
+Proof.
+  assert (i = i2 + i1) by lia; simplify_equality'. revert j x H1.
+  induction i2 as [|i2 IH]; intros j X H1; simplify_equality';
+    [by rewrite coerce_id|by rewrite g_coerce, IH].
+Qed.
+Lemma ff_ff {k i i1 i2 j} (H1 : i + k = j) (H2 : i1 + (i2 + k) = j) (x : A k) :
+  coerce H1 (ff i x) = coerce H2 (ff i1 (ff i2 x)).
+Proof.
+  assert (i = i1 + i2) by lia; simplify_equality'.
+  induction i1 as [|i1 IH]; simplify_equality';
+    [by rewrite coerce_id|by rewrite coerce_f, IH].
+Qed.
+
+Definition embed' {k} (i : nat) : A k -n> A i :=
+  match le_lt_dec i k with
+  | left H => gg (k-i) ◎ coerce (eq_sym (Nat.sub_add _ _ H))
+  | right H => coerce (Nat.sub_add k i (Nat.lt_le_incl _ _ H)) ◎ ff (i-k)
+  end.
+Lemma g_embed' {k i} (x : A k) : g (embed' (S i) x) ≡ embed' i x.
+Proof.
+  unfold embed'; destruct (le_lt_dec (S i) k), (le_lt_dec i k); simpl.
+  * symmetry; by erewrite (@gg_gg _ _ 1 (k - S i)); simpl.
+  * exfalso; lia.
+  * assert (i = k) by lia; subst.
+    rewrite (ff_ff _ (eq_refl (1 + (0 + k)))); simpl; rewrite gf.
+    by rewrite (gg_gg _ (eq_refl (0 + (0 + k)))).
+  * assert (H : 1 + ((i - k) + k) = S i) by lia; rewrite (ff_ff _ H); simpl.
+    rewrite <-(gf (ff (i - k) x)) at 2; rewrite g_coerce.
+    by erewrite coerce_proper by done.
+Qed.
+Program Definition embed_inf (k : nat) (x : A k) : T :=
+  {| tower_car n := embed' n x |}.
+Next Obligation. intros k x i. apply g_embed'. Qed.
+Instance embed_inf_ne k n : Proper (dist n ==> dist n) (embed_inf k).
+Proof. by intros x y Hxy i; simpl; rewrite Hxy. Qed.
+Definition embed (k : nat) : A k -n> T := CofeMor (embed_inf k).
+Lemma embed_f k (x : A k) : embed (S k) (f x) ≡ embed k x.
+Proof.
+  rewrite equiv_dist; intros n i.
+  unfold embed_inf, embed; simpl; unfold embed'.
+  destruct (le_lt_dec i (S k)), (le_lt_dec i k); simpl.
+  * assert (H : S k = S (k - i) + (0 + i)) by lia; rewrite (gg_gg _ H); simpl.
+    by erewrite g_coerce, gf, coerce_proper by done.
+  * assert (S k = 0 + (0 + i)) as H by lia.
+    rewrite (gg_gg _ H); simplify_equality'.
+    by rewrite (ff_ff _ (eq_refl (1 + (0 + k)))).
+  * exfalso; lia.
+  * assert (H : (i - S k) + (1 + k) = i) by lia; rewrite (ff_ff _ H); simpl.
+    by erewrite coerce_proper by done.
+Qed.
+Lemma embed_tower j n (X : T) : n ≤ j → embed j (X j) ={n}= X.
+Proof.
+  intros Hn i; simpl; unfold embed'; destruct (le_lt_dec i j) as [H|H]; simpl.
+  * rewrite <-(gg_tower i (j - i) X).
+    apply (_ : Proper (_ ==> _) (gg _)); by destruct (eq_sym _).
+  * rewrite (ff_tower j (i-j) X) by lia; by destruct (Nat.sub_add _ _ _).
+Qed.
+
+Program Definition unfold_chain (X : T) : chain (F T T) :=
+  {| chain_car n := map (project n,embed n) (f (X n)) |}.
+Next Obligation.
+  intros X n i Hi.
+  assert (∃ k, i = k + n) as [k ?] by (exists (i - n); lia); subst; clear Hi.
+  induction k as [|k Hk]; simpl; [done|].
+  rewrite Hk, (f_tower X), f_S, <-map_comp by lia.
+  apply dist_S, map_contractive.
+  split; intros Y; symmetry; apply equiv_dist; [apply g_tower|apply embed_f].
+Qed.
+Definition unfold' (X : T) : F T T := compl (unfold_chain X).
+Instance unfold_ne : Proper (dist n ==> dist n) unfold'.
+Proof.
+  by intros n X Y HXY; unfold unfold'; apply compl_ne; simpl; rewrite (HXY n).
+Qed.
+Definition unfold : T -n> F T T := CofeMor unfold'.
+
+Program Definition fold' (X : F T T) : T :=
+  {| tower_car n := g (map (embed n,project n) X) |}.
+Next Obligation.
+  intros X k; apply (_ : Proper ((≡) ==> (≡)) g).
+  rewrite <-(map_comp _ _ _ _ _ _ (embed (S k)) f (project (S k)) g).
+  apply map_ext; [apply embed_f|intros Y; apply g_tower|done].
+Qed.
+Instance fold_ne : Proper (dist n ==> dist n) fold'.
+Proof. by intros n X Y HXY k; simpl; unfold fold'; simpl; rewrite HXY. Qed.
+Definition fold : F T T -n> T := CofeMor fold'.
+
+Definition fold_unfold X : fold (unfold X) ≡ X.
+Proof.
+  assert (map_ff_gg : ∀ i k (x : A (S i + k)) (H : S i + k = i + S k),
+    map (ff i, gg i) x ≡ gg i (coerce H x)).
+  { intros i; induction i as [|i IH]; intros k x H; simpl.
+    { by rewrite coerce_id, map_id. }
+    rewrite map_comp, g_coerce; apply IH. }
+  rewrite equiv_dist; intros n k; unfold unfold, fold; simpl.
+  rewrite <-g_tower, <-(gg_tower _ n); apply (_ : Proper (_ ==> _) g).
+  transitivity (map (ff n, gg n) (X (S (n + k)))).
+  { unfold unfold'; rewrite (conv_compl (unfold_chain X) n).
+    rewrite (chain_cauchy (unfold_chain X) n (n + k)) by lia; simpl.
+    rewrite (f_tower X), <-map_comp by lia.
+    apply dist_S. apply map_contractive; split; intros x; simpl; unfold embed'.
+    * destruct (le_lt_dec _ _); simpl.
+      { assert (n = 0) by lia; subst. apply dist_0. }
+      by rewrite (ff_ff _ (eq_refl (n + (0 + k)))).
+    * destruct (le_lt_dec _ _); [|exfalso; lia]; simpl.
+      by rewrite (gg_gg _ (eq_refl (0 + (n + k)))). }
+  assert (H: S n + k = n + S k) by lia; rewrite (map_ff_gg _ _ _ H).
+  apply (_ : Proper (_ ==> _) (gg _)); by destruct H.
+Qed.
+Definition unfold_fold X : unfold (fold X) ≡ X.
+Proof.
+  rewrite equiv_dist; intros n; unfold unfold; simpl.
+  unfold unfold'; rewrite (conv_compl (unfold_chain (fold X)) n); simpl.
+  rewrite (fg (map (embed _,project n) X)),
+    <-map_comp by lia; rewrite <-(map_id _ _ X) at 2.
+  apply dist_S, map_contractive; split; intros Y i; apply embed_tower; lia.
+Qed.
+End solver.

iris/dra.v

+Require Export ra.
+
+(** From disjoint pcm *)
+Record validity {A} (P : A → Prop) : Type := Validity {
+  validity_car : A;
+  validity_is_valid : Prop;
+  validity_prf : validity_is_valid → P validity_car
+}.
+Arguments Validity {_ _} _ _ _.
+Arguments validity_car {_ _} _.
+Arguments validity_is_valid {_ _} _.
+
+Definition to_validity {A} {P : A → Prop} (x : A) : validity P :=
+  Validity x (P x) id.
+Instance validity_valid {A} (P : A → Prop) : Valid (validity P) :=
+  validity_is_valid.
+Instance validity_equiv `{Equiv A} (P : A → Prop) : Equiv (validity P) := λ x y,
+  (valid x ↔ valid y) ∧ (valid x → validity_car x ≡ validity_car y).
+Instance validity_equivalence `{Equiv A,!Equivalence ((≡) : relation A)} P :
+  Equivalence ((≡) : relation (validity P)).
+Proof.
+  split; unfold equiv, validity_equiv.
+  * by intros [x px ?]; simpl.
+  * intros [x px ?] [y py ?]; naive_solver.
+  * intros [x px ?] [y py ?] [z pz ?] [? Hxy] [? Hyz]; simpl in *.
+    split; [|intros; transitivity y]; tauto.
+Qed.
+Instance validity_valid_proper `{Equiv A} (P : A → Prop) :
+  Proper ((≡) ==> iff) (valid : validity P → Prop).
+Proof. intros ?? [??]; naive_solver. Qed.
+
+Local Notation V := valid.
+Class DRA A `{Equiv A,Valid A,Unit A,Disjoint A,Op A,Included A, Minus A} := {
+  (* setoids *)
+  dra_equivalence :> Equivalence ((≡) : relation A);
+  dra_op_proper :> Proper ((≡) ==> (≡) ==> (≡)) (⋅);
+  dra_unit_proper :> Proper ((≡) ==> (≡)) unit;
+  dra_disjoint_proper :> ∀ x, Proper ((≡) ==> impl) (disjoint x);
+  dra_minus_proper :> Proper ((≡) ==> (≡) ==> (≡)) minus;
+  dra_included_proper :> Proper ((≡) ==> (≡) ==> impl) included;
+  (* validity *)
+  dra_op_valid x y : V x → V y → x ⊥ y → V (x ⋅ y);
+  dra_unit_valid x : V x → V (unit x);
+  dra_minus_valid x y : V x → V y → x ≼ y → V (y ⩪ x);
+  (* monoid *)
+  dra_associative :> Associative (≡) (⋅);
+  dra_disjoint_ll x y z : V x → V y → V z → x ⊥ y → x ⋅ y ⊥ z → x ⊥ z;
+  dra_disjoint_move_l x y z : V x → V y → V z → x ⊥ y → x ⋅ y ⊥ z → x ⊥ y ⋅ z;
+  dra_symmetric :> Symmetric (@disjoint A _);
+  dra_commutative x y : V x → V y → x ⊥ y → x ⋅ y ≡ y ⋅ x;
+  dra_unit_disjoint_l x : V x → unit x ⊥ x;
+  dra_unit_l x : V x → unit x ⋅ x ≡ x;
+  dra_unit_idempotent x : V x → unit (unit x) ≡ unit x;
+  dra_unit_weaken x y : V x → V y → x ⊥ y → unit x ≼ unit (x ⋅ y);
+  dra_included_l x y : V x → V y → x ⊥ y → x ≼ x ⋅ y;
+  dra_disjoint_difference x y : V x → V y → x ≼ y → x ⊥ y ⩪ x;
+  dra_op_difference x y : V x → V y → x ≼ y → x ⋅ y ⩪ x ≡ y
+}.
+
+Section dra.
+Context A `{DRA A}.
+Arguments valid _ _ !_ /.
+
+Instance: Proper ((≡) ==> (≡) ==> impl) (⊥).
+Proof.
+  intros x1 x2 Hx y1 y2 Hy.
+  by rewrite Hy, (symmetry_iff (⊥) x1), (symmetry_iff (⊥) x2), Hx.
+Qed.
+Lemma dra_disjoint_rl x y z : V x → V y → V z → y ⊥ z → x ⊥ y ⋅ z → x ⊥ y.
+Proof. intros ???. rewrite !(symmetry_iff _ x). by apply dra_disjoint_ll. Qed.
+Lemma dra_disjoint_lr x y z : V x → V y → V z → x ⊥ y → x ⋅ y ⊥ z → y ⊥ z.
+Proof.
+  intros ????. rewrite dra_commutative by done. by apply dra_disjoint_ll.
+Qed.
+Lemma dra_disjoint_move_r x y z :
+  V x → V y → V z → y ⊥ z → x ⊥ y ⋅ z → x ⋅ y ⊥ z.
+Proof.
+  intros; symmetry; rewrite dra_commutative by eauto using dra_disjoint_rl.
+  apply dra_disjoint_move_l; auto; by rewrite dra_commutative.
+Qed.
+Hint Immediate dra_associative dra_commutative dra_unit_disjoint_l
+  dra_unit_l dra_unit_idempotent dra_unit_weaken dra_included_l
+  dra_op_difference dra_disjoint_difference dra_disjoint_rl
+  dra_disjoint_lr dra_disjoint_move_l dra_disjoint_move_r.
+
+Notation T := (validity (valid : A → Prop)).
+Program Instance validity_unit : Unit T := λ x,
+  Validity (unit (validity_car x)) (V x) _.
+Next Obligation. by apply dra_unit_valid, validity_prf. Qed.
+Program Instance validity_op : Op T := λ x y,
+  Validity (validity_car x ⋅ validity_car y)
+           (V x ∧ V y ∧ validity_car x ⊥ validity_car y) _.
+Next Obligation. by apply dra_op_valid; try apply validity_prf. Qed.
+Instance validity_included : Included T := λ x y,
+  V y → V x ∧ validity_car x ≼ validity_car y.
+Program Instance validity_minus : Minus T := λ x y,
+  Validity (validity_car x ⩪ validity_car y)
+           (V x ∧ V y ∧ validity_car y ≼ validity_car x) _.
+Next Obligation. by apply dra_minus_valid; try apply validity_prf. Qed.
+Instance validity_ra : RA T.
+Proof.
+  split.
+  * apply _.
+  * intros ??? [? Heq]; split; simpl; [|by intros (?&?&?); rewrite Heq].
+    split; intros (?&?&?); split_ands';
+      first [by rewrite ?Heq by tauto|by rewrite <-?Heq by tauto|tauto].
+  * by intros ?? [? Heq]; split; [done|]; simpl; intros ?; rewrite Heq.
+  * by intros ?? Heq ?; rewrite <-Heq.
+  * intros x1 x2 [? Hx] y1 y2 [? Hy];
+      split; simpl; [|by intros (?&?&?); rewrite Hx, Hy].
+    split; intros (?&?&?); split_ands'; try tauto.
+    + by rewrite <-Hx, <-Hy by done.
+    + by rewrite Hx, Hy by tauto.
+  * intros ??? [? Heq] Hle; split; [apply Hle; tauto|].
+    rewrite <-Heq by tauto; apply Hle; tauto.
+  * intros [x px ?] [y py ?] [z pz ?];
+      split; simpl; [naive_solver|intros; apply (associative _)].
+  * intros [x px ?] [y py ?]; split; naive_solver.
+  * intros [x px ?]; split; naive_solver.
+  * intros [x px ?]; split; naive_solver.
+  * intros [x px ?] [y py ?]; split; naive_solver.
+  * by intros [x px ?] [y py ?] (?&?&?).
+  * intros [x px ?] [y py ?]; split; naive_solver.
+  * intros [x px ?] [y py ?];
+      unfold included, validity_included; split; naive_solver.
+Qed.
+Definition dra_update (x y : T) :
+  (∀ z, V x → V z → validity_car x ⊥ z → V y ∧ validity_car y ⊥ z) → x ⇝ y.
+Proof.
+  intros Hxy z (?&?&?); split_ands'; auto;
+    eapply Hxy; eauto; by eapply validity_prf.
+Qed.
+End dra.

iris/excl.v

+Require Export cmra.
+Local Arguments disjoint _ _ !_ !_ /.
+Local Arguments included _ _ !_ !_ /.
+
+Inductive excl (A : Type) :=
+  | Excl : A → excl A
+  | ExclUnit : excl A
+  | ExclBot : excl A.
+Arguments Excl {_} _.
+Arguments ExclUnit {_}.
+Arguments ExclBot {_}.
+
+Inductive excl_equiv `{Equiv A} : Equiv (excl A) :=
+  | Excl_equiv (x y : A) : x ≡ y → Excl x ≡ Excl y
+  | ExclUnit_equiv : ExclUnit ≡ ExclUnit
+  | ExclBot_equiv : ExclBot ≡ ExclBot.
+Existing Instance excl_equiv.
+Instance excl_valid {A} : Valid (excl A) := λ x,
+  match x with Excl _ | ExclUnit => True | ExclBot => False end.
+Instance excl_unit {A} : Unit (excl A) := λ _, ExclUnit.
+Instance excl_op {A} : Op (excl A) := λ x y,
+  match x, y with
+  | Excl x, ExclUnit | ExclUnit, Excl x => Excl x
+  | ExclUnit, ExclUnit => ExclUnit
+  | _, _=> ExclBot
+  end.
+Instance excl_minus {A} : Minus (excl A) := λ x y,
+  match x, y with
+  | _, ExclUnit => x
+  | Excl _, Excl _ => ExclUnit
+  | _, _ => ExclBot
+  end.
+Instance excl_included `{Equiv A} : Included (excl A) := λ x y,
+  match x, y with
+  | Excl x, Excl y => x ≡ y
+  | ExclUnit, _ => True
+  | _, ExclBot => True
+  | _, _ => False
+  end.
+Definition excl_above `{Included A} (x : A) (y : excl A) : Prop :=
+  match y with Excl y' => x ≼ y' | ExclUnit => True | ExclBot => False end.
+Instance excl_ra `{Equiv A, !Equivalence (@equiv A _)} : RA (excl A).
+Proof.
+  split.
+  * split.
+    + by intros []; constructor.
+    + by destruct 1; constructor.
+    + destruct 1; inversion 1; constructor; etransitivity; eauto.
+  * by intros []; destruct 1; constructor.
+  * constructor.
+  * by destruct 1.
+  * by do 2 destruct 1; constructor.
+  * by intros []; destruct 1; simpl; try (intros Hx; rewrite Hx).
+  * by intros [?| |] [?| |] [?| |]; constructor.
+  * by intros [?| |] [?| |]; constructor.
+  * by intros [?| |]; constructor.
+  * constructor.
+  * by intros [?| |] [?| |].
+  * by intros [?| |] [?| |].
+  * by intros [?| |] [?| |]; simpl; try constructor.
+  * by intros [?| |] [?| |] ?; try constructor.
+Qed.
+Lemma excl_update {A} (x : A) y : valid y → Excl x ⇝ y.
+Proof. by destruct y; intros ? [?| |]. Qed.
+
+Section excl_above.
+  Context `{RA A}.
+  Global Instance excl_above_proper : Proper ((≡) ==> (≡) ==> iff) excl_above.
+  Proof. by intros ?? Hx; destruct 1 as [?? Hy| |]; simpl; rewrite ?Hx,?Hy. Qed.
+  Lemma excl_above_weaken (a b : A) x y :
+    excl_above b y → a ≼ b → x ≼ y → excl_above a x.
+  Proof.
+    destruct x as [a'| |], y as [b'| |]; simpl; intros ??; try done.
+    by intros Hab; rewrite Hab; transitivity b.
+  Qed.
+End excl_above.
\ No newline at end of file

iris/logic.v

+Require Import cmra cofe_instances.
+Local Hint Extern 1 (_ ≼ _) => etransitivity; [eassumption|].
+Local Hint Extern 1 (_ ≼ _) => etransitivity; [|eassumption].
+Local Hint Extern 10 (_ ≤ _) => omega.
+
+Structure iProp (A : cmraT) : Type := IProp {
+  iprop_holds :> nat → A -> Prop;
+  iprop_ne x1 x2 n : iprop_holds n x1 → x1 ={n}= x2 → iprop_holds n x2;
+  iprop_weaken x1 x2 n1 n2 :
+    x1 ≼ x2 → n2 ≤ n1 → validN n2 x2 → iprop_holds n1 x1 → iprop_holds n2 x2
+}.
+Add Printing Constructor iProp.
+Instance: Params (@iprop_holds) 3.
+
+Instance iprop_equiv (A : cmraT) : Equiv (iProp A) := λ P Q, ∀ x n,
+  validN n x → P n x ↔ Q n x.
+Instance iprop_dist (A : cmraT) : Dist (iProp A) := λ n P Q, ∀ x n',
+  n' < n → validN n' x → P n' x ↔ Q n' x.
+Program Instance iprop_compl (A : cmraT) : Compl (iProp A) := λ c,
+  {| iprop_holds n x := c (S n) n x |}.
+Next Obligation. by intros A c x y n ??; simpl in *; apply iprop_ne with x. Qed.
+Next Obligation.
+  intros A c x1 x2 n1 n2 ????; simpl in *.
+  apply (chain_cauchy c (S n2) (S n1)); eauto using iprop_weaken, cmra_valid_le.
+Qed.
+Instance iprop_cofe (A : cmraT) : Cofe (iProp A).
+Proof.
+  split.
+  * intros P Q; split; [by intros HPQ n x i ??; apply HPQ|].
+    intros HPQ x n ?; apply HPQ with (S n); auto.
+  * intros n; split.
+    + by intros P x i.
+    + by intros P Q HPQ x i ??; symmetry; apply HPQ.
+    + by intros P Q Q' HP HQ x i ??; transitivity (Q i x); [apply HP|apply HQ].
+  * intros n P Q HPQ x i ??; apply HPQ; auto.
+  * intros P Q x i ??; lia.
+  * intros c n x i ??; apply (chain_cauchy c (S i) n); auto.
+Qed.
+Instance iprop_holds_ne {A} (P : iProp A) n : Proper (dist n ==> iff) (P n).
+Proof. intros x1 x2 Hx; split; eauto using iprop_ne. Qed.
+Instance iprop_holds_proper {A} (P : iProp A) n : Proper ((≡) ==> iff) (P n).
+Proof. by intros x1 x2 Hx; apply iprop_holds_ne, equiv_dist. Qed.
+Definition iPropC (A : cmraT) : cofeT := CofeT (iProp A).
+
+(** functor *)
+Program Definition iProp_map {A B : cmraT} (f: B -n> A) `{!CMRAPreserving f}
+  (P : iProp A) : iProp B := {| iprop_holds n x := P n (f x) |}.
+Next Obligation. by intros A B f ? P y1 y2 n ? Hy; simpl; rewrite <-Hy. Qed.
+Next Obligation.
+  by intros A B f ? P y1 y2 n i ???; simpl; apply iprop_weaken; auto;
+    apply validN_preserving || apply included_preserving.
+Qed.
+
+(** logical entailement *)
+Instance iprop_entails {A} : SubsetEq (iProp A) := λ P Q, ∀ x n,
+  validN n x → P n x → Q n x.
+
+(** logical connectives *)
+Program Definition iprop_const {A} (P : Prop) : iProp A :=
+  {| iprop_holds n x := P |}.
+Solve Obligations with done.
+
+Program Definition iprop_and {A} (P Q : iProp A) : iProp A :=
+  {| iprop_holds n x := P n x ∧ Q n x |}.
+Solve Obligations with naive_solver eauto 2 using iprop_ne, iprop_weaken.
+Program Definition iprop_or {A} (P Q : iProp A) : iProp A :=
+  {| iprop_holds n x := P n x ∨ Q n x |}.
+Solve Obligations with naive_solver eauto 2 using iprop_ne, iprop_weaken.
+Program Definition iprop_impl {A} (P Q : iProp A) : iProp A :=
+  {| iprop_holds n x := ∀ x' n',
+       x ≼ x' → n' ≤ n → validN n' x' → P n' x' → Q n' x' |}.
+Next Obligation.
+  intros A P Q x1' x1 n1 HPQ Hx1 x2 n2 ????.
+  destruct (cmra_included_dist_l x1 x2 x1' n1) as (x2'&?&Hx2); auto.
+  assert (x2' ={n2}= x2) as Hx2' by (by apply dist_le with n1).
+  assert (validN n2 x2') by (by rewrite Hx2'); rewrite <-Hx2'.
+  by apply HPQ, iprop_weaken with x2' n2, iprop_ne with x2.
+Qed.
+Next Obligation. naive_solver eauto 2 with lia. Qed.
+
+Program Definition iprop_forall {A B} (P : A → iProp B) : iProp B :=
+  {| iprop_holds n x := ∀ a, P a n x |}.
+Solve Obligations with naive_solver eauto 2 using iprop_ne, iprop_weaken.
+Program Definition iprop_exist {A B} (P : A → iProp B) : iProp B :=
+  {| iprop_holds n x := ∃ a, P a n x |}.
+Solve Obligations with naive_solver eauto 2 using iprop_ne, iprop_weaken.
+
+Program Definition iprop_eq {A} {B : cofeT} (b1 b2 : B) : iProp A :=
+  {| iprop_holds n x := b1 ={n}= b2 |}.
+Solve Obligations with naive_solver eauto 2 using (dist_le (A:=B)).
+
+Program Definition iprop_sep {A} (P Q : iProp A) : iProp A :=
+  {| iprop_holds n x := ∃ x1 x2, x ={n}= x1 ⋅ x2 ∧ P n x1 ∧ Q n x2 |}.
+Next Obligation.
+  by intros A P Q x y n (x1&x2&?&?&?) Hxy; exists x1 x2; rewrite <-Hxy.
+Qed.
+Next Obligation.
+  intros A P Q x y n1 n2 Hxy ?? (x1&x2&Hx&?&?).
+  assert (∃ x2', y ={n2}= x1 ⋅ x2' ∧ x2 ≼ x2') as (x2'&Hy&?).
+  { rewrite ra_included_spec in Hxy; destruct Hxy as [z Hy].
+    exists (x2 ⋅ z); split; eauto using ra_included_l.
+    apply dist_le with n1; auto. by rewrite (associative op), <-Hx, Hy. }
+  exists x1 x2'; split_ands; auto.
+  * apply iprop_weaken with x1 n1; auto.
+    by apply cmra_valid_op_l with x2'; rewrite <-Hy.
+  * apply iprop_weaken with x2 n1; auto.
+    by apply cmra_valid_op_r with x1; rewrite <-Hy.
+Qed.
+
+Program Definition iprop_wand {A} (P Q : iProp A) : iProp A :=
+  {| iprop_holds n x := ∀ x' n',
+       n' ≤ n → validN n' (x ⋅ x') → P n' x' → Q n' (x ⋅ x') |}.
+Next Obligation.
+  intros A P Q x1 x2 n1 HPQ Hx x3 n2 ???; simpl in *.
+  rewrite <-(dist_le _ _ _ _ Hx) by done; apply HPQ; auto.
+  by rewrite (dist_le _ _ _ n2 Hx).
+Qed.
+Next Obligation.
+  intros A P Q x1 x2 n1 n2 ??? HPQ x3 n3 ???; simpl in *.
+  apply iprop_weaken with (x1 ⋅ x3) n3; auto using ra_preserving_r.
+  apply HPQ; auto.
+  apply cmra_valid_included with (x2 ⋅ x3); auto using ra_preserving_r.
+Qed.
+
+Program Definition iprop_later {A} (P : iProp A) : iProp A :=
+  {| iprop_holds n x := match n return _ with 0 => True | S n' => P n' x end |}.
+Next Obligation. intros A P ?? [|n]; eauto using iprop_ne,(dist_le (A:=A)). Qed.
+Next Obligation.
+  intros A P x1 x2 [|n1] [|n2] ????; auto with lia.
+  apply iprop_weaken with x1 n1; eauto using cmra_valid_S.
+Qed.
+Program Definition iprop_always {A} (P : iProp A) : iProp A :=
+  {| iprop_holds n x := P n (unit x) |}.
+Next Obligation. by intros A P x1 x2 n ? Hx; simpl in *; rewrite <-Hx. Qed.
+Next Obligation.
+  intros A P x1 x2 n1 n2 ????; eapply iprop_weaken with (unit x1) n1;
+    auto using ra_unit_preserving, cmra_unit_valid.
+Qed.
+
+Definition iprop_fixpoint {A} (P : iProp A → iProp A)
+  `{!Contractive P} : iProp A := fixpoint P (iprop_const True).
+
+Delimit Scope iprop_scope with I.
+Bind Scope iprop_scope with iProp.
+Arguments iprop_holds {_} _%I _ _.
+
+Notation "'False'" := (iprop_const False) : iprop_scope.
+Notation "'True'" := (iprop_const True) : iprop_scope.
+Infix "∧" := iprop_and : iprop_scope.
+Infix "∨" := iprop_or : iprop_scope.
+Infix "→" := iprop_impl : iprop_scope.
+Infix "★" := iprop_sep (at level 80, right associativity) : iprop_scope.
+Infix "-★" := iprop_wand (at level 90) : iprop_scope.
+Notation "∀ x .. y , P" :=
+  (iprop_forall (λ x, .. (iprop_forall (λ y, P)) ..)) : iprop_scope.
+Notation "∃ x .. y , P" :=
+  (iprop_exist (λ x, .. (iprop_exist (λ y, P)) ..)) : iprop_scope.
+Notation "▷ P" := (iprop_later P) (at level 20) : iprop_scope.
+Notation "□ P" := (iprop_always P) (at level 20) : iprop_scope.
+
+Section logic.
+Context {A : cmraT}.
+Implicit Types P Q : iProp A.
+
+Global Instance iprop_preorder : PreOrder ((⊆) : relation (iProp A)).
+Proof. split. by intros P x i. by intros P Q Q' HP HQ x i ??; apply HQ, HP. Qed.
+Lemma iprop_equiv_spec P Q : P ≡ Q ↔ P ⊆ Q ∧ Q ⊆ P.
+Proof.
+  split.
+  * intros HPQ; split; intros x i; apply HPQ.
+  * by intros [HPQ HQP]; intros x i ?; split; [apply HPQ|apply HQP].
+Qed.
+
+(** Non-expansiveness *)
+Global Instance iprop_const_proper : Proper (iff ==> (≡)) (@iprop_const A).
+Proof. intros P Q HPQ ???; apply HPQ. Qed.
+Global Instance iprop_and_ne n :
+  Proper (dist n ==> dist n ==> dist n) (@iprop_and A).
+Proof.
+  intros P P' HP Q Q' HQ; split; intros [??]; split; by apply HP || by apply HQ.
+Qed.
+Global Instance iprop_or_ne n :
+  Proper (dist n ==> dist n ==> dist n) (@iprop_or A).
+Proof.
+  intros P P' HP Q Q' HQ; split; intros [?|?];
+    first [by left; apply HP | by right; apply HQ].
+Qed.
+Global Instance iprop_impl_ne n :
+  Proper (dist n ==> dist n ==> dist n) (@iprop_impl A).
+Proof.
+  intros P P' HP Q Q' HQ; split; intros HPQ x' n'' ????; apply HQ,HPQ,HP; auto.
+Qed.
+Global Instance iprop_sep_ne n :
+  Proper (dist n ==> dist n ==> dist n) (@iprop_sep A).
+Proof.
+  intros P P' HP Q Q' HQ x n' ? Hx'; split; intros (x1&x2&Hx&?&?);
+    exists x1 x2; rewrite  Hx in Hx'; split_ands; try apply HP; try apply HQ;
+    eauto using cmra_valid_op_l, cmra_valid_op_r.
+Qed.
+Global Instance iprop_wand_ne n :
+  Proper (dist n ==> dist n ==> dist n) (@iprop_wand A).
+Proof.
+  intros P P' HP Q Q' HQ x n' ??; split; intros HPQ x' n'' ???;
+    apply HQ, HPQ, HP; eauto using cmra_valid_op_r.
+Qed.
+Global Instance iprop_eq_ne {B : cofeT} n :
+  Proper (dist n ==> dist n ==> dist n) (@iprop_eq A B).
+Proof.
+  intros x x' Hx y y' Hy z n'; split; intros; simpl in *.
+  * by rewrite <-(dist_le _ _ _ _ Hx), <-(dist_le _ _ _ _ Hy) by auto.
+  * by rewrite (dist_le _ _ _ _ Hx), (dist_le _ _ _ _ Hy) by auto.
+Qed.
+Global Instance iprop_forall_ne {B : cofeT} :
+  Proper (pointwise_relation _ (dist n) ==> dist n) (@iprop_forall B A).
+Proof. by intros n P1 P2 HP12 x n'; split; intros HP a; apply HP12. Qed.
+Global Instance iprop_exists_ne {B : cofeT} :
+  Proper (pointwise_relation _ (dist n) ==> dist n) (@iprop_exist B A).
+Proof.
+  by intros n P1 P2 HP12 x n'; split; intros [a HP]; exists a; apply HP12.
+Qed.
+
+(** Introduction and elimination rules *)
+Lemma iprop_True_intro P : P ⊆ True%I.
+Proof. done. Qed.
+Lemma iprop_False_elim P : False%I ⊆ P.
+Proof. by intros x n ?. Qed.
+Lemma iprop_and_elim_l P Q : (P ∧ Q)%I ⊆ P.
+Proof. by intros x n ? [??]. Qed.
+Lemma iprop_and_elim_r P Q : (P ∧ Q)%I ⊆ Q.
+Proof. by intros x n ? [??]. Qed.
+Lemma iprop_and_intro R P Q : R ⊆ P → R ⊆ Q → R ⊆ (P ∧ Q)%I.
+Proof. intros HP HQ x n ??; split. by apply HP. by apply HQ. Qed.
+Lemma iprop_or_intro_l P Q : P ⊆ (P ∨ Q)%I.
+Proof. by left. Qed.
+Lemma iprop_or_intro_r P Q : Q ⊆ (P ∨ Q)%I.
+Proof. by right. Qed.
+Lemma iprop_or_elim R P Q : P ⊆ R → Q ⊆ R → (P ∨ Q)%I ⊆ R.
+Proof. intros HP HQ x n ? [?|?]. by apply HP. by apply HQ. Qed.
+Lemma iprop_impl_intro P Q R : (R ∧ P)%I ⊆ Q → R ⊆ (P → Q)%I.
+Proof.
+  intros HQ x n ?? x' n' ????; apply HQ; naive_solver eauto using iprop_weaken.
+Qed.
+Lemma iprop_impl_elim P Q : ((P → Q) ∧ P)%I ⊆ Q.
+Proof. by intros x n ? [HQ HP]; apply HQ. Qed.
+Lemma iprop_forall_intro P `(Q: B → iProp A): (∀ b, P ⊆ Q b) → P ⊆ (∀ b, Q b)%I.
+Proof. by intros HPQ x n ?? b; apply HPQ. Qed.
+Lemma iprop_forall_elim `(P : B → iProp A) b : (∀ b, P b)%I ⊆ P b.
+Proof. intros x n ? HP; apply HP. Qed.
+Lemma iprop_exist_intro `(P : B → iProp A) b : P b ⊆ (∃ b, P b)%I.
+Proof. by intros x n ??; exists b. Qed.
+Lemma iprop_exist_elim `(P : B → iProp A) Q : (∀ b, P b ⊆ Q) → (∃ b, P b)%I ⊆ Q.
+Proof. by intros HPQ x n ? [b ?]; apply HPQ with b. Qed.
+
+(* BI connectives *)
+Lemma iprop_sep_elim_l P Q : (P ★ Q)%I ⊆ P.
+Proof.
+  intros x n Hvalid (x1&x2&Hx&?&?); rewrite Hx in Hvalid |- *.
+  by apply iprop_weaken with x1 n; auto using ra_included_l.
+Qed.
+Global Instance iprop_sep_left_id : LeftId (≡) True%I (@iprop_sep A).
+Proof.
+  intros P x n Hvalid; split.
+  * intros (x1&x2&Hx&_&?); rewrite Hx in Hvalid |- *.
+    apply iprop_weaken with x2 n; auto using ra_included_r.
+  * by intros ?; exists (unit x) x; rewrite ra_unit_l.
+Qed. 
+Global Instance iprop_sep_commutative : Commutative (≡) (@iprop_sep A).
+Proof.
+  by intros P Q x n ?; split;
+    intros (x1&x2&?&?&?); exists x2 x1; rewrite (commutative op).
+Qed.
+Global Instance iprop_sep_associative : Associative (≡) (@iprop_sep A).
+Proof.
+  intros P Q R x n ?; split.
+  * intros (x1&x2&Hx&?&y1&y2&Hy&?&?); exists (x1 ⋅ y1) y2; split_ands; auto.
+    + by rewrite <-(associative op), <-Hy, <-Hx.
+    + by exists x1 y1.
+  * intros (x1&x2&Hx&(y1&y2&Hy&?&?)&?); exists y1 (y2 ⋅ x2); split_ands; auto.
+    + by rewrite (associative op), <-Hy, <-Hx.
+    + by exists y2 x2.
+Qed.
+Lemma iprop_wand_intro P Q R : (R ★ P)%I ⊆ Q → R ⊆ (P -★ Q)%I.
+Proof.
+  intros HPQ x n ?? x' n' ???; apply HPQ; auto.
+  exists x x'; split_ands; auto.
+  eapply iprop_weaken with x n; eauto using cmra_valid_op_l.
+Qed.
+Lemma iprop_wand_elim P Q : ((P -★ Q) ★ P)%I ⊆ Q.
+Proof.
+  by intros x n Hvalid (x1&x2&Hx&HPQ&?); rewrite Hx in Hvalid |- *; apply HPQ.
+Qed.
+Lemma iprop_sep_or P Q R : ((P ∨ Q) ★ R)%I ≡ ((P ★ R) ∨ (Q ★ R))%I.
+Proof.
+  split; [by intros (x1&x2&Hx&[?|?]&?); [left|right]; exists x1 x2|].
+  intros [(x1&x2&Hx&?&?)|(x1&x2&Hx&?&?)]; exists x1 x2; split_ands;
+    first [by left | by right | done].
+Qed.
+Lemma iprop_sep_and P Q R : ((P ∧ Q) ★ R)%I ⊆ ((P ★ R) ∧ (Q ★ R))%I.
+Proof. by intros x n ? (x1&x2&Hx&[??]&?); split; exists x1 x2. Qed.
+Lemma iprop_sep_exist {B} (P : B → iProp A) Q :
+  ((∃ b, P b) ★ Q)%I ≡ (∃ b, P b ★ Q)%I.
+Proof.
+  split; [by intros (x1&x2&Hx&[b ?]&?); exists b x1 x2|].
+  intros [b (x1&x2&Hx&?&?)]; exists x1 x2; split_ands; by try exists b.
+Qed.
+Lemma iprop_sep_forall `(P : B → iProp A) Q :
+  ((∀ b, P b) ★ Q)%I ⊆ (∀ b, P b ★ Q)%I.
+Proof. by intros x n ? (x1&x2&Hx&?&?); intros b; exists x1 x2. Qed.
+
+(* Later *)
+Global Instance iprop_later_contractive : Contractive (@iprop_later A).
+Proof.
+  intros n P Q HPQ x [|n'] ??; simpl; [done|].
+  apply HPQ; eauto using cmra_valid_S.
+Qed.
+Lemma iprop_later_weaken P : P ⊆ (▷ P)%I.
+Proof.
+  intros x [|n] ??; simpl in *; [done|].
+  apply iprop_weaken with x (S n); auto using cmra_valid_S.
+Qed.
+Lemma iprop_lub P : (▷ P → P)%I ⊆ P.
+Proof.
+  intros x n ? HP; induction n as [|n IH]; [by apply HP|].
+  apply HP, IH, iprop_weaken with x (S n); eauto using cmra_valid_S.
+Qed.
+Lemma iprop_later_impl P Q : (▷ (P → Q))%I ⊆ (▷ P → ▷ Q)%I.
+Proof.
+  intros x [|n] ? HPQ x' [|n'] ???; auto with lia.
+  apply HPQ; auto using cmra_valid_S.
+Qed.
+Lemma iprop_later_and P Q : (▷ (P ∧ Q))%I ≡ (▷ P ∧ ▷ Q)%I.
+Proof. by intros x [|n]; split. Qed.
+Lemma iprop_later_or P Q : (▷ (P ∨ Q))%I ≡ (▷ P ∨ ▷ Q)%I.
+Proof. intros x [|n]; simpl; tauto. Qed.
+Lemma iprop_later_forall `(P : B → iProp A) : (▷ ∀ b, P b)%I ≡ (∀ b, ▷ P b)%I.
+Proof. by intros x [|n]. Qed.
+Lemma iprop_later_exist `(P : B → iProp A) : (∃ b, ▷ P b)%I ⊆ (▷ ∃ b, P b)%I.
+Proof. by intros x [|n]. Qed.
+Lemma iprop_later_exist' `{Inhabited B} (P : B → iProp A) :
+  (▷ ∃ b, P b)%I ≡ (∃ b, ▷ P b)%I.
+Proof.
+  intros x [|n]; split; try done.
+  by destruct (_ : Inhabited B) as [b]; exists b.
+Qed.
+Lemma iprop_later_sep P Q : (▷ (P ★ Q))%I ≡ (▷ P ★ ▷ Q)%I.
+Proof.
+  intros x n ?; split.
+  * destruct n as [|n]; simpl; [by exists x x|intros (x1&x2&Hx&?&?)].
+    destruct (cmra_extend_op x x1 x2 n)
+      as ([y1 y2]&Hx'&Hy1&Hy2); auto using cmra_valid_S; simpl in *.
+    exists y1 y2; split; [by rewrite Hx'|by rewrite Hy1, Hy2].
+  * destruct n as [|n]; simpl; [done|intros (x1&x2&Hx&?&?)].
+    exists x1 x2; eauto using (dist_S (A:=A)).
+Qed.
+
+(* Always *)
+Lemma iprop_always_necessity P : (□ P)%I ⊆ P.
+Proof.
+  intros x n ??; apply iprop_weaken with (unit x) n;auto using ra_included_unit.
+Qed.
+Lemma iprop_always_intro P Q : (□ P)%I ⊆ Q → (□ P)%I ⊆ (□ Q)%I.
+Proof.
+  intros HPQ x n ??; apply HPQ; simpl in *; auto using cmra_unit_valid.
+  by rewrite ra_unit_idempotent.
+Qed.
+Lemma iprop_always_impl P Q : (□ (P → Q))%I ⊆ (□P → □Q)%I.
+Proof.
+  intros x n ? HPQ x' n' ???.
+  apply HPQ; auto using ra_unit_preserving, cmra_unit_valid.
+Qed.
+Lemma iprop_always_and P Q : (□ (P ∧ Q))%I ≡ (□ P ∧ □ Q)%I.
+Proof. done. Qed.
+Lemma iprop_always_or P Q : (□ (P ∨ Q))%I ≡ (□ P ∨ □ Q)%I.
+Proof. done. Qed.
+Lemma iprop_always_forall `(P : B → iProp A) : (□ ∀ b, P b)%I ≡ (∀ b, □ P b)%I.
+Proof. done. Qed.
+Lemma iprop_always_exist `(P : B → iProp A) : (□ ∃ b, P b)%I ≡ (∃ b, □ P b)%I.
+Proof. done. Qed.
+Lemma iprop_always_and_always_box P Q : (□ P ∧ Q)%I ⊆ (□ P ★ Q)%I.
+Proof.
+  intros x n ? [??]; exists (unit x) x; simpl in *.
+  by rewrite ra_unit_l, ra_unit_idempotent.
+Qed.
+
+(* Fix *)
+Lemma iprop_fixpoint_unfold (P : iProp A → iProp A) `{!Contractive P} :
+  iprop_fixpoint P ≡ P (iprop_fixpoint P).
+Proof. apply fixpoint_unfold. Qed.
+End logic.
+

iris/ra.v

+Require Export collections relations.
+
+Class Valid (A : Type) := valid : A → Prop.
+Instance: Params (@valid) 2.
+
+Class Unit (A : Type) := unit : A → A.
+Instance: Params (@unit) 2.
+
+Class Op (A : Type) := op : A → A → A.
+Instance: Params (@op) 2.
+Infix "⋅" := op (at level 50, left associativity) : C_scope.
+Notation "(⋅)" := op (only parsing) : C_scope.
+
+Class Included (A : Type) := included : relation A.
+Instance: Params (@included) 2.
+Infix "≼" := included (at level 70) : C_scope.
+Notation "(≼)" := included (only parsing) : C_scope.
+Hint Extern 0 (?x ≼ ?x) => reflexivity.
+
+Class Minus (A : Type) := minus : A → A → A.
+Instance: Params (@minus) 2.
+Infix "⩪" := minus (at level 40) : C_scope.
+
+Class RA A `{Equiv A, Valid A, Unit A, Op A, Included A, Minus A} : Prop := {
+  (* setoids *)
+  ra_equivalence :> Equivalence ((≡) : relation A);
+  ra_op_proper x :> Proper ((≡) ==> (≡)) (op x);
+  ra_unit_proper :> Proper ((≡) ==> (≡)) unit;
+  ra_valid_proper :> Proper ((≡) ==> impl) valid;
+  ra_minus_proper :> Proper ((≡) ==> (≡) ==> (≡)) minus;
+  ra_included_proper x :> Proper ((≡) ==> impl) (included x);
+  (* monoid *)
+  ra_associative :> Associative (≡) (⋅);
+  ra_commutative :> Commutative (≡) (⋅);
+  ra_unit_l x : unit x ⋅ x ≡ x;
+  ra_unit_idempotent x : unit (unit x) ≡ unit x;
+  ra_unit_weaken x y : unit x ≼ unit (x ⋅ y);
+  ra_valid_op_l x y : valid (x ⋅ y) → valid x;
+  ra_included_l x y : x ≼ x ⋅ y;
+  ra_op_difference x y : x ≼ y → x ⋅ y ⩪ x ≡ y
+}.
+
+(** Updates *)
+Definition ra_update_set `{Op A, Valid A} (x : A) (P : A → Prop) :=
+  ∀ z, valid (x ⋅ z) → ∃ y, P y ∧ valid (y ⋅ z).
+Instance: Params (@ra_update_set) 3.
+Infix "⇝:" := ra_update_set (at level 70).
+Definition ra_update `{Op A, Valid A} (x y : A) := ∀ z,
+  valid (x ⋅ z) → valid (y ⋅ z).
+Infix "⇝" := ra_update (at level 70).
+Instance: Params (@ra_update) 3.
+
+(** Properties **)
+Section ra.
+Context `{RA A}.
+Implicit Types x y z : A.
+
+Global Instance ra_valid_proper' : Proper ((≡) ==> iff) valid.
+Proof. by intros ???; split; apply ra_valid_proper. Qed.
+Global Instance ra_op_proper' : Proper ((≡) ==> (≡) ==> (≡)) (⋅).
+Proof.
+  intros x1 x2 Hx y1 y2 Hy.
+  by rewrite Hy, (commutative _ x1), Hx, (commutative _ y2).
+Qed.
+Lemma ra_valid_op_r x y : valid (x ⋅ y) → valid y.
+Proof. rewrite (commutative _ x); apply ra_valid_op_l. Qed.
+
+(** ** Units *)
+Lemma ra_unit_r x : x ⋅ unit x ≡ x.
+Proof. by rewrite (commutative _ x), ra_unit_l. Qed.
+
+(** ** Order *)
+Lemma ra_included_spec x y : x ≼ y ↔ ∃ z, y ≡ x ⋅ z.
+Proof.
+  split; [by exists (y ⩪ x); rewrite ra_op_difference|].
+  intros [z Hz]; rewrite Hz; apply ra_included_l.
+Qed.
+Global Instance ra_included_proper' : Proper ((≡) ==> (≡) ==> iff) (≼).
+Proof.
+  intros x1 x2 Hx y1 y2 Hy; rewrite !ra_included_spec.
+  by setoid_rewrite Hx; setoid_rewrite Hy.
+Qed.
+Global Instance: PreOrder included.
+Proof.
+  split.
+  * by intros x; rewrite ra_included_spec; exists (unit x); rewrite ra_unit_r.
+  * intros x y z; rewrite ?ra_included_spec; intros [z1 Hy] [z2 Hz].
+    exists (z1 ⋅ z2). by rewrite (associative _), <-Hy, <-Hz.
+Qed.
+Lemma ra_included_unit x : unit x ≼ x.
+Proof. by rewrite ra_included_spec; exists x; rewrite ra_unit_l. Qed.
+Lemma ra_included_r x y : y ≼ x ⋅ y.
+Proof. rewrite (commutative _); apply ra_included_l. Qed.
+Lemma ra_preserving_l x y z : x ≼ y → z ⋅ x ≼ z ⋅ y.
+Proof.
+  rewrite !ra_included_spec.
+  by intros (z1&Hz1); exists z1; rewrite Hz1, (associative (⋅)).
+Qed.
+Lemma ra_preserving_r x y z : x ≼ y → x ⋅ z ≼ y ⋅ z.
+Proof. by intros; rewrite <-!(commutative _ z); apply ra_preserving_l. Qed.
+Lemma ra_unit_preserving x y : x ≼ y → unit x ≼ unit y.
+Proof.
+  rewrite ra_included_spec; intros [z Hy]; rewrite Hy; apply ra_unit_weaken.
+Qed.
+
+(** ** Properties of [(⇝)] relation *)
+Global Instance ra_update_preorder : PreOrder ra_update.
+Proof. split. by intros x y. intros x y y' ?? z ?; naive_solver. Qed.
+End ra.

iris/sts.v

+Require Export ra.
+Require Import sets stringmap dra.
+Local Arguments valid _ _ !_ /.
+Local Arguments op _ _ !_ !_ /.
+Local Arguments unit _ _ !_ /.
+
+Module sts.
+Inductive t {A} (R : relation A) (tok : A → stringset) :=
+  | auth : A → stringset → t R tok
+  | frag : set A → stringset → t R tok.
+Arguments auth {_ _ _} _ _.
+Arguments frag {_ _ _} _ _.
+
+Section sts_core.
+Context {A} (R : relation A) (tok : A → stringset).
+
+Inductive sts_equiv : Equiv (t R tok) :=
+  | auth_equiv s T1 T2 : T1 = T2 → auth s T1 ≡ auth s T2
+  | frag_equiv S1 S2 T1 T2 : T1 = T2 → S1 ≡ S2 → frag S1 T1 ≡ frag S2 T2.
+Global Existing Instance sts_equiv.
+Inductive step : relation (A * stringset) :=
+  | Step s1 s2 T1 T2 :
+     R s1 s2 → tok s1 ∩ T1 = ∅ → tok s2 ∩ T2 = ∅ → tok s1 ∪ T1 = tok s2 ∪ T2 →
+     step (s1,T1) (s2,T2).
+Hint Resolve Step.
+Inductive frame_step (T : stringset) (s1 s2 : A) : Prop :=
+  | Frame_step T1 T2 :
+     T1 ∩ (tok s1 ∪ T) = ∅ → step (s1,T1) (s2,T2) → frame_step T s1 s2.
+Hint Resolve Frame_step.
+Record closed (T : stringset) (S : set A) : Prop := Closed {
+  closed_disjoint s : s ∈ S → tok s ∩ T = ∅;
+  closed_step s1 s2 : s1 ∈ S → frame_step T s1 s2 → s2 ∈ S
+}.
+Lemma closed_steps S T s1 s2 :
+  closed T S → s1 ∈ S → rtc (frame_step T) s1 s2 → s2 ∈ S.
+Proof. induction 3; eauto using closed_step. Qed.
+Global Instance sts_valid : Valid (t R tok) := λ x,
+  match x with auth s T => tok s ∩ T = ∅ | frag S' T => closed T S' end.
+Definition up (T : stringset) (s : A) : set A := mkSet (rtc (frame_step T) s).
+Definition up_set (T : stringset) (S : set A) : set A := S ≫= up T.
+Global Instance sts_unit : Unit (t R tok) := λ x,
+  match x with
+  | frag S' _ => frag (up_set ∅ S') ∅ | auth s _ => frag (up ∅ s) ∅
+  end.
+Inductive sts_disjoint : Disjoint (t R tok) :=
+  | frag_frag_disjoint S1 S2 T1 T2 : T1 ∩ T2 = ∅ → frag S1 T1 ⊥ frag S2 T2
+  | auth_frag_disjoint s S T1 T2 : s ∈ S → T1 ∩ T2 = ∅ → auth s T1 ⊥ frag S T2
+  | frag_auth_disjoint s S T1 T2 : s ∈ S → T1 ∩ T2 = ∅ → frag S T1 ⊥ auth s T2.
+Global Existing Instance sts_disjoint.
+Global Instance sts_op : Op (t R tok) := λ x1 x2,
+  match x1, x2 with
+  | frag S1 T1, frag S2 T2 => frag (S1 ∩ S2) (T1 ∪ T2)
+  | auth s T1, frag _ T2 => auth s (T1 ∪ T2)
+  | frag _ T1, auth s T2 => auth s (T1 ∪ T2)
+  | auth s T1, auth _ T2 => auth s (T1 ∪ T2) (* never happens *)
+  end.
+Inductive sts_included : Included (t R tok) :=
+  | frag_frag_included S1 S2 T1 T2 S' :
+     T1 ⊆ T2 → S2 ≡ S1 ∩ S' → closed (T2 ∖ T1) S' → frag S1 T1 ≼ frag S2 T2
+  | frag_auth_included s S T1 T2 : s ∈ S → T1 ⊆ T2 → frag S T1 ≼ auth s T2
+  | auth_auth_included s T1 T2 : T1 ⊆ T2 → auth s T1 ≼ auth s T2.
+Global Existing Instance sts_included.
+Global Instance sts_minus : Minus (t R tok) := λ x1 x2,
+  match x1, x2 with
+  | frag S1 T1, frag S2 T2 => frag (up_set (T1 ∖ T2) S1) (T1 ∖ T2)
+  | auth s T1, frag _ T2 => auth s (T1 ∖ T2)
+  | frag _ T2, auth s T1 => auth s (T1 ∖ T2) (* never happens *)
+  | auth s T1, auth _ T2 => frag (up (T1 ∖ T2) s) (T1 ∖ T2)
+  end.
+
+Hint Extern 5 (_ ≡ _) => esolve_elem_of : sts.
+Hint Extern 5 (@eq stringset _ _) => esolve_elem_of : sts.
+Hint Extern 5 (_ ∈ _) => esolve_elem_of : sts.
+Hint Extern 5 (_ ⊆ _) => esolve_elem_of : sts.
+Instance: Equivalence ((≡) : relation (t R tok)).
+Proof.
+  split.
+  * by intros []; constructor.
+  * by destruct 1; constructor.
+  * destruct 1; inversion_clear 1; constructor; etransitivity; eauto.
+Qed.
+Instance closed_proper' T : Proper ((≡) ==> impl) (closed T).
+Proof.
+  intros ?? HS; destruct 1; constructor; intros until 0; rewrite <-?HS; eauto.
+Qed.
+Instance closed_proper T : Proper ((≡) ==> iff) (closed T).
+Proof. by intros ???; split; apply closed_proper'. Qed.
+Lemma closed_op T1 T2 S1 S2 :
+  closed T1 S1 → closed T2 S2 → T1 ∩ T2 = ∅ → closed (T1 ∪ T2) (S1 ∩ S2).
+Proof.
+  intros [? Hstep1] [? Hstep2] ?; split; [esolve_elem_of|].
+  intros s3 s4; rewrite !elem_of_intersection; intros [??] [T ??]; split.
+  * apply Hstep1 with s3; eauto with sts.
+  * apply Hstep2 with s3; eauto with sts.
+Qed.
+Lemma closed_all : closed ∅ set_all.
+Proof. split; auto with sts. Qed.
+Hint Resolve closed_all : sts.
+Instance up_preserving: Proper (flip (⊆) ==> (=) ==> (⊆)) up.
+Proof.
+  intros T T' HT s ? <-; apply elem_of_subseteq.
+  induction 1 as [|s1 s2 s3 [T1 T2]]; [constructor|].
+  eapply rtc_l; [eapply Frame_step with T1 T2|]; eauto with sts.
+Qed.
+Instance up_set_proper T : Proper ((≡) ==> (≡)) (up_set T).
+Proof. intros S1 S2 HS; unfold up_set; auto with sts. Qed.
+Lemma elem_of_up s T : s ∈ up T s.
+Proof. constructor. Qed.
+Lemma subseteq_up_set S T : S ⊆ up_set T S.
+Proof. intros s ?; apply elem_of_bind; eauto using elem_of_up. Qed.
+Lemma closed_up_set S T : (∀ s, s ∈ S → tok s ∩ T = ∅) → closed T (up_set T S).
+Proof.
+  intros HS; unfold up_set; split.
+  * intros s; rewrite !elem_of_bind; intros (s'&Hstep&Hs').
+    specialize (HS s' Hs'); clear Hs' S.
+    induction Hstep as [s|s1 s2 s3 [T1 T2 ? Hstep] ? IH]; auto.
+    inversion_clear Hstep; apply IH; clear IH; auto with sts.
+  * intros s1 s2; rewrite !elem_of_bind; intros (s&?&?) ?; exists s.
+    split; [eapply rtc_r|]; eauto.
+Qed.
+Lemma closed_up_set_empty S : closed ∅ (up_set ∅ S).
+Proof. eauto using closed_up_set with sts. Qed.
+Lemma closed_up s T : tok s ∩ T = ∅ → closed T (up T s).
+Proof.
+  intros. rewrite <-(collection_bind_singleton _ s).
+  apply closed_up_set; auto with sts.
+Qed.
+Lemma closed_up_empty s : closed ∅ (up ∅ s).
+Proof. eauto using closed_up with sts. Qed.
+Lemma up_closed S T : closed T S → up_set T S ≡ S.
+Proof.
+  intros; split; auto using subseteq_up_set; intros s.
+  unfold up_set; rewrite elem_of_bind; intros (s'&Hstep&?).
+  induction Hstep; eauto using closed_step.
+Qed.
+Lemma up_set_subseteq T1 T2 S1 S2 :
+  closed (T2 ∖ T1) S2 → up_set (T2 ∖ T1) (S1 ∩ S2) ⊆ S2.
+Proof.
+  intros ? s2; unfold up_set; rewrite elem_of_bind; intros (s1&?&?).
+  apply closed_steps with (T2 ∖ T1) s1; auto with sts.
+Qed.
+Global Instance sts_dra : DRA (t R tok).
+Proof.
+  split.
+  * apply _.
+  * by do 2 destruct 1; constructor; setoid_subst.
+  * by destruct 1; constructor; setoid_subst.
+  * by intros ? [|]; destruct 1; inversion_clear 1; constructor; setoid_subst.
+  * by do 2 destruct 1; constructor; setoid_subst.
+  * by do 2 destruct 1; inversion_clear 1; econstructor; setoid_subst.
+  * assert (∀ T T' S s,
+      closed T S → s ∈ S → tok s ∩ T' = ∅ → tok s ∩ (T ∪ T') = ∅).
+    { intros S T T' s [??]; esolve_elem_of. }
+    destruct 3; simpl in *; auto using closed_op with sts.
+  * intros []; simpl; eauto using closed_up, closed_up_set with sts.
+  * destruct 3; simpl in *; setoid_subst; eauto using closed_up with sts.
+    eapply closed_up_set; eauto 2 using closed_disjoint with sts.
+  * intros [] [] []; constructor; rewrite ?(associative_L _); auto with sts.
+  * destruct 4; inversion_clear 1; constructor; auto with sts.
+  * destruct 4; inversion_clear 1; constructor; auto with sts.
+  * destruct 1; constructor; auto with sts.
+  * destruct 3; constructor; auto with sts.
+  * intros []; constructor; auto using elem_of_up with sts.
+  * intros [|S T]; constructor; auto with sts.
+    assert (S ⊆ up_set ∅ S); auto using subseteq_up_set with sts.
+  * intros [s T|S T]; constructor; auto with sts.
+    + by rewrite (up_closed (up _ _)) by auto using closed_up with sts.
+    + by rewrite (up_closed (up_set _ _)) by auto using closed_up_set with sts.
+  * destruct 3 as [S1 S2| |]; simpl;
+      match goal with |- _ ≼ frag ?S _ => apply frag_frag_included with S end;
+      rewrite ?difference_diag_L;
+      eauto using closed_up_empty, closed_up_set_empty;
+      unfold up_set; esolve_elem_of.
+  * destruct 3 as [S1 S2 T1 T2| |]; econstructor; eauto with sts.
+    by replace ((T1 ∪ T2) ∖ T1) with T2 by esolve_elem_of.
+  * destruct 3; constructor; eauto using elem_of_up with sts.
+  * destruct 3 as [S1 S2 T1 T2 S'| |]; constructor;
+      rewrite ?(commutative_L _ (_ ∖ _)), <-?union_difference_L; auto with sts.
+    assert (S2 ⊆ up_set (T2 ∖ T1) S2) by eauto using subseteq_up_set.
+    assert (up_set (T2 ∖ T1) (S1 ∩ S') ⊆ S') by eauto using up_set_subseteq.
+    esolve_elem_of.
+Qed.
+Lemma step_closed s1 s2 T1 T2 S Tf :
+  step (s1,T1) (s2,T2) → closed Tf S → s1 ∈ S → T1 ∩ Tf = ∅ →
+  s2 ∈ S ∧ T2 ∩ Tf = ∅ ∧ tok s2 ∩ T2 = ∅.
+Proof.
+  inversion_clear 1 as [???? HR Hs1 Hs2]; intros [? Hstep] ??; split_ands; auto.
+  * eapply Hstep with s1, Frame_step with T1 T2; auto with sts.
+  * clear Hstep Hs1 Hs2; esolve_elem_of.
+Qed.
+End sts_core.
+End sts.
+
+Section sts_ra.
+Context {A} (R : relation A) (tok : A → stringset).
+
+Definition sts := validity (valid : sts.t R tok → Prop).
+Global Instance sts_unit : Unit sts := validity_unit _.
+Global Instance sts_op : Op sts := validity_op _.
+Global Instance sts_included : Included sts := validity_included _.
+Global Instance sts_minus : Minus sts := validity_minus _.
+Global Instance sts_ra : RA sts := validity_ra _.
+Definition sts_auth (s : A) (T : stringset) : sts := to_validity (sts.auth s T).
+Definition sts_frag (S : set A) (T : stringset) : sts :=
+  to_validity (sts.frag S T).
+Lemma sts_update s1 s2 T1 T2 :
+  sts.step R tok (s1,T1) (s2,T2) → sts_auth s1 T1 ⇝ sts_auth s2 T2.
+Proof.
+  intros ?; apply dra_update; inversion 3 as [|? S ? Tf|]; subst.
+  destruct (sts.step_closed R tok s1 s2 T1 T2 S Tf) as (?&?&?); auto.
+  by repeat constructor.
+Qed.
+End sts_ra.

prelude/assoc.v

+(* Copyright (c) 2012-2015, Robbert Krebbers. *)
+(* This file is distributed under the terms of the BSD license. *)
+(** An implementation of finite maps and finite sets using association lists
+ordered by keys. Although the lookup and insert operation are linear-time, the
+main advantage of these association lists compared to search trees, is that it
+has canonical representatives and thus extensional Leibniz equality. Compared
+to a naive unordered association list, the merge operation (used for unions,
+intersections, and difference) is also linear-time. *)
+Require Import mapset.
+Require Export fin_maps.
+
+(** Because the association list is sorted using [strict lexico] instead of
+[lexico], it automatically guarantees that no duplicates exist. *)
+Definition assoc (K : Type) `{Lexico K, !TrichotomyT lexico,
+    !StrictOrder lexico} (A : Type) : Type :=
+  dsig (λ l : list (K * A), StronglySorted lexico (l.*1)).
+
+Section assoc.
+Context `{Lexico K, !StrictOrder lexico,
+  ∀ x y : K, Decision (x = y), !TrichotomyT lexico}.
+
+Infix "⊂" := lexico.
+Notation assoc_before j l := (Forall (lexico j) (l.*1)) (only parsing).
+Notation assoc_wf l := (StronglySorted (lexico) (l.*1)) (only parsing).
+
+Lemma assoc_before_transitive {A} (l : list (K * A)) i j :
+  i ⊂ j → assoc_before j l → assoc_before i l.
+Proof. intros. eapply Forall_impl; eauto. intros. by transitivity j. Qed.
+Hint Resolve assoc_before_transitive.
+
+Hint Extern 1 (StronglySorted _ []) => constructor.
+Hint Extern 1 (StronglySorted _ (_ :: _)) => constructor.
+Hint Extern 1 (Forall _ []) => constructor.
+Hint Extern 1 (Forall _ (_ :: _)) => constructor.
+Hint Extern 100 => progress simpl.
+
+Ltac simplify_assoc := intros;
+  repeat match goal with
+  | H : Forall _ [] |- _ => clear H
+  | H : Forall _ (_ :: _) |- _ => inversion_clear H
+  | H : StronglySorted _ [] |- _ => clear H
+  | H : StronglySorted _ (_ :: _) |- _ => inversion_clear H
+  | _ => progress decompose_elem_of_list
+  | _ => progress simplify_equality'
+  | _ => match goal with |- context [?o ≫= _] => by destruct o end
+  end;
+  repeat first
+  [ progress simplify_order
+  | progress autorewrite with assoc in *; simplify_equality'
+  | destruct (trichotomyT lexico) as [[?|?]|?]; simplify_equality' ];
+  eauto 9.
+
+Fixpoint assoc_lookup_raw {A} (i : K) (l : list (K * A)) : option A :=
+  match l with
+  | [] => None
+  | (j,x) :: l =>
+    match trichotomyT lexico i j with
+    | (**i i ⊂ j *) inleft (left _) => None
+    | (**i i = j *) inleft (right _) => Some x
+    | (**i j ⊂ i *) inright _ => assoc_lookup_raw i l
+    end
+  end.
+Global Instance assoc_lookup {A} : Lookup K A (assoc K A) := λ k m,
+  assoc_lookup_raw k (`m).
+
+Lemma assoc_lookup_before {A} (l : list (K * A)) i :
+  assoc_before i l → assoc_lookup_raw i l = None.
+Proof. induction l as [|[??]]; simplify_assoc. Qed.
+Hint Rewrite @assoc_lookup_before using (by eauto) : assoc.
+
+Lemma assoc_eq {A} (l1 l2 : list (K * A)) :
+  assoc_wf l1 → assoc_wf l2 →
+  (∀ i, assoc_lookup_raw i l1 = assoc_lookup_raw i l2) → l1 = l2.
+Proof.
+  revert l2. induction l1 as [|[i x] l1 IH]; intros [|[j y] l2]; intros ?? E.
+  { done. }
+  { specialize (E j); simplify_assoc; by repeat constructor. }
+  { specialize (E i); simplify_assoc; by repeat constructor. }
+  pose proof (E i); pose proof (E j); simplify_assoc.
+  f_equal. apply IH; auto. intros i'. specialize (E i'); simplify_assoc.
+Qed.
+Definition assoc_empty_wf {A} : assoc_wf (@nil (K * A)).
+Proof. constructor. Qed.
+Global Instance assoc_empty {A} : Empty (assoc K A) := dexist _ assoc_empty_wf.
+
+Definition assoc_cons {A} (i : K) (o : option A) (l : list (K * A)) :
+  list (K * A) := match o with None => l | Some z => (i,z) :: l end.
+Lemma assoc_cons_before {A} (l : list (K * A)) i j o :
+  assoc_before i l → i ⊂ j → assoc_before i (assoc_cons j o l).
+Proof. destruct o; simplify_assoc. Qed.
+Lemma assoc_cons_wf {A} (l : list (K * A)) i o :
+  assoc_wf l → assoc_before i l → assoc_wf (assoc_cons i o l).
+Proof. destruct o; simplify_assoc. Qed.
+Hint Resolve assoc_cons_before assoc_cons_wf.
+Lemma assoc_lookup_cons {A} (l : list (K * A)) i o :
+  assoc_before i l → assoc_lookup_raw i (assoc_cons i o l) = o.
+Proof. destruct o; simplify_assoc. Qed.
+Lemma assoc_lookup_cons_lt {A} (l : list (K * A)) i j o :
+  i ⊂ j → assoc_before i l → assoc_lookup_raw i (assoc_cons j o l) = None.
+Proof. destruct o; simplify_assoc. Qed.
+Lemma assoc_lookup_cons_gt {A} (l : list (K * A)) i j o :
+  j ⊂ i → assoc_lookup_raw i (assoc_cons j o l) = assoc_lookup_raw i l.
+Proof. destruct o; simplify_assoc. Qed.
+Hint Rewrite @assoc_lookup_cons @assoc_lookup_cons_lt
+  @assoc_lookup_cons_gt using (by eauto 8) : assoc.
+
+Fixpoint assoc_alter_raw {A} (f : option A → option A)
+    (i : K) (l : list (K * A)) : list (K * A) :=
+  match l with
+  | [] => assoc_cons i (f None) []
+  | (j,x) :: l =>
+    match trichotomyT lexico i j with
+    | (**i i ⊂ j *) inleft (left _) => assoc_cons i (f None) ((j,x) :: l)
+    | (**i i = j *) inleft (right _) => assoc_cons j (f (Some x)) l
+    | (**i j ⊂ i *) inright _ => (j,x) :: assoc_alter_raw f i l
+    end
+  end.
+Lemma assoc_alter_wf {A} (f : option A → option A) i l :
+  assoc_wf l → assoc_wf (assoc_alter_raw f i l).
+Proof.
+  revert l. assert (∀ j l,
+    j ⊂ i → assoc_before j l → assoc_before j (assoc_alter_raw f i l)).
+  { intros j l. induction l as [|[??]]; simplify_assoc. }
+  intros l. induction l as [|[??]]; simplify_assoc.
+Qed.
+Global Instance assoc_alter {A} : PartialAlter K A (assoc K A) := λ f i m,
+  dexist _ (assoc_alter_wf f i _ (proj2_dsig m)).
+
+Lemma assoc_lookup_raw_alter {A} f (l : list (K * A)) i :
+  assoc_wf l →
+  assoc_lookup_raw i (assoc_alter_raw f i l) = f (assoc_lookup_raw i l).
+Proof. induction l as [|[??]]; simplify_assoc. Qed.
+Lemma assoc_lookup_raw_alter_ne {A} f (l : list (K * A)) i j :
+  assoc_wf l → i ≠ j →
+  assoc_lookup_raw j (assoc_alter_raw f i l) = assoc_lookup_raw j l.
+Proof.
+  induction l as [|[??]]; simplify_assoc; unfold assoc_cons;
+    destruct (f _); simplify_assoc.
+Qed.
+Lemma assoc_fmap_wf {A B} (f : A → B) (l : list (K * A)) :
+  assoc_wf l → assoc_wf (prod_map id f <$> l).
+Proof.
+  intros. by rewrite <-list_fmap_compose,
+    (list_fmap_ext _ fst l l) by (done; by intros []).
+Qed.
+Global Program Instance assoc_fmap: FMap (assoc K) := λ A B f m,
+  dexist _ (assoc_fmap_wf f _ (proj2_dsig m)).
+Lemma assoc_lookup_fmap {A B} (f : A → B) (l : list (K * A)) i :
+  assoc_lookup_raw i (prod_map id f <$> l) = fmap f (assoc_lookup_raw i l).
+Proof. induction l as [|[??]]; simplify_assoc. Qed.
+
+Fixpoint assoc_omap_raw {A B} (f : A → option B)
+    (l : list (K * A)) : list (K * B) :=
+  match l with
+  | [] => []
+  | (i,x) :: l => assoc_cons i (f x) (assoc_omap_raw f l)
+  end.
+Lemma assoc_omap_raw_before {A B} (f : A → option B) l j :
+  assoc_before j l → assoc_before j (assoc_omap_raw f l).
+Proof. induction l as [|[??]]; simplify_assoc. Qed.
+Hint Resolve assoc_omap_raw_before.
+Lemma assoc_omap_wf {A B} (f : A → option B) l :
+  assoc_wf l → assoc_wf (assoc_omap_raw f l).
+Proof. induction l as [|[??]]; simplify_assoc. Qed.
+Hint Resolve assoc_omap_wf.
+Global Instance assoc_omap: OMap (assoc K) := λ A B f m,
+  dexist _ (assoc_omap_wf f _ (proj2_dsig m)).
+Lemma assoc_omap_spec {A B} (f : A → option B) l i :
+  assoc_wf l →
+  assoc_lookup_raw i (assoc_omap_raw f l) = assoc_lookup_raw i l ≫= f.
+Proof. intros. induction l as [|[??]]; simplify_assoc. Qed.
+Hint Rewrite @assoc_omap_spec using (by eauto) : assoc.
+
+Fixpoint assoc_merge_raw {A B C} (f : option A → option B → option C)
+    (l : list (K * A)) : list (K * B) → list (K * C) :=
+  fix go (k : list (K * B)) :=
+  match l, k with
+  | [], _ => assoc_omap_raw (f None ∘ Some) k
+  | _, [] => assoc_omap_raw (flip f None ∘ Some) l
+  | (i,x) :: l, (j,y) :: k =>
+    match trichotomyT lexico i j with
+    | (**i i ⊂ j *) inleft (left _) =>
+      assoc_cons i (f (Some x) None) (assoc_merge_raw f l ((j,y) :: k))
+    | (**i i = j *) inleft (right _) =>
+      assoc_cons i (f (Some x) (Some y)) (assoc_merge_raw f l k)
+    | (**i j ⊂ i *) inright _ =>
+      assoc_cons j (f None (Some y)) (go k)
+    end
+  end.
+Section assoc_merge_raw.
+  Context {A B C} (f : option A → option B → option C).
+  Lemma assoc_merge_nil_l k :
+    assoc_merge_raw f [] k = assoc_omap_raw (f None ∘ Some) k.
+  Proof. by destruct k. Qed.
+  Lemma assoc_merge_nil_r l :
+    assoc_merge_raw f l [] = assoc_omap_raw (flip f None ∘ Some) l.
+  Proof. by destruct l as [|[??]]. Qed.
+  Lemma assoc_merge_cons i x j y l k :
+    assoc_merge_raw f ((i,x) :: l) ((j,y) :: k) =
+      match trichotomyT lexico i j with
+      | (**i i ⊂ j *) inleft (left _) =>
+        assoc_cons i (f (Some x) None) (assoc_merge_raw f l ((j,y) :: k))
+      | (**i i = j *) inleft (right _) =>
+        assoc_cons i (f (Some x) (Some y)) (assoc_merge_raw f l k)
+      | (**i j ⊂ i *) inright _ =>
+        assoc_cons j (f None (Some y)) (assoc_merge_raw f ((i,x) :: l) k)
+      end.
+  Proof. done. Qed.
+End assoc_merge_raw.
+Arguments assoc_merge_raw _ _ _ _ _ _ : simpl never.
+Hint Rewrite @assoc_merge_nil_l @assoc_merge_nil_r @assoc_merge_cons : assoc.
+Lemma assoc_merge_before {A B C} (f : option A → option B → option C) l1 l2 j :
+  assoc_before j l1 → assoc_before j l2 →
+  assoc_before j (assoc_merge_raw f l1 l2).
+Proof.
+  revert l2. induction l1 as [|[??] l1 IH];
+    intros l2; induction l2 as [|[??] l2 IH2]; simplify_assoc.
+Qed.
+Hint Resolve assoc_merge_before.
+Lemma assoc_merge_wf {A B C} (f : option A → option B → option C) l1 l2 :
+  assoc_wf l1 → assoc_wf l2 → assoc_wf (assoc_merge_raw f l1 l2).
+Proof.
+  revert l2. induction l1 as [|[i x] l1 IH];
+    intros l2; induction l2 as [|[j y] l2 IH2]; simplify_assoc.
+Qed.
+Global Instance assoc_merge: Merge (assoc K) := λ A B C f m1 m2,
+  dexist _ (assoc_merge_wf f _ _ (proj2_dsig m1) (proj2_dsig m2)).
+Lemma assoc_merge_spec {A B C} (f : option A → option B → option C) l1 l2 i :
+  f None None = None → assoc_wf l1 → assoc_wf l2 →
+  assoc_lookup_raw i (assoc_merge_raw f l1 l2) =
+    f (assoc_lookup_raw i l1) (assoc_lookup_raw i l2).
+Proof.
+  intros ?. revert l2. induction l1 as [|[??] l1 IH]; intros l2;
+    induction l2 as [|[??] l2 IH2]; simplify_assoc; rewrite ?IH; simplify_assoc.
+Qed.
+
+Global Instance assoc_to_list {A} : FinMapToList K A (assoc K A) := proj1_sig.
+Lemma assoc_to_list_nodup {A} (l : list (K * A)) : assoc_wf l → NoDup l.
+Proof.
+  revert l. assert (∀ i x (l : list (K * A)), assoc_before i l → (i,x) ∉ l).
+  { intros i x l. rewrite Forall_fmap, Forall_forall. intros Hl Hi.
+    destruct (irreflexivity (lexico) i). by apply (Hl (i,x) Hi). }
+  induction l as [|[??]]; simplify_assoc; constructor; auto.
+Qed.
+Lemma assoc_to_list_elem_of {A} (l : list (K * A)) i x :
+  assoc_wf l → (i,x) ∈ l ↔ assoc_lookup_raw i l = Some x.
+Proof.
+  split.
+  * induction l as [|[??]]; simplify_assoc; naive_solver.
+  * induction l as [|[??]]; simplify_assoc; [left| right]; eauto.
+Qed.
+
+(** * Instantiation of the finite map interface *)
+Hint Extern 1 (assoc_wf _) => by apply (bool_decide_unpack _).
+Global Instance: FinMap K (assoc K).
+Proof.
+  split.
+  * intros ? [l1 ?] [l2 ?] ?. apply (sig_eq_pi _), assoc_eq; auto.
+  * done.
+  * intros ?? [??] ?. apply assoc_lookup_raw_alter; auto. 
+  * intros ?? [??] ???. apply assoc_lookup_raw_alter_ne; auto.
+  * intros ??? [??] ?. apply assoc_lookup_fmap.
+  * intros ? [??]. apply assoc_to_list_nodup; auto.
+  * intros ? [??] ??. apply assoc_to_list_elem_of; auto.
+  * intros ??? [??] ?. apply assoc_omap_spec; auto.
+  * intros ????? [??] [??] ?. apply assoc_merge_spec; auto.
+Qed.
+End assoc.
+
+(** * Finite sets *)
+(** We construct finite sets using the above implementation of maps. *)
+Notation assoc_set K := (mapset (assoc K)).
+Instance assoc_map_dom `{Lexico K, !TrichotomyT (@lexico K _),
+  !StrictOrder lexico} {A} : Dom (assoc K A) (assoc_set K) := mapset_dom.
+Instance assoc_map_dom_spec `{Lexico K} `{!TrichotomyT (@lexico K _)}
+    `{!StrictOrder lexico, ∀ x y : K, Decision (x = y)} :
+  FinMapDom K (assoc K) (assoc_set K) := mapset_dom_spec.

prelude/countable.v

+(* Copyright (c) 2012-2015, Robbert Krebbers. *)
+(* This file is distributed under the terms of the BSD license. *)
+Require Export list.
+Local Obligation Tactic := idtac.
+Local Open Scope positive.
+
+Class Countable A `{∀ x y : A, Decision (x = y)} := {
+  encode : A → positive;
+  decode : positive → option A;
+  decode_encode x : decode (encode x) = Some x
+}.
+
+Definition encode_nat `{Countable A} (x : A) : nat :=
+  pred (Pos.to_nat (encode x)).
+Definition decode_nat `{Countable A} (i : nat) : option A :=
+  decode (Pos.of_nat (S i)).
+Lemma decode_encode_nat `{Countable A} x : decode_nat (encode_nat x) = Some x.
+Proof.
+  pose proof (Pos2Nat.is_pos (encode x)).
+  unfold decode_nat, encode_nat. rewrite Nat.succ_pred by lia.
+  by rewrite Pos2Nat.id, decode_encode.
+Qed.
+
+Section choice.
+  Context `{Countable A} (P : A → Prop) `{∀ x, Decision (P x)}.
+
+  Inductive choose_step: relation positive :=
+    | choose_step_None {p} : decode p = None → choose_step (Psucc p) p
+    | choose_step_Some {p x} :
+       decode p = Some x → ¬P x → choose_step (Psucc p) p.
+
+  Lemma choose_step_acc : (∃ x, P x) → Acc choose_step 1%positive.
+  Proof.
+    intros [x Hx]. cut (∀ i p,
+      i ≤ encode x → 1 + encode x = p + i → Acc choose_step p).
+    { intros help. by apply (help (encode x)). }
+    induction i as [|i IH] using Pos.peano_ind; intros p ??.
+    { constructor. intros j. assert (p = encode x) by lia; subst.
+      inversion 1 as [? Hd|?? Hd]; subst;
+        rewrite decode_encode in Hd; congruence. }
+    constructor. intros j.
+    inversion 1 as [? Hd|? y Hd]; subst; auto with lia.
+  Qed.
+
+  Fixpoint choose_go {i} (acc : Acc choose_step i) : A :=
+    match Some_dec (decode i) with
+    | inleft (x↾Hx) =>
+      match decide (P x) with
+      | left _ => x
+      | right H => choose_go (Acc_inv acc (choose_step_Some Hx H))
+      end
+    | inright H => choose_go (Acc_inv acc (choose_step_None H))
+    end.
+  Fixpoint choose_go_correct {i} (acc : Acc choose_step i) : P (choose_go acc).
+  Proof. destruct acc; simpl. repeat case_match; auto. Qed.
+  Fixpoint choose_go_pi {i} (acc1 acc2 : Acc choose_step i) :
+    choose_go acc1 = choose_go acc2.
+  Proof. destruct acc1, acc2; simpl; repeat case_match; auto. Qed.
+
+  Definition choose (H: ∃ x, P x) : A := choose_go (choose_step_acc H).
+  Definition choose_correct (H: ∃ x, P x) : P (choose H) := choose_go_correct _.
+  Definition choose_pi (H1 H2 : ∃ x, P x) :
+    choose H1 = choose H2 := choose_go_pi _ _.
+  Definition choice (HA : ∃ x, P x) : { x | P x } := _↾choose_correct HA.
+End choice.
+
+Lemma surjective_cancel `{Countable A} `{∀ x y : B, Decision (x = y)}
+  (f : A → B) `{!Surjective (=) f} : { g : B → A & Cancel (=) f g }.
+Proof.
+  exists (λ y, choose (λ x, f x = y) (surjective f y)).
+  intros y. by rewrite (choose_correct (λ x, f x = y) (surjective f y)).
+Qed.
+
+(** ** Instances *)
+Program Instance option_countable `{Countable A} : Countable (option A) := {|
+  encode o :=
+    match o with None => 1 | Some x => Pos.succ (encode x) end;
+  decode p :=
+    if decide (p = 1) then Some None else Some <$> decode (Pos.pred p)
+|}.
+Next Obligation.
+  intros ??? [x|]; simpl; repeat case_decide; auto with lia.
+  by rewrite Pos.pred_succ, decode_encode.
+Qed.
+
+Program Instance sum_countable `{Countable A} `{Countable B} :
+  Countable (A + B)%type := {|
+    encode xy :=
+      match xy with inl x => (encode x)~0 | inr y => (encode y)~1 end;
+    decode p :=
+      match p with
+      | 1 => None | p~0 => inl <$> decode p | p~1 => inr <$> decode p
+      end
+  |}.
+Next Obligation. by intros ?????? [x|y]; simpl; rewrite decode_encode. Qed.
+
+Fixpoint prod_encode_fst (p : positive) : positive :=
+  match p with
+  | 1 => 1
+  | p~0 => (prod_encode_fst p)~0~0
+  | p~1 => (prod_encode_fst p)~0~1
+  end.
+Fixpoint prod_encode_snd (p : positive) : positive :=
+  match p with
+  | 1 => 1~0
+  | p~0 => (prod_encode_snd p)~0~0
+  | p~1 => (prod_encode_snd p)~1~0
+  end.
+Fixpoint prod_encode (p q : positive) : positive :=
+  match p, q with
+  | 1, 1 => 1~1
+  | p~0, 1 => (prod_encode_fst p)~1~0
+  | p~1, 1 => (prod_encode_fst p)~1~1
+  | 1, q~0 => (prod_encode_snd q)~0~1
+  | 1, q~1 => (prod_encode_snd q)~1~1
+  | p~0, q~0 => (prod_encode p q)~0~0
+  | p~0, q~1 => (prod_encode p q)~1~0
+  | p~1, q~0 => (prod_encode p q)~0~1
+  | p~1, q~1 => (prod_encode p q)~1~1
+  end.
+Fixpoint prod_decode_fst (p : positive) : option positive :=
+  match p with
+  | p~0~0 => (~0) <$> prod_decode_fst p
+  | p~0~1 => Some match prod_decode_fst p with Some q => q~1 | _ => 1 end
+  | p~1~0 => (~0) <$> prod_decode_fst p
+  | p~1~1 => Some match prod_decode_fst p with Some q => q~1 | _ => 1 end
+  | 1~0 => None
+  | 1~1 => Some 1
+  | 1 => Some 1
+  end.
+Fixpoint prod_decode_snd (p : positive) : option positive :=
+  match p with
+  | p~0~0 => (~0) <$> prod_decode_snd p
+  | p~0~1 => (~0) <$> prod_decode_snd p
+  | p~1~0 => Some match prod_decode_snd p with Some q => q~1 | _ => 1 end
+  | p~1~1 => Some match prod_decode_snd p with Some q => q~1 | _ => 1 end
+  | 1~0 => Some 1
+  | 1~1 => Some 1
+  | 1 => None
+  end.
+
+Lemma prod_decode_encode_fst p q : prod_decode_fst (prod_encode p q) = Some p.
+Proof.
+  assert (∀ p, prod_decode_fst (prod_encode_fst p) = Some p).
+  { intros p'. by induction p'; simplify_option_equality. }
+  assert (∀ p, prod_decode_fst (prod_encode_snd p) = None).
+  { intros p'. by induction p'; simplify_option_equality. }
+  revert q. by induction p; intros [?|?|]; simplify_option_equality.
+Qed.
+Lemma prod_decode_encode_snd p q : prod_decode_snd (prod_encode p q) = Some q.
+Proof.
+  assert (∀ p, prod_decode_snd (prod_encode_snd p) = Some p).
+  { intros p'. by induction p'; simplify_option_equality. }
+  assert (∀ p, prod_decode_snd (prod_encode_fst p) = None).
+  { intros p'. by induction p'; simplify_option_equality. }
+  revert q. by induction p; intros [?|?|]; simplify_option_equality.
+Qed.
+Program Instance prod_countable `{Countable A} `{Countable B} :
+  Countable (A * B)%type := {|
+    encode xy := let (x,y) := xy in prod_encode (encode x) (encode y);
+    decode p :=
+     x ← prod_decode_fst p ≫= decode;
+     y ← prod_decode_snd p ≫= decode; Some (x, y)
+  |}.
+Next Obligation.
+  intros ?????? [x y]; simpl.
+  rewrite prod_decode_encode_fst, prod_decode_encode_snd.
+  csimpl. by rewrite !decode_encode.
+Qed.
+
+Fixpoint list_encode_ (l : list positive) : positive :=
+  match l with [] => 1 | x :: l => prod_encode x (list_encode_ l) end.
+Definition list_encode (l : list positive) : positive :=
+  prod_encode (Pos.of_nat (S (length l))) (list_encode_ l).
+
+Fixpoint list_decode_ (n : nat) (p : positive) : option (list positive) :=
+  match n with
+  | O => guard (p = 1); Some []
+  | S n =>
+     x ← prod_decode_fst p; pl ← prod_decode_snd p;
+     l ← list_decode_ n pl; Some (x :: l)
+  end.
+Definition list_decode (p : positive) : option (list positive) :=
+  pn ← prod_decode_fst p; pl ← prod_decode_snd p;
+  list_decode_ (pred (Pos.to_nat pn)) pl.
+
+Lemma list_decode_encode l : list_decode (list_encode l) = Some l.
+Proof.
+  cut (list_decode_ (length l) (list_encode_ l) = Some l).
+  { intros help. unfold list_decode, list_encode.
+    rewrite prod_decode_encode_fst, prod_decode_encode_snd; csimpl.
+    by rewrite Nat2Pos.id by done; simpl. }
+  induction l; simpl; auto.
+  by rewrite prod_decode_encode_fst, prod_decode_encode_snd;
+    simplify_option_equality.
+Qed.
+
+Program Instance list_countable `{Countable A} : Countable (list A) :=  {|
+  encode l := list_encode (encode <$> l);
+  decode p := list_decode p ≫= mapM decode
+|}.
+Next Obligation.
+  intros ??? l; simpl; rewrite list_decode_encode; simpl.
+  apply mapM_fmap_Some; auto using decode_encode.
+Qed.
+
+Program Instance pos_countable : Countable positive := {|
+  encode := id; decode := Some; decode_encode x := eq_refl
+|}.
+Program Instance N_countable : Countable N := {|
+  encode x := match x with N0 => 1 | Npos p => Pos.succ p end;
+  decode p := if decide (p = 1) then Some 0%N else Some (Npos (Pos.pred p))
+|}.
+Next Obligation.
+  intros [|p]; simpl; repeat case_decide; auto with lia.
+  by rewrite Pos.pred_succ.
+Qed.
+Program Instance Z_countable : Countable Z := {|
+  encode x :=
+    match x with Z0 => 1 | Zpos p => p~0 | Zneg p => p~1 end;
+  decode p := Some
+    match p with 1 => Z0 | p~0 => Zpos p | p~1 => Zneg p end
+|}.
+Next Obligation. by intros [|p|p]. Qed.
+Program Instance nat_countable : Countable nat := {|
+  encode x := encode (N.of_nat x);
+  decode p := N.to_nat <$> decode p
+|}.
+Next Obligation.
+  intros x; lazy beta; rewrite decode_encode; csimpl. by rewrite Nat2N.id.
+Qed.

prelude/decidable.v

+(* Copyright (c) 2012-2015, Robbert Krebbers. *)
+(* This file is distributed under the terms of the BSD license. *)
+(** This file collects theorems, definitions, tactics, related to propositions
+with a decidable equality. Such propositions are collected by the [Decision]
+type class. *)
+Require Export proof_irrel.
+
+Hint Extern 200 (Decision _) => progress (lazy beta) : typeclass_instances.
+
+Lemma dec_stable `{Decision P} : ¬¬P → P.
+Proof. firstorder. Qed.
+
+Lemma Is_true_reflect (b : bool) : reflect b b.
+Proof. destruct b. by left. right. intros []. Qed.
+Instance: Injective (=) (↔) Is_true.
+Proof. intros [] []; simpl; intuition. Qed.
+
+(** We introduce [decide_rel] to avoid inefficienct computation due to eager
+evaluation of propositions by [vm_compute]. This inefficiency occurs if
+[(x = y) := (f x = f y)] as [decide (x = y)] evaluates to [decide (f x = f y)]
+which then might lead to evaluation of [f x] and [f y]. Using [decide_rel]
+we hide [f] under a lambda abstraction to avoid this unnecessary evaluation. *)
+Definition decide_rel {A B} (R : A → B → Prop) {dec : ∀ x y, Decision (R x y)}
+  (x : A) (y : B) : Decision (R x y) := dec x y.
+Lemma decide_rel_correct {A B} (R : A → B → Prop) `{∀ x y, Decision (R x y)}
+  (x : A) (y : B) : decide_rel R x y = decide (R x y).
+Proof. done. Qed.
+
+Lemma decide_True {A} `{Decision P} (x y : A) :
+  P → (if decide P then x else y) = x.
+Proof. by destruct (decide P). Qed.
+Lemma decide_False {A} `{Decision P} (x y : A) :
+  ¬P → (if decide P then x else y) = y.
+Proof. by destruct (decide P). Qed.
+Lemma decide_iff {A} P Q `{Decision P, Decision Q} (x y : A) :
+  (P ↔ Q) → (if decide P then x else y) = (if decide Q then x else y).
+Proof. intros [??]. destruct (decide P), (decide Q); intuition. Qed.
+
+(** The tactic [destruct_decide] destructs a sumbool [dec]. If one of the
+components is double negated, it will try to remove the double negation. *)
+Tactic Notation "destruct_decide" constr(dec) "as" ident(H) :=
+  destruct dec as [H|H];
+  try match type of H with
+  | ¬¬_ => apply dec_stable in H
+  end.
+Tactic Notation "destruct_decide" constr(dec) :=
+  let H := fresh in destruct_decide dec as H.
+
+(** The tactic [case_decide] performs case analysis on an arbitrary occurrence
+of [decide] or [decide_rel] in the conclusion or hypotheses. *)
+Tactic Notation "case_decide" "as" ident(Hd) :=
+  match goal with
+  | H : context [@decide ?P ?dec] |- _ =>
+    destruct_decide (@decide P dec) as Hd
+  | H : context [@decide_rel _ _ ?R ?x ?y ?dec] |- _ =>
+    destruct_decide (@decide_rel _ _ R x y dec) as Hd
+  | |- context [@decide ?P ?dec] =>
+    destruct_decide (@decide P dec) as Hd
+  | |- context [@decide_rel _ _ ?R ?x ?y ?dec] =>
+    destruct_decide (@decide_rel _ _ R x y dec) as Hd
+  end.
+Tactic Notation "case_decide" :=
+  let H := fresh in case_decide as H.
+
+(** The tactic [solve_decision] uses Coq's [decide equality] tactic together
+with instance resolution to automatically generate decision procedures. *)
+Ltac solve_trivial_decision :=
+  match goal with
+  | |- Decision (?P) => apply _
+  | |- sumbool ?P (¬?P) => change (Decision P); apply _
+  end.
+Ltac solve_decision := intros; first
+  [ solve_trivial_decision
+  | unfold Decision; decide equality; solve_trivial_decision ].
+
+(** The following combinators are useful to create Decision proofs in
+combination with the [refine] tactic. *)
+Notation swap_if S := (match S with left H => right H | right H => left H end).
+Notation cast_if S := (if S then left _ else right _).
+Notation cast_if_and S1 S2 := (if S1 then cast_if S2 else right _).
+Notation cast_if_and3 S1 S2 S3 := (if S1 then cast_if_and S2 S3 else right _).
+Notation cast_if_and4 S1 S2 S3 S4 :=
+  (if S1 then cast_if_and3 S2 S3 S4 else right _).
+Notation cast_if_and5 S1 S2 S3 S4 S5 :=
+  (if S1 then cast_if_and4 S2 S3 S4 S5 else right _).
+Notation cast_if_and6 S1 S2 S3 S4 S5 S6 :=
+  (if S1 then cast_if_and5 S2 S3 S4 S5 S6 else right _).
+Notation cast_if_or S1 S2 := (if S1 then left _ else cast_if S2).
+Notation cast_if_or3 S1 S2 S3 := (if S1 then left _ else cast_if_or S2 S3).
+Notation cast_if_not_or S1 S2 := (if S1 then cast_if S2 else left _).
+Notation cast_if_not S := (if S then right _ else left _).
+
+(** We can convert decidable propositions to booleans. *)
+Definition bool_decide (P : Prop) {dec : Decision P} : bool :=
+  if dec then true else false.
+
+Lemma bool_decide_reflect P `{dec : Decision P} : reflect P (bool_decide P).
+Proof. unfold bool_decide. destruct dec. by left. by right. Qed.
+
+Tactic Notation "case_bool_decide" "as" ident (Hd) :=
+  match goal with
+  | H : context [@bool_decide ?P ?dec] |- _ =>
+    destruct_decide (@bool_decide_reflect P dec) as Hd
+  | |- context [@bool_decide ?P ?dec] =>
+    destruct_decide (@bool_decide_reflect P dec) as Hd
+  end.
+Tactic Notation "case_bool_decide" :=
+  let H := fresh in case_bool_decide as H.
+
+Lemma bool_decide_spec (P : Prop) {dec : Decision P} : bool_decide P ↔ P.
+Proof. unfold bool_decide. by destruct dec. Qed.
+Lemma bool_decide_unpack (P : Prop) {dec : Decision P} : bool_decide P → P.
+Proof. by rewrite bool_decide_spec. Qed.
+Lemma bool_decide_pack (P : Prop) {dec : Decision P} : P → bool_decide P.
+Proof. by rewrite bool_decide_spec. Qed.
+Lemma bool_decide_true (P : Prop) `{Decision P} : P → bool_decide P = true.
+Proof. by case_bool_decide. Qed.
+Lemma bool_decide_false (P : Prop) `{Decision P} : ¬P → bool_decide P = false.
+Proof. by case_bool_decide. Qed.
+Lemma bool_decide_iff (P Q : Prop) `{Decision P, Decision Q} :
+  (P ↔ Q) → bool_decide P = bool_decide Q.
+Proof. repeat case_bool_decide; tauto. Qed.
+
+(** * Decidable Sigma types *)
+(** Leibniz equality on Sigma types requires the equipped proofs to be
+equal as Coq does not support proof irrelevance. For decidable we
+propositions we define the type [dsig P] whose Leibniz equality is proof
+irrelevant. That is [∀ x y : dsig P, x = y ↔ `x = `y]. *)
+Definition dsig `(P : A → Prop) `{∀ x : A, Decision (P x)} :=
+  { x | bool_decide (P x) }.
+
+Definition proj2_dsig `{∀ x : A, Decision (P x)} (x : dsig P) : P (`x) :=
+  bool_decide_unpack _ (proj2_sig x).
+Definition dexist `{∀ x : A, Decision (P x)} (x : A) (p : P x) : dsig P :=
+  x↾bool_decide_pack _ p.
+Lemma dsig_eq `(P : A → Prop) `{∀ x, Decision (P x)}
+  (x y : dsig P) : x = y ↔ `x = `y.
+Proof. apply (sig_eq_pi _). Qed.
+Lemma dexists_proj1 `(P : A → Prop) `{∀ x, Decision (P x)} (x : dsig P) p :
+  dexist (`x) p = x.
+Proof. by apply dsig_eq. Qed.
+
+(** * Instances of Decision *)
+(** Instances of [Decision] for operators of propositional logic. *)
+Instance True_dec: Decision True := left I.
+Instance False_dec: Decision False := right (False_rect False).
+Instance Is_true_dec b : Decision (Is_true b).
+Proof. destruct b; apply _. Defined.
+
+Section prop_dec.
+  Context `(P_dec : Decision P) `(Q_dec : Decision Q).
+
+  Global Instance not_dec: Decision (¬P).
+  Proof. refine (cast_if_not P_dec); intuition. Defined.
+  Global Instance and_dec: Decision (P ∧ Q).
+  Proof. refine (cast_if_and P_dec Q_dec); intuition. Defined.
+  Global Instance or_dec: Decision (P ∨ Q).
+  Proof. refine (cast_if_or P_dec Q_dec); intuition. Defined.
+  Global Instance impl_dec: Decision (P → Q).
+  Proof. refine (if P_dec then cast_if Q_dec else left _); intuition. Defined.
+End prop_dec.
+Instance iff_dec `(P_dec : Decision P) `(Q_dec : Decision Q) :
+  Decision (P ↔ Q) := and_dec _ _.
+
+(** Instances of [Decision] for common data types. *)
+Instance bool_eq_dec (x y : bool) : Decision (x = y).
+Proof. solve_decision. Defined.
+Instance unit_eq_dec (x y : unit) : Decision (x = y).
+Proof. solve_decision. Defined.
+Instance prod_eq_dec `(A_dec : ∀ x y : A, Decision (x = y))
+  `(B_dec : ∀ x y : B, Decision (x = y)) (x y : A * B) : Decision (x = y).
+Proof. solve_decision. Defined.
+Instance sum_eq_dec `(A_dec : ∀ x y : A, Decision (x = y))
+  `(B_dec : ∀ x y : B, Decision (x = y)) (x y : A + B) : Decision (x = y).
+Proof. solve_decision. Defined.
+
+Instance curry_dec `(P_dec : ∀ (x : A) (y : B), Decision (P x y)) p :
+    Decision (curry P p) :=
+  match p as p return Decision (curry P p) with
+  | (x,y) => P_dec x y
+  end.
+Instance uncurry_dec `(P_dec : ∀ (p : A * B), Decision (P p)) x y :
+  Decision (uncurry P x y) := P_dec (x,y).
+
+Instance sig_eq_dec `(P : A → Prop) `{∀ x, ProofIrrel (P x)}
+  `{∀ x y : A, Decision (x = y)} (x y : sig P) : Decision (x = y).
+Proof. refine (cast_if (decide (`x = `y))); by rewrite sig_eq_pi. Defined.
+
+(** Some laws for decidable propositions *)
+Lemma not_and_l {P Q : Prop} `{Decision P} : ¬(P ∧ Q) ↔ ¬P ∨ ¬Q.
+Proof. destruct (decide P); tauto. Qed.
+Lemma not_and_r {P Q : Prop} `{Decision Q} : ¬(P ∧ Q) ↔ ¬P ∨ ¬Q.
+Proof. destruct (decide Q); tauto. Qed.
+Lemma not_and_l_alt {P Q : Prop} `{Decision P} : ¬(P ∧ Q) ↔ ¬P ∨ (¬Q ∧ P).
+Proof. destruct (decide P); tauto. Qed.
+Lemma not_and_r_alt {P Q : Prop} `{Decision Q} : ¬(P ∧ Q) ↔ (¬P ∧ Q) ∨ ¬Q.
+Proof. destruct (decide Q); tauto. Qed.

prelude/error.v

+(* Copyright (c) 2012-2015, Robbert Krebbers. *)
+(* This file is distributed under the terms of the BSD license. *)
+Require Export list.
+
+Definition error (S E A : Type) : Type := S → E + (A * S).
+
+Definition error_eval {S E A} (x : error S E A) (s : S) : E + A :=
+  match x s with inl e => inl e | inr (a,_) => inr a end.
+
+Instance error_ret {S E} : MRet (error S E) := λ A x s, inr (x,s).
+Instance error_bind {S E} : MBind (error S E) := λ A B f x s,
+  match x s with
+  | inr (a,s') => f a s'
+  | inl e => inl e
+  end.
+Instance error_fmap {S E} : FMap (error S E) := λ A B f x s,
+  match x s with
+  | inr (a,s') => inr (f a,s')
+  | inl e => inl e
+  end.
+Definition fail {S E A} (e : E) : error S E A := λ s, inl e.
+
+Definition modify {S E} (f : S → S) : error S E () := λ s, inr ((), f s).
+Definition gets {S E A} (f : S → A) : error S E A := λ s, inr (f s, s).
+
+Definition error_guard {E} P {dec : Decision P} {S A}
+    (e : E) (f : P → error S E A) : error S E A :=
+  match decide P with left H => f H | right _ => fail e end.
+Notation "'guard' P 'with' e ; o" := (error_guard P e (λ _, o))
+  (at level 65, only parsing, right associativity) : C_scope.
+Definition error_of_option {S A E} (x : option A) (e : E) : error S E A :=
+  match x with Some a => mret a | None => fail e end.
+
+Lemma error_bind_ret {S E A B} (f : A → error S E B) s s'' x b :
+  (x ≫= f) s = mret b s'' ↔ ∃ a s', x s = mret a s' ∧ f a s' = mret b s''.
+Proof. compute; destruct (x s) as [|[??]]; naive_solver. Qed.
+Lemma error_fmap_ret {S E A B} (f : A → B) s s' (x : error S E A) b :
+  (f <$> x) s = mret b s' ↔ ∃ a, x s = mret a s' ∧ b = f a.
+Proof. compute; destruct (x s) as [|[??]]; naive_solver. Qed.
+Lemma error_of_option_ret {S E A} (s s' : S) (o : option A) (e : E) a :
+  error_of_option o e s = mret a s' ↔ o = Some a ∧ s = s'.
+Proof. compute; destruct o; naive_solver. Qed.
+Lemma error_guard_ret {S E A} `{dec : Decision P} s s' (x : error S E A) e a :
+  (guard P with e ; x) s = mret a s' ↔ P ∧ x s = mret a s'.
+Proof. compute; destruct dec; naive_solver. Qed.
+Lemma error_fmap_bind {S E A B C} (f : A → B) (g : B → error S E C) x s :
+  ((f <$> x) ≫= g) s = (x ≫= g ∘ f) s.
+Proof. by compute; destruct (x s) as [|[??]]. Qed.
+
+Lemma error_associative {S E A B C} (f : A → error S E B) (g : B → error S E C) x s :
+  ((x ≫= f) ≫= g) s = (a ← x; f a ≫= g) s.
+Proof. by compute; destruct (x s) as [|[??]]. Qed.
+Lemma error_of_option_bind {S E A B} (f : A → option B) o e :
+  error_of_option (S := S) (E:=E) (o ≫= f) e
+  = a ← error_of_option o e; error_of_option (f a) e.
+Proof. by destruct o. Qed.
+
+Lemma error_gets_spec {S E A} (g : S → A) s : gets (E:=E) g s = mret (g s) s.
+Proof. done. Qed.
+Lemma error_modify_spec {S E} (g : S → S) s : modify (E:=E) g s = mret () (g s).
+Proof. done. Qed.
+Lemma error_left_gets {S E A B} (g : S → A) (f : A → error S E B) s :
+  (gets (E:=E) g ≫= f) s = f (g s) s.
+Proof. done. Qed.
+Lemma error_left_modify {S E B} (g : S → S) (f : unit → error S E B) s :
+  (modify (E:=E) g ≫= f) s = f () (g s).
+Proof. done. Qed.
+Lemma error_left_id {S E A B} (a : A) (f : A → error S E B) :
+  (mret a ≫= f) = f a.
+Proof. done. Qed.
+
+Ltac generalize_errors :=
+  csimpl;
+  let gen_error e :=
+    try (is_var e; fail 1); generalize e;
+    let x := fresh "err" in intros x in
+  repeat match goal with
+  | |- appcontext[ fail ?e ] => gen_error e
+  | |- appcontext[ error_guard _ ?e ] => gen_error e
+  | |- appcontext[ error_of_option _ ?e ] => gen_error e
+  end.
+Tactic Notation "simplify_error_equality" :=
+  repeat match goal with
+  | H : context [ gets _ _ _ ] |- _ => rewrite error_gets_spec in H
+  | H : context [ modify _ _ _ ] |- _ => rewrite error_modify_spec in H
+  | H : (mret (M:=error _ _) _ ≫= _) _ = _ |- _ => rewrite error_left_id in H
+  | H : (gets _ ≫= _) _ = _ |- _ => rewrite error_left_gets in H
+  | H : (modify _ ≫= _) _ = _ |- _ => rewrite error_left_modify in H
+  | H : error_guard _ _ _ _ = _ |- _ => apply error_guard_ret in H; destruct H
+  | _ => progress simplify_equality'
+  | H : error_of_option _ _ _ = _ |- _ =>
+    apply error_of_option_ret in H; destruct H
+  | H : mbind (M:=error _ _) _ _ _ = _ |- _ =>
+    apply error_bind_ret in H; destruct H as (?&?&?&?)
+  | H : fmap (M:=error _ _) _ _ _ = _ |- _ =>
+    apply error_fmap_ret in H; destruct H as (?&?&?)
+  | H : mbind (M:=option) _ _ = _ |- _ =>
+    apply bind_Some in H; destruct H as (?&?&?)
+  | H : fmap (M:=option) _ _ = _ |- _ =>
+    apply fmap_Some in H; destruct H as (?&?&?)
+  | H : maybe _ ?x = Some _ |- _ => is_var x; destruct x
+  | H : maybe2 _ ?x = Some _ |- _ => is_var x; destruct x
+  | H : maybe3 _ ?x = Some _ |- _ => is_var x; destruct x
+  | H : maybe4 _ ?x = Some _ |- _ => is_var x; destruct x
+  | _ => progress case_decide
+  end.
+
+Tactic Notation "error_proceed" :=
+  repeat match goal with
+  | H : context [ gets _ _ ] |- _ => rewrite error_gets_spec in H
+  | H : context [ modify _ _ ] |- _ => rewrite error_modify_spec in H
+  | H : context [ error_of_option _ _ ] |- _ => rewrite error_of_option_bind in H
+  | H : (mret (M:= _ _) _ ≫= _) _ = _ |- _ => rewrite error_left_id in H
+  | H : (gets _ ≫= _) _ = _ |- _ => rewrite error_left_gets in H
+  | H : (modify _ ≫= _) _ = _ |- _ => rewrite error_left_modify in H
+  | H : ((_ <$> _) ≫= _) _ = _ |- _ => rewrite error_fmap_bind in H
+  | H : ((_ ≫= _) ≫= _) _ = _ |- _ => rewrite error_associative in H
+  | H : (error_guard _ _ _) _ = _ |- _ =>
+     let H' := fresh in apply error_guard_ret in H; destruct H as [H' H]
+  | _ => progress simplify_equality'
+  | H : maybe _ ?x = Some _ |- _ => is_var x; destruct x
+  | H : maybe2 _ ?x = Some _ |- _ => is_var x; destruct x
+  | H : maybe3 _ ?x = Some _ |- _ => is_var x; destruct x
+  | H : maybe4 _ ?x = Some _ |- _ => is_var x; destruct x
+  end.
+Tactic Notation "error_proceed"
+    simple_intropattern(a) "as" simple_intropattern(s) :=
+  error_proceed;
+  lazymatch goal with
+  | H : (error_of_option ?o _ ≫= _) _ = _ |- _ => destruct o as [a|] eqn:?
+  | H : error_of_option ?o _ _ = _ |- _ => destruct o as [a|] eqn:?
+  | H : (_ ≫= _) _ = _ |- _ => apply error_bind_ret in H; destruct H as (a&s&?&H)
+  | H : (_ <$> _) _ = _ |- _ => apply error_fmap_ret in H; destruct H as (a&?&?)
+  end;
+  error_proceed.

prelude/fin_collections.v

+(* Copyright (c) 2012-2015, Robbert Krebbers. *)
+(* This file is distributed under the terms of the BSD license. *)
+(** This file collects definitions and theorems on finite collections. Most
+importantly, it implements a fold and size function and some useful induction
+principles on finite collections . *)
+Require Import Permutation relations listset.
+Require Export numbers collections.
+
+Instance collection_size `{Elements A C} : Size C := length ∘ elements.
+Definition collection_fold `{Elements A C} {B}
+  (f : A → B → B) (b : B) : C → B := foldr f b ∘ elements.
+
+Section fin_collection.
+Context `{FinCollection A C}.
+
+Global Instance elements_proper: Proper ((≡) ==> (≡ₚ)) elements.
+Proof.
+  intros ?? E. apply NoDup_Permutation.
+  * apply NoDup_elements.
+  * apply NoDup_elements.
+  * intros. by rewrite !elem_of_elements, E.
+Qed.
+Global Instance collection_size_proper: Proper ((≡) ==> (=)) size.
+Proof. intros ?? E. apply Permutation_length. by rewrite E. Qed.
+Lemma size_empty : size (∅ : C) = 0.
+Proof.
+  unfold size, collection_size. simpl.
+  rewrite (elem_of_nil_inv (elements ∅)); [done |].
+  intro. rewrite elem_of_elements. solve_elem_of.
+Qed.
+Lemma size_empty_inv (X : C) : size X = 0 → X ≡ ∅.
+Proof.
+  intros. apply equiv_empty. intro. rewrite <-elem_of_elements.
+  rewrite (nil_length_inv (elements X)). by rewrite elem_of_nil. done.
+Qed.
+Lemma size_empty_iff (X : C) : size X = 0 ↔ X ≡ ∅.
+Proof. split. apply size_empty_inv. intros E. by rewrite E, size_empty. Qed.
+Lemma size_non_empty_iff (X : C) : size X ≠ 0 ↔ X ≢ ∅.
+Proof. by rewrite size_empty_iff. Qed.
+Lemma size_singleton (x : A) : size {[ x ]} = 1.
+Proof.
+  change (length (elements {[ x ]}) = length [x]).
+  apply Permutation_length, NoDup_Permutation.
+  * apply NoDup_elements.
+  * apply NoDup_singleton.
+  * intros. by rewrite elem_of_elements,
+      elem_of_singleton, elem_of_list_singleton.
+Qed.
+Lemma size_singleton_inv X x y : size X = 1 → x ∈ X → y ∈ X → x = y.
+Proof.
+  unfold size, collection_size. simpl. rewrite <-!elem_of_elements.
+  generalize (elements X). intros [|? l]; intro; simplify_equality'.
+  rewrite (nil_length_inv l), !elem_of_list_singleton by done. congruence.
+Qed.
+Lemma collection_choose_or_empty X : (∃ x, x ∈ X) ∨ X ≡ ∅.
+Proof.
+  destruct (elements X) as [|x l] eqn:HX; [right|left].
+  * apply equiv_empty. intros x. by rewrite <-elem_of_elements, HX, elem_of_nil.
+  * exists x. rewrite <-elem_of_elements, HX. by left.
+Qed.
+Lemma collection_choose X : X ≢ ∅ → ∃ x, x ∈ X.
+Proof. intros. by destruct (collection_choose_or_empty X). Qed.
+Lemma collection_choose_L `{!LeibnizEquiv C} X : X ≠ ∅ → ∃ x, x ∈ X.
+Proof. unfold_leibniz. apply collection_choose. Qed.
+Lemma size_pos_elem_of X : 0 < size X → ∃ x, x ∈ X.
+Proof.
+  intros Hsz. destruct (collection_choose_or_empty X) as [|HX]; [done|].
+  contradict Hsz. rewrite HX, size_empty; lia.
+Qed.
+Lemma size_1_elem_of X : size X = 1 → ∃ x, X ≡ {[ x ]}.
+Proof.
+  intros E. destruct (size_pos_elem_of X); auto with lia.
+  exists x. apply elem_of_equiv. split.
+  * rewrite elem_of_singleton. eauto using size_singleton_inv.
+  * solve_elem_of.
+Qed.
+Lemma size_union X Y : X ∩ Y ≡ ∅ → size (X ∪ Y) = size X + size Y.
+Proof.
+  intros [E _]. unfold size, collection_size. simpl. rewrite <-app_length.
+  apply Permutation_length, NoDup_Permutation.
+  * apply NoDup_elements.
+  * apply NoDup_app; repeat split; try apply NoDup_elements.
+    intros x. rewrite !elem_of_elements. esolve_elem_of.
+  * intros. rewrite elem_of_app, !elem_of_elements. solve_elem_of.
+Qed.
+Instance elem_of_dec_slow (x : A) (X : C) : Decision (x ∈ X) | 100.
+Proof.
+  refine (cast_if (decide_rel (∈) x (elements X)));
+    by rewrite <-(elem_of_elements _).
+Defined.
+Global Program Instance collection_subseteq_dec_slow (X Y : C) :
+    Decision (X ⊆ Y) | 100 :=
+  match decide_rel (=) (size (X ∖ Y)) 0 with
+  | left E1 => left _ | right E1 => right _
+  end.
+Next Obligation.
+  intros x Ex; apply dec_stable; intro. destruct (proj1 (elem_of_empty x)).
+  apply (size_empty_inv _ E1). by rewrite elem_of_difference.
+Qed.
+Next Obligation.
+  intros E2. destruct E1. apply size_empty_iff, equiv_empty. intros x.
+  rewrite elem_of_difference. intros [E3 ?]. by apply E2 in E3.
+Qed.
+Lemma size_union_alt X Y : size (X ∪ Y) = size X + size (Y ∖ X).
+Proof.
+  rewrite <-size_union by solve_elem_of.
+  setoid_replace (Y ∖ X) with ((Y ∪ X) ∖ X) by esolve_elem_of.
+  rewrite <-union_difference, (commutative (∪)); solve_elem_of.
+Qed.
+Lemma subseteq_size X Y : X ⊆ Y → size X ≤ size Y.
+Proof. intros. rewrite (union_difference X Y), size_union_alt by done. lia. Qed.
+Lemma subset_size X Y : X ⊂ Y → size X < size Y.
+Proof.
+  intros. rewrite (union_difference X Y) by solve_elem_of.
+  rewrite size_union_alt, difference_twice.
+  cut (size (Y ∖ X) ≠ 0); [lia |].
+  by apply size_non_empty_iff, non_empty_difference.
+Qed.
+Lemma collection_wf : wf (strict (@subseteq C _)).
+Proof. apply (wf_projected (<) size); auto using subset_size, lt_wf. Qed.
+Lemma collection_ind (P : C → Prop) :
+  Proper ((≡) ==> iff) P →
+  P ∅ → (∀ x X, x ∉ X → P X → P ({[ x ]} ∪ X)) → ∀ X, P X.
+Proof.
+  intros ? Hemp Hadd. apply well_founded_induction with (⊂).
+  { apply collection_wf. }
+  intros X IH. destruct (collection_choose_or_empty X) as [[x ?]|HX].
+  * rewrite (union_difference {[ x ]} X) by solve_elem_of.
+    apply Hadd. solve_elem_of. apply IH. esolve_elem_of.
+  * by rewrite HX.
+Qed.
+Lemma collection_fold_ind {B} (P : B → C → Prop) (f : A → B → B) (b : B) :
+  Proper ((=) ==> (≡) ==> iff) P →
+  P b ∅ → (∀ x X r, x ∉ X → P r X → P (f x r) ({[ x ]} ∪ X)) →
+  ∀ X, P (collection_fold f b X) X.
+Proof.
+  intros ? Hemp Hadd.
+  cut (∀ l, NoDup l → ∀ X, (∀ x, x ∈ X ↔ x ∈ l) → P (foldr f b l) X).
+  { intros help ?. apply help; [apply NoDup_elements|].
+    symmetry. apply elem_of_elements. }
+  induction 1 as [|x l ?? IH]; simpl.
+  * intros X HX. setoid_rewrite elem_of_nil in HX.
+    rewrite equiv_empty. done. esolve_elem_of.
+  * intros X HX. setoid_rewrite elem_of_cons in HX.
+    rewrite (union_difference {[ x ]} X) by esolve_elem_of.
+    apply Hadd. solve_elem_of. apply IH. esolve_elem_of.
+Qed.
+Lemma collection_fold_proper {B} (R : relation B) `{!Equivalence R}
+    (f : A → B → B) (b : B) `{!Proper ((=) ==> R ==> R) f}
+    (Hf : ∀ a1 a2 b, R (f a1 (f a2 b)) (f a2 (f a1 b))) :
+  Proper ((≡) ==> R) (collection_fold f b).
+Proof. intros ?? E. apply (foldr_permutation R f b); auto. by rewrite E. Qed.
+Global Instance set_Forall_dec `(P : A → Prop)
+  `{∀ x, Decision (P x)} X : Decision (set_Forall P X) | 100.
+Proof.
+  refine (cast_if (decide (Forall P (elements X))));
+    abstract (unfold set_Forall; setoid_rewrite <-elem_of_elements;
+      by rewrite <-Forall_forall).
+Defined.
+Global Instance set_Exists_dec `(P : A → Prop) `{∀ x, Decision (P x)} X :
+  Decision (set_Exists P X) | 100.
+Proof.
+  refine (cast_if (decide (Exists P (elements X))));
+    abstract (unfold set_Exists; setoid_rewrite <-elem_of_elements;
+      by rewrite <-Exists_exists).
+Defined.
+Global Instance rel_elem_of_dec `{∀ x y, Decision (R x y)} x X :
+  Decision (elem_of_upto R x X) | 100 := decide (set_Exists (R x) X).
+End fin_collection.