Require Import HOcore.Prelim.

Require Import HOcore.HoCore
                HOcore.Ren.

(* 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.

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.
        contradiction.
     * destruct (nat_dec v n). exfalso. auto.
       destruct (nat_dec (xi v) (xi n)). exfalso. auto. auto.
  - do 2 rewrite union_mult. omega.
Qed.

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.

Lemma fin_sum_add
  (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.
    rewrite fin_sum_add. reflexivity.
  - now simpl.
Qed.