Require Export Struct_congr.

Inductive howe {V:Set}: binary proc0 → proc V → proc V → Prop :=
| howe_comp : ∀ Rel P Q R, is_proc Q → 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:var) P Q, @howe (incV V) Rel P Q → howe Rel (a ? P) (a ? Q)
| howe_out : ∀ Rel (a:var) P Q P' Q', howe Rel P Q → howe Rel P' Q' → howe Rel (a!(P) P') (a !(Q) Q')
| howe_nu : ∀ L Rel P Q, (∀ x, x \notin L → howe Rel (open 0 x P) (open 0 x Q))
                              → howe Rel (nu P) (nu Q)
.

Inductive howe' {V:Set}: binary proc0 → proc V → proc V → nat → Prop :=
| howe_comp' : ∀ (Rel:binary proc0) P Q R k, is_proc Q → 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:var) P Q k, @howe' (incV V) Rel P Q k → howe' Rel (a ? P) (a ? Q) (S k)
| howe_out' : ∀ Rel (a:var) 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' : ∀ L Rel P Q k, (∀ x, x \notin L → howe' Rel (open 0 x P) (open 0 x Q) k)
                                 → howe' Rel (nu P) (nu Q) (S k)
.

Hint Constructors howe howe':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. intros. apply H0; auto. TLC.LibNat.nat_math.
Qed.

Lemma howe'_implies_proc {V:Set} : ∀ Rel (P Q:proc V) n, howe' Rel P Q n → is_proc P ∧ is_proc Q.
Proof.
  intros. induction H; try (destruct IHhowe');
    try (destruct IHhowe'1); try (destruct IHhowe'2); split; eauto with hopi.
  - eapply proc_nu; eauto. apply H0.
  - eapply proc_nu; eauto. apply H0.
Qed.

Hint Extern 1 (is_proc ?P) ⇒
  match goal with
  | H: howe' _ P _ _ |- _ ⇒ forwards: @howe'_implies_proc H; intuition
  | H: howe' _ _ P _ |- _ ⇒ forwards: @howe'_implies_proc H; intuition
  end : howe.

Lemma howe'_rename {V:Set}: ∀ (Rel:binary proc0),
  (rename_compatible Rel) → ∀ (P Q:proc V) k x n,
   x \notin fn P \u fn Q → is_proc (open k x P) → is_proc (open k x Q)
  → (howe' Rel) (open k x P) (open k x Q) n →
    ∀ y, y \notin fn P \u fn Q → (howe' Rel) (open k y P) (open k y Q) n.
Proof.
  intros_all. remember (open k x P) as P'. remember (open k x Q) as Q'.
  gen x y k. induction H2 using howe'_ind_size; intros.
  destruct H2.
    + subst.
      destruct (classic (x=y)).
      subst. apply howe_comp' with R; auto.
      assert (∀ y (P:proc W), is_proc (open k x P) → open k x P = open 0 y (open k x P)).
        intros. rewrite (is_proc_open _ 0); auto.
      rewrite× (H8 y P) in H5. rewrite× (H8 y Q) in H6.
      forwards: @decomp_proc R 0 y; auto with howe. destruct H9 as [Ry [HRy [HyRy HRybody]]].
      subst. pick_fresh_V W z.
      forwards*: H H5 y z 0; try solve [autofnF].
        rewrite× <- (H8 y P).
      forwards*: (oe_rename Rel X) H6 z; try solve [autofnF].
        rewrite× <- (H8 y Q).
      rewrite× <- (H8 z P) in H9. rewrite× <- (H8 z Q) in H10.
      forwards*: @decomp_proc (open 0 z Ry) k x. destruct H11 as [Rx [HRx [HxRx HRxbody]]].
      assert (y \notin fn Rx).
        intros_all. forwards*: @fn_open_rev Rx k x. rewrite <- HRx in H12. autofnF.
      rewrite HRx in H9, H10.
      forwards*: H H9 x y k; try solve [autofnF].
      forwards*: (oe_rename Rel X) H10 y; try solve [autofnF].
      apply howe_comp' with (open k y Rx); auto.
        eapply is_proc_rename; eauto.
    + destruct P; inverts HeqP'. destruct Q; inverts HeqQ'; simpl. auto with howe.
    + destruct P; inverts HeqP'. destruct Q; inverts HeqQ'; simpl. auto with howe.
    + destruct P; inverts HeqP'. destruct Q; inverts HeqQ'; simpl.
      inverts H1. inverts H0. apply howe_par'; eauto;
      eapply H; eauto; try omega; autofnF.
    + destruct P; inverts HeqP'. destruct Q; inverts HeqQ'; simpl.
      inverts H0. inverts H1. repeat case_if; inverts H6; try solve [autofnF];
          try solve [subst; apply howe_inp'; eauto; eapply H; eauto; autofnF].
    + destruct P; inverts HeqP'. destruct Q; inverts HeqQ'; simpl.
      inverts H0. inverts H1. repeat case_if; inverts H5; try solve [false; autofnF];
       try solve [subst; apply howe_out'; eauto; eapply H; eauto; autofnF; try omega].
    + destruct P; inverts HeqP'. destruct Q; inverts HeqQ'; simpl. inverts H0; inverts H1.
      apply (howe_nu' (L \u L0 \u L1 \u \{ x} \u \{ y})). intros. rewrite× @open_open.
      replace (open 0 x0 (open (S k) y Q)) with (open (S k) y (open 0 x0 Q))
          by apply× @open_open.
      eapply H; eauto using open_open; autofnF.
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),
    rename_compatible Rel → howe Rel P Q → ∃ n, howe' Rel P Q n.
Proof.
  intros.
  induction H; try solve
    [ try (destruct (IHhowe X) as [n']);
      try (destruct (IHhowe2 X) as [n2]); try (destruct (IHhowe1 X) as [n1]);
      eexists; eauto with howe].
    pick_fresh_V V z. specialize (H0 z). forwards*: H0.
    destruct H1 as [n']. ∃ (S n'). eapply (howe_nu' (L \u fn P \u fn Q)).
    intros. eapply howe'_rename in H1; auto; intuition.
Qed.

Lemma howe_rename {V:Set}: ∀ (Rel:binary proc0),
  (rename_compatible Rel) → @rename_compatible V (howe Rel).
Proof.
  intros_all. forwards: @howe_implies_howe' H2; auto.
  destruct H4 as [n]. forwards*: @howe'_rename H4 y.
  eapply howe'_implies_howe; eauto.
Qed.

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

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

Lemma howe_implies_proc {V:Set}: ∀ Rel (P Q:proc V), howe Rel P Q → is_proc P ∧ is_proc Q.
Proof.
  intros. induction H; try (destruct IHhowe);
    try (destruct IHhowe1); try (destruct IHhowe2); split; eauto with hopi.
  - eapply proc_nu; eauto. apply H0.
  - eapply proc_nu; eauto. apply H0.
Qed.

Lemma tclosure_howe_implies_proc {V:Set} : ∀ Rel (P Q:proc V),
     tclosure (howe Rel) P Q → is_proc P ∧ is_proc Q.
Proof.
  intros. induction H; eauto using (howe_implies_proc); intuition.
Qed.

Hint Resolve howe_refl:howe.

Hint Extern 1 (is_proc ?P) ⇒
  match goal with
  | H: howe _ P _ |- _ ⇒ apply (proj1 (howe_implies_proc _ _ _ H))
  | H: howe _ _ P |- _ ⇒ apply (proj2 (howe_implies_proc _ _ _ H))
  | H: (tclosure (howe _)) P _ |- _ ⇒ forwards*: tclosure_howe_implies_proc H; intuition
  | H: (tclosure (howe _)) _ P |- _ ⇒ forwards*: tclosure_howe_implies_proc H; intuition
  end : howe.

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. apply howe_refl.
    apply tclosure_howe_implies_proc in H0; intuition.
    induction H0. apply tclosure_once. apply howe_par; auto. apply howe_refl; auto.
    apply howe_implies_proc in H; intuition.
    eapply tclosure_trans; eauto.
  - intros. apply tclosure_trans with (y//P'). apply IHtclosure1. apply tclosure_once; apply howe_refl.
    apply tclosure_howe_implies_proc in H1; intuition.
    apply IHtclosure2. apply H1.
Qed.

Lemma howe_clos_trans_inp {V:Set}: ∀ Rel (P Q:proc (incV V)) (a:var),
  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:var),
  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. apply howe_refl.
    apply tclosure_howe_implies_proc in H0; intuition.
    induction H0. apply tclosure_once. apply howe_out; auto. apply howe_refl.
    apply howe_implies_proc in H; intuition.
    eapply tclosure_trans; eauto.
  - intros. apply tclosure_trans with (a!(y) P'). apply IHtclosure1. apply tclosure_once; apply howe_refl.
    apply tclosure_howe_implies_proc in H1; intuition.
    auto.
Qed.

Lemma howe_clos_trans_nu {V:Set}:
   ∀ (Rel:binary proc0) (P Q:proc V), (rename_compatible Rel) →
           (∃ L, ∀ x, x \notin L → tclosure (howe Rel) (open 0 x P) (open 0 x Q)) →
                                  tclosure (howe Rel) (nu P) (nu Q).
Proof.
  intros. destruct H as [L]. pick_fresh_V V x.
  forwards*: H x. remember (open 0 x P) as P'. remember (open 0 x Q) as Q'. clear H.
  gen P Q. induction H0; auto; intros.
  - apply tclosure_once. subst. eapply (howe_nu (L \u fn P \u fn Q)); eauto.
    intros. forwards: @howe_implies_proc H.
    forwards: @howe_rename H x0; eauto; try solve [intuition].
 - subst. forwards: @tclosure_howe_implies_proc H0_. destruct H.
    forwards*: @decomp_proc y 0 x.
    destruct H1 as [R [ H' [H'' ] ] ].
    apply tclosure_trans with (nu R). eapply IHtclosure1; eauto.
    eapply IHtclosure2; eauto.
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),
    rename_compatible Rel → sym Rel → sym (tclosure (@howe V Rel)).
Proof.
  intros_all. induction H0.
  - induction H0; auto with howe.
    + eapply tclosure_trans; auto. apply tclosure_once. apply howe_oe; auto with howe. apply oe_sym; eauto.
    + eapply (howe_clos_trans_nu); eauto.
  - eapply tclosure_trans; eauto.
Qed.

Lemma howe_mapV {V W:Set}: ∀ Rel (P Q:proc V) (f:V→W),
    howe Rel P Q → howe Rel (mapV f P)(mapV f Q).
Proof.
  intros. generalize dependent W. induction H; intros; simpl; auto with howe.
  - eapply howe_comp; eauto; try (apply is_proc_mapV; auto). apply× @oe_mapV.
  - repeat (rewrite mapV_close). apply (howe_nu L). intros.
    repeat (rewrite <- mapV_open). apply× H0.
Qed.

Lemma howe_bind' {V W:Set}: ∀ Rel (P :proc V) (f g:V → proc W), is_proc P →
    ((∀ x, howe Rel (f x) (g x)) → howe Rel (bind f P)(bind g P)).
Proof.
  intros. generalize dependent W. induction H; intros; simpl; auto with howe.
  - apply howe_inp. apply IHis_proc. intros [ |]; simpl; auto with howe. intros; apply howe_mapV; auto.
  - apply (howe_nu L). intros.
    assert (∀ x, is_proc (mapN (fun x1 ⇒ S x1) (f x)) ∧ is_proc (mapN (fun x1 ⇒ S x1) (g x))).
      intros. forwards: @howe_implies_proc (H1 x0). intuition auto with hopi.
    repeat (rewrite <- bind_open); try (intros y; specialize (H3 y); intuition).
    apply× H0. intros. repeat (rewrite is_proc_mapN); forwards*: H1 x0; intuition.
Qed.

Lemma howe_bind {V W:Set}: ∀ Rel (P Q:proc V) (f g:V → proc W),
    howe Rel P Q → (∀ x, howe Rel (f x) (g x)) → howe Rel (bind f P)(bind g Q).
Proof.
  intros. gen W. induction H; intros; simpl; auto with howe.
  - eapply howe_comp with (bind g R).
    apply is_proc_bind; auto with hopi. intros; specialize (H2 x); auto with howe.
    apply IHhowe; eauto. apply oe_bind; auto.
    intros. specialize (H2 v). auto with howe.
  - apply howe_inp. apply IHhowe; auto. intros [ |x]; simpl; auto with howe. apply howe_mapV; auto.
  - apply (howe_nu L). intros.
    repeat (rewrite <- bind_open);
       try solve [intros; rewrite is_proc_mapN; forwards*: H1 y; auto with howe].
    apply× H0. intros.
    repeat (rewrite is_proc_mapN); forwards*: H1 x0; auto with howe.
Qed.

Lemma howe_subst {V:Set}: ∀ Rel (P' Q' :proc V) P Q,
   howe Rel P Q → howe Rel P' Q' → howe Rel (subst P P')(subst Q Q').
Proof.
  intros; apply howe_bind; auto. intros [ | ]; simpl; auto with howe.
Qed.

Lemma howe_open_list {V:Set}: ∀ (Rel:binary proc0) l (P Q:proc V), rename_compatible Rel
    → fresh (fn P) (length l) l → fresh (fn Q) (length l) l →
    (∀ k, k \in bn P → k < length l) → (∀ k, k \in bn Q → k < length l) →
    howe Rel (open_list l P) (open_list l Q) →
    howe Rel (genNu (length l) P) (genNu (length l) Q).
Proof.
  induction l; try solve [simpl; auto].
   intros. repeat (rewrite length_cons in *). simpl. apply (howe_nu (fn P \u fn Q \u from_list l)).
   intros. repeat (rewrite open_genNu).
   simpl in ×. assert (fresh \{} (length l) l) by autofs.
   assert (fresh \{x} (length l) l). apply fresh_single_notin_rev; auto.
   assert (∀ a k, k \in bn (open (length l) a P) → k < length l).
     intros_all. rewrite bn_open in H7. autofs. forwards: H1 k; auto. omega.
   assert (∀ a k, k \in bn (open (length l) a Q) → k < length l).
     intros_all. rewrite bn_open in H8. autofs. forwards: H2 k; auto. omega.
   apply IHl; eauto.
     destruct (classic (length l \in bn P)).
     forwards: @fn_open P (length l) x; auto. destruct H10. rewrite H10; auto.
     apply fresh_union_l; auto. eapply fresh_union_r1; intuition eauto.
     forwards: @fn_open P (length l) x; auto. destruct H10. rewrite H11; auto.
     eapply fresh_union_r1; intuition eauto.
     destruct (classic (length l \in bn Q)).
     forwards: @fn_open Q (length l) x; auto. destruct H10. rewrite H10; auto.
     apply fresh_union_l; auto. eapply fresh_union_r1; intuition eauto.
     forwards: @fn_open Q (length l) x; auto. destruct H10. rewrite H11; auto.
     eapply fresh_union_r1; intuition eauto.
   repeat (rewrite <- open_open_list; try omega).
   forwards: @howe_rename H3 x; auto. intros_all.
   intuition. apply fresh_union_r2 in H11.
   apply fresh_single_notin in H11. autofs. apply fn_open_list_sub in H14. autofs.
   apply fn_open_list_sub in H14. autofs.
   rewrite open_open_list; try omega. apply is_proc_open_list; eauto.
   rewrite open_open_list; try omega. apply is_proc_open_list; eauto.
   intros_all. autofs.
   apply fn_open_list_sub in H14; autofs; notinFalse.
   apply fn_open_list_sub in H14; autofs; notinFalse.
Qed.

Hint Resolve is_proc_bind is_proc_mapV:howe.
Hint Resolve howe_subst howe_mapV howe_bind:howe.