Skip to content
Snippets Groups Projects
Commit 4e11257b authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Shorten sts_ownS_op. 

Do not use proper explicitly but let setoids handle it.
parent e1589fea
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 1 addition and 4 deletions
program_logic/sts.v
+ 1
− 4
View file @ 4e11257b
...@@ -66,10 +66,7 @@ Section sts. ...@@ -66,10 +66,7 @@ Section sts.
Lemma sts_ownS_op γ S1 S2 T1 T2 : 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. sts_ownS γ (S1 ∩ S2) (T1 ∪ T2) ≡ (sts_ownS γ S1 T1 ★ sts_ownS γ S2 T2)%I.
Proof. Proof. intros. by rewrite /sts_ownS -own_op sts_op_frag. Qed.
intros HT HS1 HS2. rewrite /sts_ownS -own_op.
by apply own_proper, sts_op_frag.
Qed.
Lemma sts_alloc E N s : Lemma sts_alloc E N s :
nclose N ⊆ E → nclose N ⊆ E →
......
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