HOcore.Subst

Require Import HOcore.Prelim.

Require Import HOcore.ComplLat
               HOcore.HoCore
               HOcore.Ren.

This file contains lemmas about substitutions as well as substitutivity for transitions and their corresponding inversion lemmas

Substitutivity of transitions


Lemma step_out_substit:
  forall sigma a r p p',
    step_out a r p p' ->
    step_out a r.[sigma] p.[sigma] p'.[sigma].
Proof.
  do 5 intro. intro H1.
  induction H1.
  - apply StOutSend.
  - now apply StOutParL.
  - now apply StOutParR.
Qed.

Lemma step_in_substit:
  forall sigma a p p',
    step_in a p p' ->
  forall p2, p2 = p'.[up sigma] ->
    step_in a p.[sigma] p2.
Proof.
  intros sigma a p p' H1.
  induction H1; intros; subst.
  - apply StInReceive.
  - asimpl.
    replace q.[sigma >> ren (+1)] with q.[sigma].[ren (lift 1)] by now asimpl.
    eapply StInParL; now try apply IHstep_in.
  - asimpl.
    replace p.[sigma >> ren (+1)] with p.[sigma].[ren (lift 1)] by now asimpl.
    eapply StInParR; now try apply IHstep_in.
Qed.

Lemma step_tau_substit:
  forall sigma p p',
    step_tau p p' ->
    step_tau p.[sigma] p'.[sigma].
