Library ProcMap

Require Import FunctionalExtensionality.
Require Import HahnBase.
Require Import Heaps.
Require Import List.
Require Import Permissions.
Require Import Permutation.
Require Import Prelude.
Require Import Process.
Require Import QArith.
Require Import Qcanon.
Require Import Utf8.

Import ListNotations.

Set Implicit Arguments.

Process Maps


Module Type ProcMaps
  (dom : Domains)
  (heaps: Heaps dom)
  (procs: Processes dom).

Export dom heaps procs.

Process map entries

The set ProcMapEntry of process map entries is later used as the codomain of process maps.

Inductive ProcMapEntry :=
  | PEelem(q : Qc)(P : Proc)(xs : list ProcVar)(f : ProcVar -> Val)
  | PEfree
  | PEinvalid.

Add Search Blacklist "ProcMapEntry_rect".
Add Search Blacklist "ProcMapEntry_ind".
Add Search Blacklist "ProcMapEntry_rec".
Add Search Blacklist "ProcMapEntry_sind".

Bisimilarity

Two process map entries are equal up to bisimilarity if their components all agree, and their process terms are bisimilar.

Definition pmeBisim (c1 c2 : ProcMapEntry) : Prop :=
  match c1, c2 with
    | PEelem q1 P1 xs1 f1, PEelem q2 P2 xs2 f2 =>
        q1 = q2 /\ bisim P1 P2 /\ xs1 = xs2 /\ map f1 xs1 = map f2 xs2
    | PEfree, PEfree => True
    | PEinvalid, PEinvalid => True
    | _, _ => False
  end.

Notation "c1 ≃ c2" := (pmeBisim c1 c2) (only printing, at level 80).

The pmeBisim relation is an equivalence relation.

Global Instance pmeBisim_refl : Reflexive pmeBisim.
Global Instance pmeBisim_symm : Symmetric pmeBisim.
Global Instance pmeBisim_trans : Transitive pmeBisim.
Global Instance pmeBisim_equiv : Equivalence pmeBisim.

Hint Resolve pmeBisim_refl : core.

Bisimilarity is a congruence for PEelem.

Add Parametric Morphism : PEelem
  with signature eq ==> bisim ==> eq ==> eq ==> pmeBisim
    as PEelem_bisim_mor.

Below are several useful properties of pmeBisim.

Lemma pmeBisim_free :
  forall c1 c2, pmeBisim c1 c2 -> c1 = PEfree -> c2 = PEfree.

Lemma pmeBisim_equality :
  forall c q P xs f,
  pmeBisim c (PEelem q P xs f) ->
  exists P' f',
    c = PEelem q P' xs f' /\
    pmeBisim (PEelem q P xs f) (PEelem q P' xs f').

Lemma pmeBisim_F :
  forall q P xs F1 F2,
    (forall x : ProcVar, In x xs -> F1 x = F2 x) ->
  pmeBisim (PEelem q P xs F1) (PEelem q P xs F2).

Validity

A process map entry is valid if any fractional permission it holds is valid. Free entries are always valid, whereas invalid entries are never valid.

Definition pmeValid (c : ProcMapEntry) : Prop :=
  match c with
    | PEelem q _ _ _ => perm_valid q
    | PEfree => True
    | PEinvalid => False
  end.

Notation "√ c" := (pmeValid c) (only printing, at level 80).

Free entries are always valid, whereas invalid entries are never valid.

Lemma pmeValid_free : pmeValid PEfree.
Lemma pheValid_invalid :
  forall c, pmeValid c -> c <> PEinvalid.

Hint Resolve pmeValid_free : core.

Process map entry validity is closed under bisimilarity.

Lemma pmeValid_bisim :
  forall c1 c2, pmeBisim c1 c2 -> pmeValid c1 -> pmeValid c2.
Add Parametric Morphism : pmeValid
  with signature pmeBisim ==> iff as pmeValid_bisim_mor.

Disjointness

Two process map entries are defined to be disjoint if their permission components are together disjoint.

Definition pmeDisj (c1 c2 : ProcMapEntry) : Prop :=
  match c1, c2 with
    | PEelem q1 _ xs1 f1, PEelem q2 _ xs2 f2 =>
        perm_disj q1 q2 /\ xs1 = xs2 /\ map f1 xs1 = map f2 xs2
    | PEelem q _ _ _, PEfree
    | PEfree, PEelem q _ _ _ => perm_valid q
    | PEfree, PEfree => True
    | PEinvalid, _
    | _, PEinvalid => False
  end.

Notation "c1 ⟂ c2" := (pmeDisj c1 c2) (only printing, at level 80).

The relation pmeDisj is symmetric.

Global Instance pmeDisj_symm : Symmetric pmeDisj.

Any valid entry is disjoint with a free entry.

Lemma pmeDisj_free_l :
  forall c, pmeValid c -> pmeDisj c PEfree.
Lemma pmeDisj_free_r :
  forall c, pmeValid c -> pmeDisj PEfree c.

Hint Resolve pmeDisj_free_l pmeDisj_free_r : core.

No entry is disjoint with an invalid entry.

Lemma pmeDisj_invalid_l :
  forall c, ~ pmeDisj c PEinvalid.
