From 48d0c51ae94fe94e1030c46bc591bc6f1d331a4d Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 15 Feb 2016 22:26:52 +0100
Subject: [PATCH] *finally* arrive at the weakening for STS state asswrtions
 that we need

Turns out it only holds as a view shift, not as an implication
---
 algebra/sts.v       | 25 +++++++++++++++++--------
 program_logic/sts.v | 19 ++++++++++++++++++-
 2 files changed, 35 insertions(+), 9 deletions(-)

diff --git a/algebra/sts.v b/algebra/sts.v
index 14f8af396..b2467582d 100644
--- a/algebra/sts.v
+++ b/algebra/sts.v
@@ -220,7 +220,7 @@ Canonical Structure stsRA := validityRA (sts R tok).
 Definition sts_auth (s : A) (T : set B) : stsRA := to_validity (auth s T).
 Definition sts_frag (S : set A) (T : set B) : stsRA := to_validity (frag S T).
 
-Lemma sts_update s1 s2 T1 T2 :
+Lemma sts_update_auth s1 s2 T1 T2 :
   sts.step R tok (s1,T1) (s2,T2) → sts_auth s1 T1 ~~> sts_auth s2 T2.
 Proof.
   intros ?; apply validity_update; inversion 3 as [|? S ? Tf|]; subst.
@@ -228,6 +228,15 @@ Proof.
   repeat (done || constructor).
 Qed.
 
+Lemma sts_update_frag S1 S2 (T : set B) :
+  S1 ⊆ S2 → sts.closed R tok S2 T →
+  sts_frag S1 T ~~> sts_frag S2 T.
+Proof.
+  move=>HS Hcl. eapply validity_update; inversion 3 as [|? S ? Tf|]; subst.
+  - split; first done. constructor; last done. solve_elem_of.
+  - split; first done. constructor; solve_elem_of.
+Qed.
+
 Lemma sts_frag_included S1 S2 T1 T2 :
   sts.closed R tok S2 T2 →
   sts_frag S1 T1 ≼ sts_frag S2 T2 ↔ 
@@ -235,20 +244,20 @@ Lemma sts_frag_included S1 S2 T1 T2 :
 Proof.
   move=>Hcl2. split.
   - intros [xf EQ]. destruct xf as [xf vf Hvf]. destruct xf as [Sf Tf|Sf Tf].
-    { exfalso. inversion_clear EQ. apply H0 in Hcl2. simpl in Hcl2.
+    { exfalso. inversion_clear EQ as [Hv EQ']. apply EQ' in Hcl2. simpl in Hcl2.
       inversion Hcl2. }
-    inversion_clear EQ.
-    move:(H0 Hcl2)=>{H0} H0. inversion_clear H0.
-    destruct H as [H _]. move:(H Hcl2)=>{H} [/= Hcl1  [Hclf Hdisj]].
+    inversion_clear EQ as [Hv EQ'].
+    move:(EQ' Hcl2)=>{EQ'} EQ. inversion_clear EQ as [|? ? ? ? HT HS].
+    destruct Hv as [Hv _]. move:(Hv Hcl2)=>{Hv} [/= Hcl1  [Hclf Hdisj]].
     apply Hvf in Hclf. simpl in Hclf. clear Hvf.
     inversion_clear Hdisj. split; last (exists Tf; split_ands); [done..|].
     apply (anti_symm (⊆)).
-    + move=>s HS2. apply elem_of_intersection. split; first by apply H2.
+    + move=>s HS2. apply elem_of_intersection. split; first by apply HS.
       by apply sts.subseteq_up_set.
-    + move=>s /elem_of_intersection [HS1 Hscl]. apply H2. split; first done.
+    + move=>s /elem_of_intersection [HS1 Hscl]. apply HS. split; first done.
       destruct Hscl as [s' [Hsup Hs']].
       eapply sts.closed_steps; last (hnf in Hsup; eexact Hsup); first done.
-      solve_elem_of +H2 Hs'.
+      solve_elem_of +HS Hs'.
   - intros (Hcl1 & Tf & Htk & Hf & Hs). exists (sts_frag (sts.up_set R tok S2 Tf) Tf).
     split; first split; simpl;[|done|].
     + intros _. split_ands; first done.
diff --git a/program_logic/sts.v b/program_logic/sts.v
index a6264d277..6c9f24b7c 100644
--- a/program_logic/sts.v
+++ b/program_logic/sts.v
@@ -45,6 +45,23 @@ Section sts.
   Implicit Types P Q R : iPropG Λ Σ.
   Implicit Types γ : gname.
 
+  (* The same rule as implication does *not* hold, as could be shown using
+     sts_frag_included. *)
+  Lemma states_weaken E γ S1 S2 T :
+    S1 ⊆ S2 → closed sts.(st) sts.(tok) S2 T →
+    states StsI sts γ S1 T ⊑ pvs E E (states StsI sts γ S2 T).
+  Proof.
+    rewrite /states=>Hs Hcl. apply own_update, sts_update_frag; done.
+  Qed.
+
+  Lemma state_states E γ s S T :
+    s ∈ S → closed sts.(st) sts.(tok) S T →
+    state StsI sts γ s T ⊑ pvs E E (states StsI sts γ S T).
+  Proof.
+    move=>Hs Hcl. apply states_weaken; last done.
+    move=>s' Hup. eapply closed_steps in Hcl; last (hnf in Hup; eexact Hup); done.
+  Qed.
+
   Lemma alloc N s :
     φ s ⊑ pvs N N (∃ γ, ctx StsI sts γ N φ ∧ state StsI sts γ s (set_all ∖ sts.(tok) s)).
   Proof.
@@ -98,7 +115,7 @@ Section sts.
     rewrite -later_intro.
     rewrite own_valid_l discrete_validI. apply const_elim_sep_l=>Hval. simpl in Hval.
     transitivity (pvs E E (own StsI γ (sts_auth sts.(st) sts.(tok) s' T'))).
-    { by apply own_update, sts_update. }
+    { by apply own_update, sts_update_auth. }
     apply pvs_mono. rewrite -own_op. apply equiv_spec, own_proper.
     split; first split; simpl.
     - intros _.
-- 
GitLab