Commit 1e938dbf authored by Jonas Kastberg Hinrichsen's avatar Jonas Kastberg Hinrichsen
Browse files

gen_proc proven - deprecations remaining

parent 9ff91ebf
Pipeline #9882 canceled with stages
......@@ -215,6 +215,8 @@ Lemma auth_both_op a b : Auth (Excl' a) b ≡ ● a ⋅ ◯ b.
Proof. by rewrite /op /auth_op /= left_id. Qed.
Lemma auth_auth_valid a : a ( a).
Proof. intros; split; simpl; auto using ucmra_unit_leastN. Qed.
Lemma auth_frag_valid a : a ( a).
Proof. intros; auto using ucmra_unit_leastN. Qed.
Lemma auth_update a b a' b' :
(a,b) ~l~> (a',b') a b ~~> a' b'.
......@@ -231,6 +233,9 @@ Proof. intros. rewrite -(right_id _ _ (● a)). by apply auth_update. Qed.
Lemma auth_update_dealloc a b a' : (a,b) ~l~> (a',ε) a b ~~> a'.
Proof. intros. rewrite -(right_id _ _ ( a')). by apply auth_update. Qed.
Lemma auth_alloc_unit a : a ~~> a ε.
Proof. intros. (* rewrite -(right_id _ _ (● a)). *) by apply auth_update_alloc. Qed.
Lemma auth_local_update (a b0 b1 a' b0' b1': A) :
(b0, b1) ~l~> (b0', b1') b0' a' a'
( a b0, a b1) ~l~> ( a' b0', a' b1').
......
......@@ -417,7 +417,8 @@ Proof.
intros Hi1 Hi2 Hup; apply local_update_unital=> n mf Hmv Hm; simpl in *.
destruct (Hup n (mf !! i)) as [? Hx']; simpl in *.
{ move: (Hmv i). by rewrite Hi1. }
{ move: (Hm i). by rewrite lookup_op Hi1 Hi2 Some_op_opM (inj_iff Some). }
{ move: (Hm i). rewrite lookup_op Hi1 Hi2. rewrite Some_op_opM (inj_iff Some). eauto.
(* by rewrite lookup_op Hi1 Hi2 Some_op_opM (inj_iff Some). *) }
split; auto using insert_validN.
rewrite Hm Hx'=> j; destruct (decide (i = j)) as [->|].
- by rewrite lookup_insert lookup_op lookup_insert Some_op_opM.
......@@ -471,8 +472,144 @@ Proof.
apply (delete_local_update_cancelable m _ i (Some x));
[done|by rewrite lookup_singleton].
Qed.
End properties.
Section unital_properties.
Context `{Countable K} {A : ucmraT}.
Implicit Types m : gmap K A.
Implicit Types i : K.
Implicit Types x y : A.
Lemma insert_idN (n:nat) (m : gmap K A) (i:K) (x:A) :
m !! i {n} Some x <[ i := x ]>m {n} m.
Proof.
intros H0. apply dist_Some_inv_r' in H0. destruct H0. destruct H0. rewrite H1.
by rewrite insert_id => //.
Qed.
Lemma insert_opN (m1 : gmap K A) (m2 : gmap K A) (i:K) (x:A) (y:A) :
<[ i := x y ]>(m1 m2) = <[ i := x ]>m1 <[ i := y ]>m2 .
Proof. by rewrite (insert_merge () m1 m2 i (x y) x y). Qed.
Lemma insert_alloc_local_update (m1 :gmap K A) (m2 : gmap K A) (i:K) (x:A) (x':A) (y':A) :
m1 !! i = Some x m2 !! i = None
(x, ε) ~l~> (x', y')
(m1, m2) ~l~> (<[i:=x']>m1, <[i:=y']>m2).
Proof.
intros Hi1 Hi2 Hup.
apply local_update_unital=> n mf Hmv Hm.
assert (dist n (mf !! i) (Some x)) as Hif.
{ move: (Hm i). rewrite lookup_op. rewrite Hi1 Hi2. by rewrite left_id. }
destruct (Hup n (mf !! i)) as [? Hx'].
{ move: (Hmv i). by rewrite Hi1. }
{ simpl. rewrite Hif. rewrite -(inj_iff Some). rewrite -Some_op_opM. rewrite -Some_op. by rewrite left_id. }
simpl in *.
assert ( (y' x) {n} (x') ).
{ rewrite Hx'. by rewrite Hif. }
assert ( (m2 mf) {n} (m1) ).
{ by rewrite Hm. }
split; auto using insert_validN.
rewrite Hm Hx' => j; destruct (decide (i = j)) as [->|].
- rewrite lookup_insert. rewrite Hif. rewrite -Some_op_opM. rewrite -Some_op.
rewrite H1. apply H0.
- rewrite lookup_insert_ne //.
rewrite H2. apply Hmv.
- rewrite -(insert_idN n mf i x) =>//.
rewrite -insert_opN.
rewrite -Hm.
by rewrite H1.
Qed.
End unital_properties.
Section nested_gmap_properties.
Context `{Countable K} {A : cmraT}.
Implicit Types m : gmap K (gmap K A).
Implicit Types p i : K.
Implicit Types x y : gmap K A.
Implicit Types v : A.
Definition insert2 m p i v :=
match m !! p with
| None => <[p := {[ i := v ]}]>m
| Some(m') => <[p:= <[ i := v ]>m']>m
end.
Definition delete2 `{Countable K} {A : Type} (p i:K) (m: gmap K (gmap K A)) :=
match (m !! p) with
| None => m
| Some(m') => <[p := delete i m']>m
end.
Lemma delete_something_update m1 m2 p i x y :
m1 !! p = Some x
m2 !! p = Some y
(x, y) ~l~> (delete i x, )
(m1, m2) ~l~> (delete2 p i m1, <[ p := ]>m2).
Proof.
intros.
unfold delete2.
rewrite H0.
apply insert_local_update with x y => //.
Qed.
(* Lemma delete_something_update m1 m2 p i v : *)
(* m2 !! p = Some {[ i := v ]} → *)
(* (m1, m2) ~l~> (delete2 p i m1, <[ p := ∅ ]>m2 ). *)
(* Proof. *)
(* intros. *)
(* apply local_update_unital=> n mf Hmv Hm. *)
(* assert (m1 !! p ≡{n}≡ Some {[ i := v ]} ) by admit. *)
(* split. *)
(* - admit. *)
(* - unfold delete2. *)
(* destruct (m1 !! p). *)
(* inversion H1. *)
(* rewrite H4. *)
(* rewrite delete_insert. *)
(* rewrite Hm. *)
(* SearchAbout op. *)
(* rewrite -insert_opN. *)
(* rewrite -(insert_idN). *)
(* eapply insert_local_update. *)
(* Lemma delete_something_update m1 m2 p i x y: *)
(* m1 !! p = Some x → *)
(* m2 !! p = Some y → *)
(* (x, y) ~l~> (delete i x, ∅) → *)
(* (m1, m2) ~l~> (delete2 p i m1, <[ p := ∅ ]>m2 ). *)
(* Proof. *)
(* intros. *)
(* apply local_update_unital=> n mf Hmv Hm. *)
(* assert (m !! p ≡{n}≡ Some {[ i := x ]} ) by admit. *)
(* split. *)
(* - unfold delete2. *)
(* destruct (m !! p). inversion H0. rewrite H3. apply insert_validN =>//. rewrite delete_insert => //. apply Hmv. *)
(* - rewrite left_id. *)
(* assert (m !! p ≡{n}≡ Some {[ i := x ]} ) by admit. *)
(* assert (mf !! p ≡{n}≡ None \/ (∃ mf', mf !! p ≡{n}≡ Some (mf') /\ mf !! i ≡{n}≡ None)) by admit. *)
(* split. *)
(* - unfold delete2. *)
(* destruct (m !! p). inversion H0. rewrite H4. apply insert_validN =>//. rewrite delete_insert => //. apply Hmv. *)
(* - unfold delete2. *)
(* destruct (m !! p). *)
(* inversion H0. *)
(* rewrite H4. *)
(* rewrite left_id. *)
(* rewrite Hm. *)
(* destruct H1. *)
(* + subst. rewrite -insert_singleton_op => //. *)
(* apply delete_notin. *)
(* rewrite -insert_opN. *)
(* Admitted. *)
End nested_gmap_properties.
Print delete_something_update.
(** Functor *)
Instance gmap_fmap_ne `{Countable K} {A B : ofeT} (f : A B) n :
Proper (dist n ==> dist n) f Proper (dist n ==>dist n) (fmap (M:=gmap K) f).
......
......@@ -57,6 +57,8 @@ Section to_gen_heap.
Proof. intros l. rewrite lookup_fmap. by case (σ !! l). Qed.
Lemma lookup_to_gen_heap_None σ l : σ !! l = None to_gen_heap σ !! l = None.
Proof. by rewrite /to_gen_heap lookup_fmap=> ->. Qed.
Lemma lookup_to_gen_heap_Some σ l v : σ !! l = Some v to_gen_heap σ !! l = Some (1%Qp, to_agree (v:leibnizC V)).
Proof. by rewrite /to_gen_heap lookup_fmap=> ->. Qed.
Lemma gen_heap_singleton_included σ l q v :
{[l := (q, to_agree v)]} to_gen_heap σ σ !! l = Some v.
Proof.
......
......@@ -15,8 +15,8 @@ Definition to_excl {A} (a : A) : excl A := Excl a.
Definition gen_procUR (L V : Type) `{Countable L} : ucmraT :=
gmapUR L (gen_heapUR L V).
Definition to_gen_proc {L V} `{Countable L} (σ : (gmap L (gmap L V))) : gen_procUR L V :=
(* fmap (λ h, (fmap (λ v, (1%Qp, to_agree (v : leibnizC V))) h)) σ. *)
fmap (λ h, to_gen_heap h) σ.
(* fmap (λ h, (fmap (λ v, (1%Qp, to_agree (v : leibnizC V))) h)) σ. *)
(** The CMRA we need. *)
Class gen_procG (L V : Type) (Σ :gFunctors) `{Countable L} := GenProcG {
......@@ -41,6 +41,20 @@ Section proc_definitions.
Definition gen_proc_ctx (σ : gmap L (gmap L V)) : iProp Σ :=
own (gen_proc_name pG) ( (to_gen_proc σ)) (* ∗ gen_heap_ctx (snd σ) *).
(* Lemma unit_def : ((◯ (∅)):(auth (gen_procUR L V))) = (ε:(auth (gen_procUR L V))) . *)
(* eauto. *)
(* Qed. *)
(* Lemma derive_empty_heap (p : L) (σ : gmap L (gmap L V)) : *)
(* (* (gen_proc_ctx σ) ==∗ (gen_proc_ctx σ) ∗ (own (gen_proc_name pG) (ε)). *) *)
(* (gen_proc_ctx σ) ==∗ (gen_proc_ctx σ) ∗ (own (gen_proc_name pG) (◯ (∅))). *)
(* Proof. *)
(* iIntros "H". *)
(* rewrite unit_def. *)
(* iFrame. *)
(* iApply own_unit. *)
(* Qed. *)
Inductive proc_mapping : Type :=
| pinit : L -> proc_mapping
| pmap : L -> L -> Qp -> V -> proc_mapping
......@@ -54,27 +68,28 @@ Section proc_definitions.
| pmap p l q v => {[ p := {[ l := (q, to_agree (v : leibnizC V))]} ]}
end.
Definition proc_mapsto_def (pm : proc_mapping) : iProp Σ :=
Definition mapsto_def (pm : proc_mapping) : iProp Σ :=
own (gen_proc_name pG) ( (proc_match pm) ).
(* Definition proc_mapsto_def (p : L) (l : L) (q:Qp) (v : V) : iProp Σ := *)
(* own (gen_proc_name pG) (◯ {[ p := {[ l := (q, to_agree (v : leibnizC V)) ]} ]}). *)
(* Definition proc_mapsto_def (pid : L) (h : gmap L V) : iProp Σ := *)
(* own (gen_proc_name pG) (◯ {[ pid := to_gen_heap h ]}). *)
Definition proc_mapsto_aux : seal (@proc_mapsto_def). by eexists. Qed.
Definition proc_mapsto := unseal proc_mapsto_aux.
Definition proc_mapsto_eq : @proc_mapsto = @proc_mapsto_def := seal_eq proc_mapsto_aux.
Definition mapsto_aux : seal (@mapsto_def). by eexists. Qed.
Definition mapsto := unseal mapsto_aux.
Definition mapsto_eq : @mapsto = @mapsto_def := seal_eq mapsto_aux.
End proc_definitions.
Local Notation "l p↦{ p }{ q } v" :=
(proc_mapsto (pmap p l q v)) (at level 20).
(mapsto (pmap p l q v)) (at level 20).
Local Notation "l p↦{ p } v" :=
(l p{p}{1} v)%I (at level 20).
Local Notation "l p↦{ p }{ q } -" :=
( v, l p{p}{q} v)%I (at level 20) : uPred_scope.
Local Notation "l p↦{ p } -" :=
( v, l p{p} v)%I (at level 20) : uPred_scope.
Local Notation "< p >" :=
(proc_mapsto (pinit p)) (at level 20).
Local Notation "p↦{ p }" :=
(mapsto (pinit p)) (at level 20).
Section to_gen_proc.
Context (L V : Type) `{Countable L}.
......@@ -85,20 +100,42 @@ Section to_gen_proc.
Proof.
simpl. intros l. rewrite lookup_fmap. case (σ !! l); try reflexivity. intro g'. intros l'. rewrite lookup_fmap. by case (g' !! l').
Qed.
Lemma lookup_to_gen_proc_None σ l : σ !! l = None (to_gen_proc σ) !! l = None.
Lemma lookup_to_gen_proc_None (σ:gmap L (gmap L V)) (l:L) : σ !! l = None (to_gen_proc σ) !! l = None.
Proof. by rewrite /to_gen_proc lookup_fmap=> ->. Qed.
Lemma lookup_to_gen_proc_Some (σ:gmap L (gmap L V)) (σ':gmap L V) (l:L) : σ !! l = Some σ' (to_gen_proc σ) !! l = Some (to_gen_heap σ').
Proof. by rewrite /to_gen_proc lookup_fmap=> ->. Qed.
Lemma gen_proc_singleton_included σ (p:L) (l:L) (q:Qp) (v:V):
{[p := {[l := (q, to_agree v)]}]} (to_gen_proc σ) match (σ !! p) with None => None | Some(h) => h !! l end = Some v.
{[p := {[l := (q, to_agree v)]}]} (to_gen_proc σ) ( (σ' : gmap L V), σ !! p = Some(σ') /\ σ' !! l = Some(v)).
Proof.
rewrite singleton_included=> -[ah].
rewrite /to_gen_proc lookup_fmap fmap_Some_equiv => -[h'].
move=> /Some_included_total. destruct h'. destruct H0. rewrite H1.
intro.
rewrite H0.
revert H2.
apply gen_heap_singleton_included.
exists x.
split.
- eauto.
- revert H2. apply gen_heap_singleton_included.
Qed.
Lemma to_gen_proc_insert (p:L) (l:L) (v:V) (σ : gmap L (gmap L V)) :
(* Lemma gen_proc_singleton_included σ (p:L) (l:L) (q:Qp) (v:V): *)
(* {[p := {[l := (q, to_agree v)]}]} ≼ (to_gen_proc σ) → match (σ !! p) with None => None | Some(h) => h !! l end = Some v. *)
(* Proof. *)
(* rewrite singleton_included=> -[ah]. *)
(* rewrite /to_gen_proc lookup_fmap fmap_Some_equiv => -[h']. *)
(* move=> /Some_included_total. destruct h'. destruct H0. rewrite H1. *)
(* intro. *)
(* rewrite H0. *)
(* revert H2. *)
(* apply gen_heap_singleton_included. *)
(* Qed. *)
Lemma to_gen_proc_insert (p:L) (σ : gmap L (gmap L V)) (σ' : gmap L V) :
to_gen_proc (<[p:=σ']> σ) = <[p:=to_gen_heap σ']> (to_gen_proc σ).
Proof. by rewrite /to_gen_proc fmap_insert. Qed.
Lemma to_gen_proc_insert_val (p:L) (l:L) (v:V) (σ : gmap L (gmap L V)) :
to_gen_proc (<[ p := match (σ !! p) with None => <[l:=v]> | Some(h) => <[l:=v]>h end]>σ) = <[ p := match (σ !! p) with None => <[l:=(1%Qp, to_agree (v:leibnizC V))]>(to_gen_heap ) | Some(h) => <[l:=(1%Qp, to_agree (v:leibnizC V))]>(to_gen_heap h) end]> (to_gen_proc σ).
Proof. destruct (σ !! p).
- rewrite /to_gen_proc fmap_insert.
......@@ -108,14 +145,58 @@ Section to_gen_proc.
- rewrite /to_gen_proc fmap_insert.
assert ((to_gen_heap ((<[l := v]>):(gmap L V))) = ((<[l := (1%Qp, to_agree v)]>(to_gen_heap )):(gen_heapUR L V))). by rewrite /to_gen_heap fmap_insert. rewrite H0. reflexivity. Qed.
Lemma to_gen_proc_delete p l σ :
to_gen_proc (match σ !! p with None => σ | Some(h) => <[p := delete l h]>σ end) =
match σ !! p with None => (to_gen_proc σ) | Some(h) => <[p := delete l (to_gen_heap h)]>(to_gen_proc σ) end.
(* Definition delete2 `{Countable K} {A : Type} (p l:K) (σ:gmap K (gmap K A)) := *)
(* match (σ !! p) with *)
(* | None => σ *)
(* | Some(σ') => <[p := delete l σ']>σ *)
(* end. *)
(* Definition delete2 `{Countable K} {A : Type} (p i:K) (m: gmap K (gmap K A)) := *)
(* match (m !! p) with *)
(* | None => m *)
(* | Some(m') => <[p := delete i m']>m *)
(* end. *)
(* Lemma delete_something_update `{Countable K} {A : cmraT} (m:gmap K (gmap K A)) (p i: K) (x : A) : *)
(* (* m !! i = Some x → *) *)
(* (m, {[ p := {[ i := x ]} ]}) ~l~> (delete2 p i m, ∅). *)
(* Proof. *)
(* assert (m !! p = Some {[ i := x]}) by admit. *)
(* unfold delete2. *)
(* rewrite H1. *)
(* Admitted. *)
Lemma to_gen_proc_delete p σ :
to_gen_proc (delete p σ) = delete p (to_gen_proc σ).
Proof. by rewrite /to_gen_proc fmap_delete. Qed.
(* Lemma to_gen_proc_delete_val (p l : L) (σ : gmap L (gmap L V)) : *)
Lemma to_gen_proc_delete_val p l σ :
to_gen_proc (delete2 p l σ) = delete2 p l (to_gen_proc σ).
Proof.
destruct (σ !! p); try eauto.
- rewrite /to_gen_proc fmap_insert.
assert (to_gen_heap (delete l g) = delete l (to_gen_heap g)). apply to_gen_heap_delete. rewrite H0. reflexivity.
unfold delete2.
assert (σ !! p = None \/ o, σ !! p = Some o).
{ destruct (σ !! p).
- right. by exists g.
- left. reflexivity.
}
destruct H0.
- rewrite H0.
by rewrite lookup_to_gen_proc_None.
- destruct H0.
rewrite H0.
rewrite (lookup_to_gen_proc_Some σ x p) =>//.
rewrite to_gen_proc_insert. by rewrite to_gen_heap_delete.
Qed.
(* Lemma to_gen_proc_delete_val p l σ : *)
(* to_gen_proc (match σ !! p with None => σ | Some(h) => <[p := delete l h]>σ end) = *)
(* match σ !! p with None => (to_gen_proc σ) | Some(h) => <[p := delete l (to_gen_heap h)]>(to_gen_proc σ) end. *)
(* Proof. *)
(* destruct (σ !! p); try eauto. *)
(* - rewrite /to_gen_proc fmap_insert. *)
(* assert (to_gen_heap (delete l g) = delete l (to_gen_heap g)). apply to_gen_heap_delete. rewrite H0. reflexivity. *)
(* Qed. *)
End to_gen_proc.
Lemma gen_proc_init `{gen_procPreG L V Σ} σ :
......@@ -128,94 +209,187 @@ Qed.
(* Construction beyond this point! *)
Section gen_heap.
Context `{gen_heapG L V Σ}.
Section gen_proc.
Context `{gen_procG L V Σ}.
Implicit Types P Q : iProp Σ.
Implicit Types Φ : V iProp Σ.
Implicit Types σ : gmap L V.
Implicit Types h g : gen_heapUR L V.
Implicit Types l : L.
Implicit Types σ : gmap L (gmap L V).
Implicit Types h g : gen_procUR L V.
Implicit Types p l : L.
Implicit Types v : V.
(** General properties of mapsto *)
Global Instance mapsto_timeless l q v : Timeless (l {q} v).
Global Instance mapsto_timeless p l q v : Timeless (l p{p}{q} v).
Proof. rewrite mapsto_eq /mapsto_def. apply _. Qed.
Global Instance mapsto_fractional l v : Fractional (λ q, l {q} v)%I.
Global Instance mapsto_fractional p l v : Fractional (λ q, l p{p}{q} v)%I.
Proof.
intros p q. by rewrite mapsto_eq -own_op -auth_frag_op
op_singleton pair_op agree_idemp.
intros q q'. by rewrite mapsto_eq -own_op -auth_frag_op op_singleton op_singleton pair_op agree_idemp.
Qed.
Global Instance mapsto_as_fractional l q v :
AsFractional (l {q} v) (λ q, l {q} v)%I q.
Global Instance mapsto_as_fractional p l q v :
AsFractional (l p{p}{q} v) (λ q, l p{p}{q} v)%I q.
Proof. split. done. apply _. Qed.
Lemma mapsto_agree l q1 q2 v1 v2 : l {q1} v1 - l {q2} v2 - v1 = v2.
Print discreteC.
Lemma mapsto_agree p l q1 q2 v1 v2 : l p{p}{q1} v1 - l p{p}{q2} v2 - v1 = v2.
Proof.
apply wand_intro_r.
rewrite mapsto_eq -own_op -auth_frag_op own_valid discrete_valid.
f_equiv=> /auth_own_valid /=. rewrite op_singleton singleton_valid pair_op.
f_equiv=> /auth_own_valid /=. rewrite op_singleton singleton_valid op_singleton singleton_valid pair_op.
by intros [_ ?%agree_op_invL'].
Qed.
Global Instance ex_mapsto_fractional l : Fractional (λ q, l {q} -)%I.
(* Lemma mapsto_contains (p:L) (l:L) (v:V) (σ:gmap L (gmap L V)) (n:nat) : *)
(* gen_proc_ctx σ -∗ l p↦{p} v -∗ ⌜(∃ (σ' : gmap L V), ((to_gen_proc σ) !! p ≡{n}≡ Some (to_gen_heap σ') /\ (to_gen_heap σ') !! l ≡{n}≡ Some ((1%Qp, to_agree (v : leibnizC V)))))⌝. *)
(* Proof. *)
(* apply wand_intro_r. *)
(* rewrite mapsto_eq. *)
(* rewrite -own_op. *)
(* rewrite own_valid. *)
(* rewrite discrete_valid. *)
(* f_equiv => /=. *)
(* intros H1. *)
(* inversion H1. *)
(* simpl in H2. *)
(* specialize (H2 n). *)
(* revert H2. rewrite left_id. intros. *)
(* apply gen_proc_singleton_included in H2. *)
(* inversion H2. *)
(* exists {[ l := v ]}. *)
(* split. *)
(* - revert H2. rewrite left_id. intros. apply gen_proc_singleton_included in H2. rewrite singleton_includedN. intros. inversion H2. inversion H5. rewrite H6. revert H7. SearchAbout (≼). rewrite Some_included_totalN. rewrite singleton_includedN. inversion H7. rewrite H8. *)
(* rewrite H4. rewrite left_id. rewrite lookup_op. rewrite lookup_insert. admit. *)
(* - unfold to_gen_heap. rewrite fmap_insert. rewrite fmap_empty. by rewrite lookup_insert. *)
(* rewrite singleton_includedN in H2. *)
(* rewrite cmra_discrete_included_iff in H1. *)
(* rewrite singleton_included in H1. *)
(* rewrite singleton_included in H1. *)
(* assert ( ✓ (● to_gen_proc σ ⋅ ◯ proc_match (pmap p l 1 v)) = ✓{n} (● to_gen_proc σ ⋅ ◯ proc_match (pmap p l 1 v))) by admit. *)
(* rewrite H1 in a. *)
(* apply auth_validN_2 in a. *)
(* f_equiv => /auth_own_valid /=. *)
(* rewrite auth_own_valid. *)
(* auth_own_valid. *)
(* iIntros "H1". *)
(* iApply auth_validN_2 with "H1". *)
(* rewrite mapsto_eq -own_op -auth_frag_op own_valid discrete_valid. *)
(* f_equiv=> /auth_own_valid /=. rewrite op_singleton singleton_valid op_singleton singleton_valid pair_op. *)
(* by intros [_ ?%agree_op_invL']. *)
(* iIntros. *)
(* Admitted. *)
Global Instance ex_mapsto_fractional p l : Fractional (λ q, l p{p}{q} -)%I.
Proof.
intros p q. iSplit.
intros p' q'. iSplit.
- iDestruct 1 as (v) "[H1 H2]". iSplitL "H1"; eauto.
- iIntros "[H1 H2]". iDestruct "H1" as (v1) "H1". iDestruct "H2" as (v2) "H2".
iDestruct (mapsto_agree with "H1 H2") as %->. iExists v2. by iFrame.
Qed.
Global Instance ex_mapsto_as_fractional l q :
AsFractional (l {q} -) (λ q, l {q} -)%I q.
Global Instance ex_mapsto_as_fractional p l q :
AsFractional (l p{p}{q} -) (λ q, l p{p}{q} -)%I q.
Proof. split. done. apply _. Qed.
Lemma mapsto_valid l q v : l {q} v - q.
Lemma mapsto_valid p l q v : l p{p}{q} v - q.
Proof.
rewrite mapsto_eq /mapsto_def own_valid !discrete_valid.
by apply pure_mono=> /auth_own_valid /singleton_valid [??].
rewrite mapsto_eq. rewrite /mapsto_def. rewrite own_valid. rewrite !discrete_valid.
by apply pure_mono => /auth_own_valid /singleton_valid /singleton_valid [??].
Qed.
Lemma mapsto_valid_2 l q1 q2 v1 v2 : l {q1} v1 - l {q2} v2 - (q1 + q2)%Qp.
Lemma mapsto_valid_2 p l q1 q2 v1 v2 : l p{p}{q1} v1 - l p{p}{q2} v2 - (q1 + q2)%Qp.
Proof.
iIntros "H1 H2". iDestruct (mapsto_agree with "H1 H2") as %->.
iApply (mapsto_valid l _ v2). by iFrame.
iApply (mapsto_valid p l _ v2). by iFrame.
Qed.
Lemma gen_heap_alloc σ l v :
σ !! l = None gen_heap_ctx σ == gen_heap_ctx (<[l:=v]>σ) l v.
Lemma gen_proc_alloc p σ l v :
σ !! p = None gen_proc_ctx σ == gen_proc_ctx (<[p:={[l:=v]}]>σ) l p{p} v.
Proof.
iIntros (?) "Hσ". rewrite /gen_heap_ctx mapsto_eq /mapsto_def.
iIntros (?) "Hσ". rewrite /gen_proc_ctx mapsto_eq /mapsto_def.
iMod (own_update with "Hσ") as "[Hσ Hl]".
{ eapply auth_update_alloc,
(alloc_singleton_local_update _ _ (1%Qp, to_agree (v:leibnizC _)))=> //.
by apply lookup_to_gen_heap_None. }
iModIntro. rewrite to_gen_heap_insert. iFrame.
{ eapply auth_update_alloc. eapply (alloc_singleton_local_update _ _ (to_gen_heap {[l:=(v:leibnizC V)]})) => //.
by apply lookup_to_gen_proc_None.
apply to_gen_heap_valid. }
iModIntro. simpl. rewrite to_gen_proc_insert. unfold to_gen_heap. rewrite fmap_insert. rewrite fmap_empty. rewrite insert_empty. iFrame.
Qed.
Lemma gen_heap_dealloc σ l v :
gen_heap_ctx σ - l v == gen_heap_ctx (delete l σ).
Definition insert2 σ p l v :=
match σ !! p with
| None => <[p := {[ l := v ]}]>σ
| Some(σ') => <[p:= <[ l := v ]>σ']>σ
end.
Lemma gen_proc_alloc_val (p:L) (l:L) (v:V) (σ:gmap L (gmap L V)) (σ':gmap L V) :
σ !! p = Some σ' σ' !! l = None
(* gen_proc_ctx σ ==∗ gen_proc_ctx (<[p:=(<[l:=v]>σ')]>σ) ∗ l p↦{p} v. *)
gen_proc_ctx σ == gen_proc_ctx (insert2 σ p l v) l p{p} v.
Proof.
iIntros (? ?) "Hσ".
unfold insert2. rewrite H1.
rewrite <- insert_id with σ p σ' => //.
rewrite /gen_proc_ctx mapsto_eq /mapsto_def.
iMod (own_update with "Hσ") as "[Hσ Hl]".
{
eapply auth_update_alloc.
eapply (insert_alloc_local_update (to_gen_proc (<[p:=σ']>σ)) p (to_gen_heap σ') (to_gen_heap (<[l:=v]>σ')) (to_gen_heap (<[l:=v]>))) =>//.
- apply lookup_to_gen_proc_Some. apply lookup_insert.
- rewrite to_gen_heap_insert. rewrite to_gen_heap_insert. unfold to_gen_heap. rewrite fmap_empty.
eapply (alloc_local_update (to_gen_heap σ') l (1%Qp, to_agree (v:leibnizC _)))=> //.
by rewrite lookup_to_gen_heap_None.
}
iModIntro. rewrite to_gen_proc_insert. repeat rewrite insert_insert. rewrite to_gen_proc_insert. rewrite to_gen_heap_insert. unfold proc_match. unfold to_gen_heap. rewrite fmap_insert. rewrite fmap_empty. iFrame.
Qed.
Lemma gen_proc_dealloc (p:L) (l:L) (v:V) (σ:gmap L (gmap L V)) :
gen_proc_ctx σ - l p{p} v == gen_proc_ctx (delete2 p l σ) ( p{ p } ).
Proof.