From 02bc52b4d905eb635940ff8545d59676ad44ea8c Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 8 Jan 2017 14:21:09 +0100
Subject: [PATCH] Seal off iRes using a module.

This makes lambdarust 1 min (=7%) faster.
---
 theories/base_logic/lib/iprop.v | 66 +++++++++++++++++++++++++++++++--
 theories/base_logic/lib/own.v   | 44 ++++++----------------
 2 files changed, 74 insertions(+), 36 deletions(-)

diff --git a/theories/base_logic/lib/iprop.v b/theories/base_logic/lib/iprop.v
index 95a378c30..fd6abfdd8 100644
--- a/theories/base_logic/lib/iprop.v
+++ b/theories/base_logic/lib/iprop.v
@@ -1,6 +1,7 @@
 From iris.base_logic Require Export base_logic.
 From iris.algebra Require Import iprod gmap.
 From iris.algebra Require cofe_solver.
+Import uPred.
 Set Default Proof Using "Type".
 
 (** In this file we construct the type [iProp] of propositions of the Iris
@@ -115,10 +116,30 @@ the construction, this way we are sure we do not use any properties of the
 construction, and also avoid Coq from blindly unfolding it. *)
 Module Type iProp_solution_sig.
   Parameter iPreProp : gFunctors → ofeT.
-  Definition iResUR (Σ : gFunctors) : ucmraT :=
-    iprodUR (λ i, gmapUR gname (Σ i (iPreProp Σ))).
-  Notation iProp Σ := (uPredC (iResUR Σ)).
+  Parameter iResUR : gFunctors → ucmraT.
+
+  Parameter iRes_singleton :
+    ∀ {Σ} (i : gid Σ) (γ : gname) (a : Σ i (iPreProp Σ)), iResUR Σ.
+  Parameter iRes_ne : ∀ Σ (i : gid Σ) γ, NonExpansive (iRes_singleton i γ).
+  Parameter iRes_op : ∀ Σ (i : gid Σ) γ a1 a2,
+    iRes_singleton i γ (a1 ⋅ a2) ≡ iRes_singleton i γ a1 ⋅ iRes_singleton i γ a2.
+  Parameter iRes_valid : ∀ {M} Σ (i : gid Σ) γ a,
+    ✓ iRes_singleton i γ a -∗ (✓ a : uPred M).
+  Parameter iRes_timeless : ∀ Σ (i : gid Σ) γ a,
+    Timeless a → Timeless (iRes_singleton i γ a).
+  Parameter iRes_persistent : ∀ Σ (i : gid Σ) γ a,
+    Persistent a → Persistent (iRes_singleton i γ a).
+  Parameter iRes_updateP : ∀ Σ (i : gid Σ) γ
+      (P : Σ i (iPreProp Σ) → Prop) (Q : iResUR Σ → Prop) a,
+    a ~~>: P → (∀ b, P b → Q (iRes_singleton i γ b)) →
+    iRes_singleton i γ a ~~>: Q.
+  Parameter iRes_alloc_strong : ∀ Σ (i : gid Σ)
+      (Q : iResUR Σ → Prop) (G : gset gname) (a : Σ i (iPreProp Σ)),
+    ✓ a → (∀ γ, γ ∉ G → Q (iRes_singleton i γ a)) → ∅ ~~>: Q.
+  Parameter iRes_alloc_unit_singleton : ∀ Σ (i : gid Σ) u γ,
+    ✓ u → LeftId (≡) u (⋅) → ∅ ~~> iRes_singleton i γ u.
 
+  Notation iProp Σ := (uPredC (iResUR Σ)).
   Parameter iProp_unfold: ∀ {Σ}, iProp Σ -n> iPreProp Σ.
   Parameter iProp_fold: ∀ {Σ}, iPreProp Σ -n> iProp Σ.
   Parameter iProp_fold_unfold: ∀ {Σ} (P : iProp Σ),
@@ -135,8 +156,45 @@ Module Export iProp_solution : iProp_solution_sig.
   Definition iPreProp (Σ : gFunctors) : ofeT := iProp_result Σ.
   Definition iResUR (Σ : gFunctors) : ucmraT :=
     iprodUR (λ i, gmapUR gname (Σ i (iPreProp Σ))).
-  Notation iProp Σ := (uPredC (iResUR Σ)).
 
