Library HOC21Coinductive

Require Import HOC01Defs.
Require Import HOC02BaseLemmas.
Require Import HOC03CanonicalLemmas.
Require Import HOC04DefLTS.
Require Import HOC05WFProcesses.
Require Import HOC06FreshLemmas.
Require Import HOC07SizeLemmas.
Require Import HOC08SubstLemmas.
Require Import HOC09GVLemmas.
Require Import HOC10CongrLemmas.
Require Import HOC11TransLemmas.
Require Import HOC13Bisimulations.
Require Import HOC14IObis.


Definition in_relation_step (R : RelWfP) (p q : wfprocess) : Prop :=
  ∀ (a : chan) (fp : abstraction),
    {{p -- LabIn a ->> (AA fp)}} →
      ∃ (fq : abstraction),
        {{q -- LabIn a ->> (AA fq)}} ∧
          ∀ X, X#p → X#q →
            R (wfp_inst_Abs fp (wfp_Gvar X)) (wfp_inst_Abs fq (wfp_Gvar X)).

Definition in_ex_relation_step (R : RelWfP) (p q : wfprocess) : Prop :=
  ∀ (a : chan) (fp : abstraction),
    {{p -- LabIn a ->> (AA fp)}} →
      ∃ (fq : abstraction),
        {{q -- LabIn a ->> (AA fq)}} ∧
          ∃ X, X#p ∧ X#q ∧
            R (wfp_inst_Abs fp (wfp_Gvar X)) (wfp_inst_Abs fq (wfp_Gvar X)).

Definition out_relation_step (R : RelWfP) (p q : wfprocess) : Prop :=
  ∀ (a : chan) (p´ p´´ : wfprocess),
    {{p -- LabOut a p´´ ->> (AP p´)}} →
      ∃ (q´ q´´ : wfprocess),
        ({{q -- LabOut a q´´ ->> (AP q´)}} ∧ (R p´ q´) ∧ (R p´´ q´´)).

Definition var_relation_step (R : RelWfP) (p q : wfprocess) : Prop :=
  ∀ (X : var) (p´ : wfprocess), {{p -- LabRem X ->> (AP p´)}} →
      ∃ (q´ : wfprocess), {{q -- LabRem X ->> (AP q´)}} ∧ (R p´ q´).


CoInductive IObisC : binary wfprocess :=
 | IOCMain : ∀ (p q : wfprocess),
     IObisC q p ∧ (in_relation_step IObisC p q) ∧ (out_relation_step IObisC p q) ∧ (var_relation_step IObisC p q) →
       IObisC p q.

Inductive IObisIAux (R : binary wfprocess) : binary wfprocess :=
 | IOCIAMain : ∀ (p q : wfprocess),
     R q p ∧ (in_relation_step R p q) ∧ (out_relation_step R p q) ∧ (var_relation_step R p q) →
       IObisIAux R p q.

Inductive IObisI : binary wfprocess :=
 | IOCIMain : ∀ (R : binary wfprocess) p q, (∀ p q, (R p q) → IObisIAux R p q) → R p q → IObisI p q.

Notation "p ≈c q" := (IObisC p q) (at level 60).
Notation "p ≈i q" := (IObisI p q) (at level 60).

Hint Resolve IOCMain IOCIMain.

Lemma IObisI_sym : Symmetric IObisI.
Proof.
  introv Hxy; inverts Hxy.
  eapply IOCIMain. Focus 2.
    apply H in H0; inverts H0 as (Hr´ & Hrest).
    exact Hr´. auto.
Qed.

Lemma IObisI_in : in_relation IObisI.
Proof.
  introv Hio Ht; inverts Hio.
  apply H in H0; inverts H0 as (_ & Hi & _ & _).
  specializes Hi (>> a fp Ht).
  destruct Hi as (q´ & Ht´ & Hr). ∃ q´; split×.
  introv Hf1 Hf2; auto.
  specializes Hr Hf1 Hf2.
