Commit 8826f27c authored by Shabnam Ghasemirad's avatar Shabnam Ghasemirad

iTok removed

parent a8d7b804
......@@ -3,7 +3,7 @@ From iris.base_logic.lib Require Import invariants.
From iris.heap_lang Require Import lib.par proofmode notation lang.
Section Excl_cam.
Definition my_camera := (authR (optionUR (exclR (prodO (listO (prodO (prodO locO ZO) gnameO)) gnameO)))).
Definition my_camera := (authR (optionUR (exclR (listO (prodO locO ZO))))).
Context `{!heapG Σ, !spawnG Σ, !inG Σ my_camera}.
Lemma ghost_var_alloc n :
......
......@@ -38,12 +38,19 @@ Proof.
subst. by rewrite app_nil_r.
Qed.
Inductive lpT (A: Type) :=
| ListBot : lpT A
| ListSome : list A lpT A.
Arguments ListBot {_}.
Arguments ListSome {_}.
Instance: Params (@ListBot) 1 := {}.
Instance: Params (@ListSome) 1 := {}.
Section ListMaster.
Context {A: Type} `{EqDecision A} {EquivA : Equiv A} `{@Equivalence A EquivA} `{@LeibnizEquiv A EquivA}.
Context {A: ofeT} `{@LeibnizEquiv A ()} `{EqDecision A}.
Inductive lpT :=
| ListBot : lpT
| ListSome : list A lpT.
Notation lpT := (lpT A).
Inductive lpT_equiv : Equiv lpT :=
| ListSome_equiv l l' : l l' ListSome l ListSome l'
......@@ -55,9 +62,9 @@ Section ListMaster.
split; intros l.
- destruct l; constructor. reflexivity.
- intros y H1. destruct l, y; try done; try inversion H1.
induction H1; [|constructor]. constructor. subst. rewrite H1. reflexivity.
induction H1; [|constructor]. constructor. by simplify_eq.
- intros y z Hly Hyz. destruct l, y, z; try done; try constructor;
try inversion Hly; try inversion Hyz. subst. rewrite H3. auto.
try inversion Hly; try inversion Hyz. subst. by simplify_eq.
Qed.
Canonical Structure lpO := discreteO lpT.
......@@ -81,24 +88,24 @@ Section ListMaster.
Proof.
split.
- unfold Proper, "==>". intros.
destruct x0, y; try done; try inversion H1. simplify_eq. done.
- intros. exists cx. split; [|done]. rewrite <- H2.
destruct x, y; try done; try inversion H1. simplify_eq. done.
destruct x0, y; try done; try inversion H0; simplify_eq. done.
- intros. exists cx. split; [|done]. rewrite <- H1.
destruct x, y; try done; try inversion H0. simplify_eq. done.
- unfold Proper, "==>", impl. intros.
destruct x, y; try done; try inversion H2; try inversion H1.
destruct x, y; try done; try inversion H1; try inversion H0.
- unfold Assoc. intros. destruct x, y, z; try done.
assert (ListSome l0 ListBot = ListBot). done.
destruct (ListSome l ListSome l0); rewrite H1; try done.
destruct (ListSome l ListSome l0); rewrite H0; try done.
unfold "⋅", lp_op. admit.
- unfold Comm. intros. destruct x, y; try done.
unfold "⋅", lp_op. destruct (decide (l `prefix_of` l0));
destruct (decide (l0 `prefix_of` l)); try done.
apply (both_prefix_eq l l0) in p. subst. done. done.
- intros. destruct x. done. destruct cx; inversion H1.
- intros. destruct x. done. destruct cx; inversion H0.
unfold "⋅", lp_op. destruct (decide (l0 `prefix_of` l0)); try done.
- intros. destruct x. inversion H1. inversion H1. done.
- intros. destruct x eqn:E, y; inversion H2. admit. admit.
- intros. destruct x, y; try inversion H1; try done.
- intros. destruct x. simplify_eq. inversion H0. done.
- intros. destruct x eqn:E, y; inversion H1. admit. admit.
- intros. destruct x, y; try inversion H0; try done.
Admitted.
Canonical Structure lpR := discreteR lpT lp_ra_mixin.
......@@ -148,15 +155,15 @@ Section ListMaster.
End ListMaster.
Section lp_auth.
Context (A: Type) `{EqDecision A} {EquivA : Equiv A} `{@Equivalence A EquivA} `{@LeibnizEquiv A EquivA}
`{inG Σ (authR (@lpUR A _ _ _ _))}.
Context (A: ofeT) `{EqDecision A} `{@LeibnizEquiv A ()}
`{inG Σ (authR (@lpUR A _ _))}.
Lemma ghost_var_lp_alloc (V: list A):
(|==> γ, own γ ( (ListSome V)))%I.
(|==> γ, own γ ( (ListSome V : lpUR)))%I.
Proof.
iMod (own_alloc ( (ListSome V) (ListSome V))) as (γ) "[??]".
- by apply auth_both_valid.
- by eauto with iFrame.
- iModIntro. iExists _. by iFrame.
Qed.
Lemma own_lat_auth_update γ (V V': list A) (Ext: V `prefix_of` V'):
......@@ -166,14 +173,18 @@ Section lp_auth.
by apply own_update, auth_update, lp_local_unit_update.
Qed.
Lemma own_lat_auth_update_fork γ (V: list A):
own γ ( (ListSome V)) == own γ ( (ListSome V)) own γ ( (ListSome V)).
Proof. by apply own_lat_auth_update. Qed.
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.
Lemma own_lat_auth_max γ (V1 V2: list A) :
own γ ( (ListSome V1)) own γ ( (ListSome V2)) V2 `prefix_of` V1.
Lemma own_lat_auth_max γ (V1 V2: list A) q :
own γ ({q} (ListSome V1)) own γ ( (ListSome V2)) V2 `prefix_of` V1.
Proof.
rewrite -own_op own_valid uPred.discrete_valid auth_both_valid lp_included.
by apply bi.pure_mono=>-[? _].
rewrite -own_op own_valid uPred.discrete_valid auth_both_frac_valid lp_included.
by iIntros "[? [$ ?]]".
Qed.
End lp_auth.
\ No newline at end of file
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