Require Export Nom_Struct_congr.

Inductive howe {V:Set}: binary proc0 → proc V → proc V → Prop :=
| howe_comp : ∀ Rel P Q R, howe Rel P R →
      open_extension Rel R Q → howe Rel P Q
| howe_nil : ∀ Rel, howe Rel PO PO
| howe_var : ∀ Rel x, howe Rel (pr_var x) (pr_var x)
| howe_par : ∀ Rel P Q P' Q', howe Rel P Q → howe Rel P' Q' →
      howe Rel (P // P') (Q // Q')
| howe_inp : ∀ Rel a P Q, @howe (incV V) Rel P Q →
      howe Rel (a ? P) (a ? Q)
| howe_out : ∀ Rel a P Q P' Q', howe Rel P Q → howe Rel P' Q' →
      howe Rel (a!(P) P') (a !(Q) Q')
| howe_nu : ∀ Rel b c P Q, c `notin` fn (nu b, P) →
      howe Rel P Q → howe Rel (nu c, (swap b c P)) (nu b, Q)
.

Inductive howe' {V:Set}: binary proc0 → proc V → proc V → nat → Prop :=
| howe_comp' : ∀ Rel P Q R k, howe' Rel P R k →
      open_extension Rel R Q → howe' Rel P Q (S k)
| howe_nil' : ∀ Rel, howe' Rel PO PO 0
| howe_var' : ∀ Rel x, howe' Rel (pr_var x) (pr_var x) 0
| howe_par' : ∀ Rel P Q P' Q' k k', howe' Rel P Q k → howe' Rel P' Q' k' →
      howe' Rel (P // P') (Q // Q') (S(k+k'))
| howe_inp' : ∀ Rel a P Q k, @howe' (incV V) Rel P Q k →
      howe' Rel (a ? P) (a ? Q) (S k)
| howe_out' : ∀ Rel a P Q P' Q' k k', howe' Rel P Q k → howe' Rel P' Q' k' →
      howe' Rel (a!(P) P') (a!(Q) Q') (S(k+k'))
| howe_nu' : ∀ Rel b c P Q k, c `notin` fn (nu b, P) →
      howe' Rel P Q k → howe' Rel (nu c, (swap b c P)) (nu b, Q) (S k)
.

Hint Constructors howe howe':howe.

Lemma howe_nu_same {V:Set}: ∀ Rel a (P Q: proc V),
    howe Rel P Q → howe Rel (nu a, P) (nu a, Q).
Proof. intros. rewrite <- (swap_id _ a P) at 1; constructor; [simpl; auto | auto].
Qed.

Lemma howe'_nu_same {V:Set}: ∀ Rel a (P Q: proc V) k,
    howe' Rel P Q k → howe' Rel (nu a, P) (nu a, Q) (S k).
Proof. intros. rewrite <- (swap_id _ a P) at 1; constructor; [simpl; auto | auto].
Qed.

Lemma howe_nu_aeq {V:Set} : ∀ b c (P : proc V),
    c `notin` fn (nu b, P) → (nu c, (swap b c P) =A= nu b, P).
Proof. intros. destruct (b==c); simpls; subst; constructor; auto. simpl_swap.
  rewrite swap_sym. reflexivity. Qed.

Hint Resolve howe_nu_same howe'_nu_same:howe.

