From 8c22bd60f52e6ddd7eca936ce2857272184ca0c8 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 15 Feb 2016 18:57:38 +0100
Subject: [PATCH] establish monotnicity of ownership

---
 algebra/upred.v                 | 2 ++
 program_logic/auth.v            | 2 +-
 program_logic/ghost_ownership.v | 2 ++
 program_logic/ownership.v       | 3 +++
 4 files changed, 8 insertions(+), 1 deletion(-)

diff --git a/algebra/upred.v b/algebra/upred.v
index 465cfb505..a3ceb502a 100644
--- a/algebra/upred.v
+++ b/algebra/upred.v
@@ -846,6 +846,8 @@ Proof. done. Qed.
 (* Own and valid derived *)
 Lemma ownM_invalid (a : M) : ¬ ✓{0} a → uPred_ownM a ⊑ False.
 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 *)
 Lemma timelessP_spec P : TimelessP P ↔ ∀ x n, ✓{n} x → P 0 x → P n x.
diff --git a/program_logic/auth.v b/program_logic/auth.v
index 6d48f1294..4e94acc1c 100644
--- a/program_logic/auth.v
+++ b/program_logic/auth.v
@@ -116,7 +116,7 @@ Section auth.
     (* Getting this wand eliminated is really annoying. *)
     rewrite [(■_ ★ _)%I]comm -!assoc [(▷φ _ ★ _ ★ _)%I]assoc [(▷φ _ ★ _)%I]comm.
     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=> Lv.
     rewrite sep_exist_l; apply exist_elim=> ?.
diff --git a/program_logic/ghost_ownership.v b/program_logic/ghost_ownership.v
index c6fd4ff22..b5b8cedc6 100644
--- a/program_logic/ghost_ownership.v
+++ b/program_logic/ghost_ownership.v
@@ -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.
 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).
 Proof. by rewrite /own -to_globalF_unit always_ownG_unit. Qed.
 Lemma own_valid γ a : own i γ a ⊑ ✓ a.
diff --git a/program_logic/ownership.v b/program_logic/ownership.v
index 913b0db5b..7327ff100 100644
--- a/program_logic/ownership.v
+++ b/program_logic/ownership.v
@@ -50,6 +50,8 @@ Proof. by intros m m' Hm; unfold ownG; rewrite Hm. Qed.
 Global Instance ownG_proper : Proper ((≡) ==> (≡)) (@ownG Λ Σ) := ne_proper _.
 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.
+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).
 Proof.
   apply uPred.always_ownM.
@@ -64,6 +66,7 @@ Proof. apply (uPred.always_entails_r _ _), ownG_valid. Qed.
 Global Instance ownG_timeless m : Timeless m → TimelessP (ownG m).
 Proof. rewrite /ownG; apply _. Qed.
 
+
 (* inversion lemmas *)
 Lemma ownI_spec r n i P :
   ✓{n} r →
-- 
GitLab