Require Import HOcore.Prelim.

Require Import HOcore.ComplLat
               HOcore.HoCore.

(* Right inverse of (+1) *)
Definition minus_one: var -> process := Nil .: ids.

(* Definition simply through the property xi >>> sigma = ids *)

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

(* inj_ren_clos is symmetric *)
Global Instance inj_ren_clos_symmetric:
  SymFun inj_ren_clos.
Proof.
  intros x p q.
  split; intros [xi [sigma [p' [q' H2]]]]; intuition; subst;
  exists xi, sigma, q', p'; eauto.
Qed.

(* upren operator preserves injectivity *)
Lemma upren_preserv_inj
  (xi: var -> var)
  (sigma: var -> process):
  xi >>> sigma = ids ->
  (upren xi) >>> (up sigma) = ids.
Proof.
  intros H1. asimpl.
  asimpl. rewrite H1. now asimpl.
Qed.

(* Injectively renamed processes can be inverted *)
Lemma inj_ren_inv
  (xi: var -> var)
  (sigma: var -> process):
  xi >>> sigma = ids ->
  forall p q,
    p.[ren xi] = q.[ren xi] ->
    p = q.
Proof.
  intros H1 p q H2.
  assert (H3: p.[ren xi].[sigma] = q.[ren xi].[sigma]).
  {
    now rewrite H2.
  }
  asimpl in H3. rewrite H1 in H3. now asimpl in H3.
Qed.

(* Injectively renamed variables can be inverted *)
Lemma inj_ren_inv_var
  (xi: var -> var)
  (sigma: var -> process):
  xi >>> sigma = ids ->
  forall n1 n2,
    xi n1 = xi n2 ->
    n1 = n2.
Proof.
  intros H1 n1 n2 H2.
  assert (Var n1 = Var n2).
  {
    eapply inj_ren_inv; eauto.
    asimpl. now rewrite H2.
  }
  ainv.
Qed.

(* For a value n, it can be decided whether n is in the image of xi or not *)

Definition decidable_inj_ren
  (xi: var -> var)
  (sigma: var -> process): Prop :=
  xi >>> sigma = ids /\
  (forall n, Coq.Logic.Decidable.decidable (exists n', xi n' = n)).

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

(* decidable_inj_ren_clos is monotone *)
Global Instance decidable_inj_ren_clos_mono: Mono decidable_inj_ren_clos.
Proof.
  intros p q x x' [xi [sigma [p' [q' H2]]]] H3.
  exists xi, sigma, p', q'.
  intuition.
Qed.

(* decidable_inj_ren_clos is symmetric *)
Global Instance decidable_inj_ren_clos_symmetric:
  SymFun decidable_inj_ren_clos.
Proof.
  intros x p q.
  split; intros [xi [sigma [p' [q' H2]]]]; intuition; subst;
  exists xi, sigma, q', p'; eauto.
Qed.

(* decidable_inj_ren_clos is extensive *)
Global Instance decidable_inj_ren_clos_ext:
  Ext decidable_inj_ren_clos.
Proof.
  intros x p q H1.
  exists id, ids, p, q.
  repeat split; asimpl; eauto. intro. left. eauto.
Qed.
Hint Resolve decidable_inj_ren_clos_ext.

(* id is a decidable injective renaming *)
Lemma id_decidable_inj_ren:
  decidable_inj_ren id ids.
Proof.
  split.
  - reflexivity.
  - intro. left. eexists. reflexivity.
Qed.

(* (+1) is a decidable injective renaming *)

Lemma shift_decidable_inj_ren:
  decidable_inj_ren (+1) minus_one.