Lemma pmeDisj_invalid_r :
  forall c, ~ pmeDisj PEinvalid c.

Any two disjoint entries are also valid.

Lemma pmeDisj_valid_l :
  forall c1 c2, pmeDisj c1 c2 -> pmeValid c1.
Lemma pmeDisj_valid_r :
  forall c1 c2, pmeDisj c1 c2 -> pmeValid c2.
Lemma pmeDisj_valid :
  forall c1 c2, pmeDisj c1 c2 -> pmeValid c1 /\ pmeValid c2.

Hint Resolve pmeDisj_valid_l pmeDisj_valid_r : core.

Disjoint entries can always be replaced by bisimilar ones.

Lemma pmeDisj_bisim_l :
  forall c1 c2 c, pmeBisim c1 c2 -> pmeDisj c1 c -> pmeDisj c2 c.
Lemma pmeDisj_bisim_r :
  forall c1 c2 c, pmeBisim c1 c2 -> pmeDisj c c1 -> pmeDisj c c2.
Add Parametric Morphism : pmeDisj
  with signature pmeBisim ==> pmeBisim ==> iff
    as pmeDisj_bisim_mor.

Disjoint union

The (disjoint) union of two process map entries is defined as the addition of their process and permission components.

Definition pmeUnion (c1 c2 : ProcMapEntry) : ProcMapEntry :=
  match c1, c2 with
    | PEelem q1 P1 xs1 f1, PEelem q2 P2 xs2 f2 =>
        if procvars_eq_dec xs1 xs2 then
          if vals_eq_dec (map f1 xs1) (map f2 xs2)
          then PEelem (q1 + q2) (Ppar P1 P2) xs1 f1
          else PEinvalid
        else PEinvalid
    | PEelem q P xs f, PEfree
    | PEfree, PEelem q P xs f => PEelem q P xs f
    | PEfree, PEfree => PEfree
    | PEinvalid, _
    | _, PEinvalid => PEinvalid
  end.

Notation "c1 ⨄ c2" :=
  (pmeUnion c1 c2)
  (only printing, at level 80, right associativity).

The pmeUnion disjoint union relation is associative and commutative with respect to bisimilarity.

Lemma pmeUnion_assoc :
  forall c1 c2 c3,
  pmeBisim (pmeUnion (pmeUnion c1 c2) c3) (pmeUnion c1 (pmeUnion c2 c3)).

Lemma pmeUnion_comm :
  forall c1 c2, pmeBisim (pmeUnion c1 c2) (pmeUnion c2 c1).

The disjoint union of two disjoint entries is always valid.

Lemma pmeUnion_valid :
  forall c1 c2, pmeDisj c1 c2 -> pmeValid (pmeUnion c1 c2).

Free entries are neutral with respect to disjoint union.

Lemma pmeUnion_free_l : forall c, pmeUnion c PEfree = c.
Lemma pmeUnion_free_r : forall c, pmeUnion PEfree c = c.

Hint Rewrite pmeUnion_free_l pmeUnion_free_r : core.

Invalid entries are absorbing with respect to disjoint union.

Lemma pmeUnion_invalid_l :
  forall c, pmeUnion c PEinvalid = PEinvalid.
Lemma pmeUnion_invalid_r :
  forall c, pmeUnion PEinvalid c = PEinvalid.

Bisimilarity of entries is closed under disjoint union.

Lemma pmeUnion_bisim_l :
  forall c1 c2 c,
  pmeBisim c1 c2 -> pmeBisim (pmeUnion c1 c) (pmeUnion c2 c).
Lemma pmeUnion_bisim_r :
  forall c1 c2 c,
  pmeBisim c1 c2 -> pmeBisim (pmeUnion c c1) (pmeUnion c c2).
Add Parametric Morphism : pmeUnion
  with signature pmeBisim ==> pmeBisim ==> pmeBisim
    as pmeUnion_bisim_mor.

Hint Resolve pmeUnion_bisim_l pmeUnion_bisim_r : core.

Below are several other useful properties of pmeUnion.

Lemma pmeUnion_elem :
  forall q1 q2 P1 P2 xs f,
  pmeUnion (PEelem q1 P1 xs f) (PEelem q2 P2 xs f) =
  PEelem (q1 + q2) (Ppar P1 P2) xs f.

Lemma pmeDisj_union_l :
  forall c1 c2 c3,
  pmeDisj c1 c2 -> pmeDisj (pmeUnion c1 c2) c3 -> pmeDisj c2 c3.
Lemma pmeDisj_union_r :
  forall c1 c2 c3,
  pmeDisj c2 c3 -> pmeDisj c1 (pmeUnion c2 c3) -> pmeDisj c1 c2.

Lemma pmeDisj_assoc_l :
  forall c1 c2 c3,
  pmeDisj c1 c2 ->
  pmeDisj (pmeUnion c1 c2) c3 ->
  pmeDisj c1 (pmeUnion c2 c3).
Lemma pmeDisj_assoc_r :
  forall c1 c2 c3,
  pmeDisj c2 c3 ->
  pmeDisj c1 (pmeUnion c2 c3) ->
  pmeDisj (pmeUnion c1 c2) c3.

