Require Export 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 P Q L, (∀ a, ¬In a L → notin_ho a P → notin_ho a Q →
                               howe Rel (P a)(Q a)) → 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, 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 P Q k L, (∀ a, ¬In a L → notin_ho a P → notin_ho a Q →
                               howe' Rel (P a)(Q a) 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.
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'_rename {V:Set}: ∀ (Rel:binary proc0),
  (rename_compatible Rel) → ∀ (P Q:name → proc V) a n,
  notin_ho a P → notin_ho a Q → howe' Rel (P a)(Q a) n →
  ∀ b, notin_ho b P → notin_ho b Q → howe' Rel (P b)(Q b) n.
Proof.
  intros. remember (P a) as Pa. remember (Q a) as Qa.
  gen P Q a b. induction H1 using howe'_ind_size; intros;
  inverts H1; subst; try solve [exp_ext a; simpl; auto with howe].
  + destruct (dec_name a b); subst; eauto with howe.
    all_exp a. fresh_lp (a::b::nil) ((nu P) // (nu Q) // nu R0).
    ho_exp b R0. assert (notin_ho a (R1 x)).
      intros_all. forwards*: H7 b0.
      change (notin a ((fun x ⇒ R1 x b0) x)).
      eapply notin_rename; eauto.
    assert (notin_ho x (fun x0 : name ⇒ R1 x0 a)).
       intros_all. forwards*: H11 b0.
       change (notin x ((fun b0 ⇒ R1 b0 a) b0)).
       eapply notin_rename; eauto.
    apply howe_comp' with (R1 x b).
    forwards*: H (fun (_:name) ⇒ P a) (fun x ⇒ R1 x a) b x;
       auto with hopi. nat_math.
    forwards*: H P (R1 x) a b; auto with hopi. nat_math.
    forwards*: @oe_rename (fun x ⇒ R1 x a) (fun (_:name) ⇒ Q a) b x;
       auto with hopi.
    forwards*: @oe_rename (R1 x) Q a b; auto with hopi.
  + exp_ext a. constructor;
    eapply H; eauto; auto with hopi; nat_math.
  + destruct (dec_name a a0); subst.
    exp_ext a0. constructor;
    eapply H; eauto; auto with hopi; nat_math.
    exp_ext a. constructor;
    eapply H; eauto; auto with hopi; nat_math.
  + destruct (dec_name a a0); subst.
    exp_ext a0. constructor;
    eapply H; eauto; auto with hopi; nat_math.
    exp_ext a. constructor;
    eapply H; eauto; auto with hopi; nat_math.
  + ho_exp a P0. ho_exp a Q0. do 2 change_ext.
    apply howe_nu' with (a::b::L); intros. simpl_notin.
    assert (notin_ho a0 (P1 a)).
     intros_all. forwards*: H8 b0. change (notin a0 ((fun a ⇒ P1 a b0) a)).
     eapply notin_rename; eauto.
    assert (notin_ho a0 (Q1 a)).
     intros_all. forwards*: H9 b0. change (notin a0 ((fun a ⇒ Q1 a b0) a)).
     eapply notin_rename; eauto.
    forwards*: H5.
    change (howe' Rel ((fun b ⇒ P1 b a0) b) ((fun b ⇒ Q1 b a0) b) k).
    eapply H; eauto; auto with hopi. nat_math.
Qed.

Lemma howe_implies_howe' {V:Set}: ∀ (Rel:binary proc0),
    rename_compatible Rel → ∀ (P Q:proc V),
    howe Rel P Q → ∃ n, howe' Rel P Q n.
Proof.
   intros. induction H; repeat match goal with
    | H : rename_compatible _, H1 : rename_compatible _ → _ |-_ ⇒
    forwards*: H1; clear H1 end; default_simp; eauto with howe.
   fresh_lp L ((nu P) // nu Q). forwards*: H0 x.
   destruct H2. ∃ (S x0). apply howe_nu' with (x::L).
   intros; simpl_notin. forwards*: @howe'_rename P Q x a.
Qed.

Lemma howe_rename {V:Set}: ∀ (Rel:binary proc0),
  (rename_compatible Rel) → @rename_compatible V (howe Rel).
Proof.
  intros_all. apply howe_implies_howe' in H1; auto.
  destruct H1 as [n]. apply howe'_implies_howe with n; auto.
  forwards*: @howe'_rename P Q a b.
Qed.

Lemma howe_refl {V:Set}: ∀ Rel (P:proc V), howe Rel P P.
Proof.
  intros. induction P; eauto with howe.
  Unshelve. exact (@nil name).
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. apply× @howe_refl.
Qed.

Hint Resolve howe_refl howe_oe:howe.

Hint Constructors tclosure: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; eauto with howe.
  intros. apply tclosure_trans with (y//P'); eauto with howe.
  induction H0; eauto with howe.
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; 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; eauto with howe.
  intros. apply tclosure_trans with (a!(y) P'); eauto with howe.
  induction H0; eauto with howe.
Qed.

Lemma howe_clos_trans_nu {V:Set}:
   ∀ (Rel:binary proc0) (P Q:name → proc V), rename_compatible Rel →
   ∀ a, notin_ho a P → notin_ho a Q → tclosure (howe Rel) (P a) (Q a) →
   tclosure (howe Rel) (nu P) (nu Q).
Proof.
  intros. remember (P a) as Pa. remember (Q a) as Qa.
  gen P Q a. induction H1; auto; intros.
  - apply tclosure_once. subst. apply howe_nu with (a::nil); intros. simpl_notin.
    apply howe_rename with a; eauto.
 - subst. exp a y. apply tclosure_trans with (nu y0).
    eapply IHtclosure1; eauto. eapply IHtclosure2; eauto.
Qed.

Hint Resolve howe_clos_trans_par howe_clos_trans_inp howe_clos_trans_out: 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.
    + fresh_lp L ((nu P) // nu Q). 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. gen W. induction H; intros; simpl; eauto with howe hopi.
    eapply howe_comp; eauto. apply× @oe_mapV.
Qed.

Lemma howe_bind' {V W:Set}: ∀ (Rel:binary proc0) (P :proc V) (f g:V → proc W), rename_compatible Rel →
    ((∀ x, howe Rel (f x) (g x)) → howe Rel (bind f P)(bind g P)).
Proof.
  intros. gen W. induction P; intros; simpl; eauto with howe.
   apply howe_inp. apply IHP. intros [ |]; simpl; auto with howe. intros; apply howe_mapV; auto.
  Unshelve. exact (@nil name).
Qed.

Lemma howe_bind {V W:Set}: ∀ (Rel:binary proc0) (P Q:proc V) (f g:V → proc W), rename_compatible Rel →
    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; eauto with howe.
  - eapply howe_comp with (bind g R); eauto with howe. apply oe_bind; auto.
  - apply howe_inp. apply IHhowe; auto. intros [ |x]; simpl; auto with howe. apply howe_mapV; auto.
  - apply howe_nu with L; intros. apply H0; auto with hopi.
Qed.

Lemma howe_subst {V:Set}: ∀ (Rel:binary proc0) (P' Q' :proc V) P Q, rename_compatible Rel →
   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.

Hint Resolve howe_subst howe_mapV howe_bind:howe.