Qed.

Lemma IObisI_out : out_relation IObisI.
Proof.
  introv Hio; introv Ht. inverts Hio.
  apply H in H0; inverts H0 as (_ & _ & Ho & _).
  specializes Ho Ht; destruct Ho as (q´ & q´´ & Htq & Hr´ & Hr´´).
  ∃ q´ q´´; splits×.
Qed.

Lemma IObisI_var : var_relation IObisI.
Proof.
  introv Hio; introv Ht. inverts Hio.
  apply H in H0; inverts H0 as (_ & _ & _ & Hv).
  specializes Hv Ht; destruct Hv as (q´ & Htq & Hr).
  ∃ q´; splits×.
Qed.

Lemma IObisI_eq_IObis : ∀ p q, p ≈i q ↔ p ≈ q.
Proof.
  split; introv Hyp.
    ∃ IObisI; repeat splits¬.
      apply IObisI_sym. apply IObisI_in.
      apply IObisI_out. apply IObisI_var.
    inverts Hyp; rename x into R.
    destruct H as ((Hs & Hi & Ho & Hv) & Hr).
    econstructor; try eassumption.
    clear Hr p q; introv Hr.
    constructor; splits¬.
      specializes¬ Hi Hr.
      specializes¬ Ho Hr.
      specializes¬ Hv Hr.
Qed.

Lemma IObisC_eq_IObisI : ∀ p q, p ≈c q ↔ p ≈i q.
Proof.
  introv; split; intro Hyp.
    econstructor; try eassumption.
    clear; introv Hyp.
    inverts Hyp; constructor×.

  inverts Hyp.
  gen p q. cofix.

  constructor; splits.
  apply IObisC_eq_IObisI.
  specializes H H0; inverts× H.

  introv Ht; specializes H H0.
  inverts H as (_ & H & _ & _).
  specialize (H a fp Ht); destruct H as (fq & H´ & Hyp).
  ∃ fq; splits*; introv Hfxp Hfxq; specializes Hyp Hfxp Hfxq.

  introv Ht; specializes H H0.
  inverts H as (_ & _ & H & _).
  specializes H Ht; destruct H as (q´ & q´´ & Hyp).
  ∃ q´ q´´; splits×.

  introv Ht; specializes H H0.
  inverts H as (_ & _ & _ & H).
  specializes H Ht; destruct H as (q´ & Hyp).
  ∃ q´; splits×.
Qed.

Lemma IObis_eq_IObisC : ∀ p q, IObis p q ↔ IObisC p q.
Proof.
  introv; rewrite IObisC_eq_IObisI; rewrite× IObisI_eq_IObis.
Qed.

Instance IObisC_equivalence : Equivalence IObisC.
Proof.
  constructor; introv; repeat rewrite× <- IObis_eq_IObisC.
Qed.


CoInductive IObisC_ex : binary wfprocess :=
 | IOCMain_ex : ∀ (p q : wfprocess),
     IObisC_ex q p ∧ (in_ex_relation_step IObisC_ex p q) ∧ (out_relation_step IObisC_ex p q) ∧ (var_relation_step IObisC_ex p q) →
       IObisC_ex p q.

Inductive IObisIAux_ex (R : binary wfprocess) : binary wfprocess :=
 | IOCIAMain_ex : ∀ (p q : wfprocess),
     R q p ∧ (in_ex_relation_step R p q) ∧ (out_relation_step R p q) ∧ (var_relation_step R p q) →
       IObisIAux_ex R p q.

Inductive IObisI_ex : binary wfprocess :=
 | IOCIMain_ex : ∀ (R : binary wfprocess) p q, (∀ p q, (R p q) → IObisIAux_ex R p q) → R p q → IObisI_ex p q.

Notation "p ≈ec q" := (IObisC_ex p q) (at level 60).
Notation "p ≈ei q" := (IObisI_ex p q) (at level 60).