Lemma howe'_ind_size :
  ∀ Pr : (∀ V : Set, binary proc0 → proc V → proc V → nat → Prop),
   (∀ W (Rel : binary proc0) (P' Q':proc W) n', howe' Rel P' Q' n' →
     (∀ (V : Set) (P Q: proc V) n, howe' Rel P Q n → n < n' →
          Pr V Rel P Q n) → Pr W Rel P' Q' n')
   → ∀ (V : Set) (b : binary proc0) (p p0 : proc V) (n : nat),
      howe' b p p0 n → Pr V b p p0 n.
Proof.
  intros. gen V. induction n using TLC.LibNat.peano_induction; intros.
  apply H; auto.
Qed.


Lemma howe'_implies_howe {V:Set}: ∀ (P Q:proc V) Rel n,
    howe' Rel P Q n → howe Rel P Q.
Proof.
  intros. induction H; eauto with howe.
Qed.

Lemma howe_implies_howe' {V:Set}: ∀ (P Q:proc V) (Rel:binary proc0),
    howe Rel P Q → ∃ n, howe' Rel P Q n.
Proof.
  intros.
  induction H; try (destruct IHhowe as [n']);
    try (destruct IHhowe2 as [n2]); try (destruct IHhowe1 as [n1]);
    eexists; eauto with howe.
Qed.

Lemma howe_refl {V:Set}: ∀ Rel (P:proc V), howe Rel P P.
Proof. intros_all. induction P; eauto with howe. Qed.

Lemma howe'_refl {V:Set}: ∀ Rel (P:proc V), ∃ k, howe' Rel P P k.
Proof. intros_all. apply howe_implies_howe'. apply howe_refl. Qed.

Hint Resolve howe_refl howe'_refl :howe.

Lemma howe_genNu : ∀ V Rel L P Q,
    howe Rel P Q → howe Rel (@genNu V L P) (genNu L Q).
Proof. intros V Rel L. induction L; intros; simpl; auto with howe. Qed.


Lemma howe'_swap {V:Set} : ∀ Rel (P Q : proc V) k b c,
    mod_aeq Rel → mod_swap Rel → howe' Rel P Q k →
    howe' Rel (swap b c P) (swap b c Q) k.
Proof. intros. induction H1; simpl; auto with howe.
  - eapply howe_comp'. eauto with howe. apply oe_swap; auto.
  - rewrite swap_equivariance. constructor; auto. simpl_swap.
Qed.

Lemma mod_aeq_howe {V:Set} : ∀ Rel,
    refl Rel → mod_aeq Rel → mod_aeq (@howe V Rel).
Proof. introv ref maeq. intros_all. gen P' Q'.
  induction H; intros; simpl;
  try solve [inversion H0; inversion H1; auto with howe];
  try solve [inversion H1; inversion H2; auto with howe];
  forwards maeqoe: @mod_aeq_oe V Rel maeq.
  - apply howe_comp with R. apply IHhowe; auto; reflexivity.
    eapply maeqoe; eauto; reflexivity.
  - rewrite howe_nu_aeq in H1; auto.
    inversion H1; inversion H2; subst; auto with howe.
    + apply howe_comp with (nu b, (swap b c0 Q1)). auto with howe.
      eapply maeqoe; eauto. 2:constructor; eauto. apply oe_refl; auto.
    + rewrite <- (swap_invo _ b c0 Q0). constructor; auto. simpl; simpl_swap.
    + rewrite <- (swap_invo _ b c0 Q0). apply howe_comp with (nu b, (swap b c1 Q1)).
      constructor; auto. simpl; simpl_swap. eapply maeqoe. 3: reflexivity.
      apply oe_refl; auto. symmetry. constructor; auto. reflexivity.
Qed.

Lemma mod_aeq_left_howe' {V:Set} : ∀ Rel P Q P' k,
    refl Rel → mod_aeq Rel → howe' Rel P Q k →
    P=A=P' → @howe' V Rel P' Q k.
Proof. introv ref maeq. intros_all. gen P'.
  induction H; intros; simpl;
  try solve [inversion H0; auto with howe];
  try solve [inversion H1; auto with howe];
  forwards maeqoe: @mod_aeq_oe V Rel maeq.
  - apply howe_comp' with R. apply IHhowe'; auto; reflexivity. auto.
  - rewrite howe_nu_aeq in H1; auto. inversion H1; subst; auto with howe.
    rewrite <- (swap_invo _ b c0 Q0). constructor; auto. simpl; simpl_swap.
Qed.

Lemma howe_aeq {V:Set}: ∀ Rel (P Q:proc V),
    refl Rel → mod_aeq Rel → P=A=Q → howe Rel P Q.
Proof. intros. forwards: @mod_aeq_howe V; eauto.
  eapply H2; eauto with howe; reflexivity. Qed.

Lemma howe_oe {V:Set}: ∀ Rel (P Q:proc V),
   open_extension Rel P Q → howe Rel P Q.
Proof. intros. apply howe_comp with P; auto with howe. Qed.

Lemma howe_clos_trans_par {V:Set}: ∀ Rel (P Q P' Q':proc V),
  tclosure (howe Rel) P Q → tclosure (howe Rel) P' Q' →
  tclosure (howe Rel) (P // P')(Q //Q').
Proof.
  intros. gen P' Q'.
  induction H.
  - intros. apply tclosure_trans with (y//P'). apply tclosure_once.
      apply howe_par; auto with howe.
    induction H0. apply tclosure_once. apply howe_par; auto with howe.
    eapply tclosure_trans; eauto.
  - intros. apply tclosure_trans with (y//P'). apply IHtclosure1.
      apply tclosure_once; auto with howe.
    apply IHtclosure2. apply H1.
Qed.

Lemma howe_clos_trans_inp {V:Set}: ∀ Rel (P Q:proc (incV V)) a,
  tclosure (howe Rel) P Q → tclosure (howe Rel) (a ? P)(a ? Q).
Proof.
  intros.
  induction H.
  - apply tclosure_once. auto with howe.
  - eapply tclosure_trans; eauto with howe.
Qed.

Lemma howe_clos_trans_out {V:Set}: ∀ Rel (P Q P' Q':proc V) a,
  tclosure (howe Rel) P Q → tclosure (howe Rel) P' Q' →
  tclosure (howe Rel) (a !(P) P')(a !(Q) Q').
Proof.
  intros. gen P' Q'.
  induction H.
  - intros. apply tclosure_trans with (a!(y) P'). apply tclosure_once.
      apply howe_out; auto with howe.
    induction H0. apply tclosure_once. apply howe_out; auto with howe.
    eapply tclosure_trans; eauto.
  - intros. apply tclosure_trans with (a!(y) P'). apply IHtclosure1.
      apply tclosure_once; auto with howe. auto.
Qed.

Lemma howe_clos_trans_nu_same {V:Set}:
  ∀ (Rel:binary proc0) a (P Q:proc V),
  tclosure (howe Rel) P Q → tclosure (howe Rel) (nu a, P) (nu a, Q).
Proof.
  intros. induction H.
  - apply tclosure_once. auto with howe.
  - eapply tclosure_trans; eauto with howe.
Qed.

Lemma howe_clos_trans_nu {V:Set}:
  ∀ (Rel:binary proc0) b c (P Q:proc V),
    tclosure (howe Rel) P Q → c `notin` fn (nu b, P) →
    tclosure (howe Rel) (nu c, (swap b c P)) (nu b, Q).
Proof. intros. induction H.
  - apply tclosure_once. auto with howe.
  - eapply tclosure_trans; eauto with howe. apply howe_clos_trans_nu_same; auto.
Qed.

Hint Resolve howe_clos_trans_par howe_clos_trans_inp howe_clos_trans_out: howe.
Hint Constructors tclosure:howe.

Lemma howe_sym {V:Set}: ∀ (Rel:binary proc0),
    refl Rel → mod_aeq Rel → sym Rel → sym (tclosure (@howe V Rel)).
Proof.
  intros_all. induction H2.
  - induction H2; auto with howe.
    + eapply tclosure_trans; auto. apply tclosure_once.
      apply howe_oe; auto with howe. apply oe_sym; eauto.
    + eapply tclosure_r. eapply (howe_clos_trans_nu_same); eauto.
      apply howe_aeq; auto. symmetry. apply howe_nu_aeq. auto.
  - eapply tclosure_trans; eauto.
Qed.

Lemma howe_mapV {V W:Set}: ∀ Rel (P Q:proc V) (f:V→W),
    mod_aeq Rel → howe Rel P Q → howe Rel (mapV f P)(mapV f Q).
Proof.
  intros. gen W.
  induction H0; intros; simpl; try rewrite <- swap_mapV; auto with howe.
  eapply howe_comp; eauto. apply oe_mapV; auto.
  constructor; auto. simpl; simpl_swap.
Qed.

Hint Resolve howe_mapV:howe.

Lemma howe'_bind {V W:Set}: ∀ Rel (P Q:proc V) (f g:V → proc W) N n,
    (∀ x, fn (f x) [<=] N) → (∀ x, fn (g x) [<=] N) →
    fn P [<=] N → fn Q [<=] N → refl Rel → mod_aeq Rel → mod_swap Rel →
    howe' Rel P Q n → (∀ x, ∃ k', howe' Rel (f x) (g x) k') →
    ∃ k, howe' Rel (bind f N P) (bind g N Q) k.
Proof. introv inf ing inP inQ ref maeq swaprel howePQ howefg. gen W N.
  induction howePQ using howe'_ind_size.
  destruct howePQ; intros; unfold bind; simpl in *; foldbind; auto with howe.
  - forwards: H P R f g (union N (fn R)); eauto; try nat_math; try fsetdec;
    try solve [intro; try rewrite inf; try rewrite ing; fsetdec].
    destruct H1. ∃ (S x). apply howe_comp' with (bind g (union N (fn R)) R).
    eapply mod_aeq_left_howe'; eauto. apply aeq_bind_2; auto.
    intro; rewrite inf. 1-2:fsetdec.
    forwards maeqoe: @mod_aeq_oe maeq; auto.
    eapply maeqoe. 2: reflexivity. apply oe_bind; eauto. 4:apply aeq_bind_2; auto.
      fsetdec. 1,4:rewrite inQ; fsetdec. all:intro; rewrite ing; fsetdec.
  - forwards: H P Q; eauto; try nat_math; try fsetdec.
    forwards: H P' Q'; eauto; try nat_math; try fsetdec.
    destruct H0. destruct H1. ∃ (S x + x0). constructor; auto.
  - forwards: H P Q (liftV f) (liftV g) N; eauto. nat_math.
      1-3: intros [|x]; simpl; simpl_swap; try fsetdec; auto with howe.
      2-3: fsetdec. apply howe_implies_howe'. apply howe_mapV; auto with howe.
      destruct (howefg x). eapply howe'_implies_howe; eauto.
    destruct H0; eexists; constructor; eauto.
  - forwards: H P Q; eauto; try nat_math; try fsetdec.
    forwards: H P' Q'; eauto; try nat_math; try fsetdec.
    destruct H0. destruct H1. ∃ (S x + x0). constructor; auto.
  - destruct atom_fresh. foldbind. enough (∃ k0, howe' Rel ( bind f
      (add x N) (swap c x (swap b c P))) ( bind g (add x N) (swap b x Q)) k0)
      by (destruct H1; ∃ (S x0); auto with howe). simpl_swap in inP.
    rewrite <- swap_fs_notin in inP. 2-3:fsetdec.
    forwards: (@howe'_swap W) b x maeq howePQ; auto.
    forwards: H H1 (add x N); auto; try nat_math; try apply fnsaxp; auto;
      try solve [intro; try rewrite inf; try rewrite ing; fsetdec].
    destruct H2. ∃ (x0). eapply mod_aeq_left_howe'; eauto.
    symmetry. apply aeq_bind_3. apply fnsaxp; auto. rewrite swap_sym.
    symmetry. apply aeq_swap_cut_notin. intuition.
Qed.

Lemma howe_bind {V W:Set}: ∀ Rel (P Q:proc V) (f g:V → proc W) N,
    (∀ x, fn (f x) [<=] N) → (∀ x, fn (g x) [<=] N) →
    fn P [<=] N → fn Q [<=] N → refl Rel → mod_aeq Rel → mod_swap Rel →
    howe Rel P Q → (∀ x, howe Rel (f x) (g x)) →
    howe Rel (bind f N P) (bind g N Q).
Proof.
  intros. apply howe_implies_howe' in H6. destruct H6. forwards: @howe'_bind V.
  exact H. exact H0. exact H1. exact H2. exact H3. exact H4. exact H5. exact H6.
  intros. apply howe_implies_howe'; auto.
  destruct H8. eapply howe'_implies_howe; eauto.
Qed.

Lemma howe_subst {V:Set}: ∀ Rel (P' Q' :proc V) P Q,
    refl Rel → mod_aeq Rel → mod_swap Rel →
    howe Rel P Q → howe Rel P' Q' → howe Rel (subst P P')(subst Q Q').
Proof.
  introv ref maeq swaprel hPQ hPQ'. forwards maeqhowe: @mod_aeq_howe V maeq; auto.
  unfold subst. assert (fn P [<=] union (union (fn P) (fn P'))
    (union (fn Q) (fn Q'))) by fsetdec. assert (fn Q [<=] union (union (fn P)
    (fn P')) (union (fn Q) (fn Q'))) by fsetdec.
  eapply maeqhowe. 2-3:apply aeq_bind_2; eauto; try intros [|x]; simpl; fsetdec.
  apply howe_bind; auto; try intros [|x]; simpl; try fsetdec; auto with howe.
Qed.

Hint Resolve howe_subst howe_bind:howe.