Require Import HOcore.Prelim.

Require Import HOcore.ComplLat
               HOcore.HoCore
               HOcore.Bis
               HOcore.IoCxtBis.

Lemma step_var_rem_impl_step_var_cxt
  (p p': process)
  (v: var):
  step_var_rem v p p' ->
  exists C,
    step_var_cxt v p C /\
    p' = C.[Nil/].
Proof.
  intros H1. induction H1.
  - exists (Var 0). split; constructor.
  - decompose [ex and] IHstep_var_rem. subst.
    eexists. split; eauto. now asimpl.
   (* analog *)
  - decompose [ex and] IHstep_var_rem. subst.
    eexists. split; eauto. now asimpl.
Qed.

Lemma step_var_cxt_impl_step_var_rem
  (p C: process)
  (v: var):
  step_var_cxt v p C ->
  step_var_rem v p C.[Nil/].
Proof.
  intros H1. induction H1; subst.
  - constructor.
  - simpl. econstructor.
    + eauto.
    + now asimpl.
    (* analog *)
  - simpl. eapply StVarRemParR.
    + eauto.
    + now asimpl.
Qed.

Lemma nu_of_io_cxt_bis_f_is_closed_under_s_var_rem:
  postfp s_var_rem (nu s_io_cxt_sym).
Proof.
  intros p q [x [H11 H12]].
  intros v p' H2.
  destruct (step_var_rem_impl_step_var_cxt H2) as [C [H31 H32]].
  subst.
  destruct (H11 p q H12) as [[_ H42] _].
  specialize (H42 v C H31).
  destruct H42 as [C' [H42 H43]].
  exists C'.[Nil/]. split.
  - now apply step_var_cxt_impl_step_var_rem.
  - eapply s_io_cxt_sym_substit.
    eexists. exists C, C'. split; try split; try reflexivity.
    exists x. split; auto.
Qed.

Lemma io_cxt_bis_subset_io_rem_bis:
  nu s_io_cxt_sym <2= nu s_io_rem_sym.
Proof.
  intros p q [x [H1 H2]].
  exists (nu s_io_cxt_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_io_cxt_bis_f_is_closed_under_s_var_rem.
        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_rem_mono.
        - apply nu_of_io_cxt_bis_f_is_closed_under_s_var_rem.
          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.