Lemma pmeDisj_swap_r :
  forall c1 c2 c3,
  pmeDisj c1 c2 ->
  pmeDisj (pmeUnion c1 c2) c3 ->
  pmeDisj (pmeUnion c1 c3) c2.
Lemma pmeDisj_swap_l :
  forall c1 c2 c3,
  pmeDisj c1 c2 ->
  pmeDisj (pmeUnion c1 c2) c3 ->
  pmeDisj (pmeUnion c2 c3) c1.

Lemma pmeDisj_middle :
  forall c1 c2 c3 c4,
  pmeDisj c1 c2 ->
  pmeDisj c3 c4 ->
  pmeDisj (pmeUnion c1 c2) (pmeUnion c3 c4) ->
  pmeDisj c2 c3.

Lemma pmeDisj_compat :
  forall c1 c2 c3 c4,
  pmeDisj c1 c3 ->
  pmeDisj c2 c4 ->
  pmeDisj (pmeUnion c1 c3) (pmeUnion c2 c4) ->
  pmeDisj (pmeUnion c1 c2) (pmeUnion c3 c4).

Lemma pmeUnion_swap_l :
  forall c1 c2 c3,
  pmeBisim
    (pmeUnion c1 (pmeUnion c2 c3))
    (pmeUnion c2 (pmeUnion c1 c3)).
Lemma pmeUnion_swap_r :
  forall c1 c2 c3,
  pmeBisim
    (pmeUnion (pmeUnion c1 c2) c3)
    (pmeUnion (pmeUnion c1 c3) c2).

Lemma pmeUnion_compat :
  forall c1 c2 c3 c4,
  pmeBisim
    (pmeUnion (pmeUnion c1 c3) (pmeUnion c2 c4))
    (pmeUnion (pmeUnion c1 c2) (pmeUnion c3 c4)).

Lemma pmeUnion_free :
  forall c1 c2,
  pmeUnion c1 c2 = PEfree <-> c1 = PEfree /\ c2 = PEfree.

Lemma pmeUnion_not_free :
  forall c1 c2,
  pmeUnion c1 c2 <> PEfree <-> c1 <> PEfree \/ c2 <> PEfree.

Entirety

Any process map entry c is entire if c is an occupied entry with a full fractional permission.

Definition pmeEntire (c : ProcMapEntry) : Prop :=
  match c with
    | PEfree
    | PEinvalid => False
    | PEelem q _ _ _ => q = perm_full
  end.

Entire entries can always be replaced by bisimilar ones.

Lemma pmeEntire_bisim :
  forall c1 c2, pmeBisim c1 c2 -> pmeEntire c1 -> pmeEntire c2.
Add Parametric Morphism : pmeEntire
  with signature pmeBisim ==> iff as pmeEntire_bisim_mor.

Below are several other useful properties of entirety.

Lemma pmeEntire_union :
  forall c1 c2,
  pmeDisj c1 c2 ->
  pmeEntire c1 \/ pmeEntire c2 ->
  pmeEntire (pmeUnion c1 c2).

Lemma pmeDisj_entire_free :
  forall c1 c2, pmeDisj c1 c2 -> pmeEntire c1 -> c2 = PEfree.

Lemma pmeEntire_content :
  forall c,
  pmeEntire c -> exists P xs f, c = PEelem perm_full P xs f.

Lemma pmeEntire_exp_l :
  forall c1 c2,
  pmeDisj c1 c2 -> pmeEntire c1 -> pmeUnion c1 c2 = c1.
Lemma pmeEntire_exp_r :
  forall c1 c2,
  pmeDisj c1 c2 -> pmeEntire c2 -> pmeUnion c1 c2 = c2.

Projection

The projection of any process map entry is the list of values obtained by taking the image of the mappings stored in occupied entries (or nil if the entry of free or invalid).

Definition pmeProj (c : ProcMapEntry) : list Val :=
  match c with
    | PEelem _ _ xs f => map f xs
    | PEfree
    | PEinvalid => nil
  end.

Projection is closed under bisimilarity.

Lemma pmeProj_bisim :
  forall c1 c2, pmeBisim c1 c2 -> pmeProj c1 = pmeProj c2.
Add Parametric Morphism : pmeProj
  with signature pmeBisim ==> eq as pmeProj_bisim_mor.

Below are several useful properties for projections.

Lemma pmeProj_union :
  forall c1 c2 v,
  pmeDisj c1 c2 ->
  In v (pmeProj c1) ->
  In v (pmeProj (pmeUnion c1 c2)).

Lemma pmeProj_disj_union :
  forall c1 c2,
  pmeDisj c1 c2 ->
  pmeProj c1 <> nil ->
  pmeProj (pmeUnion c1 c2) = pmeProj c1.

Heap coverage

Any process map entry c is said to fully cover a heap h if h contains an entry at every location that is in the projection of c.

Definition pmeCovers (c : ProcMapEntry)(h : Heap) : Prop :=
  forall l, In l (pmeProj c) -> exists v, h l = Some v.

Heap coverage is closed under bisimilarity.

Lemma pmeCovers_bisim :
  forall c1 c2 h,
  pmeBisim c1 c2 -> pmeCovers c1 h -> pmeCovers c2 h.
Add Parametric Morphism : pmeCovers
  with signature pmeBisim ==> eq ==> iff as pmeCovers_bisim_mor.

Free entries cover every heap.

Lemma pmeCovers_free :
  forall h, pmeCovers PEfree h.

Below are various other useful properties of coverage.

Lemma pmeCovers_union :
  forall c1 c2 h,
  pmeDisj c1 c2 ->
  pmeCovers (pmeUnion c1 c2) h ->
  pmeCovers c1 h.

Lemma pmeCovers_hUpdate :
  forall c h l v,
  ~ In l (pmeProj c) -> pmeCovers c h -> pmeCovers c (hUpdate h l v).

Lemma pmeCovers_agrees :
  forall c h1 h2,
    (forall l, In l (pmeProj c) -> h1 l = h2 l) ->
  pmeCovers c h1 ->
  pmeCovers c h2.

Lemma pmeCovers_subheap :
  forall c h1 h2,
    (forall l v, h1 l = Some v -> h2 l = Some v) ->
  pmeCovers c h1 ->
  pmeCovers c h2.

Lemma pmeCovers_occ :
  forall c h1 h2,
    (forall l, h1 l <> None -> h2 l <> None) ->
  pmeCovers c h1 ->
  pmeCovers c h2.

Agreement

The following relation pmeAgree c1 c2 captures whether two process map entries c1 and c2 agree on their static components (which is everything except processes).

Definition pmeAgree (c1 c2 : ProcMapEntry) : Prop :=
  match c1, c2 with
    | PEfree, PEfree
    | PEinvalid, PEinvalid => True
    | PEelem q1 _ xs1 F1, PEelem q2 _ xs2 F2 =>
        q1 = q2 /\ xs1 = xs2 /\ map F1 xs1 = map F2 xs2
    | _, _ => False
  end.

The pmeAgree relation is an equivalence relation.

Global Instance pmeAgree_refl : Reflexive pmeAgree.
Global Instance pmeAgree_symm : Symmetric pmeAgree.
Global Instance pmeAgree_trans : Transitive pmeAgree.
Global Instance pmeAgree_equiv : Equivalence pmeAgree.

Hint Resolve pmeAgree_refl : core.

Bisimilarity is a subrelation of agreement.

Global Instance pmeAgree_bisim : subrelation pmeBisim pmeAgree.

Add Parametric Morphism : pmeAgree
  with signature pmeAgree ==> pmeAgree ==> iff
    as pmeAgree_agree_mor.

Disjointness is closed under agreement.

Lemma pmeDisj_agree_l :
  forall c1 c2 c3,
  pmeAgree c1 c2 -> pmeDisj c1 c3 -> pmeDisj c2 c3.
Lemma pmeDisj_agree_r :
  forall c1 c2 c3,
  pmeAgree c1 c2 -> pmeDisj c3 c1 -> pmeDisj c3 c2.
Add Parametric Morphism : pmeDisj
  with signature pmeAgree ==> pmeAgree ==> iff
    as pmeDisj_agree_mor.

Disjoint union is closed under agreement

Lemma pmeAgree_union_l :
  forall c1 c2 c3,
  pmeAgree c1 c2 -> pmeAgree (pmeUnion c1 c3) (pmeUnion c2 c3).
Lemma pmeAgree_union_r :
  forall c1 c2 c3,
  pmeAgree c1 c2 -> pmeAgree (pmeUnion c3 c1) (pmeUnion c3 c2).
Add Parametric Morphism : pmeUnion
  with signature pmeAgree ==> pmeAgree ==> pmeAgree
    as pmeUnion_agree_mor.

Hint Resolve pmeAgree_union_l pmeAgree_union_r : core.

Below are other useful properties of agreement.

Lemma pmeProj_agree :
  forall c1 c2, pmeAgree c1 c2 -> pmeProj c1 = pmeProj c2.
Add Parametric Morphism : pmeProj
  with signature pmeAgree ==> eq
    as pmeProj_agree_mor.

Lemma pmeCovers_agree :
  forall c1 c2 h,
  pmeAgree c1 c2 ->
  pmeCovers c1 h ->
  pmeCovers c2 h.
Add Parametric Morphism : pmeCovers
  with signature pmeAgree ==> eq ==> iff
    as pmeCovers_agree_mor.

Weak agreement

Weak agreement between two process map entries is essentially the same as ordinary agreement, however permission components are not involved in the agreement.

Definition pmeWeakAgree (c1 c2 : ProcMapEntry) : Prop :=
  match c1, c2 with
    | PEfree, PEfree
    | PEinvalid, PEinvalid => True
    | PEelem _ _ xs1 F1, PEelem _ _ xs2 F2 =>
        xs1 = xs2 /\ map F1 xs1 = map F2 xs2
    | _, _ => False
  end.

Weak agreement is an equivalence relation.

Global Instance pmeWeakAgree_refl : Reflexive pmeWeakAgree.
Global Instance pmeWeakAgree_symm : Symmetric pmeWeakAgree.
Global Instance pmeWeakAgree_trans : Transitive pmeWeakAgree.
Global Instance pmeWeakAgree_equiv : Equivalence pmeWeakAgree.

Hint Resolve pmeWeakAgree_refl : core.

(Ordinary) agreement and bisimilarity are both subrelations of weak agreement.

Global Instance pmeAgree_weaken : subrelation pmeAgree pmeWeakAgree.
Global Instance pmeWeakAgree_bisim : subrelation pmeBisim pmeWeakAgree.

Below are several other useful properties of weak agreement.

Lemma pmeWeakAgree_union_l :
  forall c1 c2 c3,
  pmeWeakAgree c1 c2 -> pmeWeakAgree (pmeUnion c1 c3) (pmeUnion c2 c3).
Lemma pmeWeakAgree_union_r :
  forall c1 c2 c3,
  pmeWeakAgree c1 c2 -> pmeWeakAgree (pmeUnion c3 c1) (pmeUnion c3 c2).

Hint Resolve pmeWeakAgree_union_l pmeWeakAgree_union_r : core.

Lemma pmeWeakAgree_proj :
  forall c1 c2,
  pmeWeakAgree c1 c2 -> pmeProj c1 = pmeProj c2.
Add Parametric Morphism : pmeProj
  with signature pmeWeakAgree ==> eq
  as pmeWeakAgree_proj_mor.

Occupation

The pmeOcc predicate determines whether a given process map entry is occupied, i.e., contains some element.

Definition pmeOcc (c : ProcMapEntry) : Prop :=
  match c with
    | PEelem _ _ _ _ => True
    | _ => False
  end.

Occupation is closed under bisimilarity.

Lemma pmeOcc_bisim :
  forall c1 c2, pmeBisim c1 c2 -> pmeOcc c1 -> pmeOcc c2.
Add Parametric Morphism : pmeOcc
  with signature pmeBisim ==> iff as pmeOcc_bisim_mor.

Occupation is closed under (ordinary) agreement.

Lemma pmeOcc_agree :
  forall c1 c2, pmeAgree c1 c2 -> pmeOcc c1 -> pmeOcc c2.
Add Parametric Morphism : pmeOcc
  with signature pmeAgree ==> iff as pmeOcc_agree_mor.

Below are several more useful properties of occupation.

Lemma pmeOcc_union_l :
  forall c1 c2,
  pmeDisj c1 c2 -> pmeOcc c1 -> pmeOcc (pmeUnion c1 c2).
Lemma pmeOcc_union_r :
  forall c1 c2,
  pmeDisj c1 c2 -> pmeOcc c2 -> pmeOcc (pmeUnion c1 c2).

Lemma pmeOcc_destruct :
  forall c,
  pmeOcc c -> exists q P xs f, c = PEelem q P xs f.

Lemma pmeWeakAgree_union_occ :
  forall c1 c2,
  pmeDisj c1 c2 -> pmeOcc c1 -> pmeWeakAgree c1 (pmeUnion c1 c2).

Process maps


Definition ProcMap := Val -> ProcMapEntry.

The identity process map is free at every entry.

Definition pmIden : ProcMap := fun _ => PEfree.

An update operation for process maps:

Definition pmUpdate (pm : ProcMap)(v : Val)(c : ProcMapEntry) :=
  update val_eq_dec pm v c.

Bisimilarity

Two process maps are bisimilar if their entries are pointwise bisimilar (with respect to pmeBisim).

Definition pmBisim : relation ProcMap :=
  pointwise_relation Val pmeBisim.

Notation "pm1 ≃ pm2" := (pmBisim pm1 pm2) (only printing, at level 80).

Bisimilarity preserves any free entries.

Lemma pmBisim_free :
  forall pm1 pm2 pid,
  pmBisim pm1 pm2 -> pm1 pid = PEfree -> pm2 pid = PEfree.

Bisimilarity is an equivalence relation.

Global Instance pmBisim_refl : Reflexive pmBisim.
Global Instance pmBisim_symm : Symmetric pmBisim.
Global Instance pmBisim_trans : Transitive pmBisim.
Global Instance pmBisim_equiv : Equivalence pmBisim.

Hint Resolve pmBisim_refl : core.

Process map updates are closed under bisimilarity.

Lemma pmUpdate_bisim :
  forall pm1 pm2 pid c1 c2,
  pmBisim pm1 pm2 ->
  pmeBisim c1 c2 ->
  pmBisim (pmUpdate pm1 pid c1) (pmUpdate pm2 pid c2).
Add Parametric Morphism : pmUpdate
  with signature pmBisim ==> eq ==> pmeBisim ==> pmBisim
    as pmUpdate_bisim_mor.

Hint Resolve pmUpdate_bisim : core.

Validity

Any process map is defined to be valid if all its entries are valid.

Definition pmValid (pm : ProcMap) : Prop :=
  forall pid, pmeValid (pm pid).

Notation "√ pm" := (pmValid pm) (only printing, at level 80).

Validity is closed under bisimilarity.

Lemma pmValid_bisim :
  forall pm1 pm2, pmBisim pm1 pm2 -> pmValid pm1 -> pmValid pm2.
Add Parametric Morphism : pmValid
  with signature pmBisim ==> iff as pmValid_bisim_mor.

Below are several other useful properties of validity.

Lemma pmValid_iden : pmValid pmIden.

Hint Resolve pmValid_iden : core.

