Indent some sections.

iris/base_logic/bi.v

@@ -184,72 +184,72 @@ Proof. exact: bupd_plainly. Qed.
 Module uPred.
 
 Section restate.
-Context {M : ucmra}.
-Implicit Types φ : Prop.
-Implicit Types P Q : uPred M.
-Implicit Types A : Type.
-
-(* Force implicit argument M *)
-Notation "P ⊢ Q" := (bi_entails (PROP:=uPredI M) P%I Q%I).
-Notation "P ⊣⊢ Q" := (equiv (A:=uPredI M) P%I Q%I).
-
-Global Instance ownM_ne : NonExpansive (@uPred_ownM M) := uPred_primitive.ownM_ne.
-Global Instance cmra_valid_ne {A : cmra} : NonExpansive (@uPred_cmra_valid M A) :=
-  uPred_primitive.cmra_valid_ne.
-
-(** Re-exporting primitive lemmas that are not in any interface *)
-Lemma ownM_op (a1 a2 : M) :
-  uPred_ownM (a1 ⋅ a2) ⊣⊢ uPred_ownM a1 ∗ uPred_ownM a2.
-Proof. exact: uPred_primitive.ownM_op. Qed.
-Lemma persistently_ownM_core (a : M) : uPred_ownM a ⊢ <pers> uPred_ownM (core a).
-Proof. exact: uPred_primitive.persistently_ownM_core. Qed.
-Lemma ownM_unit P : P ⊢ (uPred_ownM ε).
-Proof. exact: uPred_primitive.ownM_unit. Qed.
-Lemma later_ownM a : ▷ uPred_ownM a ⊢ ∃ b, uPred_ownM b ∧ ▷ (a ≡ b).
-Proof. exact: uPred_primitive.later_ownM. Qed.
-Lemma bupd_ownM_updateP x (Φ : M → Prop) :
-  x ~~>: Φ → uPred_ownM x ⊢ |==> ∃ y, ⌜Φ y⌝ ∧ uPred_ownM y.
-Proof. exact: uPred_primitive.bupd_ownM_updateP. Qed.
-
-(** This is really just a special case of an entailment
-between two [siProp], but we do not have the infrastructure
-to express the more general case. This temporary proof rule will
-be replaced by the proper one eventually. *)
-Lemma internal_eq_entails {A B : ofe} (a1 a2 : A) (b1 b2 : B) :
-  (∀ n, a1 ≡{n}≡ a2 → b1 ≡{n}≡ b2) → a1 ≡ a2 ⊢ b1 ≡ b2.
-Proof. exact: uPred_primitive.internal_eq_entails. Qed.
-
-Lemma ownM_valid (a : M) : uPred_ownM a ⊢ ✓ a.
-Proof. exact: uPred_primitive.ownM_valid. Qed.
-Lemma cmra_valid_intro {A : cmra} P (a : A) : ✓ a → P ⊢ (✓ a).
-Proof. exact: uPred_primitive.cmra_valid_intro. Qed.
-Lemma cmra_valid_elim {A : cmra} (a : A) : ¬ ✓{0} a → ✓ a ⊢ False.
-Proof. exact: uPred_primitive.cmra_valid_elim. Qed.
-Lemma plainly_cmra_valid_1 {A : cmra} (a : A) : ✓ a ⊢ ■ ✓ a.
-Proof. exact: uPred_primitive.plainly_cmra_valid_1. Qed.
-Lemma cmra_valid_weaken {A : cmra} (a b : A) : ✓ (a ⋅ b) ⊢ ✓ a.
-Proof. exact: uPred_primitive.cmra_valid_weaken. Qed.
-Lemma discrete_valid {A : cmra} `{!CmraDiscrete A} (a : A) : ✓ a ⊣⊢ ⌜✓ a⌝.
-Proof. exact: uPred_primitive.discrete_valid. Qed.
-
-(** This is really just a special case of an entailment
-between two [siProp], but we do not have the infrastructure
-to express the more general case. This temporary proof rule will
-be replaced by the proper one eventually. *)
-Lemma valid_entails {A B : cmra} (a : A) (b : B) :
-  (∀ n, ✓{n} a → ✓{n} b) → ✓ a ⊢ ✓ b.
-Proof. exact: uPred_primitive.valid_entails. Qed.
-
-(** Consistency/soundness statement *)
-Lemma pure_soundness φ : (⊢@{uPredI M} ⌜ φ ⌝) → φ.
-Proof. apply pure_soundness. Qed.
-
-Lemma internal_eq_soundness {A : ofe} (x y : A) : (⊢@{uPredI M} x ≡ y) → x ≡ y.
-Proof. apply internal_eq_soundness. Qed.
-
-Lemma later_soundness P : (⊢ ▷ P) → ⊢ P.
-Proof. apply later_soundness. Qed.
-(** See [derived.v] for a similar soundness result for basic updates. *)
+  Context {M : ucmra}.
+  Implicit Types φ : Prop.
+  Implicit Types P Q : uPred M.
+  Implicit Types A : Type.
+
+  (* Force implicit argument M *)
+  Notation "P ⊢ Q" := (bi_entails (PROP:=uPredI M) P%I Q%I).
+  Notation "P ⊣⊢ Q" := (equiv (A:=uPredI M) P%I Q%I).
+
+  Global Instance ownM_ne : NonExpansive (@uPred_ownM M) := uPred_primitive.ownM_ne.
+  Global Instance cmra_valid_ne {A : cmra} : NonExpansive (@uPred_cmra_valid M A) :=
+    uPred_primitive.cmra_valid_ne.
+
+  (** Re-exporting primitive lemmas that are not in any interface *)
+  Lemma ownM_op (a1 a2 : M) :
+    uPred_ownM (a1 ⋅ a2) ⊣⊢ uPred_ownM a1 ∗ uPred_ownM a2.
+  Proof. exact: uPred_primitive.ownM_op. Qed.
+  Lemma persistently_ownM_core (a : M) : uPred_ownM a ⊢ <pers> uPred_ownM (core a).
+  Proof. exact: uPred_primitive.persistently_ownM_core. Qed.
+  Lemma ownM_unit P : P ⊢ (uPred_ownM ε).
+  Proof. exact: uPred_primitive.ownM_unit. Qed.
+  Lemma later_ownM a : ▷ uPred_ownM a ⊢ ∃ b, uPred_ownM b ∧ ▷ (a ≡ b).
+  Proof. exact: uPred_primitive.later_ownM. Qed.
+  Lemma bupd_ownM_updateP x (Φ : M → Prop) :
+    x ~~>: Φ → uPred_ownM x ⊢ |==> ∃ y, ⌜Φ y⌝ ∧ uPred_ownM y.
+  Proof. exact: uPred_primitive.bupd_ownM_updateP. Qed.
+
+  (** This is really just a special case of an entailment
+  between two [siProp], but we do not have the infrastructure
+  to express the more general case. This temporary proof rule will
+  be replaced by the proper one eventually. *)
+  Lemma internal_eq_entails {A B : ofe} (a1 a2 : A) (b1 b2 : B) :
+    (∀ n, a1 ≡{n}≡ a2 → b1 ≡{n}≡ b2) → a1 ≡ a2 ⊢ b1 ≡ b2.
+  Proof. exact: uPred_primitive.internal_eq_entails. Qed.
+
+  Lemma ownM_valid (a : M) : uPred_ownM a ⊢ ✓ a.
+  Proof. exact: uPred_primitive.ownM_valid. Qed.
+  Lemma cmra_valid_intro {A : cmra} P (a : A) : ✓ a → P ⊢ (✓ a).
+  Proof. exact: uPred_primitive.cmra_valid_intro. Qed.
+  Lemma cmra_valid_elim {A : cmra} (a : A) : ¬ ✓{0} a → ✓ a ⊢ False.
+  Proof. exact: uPred_primitive.cmra_valid_elim. Qed.
+  Lemma plainly_cmra_valid_1 {A : cmra} (a : A) : ✓ a ⊢ ■ ✓ a.
+  Proof. exact: uPred_primitive.plainly_cmra_valid_1. Qed.
+  Lemma cmra_valid_weaken {A : cmra} (a b : A) : ✓ (a ⋅ b) ⊢ ✓ a.
+  Proof. exact: uPred_primitive.cmra_valid_weaken. Qed.
+  Lemma discrete_valid {A : cmra} `{!CmraDiscrete A} (a : A) : ✓ a ⊣⊢ ⌜✓ a⌝.
+  Proof. exact: uPred_primitive.discrete_valid. Qed.
+
+  (** This is really just a special case of an entailment
+  between two [siProp], but we do not have the infrastructure
+  to express the more general case. This temporary proof rule will
+  be replaced by the proper one eventually. *)
+  Lemma valid_entails {A B : cmra} (a : A) (b : B) :
+    (∀ n, ✓{n} a → ✓{n} b) → ✓ a ⊢ ✓ b.
+  Proof. exact: uPred_primitive.valid_entails. Qed.
+
+  (** Consistency/soundness statement *)
+  Lemma pure_soundness φ : (⊢@{uPredI M} ⌜ φ ⌝) → φ.
+  Proof. apply pure_soundness. Qed.
+
+  Lemma internal_eq_soundness {A : ofe} (x y : A) : (⊢@{uPredI M} x ≡ y) → x ≡ y.
+  Proof. apply internal_eq_soundness. Qed.
+
+  Lemma later_soundness P : (⊢ ▷ P) → ⊢ P.
+  Proof. apply later_soundness. Qed.
+  (** See [derived.v] for a similar soundness result for basic updates. *)
 End restate.
 
 

