# HOcore.Multiset

Require Import HOcore.Prelim.

Require Import HOcore.HoCore
HOcore.Ren.

This file contains the definition of multisets via unordered lists and some properties about them

# Multisets

(* Multisets are represented by unordered lists of nat *)
Definition multiset := list nat.
Definition nat_dec := Nat.eq_dec.
Definition mult := count_occ nat_dec.

(* Multiplicity can be split *)
Lemma union_mult (m1 m2: multiset) (n: nat):
mult (m1 ++ m2) n = mult m1 n + mult m2 n.
Proof.
induction m1.
- reflexivity.
- simpl. destruct (nat_dec a n); omega.
Qed.

(* Definition of Multiset containment *)
Definition mle (m1 m2: multiset) :=
forall a:nat, mult m1 a <= mult m2 a.

(* Counting unguarded variables *)
Fixpoint count (p: process): multiset :=
match p with
| Send a p => []
| Receive a p => []
| Var n => [n]
| Par p1 p2 => (count p1) ++ (count p2)
| Nil => []
end.

# Renaming preserves count

Lemma renaming_preserv_count
(p: process)
(n: var)
(xi: var -> var)
(sigma: var -> process)
(H1: xi >>> sigma = ids):
mult (count p) n = mult (count p.[ren xi]) (xi n).
Proof.
induction p; asimpl; auto.
- destruct (nat_dec n v).
+ clear H1. ainv. simpl.
destruct (nat_dec (xi v) (xi v)).
* destruct (nat_dec v v); auto. exfalso. auto.
* exfalso. auto.
+ simpl.
destruct (nat_dec (xi n) (xi v)).
* assert (H2: xi n = xi v) by auto.
eapply inj_ren_inv_var in H2; eauto.
* destruct (nat_dec v n). exfalso. auto.
destruct (nat_dec (xi v) (xi n)). exfalso. auto. auto.
- do 2 rewrite union_mult. omega.
Qed.

# Finite sums

Definition fin_sum (f: nat -> nat) (m: multiset): nat :=
fold_right (fun x a => (f x + a)%nat) 0 m.

Lemma fin_sum_reduce:
forall f m1 m2 x,
(fin_sum f (m1 ++ (x :: m2)) = f x + fin_sum f (m1 ++ m2))%nat.
Proof.
intros f m1. induction m1; intros m2 x.
- simpl. reflexivity.
- simpl.
rewrite IHm1. omega.
Qed.

Lemma mult_reduce_member:
forall m1 m2 x,
mult (m1 ++ x :: m2) x = S (mult (m1 ++ m2) x).
Proof.
intros m1. induction m1; intros m2 x.
- simpl. destruct (nat_dec x x). Focus 2. exfalso. now apply n.
reflexivity.
- simpl.
destruct (nat_dec x a).
+ rewrite IHm1.
destruct (nat_dec a x); reflexivity.
+ destruct (nat_dec a x). omega.
apply IHm1.
Qed.

Lemma mult_reduce_alien:
forall m1 m2 x a,
x <> a ->
mult (m1 ++ x :: m2) a = mult (m1 ++ m2) a.
Proof.
intros m1. induction m1; intros m2 x a' H1.
- simpl.
destruct (nat_dec a' x). Focus 1. exfalso. apply H1. ainv.
destruct (nat_dec x a'); omega.
- simpl.
destruct (nat_dec a' a); rewrite IHm1; auto.
Qed.

Lemma mle_impl_less_equal_fin_sums:
forall f m1 m2,
(mle m1 m2) -> fin_sum f m1 <= fin_sum f m2.
Proof.
intros f m1 m2.
remember (length m1 + length m2)%nat as n.
revert n m1 m2 Heqn.
pose (H1 := @size_recursion).
specialize (H1 nat id (fun n => forall (m1 m2 : multiset),
n = ((| m1 |) + (| m2 |))%nat ->
mle m1 m2 -> fin_sum f m1 <= fin_sum f m2)).
apply H1. clear H1.
intros n IH m1 m2 Heqn H1.
destruct n.
- assert (H2: | m1 | = 0) by omega.
destruct m1. Focus 2. simpl in H2. omega.
simpl. omega.
- remember ((| m1 |)) as n1.
destruct n1.
+ destruct m1. Focus 2. simpl in Heqn1. omega.
simpl. omega.
+ destruct m1 as [|a m1]. Focus 1. simpl in Heqn1. omega.
assert (H11: mle (a :: m1) m2) by auto.
specialize (H1 a). simpl in H1.
destruct (nat_dec a a). Focus 2. exfalso. now apply n0.
clear e.
assert (H2: mult m2 a > 0) by omega.
unfold mult in H2.
apply count_occ_In in H2.
apply in_split in H2.
destruct H2 as [l1 [l2 H3]]. subst m2.
simpl.
rewrite fin_sum_reduce.
assert (H2: fin_sum f m1 <= fin_sum f (l1 ++ l2)).
{
assert (H2: ((| m1 |) + (| l1 |) + (| l2 |))%nat < S n).
{
rewrite Heqn.
rewrite app_length. rewrite Heqn1. simpl. omega.
}
eapply IH.
- exact H2.
- rewrite app_length. omega.
- intros v.
destruct (nat_dec v a).
+ inv e. specialize (H11 a).
rewrite mult_reduce_member in H11.
simpl in H11.
destruct (nat_dec a a). Focus 2. exfalso. now apply n0.
omega.
+ specialize (H11 v). simpl in H11.
destruct (nat_dec v a). exfalso. apply n0. ainv.
rewrite mult_reduce_alien in H11; auto.
destruct (nat_dec a v). exfalso. auto.
auto.
}
omega.
Qed.

(m1 m2: multiset)
(f: nat -> nat):
fin_sum f (m1 ++ m2) = ((fin_sum f m1) + (fin_sum f m2)).
Proof.
induction m1.
- now simpl.
- simpl. rewrite IHm1. omega.
Qed.

Lemma fin_sum_lemma
(p: process)
(n: var)
(sigma: var -> process):
mult (count p.[sigma]) n =
fin_sum (fun i => mult (count (sigma i)) n) (count p).
Proof.
induction p.
- now simpl.
- now simpl.
- simpl. omega.
- simpl.
rewrite union_mult.
rewrite IHp1. rewrite IHp2.