Commit 7ca7ad53 authored by Ralf Jung's avatar Ralf Jung

Do not export ownership

Actual proofs will end up using own and inv, and none of the notions defined in ownership.v
parent fe5a098d
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).
......
(** 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.
......
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 ({_} _) =>
......
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).
......
Require Export program_logic.hoare program_logic.lifting.
Require Import program_logic.ownership.
Import uPred.
Local Notation "{{ P } } ef ?@ E {{ Q } }" :=
......
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 ({_} _) =>
......
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.
......
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.
......
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.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment