algebra/cofe.v

-From iris.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.
-
-Record chain (A : Type) `{Dist A} := {
-  chain_car :> nat → A;
-  chain_cauchy n i : n ≤ i → chain_car i ≡{n}≡ chain_car 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 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;
-  _ : Type
-}.
-Arguments CofeT' _ {_ _ _} _ _.
-Notation CofeT A m := (CofeT' A m A).
-Add Printing Constructor cofeT.
-Hint Extern 0 (Equiv _) => eapply (@cofe_equiv _) : typeclass_instances.
-Hint Extern 0 (Dist _) => eapply (@cofe_dist _) : typeclass_instances.
-Hint Extern 0 (Compl _) => eapply (@cofe_compl _) : typeclass_instances.
-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 n.
-  Proof. apply (mixin_conv_compl _ (cofe_mixin A)). Qed.
-End cofe_mixin.
-
-Hint Extern 1 (_ ≡{_}≡ _) => apply equiv_dist; assumption.
-
-(** Discrete COFEs and Timeless elements *)
-(* TODO: On paper, We called these "discrete elements". I think that makes
-   more sense. *)
-Class Timeless `{Equiv A, Dist A} (x : A) := timeless y : x ≡{0}≡ y → x ≡ y.
-Arguments timeless {_ _ _} _ {_} _ _.
-Class Discrete (A : cofeT) := discrete_timeless (x : A) :> Timeless x.
-
-(** 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; trans 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 trans x1; [|trans y1].
-    - by trans x2; [|trans 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.
-  Lemma dist_le' n n' x y : n' ≤ n → x ≡{n}≡ y → x ≡{n'}≡ y.
-  Proof. intros; eauto using dist_le. 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 := _.
-
-  Lemma conv_compl' n (c : chain A) : compl c ≡{n}≡ c (S n).
-  Proof.
-    transitivity (c n); first by apply conv_compl. symmetry.
-    apply chain_cauchy. omega.
-  Qed.
-  Lemma timeless_iff n (x : A) `{!Timeless x} y : x ≡ y ↔ x ≡{n}≡ y.
-  Proof.
-    split; intros; auto. apply (timeless _), dist_le with n; auto with lia.
-  Qed.
-End cofe.
-
-Instance const_contractive {A B : cofeT} (x : A) : Contractive (@const A B x).
-Proof. by intros n y1 y2. Qed.
-
-(** 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.
-
-(** 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 in *; try reflexivity || omega.
-  - apply (contractive_0 f).
-  - apply (contractive_S f), IH; auto with omega.
-Qed.
-
-Program Definition fixpoint_def {A : cofeT} `{Inhabited A} (f : A → A)
-  `{!Contractive f} : A := compl (fixpoint_chain f).
-Definition fixpoint_aux : { x | x = @fixpoint_def }. by eexists. Qed.
-Definition fixpoint {A AiH} f {Hf} := proj1_sig fixpoint_aux A AiH f Hf.
-Definition fixpoint_eq : @fixpoint = @fixpoint_def := proj2_sig fixpoint_aux.
-
-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_eq /fixpoint_def (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_eq /fixpoint_def
-      (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.
-
-(** 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.
-
-Notation "'λne' x .. y , t" :=
-  (@CofeMor _ _ (λ x, .. (@CofeMor _ _ (λ y, t) _) ..) _)
-  (at level 200, x binder, y binder, right associativity).
-
-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; trans (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 (cofeMor A B) 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 and constant function *)
-Definition cid {A} : A -n> A := CofeMor id.
-Instance: Params (@cid) 1.
-Definition cconst {A B : cofeT} (x : B) : A -n> B := CofeMor (const x).
-Instance: Params (@cconst) 2.
-
-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.
-
-(* Function space maps *)
-Definition cofe_mor_map {A A' B B'} (f : A' -n> A) (g : B -n> B')
-  (h : A -n> B) : A' -n> B' := g ◎ h ◎ f.
-Instance cofe_mor_map_ne {A A' B B'} n :
-  Proper (dist n ==> dist n ==> dist n ==> dist n) (@cofe_mor_map A A' B B').
-Proof. intros ??? ??? ???. by repeat apply ccompose_ne. Qed.
-
-Definition cofe_morC_map {A A' B B'} (f : A' -n> A) (g : B -n> B') :
-  (A -n> B) -n> (A' -n>  B') := CofeMor (cofe_mor_map f g).
-Instance cofe_morC_map_ne {A A' B B'} n :
-  Proper (dist n ==> dist n ==> dist n) (@cofe_morC_map A A' B B').
-Proof.
-  intros f f' Hf g g' Hg ?. rewrite /= /cofe_mor_map.
-  by repeat apply ccompose_ne.
-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 unit_cofe_mixin.
-  Global Instance unit_discrete_cofe : Discrete unitC.
-  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 (A * B) prod_cofe_mixin.
-  Global Instance prod_timeless (x : A * B) :
-    Timeless (x.1) → Timeless (x.2) → Timeless x.
-  Proof. by intros ???[??]; split; apply (timeless _). Qed.
-  Global Instance prod_discrete_cofe : Discrete A → Discrete B → Discrete prodC.
-  Proof. intros ?? [??]; apply _. 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.
-
-(** Functors *)
-Structure cFunctor := CFunctor {
-  cFunctor_car : cofeT → cofeT → cofeT;
-  cFunctor_map {A1 A2 B1 B2} :
-    ((A2 -n> A1) * (B1 -n> B2)) → cFunctor_car A1 B1 -n> cFunctor_car A2 B2;
-  cFunctor_ne {A1 A2 B1 B2} n :
-    Proper (dist n ==> dist n) (@cFunctor_map A1 A2 B1 B2);
-  cFunctor_id {A B : cofeT} (x : cFunctor_car A B) :
-    cFunctor_map (cid,cid) x ≡ x;
-  cFunctor_compose {A1 A2 A3 B1 B2 B3}
-      (f : A2 -n> A1) (g : A3 -n> A2) (f' : B1 -n> B2) (g' : B2 -n> B3) x :
-    cFunctor_map (f◎g, g'◎f') x ≡ cFunctor_map (g,g') (cFunctor_map (f,f') x)
-}.
-Existing Instance cFunctor_ne.
-Instance: Params (@cFunctor_map) 5.
-
-Delimit Scope cFunctor_scope with CF.
-Bind Scope cFunctor_scope with cFunctor.
-
-Class cFunctorContractive (F : cFunctor) :=
-  cFunctor_contractive A1 A2 B1 B2 :> Contractive (@cFunctor_map F A1 A2 B1 B2).
-
-Definition cFunctor_diag (F: cFunctor) (A: cofeT) : cofeT := cFunctor_car F A A.
-Coercion cFunctor_diag : cFunctor >-> Funclass.
-
-Program Definition constCF (B : cofeT) : cFunctor :=
-  {| cFunctor_car A1 A2 := B; cFunctor_map A1 A2 B1 B2 f := cid |}.
-Solve Obligations with done.
-
-Instance constCF_contractive B : cFunctorContractive (constCF B).
-Proof. rewrite /cFunctorContractive; apply _. Qed.
-
-Program Definition idCF : cFunctor :=
-  {| cFunctor_car A1 A2 := A2; cFunctor_map A1 A2 B1 B2 f := f.2 |}.
-Solve Obligations with done.
-
-Program Definition prodCF (F1 F2 : cFunctor) : cFunctor := {|
-  cFunctor_car A B := prodC (cFunctor_car F1 A B) (cFunctor_car F2 A B);
-  cFunctor_map A1 A2 B1 B2 fg :=
-    prodC_map (cFunctor_map F1 fg) (cFunctor_map F2 fg)
-|}.
-Next Obligation.
-  intros ?? A1 A2 B1 B2 n ???; by apply prodC_map_ne; apply cFunctor_ne.
-Qed.
-Next Obligation. by intros F1 F2 A B [??]; rewrite /= !cFunctor_id. Qed.
-Next Obligation.
-  intros F1 F2 A1 A2 A3 B1 B2 B3 f g f' g' [??]; simpl.
-  by rewrite !cFunctor_compose.
-Qed.
-
-Instance prodCF_contractive F1 F2 :
-  cFunctorContractive F1 → cFunctorContractive F2 →
-  cFunctorContractive (prodCF F1 F2).
-Proof.
-  intros ?? A1 A2 B1 B2 n ???;
-    by apply prodC_map_ne; apply cFunctor_contractive.
-Qed.
-
-Program Definition cofe_morCF (F1 F2 : cFunctor) : cFunctor := {|
-  cFunctor_car A B := cofe_mor (cFunctor_car F1 B A) (cFunctor_car F2 A B);
-  cFunctor_map A1 A2 B1 B2 fg :=
-    cofe_morC_map (cFunctor_map F1 (fg.2, fg.1)) (cFunctor_map F2 fg)
-|}.
-Next Obligation.
-  intros F1 F2 A1 A2 B1 B2 n [f g] [f' g'] Hfg; simpl in *.
-  apply cofe_morC_map_ne; apply cFunctor_ne; split; by apply Hfg.
-Qed.
-Next Obligation.
-  intros F1 F2 A B [f ?] ?; simpl. rewrite /= !cFunctor_id.
-  apply (ne_proper f). apply cFunctor_id.
-Qed.
-Next Obligation.
-  intros F1 F2 A1 A2 A3 B1 B2 B3 f g f' g' [h ?] ?; simpl in *.
-  rewrite -!cFunctor_compose. do 2 apply (ne_proper _). apply cFunctor_compose.
-Qed.
-
-Instance cofe_morCF_contractive F1 F2 :
-  cFunctorContractive F1 → cFunctorContractive F2 →
-  cFunctorContractive (cofe_morCF F1 F2).
-Proof.
-  intros ?? A1 A2 B1 B2 n [f g] [f' g'] Hfg; simpl in *.
-  apply cofe_morC_map_ne; apply cFunctor_contractive=>i ?; split; by apply Hfg.
-Qed.
-
-(** Sum *)
-Section sum.
-  Context {A B : cofeT}.
-
-  Instance sum_dist : Dist (A + B) := λ n, sum_relation (dist n) (dist n).
-  Global Instance inl_ne : Proper (dist n ==> dist n) (@inl A B) := _.
-  Global Instance inr_ne : Proper (dist n ==> dist n) (@inr A B) := _.
-  Global Instance inl_ne_inj : Inj (dist n) (dist n) (@inl A B) := _.
-  Global Instance inr_ne_inj : Inj (dist n) (dist n) (@inr A B) := _.
-
-  Program Definition inl_chain (c : chain (A + B)) (a : A) : chain A :=
-    {| chain_car n := match c n return _ with inl a' => a' | _ => a end |}.
-  Next Obligation. intros c a n i ?; simpl. by destruct (chain_cauchy c n i). Qed.
-  Program Definition inr_chain (c : chain (A + B)) (b : B) : chain B :=
-    {| chain_car n := match c n return _ with inr b' => b' | _ => b end |}.
-  Next Obligation. intros c b n i ?; simpl. by destruct (chain_cauchy c n i). Qed.
-
-  Instance sum_compl : Compl (A + B) := λ c,
-    match c 0 with
-    | inl a => inl (compl (inl_chain c a))
-    | inr b => inr (compl (inr_chain c b))
-    end.
-
-  Definition sum_cofe_mixin : CofeMixin (A + B).
-  Proof.
-    split.
-    - intros x y; split=> Hx.
-      + destruct Hx=> n; constructor; by apply equiv_dist.
-      + destruct (Hx 0); constructor; apply equiv_dist=> n; by apply (inj _).
-    - apply _.
-    - destruct 1; constructor; by apply dist_S.
-    - intros n c; rewrite /compl /sum_compl.
-      feed inversion (chain_cauchy c 0 n); first auto with lia; constructor.
-      + rewrite (conv_compl n (inl_chain c _)) /=. destruct (c n); naive_solver.
-      + rewrite (conv_compl n (inr_chain c _)) /=. destruct (c n); naive_solver.
-  Qed.
-  Canonical Structure sumC : cofeT := CofeT (A + B) sum_cofe_mixin.
-
-  Global Instance inl_timeless (x : A) : Timeless x → Timeless (inl x).
-  Proof. inversion_clear 2; constructor; by apply (timeless _). Qed.
-  Global Instance inr_timeless (y : B) : Timeless y → Timeless (inr y).
-  Proof. inversion_clear 2; constructor; by apply (timeless _). Qed.
-  Global Instance sum_discrete_cofe : Discrete A → Discrete B → Discrete sumC.
-  Proof. intros ?? [?|?]; apply _. Qed.
-End sum.
-
-Arguments sumC : clear implicits.
-Typeclasses Opaque sum_dist.
-
-Instance sum_map_ne {A A' B B' : cofeT} n :
-  Proper ((dist n ==> dist n) ==> (dist n ==> dist n) ==>
-           dist n ==> dist n) (@sum_map A A' B B').
-Proof.
-  intros f f' Hf g g' Hg ??; destruct 1; constructor; [by apply Hf|by apply Hg].
-Qed.
-Definition sumC_map {A A' B B'} (f : A -n> A') (g : B -n> B') :
-  sumC A B -n> sumC A' B' := CofeMor (sum_map f g).
-Instance sumC_map_ne {A A' B B'} n :
-  Proper (dist n ==> dist n ==> dist n) (@sumC_map A A' B B').
-Proof. intros f f' Hf g g' Hg [?|?]; constructor; [apply Hf|apply Hg]. Qed.
-
-Program Definition sumCF (F1 F2 : cFunctor) : cFunctor := {|
-  cFunctor_car A B := sumC (cFunctor_car F1 A B) (cFunctor_car F2 A B);
-  cFunctor_map A1 A2 B1 B2 fg :=
-    sumC_map (cFunctor_map F1 fg) (cFunctor_map F2 fg)
-|}.
-Next Obligation.
-  intros ?? A1 A2 B1 B2 n ???; by apply sumC_map_ne; apply cFunctor_ne.
-Qed.
-Next Obligation. by intros F1 F2 A B [?|?]; rewrite /= !cFunctor_id. Qed.
-Next Obligation.
-  intros F1 F2 A1 A2 A3 B1 B2 B3 f g f' g' [?|?]; simpl;
-    by rewrite !cFunctor_compose.
-Qed.
-
-Instance sumCF_contractive F1 F2 :
-  cFunctorContractive F1 → cFunctorContractive F2 →
-  cFunctorContractive (sumCF F1 F2).
-Proof.
-  intros ?? A1 A2 B1 B2 n ???;
-    by apply sumC_map_ne; apply cFunctor_contractive.
-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 0.
-  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 n). omega.
-  Qed.
-End discrete_cofe.
-
-Notation discreteC A := (CofeT A discrete_cofe_mixin).
-Notation leibnizC A := (CofeT A (@discrete_cofe_mixin _ equivL _)).
-
-Instance discrete_discrete_cofe `{Equiv A, @Equivalence A (≡)} :
-  Discrete (discreteC A).
-Proof. by intros x y. Qed.
-Instance leibnizC_leibniz A : LeibnizEquiv (leibnizC A).
-Proof. by intros x y. Qed.
-
-Canonical Structure natC := leibnizC nat.
-Canonical Structure boolC := leibnizC bool.
-
-(* Option *)
-Section option.
-  Context {A : cofeT}.
-
-  Instance option_dist : Dist (option A) := λ n, option_Forall2 (dist n).
-  Lemma dist_option_Forall2 n mx my : mx ≡{n}≡ my ↔ option_Forall2 (dist n) mx my.
-  Proof. done. Qed.
-
-  Program Definition option_chain (c : chain (option A)) (x : A) : chain A :=
-    {| chain_car n := from_option id x (c n) |}.
-  Next Obligation. intros c x n i ?; simpl. by destruct (chain_cauchy c n i). Qed.
-  Instance option_compl : Compl (option A) := λ c,
-    match c 0 with Some x => Some (compl (option_chain c x)) | None => None end.
-
-  Definition option_cofe_mixin : CofeMixin (option A).
-  Proof.
-    split.
-    - intros mx my; split; [by destruct 1; constructor; apply equiv_dist|].
-      intros Hxy; destruct (Hxy 0); constructor; apply equiv_dist.
-      by intros n; feed inversion (Hxy n).
-    - apply _.
-    - destruct 1; constructor; by apply dist_S.
-    - intros n c; rewrite /compl /option_compl.
-      feed inversion (chain_cauchy c 0 n); first auto with lia; constructor.
-      rewrite (conv_compl n (option_chain c _)) /=. destruct (c n); naive_solver.
-  Qed.
-  Canonical Structure optionC := CofeT (option A) option_cofe_mixin.
-  Global Instance option_discrete : Discrete A → Discrete optionC.
-  Proof. destruct 2; constructor; by apply (timeless _). Qed.
-
-  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. destruct 1; split; eauto. Qed.
-  Global Instance Some_dist_inj : Inj (dist n) (dist n) (@Some A).
-  Proof. by inversion_clear 1. Qed.
-  Global Instance from_option_ne {B} (R : relation B) (f : A → B) n :
-    Proper (dist n ==> R) f → Proper (R ==> dist n ==> R) (from_option f).
-  Proof. destruct 3; simpl; auto. 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.
-
-  Lemma dist_None n mx : mx ≡{n}≡ None ↔ mx = None.
-  Proof. split; [by inversion_clear 1|by intros ->]. Qed.
-  Lemma dist_Some_inv_l n mx my x :
-    mx ≡{n}≡ my → mx = Some x → ∃ y, my = Some y ∧ x ≡{n}≡ y.
-  Proof. destruct 1; naive_solver. Qed.
-  Lemma dist_Some_inv_r n mx my y :
-    mx ≡{n}≡ my → my = Some y → ∃ x, mx = Some x ∧ x ≡{n}≡ y.
-  Proof. destruct 1; naive_solver. Qed.
-  Lemma dist_Some_inv_l' n my x : Some x ≡{n}≡ my → ∃ x', Some x' = my ∧ x ≡{n}≡ x'.
-  Proof. intros ?%(dist_Some_inv_l _ _ _ x); naive_solver. Qed.
-  Lemma dist_Some_inv_r' n mx y : mx ≡{n}≡ Some y → ∃ y', mx = Some y' ∧ y ≡{n}≡ y'.
-  Proof. intros ?%(dist_Some_inv_r _ _ _ y); naive_solver. Qed.
-End option.
-
-Typeclasses Opaque option_dist.
-Arguments optionC : clear implicits.
-
-Instance option_fmap_ne {A B : cofeT} n:
-  Proper ((dist n ==> dist n) ==> dist n ==> dist n) (@fmap option _ A B).
-Proof. intros f f' Hf ?? []; constructor; auto. 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 optionCF (F : cFunctor) : cFunctor := {|
-  cFunctor_car A B := optionC (cFunctor_car F A B);
-  cFunctor_map A1 A2 B1 B2 fg := optionC_map (cFunctor_map F fg)
-|}.
-Next Obligation.
-  by intros F A1 A2 B1 B2 n f g Hfg; apply optionC_map_ne, cFunctor_ne.
-Qed.
-Next Obligation.
-  intros F A B x. rewrite /= -{2}(option_fmap_id x).
-  apply option_fmap_setoid_ext=>y; apply cFunctor_id.
-Qed.
-Next Obligation.
-  intros F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -option_fmap_compose.
-  apply option_fmap_setoid_ext=>y; apply cFunctor_compose.
-Qed.
-
-Instance optionCF_contractive F :
-  cFunctorContractive F → cFunctorContractive (optionCF F).
-Proof.
-  by intros ? A1 A2 B1 B2 n f g Hfg; apply optionC_map_ne, cFunctor_contractive.
-Qed.
-
-(** 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] ??; trans 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 A) 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.
-Lemma later_map_ext {A B : cofeT} (f g : A → B) x :
-  (∀ x, f x ≡ g x) → later_map f x ≡ later_map g x.
-Proof. destruct x; intros Hf; apply Hf. 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.
-
-Program Definition laterCF (F : cFunctor) : cFunctor := {|
-  cFunctor_car A B := laterC (cFunctor_car F A B);
-  cFunctor_map A1 A2 B1 B2 fg := laterC_map (cFunctor_map F fg)
-|}.
-Next Obligation.
-  intros F A1 A2 B1 B2 n fg fg' ?.
-  by apply (contractive_ne laterC_map), cFunctor_ne.
-Qed.
-Next Obligation.
-  intros F A B x; simpl. rewrite -{2}(later_map_id x).
-  apply later_map_ext=>y. by rewrite cFunctor_id.
-Qed.
-Next Obligation.
-  intros F A1 A2 A3 B1 B2 B3 f g f' g' x; simpl. rewrite -later_map_compose.
-  apply later_map_ext=>y; apply cFunctor_compose.
-Qed.
-
-Instance laterCF_contractive F : cFunctorContractive (laterCF F).
-Proof.
-  intros A1 A2 B1 B2 n fg fg' Hfg.
-  apply laterC_map_contractive => i ?. by apply cFunctor_ne, Hfg.
-Qed.
-
-(** Notation for writing functors *)
-Notation "∙" := idCF : cFunctor_scope.
-Notation "F1 -n> F2" := (cofe_morCF F1%CF F2%CF) : cFunctor_scope.
-Notation "F1 * F2" := (prodCF F1%CF F2%CF) : cFunctor_scope.
-Notation "F1 + F2" := (sumCF F1%CF F2%CF) : cFunctor_scope.
-Notation "▶ F"  := (laterCF F%CF) (at level 20, right associativity) : cFunctor_scope.
-Coercion constCF : cofeT >-> cFunctor.

algebra/dec_agree.v

