use coq-stdpp

Makefile

@@ -32,9 +32,9 @@ Makefile.coq: _CoqProject Makefile awk.Makefile
 build-dep:
 	build/opam-pins.sh < opam.pins
 	opam upgrade $(YFLAG) # it is not nice that we upgrade *all* packages here, but I found no nice way to upgrade only those that we pinned
-	opam pin add coq-iris "$$(pwd)#HEAD" -k git -n -y
-	opam install coq-iris --deps-only $(YFLAG)
-	opam pin remove coq-iris
+	opam pin add opam-builddep-temp "$$(pwd)#HEAD" -k git -n -y
+	opam install opam-builddep-temp --deps-only $(YFLAG)
+	opam pin remove opam-builddep-temp
 
 # Some files that do *not* need to be forwarded to Makefile.coq
 Makefile: ;

README.md

@@ -8,10 +8,11 @@ This version is known to compile with:
 
  - Coq 8.6
  - Ssreflect 1.6.1
+ - A development version of [std++](https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp)
 
-The easiest way to install the correct versions of the dependencies is
-through opam. Coq packages are available on the coq-released repository,
-set up by the command:
+The easiest way to install the correct versions of the dependencies is through
+opam.  Coq packages are available on the coq-released repository, set up by the
+command:
 
     opam repo add coq-released https://coq.inria.fr/opam/released
 
@@ -28,8 +29,6 @@ Run `make` to build the full development.
 
 ## Structure
 
