Require Export Struct_congr.
Require Import TLC.LibNat.

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, howe Rel P 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, 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, howe' Rel P 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. 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; default_simp; eauto with howe.
Qed.

Lemma howe_refl {V:Set}: ∀ Rel (P:proc V), howe Rel P P.
Proof.
  intros. induction P; eauto with howe.
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.

Lemma howe_mapN {V:Set}: ∀ (Rel:binary proc0),
  (rename_compatible Rel) → @rename_compatible V (howe Rel).
Proof.
  intros_all. gen f. induction H; intros; simpl; auto with howe.
  + eapply howe_comp. apply× IHhowe. apply× (oe_rename Rel X).
  + apply howe_nu. apply× IHhowe. apply× liftN_preserves_injectivity.
Qed.

Lemma howe'_mapN {V:Set}: ∀ (Rel:binary proc0),
  (rename_compatible Rel) → ∀ (P Q:proc V) n, howe' Rel P Q n → ∀ f, injective f → howe' Rel (mapN f P) (mapN f Q) n.
Proof.
  intros_all. gen f. induction H; intros; simpl; auto with howe.
  + eapply howe_comp'. apply× IHhowe'. apply× (oe_rename Rel X).
  + apply howe_nu'. apply× IHhowe'. apply× liftN_preserves_injectivity.
Qed.

Lemma howe_genNu {V:Set} : ∀ Rel (P Q:proc V) n , howe Rel P Q → howe Rel (genNu n P)(genNu n Q).
Proof.
  intros; induction n; simpl; auto with howe.
Qed.

Hint Resolve howe_refl howe_oe howe_mapN howe_genNu: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.
    induction H0. apply tclosure_once. apply howe_par; auto. apply howe_refl; auto.
    eapply tclosure_trans; eauto.
  - intros. apply tclosure_trans with (y//P'). apply IHtclosure1. apply tclosure_once; apply howe_refl.
    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. apply howe_refl.
    induction H0. apply tclosure_once. apply howe_out; auto. apply howe_refl.
    eapply tclosure_trans; eauto.
  - intros. apply tclosure_trans with (a!(y) P'). apply IHtclosure1. apply tclosure_once; apply howe_refl.
    auto.
Qed.

Lemma howe_clos_trans_nu {V:Set}:
   ∀ (Rel:binary proc0) (P Q:proc V),
           tclosure (howe Rel) P Q → tclosure (howe Rel) (nu P) (nu Q).
Proof.
  intros. induction H; auto; intros.
  - apply tclosure_once. auto with howe.
 - apply tclosure_trans with (nu y). 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. gen W. induction H; intros; simpl; auto with howe.
    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; auto with howe.
  - apply howe_inp. apply IHP. intros [ |]; simpl; auto with howe. intros; apply howe_mapV; auto.
  - apply howe_nu. apply IHP. intros. apply× @howe_mapN.
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; auto 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. apply× IHhowe. intros; apply× @howe_mapN.
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.