+  Definition iRes_singleton {Σ}
+      (i : gid Σ) (γ : gname) (a : Σ i (iPreProp Σ)) : iResUR Σ :=
+    iprod_singleton i {[ γ := a ]}.
+  Lemma iRes_ne Σ (i : gid Σ) γ : NonExpansive (iRes_singleton i γ).
+  Proof. by intros n a a' Ha; apply iprod_singleton_ne; rewrite Ha. Qed.
+  Lemma iRes_op Σ (i : gid Σ) γ a1 a2 :
+    iRes_singleton i γ (a1 ⋅ a2) ≡ iRes_singleton i γ a1 ⋅ iRes_singleton i γ a2.
+  Proof. by rewrite /iRes_singleton iprod_op_singleton op_singleton. Qed.
+  Lemma iRes_valid {M} Σ (i : gid Σ) γ a :
+    ✓ iRes_singleton i γ a -∗ (✓ a : uPred M).
+  Proof.
+    rewrite /iRes_singleton iprod_validI (forall_elim i) iprod_lookup_singleton.
+    by rewrite gmap_validI (forall_elim γ) lookup_singleton option_validI.
+  Qed.
+  Definition iRes_timeless Σ (i : gid Σ) γ a :
+    Timeless a → Timeless (iRes_singleton i γ a) := _.
+  Definition iRes_persistent Σ (i : gid Σ) γ a :
+    Persistent a → Persistent (iRes_singleton i γ a) := _.
+  Lemma iRes_updateP Σ (i : gid Σ) γ (P : _ → Prop) (Q : iResUR Σ → Prop) a :
+    a ~~>: P → (∀ b, P b → Q (iRes_singleton i γ b)) →
+    iRes_singleton i γ a ~~>: Q.
+  Proof.
+    intros. eapply iprod_singleton_updateP;
+      [by apply singleton_updateP'|naive_solver].
+  Qed.
+  Lemma iRes_alloc_strong Σ (i : gid Σ) (Q : _ → Prop) (G : gset gname) a :
+    ✓ a → (∀ γ, γ ∉ G → Q (iRes_singleton i γ a)) → ∅ ~~>: Q.
+  Proof.
+    intros Ha ?. eapply iprod_singleton_updateP_empty;
+      [eapply alloc_updateP_strong', Ha|naive_solver].
+  Qed.
+  Lemma iRes_alloc_unit_singleton Σ (i : gid Σ) u γ :
+    ✓ u → LeftId (≡) u (⋅) → ∅ ~~> iRes_singleton i γ u.
+  Proof.
+    intros. by eapply iprod_singleton_update_empty, alloc_unit_singleton_update.
+  Qed.
+
+  Notation iProp Σ := (uPredC (iResUR Σ)).
   Definition iProp_unfold {Σ} : iProp Σ -n> iPreProp Σ :=
     solution_fold (iProp_result Σ).
   Definition iProp_fold {Σ} : iPreProp Σ -n> iProp Σ := solution_unfold _.
diff --git a/theories/base_logic/lib/own.v b/theories/base_logic/lib/own.v
index 24c20fae6..5a4a60df2 100644
--- a/theories/base_logic/lib/own.v
+++ b/theories/base_logic/lib/own.v
@@ -48,12 +48,8 @@ Ltac solve_inG :=
   split; (assumption || by apply _).
 
 (** * Definition of the connective [own] *)
-Definition iRes_singleton `{i : inG Σ A} (γ : gname) (a : A) : iResUR Σ :=
-  iprod_singleton (inG_id i) {[ γ := cmra_transport inG_prf a ]}.
-Instance: Params (@iRes_singleton) 4.
-
 Definition own_def `{inG Σ A} (γ : gname) (a : A) : iProp Σ :=
-  uPred_ownM (iRes_singleton γ a).
+  uPred_ownM (iRes_singleton (inG_id _) γ (cmra_transport inG_prf a)).
 Definition own_aux : seal (@own_def). by eexists. Qed.
 Definition own {Σ A i} := unseal own_aux Σ A i.
 Definition own_eq : @own = @own_def := seal_eq own_aux.
@@ -65,16 +61,6 @@ Section global.
 Context `{inG Σ A}.
 Implicit Types a : A.
 
-(** ** Properties of [iRes_singleton] *)
-Global Instance iRes_singleton_ne γ :
-  NonExpansive (@iRes_singleton Σ A _ γ).
-Proof. by intros n a a' Ha; apply iprod_singleton_ne; rewrite Ha. Qed.
-Lemma iRes_singleton_op γ a1 a2 :
-  iRes_singleton γ (a1 ⋅ a2) ≡ iRes_singleton γ a1 ⋅ iRes_singleton γ a2.
-Proof.
-  by rewrite /iRes_singleton iprod_op_singleton op_singleton cmra_transport_op.
-Qed.
-
 (** ** Properties of [own] *)
 Global Instance own_ne γ : NonExpansive (@own Σ A _ γ).
 Proof. rewrite !own_eq. solve_proper. Qed.
@@ -82,7 +68,7 @@ Global Instance own_proper γ :
   Proper ((≡) ==> (⊣⊢)) (@own Σ A _ γ) := ne_proper _.
 
 Lemma own_op γ a1 a2 : own γ (a1 ⋅ a2) ⊣⊢ own γ a1 ∗ own γ a2.
-Proof. by rewrite !own_eq /own_def -ownM_op iRes_singleton_op. Qed.
+Proof. by rewrite !own_eq /own_def -ownM_op cmra_transport_op iRes_op. Qed.
 Lemma own_mono γ a1 a2 : a2 ≼ a1 → own γ a1 ⊢ own γ a2.
 Proof. move=> [c ->]. rewrite own_op. eauto with I. Qed.
 
@@ -92,13 +78,7 @@ Global Instance own_mono' γ : Proper (flip (≼) ==> (⊢)) (@own Σ A _ γ).
 Proof. intros a1 a2. apply own_mono. Qed.
 
 Lemma own_valid γ a : own γ a ⊢ ✓ a.
-Proof.
-  rewrite !own_eq /own_def ownM_valid /iRes_singleton.
-  rewrite iprod_validI (forall_elim (inG_id _)) iprod_lookup_singleton.
-  rewrite gmap_validI (forall_elim γ) lookup_singleton option_validI.
-  (* implicit arguments differ a bit *)
-  by trans (✓ cmra_transport inG_prf a : iProp Σ)%I; last destruct inG_prf.
-Qed.
+Proof. rewrite !own_eq /own_def ownM_valid iRes_valid. by destruct inG_prf. Qed.
 Lemma own_valid_2 γ a1 a2 : own γ a1 -∗ own γ a2 -∗ ✓ (a1 ⋅ a2).
 Proof. apply wand_intro_r. by rewrite -own_op own_valid. Qed.
 Lemma own_valid_3 γ a1 a2 a3 : own γ a1 -∗ own γ a2 -∗ own γ a3 -∗ ✓ (a1 ⋅ a2 ⋅ a3).
@@ -120,11 +100,11 @@ Lemma own_alloc_strong a (G : gset gname) :
   ✓ a → (|==> ∃ γ, ⌜γ ∉ G⌝ ∧ own γ a)%I.
 Proof.
   intros Ha.
-  rewrite -(bupd_mono (∃ m, ⌜∃ γ, γ ∉ G ∧ m = iRes_singleton γ a⌝ ∧ uPred_ownM m)%I).
+  rewrite -(bupd_mono (∃ m, ⌜∃ γ, γ ∉ G ∧
+    m = iRes_singleton (inG_id _) γ (cmra_transport inG_prf a)⌝ ∧ uPred_ownM m))%I.
   - rewrite /uPred_valid ownM_empty.
-    eapply bupd_ownM_updateP, (iprod_singleton_updateP_empty (inG_id _));
-      first (eapply alloc_updateP_strong', cmra_transport_valid, Ha);
-      naive_solver.
+    eapply bupd_ownM_updateP, iRes_alloc_strong;
+      [eapply cmra_transport_valid, Ha|naive_solver].
   - apply exist_elim=>m; apply pure_elim_l=>-[γ [Hfresh ->]].
     by rewrite !own_eq /own_def -(exist_intro γ) pure_True // left_id.
 Qed.
@@ -138,9 +118,10 @@ Qed.
 Lemma own_updateP P γ a : a ~~>: P → own γ a ==∗ ∃ a', ⌜P a'⌝ ∧ own γ a'.
 Proof.
   intros Ha. rewrite !own_eq.
-  rewrite -(bupd_mono (∃ m, ⌜∃ a', m = iRes_singleton γ a' ∧ P a'⌝ ∧ uPred_ownM m)%I).
-  - eapply bupd_ownM_updateP, iprod_singleton_updateP;
-      first by (eapply singleton_updateP', cmra_transport_updateP', Ha).
+  rewrite -(bupd_mono (∃ m, ⌜∃ a',
+    m = iRes_singleton (inG_id _) γ (cmra_transport inG_prf a') ∧
+    P a'⌝ ∧ uPred_ownM m)%I).
+  - eapply bupd_ownM_updateP, iRes_updateP; [by apply cmra_transport_updateP'|].
     naive_solver.
   - apply exist_elim=>m; apply pure_elim_l=>-[a' [-> HP]].
     rewrite -(exist_intro a'). by apply and_intro; [apply pure_intro|].
@@ -172,8 +153,7 @@ Arguments own_update_3 {_ _} [_] _ _ _ _ _ _.
 Lemma own_empty A `{inG Σ (A:ucmraT)} γ : (|==> own γ ∅)%I.
 Proof.
   rewrite /uPred_valid ownM_empty !own_eq /own_def.
-  apply bupd_ownM_update, iprod_singleton_update_empty.
-  apply (alloc_unit_singleton_update (cmra_transport inG_prf ∅)); last done.
+  apply bupd_ownM_update, iRes_alloc_unit_singleton.
   - apply cmra_transport_valid, ucmra_unit_valid.
   - intros x; destruct inG_prf. by rewrite left_id.
 Qed.
-- 
GitLab