-* The folder [prelude](theories/prelude) contains an extended "Standard Library"
-  by [Robbert Krebbers](http://robbertkrebbers.nl/thesis.html).
 * The folder [algebra](theories/algebra) contains the COFE and CMRA
   constructions as well as the solver for recursive domain equations.
 * The folder [base_logic](theories/base_logic) defines the Iris base logic and

_CoqProject

 -Q theories iris
-theories/prelude/option.v
-theories/prelude/fin_map_dom.v
-theories/prelude/bset.v
-theories/prelude/fin_maps.v
-theories/prelude/vector.v
-theories/prelude/pmap.v
-theories/prelude/stringmap.v
-theories/prelude/fin_collections.v
-theories/prelude/mapset.v
-theories/prelude/proof_irrel.v
-theories/prelude/hashset.v
-theories/prelude/pretty.v
-theories/prelude/countable.v
-theories/prelude/orders.v
-theories/prelude/natmap.v
-theories/prelude/strings.v
-theories/prelude/relations.v
-theories/prelude/collections.v
-theories/prelude/listset.v
-theories/prelude/streams.v
-theories/prelude/gmap.v
-theories/prelude/gmultiset.v
-theories/prelude/base.v
-theories/prelude/tactics.v
-theories/prelude/prelude.v
-theories/prelude/listset_nodup.v
-theories/prelude/finite.v
-theories/prelude/numbers.v
-theories/prelude/nmap.v
-theories/prelude/zmap.v
-theories/prelude/coPset.v
-theories/prelude/lexico.v
-theories/prelude/set.v
-theories/prelude/decidable.v
-theories/prelude/list.v
-theories/prelude/functions.v
-theories/prelude/hlist.v
-theories/prelude/sorting.v
 theories/algebra/cmra.v
 theories/algebra/cmra_big_op.v
 theories/algebra/cmra_tactics.v

opam

@@ -15,4 +15,5 @@ remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/iris'" ]
 depends: [
   "coq" { ((>= "8.5.1" & < "8.7~") | (= "dev"))}
   "coq-mathcomp-ssreflect" { ((>= "1.6.1" & < "1.7~") | (= "dev"))}
+  "coq-stdpp"
 ]

opam.pins

+coq-stdpp https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp 2c261344225e46042932f248db87fd1cde04b5cd

theories/algebra/base.v

 From mathcomp Require Export ssreflect.
-From iris.prelude Require Export prelude.
+From stdpp Require Export prelude.
 Set Default Proof Using "Type".
 Global Set Bullet Behavior "Strict Subproofs".
 Global Open Scope general_if_scope.
-Ltac done := prelude.tactics.done.
+Ltac done := stdpp.tactics.done.

theories/algebra/cmra_big_op.v

 From iris.algebra Require Export cmra list.
-From iris.prelude Require Import functions gmap gmultiset.
+From stdpp Require Import functions gmap gmultiset.
 Set Default Proof Using "Type".
 
 (** The operator [ [⋅] Ps ] folds [⋅] over the list [Ps]. This operator is not a

theories/algebra/coPset.v

 From iris.algebra Require Export cmra.
 From iris.algebra Require Import updates local_updates.
-From iris.prelude Require Export collections coPset.
+From stdpp Require Export collections coPset.
 Set Default Proof Using "Type".
 (** This is pretty much the same as algebra/gset, but I was not able to
 generalize the construction without breaking canonical structures. *)

theories/algebra/gmap.v

 From iris.algebra Require Export cmra.
-From iris.prelude Require Export gmap.
+From stdpp Require Export gmap.
 From iris.algebra Require Import updates local_updates.
 From iris.base_logic Require Import base_logic.
 Set Default Proof Using "Type".

theories/algebra/gset.v

 From iris.algebra Require Export cmra.
 From iris.algebra Require Import updates local_updates.
-From iris.prelude Require Export collections gmap mapset.
+From stdpp Require Export collections gmap mapset.
 Set Default Proof Using "Type".
 
 (* The union CMRA *)

theories/algebra/iprod.v

 From iris.algebra Require Export cmra.
 From iris.base_logic Require Import base_logic.
-From iris.prelude Require Import finite.
+From stdpp Require Import finite.
 Set Default Proof Using "Type".
 
 (** * Indexed product *)

theories/algebra/list.v

 From iris.algebra Require Export cmra.
-From iris.prelude Require Export list.
+From stdpp Require Export list.
 From iris.base_logic Require Import base_logic.
 From iris.algebra Require Import updates local_updates.
 Set Default Proof Using "Type".

theories/algebra/sts.v

-From iris.prelude Require Export set.
+From stdpp Require Export set.
 From iris.algebra Require Export cmra.
 From iris.algebra Require Import dra.
 Set Default Proof Using "Type".

theories/algebra/vector.v

-From iris.prelude Require Export vector.
+From stdpp Require Export vector.
 From iris.algebra Require Export ofe.
 From iris.algebra Require Import list.
 Set Default Proof Using "Type".

theories/base_logic/big_op.v

 From iris.algebra Require Export list cmra_big_op.
 From iris.base_logic Require Export base_logic.
-From iris.prelude Require Import gmap fin_collections gmultiset functions.
+From stdpp Require Import gmap fin_collections gmultiset functions.
 Set Default Proof Using "Type".
 Import uPred.
 

theories/base_logic/hlist.v

-From iris.prelude Require Export hlist.
+From stdpp Require Export hlist.
 From iris.base_logic Require Export base_logic.
 Set Default Proof Using "Type".
 Import uPred.

theories/base_logic/lib/fancy_updates.v

 From iris.base_logic.lib Require Export own.
-From iris.prelude Require Export coPset.
+From stdpp Require Export coPset.
 From iris.base_logic.lib Require Import wsat.
 From iris.algebra Require Import gmap.
 From iris.base_logic Require Import big_op.

theories/base_logic/lib/fractional.v

-From iris.prelude Require Import gmap gmultiset.
+From stdpp Require Import gmap gmultiset.
 From iris.base_logic Require Export derived.
 From iris.base_logic Require Import big_op.
 From iris.proofmode Require Import classes class_instances.

theories/base_logic/lib/namespaces.v

-From iris.prelude Require Export countable coPset.
+From stdpp Require Export countable coPset.
 From iris.algebra Require Export base.
 Set Default Proof Using "Type".
 

theories/base_logic/lib/saved_prop.v

 From iris.base_logic Require Export own.
 From iris.algebra Require Import agree.
-From iris.prelude Require Import gmap.
+From stdpp Require Import gmap.
 Set Default Proof Using "Type".
 Import uPred.
 

theories/base_logic/lib/wsat.v

 From iris.base_logic.lib Require Export own.
-From iris.prelude Require Export coPset.
+From stdpp Require Export coPset.
 From iris.algebra Require Import gmap auth agree gset coPset.
 From iris.base_logic Require Import big_op.
 From iris.proofmode Require Import tactics.

theories/base_logic/tactics.v

-From iris.prelude Require Import gmap.
+From stdpp Require Import gmap.
 From iris.base_logic Require Export base_logic big_op.
 Set Default Proof Using "Type".
 Import uPred.

theories/heap_lang/lang.v

 From iris.program_logic Require Export ectx_language ectxi_language.
 From iris.algebra Require Export ofe.
-From iris.prelude Require Export strings.
-From iris.prelude Require Import gmap.
+From stdpp Require Export strings.
+From stdpp Require Import gmap.
 Set Default Proof Using "Type".
 
 Module heap_lang.

theories/heap_lang/lib/barrier/proof.v

 From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Export lang.
 From iris.heap_lang.lib.barrier Require Export barrier.
-From iris.prelude Require Import functions.
+From stdpp Require Import functions.
 From iris.base_logic Require Import big_op lib.saved_prop lib.sts.
 From iris.heap_lang Require Import proofmode.
 From iris.heap_lang.lib.barrier Require Import protocol.

theories/heap_lang/lib/barrier/protocol.v

 From iris.algebra Require Export sts.
 From iris.base_logic Require Import lib.own.
-From iris.prelude Require Export gmap.
+From stdpp Require Export gmap.
 Set Default Proof Using "Type".
 
 (** The STS describing the main barrier protocol. Every state has an index-set

theories/heap_lang/lifting.v

@@ -4,7 +4,7 @@ From iris.program_logic Require Import ectx_lifting.
 From iris.heap_lang Require Export lang.
 From iris.heap_lang Require Import tactics.
 From iris.proofmode Require Import tactics.
-From iris.prelude Require Import fin_maps.
+From stdpp Require Import fin_maps.
 Set Default Proof Using "Type".
 Import uPred.
 

theories/prelude/bset.v

-(* Copyright (c) 2012-2017, Robbert Krebbers. *)
-(* This file is distributed under the terms of the BSD license. *)
-(** This file implements bsets as functions into Prop. *)
-From iris.prelude Require Export prelude.
-Set Default Proof Using "Type".
-
-Record bset (A : Type) : Type := mkBSet { bset_car : A → bool }.
-Arguments mkBSet {_} _.
-Arguments bset_car {_} _ _.
-Instance bset_top {A} : Top (bset A) := mkBSet (λ _, true).
-Instance bset_empty {A} : Empty (bset A) := mkBSet (λ _, false).
-Instance bset_singleton `{EqDecision A} : Singleton A (bset A) := λ x,
-  mkBSet (λ y, bool_decide (y = x)).
-Instance bset_elem_of {A} : ElemOf A (bset A) := λ x X, bset_car X x.
-Instance bset_union {A} : Union (bset A) := λ X1 X2,
-  mkBSet (λ x, bset_car X1 x || bset_car X2 x).
-Instance bset_intersection {A} : Intersection (bset A) := λ X1 X2,
-  mkBSet (λ x, bset_car X1 x && bset_car X2 x).
-Instance bset_difference {A} : Difference (bset A) := λ X1 X2,
-  mkBSet (λ x, bset_car X1 x && negb (bset_car X2 x)).
-Instance bset_collection `{EqDecision A} : Collection A (bset A).
-Proof.
-  split; [split| |].
-  - by intros x ?.
-  - by intros x y; rewrite <-(bool_decide_spec (x = y)).
-  - split. apply orb_prop_elim. apply orb_prop_intro.
-  - split. apply andb_prop_elim. apply andb_prop_intro.
-  - intros X Y x; unfold elem_of, bset_elem_of; simpl. 
-    destruct (bset_car X x), (bset_car Y x); simpl; tauto.
-Qed.
-Instance bset_elem_of_dec {A} x (X : bset A) : Decision (x ∈ X) := _.
-
-Typeclasses Opaque bset_elem_of.
-Global Opaque bset_empty bset_singleton bset_union
-  bset_intersection bset_difference.

theories/prelude/decidable.v

-(* Copyright (c) 2012-2017, 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. *)
-From iris.prelude Require Export proof_irrel.
-Set Default Proof Using "Type*".
-
-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. left; constructor. right. intros []. Qed.
-Instance: Inj (=) (↔) 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. reflexivity. Qed.
-
-Lemma decide_True {A} `{Decision P} (x y : A) :
-  P → (if decide P then x else y) = x.
-Proof. destruct (decide P); tauto. Qed.
-Lemma decide_False {A} `{Decision P} (x y : A) :
-  ¬P → (if decide P then x else y) = y.
-Proof. destruct (decide P); tauto. 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); tauto. Qed.
-
-Lemma decide_left`{Decision P, !ProofIrrel P} (HP : P) : decide P = left HP.
-Proof. destruct (decide P) as [?|?]; [|contradiction]. f_equal. apply proof_irrel. Qed.
-Lemma decide_right`{Decision P} `{!ProofIrrel (¬ P)} (HP : ¬ P) : decide P = right HP.
-Proof. destruct (decide P) as [?|?]; [contradiction|]. f_equal. apply proof_irrel. 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; [left|right]; assumption. 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. destruct dec; simpl; tauto. Qed.
-Lemma bool_decide_unpack (P : Prop) {dec : Decision P} : bool_decide P → P.
-Proof. rewrite bool_decide_spec; trivial. Qed.
-Lemma bool_decide_pack (P : Prop) {dec : Decision P} : P → bool_decide P.
-Proof. rewrite bool_decide_spec; trivial. Qed.
-Hint Resolve bool_decide_pack.
-Lemma bool_decide_true (P : Prop) `{Decision P} : P → bool_decide P = true.
-Proof. case_bool_decide; tauto. Qed.
-Lemma bool_decide_false (P : Prop) `{Decision P} : ¬P → bool_decide P = false.
-Proof. case_bool_decide; tauto. 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. apply dsig_eq; reflexivity. 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; simpl; 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 : EqDecision bool.
-Proof. solve_decision. Defined.
-Instance unit_eq_dec : EqDecision unit.
-Proof. solve_decision. Defined.
-Instance prod_eq_dec `{EqDecision A, EqDecision B} : EqDecision (A * B).
-Proof. solve_decision. Defined.
-Instance sum_eq_dec `{EqDecision A, EqDecision B} : EqDecision (A + B).
-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 sig_eq_dec `(P : A → Prop) `{∀ x, ProofIrrel (P x), EqDecision A} :
-  EqDecision (sig P).
-Proof.
- refine (λ x y, cast_if (decide (`x = `y))); rewrite sig_eq_pi; trivial.
-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.

theories/prelude/fin_map_dom.v

-(* Copyright (c) 2012-2017, Robbert Krebbers. *)
-(* This file is distributed under the terms of the BSD license. *)
-(** This file provides an axiomatization of the domain function of finite
-maps. We provide such an axiomatization, instead of implementing the domain
-function in a generic way, to allow more efficient implementations. *)
-From iris.prelude Require Export collections fin_maps.
-Set Default Proof Using "Type*".
-
-Class FinMapDom K M D `{FMap M,
-    ∀ A, Lookup K A (M A), ∀ A, Empty (M A), ∀ A, PartialAlter K A (M A),
-    OMap M, Merge M, ∀ A, FinMapToList K A (M A), EqDecision K,
-    ∀ A, Dom (M A) D, ElemOf K D, Empty D, Singleton K D,
-    Union D, Intersection D, Difference D} := {
-  finmap_dom_map :>> FinMap K M;
-  finmap_dom_collection :>> Collection K D;
-  elem_of_dom {A} (m : M A) i : i ∈ dom D m ↔ is_Some (m !! i)
-}.
-
-Section fin_map_dom.
-Context `{FinMapDom K M D}.
-
-Lemma elem_of_dom_2 {A} (m : M A) i x : m !! i = Some x → i ∈ dom D m.
-Proof. rewrite elem_of_dom; eauto. Qed.
-Lemma not_elem_of_dom {A} (m : M A) i : i ∉ dom D m ↔ m !! i = None.
-Proof. by rewrite elem_of_dom, eq_None_not_Some. Qed.
-Lemma subseteq_dom {A} (m1 m2 : M A) : m1 ⊆ m2 → dom D m1 ⊆ dom D m2.
-Proof.
-  rewrite map_subseteq_spec.
-  intros ??. rewrite !elem_of_dom. inversion 1; eauto.
-Qed.
-Lemma subset_dom {A} (m1 m2 : M A) : m1 ⊂ m2 → dom D m1 ⊂ dom D m2.
-Proof.
-  intros [Hss1 Hss2]; split; [by apply subseteq_dom |].
-  contradict Hss2. rewrite map_subseteq_spec. intros i x Hi.
-  specialize (Hss2 i). rewrite !elem_of_dom in Hss2.
-  destruct Hss2; eauto. by simplify_map_eq.
-Qed.
-Lemma dom_empty {A} : dom D (@empty (M A) _) ≡ ∅.
-Proof.
-  intros x. rewrite elem_of_dom, lookup_empty, <-not_eq_None_Some. set_solver.
-Qed.
-Lemma dom_empty_inv {A} (m : M A) : dom D m ≡ ∅ → m = ∅.
-Proof.
-  intros E. apply map_empty. intros. apply not_elem_of_dom.
-  rewrite E. set_solver.
-Qed.
-Lemma dom_alter {A} f (m : M A) i : dom D (alter f i m) ≡ dom D m.
-Proof.
-  apply elem_of_equiv; intros j; rewrite !elem_of_dom; unfold is_Some.
-  destruct (decide (i = j)); simplify_map_eq/=; eauto.
-  destruct (m !! j); naive_solver.
-Qed.
-Lemma dom_insert {A} (m : M A) i x : dom D (<[i:=x]>m) ≡ {[ i ]} ∪ dom D m.
-Proof.
-  apply elem_of_equiv. intros j. rewrite elem_of_union, !elem_of_dom.
-  unfold is_Some. setoid_rewrite lookup_insert_Some.
-  destruct (decide (i = j)); set_solver.
-Qed.
-Lemma dom_insert_subseteq {A} (m : M A) i x : dom D m ⊆ dom D (<[i:=x]>m).
-Proof. rewrite (dom_insert _). set_solver. Qed.
-Lemma dom_insert_subseteq_compat_l {A} (m : M A) i x X :
-  X ⊆ dom D m → X ⊆ dom D (<[i:=x]>m).
-Proof. intros. trans (dom D m); eauto using dom_insert_subseteq. Qed.
-Lemma dom_singleton {A} (i : K) (x : A) : dom D {[i := x]} ≡ {[ i ]}.
-Proof. rewrite <-insert_empty, dom_insert, dom_empty; set_solver. Qed.
-Lemma dom_delete {A} (m : M A) i : dom D (delete i m) ≡ dom D m ∖ {[ i ]}.
-Proof.
-  apply elem_of_equiv. intros j. rewrite elem_of_difference, !elem_of_dom.
-  unfold is_Some. setoid_rewrite lookup_delete_Some. set_solver.
-Qed.
-Lemma delete_partial_alter_dom {A} (m : M A) i f :
-  i ∉ dom D m → delete i (partial_alter f i m) = m.
-Proof. rewrite not_elem_of_dom. apply delete_partial_alter. Qed.
-Lemma delete_insert_dom {A} (m : M A) i x :
-  i ∉ dom D m → delete i (<[i:=x]>m) = m.
-Proof. rewrite not_elem_of_dom. apply delete_insert. Qed.
-Lemma map_disjoint_dom {A} (m1 m2 : M A) : m1 ⊥ₘ m2 ↔ dom D m1 ⊥ dom D m2.
-Proof.
-  rewrite map_disjoint_spec, elem_of_disjoint.
-  setoid_rewrite elem_of_dom. unfold is_Some. naive_solver.