algebra/cofe.v

-From algebra Require Export base.
-
-(** This files defines (a shallow embedding of) the category of COFEs:
-    Complete ordered families of equivalences. This is a cartesian closed
-    category, and mathematically speaking, the entire development lives
-    in this category. However, we will generally prefer to work with raw
-    Coq functions plus some registered Proper instances for non-expansiveness.
-    This makes writing such functions much easier. It turns out that it many 
-    cases, we do not even need non-expansiveness.
-
-    In principle, it would be possible to perform a large part of the
-    development on OFEs, i.e., on bisected metric spaces that are not
-    necessary complete. This is because the function space A → B has a
-    completion if B has one - for A, the metric itself suffices.
-    That would result in a simplification of some constructions, becuase
-    no completion would have to be provided. However, on the other hand,
-    we would have to introduce the notion of OFEs into our alebraic
-    hierarchy, which we'd rather avoid. Furthermore, on paper, justifying
-    this mix of OFEs and COFEs is a little fuzzy.
-*)
-
-(** Unbundeled version *)
-Class Dist A := dist : nat → relation A.
-Instance: Params (@dist) 3.
-Notation "x ≡{ n }≡ y" := (dist n x y)
-  (at level 70, n at next level, format "x  ≡{ n }≡  y").
-Hint Extern 0 (_ ≡{_}≡ _) => reflexivity.
-Hint Extern 0 (_ ≡{_}≡ _) => symmetry; assumption.
-
-Tactic Notation "cofe_subst" ident(x) :=
-  repeat match goal with
-  | _ => progress simplify_eq/=
-  | H:@dist ?A ?d ?n x _ |- _ => setoid_subst_aux (@dist A d n) x
-  | H:@dist ?A ?d ?n _ x |- _ => symmetry in H;setoid_subst_aux (@dist A d n) x
-  end.
-Tactic Notation "cofe_subst" :=
-  repeat match goal with
-  | _ => progress simplify_eq/=
-  | H:@dist ?A ?d ?n ?x _ |- _ => setoid_subst_aux (@dist A d n) x
-  | H:@dist ?A ?d ?n _ ?x |- _ => symmetry in H;setoid_subst_aux (@dist A d n) x
-  end.
-
-Tactic Notation "solve_ne" := intros; solve_proper.
-
-Record chain (A : Type) `{Dist A} := {
-  chain_car :> nat → A;
-  chain_cauchy n i : n < i → chain_car i ≡{n}≡ chain_car (S n)
-}.
-Arguments chain_car {_ _} _ _.
-Arguments chain_cauchy {_ _} _ _ _ _.
-Class Compl A `{Dist A} := compl : chain A → A.
-
-Record CofeMixin A `{Equiv A, Compl A} := {
-  mixin_equiv_dist x y : x ≡ y ↔ ∀ n, x ≡{n}≡ y;
-  mixin_dist_equivalence n : Equivalence (dist n);
-  mixin_dist_S n x y : x ≡{S n}≡ y → x ≡{n}≡ y;
-  mixin_conv_compl n c : compl c ≡{n}≡ c (S n)
-}.
-Class Contractive `{Dist A, Dist B} (f : A -> B) :=
-  contractive n x y : (∀ i, i < n → x ≡{i}≡ y) → f x ≡{n}≡ f y.
-
-(** Bundeled version *)
-Structure cofeT := CofeT {
-  cofe_car :> Type;
-  cofe_equiv : Equiv cofe_car;
-  cofe_dist : Dist cofe_car;
-  cofe_compl : Compl cofe_car;
-  cofe_mixin : CofeMixin cofe_car
-}.
-Arguments CofeT {_ _ _ _} _.
-Add Printing Constructor cofeT.
-Existing Instances cofe_equiv cofe_dist cofe_compl.
-Arguments cofe_car : simpl never.
-Arguments cofe_equiv : simpl never.
-Arguments cofe_dist : simpl never.
-Arguments cofe_compl : simpl never.
-Arguments cofe_mixin : simpl never.
-
-(** Lifting properties from the mixin *)
-Section cofe_mixin.
-  Context {A : cofeT}.
-  Implicit Types x y : A.
-  Lemma equiv_dist x y : x ≡ y ↔ ∀ n, x ≡{n}≡ y.
-  Proof. apply (mixin_equiv_dist _ (cofe_mixin A)). Qed.
-  Global Instance dist_equivalence n : Equivalence (@dist A _ n).
-  Proof. apply (mixin_dist_equivalence _ (cofe_mixin A)). Qed.
-  Lemma dist_S n x y : x ≡{S n}≡ y → x ≡{n}≡ y.
-  Proof. apply (mixin_dist_S _ (cofe_mixin A)). Qed.
-  Lemma conv_compl n (c : chain A) : compl c ≡{n}≡ c (S n).
-  Proof. apply (mixin_conv_compl _ (cofe_mixin A)). Qed.
-End cofe_mixin.
-
-(** General properties *)
-Section cofe.
-  Context {A : cofeT}.
-  Implicit Types x y : 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 A _ n).
-  Proof.
-    intros x1 x2 ? y1 y2 ?; split; intros.
-    - by transitivity x1; [|transitivity y1].
-    - by transitivity x2; [|transitivity y2].
-  Qed.
-  Global Instance dist_proper n : Proper ((≡) ==> (≡) ==> iff) (@dist A _ n).
-  Proof.
-    by move => x1 x2 /equiv_dist Hx y1 y2 /equiv_dist 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 n n' x y : x ≡{n}≡ y → n' ≤ n → x ≡{n'}≡ y.
-  Proof. induction 2; eauto using dist_S. Qed.
-  Instance ne_proper {B : cofeT} (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.
-  Instance ne_proper_2 {B C : cofeT} (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 n) (Hy n).
-  Qed.
-  Lemma contractive_S {B : cofeT} (f : A → B) `{!Contractive f} n x y :
-    x ≡{n}≡ y → f x ≡{S n}≡ f y.
-  Proof. eauto using contractive, dist_le with omega. Qed.
-  Lemma contractive_0 {B : cofeT} (f : A → B) `{!Contractive f} x y :
-    f x ≡{0}≡ f y.
-  Proof. eauto using contractive with omega. Qed.
-  Global Instance contractive_ne {B : cofeT} (f : A → B) `{!Contractive f} n :
-    Proper (dist n ==> dist n) f | 100.
-  Proof. by intros x y ?; apply dist_S, contractive_S. Qed.
-  Global Instance contractive_proper {B : cofeT} (f : A → B) `{!Contractive f} :
-    Proper ((≡) ==> (≡)) f | 100 := _.
-End cofe.
-
-(** Mapping a chain *)
-Program Definition chain_map `{Dist A, Dist B} (f : A → B)
-    `{!∀ n, Proper (dist n ==> dist n) f} (c : chain A) : chain B :=
-  {| chain_car n := f (c n) |}.
-Next Obligation. by intros ? A ? B f Hf c n i ?; apply Hf, chain_cauchy. Qed.
-
-(** Timeless elements *)
-Class Timeless {A : cofeT} (x : A) := timeless y : x ≡{0}≡ y → x ≡ y.
-Arguments timeless {_} _ {_} _ _.
-Lemma timeless_iff {A : cofeT} n (x : A) `{!Timeless x} y : x ≡ y ↔ x ≡{n}≡ y.
-Proof.
-  split; intros; [by apply equiv_dist|].
-  apply (timeless _), dist_le with n; auto with lia.
-Qed.
-
-(** Fixpoint *)
-Program Definition fixpoint_chain {A : cofeT} `{Inhabited A} (f : A → A)
-  `{!Contractive f} : chain A := {| chain_car i := Nat.iter (S i) f inhabitant |}.
-Next Obligation.
-  intros A ? f ? n. induction n as [|n IH]; intros [|i] ?; simpl; try omega.
-  - apply (contractive_0 f).
-  - apply (contractive_S f), IH; auto with omega.
-Qed.
-Program Definition fixpoint {A : cofeT} `{Inhabited A} (f : A → A)
-  `{!Contractive f} : A := compl (fixpoint_chain f).
-
-Section fixpoint.
-  Context {A : cofeT} `{Inhabited A} (f : A → A) `{!Contractive f}.
-  Lemma fixpoint_unfold : fixpoint f ≡ f (fixpoint f).
-  Proof.
-    apply equiv_dist=>n; rewrite /fixpoint (conv_compl n (fixpoint_chain f)) //.
-    induction n as [|n IH]; simpl; eauto using contractive_0, contractive_S.
-  Qed.
-  Lemma fixpoint_ne (g : A → A) `{!Contractive g} n :
-    (∀ z, f z ≡{n}≡ g z) → fixpoint f ≡{n}≡ fixpoint g.
-  Proof.
-    intros Hfg. rewrite /fixpoint
-      (conv_compl n (fixpoint_chain f)) (conv_compl n (fixpoint_chain g)) /=.
-    induction n as [|n IH]; simpl in *; [by rewrite !Hfg|].
-    rewrite Hfg; apply contractive_S, IH; auto using dist_S.
-  Qed.
-  Lemma fixpoint_proper (g : A → A) `{!Contractive g} :
-    (∀ x, f x ≡ g x) → fixpoint f ≡ fixpoint g.
-  Proof. setoid_rewrite equiv_dist; naive_solver eauto using fixpoint_ne. Qed.
-End fixpoint.
-Global Opaque fixpoint.
-
-(** Function space *)
-Record 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.
-
-Section cofe_mor.
-  Context {A B : cofeT}.
-  Global Instance cofe_mor_proper (f : cofeMor A B) : Proper ((≡) ==> (≡)) f.
-  Proof. apply ne_proper, cofe_mor_ne. Qed.
-  Instance cofe_mor_equiv : Equiv (cofeMor A B) := λ f g, ∀ x, f x ≡ g x.
-  Instance cofe_mor_dist : 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 c x n i ?. by apply (chain_cauchy c). Qed.
-  Program Instance cofe_mor_compl : Compl (cofeMor A B) := λ c,
-    {| cofe_mor_car x := compl (fun_chain c x) |}.
-  Next Obligation.
-    intros c n x y Hx. by rewrite (conv_compl n (fun_chain c x))
-      (conv_compl n (fun_chain c y)) /= Hx.
-  Qed.
-  Definition cofe_mor_cofe_mixin : CofeMixin (cofeMor A B).
-  Proof.
-    split.
-    - intros f g; split; [intros Hfg n k; apply equiv_dist, Hfg|].
-      intros Hfg k; apply equiv_dist=> n; apply Hfg.
-    - 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.
-    - intros n c x; simpl.
-      by rewrite (conv_compl n (fun_chain c x)) /=.
-  Qed.
-  Canonical Structure cofe_mor : cofeT := CofeT cofe_mor_cofe_mixin.
-
-  Global Instance cofe_mor_car_ne n :
-    Proper (dist n ==> dist n ==> dist n) (@cofe_mor_car A B).
-  Proof. intros f g Hfg x y Hx; rewrite Hx; apply Hfg. Qed.
-  Global Instance cofe_mor_car_proper :
-    Proper ((≡) ==> (≡) ==> (≡)) (@cofe_mor_car A B) := ne_proper_2 _.
-  Lemma cofe_mor_ext (f g : cofeMor A B) : f ≡ g ↔ ∀ x, f x ≡ g x.
-  Proof. done. Qed.
-End cofe_mor.
-
-Arguments cofe_mor : clear implicits.
-Infix "-n>" := cofe_mor (at level 45, right associativity).
-Instance cofe_more_inhabited {A B : cofeT} `{Inhabited B} :
-  Inhabited (A -n> B) := populate (CofeMor (λ _, inhabitant)).
-
-(** 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; rewrite /= (Hg x) (Hf (g2 x)). Qed.
-
-(** unit *)
-Section unit.
-  Instance unit_dist : Dist unit := λ _ _ _, True.
-  Instance unit_compl : Compl unit := λ _, ().
-  Definition unit_cofe_mixin : CofeMixin unit.
-  Proof. by repeat split; try exists 0. Qed.
-  Canonical Structure unitC : cofeT := CofeT unit_cofe_mixin.
-  Global Instance unit_timeless (x : ()) : Timeless x.
-  Proof. done. Qed.
-End unit.
-
-(** Product *)
-Section product.
-  Context {A B : cofeT}.
-
-  Instance prod_dist : Dist (A * B) := λ n, prod_relation (dist n) (dist n).
-  Global Instance pair_ne :
-    Proper (dist n ==> dist n ==> dist n) (@pair A B) := _.
-  Global Instance fst_ne : Proper (dist n ==> dist n) (@fst A B) := _.
-  Global Instance snd_ne : Proper (dist n ==> dist n) (@snd A B) := _.
-  Instance prod_compl : Compl (A * B) := λ c,
-    (compl (chain_map fst c), compl (chain_map snd c)).
-  Definition prod_cofe_mixin : CofeMixin (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.
-    - intros n c; split. apply (conv_compl n (chain_map fst c)).
-      apply (conv_compl n (chain_map snd c)).
-  Qed.
-  Canonical Structure prodC : cofeT := CofeT prod_cofe_mixin.
-  Global Instance pair_timeless (x : A) (y : B) :
-    Timeless x → Timeless y → Timeless (x,y).
-  Proof. by intros ?? [x' y'] [??]; split; apply (timeless _). Qed.
-End product.
-
-Arguments prodC : clear implicits.
-Typeclasses Opaque prod_dist.
-
-Instance prod_map_ne {A A' B B' : cofeT} 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.
-
-(** Discrete cofe *)
-Section discrete_cofe.
-  Context `{Equiv A, @Equivalence A (≡)}.
-  Instance discrete_dist : Dist A := λ n x y, x ≡ y.
-  Instance discrete_compl : Compl A := λ c, c 1.
-  Definition discrete_cofe_mixin : CofeMixin A.
-  Proof.
-    split.
-    - intros x y; split; [done|intros Hn; apply (Hn 0)].
-    - done.
-    - done.
-    - intros n c. rewrite /compl /discrete_compl /=.
-      symmetry; apply (chain_cauchy c 0 (S n)); omega.
-  Qed.
-  Definition discreteC : cofeT := CofeT discrete_cofe_mixin.
-  Global Instance discrete_timeless (x : A) : Timeless (x : discreteC).
-  Proof. by intros y. Qed.
-End discrete_cofe.
-Arguments discreteC _ {_ _}.
-
-Definition leibnizC (A : Type) : cofeT := @discreteC A equivL _.
-Instance leibnizC_leibniz : LeibnizEquiv (leibnizC A).
-Proof. by intros A x y. Qed.
-
-Canonical Structure natC := leibnizC nat.
-Canonical Structure boolC := leibnizC bool.
-
-(** Later *)
-Inductive later (A : Type) : Type := Next { later_car : A }.
-Add Printing Constructor later.
-Arguments Next {_} _.
-Arguments later_car {_} _.
-Lemma later_eta {A} (x : later A) : Next (later_car x) = x.
-Proof. by destruct x. Qed.
-
-Section later.
-  Context {A : cofeT}.
-  Instance later_equiv : Equiv (later A) := λ x y, later_car x ≡ later_car y.
-  Instance later_dist : 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 (c : chain (later A)) : chain A :=
-    {| chain_car n := later_car (c (S n)) |}.
-  Next Obligation. intros c n i ?; apply (chain_cauchy c (S n)); lia. Qed.
-  Instance later_compl : Compl (later A) := λ c, Next (compl (later_chain c)).
-  Definition later_cofe_mixin : CofeMixin (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.
-    - intros [|n] c; [done|by apply (conv_compl n (later_chain c))].
-  Qed.
-  Canonical Structure laterC : cofeT := CofeT later_cofe_mixin.
-  Global Instance Next_contractive : Contractive (@Next A).
-  Proof. intros [|n] x y Hxy; [done|]; apply Hxy; lia. Qed.
-  Global Instance Later_inj n : Inj (dist n) (dist (S n)) (@Next A).
-  Proof. by intros x y. Qed.
-End later.
-
-Arguments laterC : clear implicits.
-
-Definition later_map {A B} (f : A → B) (x : later A) : later B :=
-  Next (f (later_car x)).
-Instance later_map_ne {A B : cofeT} (f : A → B) n :
-  Proper (dist (pred n) ==> dist (pred n)) f →
-  Proper (dist n ==> dist n) (later_map f) | 0.
-Proof. destruct n as [|n]; intros Hf [x] [y] ?; do 2 red; simpl; auto. Qed.
-Lemma later_map_id {A} (x : later A) : later_map id x = x.
-Proof. by destruct x. Qed.
-Lemma later_map_compose {A B C} (f : A → B) (g : B → C) (x : later A) :
-  later_map (g ∘ f) x = later_map g (later_map f x).
-Proof. by destruct x. Qed.
-Definition laterC_map {A B} (f : A -n> B) : laterC A -n> laterC B :=
-  CofeMor (later_map f).
-Instance laterC_map_contractive (A B : cofeT) : Contractive (@laterC_map A B).
-Proof. intros [|n] f g Hf n'; [done|]; apply Hf; lia. Qed.

algebra/dra.v

-From algebra Require Export cmra.
-
-(** 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.
-
-Definition dra_included `{Equiv A, Valid A, Disjoint A, Op A} := λ x y,
-  ∃ z, y ≡ x ⋅ z ∧ ✓ z ∧ x ⊥ z.
-Instance: Params (@dra_included) 4.
-Local Infix "≼" := dra_included.
-
-Class DRA A `{Equiv A, Valid A, Unit A, Disjoint A, Op A, Minus A} := {
-  (* setoids *)
-  dra_equivalence :> Equivalence ((≡) : relation A);
-  dra_op_proper :> Proper ((≡) ==> (≡) ==> (≡)) (⋅);
-  dra_unit_proper :> Proper ((≡) ==> (≡)) unit;
-  dra_valid_proper :> Proper ((≡) ==> impl) valid;
-  dra_disjoint_proper :> ∀ x, Proper ((≡) ==> impl) (disjoint x);
-  dra_minus_proper :> Proper ((≡) ==> (≡) ==> (≡)) minus;
-  (* validity *)
-  dra_op_valid x y : ✓ x → ✓ y → x ⊥ y → ✓ (x ⋅ y);
-  dra_unit_valid x : ✓ x → ✓ unit x;
-  dra_minus_valid x y : ✓ x → ✓ y → x ≼ y → ✓ (y ⩪ x);
-  (* monoid *)
-  dra_assoc :> Assoc (≡) (⋅);
-  dra_disjoint_ll x y z : ✓ x → ✓ y → ✓ z → x ⊥ y → x ⋅ y ⊥ z → x ⊥ z;
-  dra_disjoint_move_l x y z : ✓ x → ✓ y → ✓ z → x ⊥ y → x ⋅ y ⊥ z → x ⊥ y ⋅ z;
-  dra_symmetric :> Symmetric (@disjoint A _);
-  dra_comm x y : ✓ x → ✓ y → x ⊥ y → x ⋅ y ≡ y ⋅ x;
-  dra_unit_disjoint_l x : ✓ x → unit x ⊥ x;
-  dra_unit_l x : ✓ x → unit x ⋅ x ≡ x;
-  dra_unit_idemp x : ✓ x → unit (unit x) ≡ unit x;
-  dra_unit_preserving x y : ✓ x → ✓ y → x ≼ y → unit x ≼ unit y;
-  dra_disjoint_minus x y : ✓ x → ✓ y → x ≼ y → x ⊥ y ⩪ x;
-  dra_op_minus x y : ✓ x → ✓ y → x ≼ y → x ⋅ y ⩪ x ≡ y
-}.
-
-Section dra.
-Context A `{DRA A}.
-Arguments valid _ _ !_ /.
-Hint Immediate dra_op_proper : typeclass_instances.
-
-Notation T := (validity (valid : A → Prop)).
-
-Instance validity_valid : Valid T := validity_is_valid.
-Instance validity_equiv : Equiv T := λ x y,
-  (valid x ↔ valid y) ∧ (valid x → validity_car x ≡ validity_car y).
-Instance validity_equivalence : Equivalence ((≡) : relation T).
-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 dra_valid_proper' : Proper ((≡) ==> iff) (valid : A → Prop).
-Proof. by split; apply dra_valid_proper. Qed.
-Instance to_validity_proper : Proper ((≡) ==> (≡)) to_validity.
-Proof. by intros x1 x2 Hx; split; rewrite /= Hx. Qed.
-Instance: Proper ((≡) ==> (≡) ==> iff) (⊥).
-Proof.
-  intros x1 x2 Hx y1 y2 Hy; split.
-  - by rewrite Hy (symmetry_iff (⊥) x1) (symmetry_iff (⊥) x2) Hx.
-  - by rewrite -Hy (symmetry_iff (⊥) x2) (symmetry_iff (⊥) x1) -Hx.
-Qed.
-Lemma dra_disjoint_rl x y z : ✓ x → ✓ y → ✓ 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 : ✓ x → ✓ y → ✓ z → x ⊥ y → x ⋅ y ⊥ z → y ⊥ z.
-Proof. intros ????. rewrite dra_comm //. by apply dra_disjoint_ll. Qed.
-Lemma dra_disjoint_move_r x y z :
-  ✓ x → ✓ y → ✓ z → y ⊥ z → x ⊥ y ⋅ z → x ⋅ y ⊥ z.
-Proof.
-  intros; symmetry; rewrite dra_comm; eauto using dra_disjoint_rl.
-  apply dra_disjoint_move_l; auto; by rewrite dra_comm.
-Qed.
-Hint Immediate dra_disjoint_move_l dra_disjoint_move_r.
-Hint Unfold dra_included.
-
-Lemma validity_valid_car_valid (z : T) : ✓ z → ✓ validity_car z.
-Proof. apply validity_prf. Qed.
-Hint Resolve validity_valid_car_valid.
-Program Instance validity_unit : Unit T := λ x,
-  Validity (unit (validity_car x)) (✓ x) _.
-Solve Obligations with naive_solver auto using dra_unit_valid.
-Program Instance validity_op : Op T := λ x y,
-  Validity (validity_car x ⋅ validity_car y)
-           (✓ x ∧ ✓ y ∧ validity_car x ⊥ validity_car y) _.
-Solve Obligations with naive_solver auto using dra_op_valid.
-Program Instance validity_minus : Minus T := λ x y,
-  Validity (validity_car x ⩪ validity_car y)
-           (✓ x ∧ ✓ y ∧ validity_car y ≼ validity_car x) _.
-Solve Obligations with naive_solver auto using dra_minus_valid.
-
-Definition validity_ra : RA (discreteC T).
-Proof.
-  split.
-  - intros ??? [? Heq]; split; simpl; [|by intros (?&?&?); rewrite Heq].
-    split; intros (?&?&?); split_and!;
-      first [rewrite ?Heq; tauto|rewrite -?Heq; tauto|tauto].
-  - by intros ?? [? Heq]; split; [done|]; simpl; intros ?; rewrite Heq.
-  - intros ?? [??]; naive_solver.
-  - intros x1 x2 [? Hx] y1 y2 [? Hy];
-      split; simpl; [|by intros (?&?&?); rewrite Hx // Hy].
-    split; intros (?&?&z&?&?); split_and!; try tauto.
-    + exists z. by rewrite -Hy // -Hx.
-    + exists z. by rewrite Hx ?Hy; tauto.
-  - intros [x px ?] [y py ?] [z pz ?]; split; simpl;
-      [intuition eauto 2 using dra_disjoint_lr, dra_disjoint_rl
-      |by intros; rewrite assoc].
-  - intros [x px ?] [y py ?]; split; naive_solver eauto using dra_comm.
-  - intros [x px ?]; split;
-      naive_solver eauto using dra_unit_l, dra_unit_disjoint_l.
-  - intros [x px ?]; split; naive_solver eauto using dra_unit_idemp.
-  - intros x y Hxy; exists (unit y ⩪ unit x).
-    destruct x as [x px ?], y as [y py ?], Hxy as [[z pz ?] [??]]; simpl in *.
-    assert (py → unit x ≼ unit y)
-      by intuition eauto 10 using dra_unit_preserving.
-    constructor; [|symmetry]; simpl in *;
-      intuition eauto using dra_op_minus, dra_disjoint_minus, dra_unit_valid.
-  - by intros [x px ?] [y py ?] (?&?&?).
-  - intros [x px ?] [y py ?] [[z pz ?] [??]]; split; simpl in *;
-      intuition eauto 10 using dra_disjoint_minus, dra_op_minus.
-Qed.
-Definition validityRA : cmraT := discreteRA validity_ra.
-Lemma validity_update (x y : validityRA) :
-  (∀ z, ✓ x → ✓ z → validity_car x ⊥ z → ✓ y ∧ validity_car y ⊥ z) → x ~~> y.
-Proof.
-  intros Hxy. apply discrete_update.
-  intros z (?&?&?); split_and!; try eapply Hxy; eauto.
-Qed.
-
-Lemma to_validity_valid (x : A) :
-  ✓ to_validity x → ✓ x.
-Proof. intros. done. Qed.
-Lemma to_validity_op (x y : A) :
-  ✓ x → ✓ y → (✓ (x ⋅ y) → x ⊥ y) →
-  to_validity (x ⋅ y) ≡ to_validity x ⋅ to_validity y.
-Proof.
-  intros Hvalx Hvaly Hdisj. split; [split | done].
-  - simpl. auto.
-  - simpl. intros (_ & _ & ?).
-    auto using dra_op_valid, to_validity_valid.
-Qed.
-
-End dra.

algebra/excl.v

-From algebra Require Export cmra.
-From algebra Require Import functor upred.
-Local Arguments validN _ _ _ !_ /.
-Local Arguments valid _ _  !_ /.
-
-Inductive excl (A : Type) :=
-  | Excl : A → excl A
-  | ExclUnit : excl A
-  | ExclBot : excl A.
-Arguments Excl {_} _.
-Arguments ExclUnit {_}.
-Arguments ExclBot {_}.
-Instance maybe_Excl {A} : Maybe (@Excl A) := λ x,
-  match x with Excl a => Some a | _ => None end.
-
-Section excl.
-Context {A : cofeT}.
-
-(* Cofe *)
-Inductive excl_equiv : 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.
-Inductive excl_dist `{Dist A} : Dist (excl A) :=
-  | Excl_dist (x y : A) n : x ≡{n}≡ y → Excl x ≡{n}≡ Excl y
-  | ExclUnit_dist n : ExclUnit ≡{n}≡ ExclUnit
-  | ExclBot_dist n : ExclBot ≡{n}≡ ExclBot.
-Existing Instance excl_dist.
-Global Instance Excl_ne n : Proper (dist n ==> dist n) (@Excl A).
-Proof. by constructor. Qed.
-Global Instance Excl_proper : Proper ((≡) ==> (≡)) (@Excl A).
-Proof. by constructor. Qed.
-Global Instance Excl_inj : Inj (≡) (≡) (@Excl A).
-Proof. by inversion_clear 1. Qed.
-Global Instance Excl_dist_inj n : Inj (dist n) (dist n) (@Excl A).
-Proof. by inversion_clear 1. Qed.
-Program Definition excl_chain
-    (c : chain (excl A)) (x : A) (H : maybe Excl (c 1) = Some x) : chain A :=
-  {| chain_car n := match c n return _ with Excl y => y | _ => x end |}.
-Next Obligation.
-  intros c x ? n [|i] ?; [omega|]; simpl.
-  destruct (c 1) eqn:?; simplify_eq/=.
-  by feed inversion (chain_cauchy c n (S i)).
-Qed.
-Instance excl_compl : Compl (excl A) := λ c,
-  match Some_dec (maybe Excl (c 1)) with
-  | inleft (exist x H) => Excl (compl (excl_chain c x H)) | inright _ => c 1
-  end.
-Definition excl_cofe_mixin : CofeMixin (excl A).
-Proof.
-  split.
-  - intros mx my; split; [by destruct 1; constructor; apply equiv_dist|].
-    intros Hxy; feed inversion (Hxy 1); subst; constructor; apply equiv_dist.
-    by intros n; feed inversion (Hxy n).
-  - intros n; split.
-    + by intros [x| |]; constructor.
-    + by destruct 1; constructor.
-    + destruct 1; inversion_clear 1; constructor; etransitivity; eauto.
-  - by inversion_clear 1; constructor; apply dist_S.
-  - intros n c; unfold compl, excl_compl.
-    destruct (Some_dec (maybe Excl (c 1))) as [[x Hx]|].
-    { assert (c 1 = Excl x) by (by destruct (c 1); simplify_eq/=).
-      assert (∃ y, c (S n) = Excl y) as [y Hy].
-      { feed inversion (chain_cauchy c 0 (S n)); eauto with lia congruence. }
-      rewrite Hy; constructor.
-      by rewrite (conv_compl n (excl_chain c x Hx)) /= Hy. }
-    feed inversion (chain_cauchy c 0 (S n)); first lia;
-       constructor; destruct (c 1); simplify_eq/=.
-Qed.
-Canonical Structure exclC : cofeT := CofeT excl_cofe_mixin.
-
-Global Instance Excl_timeless (x : A) : Timeless x → Timeless (Excl x).
-Proof. by inversion_clear 2; constructor; apply (timeless _). Qed.
-Global Instance ExclUnit_timeless : Timeless (@ExclUnit A).
-Proof. by inversion_clear 1; constructor. Qed.
-Global Instance ExclBot_timeless : Timeless (@ExclBot A).
-Proof. by inversion_clear 1; constructor. Qed.
-Global Instance excl_timeless :
-  (∀ x : A, Timeless x) → ∀ x : excl A, Timeless x.
-Proof. intros ? []; apply _. Qed.
-Global Instance excl_leibniz : LeibnizEquiv A → LeibnizEquiv (excl A).
-Proof. by destruct 2; f_equal; apply leibniz_equiv. Qed.
-
-(* CMRA *)
-Instance excl_validN : ValidN (excl A) := λ n x,
-  match x with Excl _ | ExclUnit => True | ExclBot => False end.
-Global Instance excl_empty : Empty (excl A) := ExclUnit.
-Instance excl_unit : Unit (excl A) := λ _, ∅.
-Instance excl_op : 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 : Minus (excl A) := λ x y,
-  match x, y with
-  | _, ExclUnit => x
-  | Excl _, Excl _ => ExclUnit
-  | _, _ => ExclBot
-  end.
-Definition excl_cmra_mixin : CMRAMixin (excl A).
-Proof.
-  split.
-  - by intros n []; destruct 1; constructor.
-  - constructor.
-  - by destruct 1; intros ?.
-  - by destruct 1; inversion_clear 1; constructor.
-  - intros n [?| |]; simpl; auto with lia.
-  - by intros [?| |] [?| |] [?| |]; constructor.
-  - by intros [?| |] [?| |]; constructor.
-  - by intros [?| |]; constructor.
-  - constructor.
-  - by intros n [?| |] [?| |]; exists ∅.
-  - by intros n [?| |] [?| |].
-  - by intros n [?| |] [?| |] [[?| |] Hz]; inversion_clear Hz; constructor.
-Qed.
-Definition excl_cmra_extend_mixin : CMRAExtendMixin (excl A).
-Proof.
-  intros n x y1 y2 ? Hx.
-  by exists match y1, y2 with
-    | Excl a1, Excl a2 => (Excl a1, Excl a2)
-    | ExclBot, _ => (ExclBot, y2) | _, ExclBot => (y1, ExclBot)
-    | ExclUnit, _ => (ExclUnit, x) | _, ExclUnit => (x, ExclUnit)
-    end; destruct y1, y2; inversion_clear Hx; repeat constructor.
-Qed.
-Canonical Structure exclRA : cmraT :=
-  CMRAT excl_cofe_mixin excl_cmra_mixin excl_cmra_extend_mixin.
-Global Instance excl_cmra_identity : CMRAIdentity exclRA.
-Proof. split. done. by intros []. apply _. Qed.
-Lemma excl_validN_inv_l n x y : ✓{n} (Excl x ⋅ y) → y = ∅.
-Proof. by destruct y. Qed.
-Lemma excl_validN_inv_r n x y : ✓{n} (x ⋅ Excl y) → x = ∅.
-Proof. by destruct x. Qed.
-Lemma Excl_includedN n x y : ✓{n} y → Excl x ≼{n} y ↔ y ≡{n}≡ Excl x.
-Proof.
-  intros Hvalid; split; [|by intros ->].
-  by intros [z ?]; cofe_subst; rewrite (excl_validN_inv_l n x z).
-Qed.
-
-(** Internalized properties *)
-Lemma excl_equivI {M} (x y : excl A) :
-  (x ≡ y)%I ≡ (match x, y with
-               | Excl a, Excl b => a ≡ b
-               | ExclUnit, ExclUnit | ExclBot, ExclBot => True
-               | _, _ => False
-               end : uPred M)%I.
-Proof. split. by destruct 1. by destruct x, y; try constructor. Qed.
-Lemma excl_validI {M} (x : excl A) :
-  (✓ x)%I ≡ (if x is ExclBot then False else True : uPred M)%I.
-Proof. by destruct x. Qed.
-
-(** ** Local updates *)
-Global Instance excl_local_update b :
-  LocalUpdate (λ a, if a is Excl _ then True else False) (λ _, Excl b).
-Proof. split. by intros n y1 y2 Hy. by intros n [a| |] [b'| |]. Qed.
-
-Global Instance excl_local_update_del :
-LocalUpdate (λ a, if a is Excl _ then True else False) (λ _, ExclUnit).
-Proof. split. by intros n y1 y2 Hy. by intros n [a| |] [b'| |]. Qed.
-
-(** Updates *)
-Lemma excl_update (x : A) y : ✓ y → Excl x ~~> y.
-Proof. destruct y; by intros ?? [?| |]. Qed.
-Lemma excl_updateP (P : excl A → Prop) x y : ✓ y → P y → Excl x ~~>: P.
-Proof. intros ?? n z ?; exists y. by destruct y, z as [?| |]. Qed.
-End excl.
-
-Arguments exclC : clear implicits.
-Arguments exclRA : clear implicits.
-
-(* Functor *)
-Definition excl_map {A B} (f : A → B) (x : excl A) : excl B :=
-  match x with
-  | Excl a => Excl (f a) | ExclUnit => ExclUnit | ExclBot => ExclBot
-  end.
-Lemma excl_map_id {A} (x : excl A) : excl_map id x = x.
-Proof. by destruct x. Qed.
-Lemma excl_map_compose {A B C} (f : A → B) (g : B → C) (x : excl A) :
-  excl_map (g ∘ f) x = excl_map g (excl_map f x).
-Proof. by destruct x. Qed.
-Lemma excl_map_ext {A B : cofeT} (f g : A → B) x :
-  (∀ x, f x ≡ g x) → excl_map f x ≡ excl_map g x.
-Proof. by destruct x; constructor. Qed.
-Instance excl_map_cmra_ne {A B : cofeT} n :
-  Proper ((dist n ==> dist n) ==> dist n ==> dist n) (@excl_map A B).
-Proof. by intros f f' Hf; destruct 1; constructor; apply Hf. Qed.
-Instance excl_map_cmra_monotone {A B : cofeT} (f : A → B) :
-  (∀ n, Proper (dist n ==> dist n) f) → CMRAMonotone (excl_map f).
-Proof.
-  split.
-  - intros n x y [z Hy]; exists (excl_map f z); rewrite Hy.
-    by destruct x, z; constructor.
-  - by intros n [a| |].
-Qed.
-Definition exclC_map {A B} (f : A -n> B) : exclC A -n> exclC B :=
-  CofeMor (excl_map f).
-Instance exclC_map_ne A B n : Proper (dist n ==> dist n) (@exclC_map A B).
-Proof. by intros f f' Hf []; constructor; apply Hf. Qed.
-
-Program Definition exclF : iFunctor :=
-  {| ifunctor_car := exclRA; ifunctor_map := @exclC_map |}.
-Next Obligation. by intros A x; rewrite /= excl_map_id. Qed.
-Next Obligation. by intros A B C f g x; rewrite /= excl_map_compose. Qed.

algebra/fin_maps.v

-From algebra Require Export cmra option.
-From prelude Require Export gmap.
-From algebra Require Import functor upred.
-
-Section cofe.
-Context `{Countable K} {A : cofeT}.
-Implicit Types m : gmap K A.
-
-Instance map_dist : Dist (gmap K A) := λ n m1 m2,
-  ∀ i, m1 !! i ≡{n}≡ m2 !! i.
-Program Definition map_chain (c : chain (gmap K A))
-  (k : K) : chain (option A) := {| chain_car n := c n !! k |}.
-Next Obligation. by intros c k n i ?; apply (chain_cauchy c). Qed.
-Instance map_compl : Compl (gmap K A) := λ c,
-  map_imap (λ i _, compl (map_chain c i)) (c 1).
-Definition map_cofe_mixin : CofeMixin (gmap K 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.
-  - intros n c k; rewrite /compl /map_compl lookup_imap.
-    feed inversion (λ H, chain_cauchy c 0 (S n) H k); simpl; auto with lia.
-    by rewrite conv_compl /=; apply reflexive_eq.
-Qed.
-Canonical Structure mapC : cofeT := CofeT map_cofe_mixin.
-
-(* why doesn't this go automatic? *)
-Global Instance mapC_leibniz: LeibnizEquiv A → LeibnizEquiv mapC.
-Proof. intros; change (LeibnizEquiv (gmap K A)); apply _. Qed.
-
-Global Instance lookup_ne n k :
-  Proper (dist n ==> dist n) (lookup k : gmap K A → option A).
-Proof. by intros m1 m2. Qed.
-Global Instance lookup_proper k :
-  Proper ((≡) ==> (≡)) (lookup k : gmap K A → option A) := _.
-Global Instance alter_ne f k n :
-  Proper (dist n ==> dist n) f → Proper (dist n ==> dist n) (alter f k).
-Proof.
-  intros ? m m' Hm k'.
-  by destruct (decide (k = k')); simplify_map_eq; rewrite (Hm k').
-Qed.
-Global Instance insert_ne i n :
-  Proper (dist n ==> dist n ==> dist n) (insert (M:=gmap K A) i).
-Proof.
-  intros x y ? m m' ? j; destruct (decide (i = j)); simplify_map_eq;
-    [by constructor|by apply lookup_ne].
-Qed.
-Global Instance singleton_ne i n :
-  Proper (dist n ==> dist n) (singletonM i : A → gmap K A).
-Proof. by intros ???; apply insert_ne. Qed.
-Global Instance delete_ne i n :
-  Proper (dist n ==> dist n) (delete (M:=gmap K A) i).
-Proof.
-  intros m m' ? j; destruct (decide (i = j)); simplify_map_eq;
-    [by constructor|by apply lookup_ne].
-Qed.
-
-Global Instance map_timeless `{∀ a : A, Timeless a} m : Timeless m.
-Proof. by intros m' ? i; apply: timeless. Qed.
-
-Instance map_empty_timeless : Timeless (∅ : gmap K A).
-Proof.
-  intros m Hm i; specialize (Hm i); rewrite lookup_empty in Hm |- *.
-  inversion_clear Hm; constructor.
-Qed.
-Global Instance map_lookup_timeless m i : Timeless m → Timeless (m !! i).
-Proof.
-  intros ? [x|] Hx; [|by symmetry; apply: timeless].
-  assert (m ≡{0}≡ <[i:=x]> m)
-    by (by symmetry in Hx; inversion Hx; cofe_subst; rewrite insert_id).
-  by rewrite (timeless m (<[i:=x]>m)) // lookup_insert.
-Qed.
-Global Instance map_insert_timeless m i x :
-  Timeless x → Timeless m → Timeless (<[i:=x]>m).
-Proof.
-  intros ?? m' Hm j; destruct (decide (i = j)); simplify_map_eq.
-  { by apply: timeless; rewrite -Hm lookup_insert. }
-  by apply: timeless; rewrite -Hm lookup_insert_ne.
-Qed.
-Global Instance map_singleton_timeless i x :
-  Timeless x → Timeless ({[ i := x ]} : gmap K A) := _.
-End cofe.
-
-Arguments mapC _ {_ _} _.
-
-(* CMRA *)
-Section cmra.
-Context `{Countable K} {A : cmraT}.
-Implicit Types m : gmap K A.
-
-Instance map_op : Op (gmap K A) := merge op.
-Instance map_unit : Unit (gmap K A) := fmap unit.
-Instance map_validN : ValidN (gmap K A) := λ n m, ∀ i, ✓{n} (m !! i).
-Instance map_minus : Minus (gmap K A) := merge minus.
-
-Lemma lookup_op m1 m2 i : (m1 ⋅ m2) !! i = m1 !! i ⋅ m2 !! i.
-Proof. by apply lookup_merge. Qed.
-Lemma lookup_minus m1 m2 i : (m1 ⩪ m2) !! i = m1 !! i ⩪ m2 !! i.
-Proof. by apply lookup_merge. Qed.
-Lemma lookup_unit m i : unit m !! i = unit (m !! i).
-Proof. by apply lookup_fmap. Qed.
-
-Lemma map_valid_spec m : ✓ m ↔ ∀ i, ✓ (m !! i).
-Proof. split; intros Hm ??; apply Hm. Qed.
-Lemma map_included_spec (m1 m2 : gmap K A) : m1 ≼ m2 ↔ ∀ i, m1 !! i ≼ m2 !! i.
-Proof.
-  split.
-  - by intros [m Hm]; intros i; exists (m !! i); rewrite -lookup_op Hm.
-  - intros Hm; exists (m2 ⩪ m1); intros i.
-    by rewrite lookup_op lookup_minus cmra_op_minus'.
-Qed.
-Lemma map_includedN_spec (m1 m2 : gmap K A) n :
-  m1 ≼{n} m2 ↔ ∀ i, m1 !! i ≼{n} m2 !! i.
-Proof.
-  split.
-  - by intros [m Hm]; intros i; exists (m !! i); rewrite -lookup_op Hm.
-  - intros Hm; exists (m2 ⩪ m1); intros i.
-    by rewrite lookup_op lookup_minus cmra_op_minus.
-Qed.
-
-Definition map_cmra_mixin : CMRAMixin (gmap K A).
-Proof.
-  split.
-  - by intros n m1 m2 m3 Hm i; rewrite !lookup_op (Hm i).
-  - by intros n m1 m2 Hm i; rewrite !lookup_unit (Hm i).
-  - by intros n m1 m2 Hm ? i; rewrite -(Hm i).
-  - by intros n m1 m1' Hm1 m2 m2' Hm2 i; rewrite !lookup_minus (Hm1 i) (Hm2 i).
-  - intros n m Hm i; apply cmra_validN_S, Hm.
-  - by intros m1 m2 m3 i; rewrite !lookup_op assoc.
-  - by intros m1 m2 i; rewrite !lookup_op comm.
-  - by intros m i; rewrite lookup_op !lookup_unit cmra_unit_l.
-  - by intros m i; rewrite !lookup_unit cmra_unit_idemp.
-  - intros n x y; rewrite !map_includedN_spec; intros Hm i.
-    by rewrite !lookup_unit; apply cmra_unit_preservingN.
-  - intros n m1 m2 Hm i; apply cmra_validN_op_l with (m2 !! i).
-    by rewrite -lookup_op.
-  - intros n x y; rewrite map_includedN_spec=> ? i.
-    by rewrite lookup_op lookup_minus cmra_op_minus.
-Qed.
-Definition map_cmra_extend_mixin : CMRAExtendMixin (gmap K A).
-Proof.
-  intros n m m1 m2 Hm Hm12.
-  assert (∀ i, m !! i ≡{n}≡ m1 !! i ⋅ m2 !! i) as Hm12'
-    by (by intros i; rewrite -lookup_op).
-  set (f i := cmra_extend_op n (m !! i) (m1 !! i) (m2 !! i) (Hm i) (Hm12' i)).
-  set (f_proj i := proj1_sig (f i)).
-  exists (map_imap (λ i _, (f_proj i).1) m, map_imap (λ i _, (f_proj i).2) m);
-    repeat split; intros i; rewrite /= ?lookup_op !lookup_imap.
-  - destruct (m !! i) as [x|] eqn:Hx; rewrite !Hx /=; [|constructor].
-    rewrite -Hx; apply (proj2_sig (f i)).
-  - destruct (m !! i) as [x|] eqn:Hx; rewrite /=; [apply (proj2_sig (f i))|].
-    pose proof (Hm12' i) as Hm12''; rewrite Hx in Hm12''.
-    by symmetry; apply option_op_positive_dist_l with (m2 !! i).
-  - destruct (m !! i) as [x|] eqn:Hx; simpl; [apply (proj2_sig (f i))|].
-    pose proof (Hm12' i) as Hm12''; rewrite Hx in Hm12''.
-    by symmetry; apply option_op_positive_dist_r with (m1 !! i).
-Qed.
-Canonical Structure mapRA : cmraT :=
-  CMRAT map_cofe_mixin map_cmra_mixin map_cmra_extend_mixin.
-Global Instance map_cmra_identity : CMRAIdentity mapRA.
-Proof.
-  split.
-  - by intros ? n; rewrite lookup_empty.
-  - by intros m i; rewrite /= lookup_op lookup_empty (left_id_L None _).
-  - apply map_empty_timeless.
-Qed.
-Global Instance mapRA_leibniz : LeibnizEquiv A → LeibnizEquiv mapRA.
-Proof. intros; change (LeibnizEquiv (gmap K A)); apply _. Qed.
-
-(** Internalized properties *)
-Lemma map_equivI {M} m1 m2 : (m1 ≡ m2)%I ≡ (∀ i, m1 !! i ≡ m2 !! i : uPred M)%I.
-Proof. done. Qed.
-Lemma map_validI {M} m : (✓ m)%I ≡ (∀ i, ✓ (m !! i) : uPred M)%I.
-Proof. done. Qed.
-End cmra.
-
-Arguments mapRA _ {_ _} _.
-
-Section properties.
-Context `{Countable K} {A : cmraT}.
-Implicit Types m : gmap K A.
-Implicit Types i : K.
-Implicit Types a : A.
-
-Lemma map_lookup_validN n m i x : ✓{n} m → m !! i ≡{n}≡ Some x → ✓{n} x.
-Proof. by move=> /(_ i) Hm Hi; move:Hm; rewrite Hi. Qed.
-Lemma map_lookup_valid m i x : ✓ m → m !! i ≡ Some x → ✓ x.
-Proof. move=>Hm Hi n. move:(Hm n i). by rewrite Hi. Qed.
-Lemma map_insert_validN n m i x : ✓{n} x → ✓{n} m → ✓{n} <[i:=x]>m.
-Proof. by intros ?? j; destruct (decide (i = j)); simplify_map_eq. Qed.
-Lemma map_insert_valid m i x : ✓ x → ✓ m → ✓ <[i:=x]>m.
-Proof. intros ?? n j; apply map_insert_validN; auto. Qed.
-Lemma map_singleton_validN n i x : ✓{n} ({[ i := x ]} : gmap K A) ↔ ✓{n} x.
-Proof.
-  split; [|by intros; apply map_insert_validN, cmra_empty_valid].
-  by move=>/(_ i); simplify_map_eq.
-Qed.
-Lemma map_singleton_valid i x : ✓ ({[ i := x ]} : gmap K A) ↔ ✓ x.
-Proof. split; intros ? n; eapply map_singleton_validN; eauto. Qed.
-
-Lemma map_insert_singleton_opN n m i x :
-  m !! i = None ∨ m !! i ≡{n}≡ Some (unit x) → <[i:=x]> m ≡{n}≡ {[ i := x ]} ⋅ m.
-Proof.
-  intros Hi j; destruct (decide (i = j)) as [->|];
-    [|by rewrite lookup_op lookup_insert_ne // lookup_singleton_ne // left_id].
-  rewrite lookup_op lookup_insert lookup_singleton.
-  by destruct Hi as [->| ->]; constructor; rewrite ?cmra_unit_r.
-Qed.
-Lemma map_insert_singleton_op m i x :
-  m !! i = None ∨ m !! i ≡ Some (unit x) → <[i:=x]> m ≡ {[ i := x ]} ⋅ m.
-Proof.
-  rewrite !equiv_dist; naive_solver eauto using map_insert_singleton_opN.
-Qed.
-
-Lemma map_unit_singleton (i : K) (x : A) :
-  unit ({[ i := x ]} : gmap K A) = {[ i := unit x ]}.
-Proof. apply map_fmap_singleton. Qed.
-Lemma map_op_singleton (i : K) (x y : A) :
-  {[ i := x ]} ⋅ {[ i := y ]} = ({[ i := x ⋅ y ]} : gmap K A).
-Proof. by apply (merge_singleton _ _ _ x y). Qed.
-
-Lemma singleton_includedN n m i x :
-  {[ i := x ]} ≼{n} m ↔ ∃ y, m !! i ≡{n}≡ Some y ∧ x ≼ y.
-  (* not m !! i = Some y ∧ x ≼{n} y to deal with n = 0 *)
-Proof.
-  split.
-  - move=> [m' /(_ i)]; rewrite lookup_op lookup_singleton=> Hm.
-    destruct (m' !! i) as [y|];
-      [exists (x ⋅ y)|exists x]; eauto using cmra_included_l.
-  - intros (y&Hi&?); rewrite map_includedN_spec=>j.
-    destruct (decide (i = j)); simplify_map_eq.
-    + by rewrite Hi; apply Some_Some_includedN, cmra_included_includedN.
-    + apply None_includedN.
-Qed.
-Lemma map_dom_op m1 m2 : dom (gset K) (m1 ⋅ m2) ≡ dom _ m1 ∪ dom _ m2.
-Proof.
-  apply elem_of_equiv; intros i; rewrite elem_of_union !elem_of_dom.
-  unfold is_Some; setoid_rewrite lookup_op.
-  destruct (m1 !! i), (m2 !! i); naive_solver.
-Qed.
-
-Lemma map_insert_updateP (P : A → Prop) (Q : gmap K A → Prop) m i x :
-  x ~~>: P → (∀ y, P y → Q (<[i:=y]>m)) → <[i:=x]>m ~~>: Q.
-Proof.
-  intros Hx%option_updateP' HP n mf Hm.
-  destruct (Hx n (mf !! i)) as ([y|]&?&?); try done.
-  { by generalize (Hm i); rewrite lookup_op; simplify_map_eq. }
-  exists (<[i:=y]> m); split; first by auto.
-  intros j; move: (Hm j)=>{Hm}; rewrite !lookup_op=>Hm.
-  destruct (decide (i = j)); simplify_map_eq/=; auto.
-Qed.
-Lemma map_insert_updateP' (P : A → Prop) m i x :
-  x ~~>: P → <[i:=x]>m ~~>: λ m', ∃ y, m' = <[i:=y]>m ∧ P y.
-Proof. eauto using map_insert_updateP. Qed.
-Lemma map_insert_update m i x y : x ~~> y → <[i:=x]>m ~~> <[i:=y]>m.
-Proof.
-  rewrite !cmra_update_updateP; eauto using map_insert_updateP with subst.
-Qed.
-
-Lemma map_singleton_updateP (P : A → Prop) (Q : gmap K A → Prop) i x :
-  x ~~>: P → (∀ y, P y → Q {[ i := y ]}) → {[ i := x ]} ~~>: Q.
-Proof. apply map_insert_updateP. Qed.
-Lemma map_singleton_updateP' (P : A → Prop) i x :
-  x ~~>: P → {[ i := x ]} ~~>: λ m, ∃ y, m = {[ i := y ]} ∧ P y.
-Proof. apply map_insert_updateP'. Qed.
-Lemma map_singleton_update i (x y : A) : x ~~> y → {[ i := x ]} ~~> {[ i := y ]}.
-Proof. apply map_insert_update. Qed.
-
-Lemma map_singleton_updateP_empty `{Empty A, !CMRAIdentity A}
-    (P : A → Prop) (Q : gmap K A → Prop) i :
-  ∅ ~~>: P → (∀ y, P y → Q {[ i := y ]}) → ∅ ~~>: Q.
-Proof.
-  intros Hx HQ n gf Hg.
-  destruct (Hx n (from_option ∅ (gf !! i))) as (y&?&Hy).
-  { move:(Hg i). rewrite !left_id.
-    case _: (gf !! i); simpl; auto using cmra_empty_valid. }
-  exists {[ i := y ]}; split; first by auto.
-  intros i'; destruct (decide (i' = i)) as [->|].
-  - rewrite lookup_op lookup_singleton.
-    move:Hy; case _: (gf !! i); first done.
-    by rewrite right_id.
-  - move:(Hg i'). by rewrite !lookup_op lookup_singleton_ne // !left_id.
-Qed.
-Lemma map_singleton_updateP_empty' `{Empty A, !CMRAIdentity A} (P: A → Prop) i :
-  ∅ ~~>: P → ∅ ~~>: λ m, ∃ y, m = {[ i := y ]} ∧ P y.
-Proof. eauto using map_singleton_updateP_empty. Qed.
-
-Section freshness.
-Context `{Fresh K (gset K), !FreshSpec K (gset K)}.
-Lemma map_updateP_alloc_strong (Q : gmap K A → Prop) (I : gset K) m x :
-  ✓ x → (∀ i, m !! i = None → i ∉ I → Q (<[i:=x]>m)) → m ~~>: Q.
-Proof.
-  intros ? HQ n mf Hm. set (i := fresh (I ∪ dom (gset K) (m ⋅ mf))).
-  assert (i ∉ I ∧ i ∉ dom (gset K) m ∧ i ∉ dom (gset K) mf) as [?[??]].
-  { rewrite -not_elem_of_union -map_dom_op -not_elem_of_union; apply is_fresh. }
-  exists (<[i:=x]>m); split.
-  { by apply HQ; last done; apply not_elem_of_dom. }
-  rewrite map_insert_singleton_opN; last by left; apply not_elem_of_dom.
-  rewrite -assoc -map_insert_singleton_opN;
-    last by left; apply not_elem_of_dom; rewrite map_dom_op not_elem_of_union.
-  by apply map_insert_validN; [apply cmra_valid_validN|].
-Qed.
-Lemma map_updateP_alloc (Q : gmap K A → Prop) m x :
-  ✓ x → (∀ i, m !! i = None → Q (<[i:=x]>m)) → m ~~>: Q.
-Proof. move=>??. eapply map_updateP_alloc_strong with (I:=∅); by eauto. Qed.
-Lemma map_updateP_alloc_strong' m x (I : gset K) :
-  ✓ x → m ~~>: λ m', ∃ i, i ∉ I ∧ m' = <[i:=x]>m ∧ m !! i = None.
-Proof. eauto using map_updateP_alloc_strong. Qed.
-Lemma map_updateP_alloc' m x :
-  ✓ x → m ~~>: λ m', ∃ i, m' = <[i:=x]>m ∧ m !! i = None.
-Proof. eauto using map_updateP_alloc. Qed.
-End freshness.
-
-(* Allocation is a local update: Just use composition with a singleton map. *)
-(* Deallocation is *not* a local update. The trouble is that if we
-   own {[ i ↦ x ]}, then the frame could always own "unit x", and prevent
-   deallocation. *)
-
-(* Applying a local update at a position we own is a local update. *)
-Global Instance map_alter_update `{!LocalUpdate Lv L} i :
-  LocalUpdate (λ m, ∃ x, m !! i = Some x ∧ Lv x) (alter L i).
-Proof.
-  split; first apply _.
-  intros n m1 m2 (x&Hix&?) Hm j; destruct (decide (i = j)) as [->|].
-  - rewrite lookup_alter !lookup_op lookup_alter Hix /=.
-    move: (Hm j); rewrite lookup_op Hix.
-    case: (m2 !! j)=>[y|] //=; constructor. by apply (local_updateN L).
-  - by rewrite lookup_op !lookup_alter_ne // lookup_op.
-Qed.
-End properties.
-
-(** Functor *)
-Instance map_fmap_ne `{Countable K} {A B : cofeT} (f : A → B) n :
-  Proper (dist n ==> dist n) f → Proper (dist n ==>dist n) (fmap (M:=gmap K) f).
-Proof. by intros ? m m' Hm k; rewrite !lookup_fmap; apply option_fmap_ne. Qed.
-Instance map_fmap_cmra_monotone `{Countable K} {A B : cmraT} (f : A → B)
-  `{!CMRAMonotone f} : CMRAMonotone (fmap f : gmap K A → gmap K B).
-Proof.
-  split.
-  - intros m1 m2 n; rewrite !map_includedN_spec; intros Hm i.
-    by rewrite !lookup_fmap; apply: includedN_preserving.
-  - by intros n m ? i; rewrite lookup_fmap; apply validN_preserving.
-Qed.
-Definition mapC_map `{Countable K} {A B} (f: A -n> B) : mapC K A -n> mapC K B :=
-  CofeMor (fmap f : mapC K A → mapC K B).
-Instance mapC_map_ne `{Countable K} {A B} n :
-  Proper (dist n ==> dist n) (@mapC_map K _ _ A B).
-Proof.
-  intros f g Hf m k; rewrite /= !lookup_fmap.
-  destruct (_ !! k) eqn:?; simpl; constructor; apply Hf.
-Qed.
-
-Program Definition mapF K `{Countable K} (Σ : iFunctor) : iFunctor := {|
-  ifunctor_car := mapRA K ∘ Σ; ifunctor_map A B := mapC_map ∘ ifunctor_map Σ
-|}.
-Next Obligation.
-  by intros K ?? Σ A B n f g Hfg; apply mapC_map_ne, ifunctor_map_ne.
-Qed.
-Next Obligation.
-  intros K ?? Σ A x. rewrite /= -{2}(map_fmap_id x).
-  apply map_fmap_setoid_ext=> ? y _; apply ifunctor_map_id.
-Qed.
-Next Obligation.
-  intros K ?? Σ A B C f g x. rewrite /= -map_fmap_compose.
-  apply map_fmap_setoid_ext=> ? y _; apply ifunctor_map_compose.
-Qed.

algebra/functor.v

-From algebra Require Export cmra.
-
-(** * Functors from COFE to CMRA *)
-(* TODO RJ: Maybe find a better name for this? It is not PL-specific any more. *)
-Structure iFunctor := IFunctor {
-  ifunctor_car :> cofeT → cmraT;
-  ifunctor_map {A B} (f : A -n> B) : ifunctor_car A -n> ifunctor_car B;
-  ifunctor_map_ne {A B} n : Proper (dist n ==> dist n) (@ifunctor_map A B);
-  ifunctor_map_id {A : cofeT} (x : ifunctor_car A) : ifunctor_map cid x ≡ x;
-  ifunctor_map_compose {A B C} (f : A -n> B) (g : B -n> C) x :
-    ifunctor_map (g ◎ f) x ≡ ifunctor_map g (ifunctor_map f x);
-  ifunctor_map_mono {A B} (f : A -n> B) : CMRAMonotone (ifunctor_map f)
-}.
-Existing Instances ifunctor_map_ne ifunctor_map_mono.
-
-Lemma ifunctor_map_ext (Σ : iFunctor) {A B} (f g : A -n> B) m :
-  (∀ x, f x ≡ g x) → ifunctor_map Σ f m ≡ ifunctor_map Σ g m.
-Proof. by intros; apply (ne_proper (@ifunctor_map Σ A B)). Qed.
-
-(** * Functor combinators *)
-(** We create a functor combinators for all CMRAs in the algebra directory.
-These combinators can be used to conveniently construct the global CMRA of
-the Iris program logic. Note that we have explicitly built in functor
-composition into these combinators, instead of having a notion of a functor
-from the category of CMRAs to the category of CMRAs which we can compose. This
-way we can convenient deal with (indexed) products in a uniform way. *)
-Program Definition constF (B : cmraT) : iFunctor :=
-  {| ifunctor_car A := B; ifunctor_map A1 A2 f := cid |}.
-Solve Obligations with done.
-
-Program Definition prodF (Σ1 Σ2 : iFunctor) : iFunctor := {|
-  ifunctor_car A := prodRA (Σ1 A) (Σ2 A);
-  ifunctor_map A B f := prodC_map (ifunctor_map Σ1 f) (ifunctor_map Σ2 f)
-|}.
-Next Obligation.
-  by intros Σ1 Σ2 A B n f g Hfg; apply prodC_map_ne; apply ifunctor_map_ne.
-Qed.
-Next Obligation. by intros Σ1 Σ2 A [??]; rewrite /= !ifunctor_map_id. Qed.
-Next Obligation.
-  by intros Σ1 Σ2 A B C f g [??]; rewrite /= !ifunctor_map_compose.
-Qed.

algebra/iprod.v

-From algebra Require Export cmra.
-From algebra Require Import functor upred.
-
-(** * Indexed product *)
-(** Need to put this in a definition to make canonical structures to work. *)
-Definition iprod {A} (B : A → cofeT) := ∀ x, B x.
-Definition iprod_insert {A} {B : A → cofeT} `{∀ x x' : A, Decision (x = x')}
-    (x : A) (y : B x) (f : iprod B) : iprod B := λ x',
-  match decide (x = x') with left H => eq_rect _ B y _ H | right _ => f x' end.
-Global Instance iprod_empty {A} {B : A → cofeT}
-  `{∀ x, Empty (B x)} : Empty (iprod B) := λ x, ∅.
-Definition iprod_singleton {A} {B : A → cofeT} 
-    `{∀ x x' : A, Decision (x = x'), ∀ x : A, Empty (B x)}
-  (x : A) (y : B x) : iprod B := iprod_insert x y ∅.
-Instance: Params (@iprod_insert) 4.
-Instance: Params (@iprod_singleton) 5.
-
-Section iprod_cofe.
-  Context {A} {B : A → cofeT}.
-  Implicit Types x : A.
-  Implicit Types f g : iprod B.
-
-  Instance iprod_equiv : Equiv (iprod B) := λ f g, ∀ x, f x ≡ g x.
-  Instance iprod_dist : Dist (iprod B) := λ n f g, ∀ x, f x ≡{n}≡ g x.
-  Program Definition iprod_chain (c : chain (iprod B)) (x : A) : chain (B x) :=
-    {| chain_car n := c n x |}.
-  Next Obligation. by intros c x n i ?; apply (chain_cauchy c). Qed.
-  Program Instance iprod_compl : Compl (iprod B) := λ c x,
-    compl (iprod_chain c x).
-  Definition iprod_cofe_mixin : CofeMixin (iprod B).
-  Proof.
-    split.
-    - intros f g; split; [intros Hfg n k; apply equiv_dist, Hfg|].
-      intros Hfg k; apply equiv_dist; intros n; apply Hfg.
-    - intros n; split.
-      + by intros f x.
-      + by intros f g ? x.
-      + by intros f g h ?? x; transitivity (g x).
-    - intros n f g Hfg x; apply dist_S, Hfg.
-    - intros n c x.
-      rewrite /compl /iprod_compl (conv_compl n (iprod_chain c x)).
-      apply (chain_cauchy c); lia.
-  Qed.
-  Canonical Structure iprodC : cofeT := CofeT iprod_cofe_mixin.
-
-  (** Properties of empty *)
-  Section empty.
-    Context `{∀ x, Empty (B x)}.
-    Definition iprod_lookup_empty  x : ∅ x = ∅ := eq_refl.
-    Global Instance iprod_empty_timeless :
-      (∀ x : A, Timeless (∅ : B x)) → Timeless (∅ : iprod B).
-    Proof. intros ? f Hf x. by apply: timeless. Qed.
-  End empty.
-
-  (** Properties of iprod_insert. *)
-  Context `{∀ x x' : A, Decision (x = x')}.
-
-  Global Instance iprod_insert_ne n x :
-    Proper (dist n ==> dist n ==> dist n) (iprod_insert x).
-  Proof.
-    intros y1 y2 ? f1 f2 ? x'; rewrite /iprod_insert.
-    by destruct (decide _) as [[]|].
-  Qed.
-  Global Instance iprod_insert_proper x :
-    Proper ((≡) ==> (≡) ==> (≡)) (iprod_insert x) := ne_proper_2 _.
-
-  Lemma iprod_lookup_insert f x y : (iprod_insert x y f) x = y.
-  Proof.
-    rewrite /iprod_insert; destruct (decide _) as [Hx|]; last done.
-    by rewrite (proof_irrel Hx eq_refl).
-  Qed.
-  Lemma iprod_lookup_insert_ne f x x' y :
-    x ≠ x' → (iprod_insert x y f) x' = f x'.
-  Proof. by rewrite /iprod_insert; destruct (decide _). Qed.
-
-  Global Instance iprod_lookup_timeless f x : Timeless f → Timeless (f x).
-  Proof.
-    intros ? y ?.
-    cut (f ≡ iprod_insert x y f).
-    { by move=> /(_ x)->; rewrite iprod_lookup_insert. }
-    by apply: timeless=>x'; destruct (decide (x = x')) as [->|];
-      rewrite ?iprod_lookup_insert ?iprod_lookup_insert_ne.
-  Qed.
-  Global Instance iprod_insert_timeless f x y :
-    Timeless f → Timeless y → Timeless (iprod_insert x y f).
-  Proof.
-    intros ?? g Heq x'; destruct (decide (x = x')) as [->|].
-    - rewrite iprod_lookup_insert.
-      apply: timeless. by rewrite -(Heq x') iprod_lookup_insert.
-    - rewrite iprod_lookup_insert_ne //.
-      apply: timeless. by rewrite -(Heq x') iprod_lookup_insert_ne.
-  Qed.
-
-  (** Properties of iprod_singletom. *)
-  Context `{∀ x : A, Empty (B x)}.
-
-  Global Instance iprod_singleton_ne n x :
-    Proper (dist n ==> dist n) (iprod_singleton x).
-  Proof. by intros y1 y2 Hy; rewrite /iprod_singleton Hy. Qed.
-  Global Instance iprod_singleton_proper x :
-    Proper ((≡) ==> (≡)) (iprod_singleton x) := ne_proper _.
-
-  Lemma iprod_lookup_singleton x y : (iprod_singleton x y) x = y.
-  Proof. by rewrite /iprod_singleton iprod_lookup_insert. Qed.
-  Lemma iprod_lookup_singleton_ne x x' y: x ≠ x' → (iprod_singleton x y) x' = ∅.
-  Proof. intros; by rewrite /iprod_singleton iprod_lookup_insert_ne. Qed.
-
-  Global Instance iprod_singleton_timeless x (y : B x) :
-    (∀ x : A, Timeless (∅ : B x)) → Timeless y → Timeless (iprod_singleton x y).
-  Proof. eauto using iprod_insert_timeless, iprod_empty_timeless. Qed.
-End iprod_cofe.
-
-Arguments iprodC {_} _.
-
-Section iprod_cmra.
-  Context {A} {B : A → cmraT}.
-  Implicit Types f g : iprod B.
-
-  Instance iprod_op : Op (iprod B) := λ f g x, f x ⋅ g x.
-  Instance iprod_unit : Unit (iprod B) := λ f x, unit (f x).
-  Instance iprod_validN : ValidN (iprod B) := λ n f, ∀ x, ✓{n} f x.
-  Instance iprod_minus : Minus (iprod B) := λ f g x, f x ⩪ g x.
-
-  Definition iprod_lookup_op f g x : (f ⋅ g) x = f x ⋅ g x := eq_refl.
-  Definition iprod_lookup_unit f x : (unit f) x = unit (f x) := eq_refl.
-  Definition iprod_lookup_minus f g x : (f ⩪ g) x = f x ⩪ g x := eq_refl.
-
-  Lemma iprod_includedN_spec (f g : iprod B) n : f ≼{n} g ↔ ∀ x, f x ≼{n} g x.
-  Proof.
-    split.
-    - by intros [h Hh] x; exists (h x); rewrite /op /iprod_op (Hh x).
-    - intros Hh; exists (g ⩪ f)=> x; specialize (Hh x).
-      by rewrite /op /iprod_op /minus /iprod_minus cmra_op_minus.
-  Qed.
-
-  Definition iprod_cmra_mixin : CMRAMixin (iprod B).
-  Proof.
-    split.
-    - by intros n f1 f2 f3 Hf x; rewrite iprod_lookup_op (Hf x).
-    - by intros n f1 f2 Hf x; rewrite iprod_lookup_unit (Hf x).
-    - by intros n f1 f2 Hf ? x; rewrite -(Hf x).
-    - by intros n f f' Hf g g' Hg i; rewrite iprod_lookup_minus (Hf i) (Hg i).
-    - intros n f Hf x; apply cmra_validN_S, Hf.
-    - by intros f1 f2 f3 x; rewrite iprod_lookup_op assoc.
-    - by intros f1 f2 x; rewrite iprod_lookup_op comm.
-    - by intros f x; rewrite iprod_lookup_op iprod_lookup_unit cmra_unit_l.
-    - by intros f x; rewrite iprod_lookup_unit cmra_unit_idemp.
-    - intros n f1 f2; rewrite !iprod_includedN_spec=> Hf x.
-      by rewrite iprod_lookup_unit; apply cmra_unit_preservingN, Hf.
-    - intros n f1 f2 Hf x; apply cmra_validN_op_l with (f2 x), Hf.
-    - intros n f1 f2; rewrite iprod_includedN_spec=> Hf x.
-      by rewrite iprod_lookup_op iprod_lookup_minus cmra_op_minus; try apply Hf.
-  Qed.
-  Definition iprod_cmra_extend_mixin : CMRAExtendMixin (iprod B).
-  Proof.
-    intros n f f1 f2 Hf Hf12.
-    set (g x := cmra_extend_op n (f x) (f1 x) (f2 x) (Hf x) (Hf12 x)).
-    exists ((λ x, (proj1_sig (g x)).1), (λ x, (proj1_sig (g x)).2)).
-    split_and?; intros x; apply (proj2_sig (g x)).
-  Qed.
-  Canonical Structure iprodRA : cmraT :=
-    CMRAT iprod_cofe_mixin iprod_cmra_mixin iprod_cmra_extend_mixin.
-  Global Instance iprod_cmra_identity `{∀ x, Empty (B x)} :
-    (∀ x, CMRAIdentity (B x)) → CMRAIdentity iprodRA.
-  Proof.
-    intros ?; split.
-    - intros n x; apply cmra_empty_valid.
-    - by intros f x; rewrite iprod_lookup_op left_id.
-    - by apply _.
-  Qed.
-
-  (** Internalized properties *)
-  Lemma iprod_equivI {M} g1 g2 : (g1 ≡ g2)%I ≡ (∀ i, g1 i ≡ g2 i : uPred M)%I.
-  Proof. done. Qed.
-  Lemma iprod_validI {M} g : (✓ g)%I ≡ (∀ i, ✓ g i : uPred M)%I.
-  Proof. done. Qed.
-
-  (** Properties of iprod_insert. *)
-  Context `{∀ x x' : A, Decision (x = x')}.
-
-  Lemma iprod_insert_updateP x (P : B x → Prop) (Q : iprod B → Prop) g y1 :
-    y1 ~~>: P → (∀ y2, P y2 → Q (iprod_insert x y2 g)) →
-    iprod_insert x y1 g ~~>: Q.
-  Proof.
-    intros Hy1 HP n gf Hg. destruct (Hy1 n (gf x)) as (y2&?&?).
-    { move: (Hg x). by rewrite iprod_lookup_op iprod_lookup_insert. }
-    exists (iprod_insert x y2 g); split; [auto|].
-    intros x'; destruct (decide (x' = x)) as [->|];
-      rewrite iprod_lookup_op ?iprod_lookup_insert //; [].
-    move: (Hg x'). by rewrite iprod_lookup_op !iprod_lookup_insert_ne.
-  Qed.
-
-  Lemma iprod_insert_updateP' x (P : B x → Prop) g y1 :
-    y1 ~~>: P →
-    iprod_insert x y1 g ~~>: λ g', ∃ y2, g' = iprod_insert x y2 g ∧ P y2.
-  Proof. eauto using iprod_insert_updateP. Qed.
-  Lemma iprod_insert_update g x y1 y2 :
-    y1 ~~> y2 → iprod_insert x y1 g ~~> iprod_insert x y2 g.
-  Proof.
-    rewrite !cmra_update_updateP; eauto using iprod_insert_updateP with subst.
-  Qed.
-
-  (** Properties of iprod_singleton. *)
-  Context `{∀ x, Empty (B x), ∀ x, CMRAIdentity (B x)}.
-
-  Lemma iprod_singleton_validN n x (y: B x) : ✓{n} iprod_singleton x y ↔ ✓{n} y.
-  Proof.
-    split; [by move=>/(_ x); rewrite iprod_lookup_singleton|].
-    move=>Hx x'; destruct (decide (x = x')) as [->|];
-      rewrite ?iprod_lookup_singleton ?iprod_lookup_singleton_ne //.
-    by apply cmra_empty_valid.
-  Qed.
-
-  Lemma iprod_unit_singleton x (y : B x) :
-    unit (iprod_singleton x y) ≡ iprod_singleton x (unit y).
-  Proof.
-    by move=>x'; destruct (decide (x = x')) as [->|];
-      rewrite iprod_lookup_unit ?iprod_lookup_singleton
-      ?iprod_lookup_singleton_ne // cmra_unit_empty.
-  Qed.
-
-  Lemma iprod_op_singleton (x : A) (y1 y2 : B x) :
-    iprod_singleton x y1 ⋅ iprod_singleton x y2 ≡ iprod_singleton x (y1 ⋅ y2).
-  Proof.
-    intros x'; destruct (decide (x' = x)) as [->|].
-    - by rewrite iprod_lookup_op !iprod_lookup_singleton.
-    - by rewrite iprod_lookup_op !iprod_lookup_singleton_ne // left_id.
-  Qed.
-
-  Lemma iprod_singleton_updateP x (P : B x → Prop) (Q : iprod B → Prop) y1 :
-    y1 ~~>: P → (∀ y2, P y2 → Q (iprod_singleton x y2)) →
-    iprod_singleton x y1 ~~>: Q.
-  Proof. rewrite /iprod_singleton; eauto using iprod_insert_updateP. Qed.
-  Lemma iprod_singleton_updateP' x (P : B x → Prop) y1 :
-    y1 ~~>: P →
-    iprod_singleton x y1 ~~>: λ g, ∃ y2, g = iprod_singleton x y2 ∧ P y2.
-  Proof. eauto using iprod_singleton_updateP. Qed.
-  Lemma iprod_singleton_update x y1 y2 :
-    y1 ~~> y2 → iprod_singleton x y1 ~~> iprod_singleton x y2.
-  Proof. eauto using iprod_insert_update. Qed.
-
-  Lemma iprod_singleton_updateP_empty x (P : B x → Prop) (Q : iprod B → Prop) :
-    ∅ ~~>: P → (∀ y2, P y2 → Q (iprod_singleton x y2)) → ∅ ~~>: Q.
-  Proof.
-    intros Hx HQ n gf Hg. destruct (Hx n (gf x)) as (y2&?&?); first apply Hg.
-    exists (iprod_singleton x y2); split; [by apply HQ|].
-    intros x'; destruct (decide (x' = x)) as [->|].
-    - by rewrite iprod_lookup_op iprod_lookup_singleton.
-    - rewrite iprod_lookup_op iprod_lookup_singleton_ne //. apply Hg.
-  Qed.
-  Lemma iprod_singleton_updateP_empty' x (P : B x → Prop) :
-    ∅ ~~>: P → ∅ ~~>: λ g, ∃ y2, g = iprod_singleton x y2 ∧ P y2.
-  Proof. eauto using iprod_singleton_updateP_empty. Qed.
-End iprod_cmra.
-
-Arguments iprodRA {_} _.
-
-(** * Functor *)
-Definition iprod_map {A} {B1 B2 : A → cofeT} (f : ∀ x, B1 x → B2 x)
-  (g : iprod B1) : iprod B2 := λ x, f _ (g x).
-
-Lemma iprod_map_ext {A} {B1 B2 : A → cofeT} (f1 f2 : ∀ x, B1 x → B2 x) g :
-  (∀ x, f1 x (g x) ≡ f2 x (g x)) → iprod_map f1 g ≡ iprod_map f2 g.
-Proof. done. Qed.
-Lemma iprod_map_id {A} {B: A → cofeT} (g : iprod B) : iprod_map (λ _, id) g = g.
-Proof. done. Qed.
-Lemma iprod_map_compose {A} {B1 B2 B3 : A → cofeT}
-    (f1 : ∀ x, B1 x → B2 x) (f2 : ∀ x, B2 x → B3 x) (g : iprod B1) :
-  iprod_map (λ x, f2 x ∘ f1 x) g = iprod_map f2 (iprod_map f1 g).
-Proof. done. Qed.
-
-Instance iprod_map_ne {A} {B1 B2 : A → cofeT} (f : ∀ x, B1 x → B2 x) n :
-  (∀ x, Proper (dist n ==> dist n) (f x)) →
-  Proper (dist n ==> dist n) (iprod_map f).
-Proof. by intros ? y1 y2 Hy x; rewrite /iprod_map (Hy x). Qed.
-Instance iprod_map_cmra_monotone {A} {B1 B2: A → cmraT} (f : ∀ x, B1 x → B2 x) :
-  (∀ x, CMRAMonotone (f x)) → CMRAMonotone (iprod_map f).
-Proof.
-  split.
-  - intros n g1 g2; rewrite !iprod_includedN_spec=> Hf x.
-    rewrite /iprod_map; apply includedN_preserving, Hf.
-  - intros n g Hg x; rewrite /iprod_map; apply validN_preserving, Hg.
-Qed.
-
-Definition iprodC_map {A} {B1 B2 : A → cofeT} (f : iprod (λ x, B1 x -n> B2 x)) :
-  iprodC B1 -n> iprodC B2 := CofeMor (iprod_map f).
-Instance iprodC_map_ne {A} {B1 B2 : A → cofeT} n :
-  Proper (dist n ==> dist n) (@iprodC_map A B1 B2).
-Proof. intros f1 f2 Hf g x; apply Hf. Qed.
-
-Program Definition iprodF {A} (Σ : A → iFunctor) : iFunctor := {|
-  ifunctor_car B := iprodRA (λ x, Σ x B);
-  ifunctor_map B1 B2 f := iprodC_map (λ x, ifunctor_map (Σ x) f);
-|}.
-Next Obligation.
-  by intros A Σ B1 B2 n f f' ? g; apply iprodC_map_ne=>x; apply ifunctor_map_ne.
-Qed.
-Next Obligation.
-  intros A Σ B g. rewrite /= -{2}(iprod_map_id g).
-  apply iprod_map_ext=> x; apply ifunctor_map_id.
-Qed.
-Next Obligation.
-  intros A Σ B1 B2 B3 f1 f2 g. rewrite /= -iprod_map_compose.
-  apply iprod_map_ext=> y; apply ifunctor_map_compose.
-Qed.

algebra/option.v

-From algebra Require Export cmra.
-From algebra Require Import functor upred.
-
-(* COFE *)
-Section cofe.
-Context {A : cofeT}.
-Inductive option_dist : Dist (option A) :=
-  | Some_dist n x y : x ≡{n}≡ y → Some x ≡{n}≡ Some y
-  | None_dist n : None ≡{n}≡ None.
-Existing Instance option_dist.
-Program Definition option_chain
-    (c : chain (option A)) (x : A) (H : c 1 = Some x) : chain A :=
-  {| chain_car n := from_option x (c n) |}.
-Next Obligation.
-  intros c x ? n [|i] ?; [omega|]; simpl.
-  destruct (c 1) eqn:?; simplify_eq/=.
-  by feed inversion (chain_cauchy c n (S i)).
-Qed.
-Instance option_compl : Compl (option A) := λ c,
-  match Some_dec (c 1) with
-  | inleft (exist x H) => Some (compl (option_chain c x H)) | inright _ => None
-  end.
-Definition option_cofe_mixin : CofeMixin (option A).
-Proof.
-  split.
-  - intros mx my; split; [by destruct 1; constructor; apply equiv_dist|].
-    intros Hxy; feed inversion (Hxy 1); subst; constructor; apply equiv_dist.
-    by intros n; feed inversion (Hxy n).
-  - intros n; split.
-    + by intros [x|]; constructor.
-    + by destruct 1; constructor.
-    + destruct 1; inversion_clear 1; constructor; etransitivity; eauto.
-  - by inversion_clear 1; constructor; apply dist_S.
-  - intros n c; unfold compl, option_compl.
-    destruct (Some_dec (c 1)) as [[x Hx]|].
-    { assert (is_Some (c (S n))) as [y Hy].
-      { feed inversion (chain_cauchy c 0 (S n)); eauto with lia congruence. }
-      rewrite Hy; constructor.
-      by rewrite (conv_compl n (option_chain c x Hx)) /= Hy. }
-    feed inversion (chain_cauchy c 0 (S n)); eauto with lia congruence.
-    constructor.
-Qed.
-Canonical Structure optionC := CofeT option_cofe_mixin.
-Global Instance Some_ne : Proper (dist n ==> dist n) (@Some A).
-Proof. by constructor. Qed.
-Global Instance is_Some_ne n : Proper (dist n ==> iff) (@is_Some A).
-Proof. inversion_clear 1; split; eauto. Qed.
-Global Instance Some_dist_inj : Inj (dist n) (dist n) (@Some A).
-Proof. by inversion_clear 1. Qed.
-Global Instance None_timeless : Timeless (@None A).
-Proof. inversion_clear 1; constructor. Qed.
-Global Instance Some_timeless x : Timeless x → Timeless (Some x).
-Proof. by intros ?; inversion_clear 1; constructor; apply timeless. Qed.
-Global Instance option_timeless `{!∀ a : A, Timeless a} (mx : option A) : Timeless mx.
-Proof. destruct mx; auto with typeclass_instances. Qed.
-End cofe.
-
-Arguments optionC : clear implicits.
-
-(* CMRA *)
-Section cmra.
-Context {A : cmraT}.
-
-Instance option_validN : ValidN (option A) := λ n mx,
-  match mx with Some x => ✓{n} x | None => True end.
-Global Instance option_empty : Empty (option A) := None.
-Instance option_unit : Unit (option A) := fmap unit.
-Instance option_op : Op (option A) := union_with (λ x y, Some (x ⋅ y)).
-Instance option_minus : Minus (option A) :=
-  difference_with (λ x y, Some (x ⩪ y)).
-Lemma option_includedN n (mx my : option A) :
-  mx ≼{n} my ↔ mx = None ∨ ∃ x y, mx = Some x ∧ my = Some y ∧ x ≼{n} y.
-Proof.
-  split.
-  - intros [mz Hmz].
-    destruct mx as [x|]; [right|by left].
-    destruct my as [y|]; [exists x, y|destruct mz; inversion_clear Hmz].
-    destruct mz as [z|]; inversion_clear Hmz; split_and?; auto;
-      cofe_subst; eauto using cmra_includedN_l.
-  - intros [->|(x&y&->&->&z&Hz)]; try (by exists my; destruct my; constructor).
-    by exists (Some z); constructor.
-Qed.
-Lemma None_includedN n (mx : option A) : None ≼{n} mx.
-Proof. rewrite option_includedN; auto. Qed.
-Lemma Some_Some_includedN n (x y : A) : x ≼{n} y → Some x ≼{n} Some y.
-Proof. rewrite option_includedN; eauto 10. Qed.
-Definition Some_op a b : Some (a ⋅ b) = Some a ⋅ Some b := eq_refl.
-
-Definition option_cmra_mixin  : CMRAMixin (option A).
-Proof.
-  split.
-  - by intros n [x|]; destruct 1; constructor; cofe_subst.
-  - by destruct 1; constructor; cofe_subst.
-  - by destruct 1; rewrite /validN /option_validN //=; cofe_subst.
-  - by destruct 1; inversion_clear 1; constructor; cofe_subst.
-  - intros n [x|]; unfold validN, option_validN; eauto using cmra_validN_S.
-  - intros [x|] [y|] [z|]; constructor; rewrite ?assoc; auto.
-  - intros [x|] [y|]; constructor; rewrite 1?comm; auto.
-  - by intros [x|]; constructor; rewrite cmra_unit_l.
-  - by intros [x|]; constructor; rewrite cmra_unit_idemp.
-  - intros n mx my; rewrite !option_includedN;intros [->|(x&y&->&->&?)]; auto.
-    right; exists (unit x), (unit y); eauto using cmra_unit_preservingN.
-  - intros n [x|] [y|]; rewrite /validN /option_validN /=;
-      eauto using cmra_validN_op_l.
-  - intros n mx my; rewrite option_includedN.
-    intros [->|(x&y&->&->&?)]; [by destruct my|].
-    by constructor; apply cmra_op_minus.
-Qed.
-Definition option_cmra_extend_mixin : CMRAExtendMixin (option A).
-Proof.
-  intros n mx my1 my2.
-  destruct mx as [x|], my1 as [y1|], my2 as [y2|]; intros Hx Hx';
-    try (by exfalso; inversion Hx'; auto).
-  - destruct (cmra_extend_op n x y1 y2) as ([z1 z2]&?&?&?); auto.
-    { by inversion_clear Hx'. }
-    by exists (Some z1, Some z2); repeat constructor.
-  - by exists (Some x,None); inversion Hx'; repeat constructor.
-  - by exists (None,Some x); inversion Hx'; repeat constructor.
-  - exists (None,None); repeat constructor.
-Qed.
-Canonical Structure optionRA :=
-  CMRAT option_cofe_mixin option_cmra_mixin option_cmra_extend_mixin.
-Global Instance option_cmra_identity : CMRAIdentity optionRA.
-Proof. split. done. by intros []. by inversion_clear 1. Qed.
-
-(** Misc *)
-Lemma op_is_Some mx my : is_Some (mx ⋅ my) ↔ is_Some mx ∨ is_Some my.
-Proof.
-  destruct mx, my; rewrite /op /option_op /= -!not_eq_None_Some; naive_solver.
-Qed.
-Lemma option_op_positive_dist_l n mx my : mx ⋅ my ≡{n}≡ None → mx ≡{n}≡ None.
-Proof. by destruct mx, my; inversion_clear 1. Qed.
-Lemma option_op_positive_dist_r n mx my : mx ⋅ my ≡{n}≡ None → my ≡{n}≡ None.
-Proof. by destruct mx, my; inversion_clear 1. Qed.
-
-(** Internalized properties *)
-Lemma option_equivI {M} (x y : option A) :
-  (x ≡ y)%I ≡ (match x, y with
-               | Some a, Some b => a ≡ b | None, None => True | _, _ => False
-               end : uPred M)%I.
-Proof. split. by destruct 1. by destruct x, y; try constructor. Qed.
-Lemma option_validI {M} (x : option A) :
-  (✓ x)%I ≡ (match x with Some a => ✓ a | None => True end : uPred M)%I.
-Proof. by destruct x. Qed.
-
-(** Updates *)
-Lemma option_updateP (P : A → Prop) (Q : option A → Prop) x :
-  x ~~>: P → (∀ y, P y → Q (Some y)) → Some x ~~>: Q.
-Proof.
-  intros Hx Hy n [y|] ?.
-  { destruct (Hx n y) as (y'&?&?); auto. exists (Some y'); auto. }
-  destruct (Hx n (unit x)) as (y'&?&?); rewrite ?cmra_unit_r; auto.
-  by exists (Some y'); split; [auto|apply cmra_validN_op_l with (unit x)].
-Qed.
-Lemma option_updateP' (P : A → Prop) x :
-  x ~~>: P → Some x ~~>: λ y, default False y P.
-Proof. eauto using option_updateP. Qed.
-Lemma option_update x y : x ~~> y → Some x ~~> Some y.
-Proof.
-  rewrite !cmra_update_updateP; eauto using option_updateP with congruence.
-Qed.
-Lemma option_update_None `{Empty A, !CMRAIdentity A} : ∅ ~~> Some ∅.
-Proof.
-  intros n [x|] ?; rewrite /op /cmra_op /validN /cmra_validN /= ?left_id;
-    auto using cmra_empty_valid.
-Qed.
-End cmra.
-Arguments optionRA : clear implicits.
-
-(** Functor *)
-Instance option_fmap_ne {A B : cofeT} (f : A → B) n:
-  Proper (dist n ==> dist n) f → Proper (dist n==>dist n) (fmap (M:=option) f).
-Proof. by intros Hf; destruct 1; constructor; apply Hf. Qed.
-Instance option_fmap_cmra_monotone {A B : cmraT} (f: A → B) `{!CMRAMonotone f} :
-  CMRAMonotone (fmap f : option A → option B).
-Proof.
-  split.
-  - intros n mx my; rewrite !option_includedN.
-    intros [->|(x&y&->&->&?)]; simpl; eauto 10 using @includedN_preserving.
-  - by intros n [x|] ?; rewrite /cmra_validN /=; try apply validN_preserving.
-Qed.
-Definition optionC_map {A B} (f : A -n> B) : optionC A -n> optionC B :=
-  CofeMor (fmap f : optionC A → optionC B).
-Instance optionC_map_ne A B n : Proper (dist n ==> dist n) (@optionC_map A B).
-Proof. by intros f f' Hf []; constructor; apply Hf. Qed.
-
-Program Definition optionF (Σ : iFunctor) : iFunctor := {|
-  ifunctor_car := optionRA ∘ Σ; ifunctor_map A B := optionC_map ∘ ifunctor_map Σ
-|}.
-Next Obligation.
-  by intros Σ A B n f g Hfg; apply optionC_map_ne, ifunctor_map_ne.
-Qed.
-Next Obligation.
-  intros Σ A x. rewrite /= -{2}(option_fmap_id x).
-  apply option_fmap_setoid_ext=>y; apply ifunctor_map_id.
-Qed.
-Next Obligation.
-  intros Σ A B C f g x. rewrite /= -option_fmap_compose.
-  apply option_fmap_setoid_ext=>y; apply ifunctor_map_compose.
-Qed.

algebra/sts.v

-From prelude Require Export sets.
-From algebra Require Export cmra.
-From algebra Require Import dra.
-Local Arguments valid _ _ !_ /.
-Local Arguments op _ _ !_ !_ /.
-Local Arguments unit _ _ !_ /.
-
-(** * Definition of STSs *)
-Module sts.
-Structure stsT := STS {
-  state : Type;
-  token : Type;
-  prim_step : relation state;
-  tok : state → set token;
-}.
-Arguments STS {_ _} _ _.
-Arguments prim_step {_} _ _.
-Arguments tok {_} _.
-Notation states sts := (set (state sts)).
-Notation tokens sts := (set (token sts)).
-
-(** * Theory and definitions *)
-Section sts.
-Context {sts : stsT}.
-
-(** ** Step relations *)
-Inductive step : relation (state sts * tokens sts) :=
-  | Step s1 s2 T1 T2 :
-     (* TODO: This asks for ⊥ on sets: T1 ⊥ T2 := T1 ∩ T2 ⊆ ∅. *)
-     prim_step s1 s2 → tok s1 ∩ T1 ≡ ∅ → tok s2 ∩ T2 ≡ ∅ →
-     tok s1 ∪ T1 ≡ tok s2 ∪ T2 → step (s1,T1) (s2,T2).
-Inductive frame_step (T : tokens sts) (s1 s2 : state sts) : Prop :=
-  | Frame_step T1 T2 :
-     T1 ∩ (tok s1 ∪ T) ≡ ∅ → step (s1,T1) (s2,T2) → frame_step T s1 s2.
-
-(** ** Closure under frame steps *)
-Record closed (S : states sts) (T : tokens sts) : Prop := Closed {
-  closed_ne : S ≢ ∅;
-  closed_disjoint s : s ∈ S → tok s ∩ T ⊆ ∅;
-  closed_step s1 s2 : s1 ∈ S → frame_step T s1 s2 → s2 ∈ S
-}.
-Definition up (s : state sts) (T : tokens sts) : states sts :=
-  mkSet (rtc (frame_step T) s).
-Definition up_set (S : states sts) (T : tokens sts) : states sts :=
-  S ≫= λ s, up s T.
-
-(** Tactic setup *)
-Hint Resolve Step.
-Hint Extern 10 (equiv (A:=set _) _ _) => set_solver : sts.
-Hint Extern 10 (¬equiv (A:=set _) _ _) => set_solver : sts.
-Hint Extern 10 (_ ∈ _) => set_solver : sts.
-Hint Extern 10 (_ ⊆ _) => set_solver : sts.
-
-(** ** Setoids *)
-Instance framestep_mono : Proper (flip (⊆) ==> (=) ==> (=) ==> impl) frame_step.
-Proof.
-  intros ?? HT ?? <- ?? <-; destruct 1; econstructor;
-    eauto with sts; set_solver.
-Qed.
-Global Instance framestep_proper : Proper ((≡) ==> (=) ==> (=) ==> iff) frame_step.
-Proof. by intros ?? [??] ??????; split; apply framestep_mono. Qed.
-Instance closed_proper' : Proper ((≡) ==> (≡) ==> impl) closed.
-Proof.
-  intros ?? HT ?? HS; destruct 1;
-    constructor; intros until 0; rewrite -?HS -?HT; eauto.
-Qed.
-Global Instance closed_proper : Proper ((≡) ==> (≡) ==> iff) closed.
-Proof. by split; apply closed_proper'. Qed.
-Global Instance up_preserving : Proper ((=) ==> flip (⊆) ==> (⊆)) up.
-Proof.
-  intros s ? <- T T' HT ; 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.
-Global Instance up_proper : Proper ((=) ==> (≡) ==> (≡)) up.
-Proof. by intros ??? ?? [??]; split; apply up_preserving. Qed.
-Global Instance up_set_preserving : Proper ((⊆) ==> flip (⊆) ==> (⊆)) up_set.
-Proof.
-  intros S1 S2 HS T1 T2 HT. rewrite /up_set.
-  f_equiv; last done. move =>s1 s2 Hs. simpl in HT. by apply up_preserving.
-Qed.
-Global Instance up_set_proper : Proper ((≡) ==> (≡) ==> (≡)) up_set.
-Proof. by intros S1 S2 [??] T1 T2 [??]; split; apply up_set_preserving. Qed.
-
-(** ** Properties of closure under frame steps *)
-Lemma closed_disjoint' S T s : closed S T → s ∈ S → tok s ∩ T ≡ ∅.
-Proof. intros [_ ? _]; set_solver. Qed.
-Lemma closed_steps S T s1 s2 :
-  closed S T → s1 ∈ S → rtc (frame_step T) s1 s2 → s2 ∈ S.
-Proof. induction 3; eauto using closed_step. Qed.
-Lemma closed_op T1 T2 S1 S2 :
-  closed S1 T1 → closed S2 T2 →
-  T1 ∩ T2 ≡ ∅ → S1 ∩ S2 ≢ ∅ → closed (S1 ∩ S2) (T1 ∪ T2).
-Proof.
-  intros [_ ? Hstep1] [_ ? Hstep2] ?; split; [done|set_solver|].
-  intros s3 s4; rewrite !elem_of_intersection; intros [??] [T3 T4 ?]; split.
-  - apply Hstep1 with s3, Frame_step with T3 T4; auto with sts.
-  - apply Hstep2 with s3, Frame_step with T3 T4; auto with sts.
-Qed.
-Lemma step_closed s1 s2 T1 T2 S Tf :
-  step (s1,T1) (s2,T2) → closed S Tf → s1 ∈ S → T1 ∩ Tf ≡ ∅ →
-  s2 ∈ S ∧ T2 ∩ Tf ≡ ∅ ∧ tok s2 ∩ T2 ≡ ∅.
-Proof.
-  inversion_clear 1 as [???? HR Hs1 Hs2]; intros [?? Hstep]??; split_and?; auto.
-  - eapply Hstep with s1, Frame_step with T1 T2; auto with sts.
-  - set_solver -Hstep Hs1 Hs2.
-Qed.
-
-(** ** Properties of the closure operators *)
-Lemma elem_of_up s T : s ∈ up s T.
-Proof. constructor. Qed.
-Lemma subseteq_up_set S T : S ⊆ up_set S T.
-Proof. intros s ?; apply elem_of_bind; eauto using elem_of_up. Qed.
-Lemma up_up_set s T : up s T ≡ up_set {[ s ]} T.
-Proof. by rewrite /up_set collection_bind_singleton. Qed.
-Lemma closed_up_set S T :
-  (∀ s, s ∈ S → tok s ∩ T ⊆ ∅) → S ≢ ∅ → closed (up_set S T) T.
-Proof.
-  intros HS Hne; unfold up_set; split.
-  - assert (∀ s, s ∈ up s T) by eauto using elem_of_up. set_solver.
-  - intros s; rewrite !elem_of_bind; intros (s'&Hstep&Hs').
-    specialize (HS s' Hs'); clear Hs' Hne S.
-    induction Hstep as [s|s1 s2 s3 [T1 T2 ? Hstep] ? IH]; first done.
-    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 : S ≢ ∅ → closed (up_set S ∅) ∅.
-Proof. eauto using closed_up_set with sts. Qed.
-Lemma closed_up s T : tok s ∩ T ≡ ∅ → closed (up s T) T.
-Proof.
-  intros; rewrite -(collection_bind_singleton (λ s, up s T) s).
-  apply closed_up_set; set_solver.
-Qed.
-Lemma closed_up_empty s : closed (up s ∅) ∅.
-Proof. eauto using closed_up with sts. Qed.
-Lemma up_closed S T : closed S T → up_set S T ≡ 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.
-End sts. End sts.
-
-Notation stsT := sts.stsT.
-Notation STS := sts.STS.
-
-(** * STSs form a disjoint RA *)
-(* This module should never be imported, uses the module [sts] below. *)
-Module sts_dra.
-Import sts.
-
-(* The type of bounds we can give to the state of an STS. This is the type
-   that we equip with an RA structure. *)
-Inductive car (sts : stsT) :=
-  | auth : state sts → set (token sts) → car sts
-  | frag : set (state sts) → set (token sts ) → car sts.
-Arguments auth {_} _ _.
-Arguments frag {_} _ _.
-
-Section sts_dra.
-Context {sts : stsT}.
-Infix "≼" := dra_included.
-Implicit Types S : states sts.
-Implicit Types T : tokens sts.
-
-Inductive sts_equiv : Equiv (car sts) :=
-  | 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.
-Existing Instance sts_equiv.
-Instance sts_valid : Valid (car sts) := λ x,
-  match x with auth s T => tok s ∩ T ≡ ∅ | frag S' T => closed S' T end.
-Instance sts_unit : Unit (car sts) := λ x,
-  match x with
-  | frag S' _ => frag (up_set S' ∅ ) ∅
-  | auth s _  => frag (up s ∅) ∅
-  end.
-Inductive sts_disjoint : Disjoint (car sts) :=
-  | frag_frag_disjoint S1 S2 T1 T2 :
-     S1 ∩ S2 ≢ ∅ → 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.
-Existing Instance sts_disjoint.
-Instance sts_op : Op (car sts) := λ 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.
-Instance sts_minus : Minus (car sts) := λ x1 x2,
-  match x1, x2 with
-  | frag S1 T1, frag S2 T2 => frag (up_set S1 (T1 ∖ T2)) (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 s (T1 ∖ T2)) (T1 ∖ T2)
-  end.
-
-Hint Extern 10 (equiv (A:=set _) _ _) => set_solver : sts.
-Hint Extern 10 (¬equiv (A:=set _) _ _) => set_solver : sts.
-Hint Extern 10 (_ ∈ _) => set_solver : sts.
-Hint Extern 10 (_ ⊆ _) => set_solver : sts.
-Instance sts_equivalence: Equivalence ((≡) : relation (car sts)).
-Proof.
-  split.
-  - by intros []; constructor.
-  - by destruct 1; constructor.
-  - destruct 1; inversion_clear 1; constructor; etransitivity; eauto.
-Qed.
-Global Instance sts_dra : DRA (car sts).
-Proof.
-  split.
-  - apply _.
-  - by do 2 destruct 1; constructor; setoid_subst.
-  - by destruct 1; constructor; setoid_subst.
-  - by destruct 1; simpl; intros ?; setoid_subst.
-  - by intros ? [|]; destruct 1; inversion_clear 1; constructor; setoid_subst.
-  - by do 2 destruct 1; constructor; setoid_subst.
-  - assert (∀ T T' S s,
-      closed S T → s ∈ S → tok s ∩ T' ≡ ∅ → tok s ∩ (T ∪ T') ≡ ∅).
-    { intros S T T' s [??]; set_solver. }
-    destruct 3; simpl in *; auto using closed_op with sts.
-  - intros []; simpl; eauto using closed_up, closed_up_set, closed_ne with sts.
-  - intros ???? (z&Hy&?&Hxz); destruct Hxz; inversion Hy;clear Hy; setoid_subst;
-      rewrite ?disjoint_union_difference; auto using closed_up with sts.
-    eapply closed_up_set; eauto 2 using closed_disjoint with sts.
-  - intros [] [] []; constructor; rewrite ?assoc; 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 [|S T]; constructor; auto using elem_of_up with sts.
-    assert (S ⊆ up_set S ∅ ∧ S ≢ ∅) by eauto using subseteq_up_set, closed_ne.
-    set_solver.
-  - 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.
-    + rewrite (up_closed (up _ _)); auto using closed_up with sts.
-    + rewrite (up_closed (up_set _ _));
-        eauto using closed_up_set, closed_ne with sts.
-  - intros x y ?? (z&Hy&?&Hxz); exists (unit (x ⋅ y)); split_and?.
-    + destruct Hxz;inversion_clear Hy;constructor;unfold up_set; set_solver.
-    + destruct Hxz; inversion_clear Hy; simpl;
-        auto using closed_up_set_empty, closed_up_empty with sts.
-    + destruct Hxz; inversion_clear Hy; constructor;
-        repeat match goal with
-        | |- context [ up_set ?S ?T ] =>
-           unless (S ⊆ up_set S T) by done; pose proof (subseteq_up_set S T)
-        | |- context [ up ?s ?T ] =>
-           unless (s ∈ up s T) by done; pose proof (elem_of_up s T)
-        end; auto with sts.
-  - intros x y ?? (z&Hy&_&Hxz); destruct Hxz; inversion_clear Hy; constructor;
-      repeat match goal with
-      | |- context [ up_set ?S ?T ] =>
-         unless (S ⊆ up_set S T) by done; pose proof (subseteq_up_set S T)
-      | |- context [ up ?s ?T ] =>
-           unless (s ∈ up s T) by done; pose proof (elem_of_up s T)
-      end; auto with sts.
-  - intros x y ?? (z&Hy&?&Hxz); destruct Hxz as [S1 S2 T1 T2| |];
-      inversion Hy; clear Hy; constructor; setoid_subst;
-      rewrite ?disjoint_union_difference; auto.
-    split; [|apply intersection_greatest; auto using subseteq_up_set with sts].
-    apply intersection_greatest; [auto with sts|].
-    intros s2; rewrite elem_of_intersection.
-    unfold up_set; rewrite elem_of_bind; intros (?&s1&?&?&?).
-    apply closed_steps with T2 s1; auto with sts.
-Qed.
-Canonical Structure RA : cmraT := validityRA (car sts).
-End sts_dra. End sts_dra.
-
-(** * The STS Resource Algebra *)
-(** Finally, the general theory of STS that should be used by users *)
-Notation stsRA := (@sts_dra.RA).
-
-Section sts_definitions.
-  Context {sts : stsT}.
-  Definition sts_auth (s : sts.state sts) (T : sts.tokens sts) : stsRA sts :=
-    to_validity (sts_dra.auth s T).
-  Definition sts_frag (S : sts.states sts) (T : sts.tokens sts) : stsRA sts :=
-    to_validity (sts_dra.frag S T).
-  Definition sts_frag_up (s : sts.state sts) (T : sts.tokens sts) : stsRA sts :=
-    sts_frag (sts.up s T) T.
-End sts_definitions.
-Instance: Params (@sts_auth) 2.
-Instance: Params (@sts_frag) 1.
-Instance: Params (@sts_frag_up) 2.
-
-Section stsRA.
-Import sts.
-Context {sts : stsT}.
-Implicit Types s : state sts.
-Implicit Types S : states sts.
-Implicit Types T : tokens sts.
-
-(** Setoids *)
-Global Instance sts_auth_proper s : Proper ((≡) ==> (≡)) (sts_auth s).
-Proof. (* this proof is horrible *)
-  intros T1 T2 HT. rewrite /sts_auth.
-  by eapply to_validity_proper; try apply _; constructor.
-Qed.
-Global Instance sts_frag_proper : Proper ((≡) ==> (≡) ==> (≡)) (@sts_frag sts).
-Proof.
-  intros S1 S2 ? T1 T2 HT; rewrite /sts_auth.
-  by eapply to_validity_proper; try apply _; constructor.
-Qed.
-Global Instance sts_frag_up_proper s : Proper ((≡) ==> (≡)) (sts_frag_up s).
-Proof. intros T1 T2 HT. by rewrite /sts_frag_up HT. Qed.
-
-(** Validity *)
-Lemma sts_auth_valid s T : ✓ sts_auth s T ↔ tok s ∩ T ≡ ∅.
-Proof. split. by move=> /(_ 0). by intros ??. Qed.
-Lemma sts_frag_valid S T : ✓ sts_frag S T ↔ closed S T.
-Proof. split. by move=> /(_ 0). by intros ??. Qed.
-Lemma sts_frag_up_valid s T : tok s ∩ T ≡ ∅ → ✓ sts_frag_up s T.
-Proof. intros; by apply sts_frag_valid, closed_up. Qed.
-
-Lemma sts_auth_frag_valid_inv s S T1 T2 :
-  ✓ (sts_auth s T1 ⋅ sts_frag S T2) → s ∈ S.
-Proof. by move=> /(_ 0) [? [? Hdisj]]; inversion Hdisj. Qed.
-
-(** Op *)
-Lemma sts_op_auth_frag s S T :
-  s ∈ S → closed S T → sts_auth s ∅ ⋅ sts_frag S T ≡ sts_auth s T.
-Proof.
-  intros; split; [split|constructor; set_solver]; simpl.
-  - intros (?&?&?); by apply closed_disjoint' with S.
-  - intros; split_and?. set_solver+. done. constructor; set_solver.
-Qed.
-Lemma sts_op_auth_frag_up s T :
-  tok s ∩ T ≡ ∅ → sts_auth s ∅ ⋅ sts_frag_up s T ≡ sts_auth s T.
-Proof. intros; apply sts_op_auth_frag; auto using elem_of_up, closed_up. Qed.
-
-Lemma sts_op_frag S1 S2 T1 T2 :
-  T1 ∩ T2 ⊆ ∅ → sts.closed S1 T1 → sts.closed S2 T2 →
-  sts_frag (S1 ∩ S2) (T1 ∪ T2) ≡ sts_frag S1 T1 ⋅ sts_frag S2 T2.
-Proof.
-  intros HT HS1 HS2. rewrite /sts_frag.
-  (* FIXME why does rewrite not work?? *)
-  etransitivity; last eapply to_validity_op; try done; [].
-  intros Hval. constructor; last set_solver. eapply closed_ne, Hval.
-Qed.
-
-(** Frame preserving updates *)
-Lemma sts_update_auth s1 s2 T1 T2 :
-  step (s1,T1) (s2,T2) → sts_auth s1 T1 ~~> sts_auth s2 T2.
-Proof.
-  intros ?; apply validity_update; inversion 3 as [|? S ? Tf|]; subst.
-  destruct (step_closed s1 s2 T1 T2 S Tf) as (?&?&?); auto.
-  repeat (done || constructor).
-Qed.
-
-Lemma sts_update_frag S1 S2 T :
-  closed S2 T → S1 ⊆ S2 → sts_frag S1 T ~~> sts_frag S2 T.
-Proof.
-  rewrite /sts_frag=> HS Hcl. apply validity_update.
-  inversion 3 as [|? S ? Tf|]; simplify_eq/=.
-  - split; first done. constructor; [set_solver|done].
-  - split; first done. constructor; set_solver.
-Qed.
-
-Lemma sts_update_frag_up s1 S2 T :
-  closed S2 T → s1 ∈ S2 → sts_frag_up s1 T ~~> sts_frag S2 T.
-Proof.
-  intros; by apply sts_update_frag; [|intros ?; eauto using closed_steps].
-Qed.
-
-(** Inclusion *)
-Lemma sts_frag_included S1 S2 T1 T2 :
-  closed S2 T2 →
-  sts_frag S1 T1 ≼ sts_frag S2 T2 ↔
-  (closed S1 T1 ∧ ∃ Tf, T2 ≡ T1 ∪ Tf ∧ T1 ∩ Tf ≡ ∅ ∧ S2 ≡ S1 ∩ up_set S2 Tf).
-Proof. (* This should use some general properties of DRAs. To be improved
-when we have RAs back *)
-  move=>Hcl2. split.
-  - intros [[[Sf Tf|Sf Tf] vf Hvf] EQ].
-    { exfalso. inversion_clear EQ as [Hv EQ']. apply EQ' in Hcl2. simpl in Hcl2.
-      inversion Hcl2. }
-    inversion_clear EQ as [Hv EQ'].
-    move:(EQ' Hcl2)=>{EQ'} EQ. inversion_clear EQ as [|? ? ? ? HT HS].
-    destruct Hv as [Hv _]. move:(Hv Hcl2)=>{Hv} [/= Hcl1  [Hclf Hdisj]].
-    apply Hvf in Hclf. simpl in Hclf. clear Hvf.
-    inversion_clear Hdisj. split; last (exists Tf; split_and?); [done..|].
-    apply (anti_symm (⊆)).
-    + move=>s HS2. apply elem_of_intersection. split; first by apply HS.
-      by apply subseteq_up_set.
-    + move=>s /elem_of_intersection [HS1 Hscl]. apply HS. split; first done.
-      destruct Hscl as [s' [Hsup Hs']].
-      eapply closed_steps; last (hnf in Hsup; eexact Hsup); first done.
-      set_solver +HS Hs'.
-  - intros (Hcl1 & Tf & Htk & Hf & Hs).
-    exists (sts_frag (up_set S2 Tf) Tf).
-    split; first split; simpl;[|done|].
-    + intros _. split_and?; first done.
-      * apply closed_up_set; last by eapply closed_ne.
-        move=>s Hs2. move:(closed_disjoint _ _ Hcl2 _ Hs2).
-        set_solver +Htk.
-      * constructor; last done. rewrite -Hs. by eapply closed_ne.
-    + intros _. constructor; [ set_solver +Htk | done].
-Qed.
-
-Lemma sts_frag_included' S1 S2 T :
-  closed S2 T → closed S1 T → S2 ≡ S1 ∩ up_set S2 ∅ →
-  sts_frag S1 T ≼ sts_frag S2 T.
-Proof.
-  intros. apply sts_frag_included; split_and?; auto.
-  exists ∅; split_and?; done || set_solver+.
-Qed.
-End stsRA.

algebra/upred.v

-From algebra Require Export cmra.
-Local Hint Extern 1 (_ ≼ _) => etransitivity; [eassumption|].
-Local Hint Extern 1 (_ ≼ _) => etransitivity; [|eassumption].
-Local Hint Extern 10 (_ ≤ _) => omega.
-
-Record uPred (M : cmraT) : Type := IProp {
-  uPred_holds :> nat → M → Prop;
-  uPred_ne n x1 x2 : uPred_holds n x1 → x1 ≡{n}≡ x2 → uPred_holds n x2;
-  uPred_weaken  n1 n2 x1 x2 :
-    uPred_holds n1 x1 → x1 ≼ x2 → n2 ≤ n1 → ✓{n2} x2 → uPred_holds n2 x2
-}.
-Arguments uPred_holds {_} _ _ _ : simpl never.
-Global Opaque uPred_holds.
-Local Transparent uPred_holds.
-Add Printing Constructor uPred.
-Instance: Params (@uPred_holds) 3.
-
-Delimit Scope uPred_scope with I.
-Bind Scope uPred_scope with uPred.
-Arguments uPred_holds {_} _%I _ _.
-
-Section cofe.
-  Context {M : cmraT}.
-  Instance uPred_equiv : Equiv (uPred M) := λ P Q, ∀ n x,
-    ✓{n} x → P n x ↔ Q n x.
-  Instance uPred_dist : Dist (uPred M) := λ n P Q, ∀ n' x,
-    n' ≤ n → ✓{n'} x → P n' x ↔ Q n' x.
-  Program Instance uPred_compl : Compl (uPred M) := λ c,
-    {| uPred_holds n x := c (S n) n x |}.
-  Next Obligation. by intros c n x y ??; simpl in *; apply uPred_ne with x. Qed.
-  Next Obligation.
-    intros c n1 n2 x1 x2 ????; simpl in *.
-    apply (chain_cauchy c n2 (S n1)); eauto using uPred_weaken.
-  Qed.
-  Definition uPred_cofe_mixin : CofeMixin (uPred M).
-  Proof.
-    split.
-    - intros P Q; split; [by intros HPQ n x i ??; apply HPQ|].
-      intros HPQ n x ?; apply HPQ with 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 i x ??; transitivity (Q i x);[apply HP|apply HQ].
-    - intros n P Q HPQ i x ??; apply HPQ; auto.
-    - intros n c i x ??; symmetry; apply (chain_cauchy c i (S n)); auto.
-  Qed.
-  Canonical Structure uPredC : cofeT := CofeT uPred_cofe_mixin.
-End cofe.
-Arguments uPredC : clear implicits.
-
-Instance uPred_ne' {M} (P : uPred M) n : Proper (dist n ==> iff) (P n).
-Proof. intros x1 x2 Hx; split; eauto using uPred_ne. Qed.
-Instance uPred_proper {M} (P : uPred M) n : Proper ((≡) ==> iff) (P n).
-Proof. by intros x1 x2 Hx; apply uPred_ne', equiv_dist. Qed.
-
-Lemma uPred_holds_ne {M} (P1 P2 : uPred M) n x :
-  P1 ≡{n}≡ P2 → ✓{n} x → P1 n x → P2 n x.
-Proof. intros HP ?; apply HP; auto. Qed.
-Lemma uPred_weaken' {M} (P : uPred M) n1 n2 x1 x2 :
-  x1 ≼ x2 → n2 ≤ n1 → ✓{n2} x2 → P n1 x1 → P n2 x2.
-Proof. eauto using uPred_weaken. Qed.
-
-(** functor *)
-Program Definition uPred_map {M1 M2 : cmraT} (f : M2 -n> M1)
-  `{!CMRAMonotone f} (P : uPred M1) :
-  uPred M2 := {| uPred_holds n x := P n (f x) |}.
-Next Obligation. by intros M1 M2 f ? P y1 y2 n ? Hy; rewrite /= -Hy. Qed.
-Next Obligation.
-  naive_solver eauto using uPred_weaken, included_preserving, validN_preserving.
-Qed.
-Instance uPred_map_ne {M1 M2 : cmraT} (f : M2 -n> M1)
-  `{!CMRAMonotone f} n : Proper (dist n ==> dist n) (uPred_map f).
-Proof.
-  by intros x1 x2 Hx n' y; split; apply Hx; auto using validN_preserving.
-Qed.
-Lemma uPred_map_id {M : cmraT} (P : uPred M): uPred_map cid P ≡ P.
-Proof. by intros n x ?. Qed.
-Lemma uPred_map_compose {M1 M2 M3 : cmraT} (f : M1 -n> M2) (g : M2 -n> M3)
-    `{!CMRAMonotone f, !CMRAMonotone g} (P : uPred M3):
-  uPred_map (g ◎ f) P ≡ uPred_map f (uPred_map g P).
-Proof. by intros n x Hx. Qed.
-Lemma uPred_map_ext {M1 M2 : cmraT} (f g : M1 -n> M2)
-    `{!CMRAMonotone f, !CMRAMonotone g} :
-  (∀ x, f x ≡ g x) → ∀ x, uPred_map f x ≡ uPred_map g x.
-Proof. move=> Hfg x P n Hx /=. by rewrite /uPred_holds /= Hfg. Qed.
-Definition uPredC_map {M1 M2 : cmraT} (f : M2 -n> M1) `{!CMRAMonotone f} :
-  uPredC M1 -n> uPredC M2 := CofeMor (uPred_map f : uPredC M1 → uPredC M2).
-Lemma upredC_map_ne {M1 M2 : cmraT} (f g : M2 -n> M1)
-    `{!CMRAMonotone f, !CMRAMonotone g} n :
-  f ≡{n}≡ g → uPredC_map f ≡{n}≡ uPredC_map g.
-Proof.
-  by intros Hfg P n' y ??;
-    rewrite /uPred_holds /= (dist_le _ _ _ _(Hfg y)); last lia.
-Qed.
-
-(** logical entailement *)
-Definition uPred_entails {M} (P Q : uPred M) := ∀ n x, ✓{n} x → P n x → Q n x.
-Hint Extern 0 (uPred_entails _ _) => reflexivity.
-Instance uPred_entails_rewrite_relation M : RewriteRelation (@uPred_entails M).
-
-(** logical connectives *)
-Program Definition uPred_const {M} (φ : Prop) : uPred M :=
-  {| uPred_holds n x := φ |}.
-Solve Obligations with done.
-Instance uPred_inhabited M : Inhabited (uPred M) := populate (uPred_const True).
-
-Program Definition uPred_and {M} (P Q : uPred M) : uPred M :=
-  {| uPred_holds n x := P n x ∧ Q n x |}.
-Solve Obligations with naive_solver eauto 2 using uPred_ne, uPred_weaken.
-Program Definition uPred_or {M} (P Q : uPred M) : uPred M :=
-  {| uPred_holds n x := P n x ∨ Q n x |}.
-Solve Obligations with naive_solver eauto 2 using uPred_ne, uPred_weaken.
-Program Definition uPred_impl {M} (P Q : uPred M) : uPred M :=
-  {| uPred_holds n x := ∀ n' x',
-       x ≼ x' → n' ≤ n → ✓{n'} x' → P n' x' → Q n' x' |}.
-Next Obligation.
-  intros M P Q n1 x1' x1 HPQ Hx1 n2 x2 ????.
-  destruct (cmra_included_dist_l n1 x1 x2 x1') as (x2'&?&Hx2); auto.
-  assert (x2' ≡{n2}≡ x2) as Hx2' by (by apply dist_le with n1).
-  assert (✓{n2} x2') by (by rewrite Hx2'); rewrite -Hx2'.
-  eauto using uPred_weaken, uPred_ne.
-Qed.
-Next Obligation. intros M P Q [|n] x1 x2; auto with lia. Qed.
-
-Program Definition uPred_forall {M A} (Ψ : A → uPred M) : uPred M :=
-  {| uPred_holds n x := ∀ a, Ψ a n x |}.
-Solve Obligations with naive_solver eauto 2 using uPred_ne, uPred_weaken.
-Program Definition uPred_exist {M A} (Ψ : A → uPred M) : uPred M :=
-  {| uPred_holds n x := ∃ a, Ψ a n x |}.
-Solve Obligations with naive_solver eauto 2 using uPred_ne, uPred_weaken.
-
-Program Definition uPred_eq {M} {A : cofeT} (a1 a2 : A) : uPred M :=
-  {| uPred_holds n x := a1 ≡{n}≡ a2 |}.
-Solve Obligations with naive_solver eauto 2 using (dist_le (A:=A)).
-
-Program Definition uPred_sep {M} (P Q : uPred M) : uPred M :=
-  {| uPred_holds n x := ∃ x1 x2, x ≡{n}≡ x1 ⋅ x2 ∧ P n x1 ∧ Q n x2 |}.
-Next Obligation.
-  by intros M P Q n x y (x1&x2&?&?&?) Hxy; exists x1, x2; rewrite -Hxy.
-Qed.
-Next Obligation.
-  intros M P Q n1 n2 x y (x1&x2&Hx&?&?) Hxy ??.
-  assert (∃ x2', y ≡{n2}≡ x1 ⋅ x2' ∧ x2 ≼ x2') as (x2'&Hy&?).
-  { destruct Hxy as [z Hy]; exists (x2 ⋅ z); split; eauto using cmra_included_l.
-    apply dist_le with n1; auto. by rewrite (assoc op) -Hx Hy. }
-  clear Hxy; cofe_subst y; exists x1, x2'; split_and?; [done| |].
-  - apply uPred_weaken with n1 x1; eauto using cmra_validN_op_l.
-  - apply uPred_weaken with n1 x2; eauto using cmra_validN_op_r.
-Qed.
-
-Program Definition uPred_wand {M} (P Q : uPred M) : uPred M :=
-  {| uPred_holds n x := ∀ n' x',
-       n' ≤ n → ✓{n'} (x ⋅ x') → P n' x' → Q n' (x ⋅ x') |}.
-Next Obligation.
-  intros M P Q n1 x1 x2 HPQ Hx n2 x3 ???; simpl in *.
-  rewrite -(dist_le _ _ _ _ Hx) //; apply HPQ; auto.
-  by rewrite (dist_le _ _ _ _ Hx).
-Qed.
-Next Obligation.
-  intros M P Q n1 n2 x1 x2 HPQ ??? n3 x3 ???; simpl in *.
-  apply uPred_weaken with n3 (x1 ⋅ x3);
-    eauto using cmra_validN_included, cmra_preserving_r.
-Qed.
-
-Program Definition uPred_later {M} (P : uPred M) : uPred M :=
-  {| uPred_holds n x := match n return _ with 0 => True | S n' => P n' x end |}.
-Next Obligation. intros M P [|n] ??; eauto using uPred_ne,(dist_le (A:=M)). Qed.
-Next Obligation.
-  intros M P [|n1] [|n2] x1 x2; eauto using uPred_weaken,cmra_validN_S; try lia.
-Qed.
-Program Definition uPred_always {M} (P : uPred M) : uPred M :=
-  {| uPred_holds n x := P n (unit x) |}.
-Next Obligation. by intros M P x1 x2 n ? Hx; rewrite /= -Hx. Qed.
-Next Obligation.
-  intros M P n1 n2 x1 x2 ????; eapply uPred_weaken with n1 (unit x1);
-    eauto using cmra_unit_preserving, cmra_unit_validN.
-Qed.
-
-Program Definition uPred_ownM {M : cmraT} (a : M) : uPred M :=
-  {| uPred_holds n x := a ≼{n} x |}.
-Next Obligation. by intros M a n x1 x2 [a' ?] Hx; exists a'; rewrite -Hx. Qed.
-Next Obligation.
-  intros M a n1 n2 x1 x [a' Hx1] [x2 Hx] ??.
-  exists (a' ⋅ x2). by rewrite (assoc op) -(dist_le _ _ _ _ Hx1) // Hx.
-Qed.
-Program Definition uPred_valid {M A : cmraT} (a : A) : uPred M :=
-  {| uPred_holds n x := ✓{n} a |}.
-Solve Obligations with naive_solver eauto 2 using cmra_validN_le.
-
-Notation "P ⊑ Q" := (uPred_entails P%I Q%I) (at level 70) : C_scope.
-Notation "(⊑)" := uPred_entails (only parsing) : C_scope.
-Notation "■ φ" := (uPred_const φ%C%type)
-  (at level 20, right associativity) : uPred_scope.
-Notation "x = y" := (uPred_const (x%C%type = y%C%type)) : uPred_scope.
-Notation "'False'" := (uPred_const False) : uPred_scope.
-Notation "'True'" := (uPred_const True) : uPred_scope.
-Infix "∧" := uPred_and : uPred_scope.
-Notation "(∧)" := uPred_and (only parsing) : uPred_scope.
-Infix "∨" := uPred_or : uPred_scope.
-Notation "(∨)" := uPred_or (only parsing) : uPred_scope.
-Infix "→" := uPred_impl : uPred_scope.
-Infix "★" := uPred_sep (at level 80, right associativity) : uPred_scope.
-Notation "(★)" := uPred_sep (only parsing) : uPred_scope.
-Notation "P -★ Q" := (uPred_wand P Q)
-  (at level 199, Q at level 200, right associativity) : uPred_scope.
-Notation "∀ x .. y , P" :=
-  (uPred_forall (λ x, .. (uPred_forall (λ y, P)) ..)%I) : uPred_scope.
-Notation "∃ x .. y , P" :=
-  (uPred_exist (λ x, .. (uPred_exist (λ y, P)) ..)%I) : uPred_scope.
-Notation "▷ P" := (uPred_later P)
-  (at level 20, right associativity) : uPred_scope.
-Notation "□ P" := (uPred_always P)
-  (at level 20, right associativity) : uPred_scope.
-Infix "≡" := uPred_eq : uPred_scope.
-Notation "✓ x" := (uPred_valid x) (at level 20) : uPred_scope.
-
-Definition uPred_iff {M} (P Q : uPred M) : uPred M := ((P → Q) ∧ (Q → P))%I.
-Infix "↔" := uPred_iff : uPred_scope.
-
-Class TimelessP {M} (P : uPred M) := timelessP : ▷ P ⊑ (P ∨ ▷ False).
-Arguments timelessP {_} _ {_} _ _ _ _.
-Class AlwaysStable {M} (P : uPred M) := always_stable : P ⊑ □ P.
-Arguments always_stable {_} _ {_} _ _ _ _.
-
-Module uPred. Section uPred_logic.
-Context {M : cmraT}.
-Implicit Types φ : Prop.
-Implicit Types P Q : uPred M.
-Implicit Types A : Type.
-Notation "P ⊑ Q" := (@uPred_entails M P%I Q%I). (* Force implicit argument M *)
-Arguments uPred_holds {_} !_ _ _ /.
-
-Global Instance: PreOrder (@uPred_entails M).
-Proof. split. by intros P x i. by intros P Q Q' HP HQ x i ??; apply HQ, HP. Qed.
-Global Instance: AntiSymm (≡) (@uPred_entails M).
-Proof. intros P Q HPQ HQP; split; auto. Qed.
-Lemma equiv_spec P Q : P ≡ Q ↔ P ⊑ Q ∧ Q ⊑ P.
-Proof.
-  split; [|by intros [??]; apply (anti_symm (⊑))].
-  intros HPQ; split; intros x i; apply HPQ.
-Qed.
-Global Instance entails_proper :
-  Proper ((≡) ==> (≡) ==> iff) ((⊑) : relation (uPred M)).
-Proof.
-  move => P1 P2 /equiv_spec [HP1 HP2] Q1 Q2 /equiv_spec [HQ1 HQ2]; split; intros.
-  - by transitivity P1; [|transitivity Q1].
-  - by transitivity P2; [|transitivity Q2].
-Qed.
-
-(** Non-expansiveness and setoid morphisms *)
-Global Instance const_proper : Proper (iff ==> (≡)) (@uPred_const M).
-Proof. by intros φ1 φ2 Hφ [|n] ??; try apply Hφ. Qed.
-Global Instance and_ne n : Proper (dist n ==> dist n ==> dist n) (@uPred_and M).
-Proof.
-  intros P P' HP Q Q' HQ; split; intros [??]; split; by apply HP || by apply HQ.
-Qed.
-Global Instance and_proper :
-  Proper ((≡) ==> (≡) ==> (≡)) (@uPred_and M) := ne_proper_2 _.
-Global Instance or_ne n : Proper (dist n ==> dist n ==> dist n) (@uPred_or M).
-Proof.
-  intros P P' HP Q Q' HQ; split; intros [?|?];
-    first [by left; apply HP | by right; apply HQ].
-Qed.
-Global Instance or_proper :
-  Proper ((≡) ==> (≡) ==> (≡)) (@uPred_or M) := ne_proper_2 _.
-Global Instance impl_ne n :
-  Proper (dist n ==> dist n ==> dist n) (@uPred_impl M).
-Proof.
-  intros P P' HP Q Q' HQ; split; intros HPQ x' n'' ????; apply HQ,HPQ,HP; auto.
-Qed.
-Global Instance impl_proper :
-  Proper ((≡) ==> (≡) ==> (≡)) (@uPred_impl M) := ne_proper_2 _.
-Global Instance sep_ne n : Proper (dist n ==> dist n ==> dist n) (@uPred_sep M).
-Proof.
-  intros P P' HP Q Q' HQ n' x ??; split; intros (x1&x2&?&?&?); cofe_subst x;
-    exists x1, x2; split_and?; try (apply HP || apply HQ);
-    eauto using cmra_validN_op_l, cmra_validN_op_r.
-Qed.
-Global Instance sep_proper :
-  Proper ((≡) ==> (≡) ==> (≡)) (@uPred_sep M) := ne_proper_2 _.
-Global Instance wand_ne n :
-  Proper (dist n ==> dist n ==> dist n) (@uPred_wand M).
-Proof.
-  intros P P' HP Q Q' HQ n' x ??; split; intros HPQ n'' x' ???;
-    apply HQ, HPQ, HP; eauto using cmra_validN_op_r.
-Qed.
-Global Instance wand_proper :
-  Proper ((≡) ==> (≡) ==> (≡)) (@uPred_wand M) := ne_proper_2 _.
-Global Instance eq_ne (A : cofeT) n :
-  Proper (dist n ==> dist n ==> dist n) (@uPred_eq M A).
-Proof.
-  intros x x' Hx y y' Hy n' z; split; intros; simpl in *.
-  - by rewrite -(dist_le _ _ _ _ Hx) -?(dist_le _ _ _ _ Hy); auto.
-  - by rewrite (dist_le _ _ _ _ Hx) ?(dist_le _ _ _ _ Hy); auto.
-Qed.
-Global Instance eq_proper (A : cofeT) :
-  Proper ((≡) ==> (≡) ==> (≡)) (@uPred_eq M A) := ne_proper_2 _.
-Global Instance forall_ne A :
-  Proper (pointwise_relation _ (dist n) ==> dist n) (@uPred_forall M A).
-Proof. by intros n Ψ1 Ψ2 HΨ n' x; split; intros HP a; apply HΨ. Qed.
-Global Instance forall_proper A :
-  Proper (pointwise_relation _ (≡) ==> (≡)) (@uPred_forall M A).
-Proof. by intros Ψ1 Ψ2 HΨ n' x; split; intros HP a; apply HΨ. Qed.
-Global Instance exist_ne A :
-  Proper (pointwise_relation _ (dist n) ==> dist n) (@uPred_exist M A).
-Proof. by intros n P1 P2 HP x; split; intros [a ?]; exists a; apply HP. Qed.
-Global Instance exist_proper A :
-  Proper (pointwise_relation _ (≡) ==> (≡)) (@uPred_exist M A).
-Proof. by intros P1 P2 HP n' x; split; intros [a ?]; exists a; apply HP. Qed.
-Global Instance later_contractive : Contractive (@uPred_later M).
-Proof.
-  intros n P Q HPQ [|n'] x ??; simpl; [done|].
-  apply (HPQ n'); eauto using cmra_validN_S.
-Qed.
-Global Instance later_proper :
-  Proper ((≡) ==> (≡)) (@uPred_later M) := ne_proper _.
-Global Instance always_ne n: Proper (dist n ==> dist n) (@uPred_always M).
-Proof. intros P1 P2 HP n' x; split; apply HP; eauto using cmra_unit_validN. Qed.
-Global Instance always_proper :
-  Proper ((≡) ==> (≡)) (@uPred_always M) := ne_proper _.
-Global Instance ownM_ne n : Proper (dist n ==> dist n) (@uPred_ownM M).
-Proof. move=> a b Ha n' x ? /=. by rewrite (dist_le _ _ _ _ Ha); last lia. Qed.
-Global Instance ownM_proper: Proper ((≡) ==> (≡)) (@uPred_ownM M) := ne_proper _.
-Global Instance valid_ne {A : cmraT} n :
-  Proper (dist n ==> dist n) (@uPred_valid M A).
-Proof. move=> a b Ha n' x ? /=. by rewrite (dist_le _ _ _ _ Ha); last lia. Qed.
-Global Instance valid_proper {A : cmraT} :
-  Proper ((≡) ==> (≡)) (@uPred_valid M A) := ne_proper _.
-Global Instance iff_ne n : Proper (dist n ==> dist n ==> dist n) (@uPred_iff M).
-Proof. unfold uPred_iff; solve_proper. Qed.
-Global Instance iff_proper :
-  Proper ((≡) ==> (≡) ==> (≡)) (@uPred_iff M) := ne_proper_2 _.
-
-(** Introduction and elimination rules *)
-Lemma const_intro φ P : φ → P ⊑ ■ φ.
-Proof. by intros ???. Qed.
-Lemma const_elim φ Q R : Q ⊑ ■ φ → (φ → Q ⊑ R) → Q ⊑ R.
-Proof. intros HQP HQR n x ??; apply HQR; first eapply (HQP n); eauto. Qed.
-Lemma False_elim P : False ⊑ P.
-Proof. by intros n x ?. Qed.
-Lemma and_elim_l P Q : (P ∧ Q) ⊑ P.
-Proof. by intros n x ? [??]. Qed.
-Lemma and_elim_r P Q : (P ∧ Q) ⊑ Q.
-Proof. by intros n x ? [??]. Qed.
-Lemma and_intro P Q R : P ⊑ Q → P ⊑ R → P ⊑ (Q ∧ R).
-Proof. intros HQ HR n x ??; split; auto. Qed.
-Lemma or_intro_l P Q : P ⊑ (P ∨ Q).
-Proof. intros n x ??; left; auto. Qed.
-Lemma or_intro_r P Q : Q ⊑ (P ∨ Q).
-Proof. intros n x ??; right; auto. Qed.
-Lemma or_elim P Q R : P ⊑ R → Q ⊑ R → (P ∨ Q) ⊑ R.
-Proof. intros HP HQ n x ? [?|?]. by apply HP. by apply HQ. Qed.
-Lemma impl_intro_r P Q R : (P ∧ Q) ⊑ R → P ⊑ (Q → R).
-Proof.
-  intros HQ; repeat intro; apply HQ; naive_solver eauto using uPred_weaken.
-Qed.
-Lemma impl_elim P Q R : P ⊑ (Q → R) → P ⊑ Q → P ⊑ R.
-Proof. by intros HP HP' n x ??; apply HP with n x, HP'. Qed.
-Lemma forall_intro {A} P (Ψ : A → uPred M): (∀ a, P ⊑ Ψ a) → P ⊑ (∀ a, Ψ a).
-Proof. by intros HPΨ n x ?? a; apply HPΨ. Qed.
-Lemma forall_elim {A} {Ψ : A → uPred M} a : (∀ a, Ψ a) ⊑ Ψ a.
-Proof. intros n x ? HP; apply HP. Qed.
-Lemma exist_intro {A} {Ψ : A → uPred M} a : Ψ a ⊑ (∃ a, Ψ a).
-Proof. by intros n x ??; exists a. Qed.
-Lemma exist_elim {A} (Φ : A → uPred M) Q : (∀ a, Φ a ⊑ Q) → (∃ a, Φ a) ⊑ Q.
-Proof. by intros HΦΨ n x ? [a ?]; apply HΦΨ with a. Qed.
-Lemma eq_refl {A : cofeT} (a : A) P : P ⊑ (a ≡ a).
-Proof. by intros n x ??; simpl. Qed.
-Lemma eq_rewrite {A : cofeT} a b (Ψ : A → uPred M) P
-  `{HΨ : ∀ n, Proper (dist n ==> dist n) Ψ} : P ⊑ (a ≡ b) → P ⊑ Ψ a → P ⊑ Ψ b.
-Proof.
-  intros Hab Ha n x ??; apply HΨ with n a; auto. by symmetry; apply Hab with x.
-Qed.
-Lemma eq_equiv `{Empty M, !CMRAIdentity M} {A : cofeT} (a b : A) :
-  True ⊑ (a ≡ b) → a ≡ b.
-Proof.
-  intros Hab; apply equiv_dist; intros n; apply Hab with ∅; last done.
-  apply cmra_valid_validN, cmra_empty_valid.
-Qed.
-Lemma iff_equiv P Q : True ⊑ (P ↔ Q) → P ≡ Q.
-Proof. by intros HPQ n x ?; split; intros; apply HPQ with n x. Qed.
-
-(* Derived logical stuff *)
-Lemma True_intro P : P ⊑ True.
-Proof. by apply const_intro. Qed.
-Lemma and_elim_l' P Q R : P ⊑ R → (P ∧ Q) ⊑ R.
-Proof. by rewrite and_elim_l. Qed.
-Lemma and_elim_r' P Q R : Q ⊑ R → (P ∧ Q) ⊑ R.
-Proof. by rewrite and_elim_r. Qed.
-Lemma or_intro_l' P Q R : P ⊑ Q → P ⊑ (Q ∨ R).
-Proof. intros ->; apply or_intro_l. Qed.
-Lemma or_intro_r' P Q R : P ⊑ R → P ⊑ (Q ∨ R).
-Proof. intros ->; apply or_intro_r. Qed.
-Lemma exist_intro' {A} P (Ψ : A → uPred M) a : P ⊑ Ψ a → P ⊑ (∃ a, Ψ a).
-Proof. intros ->; apply exist_intro. Qed.
-
-Hint Resolve or_elim or_intro_l' or_intro_r'.
-Hint Resolve and_intro and_elim_l' and_elim_r'.
-Hint Immediate True_intro False_elim.
-
-Lemma impl_intro_l P Q R : (Q ∧ P) ⊑ R → P ⊑ (Q → R).
-Proof. intros HR; apply impl_intro_r; rewrite -HR; auto. Qed.
-Lemma impl_elim_l P Q : ((P → Q) ∧ P) ⊑ Q.
-Proof. apply impl_elim with P; auto. Qed.
-Lemma impl_elim_r P Q : (P ∧ (P → Q)) ⊑ Q.
-Proof. apply impl_elim with P; auto. Qed.
-Lemma impl_elim_l' P Q R : P ⊑ (Q → R) → (P ∧ Q) ⊑ R.
-Proof. intros; apply impl_elim with Q; auto. Qed.
-Lemma impl_elim_r' P Q R : Q ⊑ (P → R) → (P ∧ Q) ⊑ R.
-Proof. intros; apply impl_elim with P; auto. Qed.
-Lemma impl_entails P Q : True ⊑ (P → Q) → P ⊑ Q.
-Proof. intros HPQ; apply impl_elim with P; rewrite -?HPQ; auto. Qed.
-Lemma entails_impl P Q : (P ⊑ Q) → True ⊑ (P → Q).
-Proof. auto using impl_intro_l. Qed.
-
-Lemma const_intro_l φ Q R : φ → (■φ ∧ Q) ⊑ R → Q ⊑ R.
-Proof. intros ? <-; auto using const_intro. Qed.
-Lemma const_intro_r φ Q R : φ → (Q ∧ ■φ) ⊑ R → Q ⊑ R.
-Proof. intros ? <-; auto using const_intro. Qed.
-Lemma const_elim_l φ Q R : (φ → Q ⊑ R) → (■ φ ∧ Q) ⊑ R.
-Proof. intros; apply const_elim with φ; eauto. Qed.
-Lemma const_elim_r φ Q R : (φ → Q ⊑ R) → (Q ∧ ■ φ) ⊑ R.
-Proof. intros; apply const_elim with φ; eauto. Qed.
-Lemma const_equiv (φ : Prop) : φ → (■ φ : uPred M)%I ≡ True%I.
-Proof. intros; apply (anti_symm _); auto using const_intro. Qed.
-Lemma equiv_eq {A : cofeT} P (a b : A) : a ≡ b → P ⊑ (a ≡ b).
-Proof. intros ->; apply eq_refl. Qed.
-Lemma eq_sym {A : cofeT} (a b : A) : (a ≡ b) ⊑ (b ≡ a).
-Proof.
-  apply (eq_rewrite a b (λ b, b ≡ a)%I); auto using eq_refl.
-  intros n; solve_proper.
-Qed.
-
-Lemma const_mono φ1 φ2 : (φ1 → φ2) → ■ φ1 ⊑ ■ φ2.
-Proof. intros; apply const_elim with φ1; eauto using const_intro. Qed.
-Lemma and_mono P P' Q Q' : P ⊑ Q → P' ⊑ Q' → (P ∧ P') ⊑ (Q ∧ Q').
-Proof. auto. Qed.
-Lemma and_mono_l P P' Q : P ⊑ Q → (P ∧ P') ⊑ (Q ∧ P').
-Proof. by intros; apply and_mono. Qed.
-Lemma and_mono_r P P' Q' : P' ⊑ Q' → (P ∧ P') ⊑ (P ∧ Q').
-Proof. by apply and_mono. Qed.
-Lemma or_mono P P' Q Q' : P ⊑ Q → P' ⊑ Q' → (P ∨ P') ⊑ (Q ∨ Q').
-Proof. auto. Qed.
-Lemma or_mono_l P P' Q : P ⊑ Q → (P ∨ P') ⊑ (Q ∨ P').
-Proof. by intros; apply or_mono. Qed.
-Lemma or_mono_r P P' Q' : P' ⊑ Q' → (P ∨ P') ⊑ (P ∨ Q').
-Proof. by apply or_mono. Qed.
-Lemma impl_mono P P' Q Q' : Q ⊑ P → P' ⊑ Q' → (P → P') ⊑ (Q → Q').
-Proof.
-  intros HP HQ'; apply impl_intro_l; rewrite -HQ'.
-  apply impl_elim with P; eauto.
-Qed.
-Lemma forall_mono {A} (Φ Ψ : A → uPred M) :
-  (∀ a, Φ a ⊑ Ψ a) → (∀ a, Φ a) ⊑ (∀ a, Ψ a).
-Proof.
-  intros HP. apply forall_intro=> a; rewrite -(HP a); apply forall_elim.
-Qed.
-Lemma exist_mono {A} (Φ Ψ : A → uPred M) :
-  (∀ a, Φ a ⊑ Ψ a) → (∃ a, Φ a) ⊑ (∃ a, Ψ a).
-Proof. intros HΦ. apply exist_elim=> a; rewrite (HΦ a); apply exist_intro. Qed.
-Global Instance const_mono' : Proper (impl ==> (⊑)) (@uPred_const M).
-Proof. intros φ1 φ2; apply const_mono. Qed.
-Global Instance and_mono' : Proper ((⊑) ==> (⊑) ==> (⊑)) (@uPred_and M).
-Proof. by intros P P' HP Q Q' HQ; apply and_mono. Qed.
-Global Instance and_flip_mono' :
-  Proper (flip (⊑) ==> flip (⊑) ==> flip (⊑)) (@uPred_and M).
-Proof. by intros P P' HP Q Q' HQ; apply and_mono. Qed.
-Global Instance or_mono' : Proper ((⊑) ==> (⊑) ==> (⊑)) (@uPred_or M).
-Proof. by intros P P' HP Q Q' HQ; apply or_mono. Qed.
-Global Instance or_flip_mono' :
-  Proper (flip (⊑) ==> flip (⊑) ==> flip (⊑)) (@uPred_or M).
-Proof. by intros P P' HP Q Q' HQ; apply or_mono. Qed.
-Global Instance impl_mono' :
-  Proper (flip (⊑) ==> (⊑) ==> (⊑)) (@uPred_impl M).
-Proof. by intros P P' HP Q Q' HQ; apply impl_mono. Qed.
-Global Instance forall_mono' A :
-  Proper (pointwise_relation _ (⊑) ==> (⊑)) (@uPred_forall M A).
-Proof. intros P1 P2; apply forall_mono. Qed.
-Global Instance exist_mono' A :
-  Proper (pointwise_relation _ (⊑) ==> (⊑)) (@uPred_exist M A).
-Proof. intros P1 P2; apply exist_mono. Qed.
-
-Global Instance and_idem : IdemP (≡) (@uPred_and M).
-Proof. intros P; apply (anti_symm (⊑)); auto. Qed.
-Global Instance or_idem : IdemP (≡) (@uPred_or M).
-Proof. intros P; apply (anti_symm (⊑)); auto. Qed.
-Global Instance and_comm : Comm (≡) (@uPred_and M).
-Proof. intros P Q; apply (anti_symm (⊑)); auto. Qed.
-Global Instance True_and : LeftId (≡) True%I (@uPred_and M).
-Proof. intros P; apply (anti_symm (⊑)); auto. Qed.
-Global Instance and_True : RightId (≡) True%I (@uPred_and M).
-Proof. intros P; apply (anti_symm (⊑)); auto. Qed.
-Global Instance False_and : LeftAbsorb (≡) False%I (@uPred_and M).
-Proof. intros P; apply (anti_symm (⊑)); auto. Qed.
-Global Instance and_False : RightAbsorb (≡) False%I (@uPred_and M).
-Proof. intros P; apply (anti_symm (⊑)); auto. Qed.
-Global Instance True_or : LeftAbsorb (≡) True%I (@uPred_or M).
-Proof. intros P; apply (anti_symm (⊑)); auto. Qed.
-Global Instance or_True : RightAbsorb (≡) True%I (@uPred_or M).
-Proof. intros P; apply (anti_symm (⊑)); auto. Qed.
-Global Instance False_or : LeftId (≡) False%I (@uPred_or M).
-Proof. intros P; apply (anti_symm (⊑)); auto. Qed.
-Global Instance or_False : RightId (≡) False%I (@uPred_or M).
-Proof. intros P; apply (anti_symm (⊑)); auto. Qed.
-Global Instance and_assoc : Assoc (≡) (@uPred_and M).
-Proof. intros P Q R; apply (anti_symm (⊑)); auto. Qed.
-Global Instance or_comm : Comm (≡) (@uPred_or M).
-Proof. intros P Q; apply (anti_symm (⊑)); auto. Qed.
-Global Instance or_assoc : Assoc (≡) (@uPred_or M).
-Proof. intros P Q R; apply (anti_symm (⊑)); auto. Qed.
-Global Instance True_impl : LeftId (≡) True%I (@uPred_impl M).
-Proof.
-  intros P; apply (anti_symm (⊑)).
-  - by rewrite -(left_id True%I uPred_and (_ → _)%I) impl_elim_r.
-  - by apply impl_intro_l; rewrite left_id.
-Qed.
-Lemma iff_refl Q P : Q ⊑ (P ↔ P).
-Proof. rewrite /uPred_iff; apply and_intro; apply impl_intro_l; auto. Qed.
-
-Lemma or_and_l P Q R : (P ∨ Q ∧ R)%I ≡ ((P ∨ Q) ∧ (P ∨ R))%I.
-Proof.
-  apply (anti_symm (⊑)); first auto.
-  do 2 (apply impl_elim_l', or_elim; apply impl_intro_l); auto.
-Qed.
-Lemma or_and_r P Q R : (P ∧ Q ∨ R)%I ≡ ((P ∨ R) ∧ (Q ∨ R))%I.
-Proof. by rewrite -!(comm _ R) or_and_l. Qed.
-Lemma and_or_l P Q R : (P ∧ (Q ∨ R))%I ≡ (P ∧ Q ∨ P ∧ R)%I.
-Proof.
-  apply (anti_symm (⊑)); last auto.
-  apply impl_elim_r', or_elim; apply impl_intro_l; auto.
-Qed.
-Lemma and_or_r P Q R : ((P ∨ Q) ∧ R)%I ≡ (P ∧ R ∨ Q ∧ R)%I.
-Proof. by rewrite -!(comm _ R) and_or_l. Qed.
-Lemma and_exist_l {A} P (Ψ : A → uPred M) : (P ∧ ∃ a, Ψ a)%I ≡ (∃ a, P ∧ Ψ a)%I.
-Proof.
-  apply (anti_symm (⊑)).
-  - apply impl_elim_r'. apply exist_elim=>a. apply impl_intro_l.
-    by rewrite -(exist_intro a).
-  - apply exist_elim=>a. apply and_intro; first by rewrite and_elim_l.
-    by rewrite -(exist_intro a) and_elim_r.
-Qed.
-Lemma and_exist_r {A} P (Φ: A → uPred M) : ((∃ a, Φ a) ∧ P)%I ≡ (∃ a, Φ a ∧ P)%I.
-Proof.
-  rewrite -(comm _ P) and_exist_l. apply exist_proper=>a. by rewrite comm.
-Qed.
-
-(* BI connectives *)
-Lemma sep_mono P P' Q Q' : P ⊑ Q → P' ⊑ Q' → (P ★ P') ⊑ (Q ★ Q').
-Proof.
-  intros HQ HQ' n' x ? (x1&x2&?&?&?); exists x1, x2; cofe_subst x;
-    eauto 7 using cmra_validN_op_l, cmra_validN_op_r.
-Qed.
-Global Instance True_sep : LeftId (≡) True%I (@uPred_sep M).
-Proof.
-  intros P n x Hvalid; split.
-  - intros (x1&x2&?&_&?); cofe_subst; eauto using uPred_weaken, cmra_included_r.
-  - by intros ?; exists (unit x), x; rewrite cmra_unit_l.
-Qed. 
-Global Instance sep_comm : Comm (≡) (@uPred_sep M).
-Proof.
-  by intros P Q n x ?; split;
-    intros (x1&x2&?&?&?); exists x2, x1; rewrite (comm op).
-Qed.
-Global Instance sep_assoc : Assoc (≡) (@uPred_sep M).
-Proof.
-  intros P Q R n x ?; split.
-  - intros (x1&x2&Hx&?&y1&y2&Hy&?&?); exists (x1 ⋅ y1), y2; split_and?; auto.
-    + by rewrite -(assoc op) -Hy -Hx.
-    + by exists x1, y1.
-  - intros (x1&x2&Hx&(y1&y2&Hy&?&?)&?); exists y1, (y2 ⋅ x2); split_and?; auto.
-    + by rewrite (assoc op) -Hy -Hx.
-    + by exists y2, x2.
-Qed.
-Lemma wand_intro_r P Q R : (P ★ Q) ⊑ R → P ⊑ (Q -★ R).
-Proof.
-  intros HPQR n x ?? n' x' ???; apply HPQR; auto.
-  exists x, x'; split_and?; auto.
-  eapply uPred_weaken with n x; eauto using cmra_validN_op_l.
-Qed.
-Lemma wand_elim_l P Q : ((P -★ Q) ★ P) ⊑ Q.
-Proof. by intros n x ? (x1&x2&Hx&HPQ&?); cofe_subst; apply HPQ. Qed.
-
-(* Derived BI Stuff *)
-Hint Resolve sep_mono.
-Lemma sep_mono_l P P' Q : P ⊑ Q → (P ★ P') ⊑ (Q ★ P').
-Proof. by intros; apply sep_mono. Qed.
-Lemma sep_mono_r P P' Q' : P' ⊑ Q' → (P ★ P') ⊑ (P ★ Q').
-Proof. by apply sep_mono. Qed.
-Global Instance sep_mono' : Proper ((⊑) ==> (⊑) ==> (⊑)) (@uPred_sep M).
-Proof. by intros P P' HP Q Q' HQ; apply sep_mono. Qed.
-Global Instance sep_flip_mono' :
-  Proper (flip (⊑) ==> flip (⊑) ==> flip (⊑)) (@uPred_sep M).
-Proof. by intros P P' HP Q Q' HQ; apply sep_mono. Qed.
-Lemma wand_mono P P' Q Q' : Q ⊑ P → P' ⊑ Q' → (P -★ P') ⊑ (Q -★ Q').
-Proof. intros HP HQ; apply wand_intro_r; rewrite HP -HQ; apply wand_elim_l. Qed.
-Global Instance wand_mono' : Proper (flip (⊑) ==> (⊑) ==> (⊑)) (@uPred_wand M).
-Proof. by intros P P' HP Q Q' HQ; apply wand_mono. Qed.
-
-Global Instance sep_True : RightId (≡) True%I (@uPred_sep M).
-Proof. by intros P; rewrite comm left_id. Qed.
-Lemma sep_elim_l P Q : (P ★ Q) ⊑ P.
-Proof. by rewrite (True_intro Q) right_id. Qed.
-Lemma sep_elim_r P Q : (P ★ Q) ⊑ Q.
-Proof. by rewrite (comm (★))%I; apply sep_elim_l. Qed.
-Lemma sep_elim_l' P Q R : P ⊑ R → (P ★ Q) ⊑ R.
-Proof. intros ->; apply sep_elim_l. Qed.
-Lemma sep_elim_r' P Q R : Q ⊑ R → (P ★ Q) ⊑ R.
-Proof. intros ->; apply sep_elim_r. Qed.
-Hint Resolve sep_elim_l' sep_elim_r'.
-Lemma sep_intro_True_l P Q R : True ⊑ P → R ⊑ Q → R ⊑ (P ★ Q).
-Proof. by intros; rewrite -(left_id True%I uPred_sep R); apply sep_mono. Qed.
-Lemma sep_intro_True_r P Q R : R ⊑ P → True ⊑ Q → R ⊑ (P ★ Q).
-Proof. by intros; rewrite -(right_id True%I uPred_sep R); apply sep_mono. Qed.
-Lemma sep_elim_True_l P Q R : True ⊑ P → (P ★ R) ⊑ Q → R ⊑ Q.
-Proof. by intros HP; rewrite -HP left_id. Qed.
-Lemma sep_elim_True_r P Q R : True ⊑ P → (R ★ P) ⊑ Q → R ⊑ Q.
-Proof. by intros HP; rewrite -HP right_id. Qed.
-Lemma wand_intro_l P Q R : (Q ★ P) ⊑ R → P ⊑ (Q -★ R).
-Proof. rewrite comm; apply wand_intro_r. Qed.
-Lemma wand_elim_r P Q : (P ★ (P -★ Q)) ⊑ Q.
-Proof. rewrite (comm _ P); apply wand_elim_l. Qed.
-Lemma wand_elim_l' P Q R : P ⊑ (Q -★ R) → (P ★ Q) ⊑ R.
-Proof. intros ->; apply wand_elim_l. Qed.
-Lemma wand_elim_r' P Q R : Q ⊑ (P -★ R) → (P ★ Q) ⊑ R.
-Proof. intros ->; apply wand_elim_r. Qed.
-Lemma sep_and P Q : (P ★ Q) ⊑ (P ∧ Q).
-Proof. auto. Qed.
-Lemma impl_wand P Q : (P → Q) ⊑ (P -★ Q).
-Proof. apply wand_intro_r, impl_elim with P; auto. Qed.
-Lemma const_elim_sep_l φ Q R : (φ → Q ⊑ R) → (■ φ ★ Q) ⊑ R.
-Proof. intros; apply const_elim with φ; eauto. Qed.
-Lemma const_elim_sep_r φ Q R : (φ → Q ⊑ R) → (Q ★ ■ φ) ⊑ R.
-Proof. intros; apply const_elim with φ; eauto. Qed.
-
-Global Instance sep_False : LeftAbsorb (≡) False%I (@uPred_sep M).
-Proof. intros P; apply (anti_symm _); auto. Qed.
-Global Instance False_sep : RightAbsorb (≡) False%I (@uPred_sep M).
-Proof. intros P; apply (anti_symm _); auto. Qed.
-
-Lemma sep_and_l P Q R : (P ★ (Q ∧ R)) ⊑ ((P ★ Q) ∧ (P ★ R)).
-Proof. auto. Qed.
-Lemma sep_and_r P Q R : ((P ∧ Q) ★ R) ⊑ ((P ★ R) ∧ (Q ★ R)).
-Proof. auto. Qed.
-Lemma sep_or_l P Q R : (P ★ (Q ∨ R))%I ≡ ((P ★ Q) ∨ (P ★ R))%I.
-Proof.
-  apply (anti_symm (⊑)); last by eauto 8.
-  apply wand_elim_r', or_elim; apply wand_intro_l.
-  - by apply or_intro_l.
-  - by apply or_intro_r.
-Qed.
-Lemma sep_or_r P Q R : ((P ∨ Q) ★ R)%I ≡ ((P ★ R) ∨ (Q ★ R))%I.
-Proof. by rewrite -!(comm _ R) sep_or_l. Qed.
-Lemma sep_exist_l {A} P (Ψ : A → uPred M) : (P ★ ∃ a, Ψ a)%I ≡ (∃ a, P ★ Ψ a)%I.
-Proof.
-  intros; apply (anti_symm (⊑)).
-  - apply wand_elim_r', exist_elim=>a. apply wand_intro_l.
-    by rewrite -(exist_intro a).
-  - apply exist_elim=> a; apply sep_mono; auto using exist_intro.
-Qed.
-Lemma sep_exist_r {A} (Φ: A → uPred M) Q: ((∃ a, Φ a) ★ Q)%I ≡ (∃ a, Φ a ★ Q)%I.
-Proof. setoid_rewrite (comm _ _ Q); apply sep_exist_l. Qed.
-Lemma sep_forall_l {A} P (Ψ : A → uPred M) : (P ★ ∀ a, Ψ a) ⊑ (∀ a, P ★ Ψ a).
-Proof. by apply forall_intro=> a; rewrite forall_elim. Qed.
-Lemma sep_forall_r {A} (Φ : A → uPred M) Q : ((∀ a, Φ a) ★ Q) ⊑ (∀ a, Φ a ★ Q).
-Proof. by apply forall_intro=> a; rewrite forall_elim. Qed.
-
-(* Later *)
-Lemma later_mono P Q : P ⊑ Q → ▷ P ⊑ ▷ Q.
-Proof. intros HP [|n] x ??; [done|apply HP; eauto using cmra_validN_S]. Qed.
-Lemma later_intro P : P ⊑ ▷ P.
-Proof.
-  intros [|n] x ??; simpl in *; [done|].
-  apply uPred_weaken with (S n) x; eauto using cmra_validN_S.
-Qed.
-Lemma löb P : (▷ P → P) ⊑ P.
-Proof.
-  intros n x ? HP; induction n as [|n IH]; [by apply HP|].
-  apply HP, IH, uPred_weaken with (S n) x; eauto using cmra_validN_S.
-Qed.
-Lemma later_True' : True ⊑ (▷ True : uPred M).
-Proof. by intros [|n] x. Qed.
-Lemma later_and P Q : (▷ (P ∧ Q))%I ≡ (▷ P ∧ ▷ Q)%I.
-Proof. by intros [|n] x; split. Qed.
-Lemma later_or P Q : (▷ (P ∨ Q))%I ≡ (▷ P ∨ ▷ Q)%I.
-Proof. intros [|n] x; simpl; tauto. Qed.
-Lemma later_forall {A} (Φ : A → uPred M) : (▷ ∀ a, Φ a)%I ≡ (∀ a, ▷ Φ a)%I.
-Proof. by intros [|n] x. Qed.
-Lemma later_exist_1 {A} (Φ : A → uPred M) : (∃ a, ▷ Φ a) ⊑ (▷ ∃ a, Φ a).
-Proof. by intros [|[|n]] x. Qed.
-Lemma later_exist `{Inhabited A} (Φ : A → uPred M) :
-  (▷ ∃ a, Φ a)%I ≡ (∃ a, ▷ Φ a)%I.
-Proof. intros [|[|n]] x; split; done || by exists inhabitant; simpl. Qed.
-Lemma later_sep P Q : (▷ (P ★ Q))%I ≡ (▷ P ★ ▷ Q)%I.
-Proof.
-  intros n x ?; split.
-  - destruct n as [|n]; simpl.
-    { by exists x, (unit x); rewrite cmra_unit_r. } 
-    intros (x1&x2&Hx&?&?); destruct (cmra_extend_op n x x1 x2)
-      as ([y1 y2]&Hx'&Hy1&Hy2); eauto using cmra_validN_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.
-Qed.
-
-(* Later derived *)
-Global Instance later_mono' : Proper ((⊑) ==> (⊑)) (@uPred_later M).
-Proof. intros P Q; apply later_mono. Qed.
-Lemma later_True : (▷ True : uPred M)%I ≡ True%I.
-Proof. apply (anti_symm (⊑)); auto using later_True'. Qed.
-Lemma later_impl P Q : ▷ (P → Q) ⊑ (▷ P → ▷ Q).
-Proof.
-  apply impl_intro_l; rewrite -later_and.
-  apply later_mono, impl_elim with P; auto.
-Qed.
-Lemma later_wand P Q : ▷ (P -★ Q) ⊑ (▷ P -★ ▷ Q).
-Proof. apply wand_intro_r;rewrite -later_sep; apply later_mono,wand_elim_l. Qed.
-Lemma later_iff P Q : (▷ (P ↔ Q)) ⊑ (▷P ↔ ▷Q).
-Proof. by rewrite /uPred_iff later_and !later_impl. Qed.
-Lemma löb_strong P Q : (P ∧ ▷Q) ⊑ Q → P ⊑ Q.
-Proof.
-  intros Hlöb. apply impl_entails.
-  etransitivity; last by eapply löb.
-  apply impl_intro_l, impl_intro_l. rewrite right_id -{2}Hlöb.
-  apply and_intro; first by eauto.
-  by rewrite {1}(later_intro P) later_impl impl_elim_r.
-Qed.       
-Lemma löb_all_1 {A} (Φ Ψ : A → uPred M) :
-  (∀ a, (▷ (∀ b, Φ b → Ψ b) ∧ Φ a) ⊑ Ψ a) → ∀ a, Φ a ⊑ Ψ a.
-Proof.
-  intros Hlöb a.
-  (* Part I: Revert all the bits we need for the induction into the conclusion. *)
-  apply impl_entails.
-  rewrite -[(Φ a → Ψ a)%I](forall_elim (Ψ := λ a, Φ a → Ψ a)%I a). clear a.
-  (* Part II: Perform induction. *)
-  apply löb_strong, forall_intro=>a. apply impl_intro_r.
-  by rewrite left_id Hlöb.
-Qed.
-
-(* Always *)
-Lemma always_const φ : (□ ■ φ : uPred M)%I ≡ (■ φ)%I.
-Proof. done. Qed.
-Lemma always_elim P : □ P ⊑ P.
-Proof. intros n x ?; simpl; eauto using uPred_weaken, cmra_included_unit. Qed.
-Lemma always_intro' P Q : □ P ⊑ Q → □ P ⊑ □ Q.
-Proof.
-  intros HPQ n x ??; apply HPQ; simpl in *; auto using cmra_unit_validN.
-  by rewrite cmra_unit_idemp.
-Qed.
-Lemma always_and P Q : (□ (P ∧ Q))%I ≡ (□ P ∧ □ Q)%I.
-Proof. done. Qed.
-Lemma always_or P Q : (□ (P ∨ Q))%I ≡ (□ P ∨ □ Q)%I.
-Proof. done. Qed.
-Lemma always_forall {A} (Ψ : A → uPred M) : (□ ∀ a, Ψ a)%I ≡ (∀ a, □ Ψ a)%I.
-Proof. done. Qed.
-Lemma always_exist {A} (Ψ : A → uPred M) : (□ ∃ a, Ψ a)%I ≡ (∃ a, □ Ψ a)%I.
-Proof. done. Qed.
-Lemma always_and_sep_1 P Q : □ (P ∧ Q) ⊑ □ (P ★ Q).
-Proof.
-  intros n x ? [??]; exists (unit x), (unit x); rewrite cmra_unit_unit; auto.
-Qed.
-Lemma always_and_sep_l_1 P Q : (□ P ∧ Q) ⊑ (□ P ★ Q).
-Proof.
-  intros n x ? [??]; exists (unit x), x; simpl in *.
-  by rewrite cmra_unit_l cmra_unit_idemp.
-Qed.
-Lemma always_later P : (□ ▷ P)%I ≡ (▷ □ P)%I.
-Proof. done. Qed.
-
-(* Always derived *)
-Lemma always_mono P Q : P ⊑ Q → □ P ⊑ □ Q.
-Proof. intros. apply always_intro'. by rewrite always_elim. Qed.
-Hint Resolve always_mono.
-Global Instance always_mono' : Proper ((⊑) ==> (⊑)) (@uPred_always M).
-Proof. intros P Q; apply always_mono. Qed.
-Lemma always_impl P Q : □ (P → Q) ⊑ (□ P → □ Q).
-Proof.
-  apply impl_intro_l; rewrite -always_and.
-  apply always_mono, impl_elim with P; auto.
-Qed.
-Lemma always_eq {A:cofeT} (a b : A) : (□ (a ≡ b))%I ≡ (a ≡ b : uPred M)%I.
-Proof.
-  apply (anti_symm (⊑)); auto using always_elim.
-  apply (eq_rewrite a b (λ b, □ (a ≡ b))%I); auto.
-  { intros n; solve_proper. }
-  rewrite -(eq_refl _ True) always_const; auto.
-Qed.
-Lemma always_and_sep P Q : (□ (P ∧ Q))%I ≡ (□ (P ★ Q))%I.
-Proof. apply (anti_symm (⊑)); auto using always_and_sep_1. Qed.
-Lemma always_and_sep_l' P Q : (□ P ∧ Q)%I ≡ (□ P ★ Q)%I.
-Proof. apply (anti_symm (⊑)); auto using always_and_sep_l_1. Qed.
-Lemma always_and_sep_r' P Q : (P ∧ □ Q)%I ≡ (P ★ □ Q)%I.
-Proof. by rewrite !(comm _ P) always_and_sep_l'. Qed.
-Lemma always_sep P Q : (□ (P ★ Q))%I ≡ (□ P ★ □ Q)%I.
-Proof. by rewrite -always_and_sep -always_and_sep_l' always_and. Qed.
-Lemma always_wand P Q : □ (P -★ Q) ⊑ (□ P -★ □ Q).
-Proof. by apply wand_intro_r; rewrite -always_sep wand_elim_l. Qed.
-Lemma always_sep_dup' P : (□ P)%I ≡ (□ P ★ □ P)%I.
-Proof. by rewrite -always_sep -always_and_sep (idemp _). Qed.
-Lemma always_wand_impl P Q : (□ (P -★ Q))%I ≡ (□ (P → Q))%I.
-Proof.
-  apply (anti_symm (⊑)); [|by rewrite -impl_wand].
-  apply always_intro', impl_intro_r.
-  by rewrite always_and_sep_l' always_elim wand_elim_l.
-Qed.
-Lemma always_entails_l' P Q : (P ⊑ □ Q) → P ⊑ (□ Q ★ P).
-Proof. intros; rewrite -always_and_sep_l'; auto. Qed.
-Lemma always_entails_r' P Q : (P ⊑ □ Q) → P ⊑ (P ★ □ Q).
-Proof. intros; rewrite -always_and_sep_r'; auto. Qed.
-
-(* Own *)
-Lemma ownM_op (a1 a2 : M) :
-  uPred_ownM (a1 ⋅ a2) ≡ (uPred_ownM a1 ★ uPred_ownM a2)%I.
-Proof.
-  intros n x ?; split.
-  - intros [z ?]; exists a1, (a2 ⋅ z); split; [by rewrite (assoc op)|].
-    split. by exists (unit a1); rewrite cmra_unit_r. by exists z.
-  - intros (y1&y2&Hx&[z1 Hy1]&[z2 Hy2]); exists (z1 ⋅ z2).
-    by rewrite (assoc op _ z1) -(comm op z1) (assoc op z1)
-      -(assoc op _ a2) (comm op z1) -Hy1 -Hy2.
-Qed.
-Lemma always_ownM_unit (a : M) : (□ uPred_ownM (unit a))%I ≡ uPred_ownM (unit a).
-Proof.
-  intros n x; split; [by apply always_elim|intros [a' Hx]]; simpl.
-  rewrite -(cmra_unit_idemp a) Hx.
-  apply cmra_unit_preservingN, cmra_includedN_l.
-Qed.
-Lemma always_ownM (a : M) : unit a ≡ a → (□ uPred_ownM a)%I ≡ uPred_ownM a.
-Proof. by intros <-; rewrite always_ownM_unit. Qed.
-Lemma ownM_something : True ⊑ ∃ a, uPred_ownM a.
-Proof. intros n x ??. by exists x; simpl. Qed.
-Lemma ownM_empty `{Empty M, !CMRAIdentity M} : True ⊑ uPred_ownM ∅.
-Proof. intros n x ??; by  exists x; rewrite left_id. Qed.
-
-(* Valid *)
-Lemma ownM_valid (a : M) : uPred_ownM a ⊑ ✓ a.
-Proof. intros n x Hv [a' ?]; cofe_subst; eauto using cmra_validN_op_l. Qed.
-Lemma valid_intro {A : cmraT} (a : A) : ✓ a → True ⊑ ✓ a.
-Proof. by intros ? n x ? _; simpl; apply cmra_valid_validN. Qed.
-Lemma valid_elim {A : cmraT} (a : A) : ¬ ✓{0} a → ✓ a ⊑ False.
-Proof. intros Ha n x ??; apply Ha, cmra_validN_le with n; auto. Qed.
-Lemma always_valid {A : cmraT} (a : A) : (□ (✓ a))%I ≡ (✓ a : uPred M)%I.
-Proof. done. Qed.
-Lemma valid_weaken {A : cmraT} (a b : A) : ✓ (a ⋅ b) ⊑ ✓ a.
-Proof. intros n x _; apply cmra_validN_op_l. Qed.
-
-(* Own and valid derived *)
-Lemma ownM_invalid (a : M) : ¬ ✓{0} a → uPred_ownM a ⊑ False.
-Proof. by intros; rewrite ownM_valid valid_elim. Qed.
-Global Instance ownM_mono : Proper (flip (≼) ==> (⊑)) (@uPred_ownM M).
-Proof. intros x y [z ->]. rewrite ownM_op. eauto. Qed.
-
-(* Products *)
-Lemma prod_equivI {A B : cofeT} (x y : A * B) :
-  (x ≡ y)%I ≡ (x.1 ≡ y.1 ∧ x.2 ≡ y.2 : uPred M)%I.
-Proof. done. Qed.
-Lemma prod_validI {A B : cmraT} (x : A * B) :
-  (✓ x)%I ≡ (✓ x.1 ∧ ✓ x.2 : uPred M)%I.
-Proof. done. Qed.
-
-(* Later *)
-Lemma later_equivI {A : cofeT} (x y : later A) :
-  (x ≡ y)%I ≡ (▷ (later_car x ≡ later_car y) : uPred M)%I.
-Proof. done. Qed.
-
-(* Discrete *)
-(* For equality, there already is timeless_eq *)
-Lemma discrete_validI {A : cofeT} `{∀ x : A, Timeless x}
-  `{Op A, Valid A, Unit A, Minus A} (ra : RA A) (x : discreteRA ra) :
-  (✓ x)%I ≡ (■ ✓ x : uPred M)%I.
-Proof. done. Qed.
-
-(* Timeless *)
-Lemma timelessP_spec P : TimelessP P ↔ ∀ n x, ✓{n} x → P 0 x → P n x.
-Proof.
-  split.
-  - intros HP n x ??; induction n as [|n]; auto.
-    by destruct (HP (S n) x); auto using cmra_validN_S.
-  - move=> HP [|n] x /=; auto; left.
-    apply HP, uPred_weaken with n x; eauto using cmra_validN_le.
-Qed.
-Global Instance const_timeless φ : TimelessP (■ φ : uPred M)%I.
-Proof. by apply timelessP_spec=> -[|n] x. Qed.
-Global Instance and_timeless P Q: TimelessP P → TimelessP Q → TimelessP (P ∧ Q).
-Proof. by intros ??; rewrite /TimelessP later_and or_and_r; apply and_mono. Qed.
-Global Instance or_timeless P Q : TimelessP P → TimelessP Q → TimelessP (P ∨ Q).
-Proof.
-  intros; rewrite /TimelessP later_or (timelessP P) (timelessP Q); eauto 10.
-Qed.
-Global Instance impl_timeless P Q : TimelessP Q → TimelessP (P → Q).
-Proof.
-  rewrite !timelessP_spec=> HP [|n] x ? HPQ [|n'] x' ????; auto.
-  apply HP, HPQ, uPred_weaken with (S n') x'; eauto using cmra_validN_le.
-Qed.
-Global Instance sep_timeless P Q: TimelessP P → TimelessP Q → TimelessP (P ★ Q).
-Proof.
-  intros; rewrite /TimelessP later_sep (timelessP P) (timelessP Q).
-  apply wand_elim_l', or_elim; apply wand_intro_r; auto.
-  apply wand_elim_r', or_elim; apply wand_intro_r; auto.
-  rewrite ?(comm _ Q); auto.
-Qed.
-Global Instance wand_timeless P Q : TimelessP Q → TimelessP (P -★ Q).
-Proof.
-  rewrite !timelessP_spec=> HP [|n] x ? HPQ [|n'] x' ???; auto.
-  apply HP, HPQ, uPred_weaken with (S n') x';
-    eauto 3 using cmra_validN_le, cmra_validN_op_r.
-Qed.
-Global Instance forall_timeless {A} (Ψ : A → uPred M) :
-  (∀ x, TimelessP (Ψ x)) → TimelessP (∀ x, Ψ x).
-Proof. by setoid_rewrite timelessP_spec=> HΨ n x ?? a; apply HΨ. Qed.
-Global Instance exist_timeless {A} (Ψ : A → uPred M) :
-  (∀ x, TimelessP (Ψ x)) → TimelessP (∃ x, Ψ x).
-Proof.
-  by setoid_rewrite timelessP_spec=> HΨ [|n] x ?;
-    [|intros [a ?]; exists a; apply HΨ].
-Qed.
-Global Instance always_timeless P : TimelessP P → TimelessP (□ P).
-Proof.
-  intros ?; rewrite /TimelessP.
-  by rewrite -always_const -!always_later -always_or; apply always_mono.
-Qed.
-Global Instance eq_timeless {A : cofeT} (a b : A) :
-  Timeless a → TimelessP (a ≡ b : uPred M)%I.
-Proof. by intro; apply timelessP_spec=> n x ??; apply equiv_dist, timeless. Qed.
-Global Instance ownM_timeless (a : M) : Timeless a → TimelessP (uPred_ownM a).
-Proof.
-  intros ?; apply timelessP_spec=> n x ??; apply cmra_included_includedN,
-    cmra_timeless_included_l; eauto using cmra_validN_le.
-Qed.
-Lemma timeless_eq {A : cofeT} (a b : A) :
-  Timeless a → (a ≡ b)%I ≡ (■(a ≡ b) : uPred M)%I.
-Proof.
-  intros ?. apply (anti_symm (⊑)).
-  - move=>n x ? ? /=. by apply (timeless_iff n a).
-  - eapply const_elim; first done. move=>->. apply eq_refl.
-Qed.
-
-(* Always stable *)
-Local Notation AS := AlwaysStable.
-Global Instance const_always_stable φ : AS (■ φ : uPred M)%I.
-Proof. by rewrite /AlwaysStable always_const. Qed.
-Global Instance always_always_stable P : AS (□ P).
-Proof. by intros; apply always_intro'. Qed.
-Global Instance and_always_stable P Q: AS P → AS Q → AS (P ∧ Q).
-Proof. by intros; rewrite /AlwaysStable always_and; apply and_mono. Qed.
-Global Instance or_always_stable P Q : AS P → AS Q → AS (P ∨ Q).
-Proof. by intros; rewrite /AlwaysStable always_or; apply or_mono. Qed.
-Global Instance sep_always_stable P Q: AS P → AS Q → AS (P ★ Q).
-Proof. by intros; rewrite /AlwaysStable always_sep; apply sep_mono. Qed.
-Global Instance forall_always_stable {A} (Ψ : A → uPred M) :
-  (∀ x, AS (Ψ x)) → AS (∀ x, Ψ x).
-Proof. by intros; rewrite /AlwaysStable always_forall; apply forall_mono. Qed.
-Global Instance exist_always_stable {A} (Ψ : A → uPred M) :
-  (∀ x, AS (Ψ x)) → AS (∃ x, Ψ x).
-Proof. by intros; rewrite /AlwaysStable always_exist; apply exist_mono. Qed.
-Global Instance eq_always_stable {A : cofeT} (a b : A) : AS (a ≡ b : uPred M)%I.
-Proof. by intros; rewrite /AlwaysStable always_eq. Qed.
-Global Instance valid_always_stable {A : cmraT} (a : A) : AS (✓ a : uPred M)%I.
-Proof. by intros; rewrite /AlwaysStable always_valid. Qed.
-Global Instance later_always_stable P : AS P → AS (▷ P).
-Proof. by intros; rewrite /AlwaysStable always_later; apply later_mono. Qed.
-Global Instance ownM_unit_always_stable (a : M) : AS (uPred_ownM (unit a)).
-Proof. by rewrite /AlwaysStable always_ownM_unit. Qed.
-Global Instance default_always_stable {A} P (Ψ : A → uPred M) (mx : option A) :
-  AS P → (∀ x, AS (Ψ x)) → AS (default P mx Ψ).
-Proof. destruct mx; apply _. Qed.
-
-(* Derived lemmas for always stable *)
-Lemma always_always P `{!AlwaysStable P} : (□ P)%I ≡ P.
-Proof. apply (anti_symm (⊑)); auto using always_elim. Qed.
-Lemma always_intro P Q `{!AlwaysStable P} : P ⊑ Q → P ⊑ □ Q.
-Proof. rewrite -(always_always P); apply always_intro'. Qed.
-Lemma always_entails P Q `{!AlwaysStable P} : P ⊑ □ Q → P ⊑ Q.
-Proof. rewrite -(always_always P). move=>->. by rewrite always_elim. Qed.
-Lemma always_and_sep_l P Q `{!AlwaysStable P} : (P ∧ Q)%I ≡ (P ★ Q)%I.
-Proof. by rewrite -(always_always P) always_and_sep_l'. Qed.
-Lemma always_and_sep_r P Q `{!AlwaysStable Q} : (P ∧ Q)%I ≡ (P ★ Q)%I.
-Proof. by rewrite -(always_always Q) always_and_sep_r'. Qed.
-Lemma always_sep_dup P `{!AlwaysStable P} : P ≡ (P ★ P)%I.
-Proof. by rewrite -(always_always P) -always_sep_dup'. Qed.
-Lemma always_entails_l P Q `{!AlwaysStable Q} : (P ⊑ Q) → P ⊑ (Q ★ P).
-Proof. by rewrite -(always_always Q); apply always_entails_l'. Qed.
-Lemma always_entails_r P Q `{!AlwaysStable Q} : (P ⊑ Q) → P ⊑ (P ★ Q).
-Proof. by rewrite -(always_always Q); apply always_entails_r'. Qed.
-
-(* Derived lemmas that need a combination of the above *)
-Lemma löb_strong_sep P Q : (▷(P -★ Q) ★ P) ⊑ Q → P ⊑ Q.
-Proof.
-  move/wand_intro_r=>Hlöb. rewrite -[P](left_id True (∧))%I.
-  apply impl_elim_l'. apply: always_entails. apply löb_strong.
-  rewrite left_id -always_wand_impl -always_later Hlöb. done.
-Qed.
-
-End uPred_logic.
-
-(* Hint DB for the logic *)
-Hint Resolve const_intro.
-Hint Resolve or_elim or_intro_l' or_intro_r' : I.
-Hint Resolve and_intro and_elim_l' and_elim_r' : I.
-Hint Resolve always_mono : I.
-Hint Resolve sep_elim_l' sep_elim_r' sep_mono : I.
-Hint Immediate True_intro False_elim : I.
-Hint Immediate iff_refl eq_refl : I.
-End uPred.

algebra/upred_big_op.v

-From algebra Require Export upred.
-From prelude Require Import gmap fin_collections.
-Import uPred.
-
-(** * Big ops over lists *)
-(* These are the basic building blocks for other big ops *)
-Fixpoint uPred_big_and {M} (Ps : list (uPred M)) : uPred M:=
-  match Ps with [] => True | P :: Ps => P ∧ uPred_big_and Ps end%I.
-Instance: Params (@uPred_big_and) 1.
-Notation "'Π∧' Ps" := (uPred_big_and Ps) (at level 20) : uPred_scope.
-Fixpoint uPred_big_sep {M} (Ps : list (uPred M)) : uPred M :=
-  match Ps with [] => True | P :: Ps => P ★ uPred_big_sep Ps end%I.
-Instance: Params (@uPred_big_sep) 1.
-Notation "'Π★' Ps" := (uPred_big_sep Ps) (at level 20) : uPred_scope.
-
-(** * Other big ops *)
-(** We use a type class to obtain overloaded notations *)
-Definition uPred_big_sepM {M} `{Countable K} {A}
-    (m : gmap K A) (Φ : K → A → uPred M) : uPred M :=
-  uPred_big_sep (curry Φ <$> map_to_list m).
-Instance: Params (@uPred_big_sepM) 6.
-Notation "'Π★{map' m } Φ" := (uPred_big_sepM m Φ)
-  (at level 20, m at level 10, format "Π★{map  m }  Φ") : uPred_scope.
-
-Definition uPred_big_sepS {M} `{Countable A}
-  (X : gset A) (Φ : A → uPred M) : uPred M := uPred_big_sep (Φ <$> elements X).
-Instance: Params (@uPred_big_sepS) 5.
-Notation "'Π★{set' X } Φ" := (uPred_big_sepS X Φ)
-  (at level 20, X at level 10, format "Π★{set  X }  Φ") : uPred_scope.
-
-(** * Always stability for lists *)
-Class AlwaysStableL {M} (Ps : list (uPred M)) :=
-  always_stableL : Forall AlwaysStable Ps.
-Arguments always_stableL {_} _ {_}.
-
-Section big_op.
-Context {M : cmraT}.
-Implicit Types Ps Qs : list (uPred M).
-Implicit Types A : Type.
-
-(* Big ops *)
-Global Instance big_and_proper : Proper ((≡) ==> (≡)) (@uPred_big_and M).
-Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed.
-Global Instance big_sep_proper : Proper ((≡) ==> (≡)) (@uPred_big_sep M).
-Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed.
-
-Global Instance big_and_ne n :
-  Proper (Forall2 (dist n) ==> dist n) (@uPred_big_and M).
-Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed.
-Global Instance big_sep_ne n :
-  Proper (Forall2 (dist n) ==> dist n) (@uPred_big_sep M).
-Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed.
-
-Global Instance big_and_mono' : Proper (Forall2 (⊑) ==> (⊑)) (@uPred_big_and M).
-Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed.
-Global Instance big_sep_mono' : Proper (Forall2 (⊑) ==> (⊑)) (@uPred_big_sep M).
-Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed.
-
-Global Instance big_and_perm : Proper ((≡ₚ) ==> (≡)) (@uPred_big_and M).
-Proof.
-  induction 1 as [|P Ps Qs ? IH|P Q Ps|]; simpl; auto.
-  - by rewrite IH.
-  - by rewrite !assoc (comm _ P).
-  - etransitivity; eauto.
-Qed.
-Global Instance big_sep_perm : Proper ((≡ₚ) ==> (≡)) (@uPred_big_sep M).
-Proof.
-  induction 1 as [|P Ps Qs ? IH|P Q Ps|]; simpl; auto.
-  - by rewrite IH.
-  - by rewrite !assoc (comm _ P).
-  - etransitivity; eauto.
-Qed.
-
-Lemma big_and_app Ps Qs : (Π∧ (Ps ++ Qs))%I ≡ (Π∧ Ps ∧ Π∧ Qs)%I.
-Proof. by induction Ps as [|?? IH]; rewrite /= ?left_id -?assoc ?IH. Qed.
-Lemma big_sep_app Ps Qs : (Π★ (Ps ++ Qs))%I ≡ (Π★ Ps ★ Π★ Qs)%I.
-Proof. by induction Ps as [|?? IH]; rewrite /= ?left_id -?assoc ?IH. Qed.
-
-Lemma big_and_contains Ps Qs : Qs `contains` Ps → (Π∧ Ps)%I ⊑ (Π∧ Qs)%I.
-Proof.
-  intros [Ps' ->]%contains_Permutation. by rewrite big_and_app and_elim_l.
-Qed.
-Lemma big_sep_contains Ps Qs : Qs `contains` Ps → (Π★ Ps)%I ⊑ (Π★ Qs)%I.
-Proof.
-  intros [Ps' ->]%contains_Permutation. by rewrite big_sep_app sep_elim_l.
-Qed.
-
-Lemma big_sep_and Ps : (Π★ Ps) ⊑ (Π∧ Ps).
-Proof. by induction Ps as [|P Ps IH]; simpl; auto with I. Qed.
-
-Lemma big_and_elem_of Ps P : P ∈ Ps → (Π∧ Ps) ⊑ P.
-Proof. induction 1; simpl; auto with I. Qed.
-Lemma big_sep_elem_of Ps P : P ∈ Ps → (Π★ Ps) ⊑ P.
-Proof. induction 1; simpl; auto with I. Qed.
-
-(* Big ops over finite maps *)
-Section gmap.
-  Context `{Countable K} {A : Type}.
-  Implicit Types m : gmap K A.
-  Implicit Types Φ Ψ : K → A → uPred M.
-
-  Lemma big_sepM_mono Φ Ψ m1 m2 :
-    m2 ⊆ m1 → (∀ x k, m2 !! k = Some x → Φ k x ⊑ Ψ k x) →
-    (Π★{map m1} Φ) ⊑ (Π★{map m2} Ψ).
-  Proof.
-    intros HX HΦ. transitivity (Π★{map m2} Φ)%I.
-    - by apply big_sep_contains, fmap_contains, map_to_list_contains.
-    - apply big_sep_mono', Forall2_fmap, Forall2_Forall.
-      apply Forall_forall=> -[i x] ? /=. by apply HΦ, elem_of_map_to_list.
-  Qed.
-
-  Global Instance big_sepM_ne m n :
-    Proper (pointwise_relation _ (pointwise_relation _ (dist n)) ==> (dist n))
-           (uPred_big_sepM (M:=M) m).
-  Proof.
-    intros Φ1 Φ2 HΦ. apply big_sep_ne, Forall2_fmap.
-    apply Forall2_Forall, Forall_true=> -[i x]; apply HΦ.
-  Qed.
-  Global Instance big_sepM_proper m :
-    Proper (pointwise_relation _ (pointwise_relation _ (≡)) ==> (≡))
-           (uPred_big_sepM (M:=M) m).
-  Proof.
-    intros Φ1 Φ2 HΦ; apply equiv_dist=> n.
-    apply big_sepM_ne=> k x; apply equiv_dist, HΦ.
-  Qed.
-  Global Instance big_sepM_mono' m :
-    Proper (pointwise_relation _ (pointwise_relation _ (⊑)) ==> (⊑))
-           (uPred_big_sepM (M:=M) m).
-  Proof. intros Φ1 Φ2 HΦ. apply big_sepM_mono; intros; [done|apply HΦ]. Qed.
-
-  Lemma big_sepM_empty Φ : (Π★{map ∅} Φ)%I ≡ True%I.
-  Proof. by rewrite /uPred_big_sepM map_to_list_empty. Qed.
-  Lemma big_sepM_insert Φ (m : gmap K A) i x :
-    m !! i = None → (Π★{map <[i:=x]> m} Φ)%I ≡ (Φ i x ★ Π★{map m} Φ)%I.
-  Proof. intros ?; by rewrite /uPred_big_sepM map_to_list_insert. Qed.
-  Lemma big_sepM_singleton Φ i x : (Π★{map {[i := x]}} Φ)%I ≡ (Φ i x)%I.
-  Proof.
-    rewrite -insert_empty big_sepM_insert/=; last auto using lookup_empty.
-    by rewrite big_sepM_empty right_id.
-  Qed.
-
-  Lemma big_sepM_sepM Φ Ψ m :
-    (Π★{map m} (λ i x, Φ i x ★ Ψ i x))%I ≡ (Π★{map m} Φ ★ Π★{map m} Ψ)%I.
-  Proof.
-    rewrite /uPred_big_sepM.
-    induction (map_to_list m) as [|[i x] l IH]; csimpl; rewrite ?right_id //.
-    by rewrite IH -!assoc (assoc _ (Ψ _ _)) [(Ψ _ _ ★ _)%I]comm -!assoc.
-  Qed.
-  Lemma big_sepM_later Φ m : (▷ Π★{map m} Φ)%I ≡ (Π★{map m} (λ i x, ▷ Φ i x))%I.
-  Proof.
-    rewrite /uPred_big_sepM.
-    induction (map_to_list m) as [|[i x] l IH]; csimpl; rewrite ?later_True //.
-    by rewrite later_sep IH.
-  Qed.
-End gmap.
-
-(* Big ops over finite sets *)
-Section gset.
-  Context `{Countable A}.
-  Implicit Types X : gset A.
-  Implicit Types Φ : A → uPred M.
-
-  Lemma big_sepS_mono Φ Ψ X Y :
-    Y ⊆ X → (∀ x, x ∈ Y → Φ x ⊑ Ψ x) → (Π★{set X} Φ) ⊑ (Π★{set Y} Ψ).
-  Proof.
-    intros HX HΦ. transitivity (Π★{set Y} Φ)%I.
-    - by apply big_sep_contains, fmap_contains, elements_contains.
-    - apply big_sep_mono', Forall2_fmap, Forall2_Forall.
-      apply Forall_forall=> x ? /=. by apply HΦ, elem_of_elements.
-  Qed.
-
-  Lemma big_sepS_ne X n :
-    Proper (pointwise_relation _ (dist n) ==> dist n) (uPred_big_sepS (M:=M) X).
-  Proof.
-    intros Φ1 Φ2 HΦ. apply big_sep_ne, Forall2_fmap.
-    apply Forall2_Forall, Forall_true=> x; apply HΦ.
-  Qed.
-  Lemma big_sepS_proper X :
-    Proper (pointwise_relation _ (≡) ==> (≡)) (uPred_big_sepS (M:=M) X).
-  Proof.
-    intros Φ1 Φ2 HΦ; apply equiv_dist=> n.
-    apply big_sepS_ne=> x; apply equiv_dist, HΦ.
-  Qed.
-  Lemma big_sepS_mono' X :
-    Proper (pointwise_relation _ (⊑) ==> (⊑)) (uPred_big_sepS (M:=M) X).
-  Proof. intros Φ1 Φ2 HΦ. apply big_sepS_mono; naive_solver. Qed.
-
-  Lemma big_sepS_empty Φ : (Π★{set ∅} Φ)%I ≡ True%I.
-  Proof. by rewrite /uPred_big_sepS elements_empty. Qed.
-  Lemma big_sepS_insert Φ X x :
-    x ∉ X → (Π★{set {[ x ]} ∪ X} Φ)%I ≡ (Φ x ★ Π★{set X} Φ)%I.
-  Proof. intros. by rewrite /uPred_big_sepS elements_union_singleton. Qed.
-  Lemma big_sepS_delete Φ X x :
-    x ∈ X → (Π★{set X} Φ)%I ≡ (Φ x ★ Π★{set X ∖ {[ x ]}} Φ)%I.
-  Proof.
-    intros. rewrite -big_sepS_insert; last set_solver.
-    by rewrite -union_difference_L; last set_solver.
-  Qed.
-  Lemma big_sepS_singleton Φ x : (Π★{set {[ x ]}} Φ)%I ≡ (Φ x)%I.
-  Proof. intros. by rewrite /uPred_big_sepS elements_singleton /= right_id. Qed.
-
-  Lemma big_sepS_sepS Φ Ψ X :
-    (Π★{set X} (λ x, Φ x ★ Ψ x))%I ≡ (Π★{set X} Φ ★ Π★{set X} Ψ)%I.
-  Proof.
-    rewrite /uPred_big_sepS.
-    induction (elements X) as [|x l IH]; csimpl; first by rewrite ?right_id.
-    by rewrite IH -!assoc (assoc _ (Ψ _)) [(Ψ _ ★ _)%I]comm -!assoc.
-  Qed.
-
-  Lemma big_sepS_later Φ X : (▷ Π★{set X} Φ)%I ≡ (Π★{set X} (λ x, ▷ Φ x))%I.
-  Proof.
-    rewrite /uPred_big_sepS.
-    induction (elements X) as [|x l IH]; csimpl; first by rewrite ?later_True.
-    by rewrite later_sep IH.
-  Qed.
-End gset.
-
-(* Always stable *)
-Local Notation AS := AlwaysStable.
-Local Notation ASL := AlwaysStableL.
-Global Instance big_and_always_stable Ps : ASL Ps → AS (Π∧ Ps).
-Proof. induction 1; apply _. Qed.
-Global Instance big_sep_always_stable Ps : ASL Ps → AS (Π★ Ps).
-Proof. induction 1; apply _. Qed.
-
-Global Instance nil_always_stable : ASL (@nil (uPred M)).
-Proof. constructor. Qed.
-Global Instance cons_always_stable P Ps : AS P → ASL Ps → ASL (P :: Ps).
-Proof. by constructor. Qed.
-Global Instance app_always_stable Ps Ps' : ASL Ps → ASL Ps' → ASL (Ps ++ Ps').
-Proof. apply Forall_app_2. Qed.
-Global Instance zip_with_always_stable {A B} (f : A → B → uPred M) xs ys :
-  (∀ x y, AS (f x y)) → ASL (zip_with f xs ys).
-Proof. unfold ASL=> ?; revert ys; induction xs=> -[|??]; constructor; auto. Qed.
-End big_op.

barrier/barrier.v

-From algebra Require Export upred_big_op.
-From program_logic Require Export sts saved_prop.
-From program_logic Require Import hoare.
-From heap_lang Require Export derived heap wp_tactics notation.
-Import uPred.
-
-Definition newchan := (λ: "", ref '0)%L.
-Definition signal := (λ: "x", "x" <- '1)%L.
-Definition wait := (rec: "wait" "x" :=if: !"x" = '1 then '() else "wait" "x")%L.
-
-(** The STS describing the main barrier protocol. Every state has an index-set
-    associated with it. These indices are actually [gname], because we use them
-    with saved propositions. *)
-Module barrier_proto.
-  Inductive phase := Low | High.
-  Record stateT := State { state_phase : phase; state_I : gset gname }.
-  Inductive token := Change (i : gname) | Send.
-
-  Global Instance stateT_inhabited: Inhabited stateT.
-  Proof. split. exact (State Low ∅). Qed.
-
-  Definition change_tokens (I : gset gname) : set token :=
-    mkSet (λ t, match t with Change i => i ∉ I | Send => False end).
-
-  Inductive trans : relation stateT :=
-  | ChangeI p I2 I1 : trans (State p I1) (State p I2)
-  | ChangePhase I : trans (State Low I) (State High I).
-
-  Definition tok (s : stateT) : set token :=
-      change_tokens (state_I s)
-    ∪ match state_phase s with Low => ∅ | High => {[ Send ]} end.
-
-  Canonical Structure sts := sts.STS trans tok.
-
-  (* The set of states containing some particular i *)
-  Definition i_states (i : gname) : set stateT :=
-    mkSet (λ s, i ∈ state_I s).
-
-  Lemma i_states_closed i :
-    sts.closed (i_states i) {[ Change i ]}.
-  Proof.
-    split.
-    - apply (non_empty_inhabited(State Low {[ i ]})). rewrite !mkSet_elem_of /=.
-      apply lookup_singleton.
-    - move=>[p I]. rewrite /= /tok !mkSet_elem_of /= =>HI.
-      move=>s' /elem_of_intersection. rewrite !mkSet_elem_of /=.
-      move=>[[Htok|Htok] ? ]; subst s'; first done.
-      destruct p; done.
-    - (* If we do the destruct of the states early, and then inversion
-         on the proof of a transition, it doesn't work - we do not obtain
-         the equalities we need. So we destruct the states late, because this
-         means we can use "destruct" instead of "inversion". *)
-      move=>s1 s2. rewrite !mkSet_elem_of /==> Hs1 Hstep.
-      (* We probably want some helper lemmas for this... *)
-      inversion_clear Hstep as [T1 T2 Hdisj Hstep'].
-      inversion_clear Hstep' as [? ? ? ? Htrans _ _ Htok].
-      destruct Htrans; last done; move:Hs1 Hdisj Htok.
-      rewrite /= /tok /=.
-      intros. apply dec_stable. 
-      assert (Change i ∉ change_tokens I1) as HI1
-        by (rewrite mkSet_not_elem_of; set_solver +Hs1).
-      assert (Change i ∉ change_tokens I2) as HI2.
-      { destruct p.
-        - set_solver +Htok Hdisj HI1.
-        - set_solver +Htok Hdisj HI1 / discriminate. }
-      done.
-  Qed.
-
-  (* The set of low states *)
-  Definition low_states : set stateT :=
-    mkSet (λ s, if state_phase s is Low then True else False).
-
-  Lemma low_states_closed : sts.closed low_states {[ Send ]}.
-  Proof.
-    split.
-    - apply (non_empty_inhabited(State Low ∅)). by rewrite !mkSet_elem_of /=.
-    - move=>[p I]. rewrite /= /tok !mkSet_elem_of /= =>HI.
-      destruct p; last done. set_solver.
-    - move=>s1 s2. rewrite !mkSet_elem_of /==> Hs1 Hstep.
-      inversion_clear Hstep as [T1 T2 Hdisj Hstep'].
-      inversion_clear Hstep' as [? ? ? ? Htrans _ _ Htok].
-      destruct Htrans; move:Hs1 Hdisj Htok =>/=;
-                                first by destruct p.
-      rewrite /= /tok /=. intros. set_solver +Hdisj Htok.
-  Qed.
-
-End barrier_proto.
-(* I am too lazy to type the full module name all the time. But then
-   why did we even put this into a module? Because some of the names 
-   are so general.
-   What we'd really like here is to import *some* of the names from
-   the module into our namespaces. But Coq doesn't seem to support that...?? *)
-Import barrier_proto.
-
-(** Now we come to the Iris part of the proof. *)
-Section proof.
-  Context {Σ : iFunctorG} (N : namespace).
-  Context `{heapG Σ} (heapN : namespace).
-  Context `{stsG heap_lang Σ sts}.
-  Context `{savedPropG heap_lang Σ}.
-
-  Local Hint Immediate i_states_closed low_states_closed.
-
-  Local Notation iProp := (iPropG heap_lang Σ).
-
-  Definition waiting (P : iProp) (I : gset gname) : iProp :=
-    (∃ Ψ : gname → iProp, ▷(P -★ Π★{set I} (λ i, Ψ i)) ★
-                             Π★{set I} (λ i, saved_prop_own i (Ψ i)))%I.
-
-  Definition ress (I : gset gname) : iProp :=
-    (Π★{set I} (λ i, ∃ R, saved_prop_own i R ★ ▷R))%I.
-
-  Local Notation state_to_val s :=
-    (match s with State Low _ => 0 | State High _ => 1 end).
-  Definition barrier_inv (l : loc) (P : iProp) (s : stateT) : iProp :=
-    (l ↦ '(state_to_val s) ★
-     match s with State Low I' => waiting P I' | State High I' => ress I' end
-    )%I.
-
-  Definition barrier_ctx (γ : gname) (l : loc) (P : iProp) : iProp :=
-    (heap_ctx heapN ★ sts_ctx γ N (barrier_inv l P))%I.
-
-  Global Instance barrier_ctx_ne n γ l : Proper (dist n ==> dist n) (barrier_ctx γ l).
-  Proof.
-    move=>? ? EQ. rewrite /barrier_ctx. apply sep_ne; first done. apply sts_ctx_ne.
-    move=>[p I]. rewrite /barrier_inv. destruct p; last done.
-    rewrite /waiting. by setoid_rewrite EQ.
-  Qed.
-
-  Definition send (l : loc) (P : iProp) : iProp :=
-    (∃ γ, barrier_ctx γ l P ★ sts_ownS γ low_states {[ Send ]})%I.
-
-  Global Instance send_ne n l : Proper (dist n ==> dist n) (send l).
-  Proof. (* TODO: This really ought to be doable by an automatic tactic. it is just application of already regostered congruence lemmas. *)
-    move=>? ? EQ. rewrite /send. apply exist_ne=>γ. by rewrite EQ.
-  Qed.
-
-  Definition recv (l : loc) (R : iProp) : iProp :=
-    (∃ γ P Q i, barrier_ctx γ l P ★ sts_ownS γ (i_states i) {[ Change i ]} ★
-        saved_prop_own i Q ★ ▷(Q -★ R))%I.
-
-  Global Instance recv_ne n l : Proper (dist n ==> dist n) (recv l).
-  Proof.
-    move=>? ? EQ. rewrite /send. do 4 apply exist_ne=>?. by rewrite EQ.
-  Qed.
-
-  Lemma newchan_spec (P : iProp) (Φ : val → iProp) :
-    (heap_ctx heapN ★ ∀ l, recv l P ★ send l P -★ Φ (LocV l))
-    ⊑ || newchan '() {{ Φ }}.
-  Proof.
-    rewrite /newchan. wp_rec. (* TODO: wp_seq. *)
-    rewrite -wp_pvs. wp> eapply wp_alloc; eauto with I ndisj.
-    apply forall_intro=>l. rewrite (forall_elim l). apply wand_intro_l.
-    rewrite !assoc. apply pvs_wand_r.
-    (* The core of this proof: Allocating the STS and the saved prop. *)
-    eapply sep_elim_True_r.
-    { by eapply (saved_prop_alloc _ P). }
-    rewrite pvs_frame_l. apply pvs_strip_pvs. rewrite sep_exist_l.
-    apply exist_elim=>i.
-    transitivity (pvs ⊤ ⊤ (heap_ctx heapN ★ ▷ (barrier_inv l P (State Low {[ i ]}))  ★ saved_prop_own i P)).
-    - rewrite -pvs_intro. rewrite [(_ ★ heap_ctx _)%I]comm -!assoc. apply sep_mono_r.
-      rewrite {1}[saved_prop_own _ _]always_sep_dup !assoc. apply sep_mono_l.
-      rewrite /barrier_inv /waiting -later_intro. apply sep_mono_r.
-      rewrite -(exist_intro (const P)) /=. rewrite -[saved_prop_own _ _](left_id True%I (★)%I).
-      apply sep_mono.
-      + rewrite -later_intro. apply wand_intro_l. rewrite right_id.
-        by rewrite big_sepS_singleton.
-      + by rewrite big_sepS_singleton.
-    - rewrite (sts_alloc (barrier_inv l P) ⊤ N); last by eauto.
-      rewrite !pvs_frame_r !pvs_frame_l. 
-      rewrite pvs_trans'. apply pvs_strip_pvs. rewrite sep_exist_r sep_exist_l.
-      apply exist_elim=>γ.
-      (* TODO: The record notation is rather annoying here *)
-      rewrite /recv /send. rewrite -(exist_intro γ) -(exist_intro P).
-      rewrite -(exist_intro P) -(exist_intro i) -(exist_intro γ).
-      (* This is even more annoying than usually, since rewrite sometimes unfolds stuff... *)
-      rewrite [barrier_ctx _ _ _]lock !assoc [(_ ★locked _)%I]comm !assoc -lock.
-      rewrite -always_sep_dup.
-      rewrite [barrier_ctx _ _ _]lock always_and_sep_l -!assoc assoc -lock.
-      rewrite -pvs_frame_l. apply sep_mono_r.
-      rewrite [(saved_prop_own _ _ ★ _)%I]comm !assoc. rewrite -pvs_frame_r.
-      apply sep_mono_l.
-      rewrite -assoc [(▷ _ ★ _)%I]comm assoc -pvs_frame_r.
-      eapply sep_elim_True_r; last eapply sep_mono_l.
-      { rewrite -later_intro. apply wand_intro_l. by rewrite right_id. }
-      rewrite (sts_own_weaken ⊤ _ _ (i_states i ∩ low_states) _ 
-                              ({[ Change i ]} ∪ {[ Send ]})).
-      + apply pvs_mono. rewrite sts_ownS_op; eauto; []. set_solver.
-      + rewrite /= /tok /=. apply elem_of_equiv=>t.
-        rewrite elem_of_difference elem_of_union.
-        rewrite !mkSet_elem_of /change_tokens.
-        (* TODO: destruct t; set_solver does not work. What is the best way to do on? *)
-        destruct t as [i'|]; last by naive_solver. split.
-        * move=>[_ Hn]. left. destruct (decide (i = i')); first by subst i.
-          exfalso. apply Hn. left. set_solver.
-        * move=>[[EQ]|?]; last discriminate. set_solver. 
-      + apply elem_of_intersection. rewrite !mkSet_elem_of /=. set_solver.
-      + apply sts.closed_op; eauto; first set_solver; [].
-        apply (non_empty_inhabited (State Low {[ i ]})).
-        apply elem_of_intersection.
-        rewrite !mkSet_elem_of /=. set_solver.
-  Qed.
-
-  Lemma signal_spec l P (Φ : val → iProp) :
-    heapN ⊥ N → (send l P ★ P ★ Φ '()) ⊑ || signal (LocV l) {{ Φ }}.
-  Proof.
-    intros Hdisj. rewrite /signal /send /barrier_ctx. rewrite sep_exist_r.
-    apply exist_elim=>γ. wp_rec. (* FIXME wp_let *)
-    (* I think some evars here are better than repeating *everything* *)
-    eapply (sts_fsaS _ (wp_fsa _)) with (N0:=N) (γ0:=γ); simpl;
-      eauto with I ndisj.
-    rewrite [(_ ★ sts_ownS _ _ _)%I]comm -!assoc /wp_fsa. apply sep_mono_r.
-    apply forall_intro=>-[p I]. apply wand_intro_l. rewrite -!assoc.
-    apply const_elim_sep_l=>Hs. destruct p; last done.
-    rewrite {1}/barrier_inv =>/={Hs}. rewrite later_sep.
-    eapply wp_store; eauto with I ndisj.
-    rewrite -!assoc. apply sep_mono_r. etransitivity; last eapply later_mono.
-    { (* Is this really the best way to strip the later? *)
-      erewrite later_sep. apply sep_mono_r. apply later_intro. }
-    apply wand_intro_l. rewrite -(exist_intro (State High I)).
-    rewrite -(exist_intro ∅). rewrite const_equiv /=; last first.
-    { constructor; first constructor; rewrite /= /tok /=; set_solver. }
-    rewrite left_id -later_intro {2}/barrier_inv -!assoc. apply sep_mono_r.
-    rewrite !assoc [(_ ★ P)%I]comm !assoc -2!assoc.
-    apply sep_mono; last first.
-    { apply wand_intro_l. eauto with I. }
-    (* Now we come to the core of the proof: Updating from waiting to ress. *)
-    rewrite /waiting /ress sep_exist_l. apply exist_elim=>{Φ} Φ.
-    rewrite later_wand {1}(later_intro P) !assoc wand_elim_r.
-    rewrite big_sepS_later -big_sepS_sepS. apply big_sepS_mono'=>i.
-    rewrite -(exist_intro (Φ i)) comm. done.
-  Qed.
-
-  Lemma wait_spec l P (Φ : val → iProp) :
-    heapN ⊥ N → (recv l P ★ (P -★ Φ '())) ⊑ || wait (LocV l) {{ Φ }}.
-  Proof.
-    rename P into R.
-    intros Hdisj. rewrite /wait. apply löb_strong_sep.
-    rewrite {1}/recv /barrier_ctx. rewrite !sep_exist_r.
-    apply exist_elim=>γ. rewrite !sep_exist_r. apply exist_elim=>P.
-    rewrite !sep_exist_r. apply exist_elim=>Q. rewrite !sep_exist_r.
-    apply exist_elim=>i. wp_rec.
-    (* TODO use automatic binding *)
-    apply (wp_bindi (IfCtx _ _)).
-    (* I think some evars here are better than repeating *everything* *)
-    eapply (sts_fsaS _ (wp_fsa _)) with (N0:=N) (γ0:=γ); simpl;
-      eauto with I ndisj.
-    rewrite [(_ ★ sts_ownS _ _ _)%I]comm -!assoc /wp_fsa. apply sep_mono_r.
-    apply forall_intro=>-[p I]. apply wand_intro_l. rewrite -!assoc.
-    apply const_elim_sep_l=>Hs. destruct p; last done.
-    rewrite {1}/barrier_inv =>/={Hs}. rewrite later_sep.
-    eapply wp_store; eauto with I ndisj.
-    rewrite -!assoc. apply sep_mono_r. etransitivity; last eapply later_mono.
-    { (* Is this really the best way to strip the later? *)
-      erewrite later_sep. apply sep_mono_r. apply later_intro. }
-    apply wand_intro_l. rewrite -(exist_intro (State High I)).
-  Abort.
-
-  Lemma recv_split l P1 P2 Φ :
-    (recv l (P1 ★ P2) ★ (recv l P1 ★ recv l P2 -★ Φ '())) ⊑ || Skip {{ Φ }}.
-  Proof.
-  Abort.
-
-  Lemma recv_strengthen l P1 P2 :
-    (P1 -★ P2) ⊑ (recv l P1 -★ recv l P2).
-  Proof.
-    apply wand_intro_l. rewrite /recv. rewrite sep_exist_r. apply exist_mono=>γ.
-    rewrite sep_exist_r. apply exist_mono=>P. rewrite sep_exist_r.
-    apply exist_mono=>Q. rewrite sep_exist_r. apply exist_mono=>i.
-    rewrite -!assoc. apply sep_mono_r, sep_mono_r, sep_mono_r, sep_mono_r.
-    rewrite (later_intro (P1 -★ _)%I) -later_sep. apply later_mono.
-    apply wand_intro_l. rewrite !assoc wand_elim_r wand_elim_r. done.
-  Qed.
-
-End proof.
-
-Section spec.
-  Context {Σ : iFunctorG}.
-  Context `{heapG Σ}.
-  Context `{stsG heap_lang Σ barrier_proto.sts}.
-  Context `{savedPropG heap_lang Σ}.
-
-  Local Notation iProp := (iPropG heap_lang Σ).
-
-  (* TODO: Maybe notation for LocV (and Loc)? *)
-  Lemma barrier_spec (heapN N : namespace) :
-    heapN ⊥ N →
-    ∃ (recv send : loc -> iProp -n> iProp),
-      (∀ P, heap_ctx heapN ⊑ ({{ True }} newchan '() {{ λ v, ∃ l, v = LocV l ★ recv l P ★ send l P }})) ∧
-      (∀ l P, {{ send l P ★ P }} signal (LocV l) {{ λ _, True }}) ∧
-      (∀ l P, {{ recv l P }} wait (LocV l) {{ λ _, P }}) ∧
-      (∀ l P Q, {{ recv l (P ★ Q) }} Skip {{ λ _, recv l P ★ recv l Q }}) ∧
-      (∀ l P Q, (P -★ Q) ⊑ (recv l P -★ recv l Q)).
-  Proof.
-    intros HN. exists (λ l, CofeMor (recv N heapN l)). exists (λ l, CofeMor (send N heapN l)).
-    split_and?; cbn.
-    - intros. apply: always_intro. apply impl_intro_l. rewrite -newchan_spec.
-      rewrite comm always_and_sep_r. apply sep_mono_r. apply forall_intro=>l.
-      apply wand_intro_l. rewrite right_id -(exist_intro l) const_equiv // left_id.
-      done.
-    - intros. apply ht_alt. rewrite -signal_spec; first by rewrite right_id. done.
-    - admit.
-    - admit.
-    - intros. apply recv_strengthen.
-  Abort.
-
-End spec.

coq-iris-deprecated.opam

+opam-version: "2.0"
+maintainer: "Ralf Jung <jung@mpi-sws.org>"
+authors: "The Iris Team"
+license: "BSD-3-Clause"
+homepage: "https://iris-project.org/"
+bug-reports: "https://gitlab.mpi-sws.org/iris/iris/issues"
+dev-repo: "git+https://gitlab.mpi-sws.org/iris/iris.git"
+version: "dev"
+
+synopsis: "Deprecated Iris libraries"
+description: """
+This package contains libraries that have been deprecated from Iris, and are planned to be
+entirely removed at some point.
+"""
+
+depends: [
+  "coq-iris" {= version}
+]
+
+build: ["./make-package" "iris_deprecated" "-j%{jobs}%"]
+install: ["./make-package" "iris_deprecated" "install"]

coq-iris-heap-lang.opam

+opam-version: "2.0"
+maintainer: "Ralf Jung <jung@mpi-sws.org>"
+authors: "The Iris Team"
+license: "BSD-3-Clause"
+homepage: "https://iris-project.org/"
+bug-reports: "https://gitlab.mpi-sws.org/iris/iris/issues"
+dev-repo: "git+https://gitlab.mpi-sws.org/iris/iris.git"
+version: "dev"
+
+synopsis: "The canonical example language for Iris"
+description: """
+This package defines HeapLang, a concurrent lambda calculus with references, and
+uses Iris to build a program logic for HeapLang programs.
+"""
+tags: [
+  "logpath:iris.heap_lang"
+]
+
+depends: [
+  "coq-iris" {= version}
+]
+
+build: ["./make-package" "iris_heap_lang" "-j%{jobs}%"]
+install: ["./make-package" "iris_heap_lang" "install"]

coq-iris-unstable.opam

+opam-version: "2.0"
+maintainer: "Ralf Jung <jung@mpi-sws.org>"
+authors: "The Iris Team"
+license: "BSD-3-Clause"
+homepage: "https://iris-project.org/"
+bug-reports: "https://gitlab.mpi-sws.org/iris/iris/issues"
+dev-repo: "git+https://gitlab.mpi-sws.org/iris/iris.git"
+version: "dev"
+
+synopsis: "Unfinished Iris libraries"
+description: """
+This package contains libraries that have been proposed for inclusion in Iris, but more
+work is needed before they are ready for this.
+"""
+
+depends: [
+  "coq-iris" {= version}
+  "coq-iris-heap-lang" {= version}
+]
+
+build: ["./make-package" "iris_unstable" "-j%{jobs}%"]
+install: ["./make-package" "iris_unstable" "install"]

coq-iris.opam

+opam-version: "2.0"
+maintainer: "Ralf Jung <jung@mpi-sws.org>"
+authors: "The Iris Team"
+license: "BSD-3-Clause"
+homepage: "https://iris-project.org/"
+bug-reports: "https://gitlab.mpi-sws.org/iris/iris/issues"
+dev-repo: "git+https://gitlab.mpi-sws.org/iris/iris.git"
+version: "dev"
+
+synopsis: "A Higher-Order Concurrent Separation Logic Framework with support for interactive proofs"
+description: """
+Iris is a framework for reasoning about the safety of concurrent programs using
+concurrent separation logic. It can be used to develop a program logic, for
+defining logical relations, and for reasoning about type systems, among other
+applications. This package includes the base logic, Iris Proof Mode (IPM) /
+MoSeL, and a general language-independent program logic; see coq-iris-heap-lang
+for an instantiation of the program logic to a particular programming language.
+"""
+tags: [
+  "logpath:iris.prelude"
+  "logpath:iris.algebra"
+  "logpath:iris.si_logic"
+  "logpath:iris.bi"
+  "logpath:iris.proofmode"
+  "logpath:iris.base_logic"
+  "logpath:iris.program_logic"
+]
+
+depends: [
+  "coq" { (>= "8.19" & < "9.1~") | (= "dev") }
+  "coq-stdpp" { (= "dev.2025-03-30.0.9274984b") | (= "dev") }
+]
+
+build: ["./make-package" "iris" "-j%{jobs}%"]
+install: ["./make-package" "iris" "install"]

coq-lint.sh

+#!/bin/bash
+set -e
+## A simple shell script checking for some common Coq issues.
+
+FILE="$1"
+
+if grep -E -n '^\s*((Existing\s+|Program\s+|Declare\s+)?Instance|Arguments|Remove|Hint\s+(Extern|Constructors|Resolve|Immediate|Mode|Opaque|Transparent|Unfold|Rewrite)|(Open|Close)\s+Scope|Opaque|Transparent|Typeclasses (Opaque|Transparent))\b' "$FILE"; then
+    echo "ERROR: $FILE contains 'Instance'/'Arguments'/'Hint' or another side-effect without locality (see above)."
+    echo "Please add 'Global' or 'Local' as appropriate."
+    echo
+    exit 1
+fi

docs/algebra.tex

-\section{Algebraic Structures}
-
-%%% Local Variables: 
-%%% mode: latex
-%%% TeX-master: "iris"
-%%% End: 

docs/constructions.tex

-% !TEX root = ./appendix.tex
-
-\section{Monoid constructions}
-
-We will use the notation $\mcarp{M} \eqdef |M| \setminus \{\mzero_M\}$ for the carrier of monoid $M$ without zero. When we define a carrier, a zero element is always implicitly added (we do not explicitly give it), and all cases of multiplication that are not defined (including those involving a zero element) go to that element.
-
-To disambiguate which monoid an element is part of, we use the notation $a : M$ to denote an $a$ s.t.\ $a \in |M|$.
-
-When defining a monoid, we will show some \emph{frame-preserving updates} $\melt \mupd \meltsB$ that it supports.
-Remember that
-\[
-	\melt \mupd \meltsB \eqdef \always\All \melt_f. \melt \sep \melt_f \Ra \Exists \meltB \in \meltsB. \meltB \sep \melt_f.
-\]
-The rule \ruleref{FpUpd} (and, later, \ruleref{GhostUpd}) allows us to use such updates in Hoare proofs.
-The following principles generally hold for frame-preserving updates.
-\begin{mathpar}
-	\infer{
-		\melt \mupd \meltsB
-	}{
-		\melt \mupd \meltsB \cup \meltsB'
-	}
-	\and
-	\infer{
-		\melt \mupd \meltsB
-	}{
-		\melt \mtimes \melt_f \mupd \{ \meltB \mtimes \melt_f \mid \meltB \in \meltsB \}
-	}
-\end{mathpar}
-
-Some of our constructions require or preserve \emph{cancellativity}:
-\[
-	\text{$\monoid$ cancellative} \eqdef
-	\All \melt_f, \melt, \meltB \in \mcar{\monoid}. \melt_f \mtimes \melt = \melt_f \mtimes \meltB \neq \mzero \Ra \melt = \meltB
-\]
-
-
-\subsection{Exclusive monoid}
-
-Given a set $X$, we define a monoid such that at most one $x \in X$ can be owned.
-Let $\exm{X}$ be the monoid with carrier $X \uplus \{ \munit \}$ and multiplication
-\[
-\melt \cdot \meltB \;\eqdef\;
-\begin{cases}
-  \melt & \mbox{if } \meltB = \munit \\
-  \meltB & \mbox{if } \melt = \munit
-\end{cases}
-\]
-
-The frame-preserving update
-\begin{mathpar}
-\inferH{ExUpd}
-  {x \in X}
-  {x \mupd \melt}
-\end{mathpar}
-is easily shown, as the only possible frame for $x$ is $\munit$.
-
-Exclusive monoids are cancellative.
-\begin{proof}[Proof of cancellativity]
-If $\melt_f = \munit$, then the statement is trivial.
-If $\melt_f \neq \munit$, then we must have $\melt = \meltB = \munit$, as otherwise one of the two products would be $\mzero$.
-\end{proof}
-
-\subsection{Agreement monoid}
-
-Given a set $X$, we define a monoid such that everybody agrees on which $x \in X$ has been chosen.
-Let $\agm{X}$ be the monoid with carrier $X \uplus \{ \munit \}$ and multiplication
-\[
-\melt \cdot \meltB \;\eqdef\;
-\begin{cases}
-\melt & \mbox{if } \meltB = \munit \lor \melt = \meltB \\
-\meltB & \mbox{if } \melt = \munit
-\end{cases}
-\]
-
-Agreement monoids are cancellative.
-\begin{proof}[Proof of cancellativity]
-	If $\melt_f = \munit$, then the statement is trivial.
-	If $\melt_f \neq \munit$, then if $\melt = \munit$, we must have $\meltB = \munit$ and we are done.
-	Similar so for $\meltB = \munit$.
-	So let $\melt \neq \munit \neq \meltB$ and $\melt_f \mtimes \melt = \melt_f \mtimes \meltB \neq \mzero$.
-	It follows immediately that $\melt = \melt_f = \meltB$.
-\end{proof}
-
-\subsection{Finite Powerset Monoid}
-
-Given an infinite set $X$, we define a monoid $\textmon{PowFin}$ with carrier $\mathcal{P}^{\textrm{fin}}(X)$ as follows:
-\[
-\melt \cdot \meltB \;\eqdef\; \melt \cup \meltB \quad \mbox{if } \melt \cap \meltB = \emptyset
-\]
-
-We obtain:
-\begin{mathpar}
-	\inferH{PowFinUpd}{}
-		{\emptyset \mupd \{ \{x\} \mid x \in X  \}}
-\end{mathpar}
-
-\begin{proof}[Proof of \ruleref{PowFinUpd}]
-	Assume some frame $\melt_f \sep \emptyset$. Since $\melt_f$ is finite and $X$ is infinite, there exists an $x \notin \melt_f$.
-	Pick that for the result.
-\end{proof}
-
-The powerset monoids is cancellative.
-\begin{proof}[Proof of cancellativity]
-	Let $\melt_f \mtimes \melt = \melt_f \mtimes \meltB \neq \mzero$.
-	So we have $\melt_f \sep \melt$ and $\melt_f \sep \meltB$, and we have to show $\melt = \meltB$.
-	Assume $x \in \melt$. Hence $x \in \melt_f \mtimes \melt$ and thus $x \in \melt_f \mtimes \meltB$.
-	By disjointness, $x \notin \melt_f$ and hence $x \in meltB$.
-	The other direction works the same way.
-\end{proof}
-
-\subsection{Product monoid}
-\label{sec:prodm}
-
-Given a family $(M_i)_{i \in I}$ of monoids ($I$ countable), we construct a product monoid.
-Let $\prod_{i \in I} M_i$ be the monoid with carrier $\prod_{i \in I} \mcarp{M_i}$ and point-wise multiplication, non-zero when \emph{all} individual multiplications are non-zero.
-For $f \in \prod_{i \in I} \mcarp{M_i}$, we write $f[i \mapsto a]$ for the disjoint union $f \uplus [i \mapsto a]$.
-
-Frame-preserving updates on the $M_i$ lift to the product:
-\begin{mathpar}
-  \inferH{ProdUpd}
-  {a \mupd_{M_i} B}
-  {f[i \mapsto a] \mupd \{ f[i \mapsto b] \mid b \in B\}}
-\end{mathpar}
-\begin{proof}[Proof of \ruleref{ProdUpd}]
-Assume some frame $g$ and let $c \eqdef g(i)$.
-Since $f[i \mapsto a] \sep g$, we get $f \sep g$ and $a \sep_{M_i} c$.
-Thus there exists $b \in B$ such that $b \sep_{M_i} c$.
-It suffices to show $f[i \mapsto b] \sep g$.
-Since multiplication is defined pointwise, this is the case if all components are compatible.
-For $i$, we know this from $b \sep_{M_i} c$.
-For all the other components, from $f \sep g$.
-\end{proof}
-
-If every $M_i$ is cancellative, then so is $\prod_{i \in I} M_i$.
-\begin{proof}[Proof of cancellativity]
-Let $\melt, \meltB, \melt_f \in \prod_{i \in I} \mcarp{M_i}$, and assume $\melt_f \mtimes \melt = \melt_f \mtimes \meltB \neq \mzero$.
-By the definition of multiplication, this means that for all $i \in I$ we have $\melt_f(i) \mtimes \melt(i) = \melt_f(i) \mtimes \meltB(i) \neq \mzero_{M_i}$.
-As all base monoids are cancellative, we obtain $\forall i \in I.\; \melt(i) = \meltB(i)$ from which we immediately get $\melt = \meltB$.
-\end{proof}
-
-\subsection{Fractional monoid}
-\label{sec:fracm}
-
-Given a monoid $M$, we define a monoid representing fractional ownership of some piece $\melt \in M$.
-The idea is to preserve all the frame-preserving update that $M$ could have, while additionally being able to do \emph{any} update if we own the full state (as determined by the fraction being $1$).
-Let $\fracm{M}$ be the monoid with carrier $(((0, 1] \cap \mathbb{Q}) \times M) \uplus \{\munit\}$ and multiplication
-\begin{align*}
- (q, a) \mtimes (q', a') &\eqdef (q + q', a \mtimes a') \qquad \mbox{if $q+q'\le 1$} \\
- (q, a) \mtimes \munit &\eqdef (q,a) \\
- \munit \mtimes (q,a) &\eqdef (q,a).
-\end{align*}
-
-We get the following frame-preserving update.
-\begin{mathpar}
-	\inferH{FracUpdFull}
-		{a, b \in M}
-		{(1, a) \mupd (1, b)}
-  \and\inferH{FracUpdLocal}
-	  {a \mupd_M B}
-	  {(q, a) \mupd \{q\} \times B}
-\end{mathpar}
-
-\begin{proof}[Proof of \ruleref{FracUpdFull}]
-Assume some $f \sep (1, a)$. This can only be $f = \munit$, so showing $f \sep (1, b)$ is trivial.
-\end{proof}
-
-\begin{proof}[Proof of \ruleref{FracUpdLocal}]
-	Assume some $f \sep (q, a)$. If $f = \munit$, then $f \sep (q, b)$ is trivial for any $b \in B$. Just pick the one we obtain by choosing $\munit_M$ as the frame for $a$.
-	
-	In the interesting case, we have $f = (q_f, a_f)$.
-	Obtain $b$ such that $b \in B \land b \sep a_f$.
-	Then $(q, b) \sep f$, and we are done.
-\end{proof}
-
-$\fracm{M}$ is cancellative if $M$ is cancellative.
-\begin{proof}[Proof of cancellativitiy]
-If $\melt_f = \munit$, we are trivially done.
-So let $\melt_f = (q_f, \melt_f')$.
-If $\melt = \munit$, then $\meltB = \munit$ as otherwise the fractions could not match up.
-Again, we are trivially done.
-Similar so for $\meltB = \munit$.
-So let $\melt = (q_a, \melt')$ and $\meltB = (q_b, \meltB')$.
-We have $(q_f + q_a, \melt_f' \mtimes \melt') = (q_f + q_b, \melt_f' \mtimes \meltB')$.
-We have to show $q_a = q_b$ and $\melt' = \meltB'$.
-The first is trivial, the second follows from cancellativitiy of $M$.
-\end{proof}
-
-\subsection{Finite partial function monoid}
-\label{sec:fpfunm}
-
-Given a countable set $X$ and a monoid $M$, we construct a monoid representing finite partial functions from $X$ to (non-unit, non-zero elements of) $M$.
-Let $\fpfunm{X}{M}$ be the product monoid $\prod_{x \in X} M$, as defined in \secref{sec:prodm} but restricting the carrier to functions $f$ where the set $\dom(f) \eqdef \{ x \mid f(x) \neq \munit_M \}$ is finite.
-This is well-defined as the set of these $f$ contains the unit and is closed under multiplication.
-(We identify finite partial functions from $X$ to $\mcarp{M}\setminus\{\munit_M\}$ and total functions from $X$ to $\mcarp{M}$ with finite $\munit_M$-support.)
-
-We use two frame-preserving updates:
-\begin{mathpar}
-  \inferH{FpFunAlloc}
-  {a \in \mcarp{M}}
-  {f \mupd \{ f[x \mapsto a] \mid x \notin \dom(f) \}}
-  \and
-  \inferH{FpFunUpd}
-  {a \mupd_M B}
-  {f[i \mapsto a] \mupd \{ f[i \mapsto b] \mid b \in B\}}
-\end{mathpar}
-Rule \ruleref{FpFunUpd} simply restates \ruleref{ProdUpd}.
-
-\begin{proof}[Proof of \ruleref{FpFunAlloc}]
-  Assume some $g \sep f$. Since $\dom(f \mtimes g)$ is finite, there will be some undefined element $x \notin \dom(f \mtimes g)$. Let $f' \eqdef f[x \mapsto a]$. This is compatible with $g$, so we are done.
-\end{proof}
-
-We write $[x \mapsto a]$ for the function mapping $x$ to $a$ and everything else in $X$ to $\munit$.
-
-%\subsection{Disposable monoid}
-%
-%Given a monoid $M$, we construct a monoid where, having full ownership of an element $\melt$ of $M$, one can throw it away, transitioning to a dead element.
-%Let \dispm{M} be the monoid with carrier $\mcarp{M} \uplus \{ \disposed \}$ and multiplication
-%% The previous unit must remain the unit of the new monoid, as is is always duplicable and hence we could not transition to \disposed if it were not composable with \disposed
-%\begin{align*}
-%  \melt \mtimes \meltB &\eqdef \melt \mtimes_M \meltB & \IF \melt \sep[M] \meltB \\
-%  \disposed \mtimes \disposed &\eqdef \disposed \\
-%  \munit_M \mtimes \disposed &\eqdef \disposed \mtimes \munit_M \eqdef \disposed
-%\end{align*}
-%The unit is the same as in $M$.
-%
-%The frame-preserving updates are
-%\begin{mathpar}
-% \inferH{DispUpd}
-%   {a \in \mcarp{M} \setminus \{\munit_M\} \and a \mupd_M B}
-%   {a \mupd B}
-% \and
-% \inferH{Dispose}
-%  {a \in \mcarp{M} \setminus \{\munit_M\} \and \All b \in \mcarp{M}. a \sep b \Ra b = \munit_M}
-%  {a \mupd \disposed}
-%\end{mathpar}
-%
-%\begin{proof}[Proof of \ruleref{DispUpd}]
-%Assume a frame $f$. If $f = \disposed$, then $a = \munit_M$, which is a contradiction.
-%Thus $f \in \mcarp{M}$ and we can use $a \mupd_M B$.
-%\end{proof}
-%
-%\begin{proof}[Proof of \ruleref{Dispose}]
-%The second premiss says that $a$ has no non-trivial frame in $M$. To show the update, assume a frame $f$ in $\dispm{M}$. Like above, we get $f \in \mcarp{M}$, and thus $f = \munit_M$. But $\disposed \sep \munit_M$ is trivial, so we are done.
-%\end{proof}
-
-\subsection{Authoritative monoid}\label{sec:auth}
-
-Given a monoid $M$, we construct a monoid modeling someone owning an \emph{authoritative} element $x$ of $M$, and others potentially owning fragments $\melt \le_M x$ of $x$.
-(If $M$ is an exclusive monoid, the construction is very similar to a half-ownership monoid with two asymmetric halves.)
-Let $\auth{M}$ be the monoid with carrier
-\[
-	\setComp{ (x, \melt) }{ x \in \mcarp{\exm{\mcarp{M}}} \land \melt \in \mcarp{M} \land (x = \munit_{\exm{\mcarp{M}}} \lor \melt \leq_M x) }
-\]
-and multiplication
-\[
-(x, \melt) \mtimes (y, \meltB) \eqdef
-     (x \mtimes y, \melt \mtimes \meltB) \quad \mbox{if } x \sep y \land \melt \sep \meltB \land (x \mtimes y = \munit_{\exm{\mcarp{M}}} \lor \melt \mtimes \meltB \leq_M x \mtimes y)
-\]
-Note that $(\munit_{\exm{\mcarp{M}}}, \munit_M)$ is the unit and asserts no ownership whatsoever, but $(\munit_{M}, \munit_M)$ asserts that the authoritative element is $\munit_M$.
-
-Let $x, \melt \in \mcarp M$.
-We write $\authfull x$ for full ownership $(x, \munit_M):\auth{M}$ and $\authfrag \melt$ for fragmental ownership $(\munit_{\exm{\mcarp{M}}}, \melt)$ and $\authfull x , \authfrag \melt$ for combined ownership $(x, \melt)$.
-If $x$ or $a$ is $\mzero_{M}$, then the sugar denotes $\mzero_{\auth{M}}$.
-
-\ralf{This needs syncing with the Coq development.}
-The frame-preserving update involves a rather unwieldy side-condition:
-\begin{mathpar}
-	\inferH{AuthUpd}{
-		\All\melt_f\in\mcar{\monoid}. \melt\sep\meltB \land \melt\mtimes\melt_f \le \meltB\mtimes\melt_f \Ra \melt'\mtimes\melt_f \le \melt'\mtimes\meltB \and
-		\melt' \sep \meltB
-	}{
-		\authfull \melt \mtimes \meltB, \authfrag \melt \mupd \authfull \melt' \mtimes \meltB, \authfrag \melt'
-	}
-\end{mathpar}
-We therefore derive two special cases.
-
-\paragraph{Local frame-preserving updates.}
-
-\newcommand\authupd{f}%
-Following~\cite{scsl}, we say that $\authupd: \mcar{M} \ra \mcar{M}$ is \emph{local} if
-\[
-	\All a, b \in \mcar{M}. a \sep b \land \authupd(a) \neq \mzero \Ra \authupd(a \mtimes b) = \authupd(a) \mtimes b
-\]
-Then,
-\begin{mathpar}
-	\inferH{AuthUpdLocal}
-	{\text{$\authupd$ local} \and \authupd(\melt)\sep\meltB}
-	{\authfull \melt \mtimes \meltB, \authfrag \melt \mupd \authfull \authupd(\melt) \mtimes \meltB, \authfrag \authupd(\melt)}
-\end{mathpar}
-
-\paragraph{Frame-preserving updates on cancellative monoids.}
-
-Frame-preserving updates are also possible if we assume $M$ cancellative:
-\begin{mathpar}
- \inferH{AuthUpdCancel}
-  {\text{$M$ cancellative} \and \melt'\sep\meltB}
-  {\authfull \melt \mtimes \meltB, \authfrag \melt \mupd \authfull \melt' \mtimes \meltB, \authfrag \melt'}
-\end{mathpar}
-
-\subsection{Fractional heap monoid}
-\label{sec:fheapm}
-
-By combining the fractional, finite partial function, and authoritative monoids, we construct two flavors of heaps with fractional permissions and mention their important frame-preserving updates.
-Hereinafter, we assume the set $\textdom{Val}$ of values is countable.
-
-Given a set $Y$, define $\FHeap(Y) \eqdef \fpfunm{\textdom{Val}}{\fracm{Y}}$ representing a fractional heap with codomain $Y$.
-From \S\S\ref{sec:fracm} and~\ref{sec:fpfunm} we obtain the following frame-preserving updates as well as the fact that $\FHeap(Y)$ is cancellative.
-\begin{mathpar}
-	\axiomH{FHeapUpd}{h[x \mapsto (1, y)] \mupd h[x \mapsto (1, y')]} \and
-	\axiomH{FHeapAlloc}{h \mupd \{\, h[x \mapsto (1, y)] \mid x \in \textdom{Val} \,\}}
-\end{mathpar}
-We will write $qh$ with $h : \textsort{Val} \fpfn Y$ for the function in $\FHeap(Y)$ mapping every $x \in \dom(h)$ to $(q, h(x))$, and everything else to $\munit$.
-
-Define $\AFHeap(Y) \eqdef \auth{\FHeap(Y)}$ representing an authoritative fractional heap with codomain $Y$.
-We easily obtain the following frame-preserving updates.
-\begin{mathpar}
-	\axiomH{AFHeapUpd}{
-		(\authfull h[x \mapsto (1, y)], \authfrag [x \mapsto (1, y)]) \mupd (\authfull h[x \mapsto (1, y')], \authfrag [x \mapsto (1, y')])
-	}
-	\and
-	\inferH{AFHeapAdd}{
-		x \notin \dom(h)
-	}{
-		\authfull h \mupd (\authfull h[x \mapsto (q, y)], \authfrag [x \mapsto (q, y)])
-	}
-	\and
-	\axiomH{AFHeapRemove}{
-		(\authfull h[x \mapsto (q, y)], \authfrag [x \mapsto (q, y)]) \mupd \authfull h
-	}
-\end{mathpar}
-
-\subsection{STS with tokens monoid}
-\label{sec:stsmon}
-
-\ralf{This needs syncing with the Coq development.}
-
-Given a state-transition system~(STS) $(\STSS, \ra)$, a set of tokens $\STSS$, and a labeling $\STSL: \STSS \ra \mathcal{P}(\STST)$ of \emph{protocol-owned} tokens for each state, we construct a monoid modeling an authoritative current state and permitting transitions given a \emph{bound} on the current state and a set of \emph{locally-owned} tokens.
-
-The construction follows the idea of STSs as described in CaReSL \cite{caresl}.
-We first lift the transition relation to $\STSS \times \mathcal{P}(\STST)$ (implementing a \emph{law of token conservation}) and define upwards closure:
-\begin{align*}
- (s, T) \ra (s', T') \eqdef&\, s \ra s' \land \STSL(s) \uplus T = \STSL(s') \uplus T' \\
- \textsf{frame}(s, T) \eqdef&\, (s, \STST \setminus (\STSL(s) \uplus T)) \\
- \upclose(S, T) \eqdef&\, \setComp{ s' \in \STSS}{\exists s \in S.\; \textsf{frame}(s, T) \ststrans \textsf{frame}(s', T) }
-\end{align*}
-
-\noindent
-We have
-\begin{quote}
-	If $(s, T) \ra (s', T')$\\
-	and $T_f \sep (T \uplus \STSL(s))$,\\
-	then $\textsf{frame}(s, T_f) \ra \textsf{frame}(s', T_f)$.
-\end{quote}
-\begin{proof}
-This follows directly by framing the tokens in $\STST \setminus (T_f \uplus T \uplus \STSL(s))$ around the given transition, which yields $(s, \STST \setminus (T_f \uplus \STSL{T}(s))) \ra (s', T' \uplus (\STST \setminus (T_f \uplus T \uplus \STSL{T}(s))))$.
-This is exactly what we have to show, since we know $\STSL(s) \uplus T = \STSL(s') \uplus T'$.
-\end{proof}
-
-Let $\STSMon{\STSS}$ be the monoid with carrier
-\[
-	\setComp{ (s, S, T) \in \exm{\STSS} \times \mathcal{P}(\STSS) \times \mathcal{P}(\STST) }{ \begin{aligned} &(s = \munit \lor s \in S) \land \upclose(S, T) = S   \land{} \\& S \neq \emptyset \land \All s \in S. \STSL(s) \sep T  \end{aligned} }
-\]
-and multiplication
-\[
-	(s, S, T) \mtimes (s', S', T') \eqdef (s'' \eqdef s \mtimes_{\exm{\STSS}} s', S'' \eqdef S \cap S', T'' \eqdef T \cup T') \quad \text{if }\begin{aligned}[t] &(s = \munit \lor s' = \munit) \land T \sep T' \land{} \\& S'' \neq \emptyset \land (s'' \neq \munit \Ra s'' \in S'') \end{aligned}
-\]
-
-Some sugar makes it more convenient to assert being at least in a certain state and owning some tokens: $(s, T) : \STSMon{\STSS} \eqdef (\munit, \upclose(\{s\}, T), T) : \STSMon{\STSS}$, and
-$s : \STSMon{\STSS} \eqdef (s, \emptyset) : \STSMon{\STSS}$.
-
-We will need the following frame-preserving update.
-\begin{mathpar}
-	\inferH{StsStep}{(s, T) \ststrans (s', T')}
-	 {(s, S, T) \mupd (s', \upclose(\{s'\}, T'), T')}
-\end{mathpar}
-\begin{proof}[Proof of \ruleref{StsStep}]
-Assume some upwards-closed $S_f, T_f$ (the frame cannot be authoritative) s.t.\ $s \in S_f$ and $T_f \sep (T \uplus \STSL(s))$. We have to show that this frame combines with our final monoid element, which is the case if $s' \in S_f$ and $T_f \sep T'$.
-By upward-closedness, it suffices to show $\textsf{frame}(s, T_f) \ststrans \textsf{frame}(s', T_f)$.
-This follows by induction on the path $(s, T) \ststrans (s', T')$, and using the lemma proven above for each step.
-\end{proof}
-
-
-%%% Local Variables: 
-%%% mode: latex
-%%% TeX-master: "iris"
-%%% End: 

docs/derived.tex

-\section{Derived constructions}
-
-In this section we describe some constructions that we will use throughout the rest of the appendix.
-
-\subsection{Global monoid}
-
-Hereinafter we assume the global monoid (served up as a parameter to Iris) is obtained from a family of monoids $(M_i)_{i \in I}$ by first applying the construction for finite partial functions to each~(\Sref{sec:fpfunm}), and then applying the product construction~(\Sref{sec:prodm}):
-\[ M \eqdef \prod_{i \in I} \fpfunm{\textdom{GhName}}{M_i} \]
-We don't care so much about what concretely $\textdom{GhName}$ is, as long as it is countable and infinite.
-We write $\ownGhost{\gname}{\melt : M_i}$ (or just $\ownGhost{\gname}{\melt}$ if $M_i$ is clear from the context) for $\ownGGhost{[i \mapsto [\gname \mapsto \melt]]}$ when $\melt \in \mcarp {M_i}$, and for $\FALSE$ when $\melt = \mzero_{M_i}$.
-In other words, $\ownGhost{\gname}{\melt : M_i}$ asserts that in the current state of monoid $M_i$, the name $\gname$ is allocated and has at least value $\melt$.
-
-From~\ruleref{FpUpd} and the multiplications and frame-preserving updates in~\Sref{sec:prodm} and~\Sref{sec:fpfunm}, we have the following derived rules.
-\begin{mathpar}
-	\axiomH{NewGhost}{
-		\TRUE \vs \Exists\gname. \ownGhost\gname{\melt : M_i}
-	}
-	\and
-	\inferH{GhostUpd}
-    {\melt \mupd_{M_i} B}
-    {\ownGhost\gname{\melt : M_i} \vs \Exists \meltB\in B. \ownGhost\gname{\meltB : M_i}}
-  \and
-  \axiomH{GhostEq}
-    {\ownGhost\gname{\melt : M_i} * \ownGhost\gname{\meltB : M_i} \Lra \ownGhost\gname{\melt\mtimes\meltB : M_i}}
-
-  \axiomH{GhostUnit}
-    {\TRUE \Ra \ownGhost{\gname}{\munit : M_i}}
-
-  \axiomH{GhostZero}
-    {\ownGhost\gname{\mzero : M_i} \Ra \FALSE}
-
-  \axiomH{GhostTimeless}
-    {\timeless{\ownGhost\gname{\melt : M_i}}}
-\end{mathpar}
-
-\subsection{STSs with interpretation}\label{sec:stsinterp}
-
-Building on \Sref{sec:stsmon}, after constructing the monoid $\STSMon{\STSS}$ for a particular STS, we can use an invariant to tie an interpretation, $\pred : \STSS \to \Prop$, to the STS's current state, recovering CaReSL-style reasoning~\cite{caresl}.
-
-An STS invariant asserts authoritative ownership of an STS's current state and that state's interpretation:
-\begin{align*}
-  \STSInv(\STSS, \pred, \gname) \eqdef{}& \Exists s \in \STSS. \ownGhost{\gname}{(s, \STSS, \emptyset):\STSMon{\STSS}} * \pred(s) \\
-  \STS(\STSS, \pred, \gname, \iname) \eqdef{}& \knowInv{\iname}{\STSInv(\STSS, \pred, \gname)}
-\end{align*}
-
-We can specialize \ruleref{NewInv}, \ruleref{InvOpen}, and \ruleref{InvClose} to STS invariants:
-\begin{mathpar}
- \inferH{NewSts}
-  {\infinite(\mask)}
-  {\later\pred(s) \vs[\mask] \Exists \iname \in \mask, \gname.   \STS(\STSS, \pred, \gname, \iname) * \ownGhost{\gname}{(s, \STST \setminus \STSL(s)) : \STSMon{\STSS}}}
- \and
- \axiomH{StsOpen}
-  {  \STS(\STSS, \pred, \gname, \iname) \vdash \ownGhost{\gname}{(s_0, T) : \STSMon{\STSS}} \vsE[\{\iname\}][\emptyset] \Exists s\in \upclose(\{s_0\}, T). \later\pred(s) * \ownGhost{\gname}{(s, \upclose(\{s_0\}, T), T):\STSMon{\STSS}}}
- \and
- \axiomH{StsClose}
-  {  \STS(\STSS, \pred, \gname, \iname), (s, T) \ststrans (s', T')  \proves \later\pred(s') * \ownGhost{\gname}{(s, S, T):\STSMon{\STSS}} \vs[\emptyset][\{\iname\}] \ownGhost{\gname}{(s', T') : \STSMon{\STSS}} }
-\end{mathpar}
-\begin{proof}
-\ruleref{NewSts} uses \ruleref{NewGhost} to allocate $\ownGhost{\gname}{(s, \upclose(s, T), T) : \STSMon{\STSS}}$ where $T \eqdef \STST \setminus \STSL(s)$, and \ruleref{NewInv}.
-
-\ruleref{StsOpen} just uses \ruleref{InvOpen} and \ruleref{InvClose} on $\iname$, and the monoid equality $(s, \upclose(\{s_0\}, T), T) = (s, \STSS, \emptyset) \mtimes (\munit, \upclose(\{s_0\}, T), T)$.
-
-\ruleref{StsClose} applies \ruleref{StsStep} and \ruleref{InvClose}.
-\end{proof}
-
-Using these view shifts, we can prove STS variants of the invariant rules \ruleref{Inv} and \ruleref{VSInv}~(compare the former to CaReSL's island update rule~\cite{caresl}):
-\begin{mathpar}
- \inferH{Sts}
-  {\All s \in \upclose(\{s_0\}, T). \hoare{\later\pred(s) * P}{\expr}{\Ret \val. \Exists s', T'. (s, T) \ststrans (s', T') * \later\pred(s') * Q}[\mask]
-   \and \physatomic{\expr}}
-  {  \STS(\STSS, \pred, \gname, \iname) \vdash \hoare{\ownGhost{\gname}{(s_0, T):\STSMon{\STSS}} * P}{\expr}{\Ret \val. \Exists s', T'. \ownGhost{\gname}{(s', T'):\STSMon{\STSS}} * Q}[\mask \uplus \{\iname\}]}
- \and
- \inferH{VSSts}
-  {\forall s \in \upclose(\{s_0\}, T).\; \later\pred(s) * P \vs[\mask_1][\mask_2] \exists s', T'.\; (s, T) \ststrans (s', T') * \later\pred(s') * Q}
-  {  \STS(\STSS, \pred, \gname, \iname) \vdash \ownGhost{\gname}{(s_0, T):\STSMon{\STSS}} * P \vs[\mask_1 \uplus \{\iname\}][\mask_2 \uplus \{\iname\}] \Exists s', T'. \ownGhost{\gname}{(s', T'):\STSMon{\STSS}} * Q}
-\end{mathpar}
-
-\begin{proof}[Proof of \ruleref{Sts}]\label{pf:sts}
- We have to show
- \[\hoare{\ownGhost{\gname}{(s_0, T):\STSMon{\STSS}} * P}{\expr}{\Ret \val. \Exists s', T'. \ownGhost{\gname}{(s', T'):\STSMon{\STSS}} * Q}[\mask \uplus \{\iname\}]\]
- where $\val$, $s'$, $T'$ are free in $Q$.
- 
- First, by \ruleref{ACsq} with \ruleref{StsOpen} and \ruleref{StsClose} (after moving $(s, T) \ststrans (s', T')$ into the view shift using \ruleref{VSBoxOut}), it suffices to show
- \[\hoareV{\Exists s\in \upclose(\{s_0\}, T). \later\pred(s) * \ownGhost{\gname}{(s, \upclose(\{s_0\}, T), T)} * P}{\expr}{\Ret \val. \Exists s, T, S, s', T'. (s, T) \ststrans (s', T') * \later\pred(s') * \ownGhost{\gname}{(s, S, T):\STSMon{\STSS}} * Q(\val, s', T')}[\mask]\]
-
- Now, use \ruleref{Exist} to move the $s$ from the precondition into the context and use \ruleref{Csq} to (i)~fix the $s$ and $T$ in the postcondition to be the same as in the precondition, and (ii)~fix $S \eqdef \upclose(\{s_0\}, T)$.
- It remains to show:
- \[\hoareV{s\in \upclose(\{s_0\}, T) * \later\pred(s) * \ownGhost{\gname}{(s, \upclose(\{s_0\}, T), T)} * P}{\expr}{\Ret \val. \Exists s', T'. (s, T) \ststrans (s', T') * \later\pred(s') * \ownGhost{\gname}{(s, \upclose(\{s_0\}, T), T)} * Q(\val, s', T')}[\mask]\]
- 
- Finally, use \ruleref{BoxOut} to move $s\in \upclose(\{s_0\}, T)$ into the context, and \ruleref{Frame} on $\ownGhost{\gname}{(s, \upclose(\{s_0\}, T), T)}$:
- \[s\in \upclose(\{s_0\}, T) \vdash \hoare{\later\pred(s) * P}{\expr}{\Ret \val. \Exists s', T'. (s, T) \ststrans (s', T') * \later\pred(s') * Q(\val, s', T')}[\mask]\]
- 
- This holds by our premise.
-\end{proof}
-
-% \begin{proof}[Proof of \ruleref{VSSts}]
-% This is similar to above, so we only give the proof in short notation:
-
-% \hproof{%
-% 	Context: $\knowInv\iname{\STSInv(\STSS, \pred, \gname)}$ \\
-% 	\pline[\mask_1 \uplus \{\iname\}]{
-% 		\ownGhost\gname{(s_0, T)} * P
-% 	} \\
-% 	\pline[\mask_1]{%
-% 		\Exists s. \later\pred(s) * \ownGhost\gname{(s, S, T)} * P
-% 	} \qquad by \ruleref{StsOpen} \\
-% 	Context: $s \in S \eqdef \upclose(\{s_0\}, T)$ \\
-% 	\pline[\mask_2]{%
-% 		 \Exists s', T'. \later\pred(s') * Q(s', T') * \ownGhost\gname{(s, S, T)}
-% 	} \qquad by premiss \\
-% 	Context: $(s, T) \ststrans (s', T')$ \\
-% 	\pline[\mask_2 \uplus \{\iname\}]{
-% 		\ownGhost\gname{(s', T')} * Q(s', T')
-% 	} \qquad by \ruleref{StsClose}
-% }
-% \end{proof}
-
-\subsection{Authoritative monoids with interpretation}\label{sec:authinterp}
-
-Building on \Sref{sec:auth}, after constructing the monoid $\auth{M}$ for a cancellative monoid $M$, we can tie an interpretation, $\pred : \mcarp{M} \to \Prop$, to the authoritative element of $M$, recovering reasoning that is close to the sharing rule in~\cite{krishnaswami+:icfp12}.
-
-Let $\pred_\bot$ be the extension of $\pred$ to $\mcar{M}$ with $\pred_\bot(\mzero) = \FALSE$.
-Now define
-\begin{align*}
-  \AuthInv(M, \pred, \gname) \eqdef{}& \exists \melt \in \mcar{M}.\; \ownGhost{\gname}{\authfull \melt:\auth{M}} * \pred_\bot(\melt) \\
-  \Auth(M, \pred, \gname, \iname) \eqdef{}& M~\textlog{cancellative} \land \knowInv{\iname}{\AuthInv(M, \pred, \gname)}
-\end{align*}
-
-The frame-preserving updates for $\auth{M}$ gives rise to the following view shifts:
-\begin{mathpar}
- \inferH{NewAuth}
-  {\infinite(\mask) \and M~\textlog{cancellative}}
-  {\later\pred_\bot(a) \vs[\mask] \exists \iname \in \mask, \gname.\; \Auth(M, \pred, \gname, \iname) * \ownGhost{\gname}{\authfrag a : \auth{M}}}
- \and
- \axiomH{AuthOpen}
-  {\Auth(M, \pred, \gname, \iname) \vdash \ownGhost{\gname}{\authfrag \melt : \auth{M}} \vsE[\{\iname\}][\emptyset] \exists \melt_f.\; \later\pred_\bot(\melt \mtimes \melt_f) * \ownGhost{\gname}{\authfull \melt \mtimes \melt_f, \authfrag a:\auth{M}}}
- \and
- \axiomH{AuthClose}
-  {\Auth(M, \pred, \gname, \iname) \vdash \later\pred_\bot(\meltB \mtimes \melt_f) * \ownGhost{\gname}{\authfull a \mtimes \melt_f, \authfrag a:\auth{M}} \vs[\emptyset][\{\iname\}] \ownGhost{\gname}{\authfrag \meltB : \auth{M}} }
-\end{mathpar}
-
-These view shifts in turn can be used to prove variants of the invariant rules:
-\begin{mathpar}
- \inferH{Auth}
-  {\forall \melt_f.\; \hoare{\later\pred_\bot(a \mtimes \melt_f) * P}{\expr}{\Ret\val. \exists \meltB.\; \later\pred_\bot(\meltB\mtimes \melt_f) * Q}[\mask]
-   \and \physatomic{\expr}}
-  {\Auth(M, \pred, \gname, \iname) \vdash \hoare{\ownGhost{\gname}{\authfrag a:\auth{M}} * P}{\expr}{\Ret\val. \exists \meltB.\; \ownGhost{\gname}{\authfrag \meltB:\auth{M}} * Q}[\mask \uplus \{\iname\}]}
- \and
- \inferH{VSAuth}
-  {\forall \melt_f.\; \later\pred_\bot(a \mtimes \melt_f) * P \vs[\mask_1][\mask_2] \exists \meltB.\; \later\pred_\bot(\meltB \mtimes \melt_f) * Q(\meltB)}
-  {\Auth(M, \pred, \gname, \iname) \vdash
-   \ownGhost{\gname}{\authfrag a:\auth{M}} * P \vs[\mask_1 \uplus \{\iname\}][\mask_2 \uplus \{\iname\}]
-   \exists \meltB.\; \ownGhost{\gname}{\authfrag \meltB:\auth{M}} * Q(\meltB)}
-\end{mathpar}
-
-
-\subsection{Ghost heap}
-\label{sec:ghostheap}%
-
-We define a simple ghost heap with fractional permissions.
-Some modules require a few ghost names per module instance to properly manage ghost state, but would like to expose to clients a single logical name (avoiding clutter).
-In such cases we use these ghost heaps.
-
-We seek to implement the following interface:
-\newcommand{\GRefspecmaps}{\textsf{GMapsTo}}%
-\begin{align*}
- \exists& {\fgmapsto[]} : \textsort{Val} \times \mathbb{Q}_{>} \times \textsort{Val} \ra \textsort{Prop}.\;\\
-  & \All x, q, v. x \fgmapsto[q] v \Ra x \fgmapsto[q] v \land q \in (0, 1] \\
-  &\forall x, q_1, q_2, v, w.\; x \fgmapsto[q_1] v * x \fgmapsto[q_2] w \Leftrightarrow x \fgmapsto[q_1 + q_2] v * v = w\\
-  & \forall v.\; \TRUE \vs[\emptyset] \exists x.\; x \fgmapsto[1] v \\
-  & \forall x, v, w.\; x \fgmapsto[1] v \vs[\emptyset] x \fgmapsto[1] w
-\end{align*}
-We write $x \fgmapsto v$ for $\exists q.\; x \fgmapsto[q] v$ and $x \gmapsto v$ for $x \fgmapsto[1] v$.
-Note that $x \fgmapsto v$ is duplicable but cannot be boxed (as it depends on resources); \ie we have $x \fgmapsto v \Lra x \fgmapsto v * x \fgmapsto v$ but not $x \fgmapsto v \Ra \always x \fgmapsto v$.
-
-To implement this interface, allocate an instance $\gname_G$ of $\FHeap(\textdom{Val})$ and define
-\[
-	x \fgmapsto[q] v \eqdef
-	  \begin{cases}
-    	\ownGhost{\gname_G}{x \mapsto (q, v)} & \text{if $q \in (0, 1]$} \\
-    	\FALSE & \text{otherwise}
-    \end{cases}
-\]
-The view shifts in the specification follow immediately from \ruleref{GhostUpd} and the frame-preserving updates in~\Sref{sec:fheapm}.
-The first implication is immediate from the definition.
-The second implication follows by case distinction on $q_1 + q_2 \in (0, 1]$.
-
-
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: "iris"
-%%% End:

docs/dune.md

+Support for the dune build system
+=================================
+
+**NOTE:** in case of problem with the dune build, you can ask @lepigre or
+@Blaisorblade for help.
+
+The library can be built using dune by running `dune build`. Note that `dune`
+needs to be installed separately with `opam install dune`, as it is currently
+not part of the dependencies of the project.
+
+Useful links:
+- [dune documentation](https://dune.readthedocs.io)
+- [coq zulip channel](https://coq.zulipchat.com/#narrow/stream/240550-Dune-devs-.26-users)
+
+
+Editor support
+--------------
+
+Good dune support in editors is lacking at the moment, but there are tricks you
+can play to make it work.
+
+One option is to configure your editor to invoke the `dune coq top` command
+instead of `coqtop`, but that is not easy to configure.
+
+Another option is to change the `_CoqProject` file to something like:
+```
+-Q iris iris
+-Q _build/default/iris iris
+-Q iris_heap_lang iris.heap_lang
+-Q _build/default/iris_heap_lang iris.heap_lang
+-Q iris_unstable iris.unstable
+-Q _build/default/iris_unstable iris.unstable
+-Q iris_deprecated iris.deprecated
+-Q _build/default/iris_deprecated iris.deprecated
+```
+Note that this includes two bindings for each logical path: a binding to a
+folder in the source tree (where editors will find the `.v` files), and a
+binding to the same folder under `_build/default` (where editors will find
+the corresponding `.vo` files). The binding for a source folder must come
+before the binding for the corresponding build folder, so that editors know
+to jump to source files in the source tree (and not their read-only copy in
+the build folder).
+
+If you do this, you still need to invoke `dune` manually to make sure that the
+dependencies of the file you are stepping through are up-to-date. To build a
+single file, you can do, e.g., `dune build iris/prelude/options.vo`. To build
+only the `iris` folder, you can do `dune build iris`.