Lemma pmValid_update :
  forall c pm pid,
  pmeValid c -> pmValid pm -> pmValid (pmUpdate pm pid c).

Disjointness

Two process maps are defined to be disjoint if their entries are disjoint pairwise.

Definition pmDisj : relation ProcMap :=
  pointwise_relation Val pmeDisj.

Notation "pm1 ⟂ pm2" := (pmDisj pm1 pm2) (only printing, at level 80).

Process map disjointness is a symmetric relation.

Global Instance pmDisj_symm : Symmetric pmDisj.

Disjointness is closed under bisimilarity.

Lemma pmDisj_bisim_l :
  forall pm1 pm2 pm,
  pmBisim pm1 pm2 -> pmDisj pm1 pm -> pmDisj pm2 pm.
Lemma pmDisj_bisim_r :
  forall pm1 pm2 pm,
  pmBisim pm1 pm2 -> pmDisj pm pm1 -> pmDisj pm pm2.
Add Parametric Morphism : pmDisj
  with signature pmBisim ==> pmBisim ==> iff
    as pmDisj_bisim_mor.

Any two process maps related by disjointness are also valid.

Lemma pmDisj_valid_l :
  forall pm1 pm2, pmDisj pm1 pm2 -> pmValid pm1.
Lemma pmDisj_valid_r :
  forall pm1 pm2, pmDisj pm1 pm2 -> pmValid pm2.
Lemma pmDisj_valid :
  forall pm1 pm2, pmDisj pm1 pm2 -> pmValid pm1 /\ pmValid pm2.

Below are other useful properties of disjointness.

Lemma pmDisj_iden_l :
  forall pm, pmValid pm -> pmDisj pm pmIden.
Lemma pmDisj_iden_r :
  forall pm, pmValid pm -> pmDisj pmIden pm.

Hint Resolve pmDisj_iden_l pmDisj_iden_r : core.

Lemma pmDisj_upd :
  forall c1 c2 pm1 pm2 pid,
  pmeDisj c1 c2 ->
  pmDisj pm1 pm2 ->
  pmDisj (pmUpdate pm1 pid c1) (pmUpdate pm2 pid c2).

Hint Resolve pmDisj_upd : core.

Disjoint union

The (disjoint) union of two process maps is defined to be the pairwise disjoint union of their entries.

Definition pmUnion (pm1 pm2 : ProcMap) : ProcMap :=
  fun pid => pmeUnion (pm1 pid) (pm2 pid).

Notation "pm1 ⨄ pm2" :=
  (pmUnion pm1 pm2)
  (only printing, at level 80, right associativity).

Disjoint union is closed under bisimilarity.

Lemma pmUnion_bisim :
  forall pm1 pm2 pm1' pm2',
  pmBisim pm1 pm2 -> pmBisim pm1' pm2' ->
  pmBisim (pmUnion pm1 pm1') (pmUnion pm2 pm2').
Add Parametric Morphism : pmUnion
  with signature pmBisim ==> pmBisim ==> pmBisim
    as pmUnion_bisim_mor.

Identity laws for disjoint union:

Lemma pmUnion_iden_l :
  forall pm, pmUnion pm pmIden = pm.
Lemma pmUnion_iden_r :
  forall pm, pmUnion pmIden pm = pm.

Hint Rewrite pmUnion_iden_l pmUnion_iden_r : core.

Disjoint union is associative and commutative.

Lemma pmUnion_assoc :
  forall pm1 pm2 pm3,
  pmBisim
    (pmUnion (pmUnion pm1 pm2) pm3)
    (pmUnion pm1 (pmUnion pm2 pm3)).

Lemma pmUnion_comm :
  forall pm1 pm2,
  pmBisim (pmUnion pm1 pm2) (pmUnion pm2 pm1).

Below are various other useful properties of pmUnion.

Lemma pmUnion_valid :
  forall pm1 pm2,
  pmDisj pm1 pm2 -> pmValid (pmUnion pm1 pm2).

Hint Resolve pmUnion_valid : core.

Lemma pmDisj_union_l :
  forall pm1 pm2 pm3,
  pmDisj pm1 pm2 -> pmDisj (pmUnion pm1 pm2) pm3 -> pmDisj pm2 pm3.
Lemma pmDisj_union_r :
  forall pm1 pm2 pm3,
  pmDisj pm2 pm3 -> pmDisj pm1 (pmUnion pm2 pm3) -> pmDisj pm1 pm2.

Lemma pmDisj_assoc_l :
  forall pm1 pm2 pm3,
  pmDisj pm1 pm2 ->
  pmDisj (pmUnion pm1 pm2) pm3 ->
  pmDisj pm1 (pmUnion pm2 pm3).
Lemma pmDisj_assoc_r :
  forall pm1 pm2 pm3,
  pmDisj pm2 pm3 ->
  pmDisj pm1 (pmUnion pm2 pm3) ->
  pmDisj (pmUnion pm1 pm2) pm3.

Lemma pmDisj_swap_r :
  forall pm1 pm2 pm3,
  pmDisj pm1 pm2 ->
  pmDisj (pmUnion pm1 pm2) pm3 ->
  pmDisj (pmUnion pm1 pm3) pm2.