Proof.
  split; auto.
  intros n. destruct n.
  - right. intros [n' H1]. simpl in H1. omega.
  - left. exists n. reflexivity.
Qed.

(* upren preserves deciadable injective renaming *)
Lemma upren_preserv_dec_inj_ren
  (xi: var -> var)
  (sigma: var -> process):
  decidable_inj_ren xi sigma ->
  decidable_inj_ren (upren xi) (up sigma).
Proof.
  intros [H1 H2]. split.
  - now apply upren_preserv_inj.
  - intros [| n].
    + left. now exists 0.
    + destruct (H2 n) as [[n' H3] | H3].
      * left. exists (S n'). simpl. now rewrite H3.
      * right. intros [n' H4].
        { destruct n'.
        - simpl in H4. omega.
        - simpl in H4. apply H3. eexists. eauto.
        }
Qed.

Definition bij_ren (xi xi': var -> var): Prop :=
  xi >>> xi' = id /\
  xi' >>> xi = id.

Definition bij_ren_clos:
  relation process -> relation process :=
  fun x => fun p q => exists xi xi' p' q',
    bij_ren xi xi' /\
    x p' q' /\
    p = p'.[ren xi] /\
    q = q'.[ren xi].

(* bij_ren_clos is monotone *)
Global Instance bij_ren_clos_mono: Mono bij_ren_clos.
Proof.
  intros p q x x' [xi [sigma [p' [q' H2]]]] H3.
  exists xi, sigma, p', q'.
  intuition.
Qed.

(* bij_ren_clos is symmetric *)
Global Instance bij_ren_clos_symmetric:
  SymFun bij_ren_clos.
Proof.
  intros x p q.
  split; intros [xi [sigma [p' [q' H2]]]]; intuition; subst;
  exists xi, sigma, q', p'; eauto.
Qed.

Lemma comp_preserv_bij_ren
  (xi1 xi1' xi2 xi2': var -> var)
  (H1: bij_ren xi1 xi1')
  (H2: bij_ren xi2 xi2'):
  bij_ren (xi1 >>> xi2) (xi2' >>> xi1').
Proof.
  destruct H1 as [H11 H12].
  destruct H2 as [H21 H22].
  split.
  - assert (H3: xi1 >>> (xi2 >>> xi2') >>> xi1' = id).
    { rewrite H21. now asimpl. }
    asimpl in H3. now asimpl.
  - assert (H3: xi2' >>> (xi1' >>> xi1) >>> xi2 = id).
    { rewrite H12. now asimpl. }
    asimpl in H3. now asimpl.
Qed.

(* upren operator preserves injectivity *)
Lemma upren_preserv_bij
  (xi xi': var -> var):
  bij_ren xi xi' ->
  bij_ren (upren xi) (upren xi').
Proof.
  intros [H1 H2].
  split.
  - asimpl. rewrite H1. now asimpl.
  - asimpl. rewrite H2. now asimpl.
Qed.

Lemma bij_ren_is_decidable_inj_ren
  (xi xi': var -> var):
  bij_ren xi xi' ->
  decidable_inj_ren xi (ren xi').
Proof.
  intros [H1 H2].
  split.
  - asimpl. rewrite H1. reflexivity.
  - intros n. left. exists (xi' n).
    change ((xi' >>> xi) n = n). now rewrite H2.
Qed.

Lemma decidable_inj_ren_is_inj_ren
  (xi: var -> var)
  (sigma: var -> process):
  decidable_inj_ren xi sigma ->
  xi >>> sigma = ids.
Proof.
  now intros [H1 _].
Qed.

Lemma decidable_inj_ren_comp_bij_ren_is_decidable_inj_ren
  (xi1: var -> var) (sigma1: var -> process)
  (xi2: var -> var) (xi2': var -> var)
  (H1: decidable_inj_ren xi1 sigma1)
  (H2: bij_ren xi2 xi2'):
  decidable_inj_ren (xi1 >>> xi2) (xi2' >>> sigma1).
Proof.
  destruct H1 as [H11 H12].
  destruct H2 as [H21 H22].
  split.
  - assert (H3: xi1 >>> (xi2 >>> xi2') >>> sigma1 = ids).
    { rewrite H21. now asimpl. }
    asimpl in H3. now asimpl.
  - simpl. intros n.
    specialize (H12 (xi2' n)).
    destruct H12 as [H12 | H12].
    + destruct H12 as [n' H12]. left.
      exists n'. rewrite H12.
      change ((xi2' >>> xi2) n = n). now rewrite H22.
    + right. intros [n' H3].
      apply H12. exists n'. rewrite <- H3.
      change (xi1 n' = (xi2 >>> xi2') (xi1 n')).
      now rewrite H21.
Qed.

(* Renamings are preserved on transitions. This holds for any renamings, not only injective ones. *)

Lemma step_out_preserv_ren
  (xi: var -> var):
  forall p p' p'' a,
    step_out a p'' p.[ren xi] p' ->
  exists p2' p2'',
    p' = p2'.[ren xi] /\
    p'' = p2''.[ren xi] /\
    step_out a p2'' p p2'.
Proof.
  induction p; intros p' p'' a H2.
  - remember (Send c p).[ren xi].
    destruct H2 as [a p'' | |]; ainv.
    exists Nil, p. repeat split; asimpl. constructor.
  - remember (Receive c _).[ren xi]. destruct H2; ainv.
  - ainv.
  - remember (Par p1 p2).[ren xi].
    destruct H2 as [| a3 r3 p3 p3' q3| a3 r3 q3 q3' p3]; ainv.
    + specialize (IHp1 p3' r3 a3 H2).
      destruct IHp1 as [p2' [p2'' [H31 [H32 H33]]]]. subst.
      exists (Par p2' p2). eexists. repeat split. auto.
    + specialize (IHp2 q3' r3 a3 H2).
      destruct IHp2 as [q2' [p2'' [H1 [H31 H32]]]]. subst.
      exists (Par p1 q2'). eexists. repeat split; eauto.
  - ainv.
Qed.

Lemma step_in_preserv_ren
  (xi: var -> var):
  forall p p' a,
    step_in a p.[ren xi] p' ->
  exists p2',
    p' = p2'.[up (ren xi)] /\
    step_in a p p2'.
Proof.
  induction p; intros p' a H2.
  - ainv.
  - inv H2. eauto.
  - ainv.
  - inv H2.
    + destruct (IHp1 p'0 a H3) as [p1' [H51 H52]]. subst.
      exists (Par p1' p2.[ren (+1)]). split.
      * now asimpl.
      * eapply StInParL; eauto.
    + destruct (IHp2 q' a H3) as [q1' [H51 H52]]. subst.
      exists (Par p1.[ren (+1)] q1'). split.
      * now asimpl.
      * eapply StInParR; eauto.
  - ainv.
Qed.

Lemma step_tau_preserv_ren
  (xi: var -> var):
  forall p p',
    step_tau p.[ren xi] p' ->
  exists p2',
    p' = p2'.[ren xi] /\
    step_tau p p2'.
Proof.
  induction p; intros p' H1; ainv.
  inv H1.
  - apply step_out_preserv_ren in H2.
    decompose [and ex] H2; clear H2.
    apply step_in_preserv_ren in H3.
    decompose [and ex] H3; clear H3.
    subst.
    exists (Par x x1.[x0 .: ids]). split.
    + now asimpl.
    + eapply StTauSynL; eauto.
  - apply step_out_preserv_ren in H3.
    decompose [and ex] H3; clear H3.
    apply step_in_preserv_ren in H2.
    decompose [and ex] H2; clear H2.
    subst.
    exists (Par x1.[x0 .: ids] x). split.
    + now asimpl.
    + eapply StTauSynR; eauto.
  - apply IHp1 in H3.
    destruct H3 as [p2' [H31 H32]]; subst.
    exists (Par p2' p2). split; auto.
  - apply IHp2 in H3.
    destruct H3 as [p2' [H31 H32]]; subst.
    exists (Par p1 p2'). split; auto.
Qed.

Lemma step_var_cxt_preserv_ren
  (xi: var -> var):
  forall p p' n,
    step_var_cxt n p.[ren xi] p' ->
  exists n2 p2',
    n = xi n2 /\
    p' = p2'.[ren (upren xi)] /\
    step_var_cxt n2 p p2'.
Proof.
  induction p; intros p' n H2; try ainv.
  - now exists v, (Var 0).
  - inv H2.
    + destruct (IHp1 p'0 n H3) as [n2 [p2' [H5 [H6 H7]]]]. subst.
      exists n2, (Par p2' p2.[ren (+1)]).
      repeat split; auto.
      * now asimpl.
      * econstructor; eauto.
    + destruct (IHp2 q' n H3) as [n2 [q2' [H5 [H6 H7]]]]. subst.
      exists n2, (Par p1.[ren (+1)] q2').
      repeat split; auto.
      * now asimpl.
      * eapply StVarCxtParR; eauto.
Qed.