-From iris.algebra Require Export cmra.
-Local Arguments validN _ _ _ !_ /.
-Local Arguments valid _ _  !_ /.
-Local Arguments op _ _ _ !_ /.
-Local Arguments pcore _ _ !_ /.
-
-(* This is isomorphic to option, but has a very different RA structure. *)
-Inductive dec_agree (A : Type) : Type := 
-  | DecAgree : A → dec_agree A
-  | DecAgreeBot : dec_agree A.
-Arguments DecAgree {_} _.
-Arguments DecAgreeBot {_}.
-Instance maybe_DecAgree {A} : Maybe (@DecAgree A) := λ x,
-  match x with DecAgree a => Some a | _ => None end.
-
-Section dec_agree.
-Context {A : Type} `{∀ x y : A, Decision (x = y)}.
-
-Instance dec_agree_valid : Valid (dec_agree A) := λ x,
-  if x is DecAgree _ then True else False.
-Canonical Structure dec_agreeC : cofeT := leibnizC (dec_agree A).
-
-Instance dec_agree_op : Op (dec_agree A) := λ x y,
-  match x, y with
-  | DecAgree a, DecAgree b => if decide (a = b) then DecAgree a else DecAgreeBot
-  | _, _ => DecAgreeBot
-  end.
-Instance dec_agree_pcore : PCore (dec_agree A) := Some.
-
-Definition dec_agree_ra_mixin : RAMixin (dec_agree A).
-Proof.
-  split.
-  - apply _.
-  - intros x y cx ? [=<-]; eauto.
-  - apply _.
-  - intros [?|] [?|] [?|]; by repeat (simplify_eq/= || case_match).
-  - intros [?|] [?|]; by repeat (simplify_eq/= || case_match).
-  - intros [?|] ? [=<-]; by repeat (simplify_eq/= || case_match).
-  - intros [?|]; by repeat (simplify_eq/= || case_match).
-  - intros [?|] [?|] ?? [=<-]; eauto.
-  - by intros [?|] [?|] ?.
-Qed.
-
-Canonical Structure dec_agreeR : cmraT :=
-  discreteR (dec_agree A) dec_agree_ra_mixin.
-
-(* Some properties of this CMRA *)
-Global Instance dec_agree_persistent (x : dec_agreeR) : Persistent x.
-Proof. by constructor. Qed.
-
-Lemma dec_agree_ne a b : a ≠ b → DecAgree a ⋅ DecAgree b = DecAgreeBot.
-Proof. intros. by rewrite /= decide_False. Qed.
-
-Lemma dec_agree_idemp (x : dec_agree A) : x ⋅ x = x.
-Proof. destruct x; by rewrite /= ?decide_True. Qed.
-
-Lemma dec_agree_op_inv (x1 x2 : dec_agree A) : ✓ (x1 ⋅ x2) → x1 = x2.
-Proof. destruct x1, x2; by repeat (simplify_eq/= || case_match). Qed.
-End dec_agree.
-
-Arguments dec_agreeC : clear implicits.
-Arguments dec_agreeR _ {_}.

algebra/dra.v

-From iris.algebra Require Export cmra updates.
-
-Record DRAMixin A `{Equiv A, Core A, Disjoint A, Op A, Valid A} := {
-  (* setoids *)
-  mixin_dra_equivalence : Equivalence ((≡) : relation A);
-  mixin_dra_op_proper : Proper ((≡) ==> (≡) ==> (≡)) (⋅);
-  mixin_dra_core_proper : Proper ((≡) ==> (≡)) core;
-  mixin_dra_valid_proper : Proper ((≡) ==> impl) valid;
-  mixin_dra_disjoint_proper x : Proper ((≡) ==> impl) (disjoint x);
-  (* validity *)
-  mixin_dra_op_valid x y : ✓ x → ✓ y → x ⊥ y → ✓ (x ⋅ y);
-  mixin_dra_core_valid x : ✓ x → ✓ core x;
-  (* monoid *)
-  mixin_dra_assoc : Assoc (≡) (⋅);
-  mixin_dra_disjoint_ll x y z : ✓ x → ✓ y → ✓ z → x ⊥ y → x ⋅ y ⊥ z → x ⊥ z;
-  mixin_dra_disjoint_move_l x y z :
-    ✓ x → ✓ y → ✓ z → x ⊥ y → x ⋅ y ⊥ z → x ⊥ y ⋅ z;
-  mixin_dra_symmetric : Symmetric (@disjoint A _);
-  mixin_dra_comm x y : ✓ x → ✓ y → x ⊥ y → x ⋅ y ≡ y ⋅ x;
-  mixin_dra_core_disjoint_l x : ✓ x → core x ⊥ x;
-  mixin_dra_core_l x : ✓ x → core x ⋅ x ≡ x;
-  mixin_dra_core_idemp x : ✓ x → core (core x) ≡ core x;
-  mixin_dra_core_preserving x y : 
-    ∃ z, ✓ x → ✓ y → x ⊥ y → core (x ⋅ y) ≡ core x ⋅ z ∧ ✓ z ∧ core x ⊥ z
-}.
-Structure draT := DRAT {
-  dra_car :> Type;
-  dra_equiv : Equiv dra_car;
-  dra_core : Core dra_car;
-  dra_disjoint : Disjoint dra_car;
-  dra_op : Op dra_car;
-  dra_valid : Valid dra_car;
-  dra_mixin : DRAMixin dra_car
-}.
-Arguments DRAT _ {_ _ _ _ _} _.
-Arguments dra_car : simpl never.
-Arguments dra_equiv : simpl never.
-Arguments dra_core : simpl never.
-Arguments dra_disjoint : simpl never.
-Arguments dra_op : simpl never.
-Arguments dra_valid : simpl never.
-Arguments dra_mixin : simpl never.
-Add Printing Constructor draT.
-Existing Instances dra_equiv dra_core dra_disjoint dra_op dra_valid.
-
-(** Lifting properties from the mixin *)
-Section dra_mixin.
-  Context {A : draT}.
-  Implicit Types x y : A.
-  Global Instance dra_equivalence : Equivalence ((≡) : relation A).
-  Proof. apply (mixin_dra_equivalence _ (dra_mixin A)). Qed.
-  Global Instance dra_op_proper : Proper ((≡) ==> (≡) ==> (≡)) (@op A _).
-  Proof. apply (mixin_dra_op_proper _ (dra_mixin A)). Qed.
-  Global Instance dra_core_proper : Proper ((≡) ==> (≡)) (@core A _).
-  Proof. apply (mixin_dra_core_proper _ (dra_mixin A)). Qed.
-  Global Instance dra_valid_proper : Proper ((≡) ==> impl) (@valid A _).
-  Proof. apply (mixin_dra_valid_proper _ (dra_mixin A)). Qed.
-  Global Instance dra_disjoint_proper x : Proper ((≡) ==> impl) (disjoint x).
-  Proof. apply (mixin_dra_disjoint_proper _ (dra_mixin A)). Qed.
-  Lemma dra_op_valid x y : ✓ x → ✓ y → x ⊥ y → ✓ (x ⋅ y).
-  Proof. apply (mixin_dra_op_valid _ (dra_mixin A)). Qed.
-  Lemma dra_core_valid x : ✓ x → ✓ core x.
-  Proof. apply (mixin_dra_core_valid _ (dra_mixin A)). Qed.
-  Global Instance dra_assoc : Assoc (≡) (@op A _).
-  Proof. apply (mixin_dra_assoc _ (dra_mixin A)). Qed.
-  Lemma dra_disjoint_ll x y z : ✓ x → ✓ y → ✓ z → x ⊥ y → x ⋅ y ⊥ z → x ⊥ z.
-  Proof. apply (mixin_dra_disjoint_ll _ (dra_mixin A)). Qed.
-  Lemma dra_disjoint_move_l x y z :
-    ✓ x → ✓ y → ✓ z → x ⊥ y → x ⋅ y ⊥ z → x ⊥ y ⋅ z.
-  Proof. apply (mixin_dra_disjoint_move_l _ (dra_mixin A)). Qed.
-  Global Instance  dra_symmetric : Symmetric (@disjoint A _).
-  Proof. apply (mixin_dra_symmetric _ (dra_mixin A)). Qed.
-  Lemma dra_comm x y : ✓ x → ✓ y → x ⊥ y → x ⋅ y ≡ y ⋅ x.
-  Proof. apply (mixin_dra_comm _ (dra_mixin A)). Qed.
-  Lemma dra_core_disjoint_l x : ✓ x → core x ⊥ x.
-  Proof. apply (mixin_dra_core_disjoint_l _ (dra_mixin A)). Qed.
-  Lemma dra_core_l x : ✓ x → core x ⋅ x ≡ x.
-  Proof. apply (mixin_dra_core_l _ (dra_mixin A)). Qed.
-  Lemma dra_core_idemp x : ✓ x → core (core x) ≡ core x.
-  Proof. apply (mixin_dra_core_idemp _ (dra_mixin A)). Qed.
-  Lemma dra_core_preserving x y : 
-    ∃ z, ✓ x → ✓ y → x ⊥ y → core (x ⋅ y) ≡ core x ⋅ z ∧ ✓ z ∧ core x ⊥ z.
-  Proof. apply (mixin_dra_core_preserving _ (dra_mixin A)). Qed.
-End dra_mixin.
-
-Record validity (A : draT) := Validity {
-  validity_car : A;
-  validity_is_valid : Prop;
-  validity_prf : validity_is_valid → valid validity_car
-}.
-Add Printing Constructor validity.
-Arguments Validity {_} _ _ _.
-Arguments validity_car {_} _.
-Arguments validity_is_valid {_} _.
-
-Definition to_validity {A : draT} (x : A) : validity A :=
-  Validity x (valid x) id.
-
-(* The actual construction *)
-Section dra.
-Context (A : draT).
-Implicit Types a b : A.
-Implicit Types x y z : validity A.
-Arguments valid _ _ !_ /.
-
-Instance validity_valid : Valid (validity A) := validity_is_valid.
-Instance validity_equiv : Equiv (validity A) := λ x y,
-  (valid x ↔ valid y) ∧ (valid x → validity_car x ≡ validity_car y).
-Instance validity_equivalence : Equivalence (@equiv (validity A) _).
-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; trans y]; tauto.
-Qed.
-Canonical Structure validityC : cofeT := discreteC (validity A).
-
-Instance dra_valid_proper' : Proper ((≡) ==> iff) (valid : A → Prop).
-Proof. by split; apply: dra_valid_proper. Qed.
-Global Instance to_validity_proper : Proper ((≡) ==> (≡)) to_validity.
-Proof. by intros x1 x2 Hx; split; rewrite /= Hx. Qed.
-Instance: Proper ((≡) ==> (≡) ==> iff) (disjoint : relation A).
-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 a b c : ✓ a → ✓ b → ✓ c → b ⊥ c → a ⊥ b ⋅ c → a ⊥ b.
-Proof. intros ???. rewrite !(symmetry_iff _ a). by apply dra_disjoint_ll. Qed.
-Lemma dra_disjoint_lr a b c : ✓ a → ✓ b → ✓ c → a ⊥ b → a ⋅ b ⊥ c → b ⊥ c.
-Proof. intros ????. rewrite dra_comm //. by apply dra_disjoint_ll. Qed.
-Lemma dra_disjoint_move_r a b c :
-  ✓ a → ✓ b → ✓ c → b ⊥ c → a ⊥ b ⋅ c → a ⋅ b ⊥ c.
-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.
-
-Lemma validity_valid_car_valid z : ✓ z → ✓ validity_car z.
-Proof. apply validity_prf. Qed.
-Hint Resolve validity_valid_car_valid.
-Program Instance validity_pcore : PCore (validity A) := λ x,
-  Some (Validity (core (validity_car x)) (✓ x) _).
-Solve Obligations with naive_solver eauto using dra_core_valid.
-Program Instance validity_op : Op (validity A) := λ x y,
-  Validity (validity_car x ⋅ validity_car y)
-           (✓ x ∧ ✓ y ∧ validity_car x ⊥ validity_car y) _.
-Solve Obligations with naive_solver eauto using dra_op_valid.
-
-Definition validity_ra_mixin : RAMixin (validity A).
-Proof.
-  apply ra_total_mixin; first eauto.
-  - 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 [x px ?] [y py ?] [z pz ?]; split; simpl;
-      [intuition eauto 2 using dra_disjoint_lr, dra_disjoint_rl
-      |intros; by rewrite assoc].
-  - intros [x px ?] [y py ?]; split; naive_solver eauto using dra_comm.
-  - intros [x px ?]; split;
-      naive_solver eauto using dra_core_l, dra_core_disjoint_l.
-  - intros [x px ?]; split; naive_solver eauto using dra_core_idemp.
-  - intros [x px ?] [y py ?] [[z pz ?] [? Hy]]; simpl in *.
-    destruct (dra_core_preserving x z) as (z'&Hz').
-    unshelve eexists (Validity z' (px ∧ py ∧ pz) _); [|split; simpl].
-    { intros (?&?&?); apply Hz'; tauto. }
-    + tauto.
-    + intros. rewrite Hy //. tauto.
-  - by intros [x px ?] [y py ?] (?&?&?).
-Qed.
-Canonical Structure validityR : cmraT :=
-  discreteR (validity A) validity_ra_mixin.
-
-Global Instance validity_cmra_total : CMRATotal validityR.
-Proof. rewrite /CMRATotal; eauto. Qed.
-
-Lemma validity_update x y :
-  (∀ c, ✓ x → ✓ c → validity_car x ⊥ c → ✓ y ∧ validity_car y ⊥ c) → x ~~> y.
-Proof.
-  intros Hxy; apply cmra_discrete_update=> z [?[??]].
-  split_and!; try eapply Hxy; eauto.
-Qed.
-
-Lemma to_validity_op a b :
-  (✓ (a ⋅ b) → ✓ a ∧ ✓ b ∧ a ⊥ b) →
-  to_validity (a ⋅ b) ≡ to_validity a ⋅ to_validity b.
-Proof. split; naive_solver eauto using dra_op_valid. Qed.
-
-(* TODO: This has to be proven again. *)
-(*
-Lemma to_validity_included x y:
-  (✓ y ∧ to_validity x ≼ to_validity y)%C ↔ (✓ x ∧ x ≼ y).
-Proof.
-  split.
-  - move=>[Hvl [z [Hvxz EQ]]]. move:(Hvl)=>Hvl'. apply Hvxz in Hvl'.
-    destruct Hvl' as [? [? ?]]; split; first done.
-    exists (validity_car z); eauto.
-  - intros (Hvl & z & EQ & ? & ?).
-    assert (✓ y) by (rewrite EQ; by apply dra_op_valid).
-    split; first done. exists (to_validity z). split; first split.
-    + intros _. simpl. by split_and!.
-    + intros _. setoid_subst. by apply dra_op_valid. 
-    + intros _. rewrite /= EQ //.
-Qed.
-*)
-End dra.

algebra/frac.v

-From Coq.QArith Require Import Qcanon.
-From iris.algebra Require Export cmra.
-From iris.algebra Require Import upred.
-
-Notation frac := Qp (only parsing).
-
-Section frac.
-Canonical Structure fracC := leibnizC frac.
-
-Instance frac_valid : Valid frac := λ x, (x ≤ 1)%Qc.
-Instance frac_pcore : PCore frac := λ _, None.
-Instance frac_op : Op frac := λ x y, (x + y)%Qp.
-
-Definition frac_ra_mixin : RAMixin frac.
-Proof.
-  split; try apply _; try done.
-  unfold valid, op, frac_op, frac_valid. intros x y. trans (x+y)%Qp; last done.
-  rewrite -{1}(Qcplus_0_r x) -Qcplus_le_mono_l; auto using Qclt_le_weak.
-Qed.
-Canonical Structure fracR := discreteR frac frac_ra_mixin.
-End frac.
-
-(** Internalized properties *)
-Lemma frac_equivI {M} (x y : frac) : x ≡ y ⊣⊢ (x = y : uPred M).
-Proof. by uPred.unseal. Qed.
-Lemma frac_validI {M} (x : frac) : ✓ x ⊣⊢ (■ (x ≤ 1)%Qc : uPred M).
-Proof. by uPred.unseal. Qed.
-
-(** Exclusive *)
-Global Instance frac_full_exclusive : Exclusive 1%Qp.
-Proof.
-  move=> y /Qcle_not_lt [] /=. by rewrite -{1}(Qcplus_0_r 1) -Qcplus_lt_mono_l.
-Qed.

algebra/gmap.v

-From iris.algebra Require Export cmra updates.
-From iris.prelude Require Export gmap.
-From iris.algebra Require Import upred.
-
-Section cofe.
-Context `{Countable K} {A : cofeT}.
-Implicit Types m : gmap K A.
-
-Instance gmap_dist : Dist (gmap K A) := λ n m1 m2,
-  ∀ i, m1 !! i ≡{n}≡ m2 !! i.
-Program Definition gmap_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 gmap_compl : Compl (gmap K A) := λ c,
-  map_imap (λ i _, compl (gmap_chain c i)) (c 0).
-Definition gmap_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; trans (m2 !! k).
-  - by intros n m1 m2 ? k; apply dist_S.
-  - intros n c k; rewrite /compl /gmap_compl lookup_imap.
-    feed inversion (λ H, chain_cauchy c 0 n H k); simpl; auto with lia.
-    by rewrite conv_compl /=; apply reflexive_eq.
-Qed.
-Canonical Structure gmapC : cofeT := CofeT (gmap K A) gmap_cofe_mixin.
-Global Instance gmap_discrete : Discrete A → Discrete gmapC.
-Proof. intros ? m m' ? i. by apply (timeless _). Qed.
-(* why doesn't this go automatic? *)
-Global Instance gmapC_leibniz: LeibnizEquiv A → LeibnizEquiv gmapC.
-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.
-
-Instance gmap_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 gmap_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 gmap_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 gmap_singleton_timeless i x :
-  Timeless x → Timeless ({[ i := x ]} : gmap K A) := _.
-End cofe.
-
-Arguments gmapC _ {_ _} _.
-
-(* CMRA *)
-Section cmra.
-Context `{Countable K} {A : cmraT}.
-Implicit Types m : gmap K A.
-
-Instance gmap_op : Op (gmap K A) := merge op.
-Instance gmap_pcore : PCore (gmap K A) := λ m, Some (omap pcore m).
-Instance gmap_valid : Valid (gmap K A) := λ m, ∀ i, ✓ (m !! i).
-Instance gmap_validN : ValidN (gmap K A) := λ n m, ∀ i, ✓{n} (m !! i).
-
-Lemma lookup_op m1 m2 i : (m1 ⋅ m2) !! i = m1 !! i ⋅ m2 !! i.
-Proof. by apply lookup_merge. Qed.
-Lemma lookup_core m i : core m !! i = core (m !! i).
-Proof. by apply lookup_omap. Qed.
-
-Lemma lookup_included (m1 m2 : gmap K A) : m1 ≼ m2 ↔ ∀ i, m1 !! i ≼ m2 !! i.
-Proof.
-  split; [by intros [m Hm] i; exists (m !! i); rewrite -lookup_op Hm|].
-  revert m2. induction m1 as [|i x m Hi IH] using map_ind=> m2 Hm.
-  { exists m2. by rewrite left_id. }
-  destruct (IH (delete i m2)) as [m2' Hm2'].
-  { intros j. move: (Hm j); destruct (decide (i = j)) as [->|].
-    - intros _. rewrite Hi. apply: ucmra_unit_least.
-    - rewrite lookup_insert_ne // lookup_delete_ne //. }
-  destruct (Hm i) as [my Hi']; simplify_map_eq.
-  exists (partial_alter (λ _, my) i m2')=>j; destruct (decide (i = j)) as [->|].
-  - by rewrite Hi' lookup_op lookup_insert lookup_partial_alter.
-  - move: (Hm2' j). by rewrite !lookup_op lookup_delete_ne //
-      lookup_insert_ne // lookup_partial_alter_ne.
-Qed.
-
-Lemma gmap_cmra_mixin : CMRAMixin (gmap K A).
-Proof.
-  apply cmra_total_mixin.
-  - eauto.
-  - intros n m1 m2 m3 Hm i; by rewrite !lookup_op (Hm i).
-  - intros n m1 m2 Hm i; by rewrite !lookup_core (Hm i).
-  - intros n m1 m2 Hm ? i; by rewrite -(Hm i).
-  - intros m; split.
-    + by intros ? n i; apply cmra_valid_validN.
-    + intros Hm i; apply cmra_valid_validN=> n; apply Hm.
-  - 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.
-  - intros m i. by rewrite lookup_op lookup_core cmra_core_l.
-  - intros m i. by rewrite !lookup_core cmra_core_idemp.
-  - intros m1 m2; rewrite !lookup_included=> Hm i.
-    rewrite !lookup_core. by apply cmra_core_preserving.
-  - intros n m1 m2 Hm i; apply cmra_validN_op_l with (m2 !! i).
-    by rewrite -lookup_op.
-  - 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 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))|].
-      move: (Hm12' i). rewrite Hx -!timeless_iff.
-      rewrite !(symmetry_iff _ None) !equiv_None op_None; tauto.
-    + destruct (m !! i) as [x|] eqn:Hx; simpl; [apply (proj2_sig (f i))|].
-      move: (Hm12' i). rewrite Hx -!timeless_iff.
-      rewrite !(symmetry_iff _ None) !equiv_None op_None; tauto.
-Qed.
-Canonical Structure gmapR :=
-  CMRAT (gmap K A) gmap_cofe_mixin gmap_cmra_mixin.
-
-Global Instance gmap_cmra_discrete : CMRADiscrete A → CMRADiscrete gmapR.
-Proof. split; [apply _|]. intros m ? i. by apply: cmra_discrete_valid. Qed.
-
-Lemma gmap_ucmra_mixin : UCMRAMixin (gmap K A).
-Proof.
-  split.
-  - by intros i; rewrite lookup_empty.
-  - by intros m i; rewrite /= lookup_op lookup_empty (left_id_L None _).
-  - apply gmap_empty_timeless.
-  - constructor=> i. by rewrite lookup_omap lookup_empty.
-Qed.
-Canonical Structure gmapUR :=
-  UCMRAT (gmap K A) gmap_cofe_mixin gmap_cmra_mixin gmap_ucmra_mixin.
-
-(** Internalized properties *)
-Lemma gmap_equivI {M} m1 m2 : m1 ≡ m2 ⊣⊢ (∀ i, m1 !! i ≡ m2 !! i : uPred M).
-Proof. by uPred.unseal. Qed.
-Lemma gmap_validI {M} m : ✓ m ⊣⊢ (∀ i, ✓ (m !! i) : uPred M).
-Proof. by uPred.unseal. Qed.
-End cmra.
-
-Arguments gmapR _ {_ _} _.
-Arguments gmapUR _ {_ _} _.
-
-Section properties.
-Context `{Countable K} {A : cmraT}.
-Implicit Types m : gmap K A.
-Implicit Types i : K.
-Implicit Types x y : A.
-
-Lemma lookup_opM m1 mm2 i : (m1 ⋅? mm2) !! i = m1 !! i ⋅ (mm2 ≫= (!! i)).
-Proof. destruct mm2; by rewrite /= ?lookup_op ?right_id_L. Qed.
-
-Lemma lookup_validN_Some 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 lookup_valid_Some m i x : ✓ m → m !! i ≡ Some x → ✓ x.
-Proof. move=> Hm Hi. move:(Hm i). by rewrite Hi. Qed.
-Lemma 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 insert_valid m i x : ✓ x → ✓ m → ✓ <[i:=x]>m.
-Proof. by intros ?? j; destruct (decide (i = j)); simplify_map_eq. Qed.
-Lemma singleton_validN n i x : ✓{n} ({[ i := x ]} : gmap K A) ↔ ✓{n} x.
-Proof.
-  split; [|by intros; apply insert_validN, ucmra_unit_validN].
-  by move=>/(_ i); simplify_map_eq.
-Qed.
-Lemma singleton_valid i x : ✓ ({[ i := x ]} : gmap K A) ↔ ✓ x.
-Proof. rewrite !cmra_valid_validN. by setoid_rewrite singleton_validN. Qed.
-
-Lemma insert_singleton_opN n m i x :
-  m !! i = None → <[i:=x]> m ≡{n}≡ {[ i := x ]} ⋅ m.
-Proof.
-  intros Hi j; destruct (decide (i = j)) as [->|].
-  - by rewrite lookup_op lookup_insert lookup_singleton Hi right_id.
-  - by rewrite lookup_op lookup_insert_ne // lookup_singleton_ne // left_id.
-Qed.
-Lemma insert_singleton_op m i x : m !! i = None → <[i:=x]> m ≡ {[ i := x ]} ⋅ m.
-Proof. rewrite !equiv_dist; naive_solver eauto using insert_singleton_opN. Qed.
-
-Lemma core_singleton (i : K) (x : A) cx :
-  pcore x = Some cx → core ({[ i := x ]} : gmap K A) = {[ i := cx ]}.
-Proof. apply omap_singleton. Qed.
-Lemma core_singleton' (i : K) (x : A) cx :
-  pcore x ≡ Some cx → core ({[ i := x ]} : gmap K A) ≡ {[ i := cx ]}.
-Proof.
-  intros (cx'&?&->)%equiv_Some_inv_r'. by rewrite (core_singleton _ _ cx').
-Qed.
-Lemma 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.
-
-Global Instance gmap_persistent m : (∀ x : A, Persistent x) → Persistent m.
-Proof.
-  intros; apply persistent_total=> i.
-  rewrite lookup_core. apply (persistent_core _).
-Qed.
-Global Instance gmap_singleton_persistent i (x : A) :
-  Persistent x → Persistent {[ i := x ]}.
-Proof. intros. by apply persistent_total, core_singleton'. Qed.
-
-Lemma singleton_includedN n m i x :
-  {[ i := x ]} ≼{n} m ↔ ∃ y, m !! i ≡{n}≡ Some y ∧ (x ≼{n} y ∨ x ≡{n}≡ y).
-Proof.
-  split.
-  - move=> [m' /(_ i)]; rewrite lookup_op lookup_singleton.
-    case (m' !! i)=> [y|]=> Hm.
-    + exists (x ⋅ y); eauto using cmra_includedN_l.
-    + exists x; eauto.
-  - intros (y&Hi&[[z ?]| ->]).
-    + exists (<[i:=z]>m)=> j; destruct (decide (i = j)) as [->|].
-      * rewrite Hi lookup_op lookup_singleton lookup_insert. by constructor.
-      * by rewrite lookup_op lookup_singleton_ne // lookup_insert_ne // left_id.
-    + exists (delete i m)=> j; destruct (decide (i = j)) as [->|].
-      * by rewrite Hi lookup_op lookup_singleton lookup_delete.
-      * by rewrite lookup_op lookup_singleton_ne // lookup_delete_ne // left_id.
-Qed.
-Lemma 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 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; apply cmra_total_updateP=> n mf Hm.
-  destruct (Hx n (Some (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 insert_updateP' (P : A → Prop) m i x :
-  x ~~>: P → <[i:=x]>m ~~>: λ m', ∃ y, m' = <[i:=y]>m ∧ P y.
-Proof. eauto using insert_updateP. Qed.
-Lemma insert_update m i x y : x ~~> y → <[i:=x]>m ~~> <[i:=y]>m.
-Proof. rewrite !cmra_update_updateP; eauto using insert_updateP with subst. Qed.
-
-Lemma 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 insert_updateP. Qed.
-Lemma singleton_updateP' (P : A → Prop) i x :
-  x ~~>: P → {[ i := x ]} ~~>: λ m, ∃ y, m = {[ i := y ]} ∧ P y.
-Proof. apply insert_updateP'. Qed.
-Lemma singleton_update i (x y : A) : x ~~> y → {[ i := x ]} ~~> {[ i := y ]}.
-Proof. apply insert_update. Qed.
-
-Lemma delete_update m i : m ~~> delete i m.
-Proof.
-  apply cmra_total_update=> n mf Hm j; destruct (decide (i = j)); subst.
-  - move: (Hm j). rewrite !lookup_op lookup_delete left_id.
-    apply cmra_validN_op_r.
-  - move: (Hm j). by rewrite !lookup_op lookup_delete_ne.
-Qed.
-
-Section freshness.
-  Context `{Fresh K (gset K), !FreshSpec K (gset K)}.
-  Lemma alloc_updateP_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. apply cmra_total_updateP.
-    intros 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 -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 insert_singleton_opN; last by apply not_elem_of_dom.
-    rewrite -assoc -insert_singleton_opN;
-      last by apply not_elem_of_dom; rewrite dom_op not_elem_of_union.
-    by apply insert_validN; [apply cmra_valid_validN|].
-  Qed.
-  Lemma alloc_updateP (Q : gmap K A → Prop) m x :
-    ✓ x → (∀ i, m !! i = None → Q (<[i:=x]>m)) → m ~~>: Q.
-  Proof. move=>??. eapply alloc_updateP_strong with (I:=∅); by eauto. Qed.
-  Lemma alloc_updateP_strong' m x (I : gset K) :
-    ✓ x → m ~~>: λ m', ∃ i, i ∉ I ∧ m' = <[i:=x]>m ∧ m !! i = None.
-  Proof. eauto using alloc_updateP_strong. Qed.
-  Lemma alloc_updateP' m x :
-    ✓ x → m ~~>: λ m', ∃ i, m' = <[i:=x]>m ∧ m !! i = None.
-  Proof. eauto using alloc_updateP. Qed.
-
-  Lemma alloc_unit_singleton_updateP (P : A → Prop) (Q : gmap K A → Prop) u i :
-    ✓ u → LeftId (≡) u (⋅) →
-    u ~~>: P → (∀ y, P y → Q {[ i := y ]}) → ∅ ~~>: Q.
-  Proof.
-    intros ?? Hx HQ. apply cmra_total_updateP=> n gf Hg.
-    destruct (Hx n (gf !! i)) as (y&?&Hy).
-    { move:(Hg i). rewrite !left_id.
-      case: (gf !! i)=>[x|]; rewrite /= ?left_id //.
-      intros; by apply cmra_valid_validN. }
-    exists {[ i := y ]}; split; first by auto.
-    intros i'; destruct (decide (i' = i)) as [->|].
-    - rewrite lookup_op lookup_singleton.
-      move:Hy; case: (gf !! i)=>[x|]; rewrite /= ?right_id //.
-    - move:(Hg i'). by rewrite !lookup_op lookup_singleton_ne // !left_id.
-  Qed.
-  Lemma alloc_unit_singleton_updateP' (P: A → Prop) u i :
-    ✓ u → LeftId (≡) u (⋅) →
-    u ~~>: P → ∅ ~~>: λ m, ∃ y, m = {[ i := y ]} ∧ P y.
-  Proof. eauto using alloc_unit_singleton_updateP. Qed.
-  Lemma alloc_unit_singleton_update u i (y : A) :
-    ✓ u → LeftId (≡) u (⋅) → u ~~> y → ∅ ~~> {[ i := y ]}.
-  Proof.
-    rewrite !cmra_update_updateP;
-      eauto using alloc_unit_singleton_updateP with subst.
-  Qed.
-End freshness.
-
-Lemma insert_local_update m i x y mf :
-  x ~l~> y @ mf ≫= (!! i) → <[i:=x]>m ~l~> <[i:=y]>m @ mf.
-Proof.
-  intros [Hxy Hxy']; split.
-  - intros n Hm j. move: (Hm j). destruct (decide (i = j)); subst.
-    + rewrite !lookup_opM !lookup_insert !Some_op_opM. apply Hxy.
-    + by rewrite !lookup_opM !lookup_insert_ne.
-  - intros n mf' Hm Hm' j. move: (Hm j) (Hm' j).
-    destruct (decide (i = j)); subst.
-    + rewrite !lookup_opM !lookup_insert !Some_op_opM !inj_iff. apply Hxy'.
-    + by rewrite !lookup_opM !lookup_insert_ne.
-Qed.
-
-Lemma singleton_local_update i x y mf :
-  x ~l~> y @ mf ≫= (!! i) → {[ i := x ]} ~l~> {[ i := y ]} @ mf.
-Proof. apply insert_local_update. Qed.
-
-Lemma alloc_singleton_local_update m i x mf :
-  (m ⋅? mf) !! i = None → ✓ x → m ~l~> <[i:=x]> m @ mf.
-Proof.
-  rewrite lookup_opM op_None=> -[Hi Hif] ?.
-  rewrite insert_singleton_op // comm. apply alloc_local_update.
-  intros n Hm j. move: (Hm j). destruct (decide (i = j)); subst.
-  - intros _; rewrite !lookup_opM lookup_op !lookup_singleton Hif Hi.
-    by apply cmra_valid_validN.
-  - by rewrite !lookup_opM lookup_op !lookup_singleton_ne // right_id.
-Qed.
-
-Lemma alloc_unit_singleton_local_update i x mf :
-  mf ≫= (!! i) = None → ✓ x → ∅ ~l~> {[ i := x ]} @ mf.
-Proof.
-  intros Hi; apply alloc_singleton_local_update. by rewrite lookup_opM Hi.
-Qed.
-
-Lemma delete_local_update m i x `{!Exclusive x} mf :
-  m !! i = Some x → m ~l~> delete i m @ mf.
-Proof.
-  intros Hx; split; [intros n; apply delete_update|].
-  intros n mf' Hm Hm' j. move: (Hm j) (Hm' j).
-  destruct (decide (i = j)); subst.
-  + rewrite !lookup_opM !lookup_delete Hx=> ? Hj.
-    rewrite (exclusiveN_Some_l n x (mf ≫= lookup j)) //.
-    by rewrite (exclusiveN_Some_l n x (mf' ≫= lookup j)) -?Hj.
-  + by rewrite !lookup_opM !lookup_delete_ne.
-Qed.
-End properties.
-
-(** Functor *)
-Instance gmap_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 gmap_fmap_cmra_monotone `{Countable K} {A B : cmraT} (f : A → B)
-  `{!CMRAMonotone f} : CMRAMonotone (fmap f : gmap K A → gmap K B).
-Proof.
-  split; try apply _.
-  - by intros n m ? i; rewrite lookup_fmap; apply (validN_preserving _).
-  - intros m1 m2; rewrite !lookup_included=> Hm i.
-    by rewrite !lookup_fmap; apply: included_preserving.
-Qed.
-Definition gmapC_map `{Countable K} {A B} (f: A -n> B) :
-  gmapC K A -n> gmapC K B := CofeMor (fmap f : gmapC K A → gmapC K B).
-Instance gmapC_map_ne `{Countable K} {A B} n :
-  Proper (dist n ==> dist n) (@gmapC_map K _ _ A B).
-Proof.
-  intros f g Hf m k; rewrite /= !lookup_fmap.
-  destruct (_ !! k) eqn:?; simpl; constructor; apply Hf.
-Qed.
-
-Program Definition gmapCF K `{Countable K} (F : cFunctor) : cFunctor := {|
-  cFunctor_car A B := gmapC K (cFunctor_car F A B);
-  cFunctor_map A1 A2 B1 B2 fg := gmapC_map (cFunctor_map F fg)
-|}.
-Next Obligation.
-  by intros K ?? F A1 A2 B1 B2 n f g Hfg; apply gmapC_map_ne, cFunctor_ne.
-Qed.
-Next Obligation.
-  intros K ?? F A B x. rewrite /= -{2}(map_fmap_id x).
-  apply map_fmap_setoid_ext=>y ??; apply cFunctor_id.
-Qed.
-Next Obligation.
-  intros K ?? F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -map_fmap_compose.
-  apply map_fmap_setoid_ext=>y ??; apply cFunctor_compose.
-Qed.
-Instance gmapCF_contractive K `{Countable K} F :
-  cFunctorContractive F → cFunctorContractive (gmapCF K F).
-Proof.
-  by intros ? A1 A2 B1 B2 n f g Hfg; apply gmapC_map_ne, cFunctor_contractive.
-Qed.
-
-Program Definition gmapURF K `{Countable K} (F : rFunctor) : urFunctor := {|
-  urFunctor_car A B := gmapUR K (rFunctor_car F A B);
-  urFunctor_map A1 A2 B1 B2 fg := gmapC_map (rFunctor_map F fg)
-|}.
-Next Obligation.
-  by intros K ?? F A1 A2 B1 B2 n f g Hfg; apply gmapC_map_ne, rFunctor_ne.
-Qed.
-Next Obligation.
-  intros K ?? F A B x. rewrite /= -{2}(map_fmap_id x).
-  apply map_fmap_setoid_ext=>y ??; apply rFunctor_id.
-Qed.
-Next Obligation.
-  intros K ?? F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -map_fmap_compose.
-  apply map_fmap_setoid_ext=>y ??; apply rFunctor_compose.
-Qed.
-Instance gmapRF_contractive K `{Countable K} F :
-  rFunctorContractive F → urFunctorContractive (gmapURF K F).
-Proof.
-  by intros ? A1 A2 B1 B2 n f g Hfg; apply gmapC_map_ne, rFunctor_contractive.
-Qed.

algebra/gset.v

-From iris.algebra Require Export gmap.
-From iris.algebra Require Import excl.
-From iris.prelude Require Import mapset.
-
-Definition gsetC K `{Countable K} := gmapC K (exclC unitC).
-
-Definition to_gsetC `{Countable K} (X : gset K) : gsetC K :=
-  to_gmap (Excl ()) X.
-
-Section gset.
-Context `{Countable K}.
-Implicit Types X Y : gset K.
-
-Lemma to_gsetC_empty : to_gsetC (∅ : gset K) = ∅.
-Proof. apply to_gmap_empty. Qed.
-Lemma to_gsetC_union X Y : X ⊥ Y → to_gsetC X ⋅ to_gsetC Y = to_gsetC (X ∪ Y).
-Proof.
-  intros HXY; apply: map_eq=> i; rewrite /to_gsetC /=.
-  rewrite lookup_op !lookup_to_gmap. repeat case_option_guard; set_solver.
-Qed.
-Lemma to_gsetC_valid X : ✓ to_gsetC X.
-Proof. intros i. rewrite /to_gsetC lookup_to_gmap. by case_option_guard. Qed.
-Lemma to_gsetC_valid_op X Y : ✓ (to_gsetC X ⋅ to_gsetC Y) ↔ X ⊥ Y.
-Proof.
-  split; last (intros; rewrite to_gsetC_union //; apply to_gsetC_valid).
-  intros HXY i ??; move: (HXY i); rewrite lookup_op !lookup_to_gmap.
-  rewrite !option_guard_True //.
-Qed.
-
-Context `{Fresh K (gset K), !FreshSpec K (gset K)}.
-Lemma updateP_alloc_strong (Q : gsetC K → Prop) (I : gset K) X :
-  (∀ i, i ∉ X → i ∉ I → Q (to_gsetC ({[i]} ∪ X))) → to_gsetC X ~~>: Q.
-Proof.
-  intros; apply updateP_alloc_strong with I (Excl ()); [done|]=> i.
-  rewrite /to_gsetC lookup_to_gmap_None -to_gmap_union_singleton; eauto.
-Qed.
-Lemma updateP_alloc (Q : gsetC K → Prop) X :
-  (∀ i, i ∉ X → Q (to_gsetC ({[i]} ∪ X))) → to_gsetC X ~~>: Q.
-Proof. move=>??. eapply updateP_alloc_strong with (I:=∅); by eauto. Qed.
-Lemma updateP_alloc_strong' (I : gset K) X :
-  to_gsetC X ~~>: λ Y : gsetC K, ∃ i, Y = to_gsetC ({[ i ]} ∪ X) ∧ i ∉ I ∧ i ∉ X.
-Proof. eauto using updateP_alloc_strong. Qed.
-Lemma updateP_alloc' X :
-  to_gsetC X ~~>: λ Y : gsetC K, ∃ i, Y = to_gsetC ({[ i ]} ∪ X) ∧ i ∉ X.
-Proof. eauto using updateP_alloc. Qed.
-End gset.
\ No newline at end of file

algebra/iprod.v

-From iris.algebra Require Export cmra updates.
-From iris.algebra Require Import upred.
-From iris.prelude Require Import finite.
-
-(** * Indexed product *)
-(** Need to put this in a definition to make canonical structures to work. *)
-Definition iprod `{Finite A} (B : A → cofeT) := ∀ x, B x.
-Definition iprod_insert `{Finite A} {B : A → cofeT}
-    (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.
-Instance: Params (@iprod_insert) 5.
-
-Section iprod_cofe.
-  Context `{Finite 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; trans (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 B) iprod_cofe_mixin.
-
-  (** 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. }
-    apply (timeless _)=> x'; destruct (decide (x = x')) as [->|];
-      by 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.
-End iprod_cofe.
-
-Arguments iprodC {_ _ _} _.
-
-Section iprod_cmra.
-  Context `{Finite A} {B : A → ucmraT}.
-  Implicit Types f g : iprod B.
-
-  Instance iprod_op : Op (iprod B) := λ f g x, f x ⋅ g x.
-  Instance iprod_pcore : PCore (iprod B) := λ f, Some (λ x, core (f x)).
-  Instance iprod_valid : Valid (iprod B) := λ f, ∀ x, ✓ f x.
-  Instance iprod_validN : ValidN (iprod B) := λ n f, ∀ x, ✓{n} f x.
-
-  Definition iprod_lookup_op f g x : (f ⋅ g) x = f x ⋅ g x := eq_refl.
-  Definition iprod_lookup_core f x : (core f) x = core (f x) := eq_refl.
-
-  Lemma iprod_included_spec (f g : iprod B) : f ≼ g ↔ ∀ x, f x ≼ g x.
-  Proof.
-    split; [by intros [h Hh] x; exists (h x); rewrite /op /iprod_op (Hh x)|].
-    intros [h ?]%finite_choice. by exists h.
-  Qed.
-
-  Lemma iprod_cmra_mixin : CMRAMixin (iprod B).
-  Proof.
-    apply cmra_total_mixin.
-    - eauto.
-    - by intros n f1 f2 f3 Hf x; rewrite iprod_lookup_op (Hf x).
-    - by intros n f1 f2 Hf x; rewrite iprod_lookup_core (Hf x).
-    - by intros n f1 f2 Hf ? x; rewrite -(Hf x).
-    - intros g; split.
-      + intros Hg n i; apply cmra_valid_validN, Hg.
-      + intros Hg i; apply cmra_valid_validN=> n; apply Hg.
-    - 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_core cmra_core_l.
-    - by intros f x; rewrite iprod_lookup_core cmra_core_idemp.
-    - intros f1 f2; rewrite !iprod_included_spec=> Hf x.
-      by rewrite iprod_lookup_core; apply cmra_core_preserving, Hf.
-    - intros n f1 f2 Hf x; apply cmra_validN_op_l with (f2 x), Hf.
-    - intros n f f1 f2 Hf Hf12.
-      set (g x := cmra_extend 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 iprodR :=
-    CMRAT (iprod B) iprod_cofe_mixin iprod_cmra_mixin.
-
-  Instance iprod_empty : Empty (iprod B) := λ x, ∅.
-  Definition iprod_lookup_empty x : ∅ x = ∅ := eq_refl.
-
-  Lemma iprod_ucmra_mixin : UCMRAMixin (iprod B).
-  Proof.
-    split.
-    - intros x; apply ucmra_unit_valid.
-    - by intros f x; rewrite iprod_lookup_op left_id.
-    - intros f Hf x. by apply: timeless.
-    - constructor=> x. apply persistent_core, _.
-  Qed.
-  Canonical Structure iprodUR :=
-    UCMRAT (iprod B) iprod_cofe_mixin iprod_cmra_mixin iprod_ucmra_mixin.
-
-  (** Internalized properties *)
-  Lemma iprod_equivI {M} g1 g2 : g1 ≡ g2 ⊣⊢ (∀ i, g1 i ≡ g2 i : uPred M).
-  Proof. by uPred.unseal. Qed.
-  Lemma iprod_validI {M} g : ✓ g ⊣⊢ (∀ i, ✓ g i : uPred M).
-  Proof. by uPred.unseal. Qed.
-
-  (** Properties of iprod_insert. *)
-  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; apply cmra_total_updateP.
-    intros n gf Hg. destruct (Hy1 n (Some (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.
-End iprod_cmra.
-
-Arguments iprodR {_ _ _} _.
-Arguments iprodUR {_ _ _} _.
-
-Definition iprod_singleton `{Finite A} {B : A → ucmraT} 
-  (x : A) (y : B x) : iprod B := iprod_insert x y ∅.
-Instance: Params (@iprod_singleton) 5.
-
-Section iprod_singleton.
-  Context `{Finite A} {B : A → ucmraT}.
-  Implicit Types x : A.
-
-  Global Instance iprod_singleton_ne n x :
-    Proper (dist n ==> dist n) (iprod_singleton x : B x → _).
-  Proof. intros y1 y2 ?; apply iprod_insert_ne. done. by apply equiv_dist. Qed.
-  Global Instance iprod_singleton_proper x :
-    Proper ((≡) ==> (≡)) (iprod_singleton x) := ne_proper _.
-
-  Lemma iprod_lookup_singleton x (y : B x) : (iprod_singleton x y) x = y.
-  Proof. by rewrite /iprod_singleton iprod_lookup_insert. Qed.
-  Lemma iprod_lookup_singleton_ne x x' (y : B x) :
-    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) :
-    Timeless y → Timeless (iprod_singleton x y) := _.
-
-  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 ucmra_unit_validN.
-  Qed.
-
-  Lemma iprod_core_singleton x (y : B x) :
-    core (iprod_singleton x y) ≡ iprod_singleton x (core y).
-  Proof.
-    move=>x'; destruct (decide (x = x')) as [->|];
-      by rewrite iprod_lookup_core ?iprod_lookup_singleton
-      ?iprod_lookup_singleton_ne // (persistent_core ∅).
-  Qed.
-
-  Global Instance iprod_singleton_persistent x (y : B x) :
-    Persistent y → Persistent (iprod_singleton x y).
-  Proof. by rewrite !persistent_total iprod_core_singleton=> ->. 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 : B x) :
-    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; apply cmra_total_updateP.
-    intros n gf Hg. destruct (Hx n (Some (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.
-  Lemma iprod_singleton_update_empty x (y : B x) :
-    ∅ ~~> y → ∅ ~~> iprod_singleton x y.
-  Proof.
-    rewrite !cmra_update_updateP;
-      eauto using iprod_singleton_updateP_empty with subst.
-  Qed.
-End iprod_singleton.
-
-(** * Functor *)
-Definition iprod_map `{Finite A} {B1 B2 : A → cofeT} (f : ∀ x, B1 x → B2 x)
-  (g : iprod B1) : iprod B2 := λ x, f _ (g x).
-
-Lemma iprod_map_ext `{Finite A} {B1 B2 : A → cofeT} (f1 f2 : ∀ x, B1 x → B2 x) (g : iprod B1) :
-  (∀ x, f1 x (g x) ≡ f2 x (g x)) → iprod_map f1 g ≡ iprod_map f2 g.
-Proof. done. Qed.
-Lemma iprod_map_id `{Finite A} {B : A → cofeT} (g : iprod B) :
-  iprod_map (λ _, id) g = g.
-Proof. done. Qed.
-Lemma iprod_map_compose `{Finite 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 `{Finite 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
-    `{Finite A} {B1 B2 : A → ucmraT} (f : ∀ x, B1 x → B2 x) :
-  (∀ x, CMRAMonotone (f x)) → CMRAMonotone (iprod_map f).
-Proof.
-  split; first apply _.
-  - intros n g Hg x; rewrite /iprod_map; apply (validN_preserving (f _)), Hg.
-  - intros g1 g2; rewrite !iprod_included_spec=> Hf x.
-    rewrite /iprod_map; apply (included_preserving _), Hf.
-Qed.
-
-Definition iprodC_map `{Finite 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 `{Finite 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 iprodCF `{Finite C} (F : C → cFunctor) : cFunctor := {|
-  cFunctor_car A B := iprodC (λ c, cFunctor_car (F c) A B);
-  cFunctor_map A1 A2 B1 B2 fg := iprodC_map (λ c, cFunctor_map (F c) fg)
-|}.
-Next Obligation.
-  intros C ?? F A1 A2 B1 B2 n ?? g. by apply iprodC_map_ne=>?; apply cFunctor_ne.
-Qed.
-Next Obligation.
-  intros C ?? F A B g; simpl. rewrite -{2}(iprod_map_id g).
-  apply iprod_map_ext=> y; apply cFunctor_id.
-Qed.
-Next Obligation.
-  intros C ?? F A1 A2 A3 B1 B2 B3 f1 f2 f1' f2' g. rewrite /= -iprod_map_compose.
-  apply iprod_map_ext=>y; apply cFunctor_compose.
-Qed.
-Instance iprodCF_contractive `{Finite C} (F : C → cFunctor) :
-  (∀ c, cFunctorContractive (F c)) → cFunctorContractive (iprodCF F).
-Proof.
-  intros ? A1 A2 B1 B2 n ?? g.
-  by apply iprodC_map_ne=>c; apply cFunctor_contractive.
-Qed.
-
-Program Definition iprodURF `{Finite C} (F : C → urFunctor) : urFunctor := {|
-  urFunctor_car A B := iprodUR (λ c, urFunctor_car (F c) A B);
-  urFunctor_map A1 A2 B1 B2 fg := iprodC_map (λ c, urFunctor_map (F c) fg)
-|}.
-Next Obligation.
-  intros C ?? F A1 A2 B1 B2 n ?? g.
-  by apply iprodC_map_ne=>?; apply urFunctor_ne.
-Qed.
-Next Obligation.
-  intros C ?? F A B g; simpl. rewrite -{2}(iprod_map_id g).
-  apply iprod_map_ext=> y; apply urFunctor_id.
-Qed.
-Next Obligation.
-  intros C ?? F A1 A2 A3 B1 B2 B3 f1 f2 f1' f2' g. rewrite /=-iprod_map_compose.
-  apply iprod_map_ext=>y; apply urFunctor_compose.
-Qed.
-Instance iprodURF_contractive `{Finite C} (F : C → urFunctor) :
-  (∀ c, urFunctorContractive (F c)) → urFunctorContractive (iprodURF F).
-Proof.
-  intros ? A1 A2 B1 B2 n ?? g.
-  by apply iprodC_map_ne=>c; apply urFunctor_contractive.
-Qed.

algebra/list.v

-From iris.algebra Require Export cmra updates.
-From iris.prelude Require Export list.
-From iris.algebra Require Import upred.
-
-Section cofe.
-Context {A : cofeT}.
-
-Instance list_dist : Dist (list A) := λ n, Forall2 (dist n).
-
-Lemma list_dist_lookup n l1 l2 : l1 ≡{n}≡ l2 ↔ ∀ i, l1 !! i ≡{n}≡ l2 !! i.
-Proof. setoid_rewrite dist_option_Forall2. apply Forall2_lookup. Qed.
-
-Global Instance cons_ne n : Proper (dist n ==> dist n ==> dist n) (@cons A) := _.
-Global Instance app_ne n : Proper (dist n ==> dist n ==> dist n) (@app A) := _.
-Global Instance length_ne n : Proper (dist n ==> (=)) (@length A) := _.
-Global Instance tail_ne n : Proper (dist n ==> dist n) (@tail A) := _.
-Global Instance take_ne n : Proper (dist n ==> dist n) (@take A n) := _.
-Global Instance drop_ne n : Proper (dist n ==> dist n) (@drop A n) := _.
-Global Instance list_lookup_ne n i :
-  Proper (dist n ==> dist n) (lookup (M:=list A) i).
-Proof. intros ???. by apply dist_option_Forall2, Forall2_lookup. Qed.
-Global Instance list_alter_ne n f i :
-  Proper (dist n ==> dist n) f →
-  Proper (dist n ==> dist n) (alter (M:=list A) f i) := _.
-Global Instance list_insert_ne n i :
-  Proper (dist n ==> dist n ==> dist n) (insert (M:=list A) i) := _.
-Global Instance list_inserts_ne n i :
-  Proper (dist n ==> dist n ==> dist n) (@list_inserts A i) := _.
-Global Instance list_delete_ne n i :
-  Proper (dist n ==> dist n) (delete (M:=list A) i) := _.
-Global Instance option_list_ne n : Proper (dist n ==> dist n) (@option_list A).
-Proof. intros ???; by apply Forall2_option_list, dist_option_Forall2. Qed.
-Global Instance list_filter_ne n P `{∀ x, Decision (P x)} :
-  Proper (dist n ==> iff) P →
-  Proper (dist n ==> dist n) (filter (B:=list A) P) := _.
-Global Instance replicate_ne n :
-  Proper (dist n ==> dist n) (@replicate A n) := _.
-Global Instance reverse_ne n : Proper (dist n ==> dist n) (@reverse A) := _.
-Global Instance last_ne n : Proper (dist n ==> dist n) (@last A).
-Proof. intros ???; by apply dist_option_Forall2, Forall2_last. Qed.
-Global Instance resize_ne n :
-  Proper (dist n ==> dist n ==> dist n) (@resize A n) := _.
-
-Program Definition list_chain
-    (c : chain (list A)) (x : A) (k : nat) : chain A :=
-  {| chain_car n := from_option id x (c n !! k) |}.
-Next Obligation. intros c x k n i ?. by rewrite /= (chain_cauchy c n i). Qed.
-Instance list_compl : Compl (list A) := λ c,
-  match c 0 with
-  | [] => []
-  | x :: _ => compl ∘ list_chain c x <$> seq 0 (length (c 0))
-  end.
-
-Definition list_cofe_mixin : CofeMixin (list A).
-Proof.
-  split.
-  - intros l k. rewrite equiv_Forall2 -Forall2_forall.
-    split; induction 1; constructor; intros; try apply equiv_dist; auto.
-  - apply _.
-  - rewrite /dist /list_dist. eauto using Forall2_impl, dist_S.
-  - intros n c; rewrite /compl /list_compl.
-    destruct (c 0) as [|x l] eqn:Hc0 at 1.
-    { by destruct (chain_cauchy c 0 n); auto with omega. }
-    rewrite -(λ H, length_ne _ _ _ (chain_cauchy c 0 n H)); last omega.
-    apply Forall2_lookup=> i. rewrite -dist_option_Forall2 list_lookup_fmap.
-    destruct (decide (i < length (c n))); last first.
-    { rewrite lookup_seq_ge ?lookup_ge_None_2; auto with omega. }
-    rewrite lookup_seq //= (conv_compl n (list_chain c _ _)) /=.
-    by destruct (lookup_lt_is_Some_2 (c n) i) as [? ->].
-Qed.
-Canonical Structure listC := CofeT (list A) list_cofe_mixin.
-Global Instance list_discrete : Discrete A → Discrete listC.
-Proof. induction 2; constructor; try apply (timeless _); auto. Qed.
-
-Global Instance nil_timeless : Timeless (@nil A).
-Proof. inversion_clear 1; constructor. Qed.
-Global Instance cons_timeless x l : Timeless x → Timeless l → Timeless (x :: l).
-Proof. intros ??; inversion_clear 1; constructor; by apply timeless. Qed.
-End cofe.
-
-Arguments listC : clear implicits.
-
-(** Functor *)
-Instance list_fmap_ne {A B : cofeT} (f : A → B) n:
-  Proper (dist n ==> dist n) f → Proper (dist n ==> dist n) (fmap (M:=list) f).
-Proof. intros Hf l k ?; by eapply Forall2_fmap, Forall2_impl; eauto. Qed. 
-Definition listC_map {A B} (f : A -n> B) : listC A -n> listC B :=
-  CofeMor (fmap f : listC A → listC B).
-Instance listC_map_ne A B n : Proper (dist n ==> dist n) (@listC_map A B).
-Proof. intros f f' ? l; by apply Forall2_fmap, Forall_Forall2, Forall_true. Qed.
-
-Program Definition listCF (F : cFunctor) : cFunctor := {|
-  cFunctor_car A B := listC (cFunctor_car F A B);
-  cFunctor_map A1 A2 B1 B2 fg := listC_map (cFunctor_map F fg)
-|}.
-Next Obligation.
-  by intros F A1 A2 B1 B2 n f g Hfg; apply listC_map_ne, cFunctor_ne.
-Qed.
-Next Obligation.
-  intros F A B x. rewrite /= -{2}(list_fmap_id x).
-  apply list_fmap_setoid_ext=>y. apply cFunctor_id.
-Qed.
-Next Obligation.
-  intros F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -list_fmap_compose.
-  apply list_fmap_setoid_ext=>y; apply cFunctor_compose.
-Qed.
-
-Instance listCF_contractive F :
-  cFunctorContractive F → cFunctorContractive (listCF F).
-Proof.
-  by intros ? A1 A2 B1 B2 n f g Hfg; apply listC_map_ne, cFunctor_contractive.
-Qed.
-
-(* CMRA *)
-Section cmra.
-  Context {A : ucmraT}.
-  Implicit Types l : list A.
-  Local Arguments op _ _ !_ !_ / : simpl nomatch.
-
-  Instance list_op : Op (list A) :=
-    fix go l1 l2 := let _ : Op _ := @go in
-    match l1, l2 with
-    | [], _ => l2
-    | _, [] => l1
-    | x :: l1, y :: l2 => x ⋅ y :: l1 ⋅ l2
-    end.
-  Instance list_pcore : PCore (list A) := λ l, Some (core <$> l).
-
-  Instance list_valid : Valid (list A) := Forall (λ x, ✓ x).
-  Instance list_validN : ValidN (list A) := λ n, Forall (λ x, ✓{n} x).
-
-  Lemma list_lookup_valid l : ✓ l ↔ ∀ i, ✓ (l !! i).
-  Proof.
-    rewrite {1}/valid /list_valid Forall_lookup; split.
-    - intros Hl i. by destruct (l !! i) as [x|] eqn:?; [apply (Hl i)|].
-    - intros Hl i x Hi. move: (Hl i); by rewrite Hi.
-  Qed.
-  Lemma list_lookup_validN n l : ✓{n} l ↔ ∀ i, ✓{n} (l !! i).
-  Proof.
-    rewrite {1}/validN /list_validN Forall_lookup; split.
-    - intros Hl i. by destruct (l !! i) as [x|] eqn:?; [apply (Hl i)|].
-    - intros Hl i x Hi. move: (Hl i); by rewrite Hi.
-  Qed.
-  Lemma list_lookup_op l1 l2 i : (l1 ⋅ l2) !! i = l1 !! i ⋅ l2 !! i.
-  Proof.
-    revert i l2. induction l1 as [|x l1]; intros [|i] [|y l2];
-      by rewrite /= ?left_id_L ?right_id_L.
-  Qed.
-  Lemma list_lookup_core l i : core l !! i = core (l !! i).
-  Proof.
-    rewrite /core /= list_lookup_fmap.
-    destruct (l !! i); by rewrite /= ?Some_core.
-  Qed.
-
-  Lemma list_lookup_included l1 l2 : l1 ≼ l2 ↔ ∀ i, l1 !! i ≼ l2 !! i.
-  Proof.
-    split.
-    { intros [l Hl] i. exists (l !! i). by rewrite Hl list_lookup_op. }
-    revert l1. induction l2 as [|y l2 IH]=>-[|x l1] Hl.
-    - by exists [].
-    - destruct (Hl 0) as [[z|] Hz]; inversion Hz.
-    - by exists (y :: l2).
-    - destruct (IH l1) as [l3 ?]; first (intros i; apply (Hl (S i))).
-      destruct (Hl 0) as [[z|] Hz]; inversion_clear Hz; simplify_eq/=.
-      + exists (z :: l3); by constructor.
-      + exists (core x :: l3); constructor; by rewrite ?cmra_core_r.
-  Qed.
-
-  Definition list_cmra_mixin : CMRAMixin (list A).
-  Proof.
-    apply cmra_total_mixin.
-    - eauto.
-    - intros n l l1 l2; rewrite !list_dist_lookup=> Hl i.
-      by rewrite !list_lookup_op Hl.
-    - intros n l1 l2 Hl; by rewrite /core /= Hl.
-    - intros n l1 l2; rewrite !list_dist_lookup !list_lookup_validN=> Hl ? i.
-      by rewrite -Hl.
-    - intros l. rewrite list_lookup_valid. setoid_rewrite list_lookup_validN.
-      setoid_rewrite cmra_valid_validN. naive_solver.
-    - intros n x. rewrite !list_lookup_validN. auto using cmra_validN_S.
-    - intros l1 l2 l3; rewrite list_equiv_lookup=> i.
-      by rewrite !list_lookup_op assoc.
-    - intros l1 l2; rewrite list_equiv_lookup=> i.
-      by rewrite !list_lookup_op comm.
-    - intros l; rewrite list_equiv_lookup=> i.
-      by rewrite list_lookup_op list_lookup_core cmra_core_l.
-    - intros l; rewrite list_equiv_lookup=> i.
-      by rewrite !list_lookup_core cmra_core_idemp.
-    - intros l1 l2; rewrite !list_lookup_included=> Hl i.
-      rewrite !list_lookup_core. by apply cmra_core_preserving.
-    - intros n l1 l2. rewrite !list_lookup_validN.
-      setoid_rewrite list_lookup_op. eauto using cmra_validN_op_l.
-    - intros n l. induction l as [|x l IH]=> -[|y1 l1] [|y2 l2] Hl Hl';
-        try (by exfalso; inversion_clear Hl').
-      + by exists ([], []).
-      + by exists ([], x :: l).
-      + by exists (x :: l, []).
-      + destruct (IH l1 l2) as ([l1' l2']&?&?&?),
-          (cmra_extend n x y1 y2) as ([y1' y2']&?&?&?);
-          [inversion_clear Hl; inversion_clear Hl'; auto ..|]; simplify_eq/=.
-        exists (y1' :: l1', y2' :: l2'); repeat constructor; auto.
-  Qed.
-  Canonical Structure listR := CMRAT (list A) list_cofe_mixin list_cmra_mixin.
-
-  Global Instance empty_list : Empty (list A) := [].
-  Definition list_ucmra_mixin : UCMRAMixin (list A).
-  Proof.
-    split.
-    - constructor.
-    - by intros l.
-    - by inversion_clear 1.
-    - by constructor.
-  Qed.
-  Canonical Structure listUR :=
-    UCMRAT (list A) list_cofe_mixin list_cmra_mixin list_ucmra_mixin.
-
-  Global Instance list_cmra_discrete : CMRADiscrete A → CMRADiscrete listR.
-  Proof.
-    split; [apply _|]=> l; rewrite list_lookup_valid list_lookup_validN=> Hl i.
-    by apply cmra_discrete_valid.
-  Qed.
-
-  Global Instance list_persistent l : (∀ x : A, Persistent x) → Persistent l.
-  Proof.
-    intros ?; constructor; apply list_equiv_lookup=> i.
-    by rewrite list_lookup_core (persistent_core (l !! i)).
-  Qed.
-
-  (** Internalized properties *)
-  Lemma list_equivI {M} l1 l2 : l1 ≡ l2 ⊣⊢ (∀ i, l1 !! i ≡ l2 !! i : uPred M).
-  Proof. uPred.unseal; constructor=> n x ?. apply list_dist_lookup. Qed.
-  Lemma list_validI {M} l : ✓ l ⊣⊢ (∀ i, ✓ (l !! i) : uPred M).
-  Proof. uPred.unseal; constructor=> n x ?. apply list_lookup_validN. Qed.
-End cmra.
-
-Arguments listR : clear implicits.
-Arguments listUR : clear implicits.
-
-Instance list_singletonM {A : ucmraT} : SingletonM nat A (list A) := λ n x,
-  replicate n ∅ ++ [x].
-
-Section properties.
-  Context {A : ucmraT}.
-  Implicit Types l : list A.
-  Implicit Types x y z : A.
-  Local Arguments op _ _ !_ !_ / : simpl nomatch.
-  Local Arguments cmra_op _ !_ !_ / : simpl nomatch.
-
-  Lemma list_lookup_opM l mk i : (l ⋅? mk) !! i = l !! i ⋅ (mk ≫= (!! i)).
-  Proof. destruct mk; by rewrite /= ?list_lookup_op ?right_id_L. Qed.
-
-  Lemma list_op_app l1 l2 l3 :
-    length l2 ≤ length l1 → (l1 ++ l3) ⋅ l2 = (l1 ⋅ l2) ++ l3.
-  Proof.
-    revert l2 l3.
-    induction l1 as [|x1 l1]=> -[|x2 l2] [|x3 l3] ?; f_equal/=; auto with lia.
-  Qed.
-
-  Lemma list_lookup_validN_Some n l i x : ✓{n} l → l !! i ≡{n}≡ Some x → ✓{n} x.
-  Proof. move=> /list_lookup_validN /(_ i)=> Hl Hi; move: Hl. by rewrite Hi. Qed.
-  Lemma list_lookup_valid_Some l i x : ✓ l → l !! i ≡ Some x → ✓ x.
-  Proof. move=> /list_lookup_valid /(_ i)=> Hl Hi; move: Hl. by rewrite Hi. Qed.
-
-  Lemma list_op_length l1 l2 : length (l1 ⋅ l2) = max (length l1) (length l2).
-  Proof. revert l2. induction l1; intros [|??]; f_equal/=; auto. Qed.
-
-  Lemma replicate_valid n (x : A) : ✓ x → ✓ replicate n x.
-  Proof. apply Forall_replicate. Qed.
-  Global Instance list_singletonM_ne n i :
-    Proper (dist n ==> dist n) (@list_singletonM A i).
-  Proof. intros l1 l2 ?. apply Forall2_app; by repeat constructor. Qed.
-  Global Instance list_singletonM_proper i :
-    Proper ((≡) ==> (≡)) (list_singletonM i) := ne_proper _.
-
-  Lemma elem_of_list_singletonM i z x : z ∈ {[i := x]} → z = ∅ ∨ z = x.
-  Proof.
-    rewrite elem_of_app elem_of_list_singleton elem_of_replicate. naive_solver.
-  Qed.
-  Lemma list_lookup_singletonM i x : {[ i := x ]} !! i = Some x.
-  Proof. induction i; by f_equal/=. Qed.
-  Lemma list_lookup_singletonM_ne i j x :
-    i ≠ j → {[ i := x ]} !! j = None ∨ {[ i := x ]} !! j = Some ∅.
-  Proof. revert j; induction i; intros [|j]; naive_solver auto with omega. Qed.
-  Lemma list_singletonM_validN n i x : ✓{n} {[ i := x ]} ↔ ✓{n} x.
-  Proof.
-    rewrite list_lookup_validN. split.
-    { move=> /(_ i). by rewrite list_lookup_singletonM. }
-    intros Hx j; destruct (decide (i = j)); subst.
-    - by rewrite list_lookup_singletonM.
-    - destruct (list_lookup_singletonM_ne i j x) as [Hi|Hi]; first done;
-        rewrite Hi; by try apply (ucmra_unit_validN (A:=A)).
-  Qed.
-  Lemma list_singleton_valid  i x : ✓ {[ i := x ]} ↔ ✓ x.
-  Proof.
-    rewrite !cmra_valid_validN. by setoid_rewrite list_singletonM_validN.
-  Qed.
-  Lemma list_singletonM_length i x : length {[ i := x ]} = S i.
-  Proof.
-    rewrite /singletonM /list_singletonM app_length replicate_length /=; lia.
-  Qed.
-
-  Lemma list_core_singletonM i (x : A) : core {[ i := x ]} ≡ {[ i := core x ]}.
-  Proof.
-    rewrite /singletonM /list_singletonM.
-    by rewrite {1}/core /= fmap_app fmap_replicate (persistent_core ∅).
-  Qed.
-  Lemma list_op_singletonM i (x y : A) :
-    {[ i := x ]} ⋅ {[ i := y ]} ≡ {[ i := x ⋅ y ]}.
-  Proof.
-    rewrite /singletonM /list_singletonM /=.
-    induction i; constructor; rewrite ?left_id; auto.
-  Qed.
-  Lemma list_alter_singletonM f i x : alter f i {[i := x]} = {[i := f x]}.
-  Proof.
-    rewrite /singletonM /list_singletonM /=. induction i; f_equal/=; auto.
-  Qed.
-  Global Instance list_singleton_persistent i (x : A) :
-    Persistent x → Persistent {[ i := x ]}.
-  Proof. by rewrite !persistent_total list_core_singletonM=> ->. Qed.
-
-  (* Update *)
-  Lemma list_middle_updateP (P : A → Prop) (Q : list A → Prop) l1 x l2 :
-    x ~~>: P → (∀ y, P y → Q (l1 ++ y :: l2)) → l1 ++ x :: l2 ~~>: Q.
-  Proof.
-    intros Hx%option_updateP' HP.
-    apply cmra_total_updateP=> n mf; rewrite list_lookup_validN=> Hm.
-    destruct (Hx n (Some (mf !! length l1))) as ([y|]&H1&H2); simpl in *; try done.
-    { move: (Hm (length l1)). by rewrite list_lookup_op list_lookup_middle. }
-    exists (l1 ++ y :: l2); split; auto.
-    apply list_lookup_validN=> i.
-    destruct (lt_eq_lt_dec i (length l1)) as [[?|?]|?]; subst.
-    - move: (Hm i); by rewrite !list_lookup_op !lookup_app_l.
-    - by rewrite list_lookup_op list_lookup_middle.
-    - move: (Hm i). rewrite !(cons_middle _ l1 l2) !assoc.
-      rewrite !list_lookup_op !lookup_app_r !app_length //=; lia.
-  Qed.
-
-  Lemma list_middle_update l1 l2 x y : x ~~> y → l1 ++ x :: l2 ~~> l1 ++ y :: l2.
-  Proof.
-    rewrite !cmra_update_updateP => H; eauto using list_middle_updateP with subst.
-  Qed.
-
-  Lemma list_middle_local_update l1 l2 x y ml :
-    x ~l~> y @ ml ≫= (!! length l1) →
-    l1 ++ x :: l2 ~l~> l1 ++ y :: l2 @ ml.
-  Proof.
-    intros [Hxy Hxy']; split.
-    - intros n; rewrite !list_lookup_validN=> Hl i; move: (Hl i).
-      destruct (lt_eq_lt_dec i (length l1)) as [[?|?]|?]; subst.
-      + by rewrite !list_lookup_opM !lookup_app_l.
-      + rewrite !list_lookup_opM !list_lookup_middle // !Some_op_opM; apply (Hxy n).
-      + rewrite !(cons_middle _ l1 l2) !assoc.
-        rewrite !list_lookup_opM !lookup_app_r !app_length //=; lia.
-    - intros n mk; rewrite !list_lookup_validN !list_dist_lookup => Hl Hl' i.
-      move: (Hl i) (Hl' i).
-      destruct (lt_eq_lt_dec i (length l1)) as [[?|?]|?]; subst.
-      + by rewrite !list_lookup_opM !lookup_app_l.
-      + rewrite !list_lookup_opM !list_lookup_middle // !Some_op_opM !inj_iff.
-        apply (Hxy' n).
-      + rewrite !(cons_middle _ l1 l2) !assoc.
-        rewrite !list_lookup_opM !lookup_app_r !app_length //=; lia.
-  Qed.
-
-  Lemma list_singleton_local_update i x y ml :
-    x ~l~> y @ ml ≫= (!! i) → {[ i := x ]} ~l~> {[ i := y ]} @ ml.
-  Proof. intros; apply list_middle_local_update. by rewrite replicate_length. Qed.
-End properties.
-
-(** Functor *)
-Instance list_fmap_cmra_monotone {A B : ucmraT} (f : A → B)
-  `{!CMRAMonotone f} : CMRAMonotone (fmap f : list A → list B).
-Proof.
-  split; try apply _.
-  - intros n l. rewrite !list_lookup_validN=> Hl i. rewrite list_lookup_fmap.
-    by apply (validN_preserving (fmap f : option A → option B)).
-  - intros l1 l2. rewrite !list_lookup_included=> Hl i. rewrite !list_lookup_fmap.
-    by apply (included_preserving (fmap f : option A → option B)).
-Qed.
-
-Program Definition listURF (F : urFunctor) : urFunctor := {|
-  urFunctor_car A B := listUR (urFunctor_car F A B);
-  urFunctor_map A1 A2 B1 B2 fg := listC_map (urFunctor_map F fg)
-|}.
-Next Obligation.
-  by intros F ???? n f g Hfg; apply listC_map_ne, urFunctor_ne.
-Qed.
-Next Obligation.
-  intros F A B x. rewrite /= -{2}(list_fmap_id x).
-  apply list_fmap_setoid_ext=>y. apply urFunctor_id.
-Qed.
-Next Obligation.
-  intros F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -list_fmap_compose.
-  apply list_fmap_setoid_ext=>y; apply urFunctor_compose.
-Qed.
-
-Instance listURF_contractive F :
-  urFunctorContractive F → urFunctorContractive (listURF F).
-Proof.
-  by intros ? A1 A2 B1 B2 n f g Hfg; apply listC_map_ne, urFunctor_contractive.
-Qed.

algebra/upred.v

-From iris.algebra Require Export cmra.
-Local Hint Extern 1 (_ ≼ _) => etrans; [eassumption|].
-Local Hint Extern 1 (_ ≼ _) => etrans; [|eassumption].
-Local Hint Extern 10 (_ ≤ _) => omega.
-
-Record uPred (M : ucmraT) : Type := IProp {
-  uPred_holds :> nat → M → Prop;
-  uPred_mono n x1 x2 : uPred_holds n x1 → x1 ≼{n} x2 → uPred_holds n x2;
-  uPred_closed n1 n2 x : uPred_holds n1 x → n2 ≤ n1 → ✓{n2} x → uPred_holds n2 x
-}.
-Arguments uPred_holds {_} _ _ _ : simpl never.
-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 : ucmraT}.
-
-  Inductive uPred_equiv' (P Q : uPred M) : Prop :=
-    { uPred_in_equiv : ∀ n x, ✓{n} x → P n x ↔ Q n x }.
-  Instance uPred_equiv : Equiv (uPred M) := uPred_equiv'.
-  Inductive uPred_dist' (n : nat) (P Q : uPred M) : Prop :=
-    { uPred_in_dist : ∀ n' x, n' ≤ n → ✓{n'} x → P n' x ↔ Q n' x }.
-  Instance uPred_dist : Dist (uPred M) := uPred_dist'.
-  Program Instance uPred_compl : Compl (uPred M) := λ c,
-    {| uPred_holds n x := c n n x |}.
-  Next Obligation. naive_solver eauto using uPred_mono. Qed.
-  Next Obligation.
-    intros c n1 n2 x ???; simpl in *.
-    apply (chain_cauchy c n2 n1); eauto using uPred_closed.
-  Qed.
-  Definition uPred_cofe_mixin : CofeMixin (uPred M).
-  Proof.
-    split.
-    - intros P Q; split.
-      + by intros HPQ n; split=> i x ??; apply HPQ.
-      + intros HPQ; split=> n x ?; apply HPQ with n; auto.
-    - intros n; split.
-      + by intros P; split=> x i.
-      + by intros P Q HPQ; split=> x i ??; symmetry; apply HPQ.
-      + intros P Q Q' HP HQ; split=> i x ??.
-        by trans (Q i x);[apply HP|apply HQ].
-    - intros n P Q HPQ; split=> i x ??; apply HPQ; auto.
-    - intros n c; split=>i x ??; symmetry; apply (chain_cauchy c i n); auto.
-  Qed.
-  Canonical Structure uPredC : cofeT := CofeT (uPred M) 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=> ?; eapply uPred_mono; eauto; by rewrite Hx.
-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.
-
-(** functor *)
-Program Definition uPred_map {M1 M2 : ucmraT} (f : M2 -n> M1)
-  `{!CMRAMonotone f} (P : uPred M1) :
-  uPred M2 := {| uPred_holds n x := P n (f x) |}.
-Next Obligation. naive_solver eauto using uPred_mono, includedN_preserving. Qed.
-Next Obligation. naive_solver eauto using uPred_closed, validN_preserving. Qed.
-
-Instance uPred_map_ne {M1 M2 : ucmraT} (f : M2 -n> M1)
-  `{!CMRAMonotone f} n : Proper (dist n ==> dist n) (uPred_map f).
-Proof.
-  intros x1 x2 Hx; split=> n' y ??.
-  split; apply Hx; auto using validN_preserving.
-Qed.
-Lemma uPred_map_id {M : ucmraT} (P : uPred M): uPred_map cid P ≡ P.
-Proof. by split=> n x ?. Qed.
-Lemma uPred_map_compose {M1 M2 M3 : ucmraT} (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 split=> n x Hx. Qed.
-Lemma uPred_map_ext {M1 M2 : ucmraT} (f g : M1 -n> M2)
-      `{!CMRAMonotone f} `{!CMRAMonotone g}:
-  (∀ x, f x ≡ g x) → ∀ x, uPred_map f x ≡ uPred_map g x.
-Proof. intros Hf P; split=> n x Hx /=; by rewrite /uPred_holds /= Hf. Qed.
-Definition uPredC_map {M1 M2 : ucmraT} (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 : ucmraT} (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; split=> n' y ??;
-    rewrite /uPred_holds /= (dist_le _ _ _ _(Hfg y)); last lia.
-Qed.
-
-Program Definition uPredCF (F : urFunctor) : cFunctor := {|
-  cFunctor_car A B := uPredC (urFunctor_car F B A);
-  cFunctor_map A1 A2 B1 B2 fg := uPredC_map (urFunctor_map F (fg.2, fg.1))
-|}.
-Next Obligation.
-  intros F A1 A2 B1 B2 n P Q HPQ.
-  apply uPredC_map_ne, urFunctor_ne; split; by apply HPQ.
-Qed.
-Next Obligation.
-  intros F A B P; simpl. rewrite -{2}(uPred_map_id P).
-  apply uPred_map_ext=>y. by rewrite urFunctor_id.
-Qed.
-Next Obligation.
-  intros F A1 A2 A3 B1 B2 B3 f g f' g' P; simpl. rewrite -uPred_map_compose.
-  apply uPred_map_ext=>y; apply urFunctor_compose.
-Qed.
-
-Instance uPredCF_contractive F :
-  urFunctorContractive F → cFunctorContractive (uPredCF F).
-Proof.
-  intros ? A1 A2 B1 B2 n P Q HPQ.
-  apply uPredC_map_ne, urFunctor_contractive=> i ?; split; by apply HPQ.
-Qed.
-
-(** logical entailement *)
-Inductive uPred_entails {M} (P Q : uPred M) : Prop :=
-  { uPred_in_entails : ∀ 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).
-
-Hint Resolve uPred_mono uPred_closed : uPred_def.
-
-(** logical connectives *)
-Program Definition uPred_pure_def {M} (φ : Prop) : uPred M :=
-  {| uPred_holds n x := φ |}.
-Solve Obligations with done.
-Definition uPred_pure_aux : { x | x = @uPred_pure_def }. by eexists. Qed.
-Definition uPred_pure {M} := proj1_sig uPred_pure_aux M.
-Definition uPred_pure_eq :
-  @uPred_pure = @uPred_pure_def := proj2_sig uPred_pure_aux.
-
-Instance uPred_inhabited M : Inhabited (uPred M) := populate (uPred_pure True).
-
-Program Definition uPred_and_def {M} (P Q : uPred M) : uPred M :=
-  {| uPred_holds n x := P n x ∧ Q n x |}.
-Solve Obligations with naive_solver eauto 2 with uPred_def.
-Definition uPred_and_aux : { x | x = @uPred_and_def }. by eexists. Qed.
-Definition uPred_and {M} := proj1_sig uPred_and_aux M.
-Definition uPred_and_eq: @uPred_and = @uPred_and_def := proj2_sig uPred_and_aux.
-
-Program Definition uPred_or_def {M} (P Q : uPred M) : uPred M :=
-  {| uPred_holds n x := P n x ∨ Q n x |}.
-Solve Obligations with naive_solver eauto 2 with uPred_def.
-Definition uPred_or_aux : { x | x = @uPred_or_def }. by eexists. Qed.
-Definition uPred_or {M} := proj1_sig uPred_or_aux M.
-Definition uPred_or_eq: @uPred_or = @uPred_or_def := proj2_sig uPred_or_aux.
-
-Program Definition uPred_impl_def {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 [x2 Hx1'] n2 x3 [x4 Hx3] ?; simpl in *.
-  rewrite Hx3 (dist_le _ _ _ _ Hx1'); auto. intros ??.
-  eapply HPQ; auto. exists (x2 ⋅ x4); by rewrite assoc.
-Qed.
-Next Obligation. intros M P Q [|n1] [|n2] x; auto with lia. Qed.
-Definition uPred_impl_aux : { x | x = @uPred_impl_def }. by eexists. Qed.
-Definition uPred_impl {M} := proj1_sig uPred_impl_aux M.
-Definition uPred_impl_eq :
-  @uPred_impl = @uPred_impl_def := proj2_sig uPred_impl_aux.
-
-Program Definition uPred_forall_def {M A} (Ψ : A → uPred M) : uPred M :=
-  {| uPred_holds n x := ∀ a, Ψ a n x |}.
-Solve Obligations with naive_solver eauto 2 with uPred_def.
-Definition uPred_forall_aux : { x | x = @uPred_forall_def }. by eexists. Qed.
-Definition uPred_forall {M A} := proj1_sig uPred_forall_aux M A.
-Definition uPred_forall_eq :
-  @uPred_forall = @uPred_forall_def := proj2_sig uPred_forall_aux.
-
-Program Definition uPred_exist_def {M A} (Ψ : A → uPred M) : uPred M :=
-  {| uPred_holds n x := ∃ a, Ψ a n x |}.
-Solve Obligations with naive_solver eauto 2 with uPred_def.
-Definition uPred_exist_aux : { x | x = @uPred_exist_def }. by eexists. Qed.
-Definition uPred_exist {M A} := proj1_sig uPred_exist_aux M A.
-Definition uPred_exist_eq: @uPred_exist = @uPred_exist_def := proj2_sig uPred_exist_aux.
-
-Program Definition uPred_eq_def {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)).
-Definition uPred_eq_aux : { x | x = @uPred_eq_def }. by eexists. Qed.
-Definition uPred_eq {M A} := proj1_sig uPred_eq_aux M A.
-Definition uPred_eq_eq: @uPred_eq = @uPred_eq_def := proj2_sig uPred_eq_aux.
-
-Program Definition uPred_sep_def {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.
-  intros M P Q n x y (x1&x2&Hx&?&?) [z Hy].
-  exists x1, (x2 ⋅ z); split_and?; eauto using uPred_mono, cmra_includedN_l.
-  by rewrite Hy Hx assoc.
-Qed.
-Next Obligation.
-  intros M P Q n1 n2 x (x1&x2&Hx&?&?) ?; rewrite {1}(dist_le _ _ _ _ Hx) // =>?.
-  exists x1, x2; cofe_subst; split_and!;
-    eauto using dist_le, uPred_closed, cmra_validN_op_l, cmra_validN_op_r.
-Qed.
-Definition uPred_sep_aux : { x | x = @uPred_sep_def }. by eexists. Qed.
-Definition uPred_sep {M} := proj1_sig uPred_sep_aux M.
-Definition uPred_sep_eq: @uPred_sep = @uPred_sep_def := proj2_sig uPred_sep_aux.
-
-Program Definition uPred_wand_def {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 n x1 x1' HPQ ? n3 x3 ???; simpl in *.
-  apply uPred_mono with (x1 ⋅ x3);
-    eauto using cmra_validN_includedN, cmra_preservingN_r, cmra_includedN_le.
-Qed.
-Next Obligation. naive_solver. Qed.
-Definition uPred_wand_aux : { x | x = @uPred_wand_def }. by eexists. Qed.
-Definition uPred_wand {M} := proj1_sig uPred_wand_aux M.
-Definition uPred_wand_eq :
-  @uPred_wand = @uPred_wand_def := proj2_sig uPred_wand_aux.
-
-Program Definition uPred_always_def {M} (P : uPred M) : uPred M :=
-  {| uPred_holds n x := P n (core x) |}.
-Next Obligation.
-  intros M; naive_solver eauto using uPred_mono, @cmra_core_preservingN.
-Qed.
-Next Obligation. naive_solver eauto using uPred_closed, @cmra_core_validN. Qed.
-Definition uPred_always_aux : { x | x = @uPred_always_def }. by eexists. Qed.
-Definition uPred_always {M} := proj1_sig uPred_always_aux M.
-Definition uPred_always_eq :
-  @uPred_always = @uPred_always_def := proj2_sig uPred_always_aux.
-
-Program Definition uPred_later_def {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] x1 x2; eauto using uPred_mono, cmra_includedN_S.
-Qed.
-Next Obligation.
-  intros M P [|n1] [|n2] x; eauto using uPred_closed, cmra_validN_S with lia.
-Qed.
-Definition uPred_later_aux : { x | x = @uPred_later_def }. by eexists. Qed.
-Definition uPred_later {M} := proj1_sig uPred_later_aux M.
-Definition uPred_later_eq :
-  @uPred_later = @uPred_later_def := proj2_sig uPred_later_aux.
-
-Program Definition uPred_ownM_def {M : ucmraT} (a : M) : uPred M :=
-  {| uPred_holds n x := a ≼{n} x |}.
-Next Obligation.
-  intros M a n x1 x [a' Hx1] [x2 ->].
-  exists (a' ⋅ x2). by rewrite (assoc op) Hx1.
-Qed.
-Next Obligation. naive_solver eauto using cmra_includedN_le. Qed.
-Definition uPred_ownM_aux : { x | x = @uPred_ownM_def }. by eexists. Qed.
-Definition uPred_ownM {M} := proj1_sig uPred_ownM_aux M.
-Definition uPred_ownM_eq :
-  @uPred_ownM = @uPred_ownM_def := proj2_sig uPred_ownM_aux.
-
-Program Definition uPred_valid_def {M : ucmraT} {A : cmraT} (a : A) : uPred M :=
-  {| uPred_holds n x := ✓{n} a |}.
-Solve Obligations with naive_solver eauto 2 using cmra_validN_le.
-Definition uPred_valid_aux : { x | x = @uPred_valid_def }. by eexists. Qed.
-Definition uPred_valid {M A} := proj1_sig uPred_valid_aux M A.
-Definition uPred_valid_eq :
-  @uPred_valid = @uPred_valid_def := proj2_sig uPred_valid_aux.
-
-Notation "P ⊢ Q" := (uPred_entails P%I Q%I)
-  (at level 99, Q at level 200, right associativity) : C_scope.
-Notation "(⊢)" := uPred_entails (only parsing) : C_scope.
-Notation "P ⊣⊢ Q" := (equiv (A:=uPred _) P%I Q%I)
-  (at level 95, no associativity) : C_scope.
-Notation "(⊣⊢)" := (equiv (A:=uPred _)) (only parsing) : C_scope.
-Notation "■ φ" := (uPred_pure φ%C%type)
-  (at level 20, right associativity) : uPred_scope.
-Notation "x = y" := (uPred_pure (x%C%type = y%C%type)) : uPred_scope.
-Notation "x ⊥ y" := (uPred_pure (x%C%type ⊥ y%C%type)) : uPred_scope.
-Notation "'False'" := (uPred_pure False) : uPred_scope.
-Notation "'True'" := (uPred_pure 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 99, 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_always P)
-  (at level 20, right associativity) : uPred_scope.
-Notation "▷ P" := (uPred_later 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.
-Instance: Params (@uPred_iff) 1.
-Infix "↔" := uPred_iff : uPred_scope.
-
-Definition uPred_always_if {M} (p : bool) (P : uPred M) : uPred M :=
-  (if p then □ P else P)%I.
-Instance: Params (@uPred_always_if) 2.
-Arguments uPred_always_if _ !_ _/.
-Notation "□? p P" := (uPred_always_if p P)
-  (at level 20, p at level 0, P at level 20, format "□? p  P").
-
-Class TimelessP {M} (P : uPred M) := timelessP : ▷ P ⊢ (P ∨ ▷ False).
-Arguments timelessP {_} _ {_}.
-
-Class PersistentP {M} (P : uPred M) := persistentP : P ⊢ □ P.
-Arguments persistentP {_} _ {_}.
-
-Module uPred.
-Definition unseal :=
-  (uPred_pure_eq, uPred_and_eq, uPred_or_eq, uPred_impl_eq, uPred_forall_eq,
-  uPred_exist_eq, uPred_eq_eq, uPred_sep_eq, uPred_wand_eq, uPred_always_eq,
-  uPred_later_eq, uPred_ownM_eq, uPred_valid_eq).
-Ltac unseal := rewrite !unseal /=.
-
-Section uPred_logic.
-Context {M : ucmraT}.
-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 *)
-Notation "P ⊣⊢ Q" := (equiv (A:=uPred M) P%I Q%I). (* Force implicit argument M *)
-Arguments uPred_holds {_} !_ _ _ /.
-Hint Immediate uPred_in_entails.
-
-Global Instance: PreOrder (@uPred_entails M).
-Proof.
-  split.
-  * by intros P; split=> x i.
-  * by intros P Q Q' HP HQ; split=> x i ??; apply HQ, HP.
-Qed.
-Global Instance: AntiSymm (⊣⊢) (@uPred_entails M).
-Proof. intros P Q HPQ HQP; split=> x n; by split; [apply HPQ|apply HQP]. Qed.
-Lemma equiv_spec P Q : (P ⊣⊢ Q) ↔ (P ⊢ Q) ∧ (Q ⊢ P).
-Proof.
-  split; [|by intros [??]; apply (anti_symm (⊢))].
-  intros HPQ; split; split=> x i; apply HPQ.
-Qed.
-Lemma equiv_entails P Q : (P ⊣⊢ Q) → (P ⊢ Q).
-Proof. apply equiv_spec. Qed.
-Lemma equiv_entails_sym P Q : (Q ⊣⊢ P) → (P ⊢ Q).
-Proof. apply equiv_spec. 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 trans P1; [|trans Q1].
-  - by trans P2; [|trans Q2].
-Qed.
-Lemma entails_equiv_l (P Q R : uPred M) : (P ⊣⊢ Q) → (Q ⊢ R) → (P ⊢ R).
-Proof. by intros ->. Qed.
-Lemma entails_equiv_r (P Q R : uPred M) : (P ⊢ Q) → (Q ⊣⊢ R) → (P ⊢ R).
-Proof. by intros ? <-. Qed.
-
-(** Non-expansiveness and setoid morphisms *)
-Global Instance pure_proper : Proper (iff ==> (⊣⊢)) (@uPred_pure M).
-Proof. intros φ1 φ2 Hφ. by unseal; split=> -[|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; unseal; split=> x n' ??.
-  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=> x n' ??.
-  unseal; split; (intros [?|?]; [left; by apply HP|right; by 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=> x n' ??.
-  unseal; 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; split=> n' x ??.
-  unseal; 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; split=> n' x ??; unseal; split; intros HPQ x' n'' ???;
-    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; split=> n' z; unseal; 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 n :
-  Proper (pointwise_relation _ (dist n) ==> dist n) (@uPred_forall M A).
-Proof.
-  by intros Ψ1 Ψ2 HΨ; unseal; split=> 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Ψ; unseal; split=> n' x; split; intros HP a; apply HΨ.
-Qed.
-Global Instance exist_ne A n :
-  Proper (pointwise_relation _ (dist n) ==> dist n) (@uPred_exist M A).
-Proof.
-  intros Ψ1 Ψ2 HΨ.
-  unseal; split=> n' x ??; split; intros [a ?]; exists a; by apply HΨ.
-Qed.
-Global Instance exist_proper A :
-  Proper (pointwise_relation _ (⊣⊢) ==> (⊣⊢)) (@uPred_exist M A).
-Proof.
-  intros Ψ1 Ψ2 HΨ.
-  unseal; split=> n' x ?; split; intros [a ?]; exists a; by apply HΨ.
-Qed.
-Global Instance later_contractive : Contractive (@uPred_later M).
-Proof.
-  intros n P Q HPQ; unseal; split=> -[|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.
-  unseal; split=> n' x; split; apply HP; eauto using @cmra_core_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.
-  intros a b Ha.
-  unseal; split=> 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.
-  intros a b Ha; unseal; split=> 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 pure_intro φ P : φ → P ⊢ ■ φ.
-Proof. by intros ?; unseal; split. Qed.
-Lemma pure_elim φ Q R : (Q ⊢ ■ φ) → (φ → Q ⊢ R) → Q ⊢ R.
-Proof.
-  unseal; intros HQP HQR; split=> n x ??; apply HQR; first eapply HQP; eauto.
-Qed.
-Lemma and_elim_l P Q : P ∧ Q ⊢ P.
-Proof. by unseal; split=> n x ? [??]. Qed.
-Lemma and_elim_r P Q : P ∧ Q ⊢ Q.
-Proof. by unseal; split=> n x ? [??]. Qed.
-Lemma and_intro P Q R : (P ⊢ Q) → (P ⊢ R) → P ⊢ Q ∧ R.
-Proof. intros HQ HR; unseal; split=> n x ??; by split; [apply HQ|apply HR]. Qed.
-Lemma or_intro_l P Q : P ⊢ P ∨ Q.
-Proof. unseal; split=> n x ??; left; auto. Qed.
-Lemma or_intro_r P Q : Q ⊢ P ∨ Q.
-Proof. unseal; split=> n x ??; right; auto. Qed.
-Lemma or_elim P Q R : (P ⊢ R) → (Q ⊢ R) → P ∨ Q ⊢ R.
-Proof. intros HP HQ; unseal; split=> n x ? [?|?]. by apply HP. by apply HQ. Qed.
-Lemma impl_intro_r P Q R : (P ∧ Q ⊢ R) → P ⊢ Q → R.
-Proof.
-  unseal; intros HQ; split=> n x ?? n' x' ????. apply HQ;
-    naive_solver eauto using uPred_mono, uPred_closed, cmra_included_includedN.
-Qed.
-Lemma impl_elim P Q R : (P ⊢ Q → R) → (P ⊢ Q) → P ⊢ R.
-Proof. by unseal; intros HP HP'; split=> n x ??; apply HP with n x, HP'. Qed.
-Lemma forall_intro {A} P (Ψ : A → uPred M): (∀ a, P ⊢ Ψ a) → P ⊢ ∀ a, Ψ a.
-Proof. unseal; intros HPΨ; split=> n x ?? a; by apply HPΨ. Qed.
-Lemma forall_elim {A} {Ψ : A → uPred M} a : (∀ a, Ψ a) ⊢ Ψ a.
-Proof. unseal; split=> n x ? HP; apply HP. Qed.
-Lemma exist_intro {A} {Ψ : A → uPred M} a : Ψ a ⊢ ∃ a, Ψ a.
-Proof. unseal; split=> n x ??; by exists a. Qed.
-Lemma exist_elim {A} (Φ : A → uPred M) Q : (∀ a, Φ a ⊢ Q) → (∃ a, Φ a) ⊢ Q.
-Proof. unseal; intros HΦΨ; split=> n x ? [a ?]; by apply HΦΨ with a. Qed.
-Lemma eq_refl {A : cofeT} (a : A) : True ⊢ a ≡ a.
-Proof. unseal; by split=> 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.
-  unseal; intros Hab Ha; split=> n x ??. apply HΨ with n a; auto.
-  - by symmetry; apply Hab with x.
-  - by apply Ha.
-Qed.
-Lemma eq_equiv {A : cofeT} (a b : A) : (True ⊢ a ≡ b) → a ≡ b.
-Proof.
-  unseal=> Hab; apply equiv_dist; intros n; apply Hab with ∅; last done.
-  apply cmra_valid_validN, ucmra_unit_valid.
-Qed.
-Lemma eq_rewrite_contractive {A : cofeT} a b (Ψ : A → uPred M) P
-  {HΨ : Contractive Ψ} : (P ⊢ ▷ (a ≡ b)) → (P ⊢ Ψ a) → P ⊢ Ψ b.
-Proof.
-  unseal; intros Hab Ha; split=> n x ??. apply HΨ with n a; auto.
-  - destruct n; intros m ?; first omega. apply (dist_le n); last omega.
-    symmetry. by destruct Hab as [Hab]; eapply (Hab (S n)).
-  - by apply Ha.
-Qed.
-
-(* Derived logical stuff *)
-Lemma False_elim P : False ⊢ P.
-Proof. by apply (pure_elim False). Qed.
-Lemma True_intro P : P ⊢ True.
-Proof. by apply pure_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.
-Lemma forall_elim' {A} P (Ψ : A → uPred M) : (P ⊢ ∀ a, Ψ a) → ∀ a, P ⊢ Ψ a.
-Proof. move=> HP a. by rewrite HP forall_elim. 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 iff_refl Q P : Q ⊢ P ↔ P.
-Proof. rewrite /uPred_iff; apply and_intro; apply impl_intro_l; auto. Qed.
-Lemma iff_equiv P Q : (True ⊢ P ↔ Q) → (P ⊣⊢ Q).
-Proof.
-  intros HPQ; apply (anti_symm (⊢));
-    apply impl_entails; rewrite HPQ /uPred_iff; auto.
-Qed.
-Lemma equiv_iff P Q : (P ⊣⊢ Q) → True ⊢ P ↔ Q.
-Proof. intros ->; apply iff_refl. Qed.
-
-Lemma pure_mono φ1 φ2 : (φ1 → φ2) → ■ φ1 ⊢ ■ φ2.
-Proof. intros; apply pure_elim with φ1; eauto using pure_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 pure_mono' : Proper (impl ==> (⊢)) (@uPred_pure M).
-Proof. intros φ1 φ2; apply pure_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 or_and_l P Q R : P ∨ Q ∧ R ⊣⊢ (P ∨ Q) ∧ (P ∨ R).
-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 ⊣⊢ (P ∨ R) ∧ (Q ∨ R).
-Proof. by rewrite -!(comm _ R) or_and_l. Qed.
-Lemma and_or_l P Q R : P ∧ (Q ∨ R) ⊣⊢ P ∧ Q ∨ P ∧ R.
-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 ⊣⊢ P ∧ R ∨ Q ∧ R.
-Proof. by rewrite -!(comm _ R) and_or_l. Qed.
-Lemma and_exist_l {A} P (Ψ : A → uPred M) : P ∧ (∃ a, Ψ a) ⊣⊢ ∃ a, P ∧ Ψ a.
-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 ⊣⊢ ∃ a, Φ a ∧ P.
-Proof.
-  rewrite -(comm _ P) and_exist_l. apply exist_proper=>a. by rewrite comm.
-Qed.
-
-Lemma pure_intro_l φ Q R : φ → (■ φ ∧ Q ⊢ R) → Q ⊢ R.
-Proof. intros ? <-; auto using pure_intro. Qed.
-Lemma pure_intro_r φ Q R : φ → (Q ∧ ■ φ ⊢ R) → Q ⊢ R.
-Proof. intros ? <-; auto using pure_intro. Qed.
-Lemma pure_intro_impl φ Q R : φ → (Q ⊢ ■ φ → R) → Q ⊢ R.
-Proof. intros ? ->. eauto using pure_intro_l, impl_elim_r. Qed.
-Lemma pure_elim_l φ Q R : (φ → Q ⊢ R) → ■ φ ∧ Q ⊢ R.
-Proof. intros; apply pure_elim with φ; eauto. Qed.
-Lemma pure_elim_r φ Q R : (φ → Q ⊢ R) → Q ∧ ■ φ ⊢ R.
-Proof. intros; apply pure_elim with φ; eauto. Qed.
-Lemma pure_equiv (φ : Prop) : φ → ■ φ ⊣⊢ True.
-Proof. intros; apply (anti_symm _); auto using pure_intro. Qed.
-
-Lemma eq_refl' {A : cofeT} (a : A) P : P ⊢ a ≡ a.
-Proof. rewrite (True_intro P). apply eq_refl. Qed.
-Hint Resolve eq_refl'.
-Lemma equiv_eq {A : cofeT} P (a b : A) : a ≡ b → P ⊢ a ≡ b.
-Proof. by intros ->. Qed.
-Lemma eq_sym {A : cofeT} (a b : A) : a ≡ b ⊢ b ≡ a.
-Proof. apply (eq_rewrite a b (λ b, b ≡ a)%I); auto. solve_proper. Qed.
-Lemma eq_iff P Q : P ≡ Q ⊢ P ↔ Q.
-Proof.
-  apply (eq_rewrite P Q (λ Q, P ↔ Q))%I; first solve_proper; auto using iff_refl.
-Qed.
-
-(* BI connectives *)
-Lemma sep_mono P P' Q Q' : (P ⊢ Q) → (P' ⊢ Q') → P ★ P' ⊢ Q ★ Q'.
-Proof.
-  intros HQ HQ'; unseal.
-  split; intros n' x ? (x1&x2&?&?&?); exists x1,x2; cofe_subst x;
-    eauto 7 using cmra_validN_op_l, cmra_validN_op_r, uPred_in_entails.
-Qed.
-Global Instance True_sep : LeftId (⊣⊢) True%I (@uPred_sep M).
-Proof.
-  intros P; unseal; split=> n x Hvalid; split.
-  - intros (x1&x2&?&_&?); cofe_subst; eauto using uPred_mono, cmra_includedN_r.
-  - by intros ?; exists (core x), x; rewrite cmra_core_l.
-Qed. 
-Global Instance sep_comm : Comm (⊣⊢) (@uPred_sep M).
-Proof.
-  by intros P Q; unseal; split=> 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; unseal; split=> 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.
-  unseal=> HPQR; split=> n x ?? n' x' ???; apply HPQR; auto.
-  exists x, x'; split_and?; auto.
-  eapply uPred_closed with n; eauto using cmra_validN_op_l.
-Qed.
-Lemma wand_elim_l' P Q R : (P ⊢ Q -★ R) → P ★ Q ⊢ R.
-Proof.
-  unseal =>HPQR. split; intros n x ? (?&?&?&?&?). cofe_subst.
-  eapply HPQR; eauto using cmra_validN_op_l.
-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. by 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_l P Q : (P -★ Q) ★ P ⊢ Q.
-Proof. by apply wand_elim_l'. Qed.
-Lemma wand_elim_r P Q : P ★ (P -★ Q) ⊢ Q.
-Proof. rewrite (comm _ P); 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 wand_apply_l P Q Q' R R' : (P ⊢ Q' -★ R') → (R' ⊢ R) → (Q ⊢ Q') → P ★ Q ⊢ R.
-Proof. intros -> -> <-; apply wand_elim_l. Qed.
-Lemma wand_apply_r P Q Q' R R' : (P ⊢ Q' -★ R') → (R' ⊢ R) → (Q ⊢ Q') → Q ★ P ⊢ R.
-Proof. intros -> -> <-; apply wand_elim_r. Qed.
-Lemma wand_apply_l' P Q Q' R : (P ⊢ Q' -★ R) → (Q ⊢ Q') → P ★ Q ⊢ R.
-Proof. intros -> <-; apply wand_elim_l. Qed.
-Lemma wand_apply_r' P Q Q' R : (P ⊢ Q' -★ R) → (Q ⊢ Q') → Q ★ P ⊢ R.
-Proof. intros -> <-; apply wand_elim_r. Qed.
-Lemma wand_frame_l P Q R : (Q -★ R) ⊢ P ★ Q -★ P ★ R.
-Proof. apply wand_intro_l. rewrite -assoc. apply sep_mono_r, wand_elim_r. Qed.
-Lemma wand_frame_r P Q R : (Q -★ R) ⊢ Q ★ P -★ R ★ P.
-Proof.
-  apply wand_intro_l. rewrite ![(_ ★ P)%I]comm -assoc.
-  apply sep_mono_r, wand_elim_r.
-Qed.
-Lemma wand_diag P : (P -★ P) ⊣⊢ True.
-Proof. apply (anti_symm _); auto. apply wand_intro_l; by rewrite right_id. Qed.
-Lemma wand_True P : (True -★ P) ⊣⊢ P.
-Proof.
-  apply (anti_symm _); last by auto using wand_intro_l.
-  eapply sep_elim_True_l; first reflexivity. by rewrite wand_elim_r.
-Qed.
-Lemma wand_entails P Q : (True ⊢ P -★ Q) → P ⊢ Q.
-Proof.
-  intros HPQ. eapply sep_elim_True_r; first exact: HPQ. by rewrite wand_elim_r.
-Qed.
-Lemma entails_wand P Q : (P ⊢ Q) → True ⊢ P -★ Q.
-Proof. auto using wand_intro_l. Qed.
-Lemma wand_curry P Q R : (P -★ Q -★ R) ⊣⊢ (P ★ Q -★ R).
-Proof.
-  apply (anti_symm _).
-  - apply wand_intro_l. by rewrite (comm _ P) -assoc !wand_elim_r.
-  - do 2 apply wand_intro_l. by rewrite assoc (comm _ Q) 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 pure_elim_sep_l φ Q R : (φ → Q ⊢ R) → ■ φ ★ Q ⊢ R.
-Proof. intros; apply pure_elim with φ; eauto. Qed.
-Lemma pure_elim_sep_r φ Q R : (φ → Q ⊢ R) → Q ★ ■ φ ⊢ R.
-Proof. intros; apply pure_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) ⊣⊢ (P ★ Q) ∨ (P ★ R).
-Proof.
-  apply (anti_symm (⊢)); last by eauto 8.
-  apply wand_elim_r', or_elim; apply wand_intro_l; auto.
-Qed.
-Lemma sep_or_r P Q R : (P ∨ Q) ★ R ⊣⊢ (P ★ R) ∨ (Q ★ R).
-Proof. by rewrite -!(comm _ R) sep_or_l. Qed.
-Lemma sep_exist_l {A} P (Ψ : A → uPred M) : P ★ (∃ a, Ψ a) ⊣⊢ ∃ a, P ★ Ψ a.
-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 ⊣⊢ ∃ a, Φ a ★ Q.
-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.
-
-(* Always *)
-Lemma always_pure φ : □ ■ φ ⊣⊢ ■ φ.
-Proof. by unseal. Qed.
-Lemma always_elim P : □ P ⊢ P.
-Proof.
-  unseal; split=> n x ? /=.
-  eauto using uPred_mono, @cmra_included_core, cmra_included_includedN.
-Qed.
-Lemma always_intro' P Q : (□ P ⊢ Q) → □ P ⊢ □ Q.
-Proof.
-  unseal=> HPQ; split=> n x ??; apply HPQ; simpl; auto using @cmra_core_validN.
-  by rewrite cmra_core_idemp.
-Qed.
-Lemma always_and P Q : □ (P ∧ Q) ⊣⊢ □ P ∧ □ Q.
-Proof. by unseal. Qed.
-Lemma always_or P Q : □ (P ∨ Q) ⊣⊢ □ P ∨ □ Q.
-Proof. by unseal. Qed.
-Lemma always_forall {A} (Ψ : A → uPred M) : (□ ∀ a, Ψ a) ⊣⊢ (∀ a, □ Ψ a).
-Proof. by unseal. Qed.
-Lemma always_exist {A} (Ψ : A → uPred M) : (□ ∃ a, Ψ a) ⊣⊢ (∃ a, □ Ψ a).
-Proof. by unseal. Qed.
-Lemma always_and_sep_1 P Q : □ (P ∧ Q) ⊢ □ (P ★ Q).
-Proof.
-  unseal; split=> n x ? [??].
-  exists (core x), (core x); rewrite -cmra_core_dup; auto.
-Qed.
-Lemma always_and_sep_l_1 P Q : □ P ∧ Q ⊢ □ P ★ Q.
-Proof.
-  unseal; split=> n x ? [??]; exists (core x), x; simpl in *.
-  by rewrite cmra_core_l cmra_core_idemp.
-Qed.
-Lemma always_later P : □ ▷ P ⊣⊢ ▷ □ P.
-Proof. by unseal. 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.
-Global Instance always_flip_mono' :
-  Proper (flip (⊢) ==> flip (⊢)) (@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) ⊣⊢ a ≡ b.
-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 a) always_pure; auto.
-Qed.
-Lemma always_and_sep P Q : □ (P ∧ Q) ⊣⊢ □ (P ★ Q).
-Proof. apply (anti_symm (⊢)); auto using always_and_sep_1. Qed.
-Lemma always_and_sep_l' P Q : □ P ∧ Q ⊣⊢ □ P ★ Q.
-Proof. apply (anti_symm (⊢)); auto using always_and_sep_l_1. Qed.
-Lemma always_and_sep_r' P Q : P ∧ □ Q ⊣⊢ P ★ □ Q.
-Proof. by rewrite !(comm _ P) always_and_sep_l'. Qed.
-Lemma always_sep P Q : □ (P ★ Q) ⊣⊢ □ P ★ □ Q.
-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 ⊣⊢ □ P ★ □ P.
-Proof. by rewrite -always_sep -always_and_sep (idemp _). Qed.
-Lemma always_wand_impl P Q : □ (P -★ Q) ⊣⊢ □ (P → Q).
-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.
-
-Global Instance always_if_ne n p : Proper (dist n ==> dist n) (@uPred_always_if M p).
-Proof. solve_proper. Qed.
-Global Instance always_if_proper p : Proper ((⊣⊢) ==> (⊣⊢)) (@uPred_always_if M p).
-Proof. solve_proper. Qed.
-Global Instance always_if_mono p : Proper ((⊢) ==> (⊢)) (@uPred_always_if M p).
-Proof. solve_proper. Qed.
-
-Lemma always_if_elim p P : □?p P ⊢ P.
-Proof. destruct p; simpl; auto using always_elim. Qed.
-Lemma always_elim_if p P : □ P ⊢ □?p P.
-Proof. destruct p; simpl; auto using always_elim. Qed.
-Lemma always_if_and p P Q : □?p (P ∧ Q) ⊣⊢ □?p P ∧ □?p Q.
-Proof. destruct p; simpl; auto using always_and. Qed.
-Lemma always_if_or p P Q : □?p (P ∨ Q) ⊣⊢ □?p P ∨ □?p Q.
-Proof. destruct p; simpl; auto using always_or. Qed.
-Lemma always_if_exist {A} p (Ψ : A → uPred M) : (□?p ∃ a, Ψ a) ⊣⊢ ∃ a, □?p Ψ a.
-Proof. destruct p; simpl; auto using always_exist. Qed.
-Lemma always_if_sep p P Q : □?p (P ★ Q) ⊣⊢ □?p P ★ □?p Q.
-Proof. destruct p; simpl; auto using always_sep. Qed.
-Lemma always_if_later p P : □?p ▷ P ⊣⊢ ▷ □?p P.
-Proof. destruct p; simpl; auto using always_later. Qed.
-
-(* Later *)
-Lemma later_mono P Q : (P ⊢ Q) → ▷ P ⊢ ▷ Q.
-Proof.
-  unseal=> HP; split=>-[|n] x ??; [done|apply HP; eauto using cmra_validN_S].
-Qed.
-Lemma later_intro P : P ⊢ ▷ P.
-Proof.
-  unseal; split=> -[|n] x ??; simpl in *; [done|].
-  apply uPred_closed with (S n); eauto using cmra_validN_S.
-Qed.
-Lemma löb P : (▷ P → P) ⊢ P.
-Proof.
-  unseal; split=> n x ? HP; induction n as [|n IH]; [by apply HP|].
-  apply HP, IH, uPred_closed with (S n); eauto using cmra_validN_S.
-Qed.
-Lemma later_and P Q : ▷ (P ∧ Q) ⊣⊢ ▷ P ∧ ▷ Q.
-Proof. unseal; split=> -[|n] x; by split. Qed.
-Lemma later_or P Q : ▷ (P ∨ Q) ⊣⊢ ▷ P ∨ ▷ Q.
-Proof. unseal; split=> -[|n] x; simpl; tauto. Qed.
-Lemma later_forall {A} (Φ : A → uPred M) : (▷ ∀ a, Φ a) ⊣⊢ (∀ a, ▷ Φ a).
-Proof. unseal; by split=> -[|n] x. Qed.
-Lemma later_exist_1 {A} (Φ : A → uPred M) : (∃ a, ▷ Φ a) ⊢ (▷ ∃ a, Φ a).
-Proof. unseal; by split=> -[|[|n]] x. Qed.
-Lemma later_exist_2 `{Inhabited A} (Φ : A → uPred M) : (▷ ∃ a, Φ a) ⊢ ∃ a, ▷ Φ a.
-Proof. unseal; split=> -[|[|n]] x; done || by exists inhabitant. Qed.
-Lemma later_sep P Q : ▷ (P ★ Q) ⊣⊢ ▷ P ★ ▷ Q.
-Proof.
-  unseal; split=> n x ?; split.
-  - destruct n as [|n]; simpl.
-    { by exists x, (core x); rewrite cmra_core_r. }
-    intros (x1&x2&Hx&?&?); destruct (cmra_extend 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.
-Global Instance later_flip_mono' :
-  Proper (flip (⊢) ==> flip (⊢)) (@uPred_later M).
-Proof. intros P Q; apply later_mono. Qed.
-Lemma later_True : ▷ True ⊣⊢ True.
-Proof. apply (anti_symm (⊢)); auto using later_intro. 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_exist `{Inhabited A} (Φ : A → uPred M) :
-  ▷ (∃ a, Φ a) ⊣⊢ (∃ a, ▷ Φ a).
-Proof. apply: anti_symm; eauto using later_exist_2, later_exist_1. 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.
-
-(* Own *)
-Lemma ownM_op (a1 a2 : M) :
-  uPred_ownM (a1 ⋅ a2) ⊣⊢ uPred_ownM a1 ★ uPred_ownM a2.
-Proof.
-  unseal; split=> n x ?; split.
-  - intros [z ?]; exists a1, (a2 ⋅ z); split; [by rewrite (assoc op)|].
-    split. by exists (core a1); rewrite cmra_core_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 (a : M) : Persistent a → □ uPred_ownM a ⊣⊢ uPred_ownM a.
-Proof.
-  split=> n x /=; split; [by apply always_elim|unseal; intros Hx]; simpl.
-  rewrite -(persistent_core a). by apply cmra_core_preservingN.
-Qed.
-Lemma ownM_something : True ⊢ ∃ a, uPred_ownM a.
-Proof. unseal; split=> n x ??. by exists x; simpl. Qed.
-Lemma ownM_empty : True ⊢ uPred_ownM ∅.
-Proof. unseal; split=> n x ??; by  exists x; rewrite left_id. Qed.
-
-(* Valid *)
-Lemma ownM_valid (a : M) : uPred_ownM a ⊢ ✓ a.
-Proof.
-  unseal; split=> n x Hv [a' ?]; cofe_subst; eauto using cmra_validN_op_l.
-Qed.
-Lemma valid_intro {A : cmraT} (a : A) : ✓ a → True ⊢ ✓ a.
-Proof. unseal=> ?; split=> n x ? _ /=; by apply cmra_valid_validN. Qed.
-Lemma valid_elim {A : cmraT} (a : A) : ¬ ✓{0} a → ✓ a ⊢ False.
-Proof. unseal=> Ha; split=> n x ??; apply Ha, cmra_validN_le with n; auto. Qed.
-Lemma always_valid {A : cmraT} (a : A) : □ ✓ a ⊣⊢ ✓ a.
-Proof. by unseal. Qed.
-Lemma valid_weaken {A : cmraT} (a b : A) : ✓ (a ⋅ b) ⊢ ✓ a.
-Proof. unseal; split=> 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 a b [b' ->]. rewrite ownM_op. eauto. Qed.
-
-(* Products *)
-Lemma prod_equivI {A B : cofeT} (x y : A * B) : x ≡ y ⊣⊢ x.1 ≡ y.1 ∧ x.2 ≡ y.2.
-Proof. by unseal. Qed.
-Lemma prod_validI {A B : cmraT} (x : A * B) : ✓ x ⊣⊢ ✓ x.1 ∧ ✓ x.2.
-Proof. by unseal. Qed.
-
-(* Later *)
-Lemma later_equivI {A : cofeT} (x y : later A) :
-  x ≡ y ⊣⊢ ▷ (later_car x ≡ later_car y).
-Proof. by unseal. Qed.
-
-(* Discrete *)
-Lemma discrete_valid {A : cmraT} `{!CMRADiscrete A} (a : A) : ✓ a ⊣⊢ ■ ✓ a.
-Proof. unseal; split=> n x _. by rewrite /= -cmra_discrete_valid_iff. Qed.
-Lemma timeless_eq {A : cofeT} (a b : A) : Timeless a → a ≡ b ⊣⊢ ■ (a ≡ b).
-Proof.
-  unseal=> ?. apply (anti_symm (⊢)); split=> n x ?; by apply (timeless_iff n).
-Qed.
-
-(* Option *)
-Lemma option_equivI {A : cofeT} (mx my : option A) :
-  mx ≡ my ⊣⊢ match mx, my with
-             | Some x, Some y => x ≡ y | None, None => True | _, _ => False
-             end.
-Proof.
-  uPred.unseal. do 2 split. by destruct 1. by destruct mx, my; try constructor.
-Qed.
-Lemma option_validI {A : cmraT} (mx : option A) :
-  ✓ mx ⊣⊢ match mx with Some x => ✓ x | None => True end.
-Proof. uPred.unseal. by destruct mx. 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.
-    move: HP; rewrite /TimelessP; unseal=> /uPred_in_entails /(_ (S n) x).
-    by destruct 1; auto using cmra_validN_S.
-  - move=> HP; rewrite /TimelessP; unseal; split=> -[|n] x /=; auto; left.
-    apply HP, uPred_closed with n; eauto using cmra_validN_le.
-Qed.
-
-Global Instance pure_timeless φ : TimelessP (■ φ : uPred M)%I.
-Proof. by apply timelessP_spec; unseal => -[|n] x. Qed.
-Global Instance valid_timeless {A : cmraT} `{CMRADiscrete A} (a : A) :
-   TimelessP (✓ a : uPred M)%I.
-Proof.
-  apply timelessP_spec; unseal=> n x /=. by rewrite -!cmra_discrete_valid_iff.
-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 _) (timelessP Q); eauto 10.
-Qed.
-Global Instance impl_timeless P Q : TimelessP Q → TimelessP (P → Q).
-Proof.
-  rewrite !timelessP_spec; unseal=> HP [|n] x ? HPQ [|n'] x' ????; auto.
-  apply HP, HPQ, uPred_closed with (S n'); 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; unseal=> HP [|n] x ? HPQ [|n'] x' ???; auto.
-  apply HP, HPQ, uPred_closed with (S n');
-    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; unseal=> 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; unseal=> 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_pure -!always_later -always_or; apply always_mono.
-Qed.
-Global Instance always_if_timeless p P : TimelessP P → TimelessP (□?p P).
-Proof. destruct p; apply _. Qed.
-Global Instance eq_timeless {A : cofeT} (a b : A) :
-  Timeless a → TimelessP (a ≡ b : uPred M)%I.
-Proof.
-  intro; apply timelessP_spec; unseal=> n x ??; by apply equiv_dist, timeless.
-Qed.
-Global Instance ownM_timeless (a : M) : Timeless a → TimelessP (uPred_ownM a).
-Proof.
-  intro; apply timelessP_spec; unseal=> n x ??; apply cmra_included_includedN,
-    cmra_timeless_included_l; eauto using cmra_validN_le.
-Qed.
-
-(* Persistence *)
-Global Instance pure_persistent φ : PersistentP (■ φ : uPred M)%I.
-Proof. by rewrite /PersistentP always_pure. Qed.
-Global Instance always_persistent P : PersistentP (□ P).
-Proof. by intros; apply always_intro'. Qed.
-Global Instance and_persistent P Q :
-  PersistentP P → PersistentP Q → PersistentP (P ∧ Q).
-Proof. by intros; rewrite /PersistentP always_and; apply and_mono. Qed.
-Global Instance or_persistent P Q :
-  PersistentP P → PersistentP Q → PersistentP (P ∨ Q).
-Proof. by intros; rewrite /PersistentP always_or; apply or_mono. Qed.
-Global Instance sep_persistent P Q :
-  PersistentP P → PersistentP Q → PersistentP (P ★ Q).
-Proof. by intros; rewrite /PersistentP always_sep; apply sep_mono. Qed.
-Global Instance forall_persistent {A} (Ψ : A → uPred M) :
-  (∀ x, PersistentP (Ψ x)) → PersistentP (∀ x, Ψ x).
-Proof. by intros; rewrite /PersistentP always_forall; apply forall_mono. Qed.
-Global Instance exist_persistent {A} (Ψ : A → uPred M) :
-  (∀ x, PersistentP (Ψ x)) → PersistentP (∃ x, Ψ x).
-Proof. by intros; rewrite /PersistentP always_exist; apply exist_mono. Qed.
-Global Instance eq_persistent {A : cofeT} (a b : A) :
-  PersistentP (a ≡ b : uPred M)%I.
-Proof. by intros; rewrite /PersistentP always_eq. Qed.
-Global Instance valid_persistent {A : cmraT} (a : A) :
-  PersistentP (✓ a : uPred M)%I.
-Proof. by intros; rewrite /PersistentP always_valid. Qed.
-Global Instance later_persistent P : PersistentP P → PersistentP (▷ P).
-Proof. by intros; rewrite /PersistentP always_later; apply later_mono. Qed.
-Global Instance ownM_persistent : Persistent a → PersistentP (@uPred_ownM M a).
-Proof. intros. by rewrite /PersistentP always_ownM. Qed.
-Global Instance from_option_persistent {A} P (Ψ : A → uPred M) (mx : option A) :
-  (∀ x, PersistentP (Ψ x)) → PersistentP P → PersistentP (from_option Ψ P mx).
-Proof. destruct mx; apply _. Qed.
-
-(* Derived lemmas for persistence *)
-Lemma always_always P `{!PersistentP P} : □ P ⊣⊢ P.
-Proof. apply (anti_symm (⊢)); auto using always_elim. Qed.
-Lemma always_if_always p P `{!PersistentP P} : □?p P ⊣⊢ P.
-Proof. destruct p; simpl; auto using always_always. Qed.
-Lemma always_intro P Q `{!PersistentP P} : (P ⊢ Q) → P ⊢ □ Q.
-Proof. rewrite -(always_always P); apply always_intro'. Qed.
-Lemma always_and_sep_l P Q `{!PersistentP P} : P ∧ Q ⊣⊢ P ★ Q.
-Proof. by rewrite -(always_always P) always_and_sep_l'. Qed.
-Lemma always_and_sep_r P Q `{!PersistentP Q} : P ∧ Q ⊣⊢ P ★ Q.
-Proof. by rewrite -(always_always Q) always_and_sep_r'. Qed.
-Lemma always_sep_dup P `{!PersistentP P} : P ⊣⊢ P ★ P.
-Proof. by rewrite -(always_always P) -always_sep_dup'. Qed.
-Lemma always_entails_l P Q `{!PersistentP Q} : (P ⊢ Q) → P ⊢ Q ★ P.
-Proof. by rewrite -(always_always Q); apply always_entails_l'. Qed.
-Lemma always_entails_r P Q `{!PersistentP Q} : (P ⊢ Q) → P ⊢ P ★ Q.
-Proof. by rewrite -(always_always Q); apply always_entails_r'. Qed.
-End uPred_logic.
-
-(* Hint DB for the logic *)
-Hint Resolve pure_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 iris.algebra Require Export upred list.
-From iris.prelude Require Import gmap fin_collections functions.
-Import uPred.
-
-(** We define the following big operators:
-
-- The operators [ [★] Ps ] and [ [∧] Ps ] fold [★] and [∧] over the list [Ps].
-  This operator is not a quantifier, so it binds strongly.
-- The operator [ [★ map] k ↦ x ∈ m, P ] asserts that [P] holds separately for
-  each [k ↦ x] in the map [m]. This operator is a quantifier, and thus has the
-  same precedence as [∀] and [∃].
-- The operator [ [★ set] x ∈ X, P ] asserts that [P] holds separately for each
-  [x] in the set [X]. This operator is a quantifier, and thus has the same
-  precedence as [∀] and [∃]. *)
-
-(** * 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 :=
-  [★] (curry Φ <$> map_to_list m).
-Instance: Params (@uPred_big_sepM) 6.
-Notation "'[★' 'map' ] k ↦ x ∈ m , P" := (uPred_big_sepM m (λ k x, P))
-  (at level 200, m at level 10, k, x at level 1, right associativity,
-   format "[★  map ]  k ↦ x  ∈  m ,  P") : uPred_scope.
-
-Definition uPred_big_sepS {M} `{Countable A}
-  (X : gset A) (Φ : A → uPred M) : uPred M := [★] (Φ <$> elements X).
-Instance: Params (@uPred_big_sepS) 5.
-Notation "'[★' 'set' ] x ∈ X , P" := (uPred_big_sepS X (λ x, P))
-  (at level 200, X at level 10, x at level 1, right associativity,
-   format "[★  set ]  x  ∈  X ,  P") : uPred_scope.
-
-(** * Persistence of lists of uPreds *)
-Class PersistentL {M} (Ps : list (uPred M)) :=
-  persistentL : Forall PersistentP Ps.
-Arguments persistentL {_} _ {_}.
-
-(** * Properties *)
-Section big_op.
-Context {M : ucmraT}.
-Implicit Types Ps Qs : list (uPred M).
-Implicit Types A : Type.
-
-(** ** Big ops over lists *)
-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 (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 (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).
-  - etrans; 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).
-  - etrans; eauto.
-Qed.
-
-Lemma big_and_app Ps Qs : [∧] (Ps ++ Qs) ⊣⊢ [∧] Ps ∧ [∧] Qs.
-Proof. induction Ps as [|?? IH]; by rewrite /= ?left_id -?assoc ?IH. Qed.
-Lemma big_sep_app Ps Qs : [★] (Ps ++ Qs) ⊣⊢ [★] Ps ★ [★] Qs.
-Proof. by induction Ps as [|?? IH]; rewrite /= ?left_id -?assoc ?IH. Qed.
-
-Lemma big_and_contains Ps Qs : Qs `contains` Ps → [∧] Ps ⊢ [∧] Qs.
-Proof.
-  intros [Ps' ->]%contains_Permutation. by rewrite big_and_app and_elim_l.
-Qed.
-Lemma big_sep_contains Ps Qs : Qs `contains` Ps → [★] Ps ⊢ [★] Qs.
-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 → (∀ k x, m2 !! k = Some x → Φ k x ⊢ Ψ k x) →
-    ([★ map] k ↦ x ∈ m1, Φ k x) ⊢ [★ map] k ↦ x ∈ m2, Ψ k x.
-  Proof.
-    intros HX HΦ. trans ([★ map] k↦x ∈ m2, Φ k x)%I.
-    - by apply big_sep_contains, fmap_contains, map_to_list_contains.
-    - apply big_sep_mono', Forall2_fmap, Forall_Forall2.
-      apply Forall_forall=> -[i x] ? /=. by apply HΦ, elem_of_map_to_list.
-  Qed.
-  Lemma big_sepM_proper Φ Ψ m1 m2 :
-    m1 ≡ m2 → (∀ k x, m1 !! k = Some x → m2 !! k = Some x → Φ k x ⊣⊢ Ψ k x) →
-    ([★ map] k ↦ x ∈ m1, Φ k x) ⊣⊢ ([★ map] k ↦ x ∈ m2, Ψ k x).
-  Proof.
-    (* FIXME: Coq bug since 8.5pl1. Without the @ in [@lookup_weaken] it gives
-    File "./algebra/upred_big_op.v", line 114, characters 4-131:
-    Anomaly: Uncaught exception Univ.AlreadyDeclared. Please report. *)
-    intros [??] ?; apply (anti_symm (⊢)); apply big_sepM_mono;
-      eauto using equiv_entails, equiv_entails_sym, @lookup_weaken.
-  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 Forall_Forall2, 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Φ. by apply big_sepM_proper; intros; last apply HΦ. Qed.
-  Global Instance big_sepM_mono' m :
-    Proper (pointwise_relation _ (pointwise_relation _ (⊢)) ==> (⊢))
-           (uPred_big_sepM (M:=M) m).
-  Proof. intros Φ1 Φ2 HΦ. by apply big_sepM_mono; intros; last apply HΦ. Qed.
-
-  Lemma big_sepM_empty Φ : ([★ map] k↦x ∈ ∅, Φ k x) ⊣⊢ True.
-  Proof. by rewrite /uPred_big_sepM map_to_list_empty. Qed.
-
-  Lemma big_sepM_insert Φ m i x :
-    m !! i = None →
-    ([★ map] k↦y ∈ <[i:=x]> m, Φ k y) ⊣⊢ Φ i x ★ [★ map] k↦y ∈ m, Φ k y.
-  Proof. intros ?; by rewrite /uPred_big_sepM map_to_list_insert. Qed.
-
-  Lemma big_sepM_delete Φ m i x :
-    m !! i = Some x →
-    ([★ map] k↦y ∈ m, Φ k y) ⊣⊢ Φ i x ★ [★ map] k↦y ∈ delete i m, Φ k y.
-  Proof.
-    intros. rewrite -big_sepM_insert ?lookup_delete //.
-    by rewrite insert_delete insert_id.
-  Qed.
-
-  Lemma big_sepM_lookup Φ m i x :
-    m !! i = Some x → ([★ map] k↦y ∈ m, Φ k y) ⊢ Φ i x.
-  Proof. intros. by rewrite big_sepM_delete // sep_elim_l. Qed.
-
-  Lemma big_sepM_singleton Φ i x : ([★ map] k↦y ∈ {[i:=x]}, Φ k y) ⊣⊢ Φ i x.
-  Proof.
-    rewrite -insert_empty big_sepM_insert/=; last auto using lookup_empty.
-    by rewrite big_sepM_empty right_id.
-  Qed.
-
-  Lemma big_sepM_fmap {B} (f : A → B) (Φ : K → B → uPred M) m :
-    ([★ map] k↦y ∈ f <$> m, Φ k y) ⊣⊢ ([★ map] k↦y ∈ m, Φ k (f y)).
-  Proof.
-    rewrite /uPred_big_sepM map_to_list_fmap -list_fmap_compose.
-    f_equiv; apply reflexive_eq, list_fmap_ext. by intros []. done.
-  Qed.
-
-  Lemma big_sepM_insert_override (Φ : K → uPred M) m i x y :
-    m !! i = Some x →
-    ([★ map] k↦_ ∈ <[i:=y]> m, Φ k) ⊣⊢ ([★ map] k↦_ ∈ m, Φ k).
-  Proof.
-    intros. rewrite -insert_delete big_sepM_insert ?lookup_delete //.
-    by rewrite -big_sepM_delete.
-  Qed.
-
-  Lemma big_sepM_fn_insert {B} (Ψ : K → A → B → uPred M) (f : K → B) m i x b :
-    m !! i = None →
-       ([★ map] k↦y ∈ <[i:=x]> m, Ψ k y (<[i:=b]> f k))
-    ⊣⊢ (Ψ i x b ★ [★ map] k↦y ∈ m, Ψ k y (f k)).
-  Proof.
-    intros. rewrite big_sepM_insert // fn_lookup_insert.
-    apply sep_proper, big_sepM_proper; auto=> k y ??.
-    by rewrite fn_lookup_insert_ne; last set_solver.
-  Qed.
-  Lemma big_sepM_fn_insert' (Φ : K → uPred M) m i x P :
-    m !! i = None →
-    ([★ map] k↦y ∈ <[i:=x]> m, <[i:=P]> Φ k) ⊣⊢ (P ★ [★ map] k↦y ∈ m, Φ k).
-  Proof. apply (big_sepM_fn_insert (λ _ _, id)). Qed.
-
-  Lemma big_sepM_sepM Φ Ψ m :
-       ([★ map] k↦x ∈ m, Φ k x ★ Ψ k x)
-    ⊣⊢ ([★ map] k↦x ∈ m, Φ k x) ★ ([★ map] k↦x ∈ m, Ψ k x).
-  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] k↦x ∈ m, Φ k x) ⊣⊢ ([★ map] k↦x ∈ m, ▷ Φ k x).
-  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.
-
-  Lemma big_sepM_always Φ m :
-    (□ [★ map] k↦x ∈ m, Φ k x) ⊣⊢ ([★ map] k↦x ∈ m, □ Φ k x).
-  Proof.
-    rewrite /uPred_big_sepM.
-    induction (map_to_list m) as [|[i x] l IH]; csimpl; rewrite ?always_pure //.
-    by rewrite always_sep IH.
-  Qed.
-
-  Lemma big_sepM_always_if p Φ m :
-    □?p ([★ map] k↦x ∈ m, Φ k x) ⊣⊢ ([★ map] k↦x ∈ m, □?p Φ k x).
-  Proof. destruct p; simpl; auto using big_sepM_always. Qed.
-
-  Lemma big_sepM_forall Φ m :
-    (∀ k x, PersistentP (Φ k x)) →
-    ([★ map] k↦x ∈ m, Φ k x) ⊣⊢ (∀ k x, m !! k = Some x → Φ k x).
-  Proof.
-    intros. apply (anti_symm _).
-    { apply forall_intro=> k; apply forall_intro=> x.
-      apply impl_intro_l, pure_elim_l=> ?; by apply big_sepM_lookup. }
-    rewrite /uPred_big_sepM. setoid_rewrite <-elem_of_map_to_list.
-    induction (map_to_list m) as [|[i x] l IH]; csimpl; auto.
-    rewrite -always_and_sep_l; apply and_intro.
-    - rewrite (forall_elim i) (forall_elim x) pure_equiv; last by left.
-      by rewrite True_impl.
-    - rewrite -IH. apply forall_mono=> k; apply forall_mono=> y.
-      apply impl_intro_l, pure_elim_l=> ?. rewrite pure_equiv; last by right.
-      by rewrite True_impl.
-  Qed.
-
-  Lemma big_sepM_impl Φ Ψ m :
-    □ (∀ k x, m !! k = Some x → Φ k x → Ψ k x) ∧ ([★ map] k↦x ∈ m, Φ k x)
-    ⊢ [★ map] k↦x ∈ m, Ψ k x.
-  Proof.
-    rewrite always_and_sep_l. do 2 setoid_rewrite always_forall.
-    setoid_rewrite always_impl; setoid_rewrite always_pure.
-    rewrite -big_sepM_forall -big_sepM_sepM. apply big_sepM_mono; auto=> k x ?.
-    by rewrite -always_wand_impl always_elim wand_elim_l.
-  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 ∈ X, Φ x) ⊢ [★ set] x ∈ Y, Ψ x.
-  Proof.
-    intros HX HΦ. trans ([★ set] x ∈ Y, Φ x)%I.
-    - by apply big_sep_contains, fmap_contains, elements_contains.
-    - apply big_sep_mono', Forall2_fmap, Forall_Forall2.
-      apply Forall_forall=> x ? /=. by apply HΦ, elem_of_elements.
-  Qed.
-  Lemma big_sepS_proper Φ Ψ X Y :
-    X ≡ Y → (∀ x, x ∈ X → x ∈ Y → Φ x ⊣⊢ Ψ x) →
-    ([★ set] x ∈ X, Φ x) ⊣⊢ ([★ set] x ∈ Y, Ψ x).
-  Proof.
-    intros [??] ?; apply (anti_symm (⊢)); apply big_sepS_mono;
-      eauto using equiv_entails, equiv_entails_sym.
-  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 Forall_Forall2, 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 big_sepS_proper; naive_solver. 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] x ∈ ∅, Φ x) ⊣⊢ True.
-  Proof. by rewrite /uPred_big_sepS elements_empty. Qed.
-
-  Lemma big_sepS_insert Φ X x :
-    x ∉ X → ([★ set] y ∈ {[ x ]} ∪ X, Φ y) ⊣⊢ (Φ x ★ [★ set] y ∈ X, Φ y).
-  Proof. intros. by rewrite /uPred_big_sepS elements_union_singleton. Qed.
-  Lemma big_sepS_fn_insert {B} (Ψ : A → B → uPred M) f X x b :
-    x ∉ X →
-       ([★ set] y ∈ {[ x ]} ∪ X, Ψ y (<[x:=b]> f y))
-    ⊣⊢ (Ψ x b ★ [★ set] y ∈ X, Ψ y (f y)).
-  Proof.
-    intros. rewrite big_sepS_insert // fn_lookup_insert.
-    apply sep_proper, big_sepS_proper; auto=> y ??.
-    by rewrite fn_lookup_insert_ne; last set_solver.
-  Qed.
-  Lemma big_sepS_fn_insert' Φ X x P :
-    x ∉ X → ([★ set] y ∈ {[ x ]} ∪ X, <[x:=P]> Φ y) ⊣⊢ (P ★ [★ set] y ∈ X, Φ y).
-  Proof. apply (big_sepS_fn_insert (λ y, id)). Qed.
-
-  Lemma big_sepS_delete Φ X x :
-    x ∈ X → ([★ set] y ∈ X, Φ y) ⊣⊢ Φ x ★ [★ set] y ∈ X ∖ {[ x ]}, Φ y.
-  Proof.
-    intros. rewrite -big_sepS_insert; last set_solver.
-    by rewrite -union_difference_L; last set_solver.
-  Qed.
-
-  Lemma big_sepS_elem_of Φ X x : x ∈ X → ([★ set] y ∈ X, Φ y) ⊢ Φ x.
-  Proof. intros. by rewrite big_sepS_delete // sep_elim_l. Qed.
-
-  Lemma big_sepS_singleton Φ x : ([★ set] y ∈ {[ x ]}, Φ y) ⊣⊢ Φ x.
-  Proof. intros. by rewrite /uPred_big_sepS elements_singleton /= right_id. Qed.
-
-  Lemma big_sepS_sepS Φ Ψ X :
-    ([★ set] y ∈ X, Φ y ★ Ψ y) ⊣⊢ ([★ set] y ∈ X, Φ y) ★ ([★ set] y ∈ X, Ψ y).
-  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] y ∈ X, Φ y) ⊣⊢ ([★ set] y ∈ X, ▷ Φ y).
-  Proof.
-    rewrite /uPred_big_sepS.
-    induction (elements X) as [|x l IH]; csimpl; first by rewrite ?later_True.
-    by rewrite later_sep IH.
-  Qed.
-
-  Lemma big_sepS_always Φ X : □ ([★ set] y ∈ X, Φ y) ⊣⊢ ([★ set] y ∈ X, □ Φ y).
-  Proof.
-    rewrite /uPred_big_sepS.
-    induction (elements X) as [|x l IH]; csimpl; first by rewrite ?always_pure.
-    by rewrite always_sep IH.
-  Qed.
-
-  Lemma big_sepS_always_if q Φ X :
-    □?q ([★ set] y ∈ X, Φ y) ⊣⊢ ([★ set] y ∈ X, □?q Φ y).
-  Proof. destruct q; simpl; auto using big_sepS_always. Qed.
-
-  Lemma big_sepS_forall Φ X :
-    (∀ x, PersistentP (Φ x)) → ([★ set] x ∈ X, Φ x) ⊣⊢ (∀ x, ■ (x ∈ X) → Φ x).
-  Proof.
-    intros. apply (anti_symm _).
-    { apply forall_intro=> x.
-      apply impl_intro_l, pure_elim_l=> ?; by apply big_sepS_elem_of. }
-    rewrite /uPred_big_sepS. setoid_rewrite <-elem_of_elements.
-    induction (elements X) as [|x l IH]; csimpl; auto.
-    rewrite -always_and_sep_l; apply and_intro.
-    - rewrite (forall_elim x) pure_equiv; last by left. by rewrite True_impl.
-    - rewrite -IH. apply forall_mono=> y.
-      apply impl_intro_l, pure_elim_l=> ?. rewrite pure_equiv; last by right.
-      by rewrite True_impl.
-  Qed.
-
-  Lemma big_sepS_impl Φ Ψ X :
-      □ (∀ x, ■ (x ∈ X) → Φ x → Ψ x) ∧ ([★ set] x ∈ X, Φ x) ⊢ [★ set] x ∈ X, Ψ x.
-  Proof.
-    rewrite always_and_sep_l always_forall.
-    setoid_rewrite always_impl; setoid_rewrite always_pure.
-    rewrite -big_sepS_forall -big_sepS_sepS. apply big_sepS_mono; auto=> x ?.
-    by rewrite -always_wand_impl always_elim wand_elim_l.
-  Qed.
-End gset.
-
-(** ** Persistence *)
-Global Instance big_and_persistent Ps : PersistentL Ps → PersistentP ([∧] Ps).
-Proof. induction 1; apply _. Qed.
-Global Instance big_sep_persistent Ps : PersistentL Ps → PersistentP ([★] Ps).
-Proof. induction 1; apply _. Qed.
-
-Global Instance nil_persistent : PersistentL (@nil (uPred M)).
-Proof. constructor. Qed.
-Global Instance cons_persistent P Ps :
-  PersistentP P → PersistentL Ps → PersistentL (P :: Ps).
-Proof. by constructor. Qed.
-Global Instance app_persistent Ps Ps' :
-  PersistentL Ps → PersistentL Ps' → PersistentL (Ps ++ Ps').
-Proof. apply Forall_app_2. Qed.
-Global Instance zip_with_persistent {A B} (f : A → B → uPred M) xs ys :
-  (∀ x y, PersistentP (f x y)) → PersistentL (zip_with f xs ys).
-Proof.
-  unfold PersistentL=> ?; revert ys; induction xs=> -[|??]; constructor; auto.
-Qed.
-End big_op.

algebra/upred_hlist.v

-From iris.prelude Require Export hlist.
-From iris.algebra Require Export upred.
-Import uPred.
-
-Fixpoint uPred_hexist {M As} : himpl As (uPred M) → uPred M :=
-  match As return himpl As (uPred M) → uPred M with
-  | tnil => id
-  | tcons A As => λ Φ, ∃ x, uPred_hexist (Φ x)
-  end%I.
-Fixpoint uPred_hforall {M As} : himpl As (uPred M) → uPred M :=
-  match As return himpl As (uPred M) → uPred M with
-  | tnil => id
-  | tcons A As => λ Φ, ∀ x, uPred_hforall (Φ x)
-  end%I.
-
-Section hlist.
-Context {M : ucmraT}.
-
-Lemma hexist_exist {As B} (f : himpl As B) (Φ : B → uPred M) :
-  uPred_hexist (hcompose Φ f) ⊣⊢ ∃ xs : hlist As, Φ (f xs).
-Proof.
-  apply (anti_symm _).
-  - induction As as [|A As IH]; simpl.
-    + by rewrite -(exist_intro hnil) .
-    + apply exist_elim=> x; rewrite IH; apply exist_elim=> xs.
-      by rewrite -(exist_intro (hcons x xs)).
-  - apply exist_elim=> xs; induction xs as [|A As x xs IH]; simpl; auto.
-    by rewrite -(exist_intro x) IH.
-Qed.
-
-Lemma hforall_forall {As B} (f : himpl As B) (Φ : B → uPred M) :
-  uPred_hforall (hcompose Φ f) ⊣⊢ ∀ xs : hlist As, Φ (f xs).
-Proof.
-  apply (anti_symm _).
-  - apply forall_intro=> xs; induction xs as [|A As x xs IH]; simpl; auto.
-    by rewrite (forall_elim x) IH.
-  - induction As as [|A As IH]; simpl.
-    + by rewrite (forall_elim hnil) .
-    + apply forall_intro=> x; rewrite -IH; apply forall_intro=> xs.
-      by rewrite (forall_elim (hcons x xs)).
-Qed.
-End hlist.

algebra/upred_tactics.v

-From iris.prelude Require Import gmap.
-From iris.algebra Require Export upred.
-From iris.algebra Require Export upred_big_op.
-Import uPred.
-
-Module uPred_reflection. Section uPred_reflection.
-  Context {M : ucmraT}.
-
-  Inductive expr :=
-    | ETrue : expr
-    | EVar : nat → expr
-    | ESep : expr → expr → expr.
-  Fixpoint eval (Σ : list (uPred M)) (e : expr) : uPred M :=
-    match e with
-    | ETrue => True
-    | EVar n => from_option id True%I (Σ !! n)
-    | ESep e1 e2 => eval Σ e1 ★ eval Σ e2
-    end.
-  Fixpoint flatten (e : expr) : list nat :=
-    match e with
-    | ETrue => []
-    | EVar n => [n]
-    | ESep e1 e2 => flatten e1 ++ flatten e2
-    end.
-
-  Notation eval_list Σ l := ([★] ((λ n, from_option id True%I (Σ !! n)) <$> l))%I.
-  Lemma eval_flatten Σ e : eval Σ e ⊣⊢ eval_list Σ (flatten e).
-  Proof.
-    induction e as [| |e1 IH1 e2 IH2];
-      rewrite /= ?right_id ?fmap_app ?big_sep_app ?IH1 ?IH2 //. 
-  Qed.
-  Lemma flatten_entails Σ e1 e2 :
-    flatten e2 `contains` flatten e1 → eval Σ e1 ⊢ eval Σ e2.
-  Proof.
-    intros. rewrite !eval_flatten. by apply big_sep_contains, fmap_contains.
-  Qed.
-  Lemma flatten_equiv Σ e1 e2 :
-    flatten e2 ≡ₚ flatten e1 → eval Σ e1 ⊣⊢ eval Σ e2.
-  Proof. intros He. by rewrite !eval_flatten He. Qed.
-
-  Fixpoint prune (e : expr) : expr :=
-    match e with
-    | ETrue => ETrue
-    | EVar n => EVar n
-    | ESep e1 e2 =>
-       match prune e1, prune e2 with
-       | ETrue, e2' => e2'
-       | e1', ETrue => e1'
-       | e1', e2' => ESep e1' e2'
-       end
-    end.
-  Lemma flatten_prune e : flatten (prune e) = flatten e.
-  Proof.
-    induction e as [| |e1 IH1 e2 IH2]; simplify_eq/=; auto.
-    rewrite -IH1 -IH2. by repeat case_match; rewrite ?right_id_L.
-  Qed.
-  Lemma prune_correct Σ e : eval Σ (prune e) ⊣⊢ eval Σ e.
-  Proof. by rewrite !eval_flatten flatten_prune. Qed.
-
-  Fixpoint cancel_go (n : nat) (e : expr) : option expr :=
-    match e with
-    | ETrue => None
-    | EVar n' => if decide (n = n') then Some ETrue else None
-    | ESep e1 e2 => 
-       match cancel_go n e1 with
-       | Some e1' => Some (ESep e1' e2)
-       | None => ESep e1 <$> cancel_go n e2
-       end
-    end.
-  Definition cancel (ns : list nat) (e: expr) : option expr :=
-    prune <$> fold_right (mbind ∘ cancel_go) (Some e) ns.
-  Lemma flatten_cancel_go e e' n :
-    cancel_go n e = Some e' → flatten e ≡ₚ n :: flatten e'.
-  Proof.
-    revert e'; induction e as [| |e1 IH1 e2 IH2]; intros;
-      repeat (simplify_option_eq || case_match); auto.
-    - by rewrite IH1 //.
-    - by rewrite IH2 // Permutation_middle.
-  Qed.
-  Lemma flatten_cancel e e' ns :
-    cancel ns e = Some e' → flatten e ≡ₚ ns ++ flatten e'.
-  Proof.
-    rewrite /cancel fmap_Some=> -[{e'}e' [He ->]]; rewrite flatten_prune.
-    revert e' He; induction ns as [|n ns IH]=> e' He; simplify_option_eq; auto.
-    rewrite Permutation_middle -flatten_cancel_go //; eauto.
-  Qed.
-  Lemma cancel_entails Σ e1 e2 e1' e2' ns :
-    cancel ns e1 = Some e1' → cancel ns e2 = Some e2' →
-    (eval Σ e1' ⊢ eval Σ e2') → eval Σ e1 ⊢ eval Σ e2.
-  Proof.
-    intros ??. rewrite !eval_flatten.
-    rewrite (flatten_cancel e1 e1' ns) // (flatten_cancel e2 e2' ns) //; csimpl.
-    rewrite !fmap_app !big_sep_app. apply sep_mono_r.
-  Qed.
-
-  Fixpoint to_expr (l : list nat) : expr :=
-    match l with
-    | [] => ETrue
-    | [n] => EVar n
-    | n :: l => ESep (EVar n) (to_expr l)
-    end.
-  Arguments to_expr !_ / : simpl nomatch.
-  Lemma eval_to_expr Σ l : eval Σ (to_expr l) ⊣⊢ eval_list Σ l.
-  Proof.
-    induction l as [|n1 [|n2 l] IH]; csimpl; rewrite ?right_id //.
-    by rewrite IH.
-  Qed.
-
-  Lemma split_l Σ e ns e' :
-    cancel ns e = Some e' → eval Σ e ⊣⊢ (eval Σ (to_expr ns) ★ eval Σ e').
-  Proof.
-    intros He%flatten_cancel.
-    by rewrite eval_flatten He fmap_app big_sep_app eval_to_expr eval_flatten.
-  Qed.
-  Lemma split_r Σ e ns e' :
-    cancel ns e = Some e' → eval Σ e ⊣⊢ (eval Σ e' ★ eval Σ (to_expr ns)).
-  Proof. intros. rewrite /= comm. by apply split_l. Qed.
-
-  Class Quote (Σ1 Σ2 : list (uPred M)) (P : uPred M) (e : expr) := {}.
-  Global Instance quote_True Σ : Quote Σ Σ True ETrue.
-  Global Instance quote_var Σ1 Σ2 P i:
-    rlist.QuoteLookup Σ1 Σ2 P i → Quote Σ1 Σ2 P (EVar i) | 1000.
-  Global Instance quote_sep Σ1 Σ2 Σ3 P1 P2 e1 e2 :
-    Quote Σ1 Σ2 P1 e1 → Quote Σ2 Σ3 P2 e2 → Quote Σ1 Σ3 (P1 ★ P2) (ESep e1 e2).
-
-  Class QuoteArgs (Σ: list (uPred M)) (Ps: list (uPred M)) (ns: list nat) := {}.
-  Global Instance quote_args_nil Σ : QuoteArgs Σ nil nil.
-  Global Instance quote_args_cons Σ Ps P ns n :
-    rlist.QuoteLookup Σ Σ P n →
-    QuoteArgs Σ Ps ns → QuoteArgs Σ (P :: Ps) (n :: ns).
-  End uPred_reflection.
-
-  Ltac quote :=
-    match goal with
-    | |- ?P1 ⊢ ?P2 =>
-      lazymatch type of (_ : Quote [] _ P1 _) with Quote _ ?Σ2 _ ?e1 =>
-      lazymatch type of (_ : Quote Σ2 _ P2 _) with Quote _ ?Σ3 _ ?e2 =>
-        change (eval Σ3 e1 ⊢ eval Σ3 e2) end end
-    end.
-  Ltac quote_l :=
-    match goal with
-    | |- ?P1 ⊢ ?P2 =>
-      lazymatch type of (_ : Quote [] _ P1 _) with Quote _ ?Σ2 _ ?e1 =>
-        change (eval Σ2 e1 ⊢ P2) end
-    end.
-End uPred_reflection.
-
-Tactic Notation "solve_sep_entails" :=
-  uPred_reflection.quote; apply uPred_reflection.flatten_entails;
-  apply (bool_decide_unpack _); vm_compute; exact Logic.I.
-
-Ltac close_uPreds Ps tac :=
-  let M := match goal with |- @uPred_entails ?M _ _ => M end in
-  let rec go Ps Qs :=
-    lazymatch Ps with
-    | [] => let Qs' := eval cbv [reverse rev_append] in (reverse Qs) in tac Qs'
-    | ?P :: ?Ps => find_pat P ltac:(fun Q => go Ps (Q :: Qs))
-    end in
-  (* avoid evars in case Ps = @nil ?A *)
-  try match Ps with [] => unify Ps (@nil (uPred M)) end;
-  go Ps (@nil (uPred M)).
-
-Tactic Notation "cancel" constr(Ps) :=
-  uPred_reflection.quote;
-  let Σ := match goal with |- uPred_reflection.eval ?Σ _ ⊢ _ => Σ end in
-  let ns' := lazymatch type of (_ : uPred_reflection.QuoteArgs Σ Ps _) with
-             | uPred_reflection.QuoteArgs _ _ ?ns' => ns'
-             end in
-  eapply uPred_reflection.cancel_entails with (ns:=ns');
-    [cbv; reflexivity|cbv; reflexivity|simpl].
-
-Tactic Notation "ecancel" open_constr(Ps) :=
-  close_uPreds Ps ltac:(fun Qs => cancel Qs).
-
-(** [to_front [P1, P2, ..]] rewrites in the premise of ⊢ such that
-    the assumptions P1, P2, ... appear at the front, in that order. *)
-Tactic Notation "to_front" open_constr(Ps) :=
-  close_uPreds Ps ltac:(fun Ps =>
-    uPred_reflection.quote_l;
-    let Σ := match goal with |- uPred_reflection.eval ?Σ _ ⊢ _ => Σ end in
-    let ns' := lazymatch type of (_ : uPred_reflection.QuoteArgs Σ Ps _) with
-               | uPred_reflection.QuoteArgs _ _ ?ns' => ns'
-               end in
-    eapply entails_equiv_l;
-      first (apply uPred_reflection.split_l with (ns:=ns'); cbv; reflexivity);
-      simpl).
-
-Tactic Notation "to_back" open_constr(Ps) :=
-  close_uPreds Ps ltac:(fun Ps =>
-    uPred_reflection.quote_l;
-    let Σ := match goal with |- uPred_reflection.eval ?Σ _ ⊢ _ => Σ end in
-    let ns' := lazymatch type of (_ : uPred_reflection.QuoteArgs Σ Ps _) with
-               | uPred_reflection.QuoteArgs _ _ ?ns' => ns'
-               end in
-    eapply entails_equiv_l;
-      first (apply uPred_reflection.split_r with (ns:=ns'); cbv; reflexivity);
-      simpl).
-
-(** [sep_split] is used to introduce a (★).
-    Use [sep_split left: [P1, P2, ...]] to define which assertions will be
-    taken to the left; the rest will be available on the right.
-    [sep_split right: [P1, P2, ...]] works the other way around. *)
-Tactic Notation "sep_split" "right:" open_constr(Ps) :=
-  to_back Ps; apply sep_mono.
-Tactic Notation "sep_split" "left:" open_constr(Ps) :=
-  to_front Ps; apply sep_mono.

benchmark/.gitignore

-__pycache__
-build-times.log*
-gitlab-extract

benchmark/gitlab-extract.py

-#!/usr/bin/env python3
-import argparse, pprint, sys
-import requests
-import parse_log
-
-def last(it):
-    r = None
-    for i in it:
-        r = i
-    return r
-
-def first(it):
-    for i in it:
-        return i
-    return None
-
-def req(path):
-    url = '%s/api/v3/%s' % (args.server, path)
-    return requests.get(url, headers={'PRIVATE-TOKEN': args.private_token})
-
-# read command-line arguments
-parser = argparse.ArgumentParser(description='Extract iris-coq build logs from GitLab')
-parser.add_argument("-t", "--private-token",
-                    dest="private_token", required=True,
-                    help="The private token used to authenticate access.")
-parser.add_argument("-s", "--server",
-                    dest="server", default="https://gitlab.mpi-sws.org/",
-                    help="The GitLab server to contact.")
-parser.add_argument("-p", "--project",
-                    dest="project", default="FP/iris-coq",
-                    help="The name of the project on GitLab.")
-parser.add_argument("-f", "--file",
-                    dest="file", required=True,
-                    help="Filename to store the load in.")
-parser.add_argument("-c", "--commits",
-                    dest="commits",
-                    help="The commits to fetch. Default is everything since the most recent entry in the log file.")
-args = parser.parse_args()
-log_file = sys.stdout if args.file == "-" else open(args.file, "a")
-
-# determine commit, if missing
-if args.commits is None:
-    if args.file == "-":
-        raise Exception("If you do not give explicit commits, you have to give a logfile so that we can determine the missing commits.")
-    last_result = last(parse_log.parse(open(args.file, "r"), parse_times = False))
-    args.commits = "{}..origin/master".format(last_result.commit)
-
-projects = req("projects")
-project = first(filter(lambda p: p['path_with_namespace'] == args.project, projects.json()))
-if project is None:
-    sys.stderr.write("Project not found.\n")
-    sys.exit(1)
-
-for commit in parse_log.parse_git_commits(args.commits):
-    print("Fetching {}...".format(commit))
-    commit_data = req("/projects/{}/repository/commits/{}".format(project['id'], commit))
-    if commit_data.status_code != 200:
-        raise Exception("Commit not found?")
-    builds = req("/projects/{}/repository/commits/{}/builds".format(project['id'], commit))
-    if builds.status_code != 200:
-        # no build
-        continue
-    build = first(sorted(builds.json(), key = lambda b: -int(b['id'])))
-    assert build is not None
-    if build['status'] == 'failed':
-        # build failed
-        continue
-    if build['status'] == 'running':
-        # build still running, don't fetch this or any later commit
-        break
-    # now fetch the build times
-    build_times = requests.get("{}/builds/{}/artifacts/file/build-time.txt".format(project['web_url'], build['id']))
-    if build_times.status_code != 200:
-        raise Exception("No artifact at build?")
-    # Output in the log file format
-    log_file.write("# {}\n".format(commit))
-    log_file.write(build_times.text)
-    log_file.flush()

benchmark/parse_log.py

-import re, subprocess
-
-class Result:
-    def __init__(self, commit, times):
-        self.commit = commit
-        self.times = times
-
-def parse(file, parse_times = True):
-    '''[file] should be a file-like object, an iterator over the lines.
-       yields a list of Result objects.'''
-    commit_re = re.compile("^# ([a-z0-9]+)$")
-    time_re = re.compile("^([a-zA-Z0-9_/-]+) \(user: ([0-9.]+) mem: ([0-9]+) ko\)$")
-    commit = None
-    times = None
-    for line in file:
-        # next commit?
-        m = commit_re.match(line)
-        if m is not None:
-            # previous commit, if any, is done now
-            if commit is not None:
-                yield Result(commit, times)
-            # start recording next commit
-            commit = m.group(1)
-            if parse_times:
-                times = {} # reset the recorded times
-            continue
-        # next file time?
-        m = time_re.match(line)
-        if m is not None:
-            if times is not None:
-                name = m.group(1)
-                time = float(m.group(2))
-                times[name] = time
-            continue
-        # nothing else we know about, ignore
-    # end of file. previous commit, if any, is done now.
-    if commit is not None:
-        yield Result(commit, times)
-
-def parse_git_commits(commits):
-    '''Returns an iterable of SHA1s'''
-    if commits.find('..') >= 0:
-        # a range of commits
-        commits = subprocess.check_output(["git", "rev-list", commits])
-    else:
-        # a single commit
-        commits = subprocess.check_output(["git", "rev-parse", commits])
-    return reversed(commits.decode("utf-8").strip().split('\n'))

benchmark/visualize.py

-#!/usr/bin/env python3
-import argparse, sys, pprint, itertools
-import matplotlib.pyplot as plt
-import parse_log
-
-markers = itertools.cycle([(3, 0), (3, 0, 180), (4, 0), (4, 0, 45), (8, 0)])
-
-# read command-line arguments
-parser = argparse.ArgumentParser(description='Visualize iris-coq build times')
-parser.add_argument("-f", "--file",
-                    dest="file", required=True,
-                    help="Filename to get the data from.")
-parser.add_argument("-t", "--timings", nargs='+',
-                    dest="timings",
-                    help="The names of the Coq files (with or without the extension) whose timings should be extracted")
-parser.add_argument("-c", "--commits",
-                    dest="commits",
-                    help="Restrict the graph to the given commits.")
-args = parser.parse_args()
-pp = pprint.PrettyPrinter()
-log_file = sys.stdin if args.file == "-" else open(args.file, "r")
-
-results = parse_log.parse(log_file, parse_times = True)
-if args.commits:
-    commits = set(parse_log.parse_git_commits(args.commits))
-    results = filter(lambda r: r.commit in commits, results)
-results = list(results)
-
-timings = list(map(lambda t: t[:-2] if t.endswith(".v") else t, args.timings))
-for timing in timings:
-    plt.plot(list(map(lambda r: r.times.get(timing), results)), marker=next(markers), markersize=8)
-plt.legend(timings, loc = 'upper left', bbox_to_anchor=(1.05, 1.0))
-plt.xticks(range(len(results)), list(map(lambda r: r.commit[:7], results)), rotation=70)
-plt.subplots_adjust(bottom=0.2, right=0.7) # more space for the commit labels and legend
-
-plt.xlabel('Commit')
-plt.ylabel('Time (s)')
-plt.title('Time to compile files')
-plt.grid(True)
-plt.show()

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"]