From 0f025d838fc07eda0789a43d77e3bdd60677ef06 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 16 Nov 2015 12:09:05 +0100
Subject: [PATCH] More consistent names in logic.v.

---
 iris/logic.v | 212 +++++++++++++++++++++++++--------------------------
 1 file changed, 106 insertions(+), 106 deletions(-)

diff --git a/iris/logic.v b/iris/logic.v
index acbb88613..e81f1f382 100644
--- a/iris/logic.v
+++ b/iris/logic.v
@@ -3,8 +3,8 @@ Local Hint Extern 1 (_ ≼ _) => etransitivity; [eassumption|].
 Local Hint Extern 1 (_ ≼ _) => etransitivity; [|eassumption].
 Local Hint Extern 10 (_ ≤ _) => omega.
 
-Structure iProp (A : cmraT) : Type := IProp {
-  iprop_holds :> nat → A -> Prop;
+Structure iProp (M : cmraT) : Type := IProp {
+  iprop_holds :> nat → M -> Prop;
   iprop_ne x1 x2 n : iprop_holds n x1 → x1 ={n}= x2 → iprop_holds n x2;
   iprop_weaken x1 x2 n1 n2 :
     x1 ≼ x2 → n2 ≤ n1 → validN n2 x2 → iprop_holds n1 x1 → iprop_holds n2 x2
@@ -12,18 +12,18 @@ Structure iProp (A : cmraT) : Type := IProp {
 Add Printing Constructor iProp.
 Instance: Params (@iprop_holds) 3.
 
-Instance iprop_equiv (A : cmraT) : Equiv (iProp A) := λ P Q, ∀ x n,
+Instance iprop_equiv (M : cmraT) : Equiv (iProp M) := λ P Q, ∀ x n,
   validN n x → P n x ↔ Q n x.
-Instance iprop_dist (A : cmraT) : Dist (iProp A) := λ n P Q, ∀ x n',
+Instance iprop_dist (M : cmraT) : Dist (iProp M) := λ n P Q, ∀ x n',
   n' < n → validN n' x → P n' x ↔ Q n' x.
-Program Instance iprop_compl (A : cmraT) : Compl (iProp A) := λ c,
+Program Instance iprop_compl (M : cmraT) : Compl (iProp M) := λ c,
   {| iprop_holds n x := c (S n) n x |}.
-Next Obligation. by intros A c x y n ??; simpl in *; apply iprop_ne with x. Qed.
+Next Obligation. by intros M c x y n ??; simpl in *; apply iprop_ne with x. Qed.
 Next Obligation.
-  intros A c x1 x2 n1 n2 ????; simpl in *.
+  intros M c x1 x2 n1 n2 ????; simpl in *.
   apply (chain_cauchy c (S n2) (S n1)); eauto using iprop_weaken, cmra_valid_le.
 Qed.
-Instance iprop_cofe (A : cmraT) : Cofe (iProp A).
+Instance iprop_cofe (M : cmraT) : Cofe (iProp M).
 Proof.
   split.
   * intros P Q; split; [by intros HPQ n x i ??; apply HPQ|].
@@ -36,50 +36,50 @@ Proof.
   * intros P Q x i ??; lia.
   * intros c n x i ??; apply (chain_cauchy c (S i) n); auto.
 Qed.
-Instance iprop_holds_ne {A} (P : iProp A) n : Proper (dist n ==> iff) (P n).
+Instance iprop_holds_ne {M} (P : iProp M) n : Proper (dist n ==> iff) (P n).
 Proof. intros x1 x2 Hx; split; eauto using iprop_ne. Qed.
-Instance iprop_holds_proper {A} (P : iProp A) n : Proper ((≡) ==> iff) (P n).
+Instance iprop_holds_proper {M} (P : iProp M) n : Proper ((≡) ==> iff) (P n).
 Proof. by intros x1 x2 Hx; apply iprop_holds_ne, equiv_dist. Qed.
-Definition iPropC (A : cmraT) : cofeT := CofeT (iProp A).
+Definition iPropC (M : cmraT) : cofeT := CofeT (iProp M).
 
 (** functor *)
-Program Definition iprop_map {A B : cmraT} (f : B → A)
+Program Definition iprop_map {M1 M2 : cmraT} (f : M2 → M1)
   `{!∀ n, Proper (dist n ==> dist n) f, !CMRAPreserving f}
-  (P : iProp A) : iProp B := {| iprop_holds n x := P n (f x) |}.
-Next Obligation. by intros A B f ?? P y1 y2 n ? Hy; simpl; rewrite <-Hy. Qed.
+  (P : iProp M1) : iProp M2 := {| iprop_holds n x := P n (f x) |}.
+Next Obligation. by intros M1 M2 f ?? P y1 y2 n ? Hy; simpl; rewrite <-Hy. Qed.
 Next Obligation.
-  by intros A B f ?? P y1 y2 n i ???; simpl; apply iprop_weaken; auto;
+  by intros M1 M2 f ?? P y1 y2 n i ???; simpl; apply iprop_weaken; auto;
     apply validN_preserving || apply included_preserving.
 Qed.
-Instance iprop_map_ne {A B : cmraT} (f : B → A)
+Instance iprop_map_ne {M1 M2 : cmraT} (f : M2 → M1)
   `{!∀ n, Proper (dist n ==> dist n) f, !CMRAPreserving f} :
   Proper (dist n ==> dist n) (iprop_map f).
 Proof.
   by intros n x1 x2 Hx y n'; split; apply Hx; try apply validN_preserving.
 Qed.
-Definition ipropC_map {A B : cmraT} (f : B -n> A) `{!CMRAPreserving f} :
-  iPropC A -n> iPropC B := CofeMor (iprop_map f : iPropC A → iPropC B).
+Definition ipropC_map {M1 M2 : cmraT} (f : M2 -n> M1) `{!CMRAPreserving f} :
+  iPropC M1 -n> iPropC M2 := CofeMor (iprop_map f : iPropC M1 → iPropC M2).
 
 (** logical entailement *)
-Instance iprop_entails {A} : SubsetEq (iProp A) := λ P Q, ∀ x n,
+Instance iprop_entails {M} : SubsetEq (iProp M) := λ P Q, ∀ x n,
   validN n x → P n x → Q n x.
 
 (** logical connectives *)
-Program Definition iprop_const {A} (P : Prop) : iProp A :=
+Program Definition iprop_const {M} (P : Prop) : iProp M :=
   {| iprop_holds n x := P |}.
 Solve Obligations with done.
 
-Program Definition iprop_and {A} (P Q : iProp A) : iProp A :=
+Program Definition iprop_and {M} (P Q : iProp M) : iProp M :=
   {| iprop_holds n x := P n x ∧ Q n x |}.
 Solve Obligations with naive_solver eauto 2 using iprop_ne, iprop_weaken.
-Program Definition iprop_or {A} (P Q : iProp A) : iProp A :=
+Program Definition iprop_or {M} (P Q : iProp M) : iProp M :=
   {| iprop_holds n x := P n x ∨ Q n x |}.
 Solve Obligations with naive_solver eauto 2 using iprop_ne, iprop_weaken.
-Program Definition iprop_impl {A} (P Q : iProp A) : iProp A :=
+Program Definition iprop_impl {M} (P Q : iProp M) : iProp M :=
   {| iprop_holds n x := ∀ x' n',
        x ≼ x' → n' ≤ n → validN n' x' → P n' x' → Q n' x' |}.
 Next Obligation.
-  intros A P Q x1' x1 n1 HPQ Hx1 x2 n2 ????.
+  intros M P Q x1' x1 n1 HPQ Hx1 x2 n2 ????.
   destruct (cmra_included_dist_l x1 x2 x1' n1) as (x2'&?&Hx2); auto.
   assert (x2' ={n2}= x2) as Hx2' by (by apply dist_le with n1).
   assert (validN n2 x2') by (by rewrite Hx2'); rewrite <-Hx2'.
@@ -87,24 +87,24 @@ Next Obligation.
 Qed.
 Next Obligation. naive_solver eauto 2 with lia. Qed.
 
-Program Definition iprop_forall {A B} (P : A → iProp B) : iProp B :=
+Program Definition iprop_forall {M A} (P : A → iProp M) : iProp M :=
   {| iprop_holds n x := ∀ a, P a n x |}.
 Solve Obligations with naive_solver eauto 2 using iprop_ne, iprop_weaken.
-Program Definition iprop_exist {A B} (P : A → iProp B) : iProp B :=
+Program Definition iprop_exist {M A} (P : A → iProp M) : iProp M :=
   {| iprop_holds n x := ∃ a, P a n x |}.
 Solve Obligations with naive_solver eauto 2 using iprop_ne, iprop_weaken.
 
-Program Definition iprop_eq {A} {B : cofeT} (b1 b2 : B) : iProp A :=
-  {| iprop_holds n x := b1 ={n}= b2 |}.
-Solve Obligations with naive_solver eauto 2 using (dist_le (A:=B)).
+Program Definition iprop_eq {M} {A : cofeT} (a1 a2 : A) : iProp M :=
+  {| iprop_holds n x := a1 ={n}= a2 |}.
+Solve Obligations with naive_solver eauto 2 using (dist_le (A:=A)).
 
-Program Definition iprop_sep {A} (P Q : iProp A) : iProp A :=
+Program Definition iprop_sep {M} (P Q : iProp M) : iProp M :=
   {| iprop_holds n x := ∃ x1 x2, x ={n}= x1 ⋅ x2 ∧ P n x1 ∧ Q n x2 |}.
 Next Obligation.
-  by intros A P Q x y n (x1&x2&?&?&?) Hxy; exists x1, x2; rewrite <-Hxy.
+  by intros M P Q x y n (x1&x2&?&?&?) Hxy; exists x1, x2; rewrite <-Hxy.
 Qed.
 Next Obligation.
-  intros A P Q x y n1 n2 Hxy ?? (x1&x2&Hx&?&?).
+  intros M P Q x y n1 n2 Hxy ?? (x1&x2&Hx&?&?).
   assert (∃ x2', y ={n2}= x1 ⋅ x2' ∧ x2 ≼ x2') as (x2'&Hy&?).
   { rewrite ra_included_spec in Hxy; destruct Hxy as [z Hy].
     exists (x2 â‹… z); split; eauto using ra_included_l.
@@ -116,49 +116,49 @@ Next Obligation.
     by apply cmra_valid_op_r with x1; rewrite <-Hy.
 Qed.
 
-Program Definition iprop_wand {A} (P Q : iProp A) : iProp A :=
+Program Definition iprop_wand {M} (P Q : iProp M) : iProp M :=
   {| iprop_holds n x := ∀ x' n',
        n' ≤ n → validN n' (x ⋅ x') → P n' x' → Q n' (x ⋅ x') |}.
 Next Obligation.
-  intros A P Q x1 x2 n1 HPQ Hx x3 n2 ???; simpl in *.
+  intros M P Q x1 x2 n1 HPQ Hx x3 n2 ???; simpl in *.
   rewrite <-(dist_le _ _ _ _ Hx) by done; apply HPQ; auto.
   by rewrite (dist_le _ _ _ n2 Hx).
 Qed.
 Next Obligation.
-  intros A P Q x1 x2 n1 n2 ??? HPQ x3 n3 ???; simpl in *.
+  intros M P Q x1 x2 n1 n2 ??? HPQ x3 n3 ???; simpl in *.
   apply iprop_weaken with (x1 â‹… x3) n3; auto using ra_preserving_r.
   apply HPQ; auto.
   apply cmra_valid_included with (x2 â‹… x3); auto using ra_preserving_r.
 Qed.
 
-Program Definition iprop_later {A} (P : iProp A) : iProp A :=
+Program Definition iprop_later {M} (P : iProp M) : iProp M :=
   {| iprop_holds n x := match n return _ with 0 => True | S n' => P n' x end |}.
-Next Obligation. intros A P ?? [|n]; eauto using iprop_ne,(dist_le (A:=A)). Qed.
+Next Obligation. intros M P ?? [|n]; eauto using iprop_ne,(dist_le (A:=M)). Qed.
 Next Obligation.
-  intros A P x1 x2 [|n1] [|n2] ????; auto with lia.
+  intros M P x1 x2 [|n1] [|n2] ????; auto with lia.
   apply iprop_weaken with x1 n1; eauto using cmra_valid_S.
 Qed.
-Program Definition iprop_always {A} (P : iProp A) : iProp A :=
+Program Definition iprop_always {M} (P : iProp M) : iProp M :=
   {| iprop_holds n x := P n (unit x) |}.
-Next Obligation. by intros A P x1 x2 n ? Hx; simpl in *; rewrite <-Hx. Qed.
+Next Obligation. by intros M P x1 x2 n ? Hx; simpl in *; rewrite <-Hx. Qed.
 Next Obligation.
-  intros A P x1 x2 n1 n2 ????; eapply iprop_weaken with (unit x1) n1;
+  intros M P x1 x2 n1 n2 ????; eapply iprop_weaken with (unit x1) n1;
     auto using ra_unit_preserving, cmra_unit_valid.
 Qed.
 
-Program Definition iprop_own {A : cmraT} (a : A) : iProp A :=
+Program Definition iprop_own {M : cmraT} (a : M) : iProp M :=
   {| iprop_holds n x := ∃ a', x ={n}= a ⋅ a' |}.
-Next Obligation. by intros A a x1 x2 n [a' Hx] ?; exists a'; rewrite <-Hx. Qed.
+Next Obligation. by intros M a x1 x2 n [a' Hx] ?; exists a'; rewrite <-Hx. Qed.
 Next Obligation.
-  intros A a x1 x n1 n2; rewrite ra_included_spec; intros [x2 Hx] ?? [a' Hx1].
+  intros M a x1 x n1 n2; rewrite ra_included_spec; intros [x2 Hx] ?? [a' Hx1].
   exists (a' â‹… x2). by rewrite (associative op), <-(dist_le _ _ _ _ Hx1), Hx.
 Qed.
-Program Definition iprop_valid {A : cmraT} (a : A) : iProp A :=
+Program Definition iprop_valid {M : cmraT} (a : M) : iProp M :=
   {| iprop_holds n x := validN n a |}.
 Solve Obligations with naive_solver eauto 2 using cmra_valid_le.
 
-Definition iprop_fixpoint {A} (P : iProp A → iProp A)
-  `{!Contractive P} : iProp A := fixpoint P (iprop_const True).
+Definition iprop_fixpoint {M} (P : iProp M → iProp M)
+  `{!Contractive P} : iProp M := fixpoint P (iprop_const True).
 
 Delimit Scope iprop_scope with I.
 Bind Scope iprop_scope with iProp.
@@ -179,10 +179,10 @@ Notation "â–· P" := (iprop_later P) (at level 20) : iprop_scope.
 Notation "â–¡ P" := (iprop_always P) (at level 20) : iprop_scope.
 
 Section logic.
-Context {A : cmraT}.
-Implicit Types P Q : iProp A.
+Context {M : cmraT}.
+Implicit Types P Q : iProp M.
 
-Global Instance iprop_preorder : PreOrder ((⊆) : relation (iProp A)).
+Global Instance iprop_preorder : PreOrder ((⊆) : relation (iProp M)).
 Proof. split. by intros P x i. by intros P Q Q' HP HQ x i ??; apply HQ, HP. Qed.
 Lemma iprop_equiv_spec P Q : P ≡ Q ↔ P ⊆ Q ∧ Q ⊆ P.
 Proof.
@@ -192,90 +192,90 @@ Proof.
 Qed.
 
 (** Non-expansiveness *)
-Global Instance iprop_const_proper : Proper (iff ==> (≡)) (@iprop_const A).
+Global Instance iprop_const_proper : Proper (iff ==> (≡)) (@iprop_const M).
 Proof. intros P Q HPQ ???; apply HPQ. Qed.
 Global Instance iprop_and_ne n :
-  Proper (dist n ==> dist n ==> dist n) (@iprop_and A).
+  Proper (dist n ==> dist n ==> dist n) (@iprop_and M).
 Proof.
   intros P P' HP Q Q' HQ; split; intros [??]; split; by apply HP || by apply HQ.
 Qed.
 Global Instance iprop_and_proper :
-  Proper ((≡) ==> (≡) ==> (≡)) (@iprop_and A) := ne_proper_2 _.
+  Proper ((≡) ==> (≡) ==> (≡)) (@iprop_and M) := ne_proper_2 _.
 Global Instance iprop_or_ne n :
-  Proper (dist n ==> dist n ==> dist n) (@iprop_or A).
+  Proper (dist n ==> dist n ==> dist n) (@iprop_or M).
 Proof.
   intros P P' HP Q Q' HQ; split; intros [?|?];
     first [by left; apply HP | by right; apply HQ].
 Qed.
 Global Instance iprop_or_proper :
-  Proper ((≡) ==> (≡) ==> (≡)) (@iprop_or A) := ne_proper_2 _.
+  Proper ((≡) ==> (≡) ==> (≡)) (@iprop_or M) := ne_proper_2 _.
 Global Instance iprop_impl_ne n :
-  Proper (dist n ==> dist n ==> dist n) (@iprop_impl A).
+  Proper (dist n ==> dist n ==> dist n) (@iprop_impl M).
 Proof.
   intros P P' HP Q Q' HQ; split; intros HPQ x' n'' ????; apply HQ,HPQ,HP; auto.
 Qed.
 Global Instance iprop_impl_proper :
-  Proper ((≡) ==> (≡) ==> (≡)) (@iprop_impl A) := ne_proper_2 _.
+  Proper ((≡) ==> (≡) ==> (≡)) (@iprop_impl M) := ne_proper_2 _.
 Global Instance iprop_sep_ne n :
-  Proper (dist n ==> dist n ==> dist n) (@iprop_sep A).
+  Proper (dist n ==> dist n ==> dist n) (@iprop_sep M).
 Proof.
   intros P P' HP Q Q' HQ x n' ? Hx'; split; intros (x1&x2&Hx&?&?);
     exists x1, x2; rewrite  Hx in Hx'; split_ands; try apply HP; try apply HQ;
     eauto using cmra_valid_op_l, cmra_valid_op_r.
 Qed.
 Global Instance iprop_sep_proper :
-  Proper ((≡) ==> (≡) ==> (≡)) (@iprop_sep A) := ne_proper_2 _.
+  Proper ((≡) ==> (≡) ==> (≡)) (@iprop_sep M) := ne_proper_2 _.
 Global Instance iprop_wand_ne n :
-  Proper (dist n ==> dist n ==> dist n) (@iprop_wand A).
+  Proper (dist n ==> dist n ==> dist n) (@iprop_wand M).
 Proof.
   intros P P' HP Q Q' HQ x n' ??; split; intros HPQ x' n'' ???;
     apply HQ, HPQ, HP; eauto using cmra_valid_op_r.
 Qed.
 Global Instance iprop_wand_proper :
-  Proper ((≡) ==> (≡) ==> (≡)) (@iprop_wand A) := ne_proper_2 _.
-Global Instance iprop_eq_ne {B : cofeT} n :
-  Proper (dist n ==> dist n ==> dist n) (@iprop_eq A B).
+  Proper ((≡) ==> (≡) ==> (≡)) (@iprop_wand M) := ne_proper_2 _.
+Global Instance iprop_eq_ne {A : cofeT} n :
+  Proper (dist n ==> dist n ==> dist n) (@iprop_eq M A).
 Proof.
   intros x x' Hx y y' Hy z n'; split; intros; simpl in *.
   * by rewrite <-(dist_le _ _ _ _ Hx), <-(dist_le _ _ _ _ Hy) by auto.
   * by rewrite (dist_le _ _ _ _ Hx), (dist_le _ _ _ _ Hy) by auto.
 Qed.
-Global Instance iprop_eq_proper {B : cofeT} :
-  Proper ((≡) ==> (≡) ==> (≡)) (@iprop_eq A B) := ne_proper_2 _.
-Global Instance iprop_forall_ne {B : cofeT} :
-  Proper (pointwise_relation _ (dist n) ==> dist n) (@iprop_forall B A).
+Global Instance iprop_eq_proper {A : cofeT} :
+  Proper ((≡) ==> (≡) ==> (≡)) (@iprop_eq M A) := ne_proper_2 _.
+Global Instance iprop_forall_ne {A : cofeT} :
+  Proper (pointwise_relation _ (dist n) ==> dist n) (@iprop_forall M A).
 Proof. by intros n P1 P2 HP12 x n'; split; intros HP a; apply HP12. Qed.
-Global Instance iprop_forall_proper {B : cofeT} :
-  Proper (pointwise_relation _ (≡) ==> (≡)) (@iprop_forall B A).
+Global Instance iprop_forall_proper {A : cofeT} :
+  Proper (pointwise_relation _ (≡) ==> (≡)) (@iprop_forall M A).
 Proof. by intros P1 P2 HP12 x n'; split; intros HP a; apply HP12. Qed.
-Global Instance iprop_exists_ne {B : cofeT} :
-  Proper (pointwise_relation _ (dist n) ==> dist n) (@iprop_exist B A).
+Global Instance iprop_exists_ne {A : cofeT} :
+  Proper (pointwise_relation _ (dist n) ==> dist n) (@iprop_exist M A).
 Proof.
   by intros n P1 P2 HP12 x n'; split; intros [a HP]; exists a; apply HP12.
 Qed.
-Global Instance iprop_exist_proper {B : cofeT} :
-  Proper (pointwise_relation _ (≡) ==> (≡)) (@iprop_exist B A).
+Global Instance iprop_exist_proper {A : cofeT} :
+  Proper (pointwise_relation _ (≡) ==> (≡)) (@iprop_exist M A).
 Proof.
   by intros P1 P2 HP12 x n'; split; intros [a HP]; exists a; apply HP12.
 Qed.
-Global Instance iprop_later_contractive : Contractive (@iprop_later A).
+Global Instance iprop_later_contractive : Contractive (@iprop_later M).
 Proof.
   intros n P Q HPQ x [|n'] ??; simpl; [done|].
   apply HPQ; eauto using cmra_valid_S.
 Qed.
 Global Instance iprop_later_proper :
-  Proper ((≡) ==> (≡)) (@iprop_later A) := ne_proper _.
-Global Instance iprop_always_ne n: Proper (dist n ==> dist n) (@iprop_always A).
+  Proper ((≡) ==> (≡)) (@iprop_later M) := ne_proper _.
+Global Instance iprop_always_ne n: Proper (dist n ==> dist n) (@iprop_always M).
 Proof. intros P1 P2 HP x n'; split; apply HP; eauto using cmra_unit_valid. Qed.
 Global Instance iprop_always_proper :
-  Proper ((≡) ==> (≡)) (@iprop_always A) := ne_proper _.
-Global Instance iprop_own_ne n : Proper (dist n ==> dist n) (@iprop_own A).
+  Proper ((≡) ==> (≡)) (@iprop_always M) := ne_proper _.
+Global Instance iprop_own_ne n : Proper (dist n ==> dist n) (@iprop_own M).
 Proof.
   by intros a1 a2 Ha x n'; split; intros [a' ?]; exists a'; simpl; first
     [rewrite <-(dist_le _ _ _ _ Ha) by lia|rewrite (dist_le _ _ _ _ Ha) by lia].
 Qed.
 Global Instance iprop_own_proper :
-  Proper ((≡) ==> (≡)) (@iprop_own A) := ne_proper _.
+  Proper ((≡) ==> (≡)) (@iprop_own M) := ne_proper _.
 
 (** Introduction and elimination rules *)
 Lemma iprop_True_intro P : P ⊆ True%I.
@@ -300,14 +300,14 @@ Proof.
 Qed.
 Lemma iprop_impl_elim P Q : ((P → Q) ∧ P)%I ⊆ Q.
 Proof. by intros x n ? [HQ HP]; apply HQ. Qed.
-Lemma iprop_forall_intro P `(Q: B → iProp A): (∀ b, P ⊆ Q b) → P ⊆ (∀ b, Q b)%I.
-Proof. by intros HPQ x n ?? b; apply HPQ. Qed.
-Lemma iprop_forall_elim `(P : B → iProp A) b : (∀ b, P b)%I ⊆ P b.
+Lemma iprop_forall_intro P `(Q: A → iProp M): (∀ a, P ⊆ Q a) → P ⊆ (∀ a, Q a)%I.
+Proof. by intros HPQ x n ?? a; apply HPQ. Qed.
+Lemma iprop_forall_elim `(P : A → iProp M) a : (∀ a, P a)%I ⊆ P a.
 Proof. intros x n ? HP; apply HP. Qed.
-Lemma iprop_exist_intro `(P : B → iProp A) b : P b ⊆ (∃ b, P b)%I.
-Proof. by intros x n ??; exists b. Qed.
-Lemma iprop_exist_elim `(P : B → iProp A) Q : (∀ b, P b ⊆ Q) → (∃ b, P b)%I ⊆ Q.
-Proof. by intros HPQ x n ? [b ?]; apply HPQ with b. Qed.
+Lemma iprop_exist_intro `(P : A → iProp M) a : P a ⊆ (∃ a, P a)%I.
+Proof. by intros x n ??; exists a. Qed.
+Lemma iprop_exist_elim `(P : A → iProp M) Q : (∀ a, P a ⊆ Q) → (∃ a, P a)%I ⊆ Q.
+Proof. by intros HPQ x n ? [a ?]; apply HPQ with a. Qed.
 
 (* BI connectives *)
 Lemma iprop_sep_elim_l P Q : (P ★ Q)%I ⊆ P.
@@ -315,19 +315,19 @@ Proof.
   intros x n Hvalid (x1&x2&Hx&?&?); rewrite Hx in Hvalid |- *.
   by apply iprop_weaken with x1 n; auto using ra_included_l.
 Qed.
-Global Instance iprop_sep_left_id : LeftId (≡) True%I (@iprop_sep A).
+Global Instance iprop_sep_left_id : LeftId (≡) True%I (@iprop_sep M).
 Proof.
   intros P x n Hvalid; split.
   * intros (x1&x2&Hx&_&?); rewrite Hx in Hvalid |- *.
     apply iprop_weaken with x2 n; auto using ra_included_r.
   * by intros ?; exists (unit x), x; rewrite ra_unit_l.
 Qed. 
-Global Instance iprop_sep_commutative : Commutative (≡) (@iprop_sep A).
+Global Instance iprop_sep_commutative : Commutative (≡) (@iprop_sep M).
 Proof.
   by intros P Q x n ?; split;
     intros (x1&x2&?&?&?); exists x2, x1; rewrite (commutative op).
 Qed.
-Global Instance iprop_sep_associative : Associative (≡) (@iprop_sep A).
+Global Instance iprop_sep_associative : Associative (≡) (@iprop_sep M).
 Proof.
   intros P Q R x n ?; split.
   * intros (x1&x2&Hx&?&y1&y2&Hy&?&?); exists (x1 â‹… y1), y2; split_ands; auto.
@@ -355,15 +355,15 @@ Proof.
 Qed.
 Lemma iprop_sep_and P Q R : ((P ∧ Q) ★ R)%I ⊆ ((P ★ R) ∧ (Q ★ R))%I.
 Proof. by intros x n ? (x1&x2&Hx&[??]&?); split; exists x1, x2. Qed.
-Lemma iprop_sep_exist {B} (P : B → iProp A) Q :
+Lemma iprop_sep_exist `(P : A → iProp M) Q :
   ((∃ b, P b) ★ Q)%I ≡ (∃ b, P b ★ Q)%I.
 Proof.
-  split; [by intros (x1&x2&Hx&[b ?]&?); exists b, x1, x2|].
-  intros [b (x1&x2&Hx&?&?)]; exists x1, x2; split_ands; by try exists b.
+  split; [by intros (x1&x2&Hx&[a ?]&?); exists a, x1, x2|].
+  intros [a (x1&x2&Hx&?&?)]; exists x1, x2; split_ands; by try exists a.
 Qed.
-Lemma iprop_sep_forall `(P : B → iProp A) Q :
-  ((∀ b, P b) ★ Q)%I ⊆ (∀ b, P b ★ Q)%I.
-Proof. by intros x n ? (x1&x2&Hx&?&?); intros b; exists x1, x2. Qed.
+Lemma iprop_sep_forall `(P : A → iProp M) Q :
+  ((∀ a, P a) ★ Q)%I ⊆ (∀ a, P a ★ Q)%I.
+Proof. by intros x n ? (x1&x2&Hx&?&?); intros a; exists x1, x2. Qed.
 
 (* Later *)
 Lemma iprop_later_weaken P : P ⊆ (▷ P)%I.
@@ -385,15 +385,15 @@ Lemma iprop_later_and P Q : (▷ (P ∧ Q))%I ≡ (▷ P ∧ ▷ Q)%I.
 Proof. by intros x [|n]; split. Qed.
 Lemma iprop_later_or P Q : (▷ (P ∨ Q))%I ≡ (▷ P ∨ ▷ Q)%I.
 Proof. intros x [|n]; simpl; tauto. Qed.
-Lemma iprop_later_forall `(P : B → iProp A) : (▷ ∀ b, P b)%I ≡ (∀ b, ▷ P b)%I.
+Lemma iprop_later_forall `(P : A → iProp M) : (▷ ∀ a, P a)%I ≡ (∀ a, ▷ P a)%I.
 Proof. by intros x [|n]. Qed.
-Lemma iprop_later_exist `(P : B → iProp A) : (∃ b, ▷ P b)%I ⊆ (▷ ∃ b, P b)%I.
+Lemma iprop_later_exist `(P : A → iProp M) : (∃ a, ▷ P a)%I ⊆ (▷ ∃ a, P a)%I.
 Proof. by intros x [|n]. Qed.
-Lemma iprop_later_exist' `{Inhabited B} (P : B → iProp A) :
-  (▷ ∃ b, P b)%I ≡ (∃ b, ▷ P b)%I.
+Lemma iprop_later_exist' `{Inhabited A} (P : A → iProp M) :
+  (▷ ∃ a, P a)%I ≡ (∃ a, ▷ P a)%I.
 Proof.
   intros x [|n]; split; try done.
-  by destruct (_ : Inhabited B) as [b]; exists b.
+  by destruct (_ : Inhabited A) as [a]; exists a.
 Qed.
 Lemma iprop_later_sep P Q : (▷ (P ★ Q))%I ≡ (▷ P ★ ▷ Q)%I.
 Proof.
@@ -403,7 +403,7 @@ Proof.
       as ([y1 y2]&Hx'&Hy1&Hy2); auto using cmra_valid_S; simpl in *.
     exists y1, y2; split; [by rewrite Hx'|by rewrite Hy1, Hy2].
   * destruct n as [|n]; simpl; [done|intros (x1&x2&Hx&?&?)].
-    exists x1, x2; eauto using (dist_S (A:=A)).
+    exists x1, x2; eauto using (dist_S (A:=M)).
 Qed.
 
 (* Always *)
@@ -425,9 +425,9 @@ Lemma iprop_always_and P Q : (□ (P ∧ Q))%I ≡ (□ P ∧ □ Q)%I.
 Proof. done. Qed.
 Lemma iprop_always_or P Q : (□ (P ∨ Q))%I ≡ (□ P ∨ □ Q)%I.
 Proof. done. Qed.
-Lemma iprop_always_forall `(P : B → iProp A) : (□ ∀ b, P b)%I ≡ (∀ b, □ P b)%I.
+Lemma iprop_always_forall `(P : A → iProp M) : (□ ∀ a, P a)%I ≡ (∀ a, □ P a)%I.
 Proof. done. Qed.
-Lemma iprop_always_exist `(P : B → iProp A) : (□ ∃ b, P b)%I ≡ (∃ b, □ P b)%I.
+Lemma iprop_always_exist `(P : A → iProp M) : (□ ∃ a, P a)%I ≡ (∃ a, □ P a)%I.
 Proof. done. Qed.
 Lemma iprop_always_and_always_box P Q : (□ P ∧ Q)%I ⊆ (□ P ★ Q)%I.
 Proof.
@@ -436,7 +436,7 @@ Proof.
 Qed.
 
 (* Own *)
-Lemma iprop_own_op (a1 a2 : A) :
+Lemma iprop_own_op (a1 a2 : M) :
   iprop_own (a1 ⋅ a2) ≡ (iprop_own a1 ★ iprop_own a2)%I.
 Proof.
   intros x n ?; split.
@@ -446,13 +446,13 @@ Proof.
     rewrite (associative op), <-(commutative op z1), <-!(associative op), <-Hy2.
     by rewrite (associative op), (commutative op z1), <-Hy1.
 Qed.
-Lemma iprop_own_valid (a : A) : iprop_own a ⊆ iprop_valid a.
+Lemma iprop_own_valid (a : M) : iprop_own a ⊆ iprop_valid a.
 Proof.
   intros x n Hv [a' Hx]; simpl; rewrite Hx in Hv; eauto using cmra_valid_op_l.
 Qed.
 
 (* Fix *)
-Lemma iprop_fixpoint_unfold (P : iProp A → iProp A) `{!Contractive P} :
+Lemma iprop_fixpoint_unfold (P : iProp M → iProp M) `{!Contractive P} :
   iprop_fixpoint P ≡ P (iprop_fixpoint P).
 Proof. apply fixpoint_unfold. Qed.
 End logic.
-- 
GitLab