iris/base_logic/derived.v

@@ -9,125 +9,123 @@ Import bi.bi base_logic.bi.uPred.
 
 Module uPred.
 Section derived.
-Context {M : ucmra}.
-Implicit Types φ : Prop.
-Implicit Types P Q : uPred M.
-Implicit Types A : Type.
-
-(* Force implicit argument M *)
-Notation "P ⊢ Q" := (bi_entails (PROP:=uPredI M) P Q).
-Notation "P ⊣⊢ Q" := (equiv (A:=uPredI M) P%I Q%I).
-
-(** Propers *)
-Global Instance ownM_proper: Proper ((≡) ==> (⊣⊢)) (@uPred_ownM M) := ne_proper _.
-Global Instance cmra_valid_proper {A : cmra} :
-  Proper ((≡) ==> (⊣⊢)) (@uPred_cmra_valid M A) := ne_proper _.
-
-(** Own and valid derived *)
-Lemma persistently_cmra_valid_1 {A : cmra} (a : A) : ✓ a ⊢@{uPredI M} <pers> (✓ a).
-Proof. by rewrite {1}plainly_cmra_valid_1 plainly_elim_persistently. Qed.
-Lemma intuitionistically_ownM (a : M) : CoreId a → □ uPred_ownM a ⊣⊢ uPred_ownM a.
-Proof.
-  rewrite /bi_intuitionistically affine_affinely=>?; apply (anti_symm _);
-    [by rewrite persistently_elim|].
-  by rewrite {1}persistently_ownM_core core_id_core.
-Qed.
-Lemma ownM_invalid (a : M) : ¬ ✓{0} a → uPred_ownM a ⊢ False.
-Proof. by intros; rewrite ownM_valid cmra_valid_elim. Qed.
-Global Instance ownM_mono : Proper (flip (≼) ==> (⊢)) (@uPred_ownM M).
-Proof. intros a b [b' ->]. by rewrite ownM_op sep_elim_l. Qed.
-Lemma ownM_unit' : uPred_ownM ε ⊣⊢ True.
-Proof. apply (anti_symm _); first by apply pure_intro. apply ownM_unit. Qed.
-Lemma plainly_cmra_valid {A : cmra} (a : A) : ■ ✓ a ⊣⊢ ✓ a.
-Proof. apply (anti_symm _), plainly_cmra_valid_1. apply plainly_elim, _. Qed.
-Lemma intuitionistically_cmra_valid {A : cmra} (a : A) : □ ✓ a ⊣⊢ ✓ a.
-Proof.
-  rewrite /bi_intuitionistically affine_affinely. intros; apply (anti_symm _);
-    first by rewrite persistently_elim.
-  apply:persistently_cmra_valid_1.
-Qed.
-Lemma bupd_ownM_update x y : x ~~> y → uPred_ownM x ⊢ |==> uPred_ownM y.
-Proof.
-  intros; rewrite (bupd_ownM_updateP _ (y =.)); last by apply cmra_update_updateP.
-  by apply bupd_mono, exist_elim=> y'; apply pure_elim_l=> ->.
-Qed.
-
-(** Timeless instances *)
-Global Instance valid_timeless {A : cmra} `{!CmraDiscrete A} (a : A) :
-  Timeless (✓ a : uPred M)%I.
-Proof. rewrite /Timeless !discrete_valid. apply (timeless _). Qed.
-Global Instance ownM_timeless (a : M) : Discrete a → Timeless (uPred_ownM a).
-Proof.
-  intros ?. rewrite /Timeless later_ownM. apply exist_elim=> b.
-  rewrite (timeless (a≡b)) (except_0_intro (uPred_ownM b)) -except_0_and.
-  apply except_0_mono. rewrite internal_eq_sym.
-  apply (internal_eq_rewrite' b a (uPred_ownM) _);
-    auto using and_elim_l, and_elim_r.
-Qed.
-
-(** Plainness *)
-Global Instance cmra_valid_plain {A : cmra} (a : A) :
-  Plain (✓ a : uPred M)%I.
-Proof. rewrite /Persistent. apply plainly_cmra_valid_1. Qed.
-
-(** Persistence *)
-Global Instance cmra_valid_persistent {A : cmra} (a : A) :
-  Persistent (✓ a : uPred M)%I.
-Proof. rewrite /Persistent. apply persistently_cmra_valid_1. Qed.
-Global Instance ownM_persistent a : CoreId a → Persistent (@uPred_ownM M a).
-Proof.
-  intros. rewrite /Persistent -{2}(core_id_core a). apply persistently_ownM_core.
-Qed.
-
-(** For big ops *)
-Global Instance uPred_ownM_sep_homomorphism :
-  MonoidHomomorphism op uPred_sep (≡) (@uPred_ownM M).
-Proof. split; [split|]; try apply _; [apply ownM_op | apply ownM_unit']. Qed.
-
-(** Soundness statement for our modalities: facts derived under modalities in
-the empty context also without the modalities.
-For basic updates, soundness only holds for plain propositions. *)
-Lemma bupd_soundness P `{!Plain P} : (⊢ |==> P) → ⊢ P.
-Proof. rewrite bupd_plain. done. Qed.
-
-Lemma laterN_soundness P n : (⊢ ▷^n P) → ⊢ P.
-Proof. induction n; eauto using later_soundness. Qed.
-
-(** As pure demonstration, we also show that this holds for an arbitrary nesting
-of modalities. We have to do a bit of work to be able to state this theorem
-though. *)
-Inductive modality := MBUpd | MLater | MPersistently | MPlainly.
-Definition denote_modality (m : modality) : uPred M → uPred M :=
-  match m with
-  | MBUpd => bupd
-  | MLater => bi_later
-  | MPersistently => bi_persistently
-  | MPlainly => plainly
-  end.
-Definition denote_modalities (ms : list modality) : uPred M → uPred M :=
-  λ P, foldr denote_modality P ms.
-
-(** Now we can state and prove 'soundness under arbitrary modalities' for plain
-propositions. This is probably not a lemma you want to actually use. *)
-Corollary modal_soundness P `{!Plain P} (ms : list modality) :
-  (⊢ denote_modalities ms P) → ⊢ P.
-Proof.
-  intros H. apply (laterN_soundness _ (length ms)).
-  move: H. apply bi_emp_valid_mono.
-  induction ms as [|m ms IH]; first done; simpl.
-  destruct m; simpl; rewrite IH.
-  - rewrite -later_intro. apply bupd_plain. apply _.
-  - done.
-  - rewrite -later_intro persistently_elim. done.
-  - rewrite -later_intro plainly_elim. done.
-Qed.
-
-(** Consistency: one cannot deive [False] in the logic, not even under
-modalities. Again this is just for demonstration and probably not practically
-useful. *)
-Corollary consistency : ¬ ⊢@{uPredI M} False.
-Proof. intros H. by eapply pure_soundness. Qed.
-
+  Context {M : ucmra}.
+  Implicit Types φ : Prop.
+  Implicit Types P Q : uPred M.
+  Implicit Types A : Type.
+
+  (* Force implicit argument M *)
+  Notation "P ⊢ Q" := (bi_entails (PROP:=uPredI M) P Q).
+  Notation "P ⊣⊢ Q" := (equiv (A:=uPredI M) P%I Q%I).
+
+  (** Propers *)
+  Global Instance ownM_proper: Proper ((≡) ==> (⊣⊢)) (@uPred_ownM M) := ne_proper _.
+  Global Instance cmra_valid_proper {A : cmra} :
+    Proper ((≡) ==> (⊣⊢)) (@uPred_cmra_valid M A) := ne_proper _.
+
+  (** Own and valid derived *)
+  Lemma persistently_cmra_valid_1 {A : cmra} (a : A) : ✓ a ⊢@{uPredI M} <pers> (✓ a).
+  Proof. by rewrite {1}plainly_cmra_valid_1 plainly_elim_persistently. Qed.
+  Lemma intuitionistically_ownM (a : M) : CoreId a → □ uPred_ownM a ⊣⊢ uPred_ownM a.
+  Proof.
+    rewrite /bi_intuitionistically affine_affinely=>?; apply (anti_symm _);
+      [by rewrite persistently_elim|].
+    by rewrite {1}persistently_ownM_core core_id_core.
+  Qed.
+  Lemma ownM_invalid (a : M) : ¬ ✓{0} a → uPred_ownM a ⊢ False.
+  Proof. by intros; rewrite ownM_valid cmra_valid_elim. Qed.
+  Global Instance ownM_mono : Proper (flip (≼) ==> (⊢)) (@uPred_ownM M).
+  Proof. intros a b [b' ->]. by rewrite ownM_op sep_elim_l. Qed.
+  Lemma ownM_unit' : uPred_ownM ε ⊣⊢ True.
+  Proof. apply (anti_symm _); first by apply pure_intro. apply ownM_unit. Qed.
+  Lemma plainly_cmra_valid {A : cmra} (a : A) : ■ ✓ a ⊣⊢ ✓ a.
+  Proof. apply (anti_symm _), plainly_cmra_valid_1. apply plainly_elim, _. Qed.
+  Lemma intuitionistically_cmra_valid {A : cmra} (a : A) : □ ✓ a ⊣⊢ ✓ a.
+  Proof.
+    rewrite /bi_intuitionistically affine_affinely. intros; apply (anti_symm _);
+      first by rewrite persistently_elim.
+    apply:persistently_cmra_valid_1.
+  Qed.
+  Lemma bupd_ownM_update x y : x ~~> y → uPred_ownM x ⊢ |==> uPred_ownM y.
+  Proof.
+    intros; rewrite (bupd_ownM_updateP _ (y =.)); last by apply cmra_update_updateP.
+    by apply bupd_mono, exist_elim=> y'; apply pure_elim_l=> ->.
+  Qed.
+
+  (** Timeless instances *)
+  Global Instance valid_timeless {A : cmra} `{!CmraDiscrete A} (a : A) :
+    Timeless (✓ a : uPred M)%I.
+  Proof. rewrite /Timeless !discrete_valid. apply (timeless _). Qed.
+  Global Instance ownM_timeless (a : M) : Discrete a → Timeless (uPred_ownM a).
+  Proof.
+    intros ?. rewrite /Timeless later_ownM. apply exist_elim=> b.
+    rewrite (timeless (a≡b)) (except_0_intro (uPred_ownM b)) -except_0_and.
+    apply except_0_mono. rewrite internal_eq_sym.
+    apply (internal_eq_rewrite' b a (uPred_ownM) _);
+      auto using and_elim_l, and_elim_r.
+  Qed.
+
+  (** Plainness *)
+  Global Instance cmra_valid_plain {A : cmra} (a : A) :
+    Plain (✓ a : uPred M)%I.
+  Proof. rewrite /Persistent. apply plainly_cmra_valid_1. Qed.
+
+  (** Persistence *)
+  Global Instance cmra_valid_persistent {A : cmra} (a : A) :
+    Persistent (✓ a : uPred M)%I.
+  Proof. rewrite /Persistent. apply persistently_cmra_valid_1. Qed.
+  Global Instance ownM_persistent a : CoreId a → Persistent (@uPred_ownM M a).
+  Proof.
+    intros. rewrite /Persistent -{2}(core_id_core a). apply persistently_ownM_core.
+  Qed.
+
+  (** For big ops *)
+  Global Instance uPred_ownM_sep_homomorphism :
+    MonoidHomomorphism op uPred_sep (≡) (@uPred_ownM M).
+  Proof. split; [split|]; try apply _; [apply ownM_op | apply ownM_unit']. Qed.
+
+  (** Soundness statement for our modalities: facts derived under modalities in
+  the empty context also without the modalities.
+  For basic updates, soundness only holds for plain propositions. *)
+  Lemma bupd_soundness P `{!Plain P} : (⊢ |==> P) → ⊢ P.
+  Proof. rewrite bupd_plain. done. Qed.
+
+  Lemma laterN_soundness P n : (⊢ ▷^n P) → ⊢ P.
+  Proof. induction n; eauto using later_soundness. Qed.
+
+  (** As pure demonstration, we also show that this holds for an arbitrary nesting
+  of modalities. We have to do a bit of work to be able to state this theorem
+  though. *)
+  Inductive modality := MBUpd | MLater | MPersistently | MPlainly.
+  Definition denote_modality (m : modality) : uPred M → uPred M :=
+    match m with
+    | MBUpd => bupd
+    | MLater => bi_later
+    | MPersistently => bi_persistently
+    | MPlainly => plainly
+    end.
+  Definition denote_modalities (ms : list modality) : uPred M → uPred M :=
+    λ P, foldr denote_modality P ms.
+
+  (** Now we can state and prove 'soundness under arbitrary modalities' for plain
+  propositions. This is probably not a lemma you want to actually use. *)
+  Corollary modal_soundness P `{!Plain P} (ms : list modality) :
+    (⊢ denote_modalities ms P) → ⊢ P.
+  Proof.
+    intros H. apply (laterN_soundness _ (length ms)).
+    move: H. apply bi_emp_valid_mono.
+    induction ms as [|m ms IH]; first done; simpl.
+    destruct m; simpl; rewrite IH.
+    - rewrite -later_intro. apply bupd_plain. apply _.
+    - done.
+    - rewrite -later_intro persistently_elim. done.
+    - rewrite -later_intro plainly_elim. done.
+  Qed.
+
+  (** Consistency: one cannot deive [False] in the logic, not even under
+  modalities. Again this is just for demonstration and probably not practically
+  useful. *)
+  Corollary consistency : ¬ ⊢@{uPredI M} False.
+  Proof. intros H. by eapply pure_soundness. Qed.
 End derived.
-
 End uPred.

iris/base_logic/proofmode.v

@@ -2,44 +2,43 @@ From iris.algebra Require Import proofmode_classes.
 From iris.proofmode Require Import classes.
 From iris.base_logic Require Export derived.
 From iris.prelude Require Import options.
-
 Import base_logic.bi.uPred.
 
 (* Setup of the proof mode *)
 Section class_instances.
-Context {M : ucmra}.
-Implicit Types P Q R : uPred M.
+  Context {M : ucmra}.
+  Implicit Types P Q R : uPred M.
 
-Global Instance into_pure_cmra_valid `{!CmraDiscrete A} (a : A) :
-  @IntoPure (uPredI M) (✓ a) (✓ a).
-Proof. by rewrite /IntoPure discrete_valid. Qed.
+  Global Instance into_pure_cmra_valid `{!CmraDiscrete A} (a : A) :
+    @IntoPure (uPredI M) (✓ a) (✓ a).
+  Proof. by rewrite /IntoPure discrete_valid. Qed.
 
-Global Instance from_pure_cmra_valid {A : cmra} (a : A) :
-  @FromPure (uPredI M) false (✓ a) (✓ a).
-Proof.
-  rewrite /FromPure /=. eapply bi.pure_elim=> // ?.
-  rewrite -uPred.cmra_valid_intro //.
-Qed.
+  Global Instance from_pure_cmra_valid {A : cmra} (a : A) :
+    @FromPure (uPredI M) false (✓ a) (✓ a).
+  Proof.
+    rewrite /FromPure /=. eapply bi.pure_elim=> // ?.
+    rewrite -uPred.cmra_valid_intro //.
+  Qed.
 
-Global Instance from_sep_ownM (a b1 b2 : M) :
-  IsOp a b1 b2 →
-  FromSep (uPred_ownM a) (uPred_ownM b1) (uPred_ownM b2).
-Proof. intros. by rewrite /FromSep -ownM_op -is_op. Qed.
-Global Instance from_sep_ownM_core_id (a b1 b2 : M) :
-  IsOp a b1 b2 → TCOr (CoreId b1) (CoreId b2) →
-  FromAnd (uPred_ownM a) (uPred_ownM b1) (uPred_ownM b2).
-Proof.
-  intros ? H. rewrite /FromAnd (is_op a) ownM_op.
-  destruct H; by rewrite bi.persistent_and_sep.
-Qed.
+  Global Instance from_sep_ownM (a b1 b2 : M) :
+    IsOp a b1 b2 →
+    FromSep (uPred_ownM a) (uPred_ownM b1) (uPred_ownM b2).
+  Proof. intros. by rewrite /FromSep -ownM_op -is_op. Qed.
+  Global Instance from_sep_ownM_core_id (a b1 b2 : M) :
+    IsOp a b1 b2 → TCOr (CoreId b1) (CoreId b2) →
+    FromAnd (uPred_ownM a) (uPred_ownM b1) (uPred_ownM b2).
+  Proof.
+    intros ? H. rewrite /FromAnd (is_op a) ownM_op.
+    destruct H; by rewrite bi.persistent_and_sep.
+  Qed.
 
-Global Instance into_and_ownM p (a b1 b2 : M) :
-  IsOp a b1 b2 → IntoAnd p (uPred_ownM a) (uPred_ownM b1) (uPred_ownM b2).
-Proof.
-  intros. apply bi.intuitionistically_if_mono. by rewrite (is_op a) ownM_op bi.sep_and.
-Qed.
+  Global Instance into_and_ownM p (a b1 b2 : M) :
+    IsOp a b1 b2 → IntoAnd p (uPred_ownM a) (uPred_ownM b1) (uPred_ownM b2).
+  Proof.
+    intros. apply bi.intuitionistically_if_mono. by rewrite (is_op a) ownM_op bi.sep_and.
+  Qed.
 
-Global Instance into_sep_ownM (a b1 b2 : M) :
-  IsOp a b1 b2 → IntoSep (uPred_ownM a) (uPred_ownM b1) (uPred_ownM b2).
-Proof. intros. by rewrite /IntoSep (is_op a) ownM_op. Qed.
+  Global Instance into_sep_ownM (a b1 b2 : M) :
+    IsOp a b1 b2 → IntoSep (uPred_ownM a) (uPred_ownM b1) (uPred_ownM b2).
+  Proof. intros. by rewrite /IntoSep (is_op a) ownM_op. Qed.
 End class_instances.

iris/si_logic/siprop.v

@@ -130,188 +130,188 @@ Local Definition siProp_unseal :=
 Ltac unseal := rewrite !siProp_unseal /=.
 
 Section primitive.
-Local Arguments siProp_holds !_ _ /.
-
-(** The notations below are implicitly local due to the section, so we do not
-mind the overlap with the general BI notations. *)
-Notation "P ⊢ Q" := (siProp_entails P Q).
-Notation "'True'" := (siProp_pure True) : bi_scope.
-Notation "'False'" := (siProp_pure False) : bi_scope.
-Notation "'⌜' φ '⌝'" := (siProp_pure φ%type%stdpp) : bi_scope.
-Infix "∧" := siProp_and : bi_scope.
-Infix "∨" := siProp_or : bi_scope.
-Infix "→" := siProp_impl : bi_scope.
-Notation "∀ x .. y , P" :=
-  (siProp_forall (λ x, .. (siProp_forall (λ y, P%I)) ..)) : bi_scope.
-Notation "∃ x .. y , P" :=
-  (siProp_exist (λ x, .. (siProp_exist (λ y, P%I)) ..)) : bi_scope.
-Notation "x ≡ y" := (siProp_internal_eq x y) : bi_scope.
-Notation "▷ P" := (siProp_later P) : bi_scope.
-
-(** Below there follow the primitive laws for [siProp]. There are no derived laws
-in this file. *)
-
-(** Entailment *)
-Lemma entails_po : PreOrder siProp_entails.
-Proof.
-  split.
-  - intros P; by split=> i.
-  - intros P Q Q' HP HQ; split=> i ?; by apply HQ, HP.
-Qed.
-Lemma entails_anti_symm : AntiSymm (≡) siProp_entails.
-Proof. intros P Q HPQ HQP; split=> n; by split; [apply HPQ|apply HQP]. Qed.
-Lemma equiv_entails P Q : (P ≡ Q) ↔ (P ⊢ Q) ∧ (Q ⊢ P).
-Proof.
-  split.
-  - intros HPQ; split; split=> i; apply HPQ.
-  - intros [??]. by apply entails_anti_symm.
-Qed.
-
-(** Non-expansiveness and setoid morphisms *)
-Lemma pure_ne n : Proper (iff ==> dist n) siProp_pure.
-Proof. intros φ1 φ2 Hφ. by unseal. Qed.
-Lemma and_ne : NonExpansive2 siProp_and.
-Proof.
-  intros n P P' HP Q Q' HQ; unseal; split=> n' ?.
-  split; (intros [??]; split; [by apply HP|by apply HQ]).
-Qed.
-Lemma or_ne : NonExpansive2 siProp_or.
-Proof.
-  intros n P P' HP Q Q' HQ; split=> n' ?.
-  unseal; split; (intros [?|?]; [left; by apply HP|right; by apply HQ]).
-Qed.
-Lemma impl_ne : NonExpansive2 siProp_impl.
-Proof.
-  intros n P P' HP Q Q' HQ; split=> n' ?.
-  unseal; split; intros HPQ n'' ??; apply HQ, HPQ, HP; auto with lia.
-Qed.
-Lemma forall_ne A n :
-  Proper (pointwise_relation _ (dist n) ==> dist n) (@siProp_forall A).
-Proof.
-   by intros Ψ1 Ψ2 HΨ; unseal; split=> n' x; split; intros HP a; apply HΨ.
-Qed.
-Lemma exist_ne A n :
-  Proper (pointwise_relation _ (dist n) ==> dist n) (@siProp_exist A).
-Proof.
-  intros Ψ1 Ψ2 HΨ.
-  unseal; split=> n' ?; split; intros [a ?]; exists a; by apply HΨ.
-Qed.
-Lemma later_contractive : Contractive siProp_later.
-Proof.
-  unseal; intros [|n] P Q HPQ; split=> -[|n'] ? //=; try lia.
-  apply HPQ; lia.
-Qed.
-Lemma internal_eq_ne (A : ofe) : NonExpansive2 (@siProp_internal_eq A).
-Proof.
-  intros n 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.
-
-(** Introduction and elimination rules *)
-Lemma pure_intro (φ : Prop) P : φ → P ⊢ ⌜ φ ⌝.
-Proof. intros ?. unseal; by split. Qed.
-Lemma pure_elim' (φ : Prop) P : (φ → True ⊢ P) → ⌜ φ ⌝ ⊢ P.
-Proof. unseal=> HP; split=> n ?. by apply HP. Qed.
-Lemma pure_forall_2 {A} (φ : A → Prop) : (∀ a, ⌜ φ a ⌝) ⊢ ⌜ ∀ a, φ a ⌝.
-Proof. by unseal. Qed.
-
-Lemma and_elim_l P Q : P ∧ Q ⊢ P.
-Proof. unseal; by split=> n [??]. Qed.
-Lemma and_elim_r P Q : P ∧ Q ⊢ Q.
-Proof. unseal; by split=> n [??]. Qed.
-Lemma and_intro P Q R : (P ⊢ Q) → (P ⊢ R) → P ⊢ Q ∧ R.
-Proof.
-  intros HQ HR; unseal; split=> n ?.
-  split.
-  - by apply HQ.
-  - by apply HR.
-Qed.
-
-Lemma or_intro_l P Q : P ⊢ P ∨ Q.
-Proof. unseal; split=> n ?; left; auto. Qed.
-Lemma or_intro_r P Q : Q ⊢ P ∨ Q.
-Proof. unseal; split=> n ?; right; auto. Qed.
-Lemma or_elim P Q R : (P ⊢ R) → (Q ⊢ R) → P ∨ Q ⊢ R.
-Proof.
-  intros HP HQ. unseal; split=> n [?|?].
-  - by apply HP.
-  - by apply HQ.
-Qed.
-
-Lemma impl_intro_r P Q R : (P ∧ Q ⊢ R) → P ⊢ Q → R.
-Proof.
-  unseal=> HQ; split=> n ? n' ??.
-  apply HQ; naive_solver eauto using siProp_closed.
-Qed.
-Lemma impl_elim_l' P Q R : (P ⊢ Q → R) → P ∧ Q ⊢ R.
-Proof. unseal=> HP; split=> n [??]. apply HP with n; auto. Qed.
-
-Lemma forall_intro {A} P (Ψ : A → siProp) : (∀ a, P ⊢ Ψ a) → P ⊢ ∀ a, Ψ a.
-Proof. unseal; intros HPΨ; split=> n ? a; by apply HPΨ. Qed.
-Lemma forall_elim {A} {Ψ : A → siProp} a : (∀ a, Ψ a) ⊢ Ψ a.
-Proof. unseal; split=> n HP; apply HP. Qed.
-
-Lemma exist_intro {A} {Ψ : A → siProp} a : Ψ a ⊢ ∃ a, Ψ a.
-Proof. unseal; split=> n ?; by exists a. Qed.
-Lemma exist_elim {A} (Φ : A → siProp) Q : (∀ a, Φ a ⊢ Q) → (∃ a, Φ a) ⊢ Q.
-Proof. unseal; intros HΨ; split=> n [a ?]; by apply HΨ with a. Qed.
-
-(** Equality *)
-Lemma internal_eq_refl {A : ofe} P (a : A) : P ⊢ (a ≡ a).
-Proof. unseal; by split=> n ? /=. Qed.
-Lemma internal_eq_rewrite {A : ofe} a b (Ψ : A → siProp) :
-  NonExpansive Ψ → a ≡ b ⊢ Ψ a → Ψ b.
-Proof.
-  intros Hnonexp. unseal; split=> n Hab n' ? HΨ. eapply Hnonexp with n a; auto.
-Qed.
-
-Lemma fun_ext {A} {B : A → ofe} (f g : discrete_fun B) : (∀ x, f x ≡ g x) ⊢ f ≡ g.
-Proof. by unseal. Qed.
-Lemma sig_eq {A : ofe} (P : A → Prop) (x y : sig P) : `x ≡ `y ⊢ x ≡ y.
-Proof. by unseal. Qed.
-Lemma discrete_eq_1 {A : ofe} (a b : A) : Discrete a → a ≡ b ⊢ ⌜a ≡ b⌝.
-Proof. unseal=> ?. split=> n. by apply (discrete_iff n). Qed.
-
-Lemma prop_ext_2 P Q : ((P → Q) ∧ (Q → P)) ⊢ P ≡ Q.
-Proof.
-  unseal; split=> n /= HPQ. split=> n' ?.
-  move: HPQ=> [] /(_ n') ? /(_ n'). naive_solver.
-Qed.
-
-(** Later *)
-Lemma later_eq_1 {A : ofe} (x y : A) : Next x ≡ Next y ⊢ ▷ (x ≡ y).
-Proof. by unseal. Qed.
-Lemma later_eq_2 {A : ofe} (x y : A) : ▷ (x ≡ y) ⊢ Next x ≡ Next y.
-Proof. by unseal. Qed.
-
-Lemma later_mono P Q : (P ⊢ Q) → ▷ P ⊢ ▷ Q.
-Proof. unseal=> HP; split=>-[|n]; [done|apply HP; eauto using cmra_validN_S]. Qed.
-Lemma later_intro P : P ⊢ ▷ P.
-Proof. unseal; split=> -[|n] /= HP; eauto using siProp_closed. Qed.
-
-Lemma later_forall_2 {A} (Φ : A → siProp) : (∀ a, ▷ Φ a) ⊢ ▷ ∀ a, Φ a.
-Proof. unseal; by split=> -[|n]. Qed.
-Lemma later_exist_false {A} (Φ : A → siProp) :
-  (▷ ∃ a, Φ a) ⊢ ▷ False ∨ (∃ a, ▷ Φ a).
-Proof. unseal; split=> -[|[|n]] /=; eauto. Qed.
-Lemma later_false_em P : ▷ P ⊢ ▷ False ∨ (▷ False → P).
-Proof.
-  unseal; split=> -[|n] /= HP; [by left|right].
-  intros [|n'] ?; eauto using siProp_closed with lia.
-Qed.
-
-(** Consistency/soundness statement *)
-Lemma pure_soundness φ : (True ⊢ ⌜ φ ⌝) → φ.
-Proof. unseal=> -[H]. by apply (H 0). Qed.
-
-Lemma internal_eq_soundness {A : ofe} (x y : A) : (True ⊢ x ≡ y) → x ≡ y.
-Proof. unseal=> -[H]. apply equiv_dist=> n. by apply (H n). Qed.
-
-Lemma later_soundness P : (True ⊢ ▷ P) → (True ⊢ P).
-Proof.
-  unseal=> -[HP]; split=> n _. apply siProp_closed with n; last done.
-  by apply (HP (S n)).
-Qed.
+  Local Arguments siProp_holds !_ _ /.
+
+  (** The notations below are implicitly local due to the section, so we do not
+  mind the overlap with the general BI notations. *)
+  Notation "P ⊢ Q" := (siProp_entails P Q).
+  Notation "'True'" := (siProp_pure True) : bi_scope.
+  Notation "'False'" := (siProp_pure False) : bi_scope.
+  Notation "'⌜' φ '⌝'" := (siProp_pure φ%type%stdpp) : bi_scope.
+  Infix "∧" := siProp_and : bi_scope.
+  Infix "∨" := siProp_or : bi_scope.
+  Infix "→" := siProp_impl : bi_scope.
+  Notation "∀ x .. y , P" :=
+    (siProp_forall (λ x, .. (siProp_forall (λ y, P%I)) ..)) : bi_scope.
+  Notation "∃ x .. y , P" :=
+    (siProp_exist (λ x, .. (siProp_exist (λ y, P%I)) ..)) : bi_scope.
+  Notation "x ≡ y" := (siProp_internal_eq x y) : bi_scope.
+  Notation "▷ P" := (siProp_later P) : bi_scope.
+
+  (** Below there follow the primitive laws for [siProp]. There are no derived laws
+  in this file. *)
+
+  (** Entailment *)
+  Lemma entails_po : PreOrder siProp_entails.
+  Proof.
+    split.
+    - intros P; by split=> i.
+    - intros P Q Q' HP HQ; split=> i ?; by apply HQ, HP.
+  Qed.
+  Lemma entails_anti_symm : AntiSymm (≡) siProp_entails.
+  Proof. intros P Q HPQ HQP; split=> n; by split; [apply HPQ|apply HQP]. Qed.
+  Lemma equiv_entails P Q : (P ≡ Q) ↔ (P ⊢ Q) ∧ (Q ⊢ P).
+  Proof.
+    split.
+    - intros HPQ; split; split=> i; apply HPQ.
+    - intros [??]. by apply entails_anti_symm.
+  Qed.
+
+  (** Non-expansiveness and setoid morphisms *)
+  Lemma pure_ne n : Proper (iff ==> dist n) siProp_pure.
+  Proof. intros φ1 φ2 Hφ. by unseal. Qed.
+  Lemma and_ne : NonExpansive2 siProp_and.
+  Proof.
+    intros n P P' HP Q Q' HQ; unseal; split=> n' ?.
+    split; (intros [??]; split; [by apply HP|by apply HQ]).
+  Qed.
+  Lemma or_ne : NonExpansive2 siProp_or.
+  Proof.
+    intros n P P' HP Q Q' HQ; split=> n' ?.
+    unseal; split; (intros [?|?]; [left; by apply HP|right; by apply HQ]).
+  Qed.
+  Lemma impl_ne : NonExpansive2 siProp_impl.
+  Proof.
+    intros n P P' HP Q Q' HQ; split=> n' ?.
+    unseal; split; intros HPQ n'' ??; apply HQ, HPQ, HP; auto with lia.
+  Qed.
+  Lemma forall_ne A n :
+    Proper (pointwise_relation _ (dist n) ==> dist n) (@siProp_forall A).
+  Proof.
+     by intros Ψ1 Ψ2 HΨ; unseal; split=> n' x; split; intros HP a; apply HΨ.
+  Qed.
+  Lemma exist_ne A n :
+    Proper (pointwise_relation _ (dist n) ==> dist n) (@siProp_exist A).
+  Proof.
+    intros Ψ1 Ψ2 HΨ.
+    unseal; split=> n' ?; split; intros [a ?]; exists a; by apply HΨ.
+  Qed.
+  Lemma later_contractive : Contractive siProp_later.
+  Proof.
+    unseal; intros [|n] P Q HPQ; split=> -[|n'] ? //=; try lia.
+    apply HPQ; lia.
+  Qed.
+  Lemma internal_eq_ne (A : ofe) : NonExpansive2 (@siProp_internal_eq A).
+  Proof.
+    intros n 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.
+
+  (** Introduction and elimination rules *)
+  Lemma pure_intro (φ : Prop) P : φ → P ⊢ ⌜ φ ⌝.
+  Proof. intros ?. unseal; by split. Qed.
+  Lemma pure_elim' (φ : Prop) P : (φ → True ⊢ P) → ⌜ φ ⌝ ⊢ P.
+  Proof. unseal=> HP; split=> n ?. by apply HP. Qed.
+  Lemma pure_forall_2 {A} (φ : A → Prop) : (∀ a, ⌜ φ a ⌝) ⊢ ⌜ ∀ a, φ a ⌝.
+  Proof. by unseal. Qed.
+
+  Lemma and_elim_l P Q : P ∧ Q ⊢ P.
+  Proof. unseal; by split=> n [??]. Qed.
+  Lemma and_elim_r P Q : P ∧ Q ⊢ Q.
+  Proof. unseal; by split=> n [??]. Qed.
+  Lemma and_intro P Q R : (P ⊢ Q) → (P ⊢ R) → P ⊢ Q ∧ R.
+  Proof.
+    intros HQ HR; unseal; split=> n ?.
+    split.
+    - by apply HQ.
+    - by apply HR.
+  Qed.
+
+  Lemma or_intro_l P Q : P ⊢ P ∨ Q.
+  Proof. unseal; split=> n ?; left; auto. Qed.
+  Lemma or_intro_r P Q : Q ⊢ P ∨ Q.
+  Proof. unseal; split=> n ?; right; auto. Qed.
+  Lemma or_elim P Q R : (P ⊢ R) → (Q ⊢ R) → P ∨ Q ⊢ R.
+  Proof.
+    intros HP HQ. unseal; split=> n [?|?].
+    - by apply HP.
+    - by apply HQ.
+  Qed.
+
+  Lemma impl_intro_r P Q R : (P ∧ Q ⊢ R) → P ⊢ Q → R.
+  Proof.
+    unseal=> HQ; split=> n ? n' ??.
+    apply HQ; naive_solver eauto using siProp_closed.
+  Qed.
+  Lemma impl_elim_l' P Q R : (P ⊢ Q → R) → P ∧ Q ⊢ R.
+  Proof. unseal=> HP; split=> n [??]. apply HP with n; auto. Qed.
+
+  Lemma forall_intro {A} P (Ψ : A → siProp) : (∀ a, P ⊢ Ψ a) → P ⊢ ∀ a, Ψ a.
+  Proof. unseal; intros HPΨ; split=> n ? a; by apply HPΨ. Qed.
+  Lemma forall_elim {A} {Ψ : A → siProp} a : (∀ a, Ψ a) ⊢ Ψ a.
+  Proof. unseal; split=> n HP; apply HP. Qed.
+
+  Lemma exist_intro {A} {Ψ : A → siProp} a : Ψ a ⊢ ∃ a, Ψ a.
+  Proof. unseal; split=> n ?; by exists a. Qed.
+  Lemma exist_elim {A} (Φ : A → siProp) Q : (∀ a, Φ a ⊢ Q) → (∃ a, Φ a) ⊢ Q.
+  Proof. unseal; intros HΨ; split=> n [a ?]; by apply HΨ with a. Qed.
+
+  (** Equality *)
+  Lemma internal_eq_refl {A : ofe} P (a : A) : P ⊢ (a ≡ a).
+  Proof. unseal; by split=> n ? /=. Qed.
+  Lemma internal_eq_rewrite {A : ofe} a b (Ψ : A → siProp) :
+    NonExpansive Ψ → a ≡ b ⊢ Ψ a → Ψ b.
+  Proof.
+    intros Hnonexp. unseal; split=> n Hab n' ? HΨ. eapply Hnonexp with n a; auto.
+  Qed.
+
+  Lemma fun_ext {A} {B : A → ofe} (f g : discrete_fun B) : (∀ x, f x ≡ g x) ⊢ f ≡ g.
+  Proof. by unseal. Qed.
+  Lemma sig_eq {A : ofe} (P : A → Prop) (x y : sig P) : `x ≡ `y ⊢ x ≡ y.
+  Proof. by unseal. Qed.
+  Lemma discrete_eq_1 {A : ofe} (a b : A) : Discrete a → a ≡ b ⊢ ⌜a ≡ b⌝.
+  Proof. unseal=> ?. split=> n. by apply (discrete_iff n). Qed.
+
+  Lemma prop_ext_2 P Q : ((P → Q) ∧ (Q → P)) ⊢ P ≡ Q.
+  Proof.
+    unseal; split=> n /= HPQ. split=> n' ?.
+    move: HPQ=> [] /(_ n') ? /(_ n'). naive_solver.
+  Qed.
+
+  (** Later *)
+  Lemma later_eq_1 {A : ofe} (x y : A) : Next x ≡ Next y ⊢ ▷ (x ≡ y).
+  Proof. by unseal. Qed.
+  Lemma later_eq_2 {A : ofe} (x y : A) : ▷ (x ≡ y) ⊢ Next x ≡ Next y.
+  Proof. by unseal. Qed.
+
+  Lemma later_mono P Q : (P ⊢ Q) → ▷ P ⊢ ▷ Q.
+  Proof. unseal=> HP; split=>-[|n]; [done|apply HP; eauto using cmra_validN_S]. Qed.
+  Lemma later_intro P : P ⊢ ▷ P.
+  Proof. unseal; split=> -[|n] /= HP; eauto using siProp_closed. Qed.
+
+  Lemma later_forall_2 {A} (Φ : A → siProp) : (∀ a, ▷ Φ a) ⊢ ▷ ∀ a, Φ a.
+  Proof. unseal; by split=> -[|n]. Qed.
+  Lemma later_exist_false {A} (Φ : A → siProp) :
+    (▷ ∃ a, Φ a) ⊢ ▷ False ∨ (∃ a, ▷ Φ a).
+  Proof. unseal; split=> -[|[|n]] /=; eauto. Qed.
+  Lemma later_false_em P : ▷ P ⊢ ▷ False ∨ (▷ False → P).
+  Proof.
+    unseal; split=> -[|n] /= HP; [by left|right].
+    intros [|n'] ?; eauto using siProp_closed with lia.
+  Qed.
+
+  (** Consistency/soundness statement *)
+  Lemma pure_soundness φ : (True ⊢ ⌜ φ ⌝) → φ.
+  Proof. unseal=> -[H]. by apply (H 0). Qed.
+
+  Lemma internal_eq_soundness {A : ofe} (x y : A) : (True ⊢ x ≡ y) → x ≡ y.
+  Proof. unseal=> -[H]. apply equiv_dist=> n. by apply (H n). Qed.
+
+  Lemma later_soundness P : (True ⊢ ▷ P) → (True ⊢ P).
+  Proof.
+    unseal=> -[HP]; split=> n _. apply siProp_closed with n; last done.
+    by apply (HP (S n)).
+  Qed.
 End primitive.
 End siProp_primitive.