Commit b00233e4 authored by Ralf Jung's avatar Ralf Jung
Browse files

sts_ownS_op: fix stupid typo

parent fa9570a8
...@@ -333,7 +333,7 @@ Lemma sts_op_auth_frag_up s T : ...@@ -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. Proof. intros; apply sts_op_auth_frag; auto using elem_of_up, closed_up. Qed.
Lemma sts_op_frag S1 S2 T1 T2 : 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. sts_frag (S1 S2) (T1 T2) sts_frag S1 T1 sts_frag S2 T2.
Proof. Proof.
intros HT HS1 HS2. rewrite /sts_frag. intros HT HS1 HS2. rewrite /sts_frag.
......
...@@ -53,18 +53,19 @@ Section sts. ...@@ -53,18 +53,19 @@ Section sts.
(* The same rule as implication does *not* hold, as could be shown using (* The same rule as implication does *not* hold, as could be shown using
sts_frag_included. *) sts_frag_included. *)
Lemma sts_ownS_weaken E γ S1 S2 T : Lemma sts_ownS_weaken E γ S1 S2 T1 T2 :
S1 S2 sts.closed S2 T T1 T2 S1 S2 sts.closed S2 T2
sts_ownS γ S1 T pvs E E (sts_ownS γ S2 T). sts_ownS γ S1 T1 pvs E E (sts_ownS γ S2 T2).
Proof. intros. by apply own_update, sts_update_frag. Qed. Proof. intros -> ? ?. by apply own_update, sts_update_frag. Qed.
Lemma sts_own_weaken E γ s S T : Lemma sts_own_weaken E γ s S T1 T2 :
s S sts.closed S T T1 T2 s S sts.closed S T2
sts_own γ s T pvs E E (sts_ownS γ S T). sts_own γ s T1 pvs E E (sts_ownS γ S T2).
Proof. intros. by apply own_update, sts_update_frag_up. Qed. (* 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 : 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. intros. by rewrite /sts_ownS -own_op sts_op_frag. Qed. Proof. intros. by rewrite /sts_ownS -own_op sts_op_frag. Qed.
......
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