From 7ca7ad538fdd00d86ffcddce7d87216f4d673c17 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 8 Feb 2016 17:39:01 +0100
Subject: [PATCH] Do not export ownership

Actual proofs will end up using own and inv, and none of the notions defined in ownership.v
---
 heap_lang/lifting.v           |  2 +-
 heap_lang/tests.v             |  2 +-
 program_logic/adequacy.v      |  2 +-
 program_logic/global_cmra.v   | 43 ++++++++++++++++++-----------------
 program_logic/hoare_lifting.v |  1 +
 program_logic/lifting.v       |  2 +-
 program_logic/namespace.v     |  3 ++-
 program_logic/pviewshifts.v   |  5 ++--
 program_logic/viewshifts.v    |  1 +
 9 files changed, 33 insertions(+), 28 deletions(-)

diff --git a/heap_lang/lifting.v b/heap_lang/lifting.v
index a6793e3e5..4c93c721a 100644
--- a/heap_lang/lifting.v
+++ b/heap_lang/lifting.v
@@ -1,4 +1,4 @@
-Require Import prelude.gmap program_logic.lifting.
+Require Import prelude.gmap program_logic.lifting program_logic.ownership.
 Require Export program_logic.weakestpre heap_lang.heap_lang_tactics.
 Import uPred heap_lang.
 Local Hint Extern 0 (language.reducible _ _) => do_step ltac:(eauto 2).
diff --git a/heap_lang/tests.v b/heap_lang/tests.v
index 509edcb65..6996b7096 100644
--- a/heap_lang/tests.v
+++ b/heap_lang/tests.v
@@ -1,5 +1,5 @@
 (** This file is essentially a bunch of testcases. *)
-Require Import program_logic.upred.
+Require Import program_logic.upred program_logic.ownership.
 Require Import heap_lang.lifting heap_lang.sugar.
 Import heap_lang uPred notations.
 
diff --git a/program_logic/adequacy.v b/program_logic/adequacy.v
index 9c0d6f339..930c17e49 100644
--- a/program_logic/adequacy.v
+++ b/program_logic/adequacy.v
@@ -1,5 +1,5 @@
 Require Export program_logic.hoare.
-Require Import program_logic.wsat.
+Require Import program_logic.wsat program_logic.ownership.
 Local Hint Extern 10 (_ ≤ _) => omega.
 Local Hint Extern 100 (@eq coPset _ _) => eassumption || solve_elem_of.
 Local Hint Extern 10 (✓{_} _) =>
diff --git a/program_logic/global_cmra.v b/program_logic/global_cmra.v
index c93d2518c..a79fce247 100644
--- a/program_logic/global_cmra.v
+++ b/program_logic/global_cmra.v
@@ -1,24 +1,25 @@
-Require Export algebra.iprod program_logic.ownership program_logic.pviewshifts.
+Require Export algebra.iprod program_logic.pviewshifts.
+Require Import program_logic.ownership.
 Import uPred.
 
 Definition gid := positive.
-Definition globalC (Δ : gid → iFunctor) : iFunctor :=
-  iprodF (λ i, mapF gid (Δ i)).
+Definition globalC (Σ : gid → iFunctor) : iFunctor :=
+  iprodF (λ i, mapF gid (Σ i)).
 
-Class InG Λ (Δ : gid → iFunctor) (i : gid) (A : cmraT) :=
-  inG : A = Δ i (laterC (iPreProp Λ (globalC Δ))).
-Definition to_funC {Λ} {Δ : gid → iFunctor} (i : gid) 
-           `{!InG Λ Δ i A} (a : A) : Δ i (laterC (iPreProp Λ (globalC Δ))) :=
+Class InG Λ (Σ : gid → iFunctor) (i : gid) (A : cmraT) :=
+  inG : A = Σ i (laterC (iPreProp Λ (globalC Σ))).
+Definition to_Σ {Λ} {Σ : gid → iFunctor} (i : gid) 
+           `{!InG Λ Σ i A} (a : A) : Σ i (laterC (iPreProp Λ (globalC Σ))) :=
   eq_rect A id a _ inG.
-Definition to_globalC {Λ} {Δ : gid → iFunctor}
-           (i : gid) (γ : gid) `{!InG Λ Δ i A} (a : A) : iGst Λ (globalC Δ) :=
-  iprod_singleton i {[ γ ↦ to_funC _ a ]}.
-Definition own {Λ} {Δ : gid → iFunctor}
-    (i : gid) `{!InG Λ Δ i A} (γ : gid) (a : A) : iProp Λ (globalC Δ) :=
-  ownG (Σ:=globalC Δ) (to_globalC i γ a).
+Definition to_globalC {Λ} {Σ : gid → iFunctor}
+           (i : gid) (γ : gid) `{!InG Λ Σ i A} (a : A) : iGst Λ (globalC Σ) :=
+  iprod_singleton i {[ γ ↦ to_Σ _ a ]}.
+Definition own {Λ} {Σ : gid → iFunctor}
+    (i : gid) `{!InG Λ Σ i A} (γ : gid) (a : A) : iProp Λ (globalC Σ) :=
+  ownG (to_globalC i γ a).
 
 Section global.
-Context {Λ : language} {Δ : gid → iFunctor} (i : gid) `{!InG Λ Δ i A}.
+Context {Λ : language} {Σ : gid → iFunctor} (i : gid) `{!InG Λ Σ i A}.
 Implicit Types a : A.
 
 (* Proeprties of to_globalC *)
