From b00233e45d626a4fc79320a25afc2f133f6f603b Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 17 Feb 2016 12:54:20 +0100
Subject: [PATCH] sts_ownS_op: fix stupid typo

---
 algebra/sts.v       |  2 +-
 program_logic/sts.v | 19 ++++++++++---------
 2 files changed, 11 insertions(+), 10 deletions(-)

diff --git a/algebra/sts.v b/algebra/sts.v
index a28c5e202..d88da5b16 100644
--- a/algebra/sts.v
+++ b/algebra/sts.v
@@ -333,7 +333,7 @@ Lemma sts_op_auth_frag_up s T :
 Proof. intros; apply sts_op_auth_frag; auto using elem_of_up, closed_up. Qed.
 
 Lemma sts_op_frag S1 S2 T1 T2 :
-  T1 ∪ T2 ⊆ ∅ → sts.closed S1 T1 → sts.closed S2 T2 →
+  T1 ∩ T2 ⊆ ∅ → sts.closed S1 T1 → sts.closed S2 T2 →
   sts_frag (S1 ∩ S2) (T1 ∪ T2) ≡ sts_frag S1 T1 ⋅ sts_frag S2 T2.
 Proof.
   intros HT HS1 HS2. rewrite /sts_frag.
diff --git a/program_logic/sts.v b/program_logic/sts.v
index 1a7b45ed1..6dab4f8bb 100644
--- a/program_logic/sts.v
+++ b/program_logic/sts.v
@@ -53,18 +53,19 @@ Section sts.
 
   (* The same rule as implication does *not* hold, as could be shown using
      sts_frag_included. *)
-  Lemma sts_ownS_weaken E γ S1 S2 T :
-    S1 ⊆ S2 → sts.closed S2 T →
-    sts_ownS γ S1 T ⊑ pvs E E (sts_ownS γ S2 T).
-  Proof. intros. by apply own_update, sts_update_frag. Qed.
+  Lemma sts_ownS_weaken E γ S1 S2 T1 T2 :
+    T1 ≡ T2 → S1 ⊆ S2 → sts.closed S2 T2 →
+    sts_ownS γ S1 T1 ⊑ pvs E E (sts_ownS γ S2 T2).
+  Proof. intros -> ? ?. by apply own_update, sts_update_frag. Qed.
 
-  Lemma sts_own_weaken E γ s S T :
-    s ∈ S → sts.closed S T →
-    sts_own γ s T ⊑ pvs E E (sts_ownS γ S T).
-  Proof. intros. by apply own_update, sts_update_frag_up. Qed.
+  Lemma sts_own_weaken E γ s S T1 T2 :
+    T1 ≡ T2 → s ∈ S → sts.closed S T2 →
+    sts_own γ s T1 ⊑ pvs E E (sts_ownS γ S T2).
+  (* FIXME for some reason, using "->" instead of "<-" does not work? *)
+  Proof. intros <- ? ?. by apply own_update, sts_update_frag_up. Qed.
 
   Lemma sts_ownS_op γ S1 S2 T1 T2 :
-    T1 ∪ T2 ⊆ ∅ → sts.closed S1 T1 → sts.closed S2 T2 →
+    T1 ∩ T2 ⊆ ∅ → sts.closed S1 T1 → sts.closed S2 T2 →
     sts_ownS γ (S1 ∩ S2) (T1 ∪ T2) ≡ (sts_ownS γ S1 T1 ★ sts_ownS γ S2 T2)%I.
   Proof. intros. by rewrite /sts_ownS -own_op sts_op_frag. Qed.
 
-- 
GitLab