Lemma pmDisj_swap_l :
  forall pm1 pm2 pm3,
  pmDisj pm1 pm2 ->
  pmDisj (pmUnion pm1 pm2) pm3 ->
  pmDisj (pmUnion pm2 pm3) pm1.

Lemma pmUnion_update :
  forall pm1 pm2 c1 c2 pid,
  pmUpdate (pmUnion pm1 pm2) pid (pmeUnion c1 c2) =
  pmUnion (pmUpdate pm1 pid c1) (pmUpdate pm2 pid c2).

Hint Rewrite pmUnion_update : core.

Lemma pmUnion_elem :
  forall pm1 pm2 pid,
  pmeUnion (pm1 pid) (pm2 pid) = pmUnion pm1 pm2 pid.

Lemma pmDisj_middle :
  forall pm1 pm2 pm3 pm4,
  pmDisj pm1 pm2 ->
  pmDisj pm3 pm4 ->
  pmDisj (pmUnion pm1 pm2) (pmUnion pm3 pm4) ->
  pmDisj pm2 pm3.

Lemma pmDisj_compat :
  forall pm1 pm2 pm3 pm4,
  pmDisj pm1 pm3 ->
  pmDisj pm2 pm4 ->
  pmDisj (pmUnion pm1 pm3) (pmUnion pm2 pm4) ->
  pmDisj (pmUnion pm1 pm2) (pmUnion pm3 pm4).

Lemma pmUnion_swap_l :
  forall pm1 pm2 pm3,
  pmBisim
    (pmUnion pm1 (pmUnion pm2 pm3))
    (pmUnion pm2 (pmUnion pm1 pm3)).
Lemma pmUnion_swap_r :
  forall pm1 pm2 pm3,
  pmBisim
    (pmUnion (pmUnion pm1 pm2) pm3)
    (pmUnion (pmUnion pm1 pm3) pm2).

Hint Resolve pmUnion_swap_l pmUnion_swap_r : core.

Lemma pmUnion_compat :
  forall pm1 pm2 pm3 pm4,
  pmBisim
    (pmUnion (pmUnion pm1 pm3) (pmUnion pm2 pm4))
    (pmUnion (pmUnion pm1 pm2) (pmUnion pm3 pm4)).

Hint Resolve pmUnion_compat : core.

Finiteness

Any process map pm is defined to be finite all occupied entries of pm can be mapped to a finite structure, in this case a list.

Definition pmFinite (pm : ProcMap) : Prop :=
  exists xs : list Val,
    forall pid, pm pid <> PEfree -> In pid xs.

Finiteness is closed under bisimilarity.

Lemma pmFinite_bisim :
  forall pm1 pm2,
  pmBisim pm1 pm2 -> pmFinite pm1 -> pmFinite pm2.
Add Parametric Morphism : pmFinite
  with signature pmBisim ==> iff as pmFinite_bisim_mor.

The identity process map is trivially finite.

Lemma pmFinite_iden : pmFinite pmIden.

Hint Resolve pmFinite_iden : core.

The following property is the main property of interest: if a process map pm is finite, then one is always able to find an unoccupied entry in pm.

Lemma pmFinite_free :
  forall pm, pmFinite pm -> exists pid, pm pid = PEfree.

Process map updates preserve finiteness.

Lemma pmFinite_update :
  forall pm pid c,
  pmFinite pm -> pmFinite (pmUpdate pm pid c).

Below are several other interesting properties of finiteness.

Lemma pmFinite_union :
  forall pm1 pm2,
  pmFinite (pmUnion pm1 pm2) <-> pmFinite pm1 /\ pmFinite pm2.

Projections

Any value v is defined to be in the projection of pm if v is in the projection of one of the entries of pm.

Definition pmProj (pm : ProcMap)(v : Val) : Prop :=
  exists pid, In v (pmeProj (pm pid)).

Process map projections are closed under bisimilarity.

Lemma pmProj_bisim :
  forall pm1 pm2 l,
  pmBisim pm1 pm2 -> pmProj pm1 l -> pmProj pm2 l.
Add Parametric Morphism : pmProj
  with signature pmBisim ==> eq ==> iff as pmProj_bisim_mor.

Below are several other useful properties of projections.

Lemma pmProj_union :
  forall pm1 pm2 v,
  pmDisj pm1 pm2 -> pmProj pm1 v -> pmProj (pmUnion pm1 pm2) v.

Coverings

Any process map pm is defined to cover a heap h if all entries of pm cover h (with respect to pmeCovers).

Definition pmCovers (pm : ProcMap)(h : Heap) : Prop :=
  forall pid, pmeCovers (pm pid) h.

Coverage is closed under bisimilarity.

Lemma pmCovers_bisim :
  forall pm1 pm2 h,
  pmBisim pm1 pm2 -> pmCovers pm1 h -> pmCovers pm2 h.
Add Parametric Morphism : pmCovers
  with signature pmBisim ==> eq ==> iff
    as pmCovers_bisim_mor.

The identity process map covers any heap.

Lemma pmCovers_iden :
  forall h, pmCovers pmIden h.

Below are several other useful properties of coverage.

Lemma pmCovers_update :
  forall pm h pid c,
    (forall l, In l (pmeProj c) -> exists v, h l = Some v) ->
  pmCovers pm h ->
  pmCovers (pmUpdate pm pid c) h.

