Commit 8c22bd60 authored by Ralf Jung's avatar Ralf Jung

establish monotnicity of ownership

parent b761292e
...@@ -846,6 +846,8 @@ Proof. done. Qed. ...@@ -846,6 +846,8 @@ Proof. done. Qed.
(* Own and valid derived *) (* Own and valid derived *)
Lemma ownM_invalid (a : M) : ¬ {0} a uPred_ownM a False. Lemma ownM_invalid (a : M) : ¬ {0} a uPred_ownM a False.
Proof. by intros; rewrite ownM_valid valid_elim. Qed. Proof. by intros; rewrite ownM_valid valid_elim. Qed.
Global Instance ownM_mono : Proper (flip () ==> ()) (@uPred_ownM M).
Proof. move=>a b [c H]. rewrite H ownM_op. eauto. Qed.
(* Timeless *) (* Timeless *)
Lemma timelessP_spec P : TimelessP P x n, {n} x P 0 x P n x. Lemma timelessP_spec P : TimelessP P x n, {n} x P 0 x P n x.
......
...@@ -116,7 +116,7 @@ Section auth. ...@@ -116,7 +116,7 @@ Section auth.
(* Getting this wand eliminated is really annoying. *) (* Getting this wand eliminated is really annoying. *)
rewrite [(_ _)%I]comm -!assoc [(▷φ _ _ _)%I]assoc [(▷φ _ _)%I]comm. rewrite [(_ _)%I]comm -!assoc [(▷φ _ _ _)%I]assoc [(▷φ _ _)%I]comm.
rewrite wand_elim_r fsa_frame_l. rewrite wand_elim_r fsa_frame_l.
apply (fsa_mono_pvs fsa)=> v. apply (fsa_mono_pvs fsa)=> x.
rewrite sep_exist_l; apply exist_elim=> L. rewrite sep_exist_l; apply exist_elim=> L.
rewrite sep_exist_l; apply exist_elim=> Lv. rewrite sep_exist_l; apply exist_elim=> Lv.
rewrite sep_exist_l; apply exist_elim=> ?. rewrite sep_exist_l; apply exist_elim=> ?.
......
...@@ -66,6 +66,8 @@ Global Instance own_proper γ : Proper ((≡) ==> (≡)) (own i γ) := ne_proper ...@@ -66,6 +66,8 @@ Global Instance own_proper γ : Proper ((≡) ==> (≡)) (own i γ) := ne_proper
Lemma own_op γ a1 a2 : own i γ (a1 a2) (own i γ a1 own i γ a2)%I. Lemma own_op γ a1 a2 : own i γ (a1 a2) (own i γ a1 own i γ a2)%I.
Proof. by rewrite /own -ownG_op to_globalF_op. Qed. Proof. by rewrite /own -ownG_op to_globalF_op. Qed.
Global Instance own_mono γ : Proper (flip () ==> ()) (own i γ).
Proof. move=>a b [c H]. rewrite H own_op. eauto with I. Qed.
Lemma always_own_unit γ a : ( own i γ (unit a))%I own i γ (unit a). Lemma always_own_unit γ a : ( own i γ (unit a))%I own i γ (unit a).
Proof. by rewrite /own -to_globalF_unit always_ownG_unit. Qed. Proof. by rewrite /own -to_globalF_unit always_ownG_unit. Qed.
Lemma own_valid γ a : own i γ a a. Lemma own_valid γ a : own i γ a a.
......
...@@ -50,6 +50,8 @@ Proof. by intros m m' Hm; unfold ownG; rewrite Hm. Qed. ...@@ -50,6 +50,8 @@ Proof. by intros m m' Hm; unfold ownG; rewrite Hm. Qed.
Global Instance ownG_proper : Proper (() ==> ()) (@ownG Λ Σ) := ne_proper _. Global Instance ownG_proper : Proper (() ==> ()) (@ownG Λ Σ) := ne_proper _.
Lemma ownG_op m1 m2 : ownG (m1 m2) (ownG m1 ownG m2)%I. Lemma ownG_op m1 m2 : ownG (m1 m2) (ownG m1 ownG m2)%I.
Proof. by rewrite /ownG -uPred.ownM_op Res_op !left_id. Qed. Proof. by rewrite /ownG -uPred.ownM_op Res_op !left_id. Qed.
Global Instance ownG_mono : Proper (flip () ==> ()) (@ownG Λ Σ).
Proof. move=>a b [c H]. rewrite H ownG_op. eauto with I. Qed.
Lemma always_ownG_unit m : ( ownG (unit m))%I ownG (unit m). Lemma always_ownG_unit m : ( ownG (unit m))%I ownG (unit m).
Proof. Proof.
apply uPred.always_ownM. apply uPred.always_ownM.
...@@ -64,6 +66,7 @@ Proof. apply (uPred.always_entails_r _ _), ownG_valid. Qed. ...@@ -64,6 +66,7 @@ Proof. apply (uPred.always_entails_r _ _), ownG_valid. Qed.
Global Instance ownG_timeless m : Timeless m TimelessP (ownG m). Global Instance ownG_timeless m : Timeless m TimelessP (ownG m).
Proof. rewrite /ownG; apply _. Qed. Proof. rewrite /ownG; apply _. Qed.
(* inversion lemmas *) (* inversion lemmas *)
Lemma ownI_spec r n i P : Lemma ownI_spec r n i P :
{n} r {n} r
......
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