Library HOC07SizeLemmas

Require Import HOC01Defs.
Require Import HOC02BaseLemmas.
Require Import HOC03CanonicalLemmas.
Require Import HOC04DefLTS.
Require Import HOC05WFProcesses.


Lemma sizeX_GV : ∀ X p,
  X \in (GV p) ↔ sizeX X p > 0.
Proof.
  induction p; simpls×.
  split; rewrite× in_empty. nat_math.
  split; introv H ; cases_if. nat_math.
  false n. rewrite¬ in_singleton in H.
  rewrite¬ in_singleton. false. nat_math.
  split; introv H. rewrite in_union in H.
  inversion_clear H.
  asserts IHp1´: (sizeX X p1 > 0). applys¬ IHp1.
  clear IHp1 IHp2 H0. nat_math.
  asserts IHp2´: (sizeX X p2 > 0). applys¬ IHp2.
  clear IHp1 IHp2 H0. nat_math.
  asserts Hs: ((sizeX X p1 > 0) ∨ (sizeX X p2 > 0)).
  clear IHp1 IHp2. nat_math.
  rewrite in_union. elim Hs ; introv H1.
  left. applys¬ IHp1.
  right. applys¬ IHp2.
  split; rewrite× in_empty. nat_math.
Qed.

Lemma sizeX_gfresh : ∀ X p,
  X#p ↔ sizeX X p =0.
Proof.
  introv ; split ; introv H.
  remember (sizeX X p). destruct n. reflexivity.
  assert (Hgv: X \in (GV p)). applys× sizeX_GV. nat_math.
  exfalso. applys¬ H. introv H0. apply sizeX_GV in H0. nat_math.
Qed.

Lemma sizeX_cp: ∀ X p, closed_process p → sizeX X p = 0.
Proof.
  induction p; introv Hcp; simpls~; unfolds in Hcp; simpls.
    apply singleton_absurd in Hcp. false.
    apply union_empty in Hcp. destruct Hcp. rewrite IHp1, IHp2; auto.
Qed.