@@ -27,7 +28,7 @@ Lemma globalC_op γ a1 a2 :
 Proof.
   rewrite /to_globalC iprod_op_singleton map_op_singleton.
   apply iprod_singleton_proper, (fin_maps.singleton_proper (M:=gmap _)).
-  by rewrite /to_funC; destruct inG.
+  by rewrite /to_Σ; destruct inG.
 Qed.
 
 Lemma globalC_validN n γ a :
@@ -35,7 +36,7 @@ Lemma globalC_validN n γ a :
 Proof.
   rewrite /to_globalC.
   rewrite -iprod_validN_singleton -map_validN_singleton.
-  by rewrite /to_funC; destruct inG.
+  by rewrite /to_Σ; destruct inG.
 Qed.
 
 (* Properties of own *)
@@ -43,7 +44,7 @@ Qed.
 Global Instance own_ne γ n : Proper (dist n ==> dist n) (own i γ).
 Proof.
   intros m m' Hm; apply ownG_ne, iprod_singleton_ne, singleton_ne.
-  by rewrite /to_globalC /to_funC; destruct inG.
+  by rewrite /to_globalC /to_Σ; destruct inG.
 Qed.
 
 Global Instance own_proper γ : Proper ((≡) ==> (≡)) (own i γ) := ne_proper _.
@@ -54,14 +55,14 @@ Proof. rewrite /own -ownG_op. apply ownG_proper, globalC_op. Qed.
 (* TODO: This also holds if we just have ✓a at the current step-idx, as Iris
    assertion. However, the map_updateP_alloc does not suffice to show this. *)
 Lemma own_alloc E a :
-  ✓a → True ⊑ pvs E E (∃ γ, own (Δ:=Δ) i γ a).
+  ✓a → True ⊑ pvs E E (∃ γ, own i γ a).
 Proof.
-  intros Hm. set (P m := ∃ γ, m = to_globalC (Δ:=Δ) i γ a).
+  intros Hm. set (P m := ∃ γ, m = to_globalC i γ a).
   rewrite -(pvs_mono _ _ (∃ m, ■P m ∧ ownG m)%I).
   - rewrite -pvs_updateP_empty //; [].
     subst P. eapply (iprod_singleton_updateP_empty i).
-    + eapply map_updateP_alloc' with (x:=to_funC i a).
-      by rewrite /to_funC; destruct inG.
+    + eapply map_updateP_alloc' with (x:=to_Σ i a).
+      by rewrite /to_Σ; destruct inG.
     + simpl. move=>? [γ [-> ?]]. exists γ. done.
   - apply exist_elim=>m. apply const_elim_l.
     move=>[p ->] {P}. by rewrite -(exist_intro p).
diff --git a/program_logic/hoare_lifting.v b/program_logic/hoare_lifting.v
index 75cd71b80..b049cfb67 100644
--- a/program_logic/hoare_lifting.v
+++ b/program_logic/hoare_lifting.v
@@ -1,4 +1,5 @@
 Require Export program_logic.hoare program_logic.lifting.
+Require Import program_logic.ownership.
 Import uPred.
 
 Local Notation "{{ P } } ef ?@ E {{ Q } }" :=
diff --git a/program_logic/lifting.v b/program_logic/lifting.v
index 295115aa9..98426ec3d 100644
--- a/program_logic/lifting.v
+++ b/program_logic/lifting.v
@@ -1,5 +1,5 @@
 Require Export program_logic.weakestpre.
-Require Import program_logic.wsat.
+Require Import program_logic.wsat program_logic.ownership.
 Local Hint Extern 10 (_ ≤ _) => omega.
 Local Hint Extern 100 (@eq coPset _ _) => solve_elem_of.
 Local Hint Extern 10 (✓{_} _) =>
diff --git a/program_logic/namespace.v b/program_logic/namespace.v
index 76e8a34c0..2a98cc3ef 100644
--- a/program_logic/namespace.v
+++ b/program_logic/namespace.v
@@ -1,5 +1,6 @@
 Require Export algebra.base prelude.countable prelude.co_pset.
-Require Export program_logic.ownership program_logic.pviewshifts.
+Require Import program_logic.ownership.
+Require Export program_logic.pviewshifts.
 
 Definition namespace := list positive.
 Definition nnil : namespace := nil.
diff --git a/program_logic/pviewshifts.v b/program_logic/pviewshifts.v
index d9da27c12..b9728d643 100644
--- a/program_logic/pviewshifts.v
+++ b/program_logic/pviewshifts.v
@@ -1,5 +1,6 @@
-Require Export program_logic.ownership prelude.co_pset.
-Require Import program_logic.wsat.
+Require Export prelude.co_pset.
+Require Export program_logic.model.
+Require Import program_logic.ownership program_logic.wsat.
 Local Hint Extern 10 (_ ≤ _) => omega.
 Local Hint Extern 100 (@eq coPset _ _) => solve_elem_of.
 Local Hint Extern 100 (_ ∉ _) => solve_elem_of.
diff --git a/program_logic/viewshifts.v b/program_logic/viewshifts.v
index 019fc6a1b..812844f87 100644
--- a/program_logic/viewshifts.v
+++ b/program_logic/viewshifts.v
@@ -1,4 +1,5 @@
 Require Export program_logic.pviewshifts.
+Require Import program_logic.ownership.
 
 Definition vs {Λ Σ} (E1 E2 : coPset) (P Q : iProp Λ Σ) : iProp Λ Σ :=
   (□ (P → pvs E1 E2 Q))%I.
-- 
GitLab