Proof.
  intros sigma p p' H. induction H; intros; subst; simpl.
  - pose (IH1 := step_out_substit sigma H).
    pose (IH2 := @step_in_substit sigma a q q' H0).
    replace q'.[r .: ids].[sigma] with q'.[up sigma].[r.[sigma] .: ids] by now asimpl.
    eapply StTauSynL.
    + now apply IH1.
    + now apply IH2.
    + reflexivity.
  - subst. simpl.
    pose (IH1 := @step_in_substit sigma a p p' H).
    pose (IH2 := step_out_substit sigma H0).
    replace p'.[r .: ids].[sigma] with p'.[up sigma].[r.[sigma] .: ids] by now asimpl.
    eapply StTauSynR.
    + now apply IH1.
    + now apply IH2.
    + reflexivity.
  - auto.
  - auto.
Qed.

Lemma step_var_cxt_substit_ren:
  forall xi n p p',
    step_var_cxt n p p' ->
    step_var_cxt (xi n) p.[ren xi] p'.[ren (upren xi)].
Proof.
  intros xi n p p' H1.
  induction H1; subst.
  - asimpl. constructor.
  - asimpl.
    assert (H2: step_var_cxt (xi n) (Par p.[ren xi] q.[ren xi])
      (Par p'.[ren (upren xi)] q.[ren xi].[ren (+1)])).
    { eapply StVarCxtParL; eauto. }
    now asimpl in H2.
  - asimpl.
    assert (H2: step_var_cxt (xi n) (Par p.[ren xi] q.[ren xi])
      (Par p.[ren xi].[ren (+1)] q'.[ren (upren xi)])).
    { eapply StVarCxtParR; eauto. }
    now asimpl in H2.
Qed.

Propagation via context


Lemma step_out_propagation_cxt:
  forall sigma p C n a q'' q',
    step_var_cxt n p C ->
    step_out a q'' (sigma n) q' ->
    step_out a q'' p.[sigma] C.[q' .: sigma].
Proof.
  intros sigma p C n a q'' q' H1 H2.
  induction H1; subst; asimpl; auto.
Qed.

Lemma step_in_propagation_cxt:
  forall sigma p C n a q',
    step_var_cxt n p C ->
    step_in a (sigma n) q' ->
    step_in a p.[sigma] C.[q' .: (sigma >> (ren (+1)))].
Proof.
  intros sigma p C n a q' H1 H2.
  induction H1; subst; auto.
  - asimpl. eapply StInParL.
    + now apply IHstep_var_cxt.
    + now asimpl.
  - asimpl. eapply StInParR.
    + now apply IHstep_var_cxt.
    + now asimpl.
Qed.

Lemma step_tau_propagation_cxt:
  forall sigma p C n q',
    step_var_cxt n p C ->
    step_tau (sigma n) q' ->
    step_tau p.[sigma] C.[q' .: sigma].
Proof.
  intros sigma p C n q' H1 H2.
  induction H1; subst; auto.
  - asimpl. apply StTauParL. now apply IHstep_var_cxt.
  - asimpl. apply StTauParR. now apply IHstep_var_cxt.
Qed.

Lemma context_fill_step_var_cxt:
  forall sigma p C n n' q',
    step_var_cxt n p C ->
    step_var_cxt n' (sigma n) q' ->
    step_var_cxt n' p.[sigma] C.[q' .: (sigma >> (ren (+1)))].
Proof.
  intros sigma p C n n' q' H1 H2.
  induction H1; subst; auto.
  - asimpl. eapply StVarCxtParL.
    + now apply IHstep_var_cxt.
    + now asimpl.
  - asimpl. eapply StVarCxtParR.
    + now apply IHstep_var_cxt.
    + now asimpl.
Qed.

Inversion lemmas for transitions of substituted processes


Lemma step_out_inv_subst:
  forall sigma p q r a,
    step_out a r p.[sigma] q ->
  (exists q' r',
     step_out a r' p q' /\
     r = r'.[sigma] /\
     q = q'.[sigma]
  ) \/
  (exists n s C,
     step_out a r (sigma n) s /\
     step_var_cxt n p C /\
     q = C.[s .: sigma]
  ).
Proof.
  intros sigma p.
  induction p; intros q r a H1; ainv.
  - left. repeat eexists; eauto.
  - right. exists v, q, (Var 0). repeat split; auto.
  - inv H1.
    + rename p' into p1'.
      destruct (IHp1 p1' r a H5) as [IHp11 | IHp12].
      * left.
        destruct IHp11 as [p1'' [r' [H6 [H7 H8]]]]. subst.
        do 2 eexists. repeat split; eauto.
      * right.
        destruct IHp12 as [n [s [C [H6 [H7 H8]]]]]. subst.
        exists n, s, (Par C p2.[ren (+1)]).
        {
          repeat split; auto.
          - eapply StVarCxtParL; eauto.
          - now asimpl.
        }
    + (* analog *)
      rename q' into p2'.
      destruct (IHp2 p2' r a H5) as [IHp21 | IHp22].
      * left.
        destruct IHp21 as [p2'' [r' [H6 [H7 H8]]]]. subst.
        do 2 eexists. repeat split; eauto.
      * right.
        destruct IHp22 as [n [s [C [H6 [H7 H8]]]]]. subst.
        exists n, s, (Par p1.[ren (+1)] C).
        {
          repeat split; auto.
          - eapply StVarCxtParR; eauto.
          - now asimpl.
        }
Qed.

Lemma step_in_inv_subst:
  forall sigma p q a,
    step_in a p.[sigma] q ->
  (exists q',
     step_in a p q' /\
     q = q'.[up sigma]
  ) \/
  (exists n s C,
     step_in a (sigma n) s /\
     step_var_cxt n p C /\
     q = C.[s .: (sigma >> (ren (+1)))]
  ).
Proof.
  intros sigma p.
  induction p; intros q a H1; ainv.
  - left. eexists. eauto.
  - right. exists v, q, (Var 0). eauto.
  - inv H1.
    + rename p' into p1'.
      destruct (IHp1 p1' a H3) as [IHp11 | IHp12].
      * left.
        destruct IHp11 as [p1'' [H4 H5]]. subst.
        eexists. repeat split.
          econstructor; eauto.
          now asimpl.
      * right.
        destruct IHp12 as [n [s [C [H4 [H5 H6]]]]]. subst.
        exists n, s, (Par C p2.[ren (+1)]).
        repeat split; auto.
          econstructor; eauto.
          now asimpl.
    + (* analog *)
      rename q' into p2'.
      destruct (IHp2 p2' a H3) as [IHp11 | IHp12].
      * left.
        destruct IHp11 as [p2'' [H4 H5]]. subst.
        eexists. repeat split.
          eapply StInParR. eauto. reflexivity.
          now asimpl.
      * right.
        destruct IHp12 as [n [s [C [H4 [H5 H6]]]]]. subst.
        exists n, s, (Par p1.[ren (+1)] C).
        repeat split; auto.
          eapply StVarCxtParR. eauto. reflexivity.
          now asimpl.
Qed.

Lemma step_var_cxt_inv_subst:
  forall sigma p C v,
    step_var_cxt v p.[sigma] C ->
  exists v' C' s,
    step_var_cxt v' p C' /\
    step_var_cxt v (sigma v') s /\
    C = C'.[s .: (sigma >> (ren (+1)))].
Proof.
  intros sigma p.
  induction p; intros q v' H1; ainv.
  - exists v, (Var 0), q. repeat split; eauto.
  - inv H1.
    + rename p' into p1'.
      destruct (IHp1 p1' v' H3) as [v [C [s [H4 [H5 H6]]]]]. subst.
      exists v, (Par C p2.[ren (+1)]), s. repeat split.
      * econstructor; eauto.
      * auto.
      * now asimpl.
    + (* analog *)
      rename q' into p2'.
      destruct (IHp2 p2' v' H3) as [v [C [s [H4 [H5 H6]]]]]. subst.
      exists v, (Par p1.[ren (+1)] C), s. repeat split.
      * eapply StVarCxtParR; eauto.
      * auto.
      * now asimpl.
Qed.

Substitution Closure


Definition subst_clos:
  relation process -> relation process :=
  fun x => fun p q => exists sigma p' q',
    x p' q' /\
    p = p'.[sigma] /\
    q = q'.[sigma].

(* subst_clos is monotone *)
Global Instance subst_clos_mono: Mono subst_clos.
Proof.
  intros p q x x' [sigma [p' [q' [H1 [H2 H3]]]]] H4. subst.
  exists sigma, p', q'. intuition.
Qed.

(* subst_clos is symmetric *)
Global Instance subst_clos_symmetric:
  SymFun subst_clos.
Proof.
  intros x p q.
  split; intros [sigma [p' [q' [H1 [H2 H3]]]]]; subst;
  now repeat eexists.
Qed.

(* subst_clos is extensive *)
Global Instance subst_clos_ext:
  Ext subst_clos.
Proof.
  intros x p q H1.
  exists ids. repeat eexists; asimpl; eauto.
Qed.