Require Import HOcore.Prelim.

Require Import HOcore.ComplLat
               HOcore.HoCore
               HOcore.Multiset
               HOcore.Bis
               HOcore.IoMultiBis.

Lemma unguarded_var_then_nil_step
  (n: nat)
  (p: process):
  1 <= mult (count p) n ->
  exists p',
    step_var_rem n p p'.
Proof.
  intros H1. induction p; try (cbv in H1; omega).
  - destruct (nat_dec n v).
    + ainv. exists Nil. constructor.
    + cbn in H1. destruct (nat_dec v n); try contradiction; omega.
  - simpl in H1.
    rewrite union_mult in H1.
    remember (mult (count p1) n) as z.
    destruct z.
    + simpl in H1.
      specialize (IHp2 H1). destruct IHp2 as [p' H3].
      eexists. eapply StVarRemParR; eauto.
    + assert (1 <= S z) by omega.
      specialize (IHp1 H). destruct IHp1 as [p' H3].
      exists (Par p' p2).
      eapply StVarRemParL; eauto.
Qed.

Lemma nil_step_then_unguarded_var
  (n: nat)
  (p p': process):
  step_var_rem n p p' ->
  1 <= mult (count p) n.
Proof.
  induction 1.
  - simpl. destruct (nat_dec n n); try omega; intuition.
  - simpl. rewrite union_mult. omega.
  - simpl. rewrite union_mult. omega.
Qed.

Lemma step_var_rem_decreases_var_occurrence
  (p p': process)
  (v: var):
  step_var_rem v p p' ->
  S (mult (count p') v) =
  mult (count p) v.
Proof.
  induction 1; subst.
  - simpl. destruct (nat_dec n n); try omega.
  - simpl. do 2 rewrite union_mult. omega.
  - simpl. do 2 rewrite union_mult. omega.
Qed.

Lemma nu_of_s_io_rem_sym_is_closed_under_s_var_multi:
  postfp s_var_multi (nu s_io_rem_sym).
Proof.
  intros p q H1.
  unfold s_var_multi. intros v.
  remember (mult (count p) v + mult (count q) v) as n.
  revert n p q Heqn H1.
  pose (H1 := @size_recursion).
  specialize (H1 nat id (fun n => forall (p q : process),
   n = (mult (count p) v + mult (count q) v) ->
   nu s_io_rem_sym p q -> (mult (count p) v) <= (mult (count q) v))).
  apply H1. clear H1.
  intros n IH p q Heqn [x [H41 H42]].
  (* now begins the induction step *)
  assert (H3: 0 = mult (count p) v \/ 1 <= mult (count p) v) by omega.
  destruct H3 as [H3 | H3].
  - omega.
  - destruct (unguarded_var_then_nil_step H3) as [p' H5].
    destruct (H41 p q H42) as [H81 H82].
    destruct H81 as [_ H81].
    destruct (H81 v p' H5) as [q' [H61 H62]].
    (* it must hold n > 0 *)
    assert (H611: step_var_rem v q q') by auto.
    apply nil_step_then_unguarded_var in H61.
    destruct n. Focus 1. omega.
    (* now use IH *)
    apply step_var_rem_decreases_var_occurrence in H5.
    apply step_var_rem_decreases_var_occurrence in H611.
    rewrite <- H5. rewrite <- H611.
    assert (mult (count p') v <= mult (count q') v).
    {
      destruct n; try omega.
      specialize (IH n).
      apply IH.
      - simpl. omega.
      - omega.
      - exists x. split; auto.
    }
    omega.
Qed.

Lemma io_rem_bis_subset_io_multi_bis:
  nu s_io_rem_sym <2= nu s_io_multi_sym.
Proof.
  intros p q [x [H1 H2]].
  exists (nu s_io_rem_sym). split.
  - clear H2 p q.
    intros p q [x' [H21 H22]].
    destruct (H21 p q H22) as [[[H31 H32] H33] [[H34 H365] H66]].
    split.
    + repeat split.
      * eapply s_ho_out_mono; eauto.
        repeat intro. exists x'; auto.
      * eapply s_ho_in_mono; eauto.
        repeat intro. exists x'; auto.
      * apply nu_of_s_io_rem_sym_is_closed_under_s_var_multi.
        exists x'. split; auto.
    + repeat split.
      * eapply s_ho_out_mono; eauto.
        repeat intro. exists x'; auto.
      * eapply s_ho_in_mono; eauto.
        repeat intro. exists x'; auto.
      * { eapply s_var_multi_mono.
        - apply nu_of_s_io_rem_sym_is_closed_under_s_var_multi.
          exists (transp x'). split; auto.
          repeat intro. apply symmetrize_fun_correct.
          hnf. split; now apply H21.
        - repeat intro.
          apply sym_f_impl_sym_nu; auto.
          apply symmetrize_fun_correct. }
  - exists x. split; auto.
Qed.