Hint Resolve IOCMain_ex IOCIMain_ex.

Lemma IObisI_ex_sym : Symmetric IObisI_ex.
Proof.
  introv Hxy; inverts Hxy.
  eapply IOCIMain_ex. Focus 2.
    apply H in H0; inverts H0 as (Hr´ & Hrest).
    exact Hr´. auto.
Qed.

Lemma IObisI_ex_in_ex : in_relation_ex IObisI_ex.
Proof.
  introv Hio Ht; inverts Hio.
  apply H in H0; inverts H0 as (_ & Hi & _ & _).
  specializes Hi (>> a fp Ht).
  destruct Hi as (q´ & Ht´ & Hr). ∃ q´; splits×.
  destruct Hr as (X & Hfxp & Hfxq & Hr); ∃ X; splits×.
Qed.

Lemma IObisI_ex_out : out_relation IObisI_ex.
Proof.
  introv Hio; introv Ht. inverts Hio.
  apply H in H0; inverts H0 as (_ & _ & Ho & _).
  specializes Ho Ht; destruct Ho as (q´ & q´´ & Htq & Hr´ & Hr´´).
  ∃ q´ q´´; splits×.
Qed.

Lemma IObisI_ex_var : var_relation IObisI_ex.
Proof.
  introv Hio; introv Ht. inverts Hio.
  apply H in H0; inverts H0 as (_ & _ & _ & Hv).
  specializes Hv Ht; destruct Hv as (q´ & Htq & Hr).
  ∃ q´; splits×.
Qed.

Lemma IObisI_ex_eq_IObis_ex : ∀ p q, p ≈ei q ↔ IObis_ex p q.
Proof.
  split; introv Hyp.
    ∃ IObisI_ex; repeat splits¬.
      apply IObisI_ex_sym. apply IObisI_ex_in_ex.
      apply IObisI_ex_out. apply IObisI_ex_var.
    inverts Hyp; rename x into R.
    destruct H as ((Hs & Hi & Ho & Hv) & Hr).
    econstructor; try eassumption.
    clear Hr p q; introv Hr.
    constructor; splits¬.
      specializes¬ Hi Hr.
      specializes¬ Ho Hr.
      specializes¬ Hv Hr.
Qed.

Lemma IObisC_ex_eq_IObisI_ex : ∀ p q, p ≈ec q ↔ p ≈ei q.
Proof.
  introv; split; intro Hyp.
    econstructor; try eassumption.
    clear; introv Hyp.
    inverts Hyp; constructor×.

  inverts Hyp.
  gen p q. cofix.

  constructor; splits.
  apply IObisC_ex_eq_IObisI_ex.
  specializes H H0; inverts× H.

  introv Ht; specializes H H0.
  inverts H as (_ & H & _ & _).
  specialize (H a fp Ht); destruct H as (fq & H´ & X & Hfx1 & Hfx2 & Hr).
  ∃ fq; splits*; ∃× X.

  introv Ht; specializes H H0.
  inverts H as (_ & _ & H & _).
  specializes H Ht; destruct H as (q´ & q´´ & Hyp).
  ∃ q´ q´´; splits×.

  introv Ht; specializes H H0.
  inverts H as (_ & _ & _ & H).
  specializes H Ht; destruct H as (q´ & Hyp).
  ∃ q´; splits×.
Qed.

Lemma IObis_ex_eq_IObisC_ex : ∀ p q, IObis_ex p q ↔ IObisC_ex p q.
Proof.
  introv; rewrite IObisC_ex_eq_IObisI_ex; rewrite× IObisI_ex_eq_IObis_ex.
Qed.

Instance IObisC_ex_equivalence : Equivalence IObisC_ex.
Proof.
  constructor; introv;
  repeat rewrite <- IObis_ex_eq_IObisC_ex;
  repeat rewrite× <- IObis_IObis_ex.
Qed.