Commit d3a14f04 authored by Shabnam Ghasemirad's avatar Shabnam Ghasemirad

Tuple stores eliminated. TODO: prove fractional auth agreement for master...

Tuple stores eliminated. TODO: prove fractional auth agreement for master camera and fixing invariant for 1 element case.
parent 8826f27c
......@@ -27,6 +27,16 @@ Proof.
by exists x.
Qed.
Lemma non_nil_prefix : (A : Type) (a : A) (l l' : list A),
(a :: l) `prefix_of` l' l'', l' = a :: l'' l `prefix_of` l''.
Proof.
intros A a l l' Hpre. inversion Hpre.
replace (a :: l) with ([a] ++ l) in H by done.
rewrite <- app_assoc in H. exists (l ++ x).
replace ([a] ++ l ++ x) with (a :: l ++ x) in H by done.
split. assumption. exists x. done.
Qed.
Instance prefix_PO {A: Type}: PartialOrder (@prefix A).
Proof.
split; [apply _|].
......@@ -176,10 +186,22 @@ Section lp_auth.
Lemma own_lat_auth_update_fork γ (V: list A) q:
own γ ({q} (ListSome V)) == own γ ({q} (ListSome V)) own γ ( (ListSome V)).
Proof.
rewrite -own_op. apply own_update.
rewrite -auth_both_frac_op. apply cmra_total_update.
move => n [[[??]|]?] //= [/= ? ?].
Admitted.
rewrite -own_op. apply own_update, cmra_total_update.
move=> n [[[? a1]|] bf1] [/= VL [a0 [Eq [[bf2 Ha] VL2]]]]; do 2 red; simpl in *.
- split; [done|].
exists a0. split; last split; [done| |done].
rewrite left_id. apply discrete_iff in Eq; [|apply _].
have Eq1: to_agree (ListSome V) a1.
{ apply agree_op_inv. by rewrite Eq. }
move : Eq. rewrite -Eq1 agree_idemp. intros Eq%to_agree_inj. rewrite Eq.
rewrite (_: a0 bf1 a0) //.
apply lp_absorb. rewrite Ha left_id. apply : cmra_included_l.
- split; [done|]. apply to_agree_injN in Eq.
move: Ha; rewrite !left_id => Ha.
exists a0. rewrite Eq. split; last split; [done| |done].
rewrite left_id (_: a0 bf1 a0) //.
apply lp_absorb. rewrite Ha. apply : cmra_included_l.
Qed.
Lemma own_lat_auth_max γ (V1 V2: list A) q :
own γ ({q} (ListSome V1)) own γ ( (ListSome V2)) V2 `prefix_of` V1.
......@@ -187,4 +209,12 @@ Section lp_auth.
rewrite -own_op own_valid uPred.discrete_valid auth_both_frac_valid lp_included.
by iIntros "[? [$ ?]]".
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.
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