Lemma sizeX_subst1_cp : ∀ X p q,
  closed_process q → sizeX X ([q // X]p) = 0.
Proof.
  introv H.
  induction p; simpls× ; try cases_if.
    applys¬ sizeX_cp.
    simpl. cases_if¬.
    rewrite IHp1, IHp2; auto.
Qed.

Lemma sizeX_subst2_cp : ∀ X Y p q, X≠Y →
  closed_process q → sizeX X ([q // Y]p) = sizeX X p.
Proof.
  introv Hn Hcp.
  induction p; simpls× ; repeat cases_if.
    applys¬ sizeX_cp.
    rewrite e. simpl. cases_if¬.
    simpl. cases_if¬.
Qed.

Lemma sizeX_subst : ∀ X X´ p q,
  sizeX X q = 0 → X ≠ X´ → sizeX X p = sizeX X ([q // X´]p).
Proof.
  introv Hs Hf.
  induction p; simpls*; repeat cases_if*;
    simpl; cases_if×.
Qed.

Lemma sizeX_in : ∀ a X p (m : wfprocess) f,
  sizeX X m = 0 → {{p--LabIn a->>(AA f)}} → sizeX X p = sizeX X (wfp_inst_Abs f m).
Proof with freshen_up.
  introv H Ht.
  inductions Ht ; simpls×.
  tests : (X0 = X).
    assert (X # [Lvar (f X p) // X]p) by (apply gfresh_in_self_subst; freshen_up).
    assert (X # [m // X]p) by
      (apply gfresh_in_self_subst; freshen_up; rewrite¬ sizeX_gfresh).
  repeat rewrite sizeX_gfresh in *; nat_math.
  repeat rewrite¬ <- sizeX_subst.
  destruct f; destruct ap; inverts x. simpl. erewrite <- IHHt. reflexivity.
  assumption. reflexivity. reflexivity.
  destruct f; destruct aq; inverts x.
  simpl. erewrite <- IHHt. reflexivity.
  assumption. reflexivity. reflexivity.
Qed.

Lemma sizeX_out : ∀ a X p p´ p´´,
  {{p--LabOut a p´´->>(AP p´)}} → sizeX X p = sizeX X p´ + sizeX X p´´.
Proof.
  introv Ht.
  inductions Ht; simpls×.
  destruct ap; inverts x. simpls.
  rewrite IHHt with (p´:=w); auto; nat_math.
  destruct aq; inverts x. simpl.
  rewrite IHHt with (p´:= w); auto; nat_math.
Qed.

Lemma sizeX_remove : ∀ X p p´,
  {{p--LabRem X->>(AP p´)}} → sizeX X p = S (sizeX X p´).
Proof.
  introv Ht.
  inductions Ht; simpls.
  cases_if×.
  destruct ap; inverts x. simpl.
  rewrite (IHHt w); (reflexivity || nat_math).
  destruct aq; inverts x. simpl.
  rewrite (IHHt w); (reflexivity || omega).
Qed.


Lemma sizeX_2_sizeX: ∀ X Y p, X # p →
  sizeX Y p = sizeX X ([(Gvar X) // Y]p).
Proof with freshen_up.
  induction p; introv Hf; simpls; repeat cases_if~; simpls*; try cases_if×.
    rewrite e in Hf. rewrite gfresh_gvar in Hf. false.
    rewrite gfresh_par_iff in Hf; inverts Hf.
    specializes IHp1 H. specializes IHp2 H0. nat_math.
Qed.


Lemma sizeCh_CHS: ∀ p, (∃ m, sizeCh m p > 0) ↔ CHS p ≠ \{}.
Proof.
  split; introv H.
    destruct H as (m & Hs). induction p; simpls.
      introv H. apply union_empty in H. destruct H. apply singleton_absurd in H. apply H.
      introv H. apply union_empty in H. destruct H. apply singleton_absurd in H. apply H.
      nat_math.
      nat_math.
      assert (sizeCh m p1 > 0 ∨ sizeCh m p2 > 0).
        nat_math.
      destruct H; apply union_not_empty.
        left. apply¬ IHp1.
        right. apply¬ IHp2.
      nat_math.
    induction p; simpls.
      ∃ c. cases_if. nat_math.
      ∃ c. cases_if. nat_math.
      false¬ H.
      false¬ H.
      apply union_not_empty in H. destruct H.
        destruct (IHp1 H) as (m & Hsize). ∃ m. nat_math.
        destruct (IHp2 H) as (m & Hsize). ∃ m. nat_math.
      false¬ H.
Qed.

Lemma sizeCh_cfresh: ∀ m p, m###p ↔ sizeCh m p = 0.
Proof.
  introv ; induction p; split ; introv H; simpls~; try cases_if; unfolds fresh_chan; simpls¬.
    rewrite notin_union in H. rewrite notin_singleton in H. destruct H. congruence.
    rewrite notin_union in H. applys× IHp.
    rewrite notin_union. rewrite notin_singleton. split×.
    rewrite notin_union in H. rewrite notin_singleton in H. destruct H. congruence.
    rewrite notin_union in H. applys× IHp.
    rewrite notin_union. rewrite notin_singleton. split×.
    rewrite notin_union in H. intuition.
    rewrite notin_union. intuition.
Qed.

Lemma sizeCh_neq: ∀ m n p, sizeCh m p ≠ sizeCh n p → m ≠ n.
Proof.
  introv H. induction p; simpls~; repeat cases_if~; try congruence.
Qed.

Lemma sizeCh_in_nfr: ∀ a p f, {{p--LabIn a->>(AA f)}} → sizeCh a p > 0.
Proof.
  introv Ht. inductions Ht; simpl.
    cases_if. nat_math.
    destruct ap; inverts x.
     specializes IHHt. reflexivity. nat_math.
    destruct aq; inverts x.
     specializes IHHt. reflexivity. nat_math.
Qed.

Lemma sizeCh_out_nfr: ∀ a p p´ p´´, {{p--LabOut a p´´->>(AP p´)}} → sizeCh a p > 0.
Proof.
  introv Ht. inductions Ht; simpl.
    cases_if. nat_math.
    destruct ap; inverts x.
     specializes IHHt. reflexivity. nat_math.
    destruct aq; inverts x.
     specializes IHHt. reflexivity. nat_math.
Qed.

Lemma sizeCh_subst: ∀ m X p q, sizeCh m q = 0 →
  sizeCh m p = sizeCh m ([q // X]p).
Proof.
  introv. induction p; simpls~; repeat cases_if; simpls¬.
Qed.

Lemma sizeCh_in_neq : ∀ a m (p q : wfprocess) f, a ≠ m →
  sizeCh m q = 0 → {{p--LabIn a->>(AA f)}} → sizeCh m p = sizeCh m (wfp_inst_Abs f q).
Proof.
  introv Hneq Hs Ht. inductions Ht.
    simpl. cases_if. repeat rewrite× <- sizeCh_subst.
    destruct ap; inverts x.
     simpl. rewrite¬ (IHHt a a0).
    destruct aq; inverts x.
     simpl. rewrite¬ (IHHt a a0).
Qed.

Lemma sizeCh_in_eq : ∀ m (p q : wfprocess) f,
  sizeCh m q = 0 → {{p--LabIn m->>(AA f)}} → sizeCh m p = sizeCh m (wfp_inst_Abs f q) + 1.
Proof.
  introv Hs Ht. inductions Ht.
    simpl. cases_if. repeat rewrite¬ <- sizeCh_subst. nat_math.
    destruct ap; inverts x.
     simpl. rewrite¬ (IHHt m a). nat_math.
    destruct aq; inverts x.
     simpl. rewrite¬ (IHHt m a). nat_math.
Qed.

Lemma sizeCh_out_neq : ∀ a m p p´ p´´, a ≠ m →
  {{p--LabOut a p´´->>(AP p´)}} → sizeCh m p = sizeCh m p´ + sizeCh m p´´.
Proof.
  introv Hneq Ht. inductions Ht.
    simpl. cases_if¬.
    destruct ap; inverts x.
     simpl. rewrite¬ (IHHt w); simpl; nat_math.
    destruct aq; inverts x.
     simpl. rewrite¬ (IHHt w); simpl; nat_math.
Qed.

Lemma sizeCh_out_eq : ∀ m p p´ p´´,
  {{p--LabOut m p´´->>(AP p´)}} → sizeCh m p = sizeCh m p´ + sizeCh m p´´ + 1.
Proof.
  introv Ht. inductions Ht.
    simpl. cases_if¬. nat_math.
    destruct ap; inverts x.
     simpl. rewrite¬ (IHHt w); simpl; nat_math.
    destruct aq; inverts x.
     simpl. rewrite¬ (IHHt w); simpl; nat_math.
Qed.

Lemma sizeX_Ch: ∀ m X p, m###p → sizeX X p = sizeCh m ([Send m Nil//X]p).
Proof with freshen_up.
  inductions p; introv Hf; simpls¬...
    rewrite cfresh_send in Hf. destruct Hf. cases_if¬.
    rewrite cfresh_receive in Hf. destruct Hf. cases_if¬.
    repeat cases_if. simpl. cases_if¬.
    simpls¬.
Qed.


Lemma size_swap : ∀ X X´ p,
  (size ({{[X,X´]}}p)) = (size p).
Proof.
  induction p; simpls×.
Qed.

Lemma size_in : ∀ a (p m : wfprocess) f,
  size m = 1 → {{p--LabIn a->>(AA f)}} → size p = S (size (wfp_inst_Abs f m)).
Proof.
  introv H Ht.
  inductions Ht; simpls×. repeat erewrite× size_subst.
  destruct f; destruct ap; inverts x. simpl. erewrite× IHHt.
  destruct f; destruct aq; inverts x. simpl.
  erewrite IHHt with (f0:=f); auto; nat_math.
Qed.

Lemma size_out : ∀ a p p´ p´´,
  {{p--LabOut a p´´->>(AP p´)}} → size p = size p´ + S (size p´´).
Proof.
  introv Ht.
  inductions Ht; simpls×.
  destruct ap; inverts x. simpl.
  rewrite IHHt with (p´:=w). nat_math.
  reflexivity.
  destruct aq; inverts x. simpl.
  rewrite IHHt with (p´:=w). omega.
  reflexivity.
Qed.

Lemma size_remove : ∀ X p p´,
  {{p--LabRem X->>(AP p´)}} → size p = S (size p´).
Proof.
  introv Ht.
  inductions Ht ; simpls×.
  destruct ap; inverts x. simpl.
  rewrite× (IHHt w).
  destruct aq; inverts x. simpl.
  rewrite× (IHHt w).
Qed.


Lemma sizeP_swap : ∀ X X´ p,
  (sizeP ({{[X,X´]}}p)) = (sizeP p).
Proof.
  induction p; simpls×.
Qed.

Lemma sizeP_in : ∀ a (p m : wfprocess) f,
  sizeP m = 1 → {{p--LabIn a->>(AA f)}} → sizeP p = sizeP (wfp_inst_Abs f m) + 1.
Proof.
  introv H Ht.
  inductions Ht; simpls¬. repeat rewrite¬ sizeP_subst.
  destruct f; destruct ap; inverts x.
    simpl. erewrite× IHHt. nat_math.
  destruct f; destruct aq; inverts x.
    simpl. erewrite× IHHt. nat_math.
Qed.

Lemma sizeP_out : ∀ a p p´ p´´,
  {{p--LabOut a p´´->>(AP p´)}} → sizeP p = sizeP p´ + sizeP p´´ + 1.
Proof.
  introv Ht.
  inductions Ht; simpls¬.
  destruct ap; inverts x.
    simpl. erewrite× IHHt. nat_math.
  destruct aq; inverts x.
    simpl. erewrite× IHHt. nat_math.
Qed.

Lemma sizeP_remove : ∀ X p p´,
  {{p--LabRem X->>(AP p´)}} → sizeP p = S (sizeP p´).
Proof.
  introv Ht.
  inductions Ht ; simpls×.
  destruct ap; inverts x. simpl.
  rewrite× (IHHt w).
  destruct aq; inverts x. simpl.
  rewrite× (IHHt w).
Qed.


Lemma wfp_size_send : ∀ a p, wfp_size (wfp_Send a p) = S (wfp_size p).
Proof.
  solve_wfp_size.
Qed.

Lemma wfp_size_abs : ∀ a X p, wfp_size (wfp_Abs a X p) = S (wfp_size p).
Proof.
  intros. unfolds wfp_size. simpls. rewrite¬ size_subst.
Qed.

Lemma wfp_size_gvar : ∀ X, wfp_size (wfp_Gvar X) = 1.
Proof.
  solve_wfp_size.
Qed.

Lemma wfp_size_par : ∀ p q, wfp_size (wfp_Par p q) = S (wfp_size p + wfp_size q).
Proof.
  solve_wfp_size.
Qed.

Lemma wfp_size_nil : wfp_size (wfp_Nil) = 0.
Proof.
  solve_wfp_size.
Qed.

Ltac simpl_wfp_size := repeat
 (repeat rewrite wfp_size_send in *;
  repeat rewrite wfp_size_abs in *;
  repeat rewrite wfp_size_gvar in *;
  repeat rewrite wfp_size_par in *;
  repeat rewrite wfp_size_nil in *).

Lemma wfp_sizeP_send : ∀ a p, wfp_sizeP (wfp_Send a p) = S (wfp_sizeP p).
Proof.
  solve_wfp_sizeP.
Qed.

Lemma wfp_sizeP_abs : ∀ a X p, wfp_sizeP (wfp_Abs a X p) = S (wfp_sizeP p).
Proof.
  intros. unfolds wfp_sizeP. simpls. rewrite¬ sizeP_subst. nat_math.
Qed.

Lemma wfp_sizeP_gvar : ∀ X, wfp_sizeP (wfp_Gvar X) = 1.
Proof.
  solve_wfp_sizeP.
Qed.

Lemma wfp_sizeP_par : ∀ p q, wfp_sizeP (wfp_Par p q) = wfp_sizeP p + wfp_sizeP q.
Proof.
  solve_wfp_sizeP.
Qed.

Lemma wfp_sizeP_nil : wfp_sizeP (wfp_Nil) = 0.
Proof.
  solve_wfp_sizeP.
Qed.

Ltac simpl_wfp_sizeP := repeat
 (repeat rewrite wfp_sizeP_send in *;
  repeat rewrite wfp_sizeP_abs in *;
  repeat rewrite wfp_sizeP_gvar in *;
  repeat rewrite wfp_sizeP_par in *;
  repeat rewrite wfp_sizeP_nil in *).

Ltac simpl_sizes := repeat (simpl_wfp_size; simpl_wfp_sizeP).