Lemma pmCovers_hUpdate :
  forall pm h l v,
  ~ pmProj pm l -> pmCovers pm h -> pmCovers pm (hUpdate h l v).

Lemma pmCovers_union :
  forall pm1 pm2 h,
  pmDisj pm1 pm2 ->
  pmCovers (pmUnion pm1 pm2) h ->
  pmCovers pm1 h.

Lemma pmCovers_agrees :
  forall pm h1 h2,
    (forall l, pmProj pm l -> h1 l = h2 l) ->
  pmCovers pm h1 ->
  pmCovers pm h2.

Lemma pmCovers_subheap :
  forall pm h1 h2,
    (forall l v, h1 l = Some v -> h2 l = Some v) ->
  pmCovers pm h1 ->
  pmCovers pm h2.

Lemma pmCovers_occ :
  forall pm h1 h2,
    (forall l, h1 l <> None -> h2 l <> None) ->
  pmCovers pm h1 ->
  pmCovers pm h2.

Agreement

Any two process maps are defined to agree if their entries agree pairwise with respect to pmeAgree.

Definition pmAgree : relation ProcMap :=
  pointwise_relation Val pmeAgree.

Process map agreement is an equivalence relation.

Global Instance pmAgree_refl : Reflexive pmAgree.
Global Instance pmAgree_symm : Symmetric pmAgree.
Global Instance pmAgree_trans : Transitive pmAgree.
Global Instance pmAgree_equiv : Equivalence pmAgree.

Hint Resolve pmAgree_refl : core.

Bisimilarity is a subrelation of agreement.

Global Instance pmAgree_bisim : subrelation pmBisim pmAgree.

Add Parametric Morphism : pmAgree
  with signature pmAgree ==> pmAgree ==> iff
    as pmAgree_agree_mor.

Disjoint maps may always be replaced by agreeing ones.

Add Parametric Morphism : pmDisj
  with signature pmAgree ==> pmAgree ==> iff
    as pmDisj_agree_mor.

Process map finiteness is closed under agreement.

Lemma pmFinite_agree :
  forall pm1 pm2,
  pmAgree pm1 pm2 -> pmFinite pm1 -> pmFinite pm2.
Add Parametric Morphism : pmFinite
  with signature pmAgree ==> iff as pmFinite_agree_mor.

Also coverage is closed under agreement.

Lemma pmCovers_agree :
  forall pm1 pm2 h,
  pmAgree pm1 pm2 -> pmCovers pm1 h -> pmCovers pm2 h.
Add Parametric Morphism : pmCovers
  with signature pmAgree ==> eq ==> iff as pmCovers_agree_mor.

Disjoint union is closed under agreement.

Lemma pmAgree_union_l :
  forall pm1 pm2 pm3,
  pmAgree pm1 pm2 -> pmAgree (pmUnion pm1 pm3) (pmUnion pm2 pm3).
Lemma pmAgree_union_r :
  forall pm1 pm2 pm3,
  pmAgree pm1 pm2 -> pmAgree (pmUnion pm3 pm1) (pmUnion pm3 pm2).
Add Parametric Morphism : pmUnion
  with signature pmAgree ==> pmAgree ==> pmAgree
    as pmUnion_agree_mor.

Hint Resolve pmAgree_union_l pmAgree_union_r : core.

Weak agreement

Two process maps are defined to agree weakly if their entries pointwise weakly agree with each other, with respect to pmeWeakAgree.

Definition pmWeakAgree : relation ProcMap :=
  pointwise_relation Val pmeWeakAgree.

Weak agreement is an equivalence relation.

Global Instance pmWeakAgree_refl : Reflexive pmWeakAgree.
Global Instance pmWeakAgree_symm : Symmetric pmWeakAgree.
Global Instance pmWeakAgree_trans : Transitive pmWeakAgree.
Global Instance pmWeakAgree_equiv : Equivalence pmWeakAgree.

Hint Resolve pmWeakAgree_refl : core.

Bisimilarity and agreement are both subrelations of weak agreement.

Global Instance pmWeakAgree_bisim : subrelation pmBisim pmWeakAgree.
Global Instance pmWeakAgree_agree : subrelation pmAgree pmWeakAgree.

Process map finiteness is closed under weak agreement.

Lemma pmFinite_weak_agree :
  forall pm1 pm2,
  pmWeakAgree pm1 pm2 -> pmFinite pm1 -> pmFinite pm2.
Add Parametric Morphism : pmFinite
  with signature pmWeakAgree ==> iff
    as pmFinite_weak_agree_mor.

Below are other useful properties of weak agreement.

Lemma pmWeakAgree_union_l :
  forall pm1 pm2 pm3,
  pmWeakAgree pm1 pm2 ->
  pmWeakAgree (pmUnion pm1 pm3) (pmUnion pm2 pm3).
Lemma pmWeakAgree_union_r :
  forall pm1 pm2 pm3,
  pmWeakAgree pm1 pm2 ->
  pmWeakAgree (pmUnion pm3 pm1) (pmUnion pm3 pm2).

Hint Resolve pmWeakAgree_union_l pmWeakAgree_union_r : core.

End ProcMaps.