Commit 48d0c51a authored by Ralf Jung's avatar Ralf Jung

*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
parent ff508ad9
......@@ -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.
intros ?; apply validity_update; inversion 3 as [|? S ? Tf|]; subst.
......@@ -228,6 +228,15 @@ Proof.
repeat (done || constructor).
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.
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.
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 :
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.
......@@ -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).
rewrite /states=>Hs Hcl. apply own_update, sts_update_frag; done.
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).
move=>Hs Hcl. apply states_weaken; last done.
move=>s' Hup. eapply closed_steps in Hcl; last (hnf in Hup; eexact Hup); done.
Lemma alloc N s :
φ s pvs N N ( γ, ctx StsI sts γ N φ state StsI sts γ s (set_all sts.(tok) s)).
......@@ -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 _.
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