Commit 033b99da authored by Shabnam Ghasemirad's avatar Shabnam Ghasemirad

invariant changed. splited to link_inv and value_inv. tryDeq reproved. tryEnq nil case proved.

parent f1d05839
......@@ -211,10 +211,10 @@ Section lp_auth.
Qed.
Lemma own_lat_auth_frac_agree γ (V1 V2: list A) p q :
own γ ({q} (ListSome V1) {p} (ListSome V2)) V1 V2.
intros. assert (({q} ListSome V1 {p} ListSome V2)).
{ admit. }
apply auth_auth_frac_op_inv in H2. by inversion H2.
Admitted.
own γ ({q} (ListSome V1) {p} (ListSome V2)) V2 = V1.
Proof.
rewrite own_valid. iIntros "H". iDestruct "H" as %E%auth_auth_frac_op_inv.
inversion E. by simplify_eq.
Qed.
End lp_auth.
\ No newline at end of file
This diff is collapsed.
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