Commit e11f52aa authored by Ralf Jung's avatar Ralf Jung

show that owning a ghost-unit can be boxed

parent 1f918268
...@@ -950,6 +950,16 @@ Module Type IRIS_CORE (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORL ...@@ -950,6 +950,16 @@ Module Type IRIS_CORE (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORL
rewrite ->Hg1, Hg2. apply pordR. exact Heq. rewrite ->Hg1, Hg2. apply pordR. exact Heq.
Qed. Qed.
Lemma ownL_box (g: RL.res) :
ownL (1 g) == ownL (1 g).
Proof.
apply pord_antisym; last exact:box_elim.
move=>w n. destruct n; first (intro; exact:bpred).
case=>[gr Heq]. simpl. destruct (ra_unit_mono (1 g) gr) as [g' Heq'].
simpl in Heq. rewrite -Heq. exists g'.
rewrite (comm gr) Heq' ra_unit_idem comm. reflexivity.
Qed.
Lemma ownL_something: Lemma ownL_something:
valid(xist ownL). valid(xist ownL).
Proof. Proof.
......
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