Library HOC22Decidability

Require Import LibEpsilon.
Require Import Coq.Logic.Decidable.
Require Import Program.

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 HOC10CongrLemmas.
Require Import HOC11TransLemmas.
Require Import HOC12Guarded.
Require Import HOC13Bisimulations.
Require Import HOC14IObis.
Require Import HOC21Coinductive.


Fixpoint GV_union (lp : list process) :=
match lp with
  | p :: lp ⇒ (GV p) \u GV_union lp
  | nil ⇒ \{}
end.

Lemma GV_union_included : ∀ (lp : list process),
  Forall (fun p ⇒ (GV p) \c GV_union lp) lp.
Proof.
  inductions lp.
    apply Forall_nil.
    apply¬ Forall_cons; simpl.
      introv p; rewrite¬ in_union.
      rewrite <- Forall_Mem in *; introv Hm.
      specializes IHlp Hm.
      introv Hin; specializes IHlp Hin.
      rewrite¬ in_union.
Qed.

Fixpoint abs_subst (fp : abstraction) Y : abstraction :=
match fp with
  | AbsPure X p ⇒ AbsPure Y (wfp_subst (wfp_Gvar Y) X p)
  | AbsPar1 fp q ⇒ AbsPar1 (abs_subst fp Y) q
  | AbsPar2 p fq ⇒ AbsPar2 p (abs_subst fq Y)
end.

Lemma inst_abs_subst_eq :
  ∀ p a fp Y q,
    {{p -- LabIn a ->> AA fp}} → Y # p → wfp_inst_Abs fp q = wfp_inst_Abs (abs_subst fp Y) q.
Proof with automate.
  induction p using (measure_induction wfp_size).
  destruct_wf p; introv Ht Hfy; try solve [inverts¬ Ht].

  lets H1 : wfp_trans_in_chan_eq Ht; subst a0.
  lets Hyp : wfp_trans_in_abs_eq Ht; inverts Hyp as Hyp; simpl.
    rewrite wfp_gfresh_Abs in Hfy; inverts Hfy as Hfy.
      rewrite¬ wfp_subst_gvar_idem.
      rewrite¬ <- wfp_subst_decomposition_g.
    destruct Hyp as (Z & Hneqz & Hfz & Heq); subst; simpl.
    rewrite wfp_gfresh_Abs in Hfy; inverts Hfy as Hfy.
      repeat rewrite¬ <- wfp_subst_decomposition_g.
      simpl; fresh_solve.
      rewrite¬ <- wfp_subst_decomposition_g.
      tests : (Y = Z).
        rewrite wfp_subst_gvar_idem.
        rewrite¬ <- wfp_subst_decomposition_g.
        repeat rewrite¬ <- wfp_subst_decomposition_g.
        tests : (Y = X); simpl; fresh_solve.

  simpl in Hfy; rewrite gfresh_par_iff in Hfy. inverts Ht...
    destruct ap; inverts H4; simpls; fequals.
    eapply H... auto...
    destruct aq; inverts H4; simpls; fequals.
    eapply H... auto...
Qed.

Instance inhabited_var_wfprocess : Inhab (var × wfprocess).
Proof.
  lets Hyp : (var_fresh (\{})).
  destruct Hyp as (X & _).
  constructor.
  ∃¬ (X, wfp_Nil).
Qed.

Lemma get_Abs_from_Receive : ∀ a x p (forbidden : list process), wf (Receive a x p) →
  sig2
    (fun T : (var × wfprocess) ⇒ Receive a x p = proc (wfp_Abs a (fst T) (snd T)))
    (fun T : (var × wfprocess) ⇒ Forall (fun p ⇒ (fst T # p)) forbidden).
Proof.
  introv Hwf.
  lets Hyp : (var_fresh ((GV p) \u GV_union forbidden)).
  destruct Hyp as (X & Hx).
  lets Hyp : wf_receive Hwf.
  rewrite notin_union in Hx; inverts Hx.
  specializes Hyp H; destruct Hyp as (Hwf´ & Heq).
  set (wfp := mkWfP ([Gvar X /// x]p) Hwf´).
  ∃ (X, wfp); simpls¬.
    lets Hyp : GV_union_included forbidden.
    rewrite <- Forall_Mem in ×.
    intros q Hm; specializes Hyp Hm; unfold fresh_gvar.
    unfold notin in *; introv Hin; apply H0.
    unfold subset in ×. jauto.
Qed.

Definition Abs_from_Receive a x p (Hwf : wf (Receive a x p)) (forbidden : list process) :=
  epsilon (fun T ⇒ Receive a x p = proc (wfp_Abs a (fst T) (snd T)) ∧ Forall (fun p ⇒ (fst T # p)) forbidden).

Lemma Abs_from_Receive_spec : ∀ a x p (Hwf : wf (Receive a x p)) (forbidden : list process),
  Receive a x p = proc (wfp_Abs a (fst (Abs_from_Receive a x p Hwf forbidden)) (snd (Abs_from_Receive a x p Hwf forbidden))) ∧ Forall (fun q ⇒ (fst (Abs_from_Receive a x p Hwf forbidden)) # q) forbidden.
Proof.
  introv.
  unfold Abs_from_Receive.
  spec_epsilon¬ as Yep.
  lets Hyp : get_Abs_from_Receive a x p forbidden Hwf.
  inverts Hyp; ∃¬ x0.
Qed.


Fixpoint out_der_aux (p : process) :=
match p as p0 return (wf p0 → _) with
  | Send a p´ ⇒ (fun Hwfp ⇒
     let wfp´ := mkWfP p´ (wf_send a p´ Hwfp) in
      cons (a, wfp´, wfp_Nil) nil)
  | Par p´ q´ ⇒ (fun Hwfp ⇒
     let wfp := mkWfP p´ (wf_par1 p´ q´ Hwfp) in
       let wfq := mkWfP q´ (wf_par2 p´ q´ Hwfp) in
         rev_append
           (List.map (fun (e : (chan × wfprocess × wfprocess)) ⇒
             match e with (a, m, p´) ⇒ (a, m, wfp_Par p´ wfq) end) (out_der_aux p´ (wf_cond wfp)))
           (List.map (fun (e : (chan × wfprocess × wfprocess)) ⇒
             match e with (a, m, p´) ⇒ (a, m, wfp_Par wfp p´) end) (out_der_aux q´ (wf_cond wfq))))
  | _ ⇒ (fun _ ⇒ nil)
end.

Lemma out_der_aux_eq : ∀ (p : process) (Hwf1 Hwf2 : wf p),
  out_der_aux p Hwf1 = out_der_aux p Hwf2.
Proof.
  destruct p; try solve [simpls*];
    introv; simpl; repeat fequals;
    extens; introv;
      destruct x1; destruct p; repeat fequals.
Qed.

Definition out_der (p : wfprocess) : (list (chan × wfprocess × wfprocess)) :=
  out_der_aux p (wf_cond p).

Lemma out_der_ok : ∀ p a m p´,
  {{p -- LabOut a m ->> (AP p´)}} ↔ (List.In (a, m, p´)) (out_der p).
Proof.
  induction p using wfp_ind_gen; introv; split; introv Hyp; try solve [inverts Hyp].

  inverts Hyp; subst_wfp. simpl; left.
  fequals. fequals. rewrite_wfp_equal.

  simpls; inverts Hyp as Hyp; inverts Hyp.
  assert (p = mkWfP p (wf_send a0 p (WfSend a0 p (wf_cond p)))) by rewrite_wfp_equal.
  rewrite <- H; auto.

  inverts Hyp; subst_wfp; unfold out_der in *; simpls.

rewrite rev_append_rev. apply in_or_app. left.
  rewrite <- in_rev. apply in_map_iff.
  destruct ap; inverts H3.
  specialize (IHp1 a m w). destruct IHp1 as [IHp1 IHp1´].
  specialize (IHp1 H2). clear IHp1´ IHp2.
  ∃ (a, m, w). splits.
    fequals. fequals. rewrite_wfp_equal.
    erewrite out_der_aux_eq. eassumption.

rewrite rev_append_rev. apply in_or_app. right.
  apply in_map_iff.
  destruct aq; inverts H3.
  specialize (IHp2 a m w). destruct IHp2 as [IHp2 IHp2´].
  specialize (IHp2 H2). clear IHp2´ IHp1.
  ∃ (a, m, w). splits.
    fequals. fequals. rewrite_wfp_equal.
    erewrite out_der_aux_eq. eassumption.

  unfolds out_der; simpls.
rewrite rev_append_rev in Hyp.
  rewrite in_app_iff in Hyp. destruct Hyp as [H | H].
  rewrite <- in_rev in H. rewrite in_map_iff in H.
  destruct H as [pdt Heq]. destruct pdt as [[c m´] p1´].
  destruct Heq as [Heq Hin]. inverts Heq.
  assert (p2 = mkWfP p2 (wf_par2 p1 p2 (WfPar p1 p2 (wf_cond p1) (wf_cond p2)))) by rewrite_wfp_equal.
  rewrite <- H in ×.
  apply¬ act1_out. apply¬ IHp1.
  erewrite out_der_aux_eq. eassumption.

rewrite in_map_iff in H.
  destruct H as [pdt Heq]. destruct pdt as [[c m´] p2´].
  destruct Heq as [Heq Hin]. inverts Heq.
  assert (p1 = mkWfP p1 (wf_par1 p1 p2 (WfPar p1 p2 (wf_cond p1) (wf_cond p2)))) by rewrite_wfp_equal.
  rewrite <- H in ×.
  apply¬ act2_out. apply¬ IHp2.
  erewrite out_der_aux_eq. eassumption.
Qed.


Fixpoint X_der_aux (p : process) :=
  match p as p0 return (wf p0 → _) with
    | Gvar X ⇒ (fun _ ⇒
       cons (X, wfp_Nil) nil)
    | Par p q ⇒ (fun Hwfp ⇒
       let wfp := mkWfP p (wf_par1 p q Hwfp) in
         let wfq := mkWfP q (wf_par2 p q Hwfp) in
           rev_append
             (List.map (fun (e : (var × wfprocess)) ⇒
               match e with (X, p´) ⇒ (X, wfp_Par p´ wfq) end) (X_der_aux wfp (wf_cond wfp)))
             (List.map (fun (e : (var × wfprocess)) ⇒
               match e with (X, p´) ⇒ (X, wfp_Par wfp p´) end) (X_der_aux wfq (wf_cond wfq))))
    | _ ⇒ (fun _ ⇒ nil)
  end.

Lemma X_der_aux_eq : ∀ (p : process) (Hwf1 Hwf2 : wf p),
  X_der_aux p Hwf1 = X_der_aux p Hwf2.
Proof.
  destruct p; try solve [simpls*];
    introv; simpl; repeat fequals;
    extens; introv;
      destruct x1; repeat fequals.
Qed.

Definition X_der (p : wfprocess) :=
  X_der_aux p (wf_cond p).

Lemma X_der_ok : ∀ p X p´,
  {{p -- LabRem X ->> (AP p´)}} ↔ (List.In (X, p´) (X_der p)).
Proof.
  induction p using wfp_ind_gen; introv; split; introv Hyp; try solve [inverts Hyp].

  inverts Hyp; subst_wfp. simpl; left.
  fequals.

  unfolds X_der; simpls; inverts Hyp as Hyp; inverts¬ Hyp.

  inverts Hyp; subst_wfp;
  unfolds X_der; simpls.

rewrite rev_append_rev. apply in_or_app. left.
  rewrite <- in_rev. apply in_map_iff.
  destruct ap; inverts H3.
  specialize (IHp1 X w). destruct IHp1 as [IHp1 IHp1´].
  specialize (IHp1 H2). clear IHp1´ IHp2.
  ∃ (X, w). splits.
    fequals. fequals. rewrite_wfp_equal.
    erewrite X_der_aux_eq. eassumption.

rewrite rev_append_rev. apply in_or_app. right.
  apply in_map_iff.
  destruct aq; inverts H3.
  specialize (IHp2 X w). destruct IHp2 as [IHp2 IHp2´].
  specialize (IHp2 H2). clear IHp2´ IHp1.
  ∃ (X, w). splits.
    fequals. fequals. rewrite_wfp_equal.
    erewrite X_der_aux_eq. eassumption.

  unfolds X_der; simpls.
rewrite rev_append_rev in Hyp.
  rewrite in_app_iff in Hyp. destruct Hyp as [H | H].
  rewrite <- in_rev in H. rewrite in_map_iff in H.
  destruct H as [pdt Heq]. destruct pdt as [Y p1´].
  destruct Heq as [Heq Hin]. inverts Heq.
  assert (p2 = mkWfP p2 (wf_par2 p1 p2 (WfPar p1 p2 (wf_cond p1) (wf_cond p2)))) by rewrite_wfp_equal.
  rewrite <- H in ×.
  apply¬ act1_rem. apply¬ IHp1.
  erewrite X_der_aux_eq. eassumption.

rewrite in_map_iff in H.
  destruct H as [pdt Heq]. destruct pdt as [Y p2´].
  destruct Heq as [Heq Hin]. inverts Heq.
  assert (p1 = mkWfP p1 (wf_par1 p1 p2 (WfPar p1 p2 (wf_cond p1) (wf_cond p2)))) by rewrite_wfp_equal.
  rewrite <- H in ×.
  apply¬ act2_rem. apply¬ IHp2.
  erewrite X_der_aux_eq. eassumption.
Qed.


Fixpoint in_der_aux (p : process) (forbidden : list process) :=
  match p as p0 return (wf p0 → _) with
    | Receive a x p ⇒ (fun Hwfp ⇒
       cons (a, AbsPure (fst (Abs_from_Receive a x p Hwfp forbidden)) (snd (Abs_from_Receive a x p Hwfp forbidden))) nil)
    | Par p q ⇒ (fun Hwfp ⇒
       let wfp := mkWfP p (wf_par1 p q Hwfp) in
         let wfq := mkWfP q (wf_par2 p q Hwfp) in
           rev_append
             (List.map (fun (e : (chan × abstraction)) ⇒
               match e with (a, f) ⇒ (a, AbsPar1 f wfq) end) (in_der_aux wfp (q :: forbidden) (wf_cond wfp)))
             (List.map (fun (e : (chan × abstraction)) ⇒
               match e with (a, f) ⇒ (a, AbsPar2 wfp f) end) (in_der_aux wfq (p :: forbidden) (wf_cond wfq))))
    | _ ⇒ (fun _ ⇒ nil)
  end.

Lemma in_der_aux_eq : ∀ (p : process) (forbidden : list process) (Hwf1 Hwf2 : wf p),
  in_der_aux p forbidden Hwf1 = in_der_aux p forbidden Hwf2.
Proof.
  destruct p; try solve [simpls*];
    introv; simpl; repeat fequals;
    extens; introv;
      destruct x1; repeat fequals.
Qed.

Definition in_der (p : wfprocess) (forbidden : list process) :=
  in_der_aux p forbidden (wf_cond p).

Lemma in_der_ok_rl : ∀ p a fp forbidden,
  (List.In (a, fp) (in_der p forbidden)) → {{p -- LabIn a ->> (AA fp)}}.
Proof.
  induction p using wfp_ind_gen; introv Hyp; try solve [inverts Hyp].

  simpls.
  lets Habs : Abs_from_Receive_spec a (f X p) ([Lvar (f X p) // X]p).
  lets Hwf : (WfAbs a X p (wf_cond p)); unfold Abs in Hwf.
  specialize (Habs Hwf).
  inverts Hyp as Hyp; inverts Hyp.
  specializes Habs forbidden. destruct Habs as (Habs & _).
  assert (wfp_Abs a0 X p = wfp_Abs a0
           (fst (Abs_from_Receive a0 (f X p) ([Lvar (f X p) // X]p) Hwf forbidden))
           (snd (Abs_from_Receive a0 (f X p) ([Lvar (f X p) // X]p) Hwf forbidden))) by
    rewrite_wfp_equal.
  rewrite H0. constructor.

  unfolds in_der; simpls.
rewrite rev_append_rev in Hyp.
  rewrite in_app_iff in Hyp. destruct Hyp as [H | H].
  rewrite <- in_rev in H. rewrite in_map_iff in H.
  destruct H as [pdt Heq]. destruct pdt as [a´ fp´].
  destruct Heq as [Heq Hin]. inverts Heq.
  assert (p2 = mkWfP p2 (wf_par2 p1 p2 (WfPar p1 p2 (wf_cond p1) (wf_cond p2)))) by rewrite_wfp_equal.
  rewrite <- H in ×.
  apply¬ act1_in. eapply IHp1. erewrite in_der_aux_eq. eassumption.

rewrite in_map_iff in H.
  destruct H as [pdt Heq]. destruct pdt as [a´ fp´].
  destruct Heq as [Heq Hin]. inverts Heq.
  assert (p1 = mkWfP p1 (wf_par1 p1 p2 (WfPar p1 p2 (wf_cond p1) (wf_cond p2)))) by rewrite_wfp_equal.
  rewrite <- H in ×.
  apply¬ act2_in. eapply IHp2. erewrite in_der_aux_eq. eassumption.
Qed.

Lemma in_der_ok_lr : ∀ a p fp forbidden,
  {{p -- LabIn a ->> AA fp}} →
    List.In (a, fp) (in_der p forbidden) ∨
    ∃ Y, Forall (fun p ⇒ Y # p) (proc p :: forbidden) ∧ List.In (a, abs_subst fp Y) (in_der p forbidden).
Proof.
  induction p using wfp_ind_gen; introv Hyp; try solve [inverts Hyp].
  lets H1 : wfp_trans_in_chan_eq Hyp; subst a0.
  lets H1 : wfp_trans_in_abs_eq Hyp; inverts H1 as H1; simpl.

  lets Hwf : (WfAbs a X p (wf_cond p)); unfold Abs in Hwf.
  set (Y := (fst (Abs_from_Receive a (f X p) ([Lvar (f X p) // X]p) Hwf forbidden))).
  set (q := (snd (Abs_from_Receive a (f X p) ([Lvar (f X p) // X]p) Hwf forbidden))).
  lets Habs : Abs_from_Receive_spec a (f X p) ([Lvar (f X p) // X]p).
  specialize (Habs Hwf forbidden). destruct Habs as (Habs & Hfyf). fold Y in Habs, Hfyf. fold q in Habs.
  replace (Receive a (f X p) ([Lvar (f X p) // X]p)) with (proc (wfp_Abs a X p)) in Habs.
  rewrite <- wfprocess_eq in Habs; symmetry in Habs; apply wfp_Abs_equal in Habs.
  destruct Habs as (_ & Habs). cases_if×.
  left. rewrite e. rewrite× Habs.
  right. destruct Habs as (Heq & Hfy).
  ∃ Y. splits.
    apply¬ Forall_cons.
    unfold Abs; rewrite gfresh_receive; fresh_solve.
    rewrite× <- Heq.
  simpl; unfolds¬ Abs.

 destruct H1 as (Z & Hneqz & Hfz & Heq); subst.
  lets Hwf : (WfAbs a X p (wf_cond p)); unfold Abs in Hwf.
  set (Y := (fst (Abs_from_Receive a (f X p) ([Lvar (f X p) // X]p) Hwf forbidden))).
  set (q := (snd (Abs_from_Receive a (f X p) ([Lvar (f X p) // X]p) Hwf forbidden))).
  lets Habs : Abs_from_Receive_spec a (f X p) ([Lvar (f X p) // X]p).
  specialize (Habs Hwf forbidden). destruct Habs as (Habs & Hfyf). fold Y in Habs, Hfyf. fold q in Habs.
  replace (Receive a (f X p) ([Lvar (f X p) // X]p)) with (proc (wfp_Abs a X p)) in Habs.
  rewrite <- wfprocess_eq in Habs; symmetry in Habs; apply wfp_Abs_equal in Habs.
  destruct Habs as (_ & Habs). cases_if×.
    rewrite e. simpl. right. ∃ X; splits.
     rewrite <- e; apply¬ Forall_cons.
     unfold Abs; rewrite gfresh_receive; fresh_solve.
     left. fequals. fequals. rewrite¬ <- wfp_subst_decomposition_g.
      rewrite wfp_subst_gvar_idem. rewrite¬ Habs.
    destruct Habs as (Heq & Hf).
    right; ∃ Y; rewrite Heq. splits.
    apply¬ Forall_cons.
    unfold Abs; rewrite gfresh_receive; fresh_solve.
    left. simpl; fequals. fequals. rewrite¬ <- wfp_subst_decomposition_g.
  simpl; unfolds¬ Abs.

  inverts Hyp; subst_wfp;
  unfolds in_der; simpl.

  destruct ap; inverts H3; rename a0 into fp.
  specialize (IHp1 fp (proc p2 :: forbidden) H2). inverts IHp1.
    left. rewrite rev_append_rev. apply in_or_app. left.
    rewrite <- in_rev. apply in_map_iff.
    assert (p2 = mkWfP p2 (wf_par2 p1 p2 (WfPar p1 p2 (wf_cond p1) (wf_cond p2)))) by rewrite_wfp_equal.
    ∃ (a, fp); splits.
    rewrite¬ <- H0. erewrite in_der_aux_eq. eassumption.

    right. destruct H as (Y & Hfy & IHp1´).
    ∃ Y; splits.
      inverts Hfy. inverts H3. apply¬ Forall_cons.
      rewrite× gfresh_par_iff.
    rewrite rev_append_rev. apply in_or_app. left.
    rewrite <- in_rev. apply in_map_iff.
    assert (p2 = mkWfP p2 (wf_par2 p1 p2 (WfPar p1 p2 (wf_cond p1) (wf_cond p2)))) by rewrite_wfp_equal.
    ∃ (a, abs_subst fp Y); splits.
    rewrite¬ <- H. erewrite in_der_aux_eq. eassumption.

  destruct aq; inverts H3; rename a0 into fp.
  specialize (IHp2 fp (proc p1 :: forbidden) H2). inverts IHp2.
    left. rewrite rev_append_rev. apply in_or_app. right.
    apply in_map_iff.
    assert (p1 = mkWfP p1 (wf_par1 p1 p2 (WfPar p1 p2 (wf_cond p1) (wf_cond p2)))) by rewrite_wfp_equal.
    ∃ (a, fp); splits.
    rewrite¬ <- H0. erewrite in_der_aux_eq. eassumption.

    right. destruct H as (Y & Hfy & IHp1´).
    ∃ Y; splits.
      inverts Hfy. inverts H3. apply¬ Forall_cons.
      rewrite× gfresh_par_iff.
    rewrite rev_append_rev. apply in_or_app. right.
    apply in_map_iff.
    assert (p1 = mkWfP p1 (wf_par1 p1 p2 (WfPar p1 p2 (wf_cond p1) (wf_cond p2)))) by rewrite_wfp_equal.
    ∃ (a, abs_subst fp Y); splits.
    rewrite¬ <- H. erewrite in_der_aux_eq. eassumption.
Qed.


Fixpoint bio_aux (p q : wfprocess) (n : nat) : bool :=
  match n with
    | 0 ⇒ false
    | S n ⇒
      (forallb (fun ep ⇒ match ep with (a,m,p´) ⇒
        (existsb (fun eq ⇒ match eq with (b,m´,q´) ⇒
          (beq_nat a b) && (bio_aux p´ q´ n) && (bio_aux m m´ n) end) (out_der q)) end) (out_der p))
      &&
      (forallb (fun eq ⇒ match eq with (a,m,q´) ⇒
        (existsb (fun ep ⇒ match ep with (b,m´,p´) ⇒
          (beq_nat b a) && (bio_aux p´ q´ n) && (bio_aux m´ m n) end) (out_der p)) end) (out_der q))
      &&
      (forallb (fun ep ⇒ match ep with (a,fp) ⇒
        (existsb (fun eq ⇒ match eq with (b,fq) ⇒
          (beq_nat a b) && (let X := var_gen (GV (Par p q)) in bio_aux (wfp_inst_Abs fp (wfp_Gvar X)) (wfp_inst_Abs fq (wfp_Gvar X)) n) end)
            (in_der q nil)) end) (in_der p nil))
      &&
      (forallb (fun eq ⇒ match eq with (a,fq) ⇒
        (existsb (fun ep ⇒ match ep with (b,fp) ⇒
          (beq_nat b a) && (let X := var_gen (GV (Par p q)) in bio_aux (wfp_inst_Abs fp (wfp_Gvar X)) (wfp_inst_Abs fq (wfp_Gvar X)) n) end)
            (in_der p nil)) end) (in_der q nil))
      &&
      (forallb (fun ep ⇒ match ep with (X,p´) ⇒
        (existsb (fun eq ⇒ match eq with (Y,q´) ⇒
          (ifb (X=Y) then true else false) && (bio_aux p´ q´ n) end) (X_der q)) end) (X_der p))
      &&
      (forallb (fun eq ⇒ match eq with (X,q´) ⇒
        (existsb (fun ep ⇒ match ep with (Y,p´) ⇒
          (ifb (Y=X) then true else false) && (bio_aux p´ q´ n) end) (X_der p)) end) (X_der q))
  end.

Definition bio p q := bio_aux p q (S (wfp_size p)).

Lemma bio_aux_ok1 : ∀ (p q : wfprocess) n,
  n > size p → bio_aux p q n = true → p ≈ec q.
Proof.
  induction p as [p HI] using (measure_induction wfp_size).
  intros q n Hn Htrue. destruct n. inverts Hn.
  inverts Htrue.
  simpls.
  apply andb_prop in Htrue. destruct Htrue as [Htrue ?].
  apply andb_prop in Htrue. destruct Htrue as [Htrue ?].
  apply andb_prop in Htrue. destruct Htrue as [Htrue ?].
  apply andb_prop in Htrue. destruct Htrue as [Htrue ?].
  apply andb_prop in Htrue. destruct Htrue as [Htrue ?].

  cofix. constructor.
  splits. constructor. splits¬.

      introv H4.
      clear H H0 H2 H3 Htrue. rename H1 into H0.
      rewrite forallb_forall in H0.
      assert (Ht: {{q -- LabIn a ->> AA fp}}). assumption.
      lets H4´ : H4; apply in_der_ok_lr with (forbidden := nil) in H4.
      inverts H4 as H4.
      specialize (H0 _ H4).
      simpl in H0. rewrite existsb_exists in H0.
      destruct H0 as [[b q´] [Hin Heq]].
      apply andb_prop in Heq. destruct Heq as [Heq1 Heq2].
      apply beq_nat_true_iff in Heq1. subst a.
      apply in_der_ok_rl in Hin. ∃ q´; splits¬.
      ∃ (var_gen (GV p \u GV q)). split. unfolds¬ fresh_gvar.
      applys¬ notin_var_gen.
      split. unfolds¬ fresh_gvar. applys¬ notin_var_gen.
      symmetry. apply HI with (n:=n).
      unfold wfp_size; simpl.
      apply size_in with (m:=(wfp_Gvar (var_gen (GV p \u GV q)))) in Hin.
      rewrite Hin. nat_math. reflexivity.
      unfold wfp_size; simpl.
      apply size_in with (m:=(wfp_Gvar (var_gen (GV p \u GV q)))) in Hin.
      rewrite Hin in Hn. nat_math.
      reflexivity. cases_if¬.

      destruct H4 as (Y & Hfy & H4). rewrite Forall_to_conj_1 in Hfy.
      specialize (H0 _ H4).
      simpl in H0. rewrite existsb_exists in H0.
      destruct H0 as [[b q´] [Hin Heq]].
      apply andb_prop in Heq. destruct Heq as [Heq1 Heq2].
      apply beq_nat_true_iff in Heq1. subst a.
      ∃ q´; splits. apply¬ in_der_ok_rl. eassumption.
      ∃ (var_gen (GV p \u GV q)).
      split. unfolds¬ fresh_gvar. apply notin_var_gen. introv H. auto¬.
      split. unfolds¬ fresh_gvar. apply notin_var_gen. introv H. auto¬.
      symmetry. apply in_der_ok_rl in Hin. apply HI with (n:=n).
      apply size_in with (m:=(wfp_Gvar (var_gen (GV p \u GV q)))) in Hin.
      unfold wfp_size; simpl. rewrite Hin. nat_math. reflexivity.
      apply size_in with (m:=(wfp_Gvar (var_gen (GV p \u GV q)))) in Hin.
      simpl; rewrite Hin in Hn. nat_math. reflexivity. cases_if¬.
      rewrite <- inst_abs_subst_eq with (p := q) (a := b) in H; auto.

      clear H H0 H1 H2 Htrue. rename H3 into H0. introv H4.
      rewrite forallb_forall in H0.
      assert (Ht: {{q -- LabOut a p´´ ->> AP p´}}). assumption.
      apply out_der_ok in H4. specialize (H0 _ H4).
      simpl in H0. rewrite existsb_exists in H0.
      destruct H0 as [[[b m´] q´] [Hin Heq]].
      apply andb_prop in Heq. destruct Heq as [Heq Heq3].
      apply andb_prop in Heq. destruct Heq as [Heq1 Heq2].
      apply beq_nat_true_iff in Heq1. subst a.
      apply out_der_ok in Hin.
      ∃ q´ m´. intuition.
      symmetry. apply HI with (n:=n).
      unfold wfp_size; simpl; apply size_out in Hin. rewrite Hin. nat_math.
      apply size_out in Hin. simpl; rewrite Hin in Hn. nat_math. assumption.
      symmetry. apply HI with (n:=n).
      unfold wfp_size; simpl; apply size_out in Hin. rewrite Hin. nat_math.
      apply size_out in Hin. simpl; rewrite Hin in Hn. nat_math. cases_if¬.

      clear H0 H1 H2 H3 Htrue. rename H into H0. introv H4.
      cases_if¬.
      rewrite forallb_forall in H.
      assert (Ht: {{q -- LabRem X ->> AP p´}}). assumption.
      apply X_der_ok in H4. specialize (H _ H4).
      simpl in H. rewrite existsb_exists in H.
      destruct H as [[a q´] [Hin Heq]].
      apply andb_prop in Heq. destruct Heq as [Heq1 Heq2].
      cases_if¬.
      cases_if.
      subst a.
      apply X_der_ok in Hin. ∃ q´. splits¬.
      symmetry. apply HI with (n:=n).
      apply size_remove in Hin.
      unfold wfp_size; simpl; rewrite Hin. nat_math.
      apply size_remove in Hin. simpl; rewrite Hin in Hn. nat_math. assumption.

      clear H H0 H1 H3 Htrue. rename H2 into H0. introv H4.
      rewrite forallb_forall in H0.
      assert (Ht: {{p -- LabIn a ->> AA fp}}). assumption.
      lets H4´ : H4; apply in_der_ok_lr with (forbidden := nil) in H4.
      inverts H4 as H4.
      specialize (H0 _ H4).
      simpl in H0. rewrite existsb_exists in H0.
      destruct H0 as [[b q´] [Hin Heq]].
      apply andb_prop in Heq. destruct Heq as [Heq1 Heq2].
      apply beq_nat_true_iff in Heq1. subst a.
      ∃ q´; splits. apply¬ in_der_ok_rl. eassumption.
      ∃ (var_gen (GV p \u GV q)).
      split. unfolds¬ fresh_gvar. apply notin_var_gen. introv H. auto¬.
      split. unfolds¬ fresh_gvar. apply notin_var_gen. introv H. auto¬.
      apply HI with (n:=n).
      apply size_in with (m:=(wfp_Gvar (var_gen (GV p \u GV q)))) in Ht.
      unfold wfp_size; simpl. rewrite Ht. nat_math. reflexivity.
      apply size_in with (m:=(wfp_Gvar (var_gen (GV p \u GV q)))) in Ht.
      simpl; rewrite Ht in Hn. nat_math. reflexivity. cases_if¬.

      destruct H4 as (Y & Hfy & H4). rewrite Forall_to_conj_1 in Hfy.
      specialize (H0 _ H4).
      simpl in H0. rewrite existsb_exists in H0.
      destruct H0 as [[b q´] [Hin Heq]].
      apply andb_prop in Heq. destruct Heq as [Heq1 Heq2].
      apply beq_nat_true_iff in Heq1. subst a.
      ∃ q´; splits. apply¬ in_der_ok_rl. eassumption.
      ∃ (var_gen (GV p \u GV q)).
      split. unfolds¬ fresh_gvar. apply notin_var_gen. introv H. auto¬.
      split. unfolds¬ fresh_gvar. apply notin_var_gen. introv H. auto¬.
      apply HI with (n:=n).
      apply size_in with (m:=(wfp_Gvar (var_gen (GV p \u GV q)))) in Ht.
      unfold wfp_size; simpl. rewrite Ht. nat_math. reflexivity.
      apply size_in with (m:=(wfp_Gvar (var_gen (GV p \u GV q)))) in Ht.
      simpl; rewrite Ht in Hn. nat_math. reflexivity. cases_if¬.
      rewrite <- inst_abs_subst_eq with (p := p) (a := b) in H; auto.

      clear H H0 H1 H2 H3. introv H4.
      assert (Ht: {{p -- LabOut a p´´ ->> AP p´}}). assumption.
      apply out_der_ok in H4.
      forwards [Hfa _]: forallb_forall.
      forwards H0: Hfa Htrue.
      eassumption.
      simpls.
      rewrite existsb_exists in H0.
      destruct H0 as [[[b m´] q´] [Hin Heq]].
      apply andb_prop in Heq. destruct Heq as [Heq Heq3].
      apply andb_prop in Heq. destruct Heq as [Heq1 Heq2].
      apply beq_nat_true_iff in Heq1. subst a.
      ∃ q´ m´. split. apply out_der_ok. assumption.
      split. apply HI with (n:=n). apply size_out in Ht.
      unfold wfp_size; rewrite Ht. nat_math.
      apply size_out in Ht. rewrite Ht in Hn. nat_math. assumption.
      apply HI with (n:=n). apply size_out in Ht.
      unfold wfp_size; rewrite Ht. nat_math.
      apply size_out in Ht. rewrite Ht in Hn. nat_math.
      cases¬ (bio_aux p´´ m´ n).

      clear H H1 H2 H3 Htrue. introv H4.
      rewrite forallb_forall in H0.
      assert (Ht: {{p -- LabRem X ->> AP p´}}). assumption.
      apply X_der_ok in H4. specialize (H0 _ H4).
      simpl in H0. rewrite existsb_exists in H0.
      destruct H0 as [[a q´] [Hin Heq]].
      apply andb_prop in Heq. destruct Heq as [Heq1 Heq2].
      cases_if¬. cases_if¬.
      subst a.
      ∃ q´. split. applys¬ X_der_ok.
      apply HI with (n:=n). apply size_remove in Ht.
      unfold wfp_size; rewrite Ht. nat_math.
      apply size_remove in Ht. rewrite Ht in Hn. nat_math. assumption.
Qed.

Lemma bio_aux_ok2 : ∀ p q,
  p ≈ q → ∀ n, n > size p → bio_aux p q n = true.
Proof.
  induction p as [p HI] using (measure_induction wfp_size).
  intros q Hio n Hn.
  destruct n. inversion Hn.
  simpls¬. false. nat_math.
  simpls¬.
  repeat (apply andb_true_intro; splits~); apply forallb_forall.
intros [[a m] p´] Hin.
    apply out_der_ok in Hin.
    apply IObis_out in Hio; auto. specialize (Hio a p´ m Hin).
    destruct Hio as [q´ [m´ [Ht Hio]]].
    apply existsb_exists. ∃ (a, m´, q´). split.
    now apply out_der_ok.
    repeat (apply andb_true_intro; split).
    symmetry. apply beq_nat_refl.
    apply (HI p´). apply size_out in Hin.
    unfold wfp_size; simpl; nat_math.
    intuition. apply size_out in Hin; simpl; nat_math.
    apply (HI m). apply size_out in Hin.
    unfold wfp_size; simpl; nat_math.
    intuition. apply size_out in Hin; simpl; nat_math. auto¬.
intros [[a m] q´] Hin.
    apply out_der_ok in Hin.
    symmetry in Hio. apply IObis_out in Hio; auto. specialize (Hio a q´ m Hin).
    destruct Hio as [p´ [m´ [Ht Hio]]].
    apply existsb_exists. ∃ (a, m´, p´). split.
    now apply out_der_ok.
    repeat (apply andb_true_intro; split).
    symmetry. apply beq_nat_refl.
    eapply (HI p´ _ q´).
    symmetry. intuition. apply size_out in Ht.
    unfold wfp_size; simpl; nat_math.
    eapply (HI m´ _ m).
    intuition. apply size_out in Ht.
    unfold wfp_size; simpl; nat_math. auto¬.
intros [a p´] Hin. apply in_der_ok_rl in Hin.
    apply IObis_in in Hio; auto. specialize (Hio _ _ Hin).
    destruct Hio as [q´ [Ht Hio]].
    apply existsb_exists. lets Ht´ : Ht.
    apply in_der_ok_lr with (forbidden := nil) in Ht.
    inverts Ht as Ht.
      ∃ (a,q´). splits¬.
      repeat (apply andb_true_intro; split).
      symmetry. apply beq_nat_refl.
      apply HI. unfold wfp_size; simpl; lets Hin´ : Hin.
      apply size_in with (m:=(wfp_Gvar (var_gen (GV p \u GV q)))) in Hin´.
      rewrite Hin´ in Hn. nat_math. reflexivity.
      apply Hio. unfolds¬ fresh_gvar. applys¬ notin_var_gen.
      unfolds¬ fresh_gvar. applys¬ notin_var_gen.
      simpl; lets Hin´ : Hin.
      apply size_in with (m:=(wfp_Gvar (var_gen (GV p \u GV q)))) in Hin´.
      rewrite Hin´ in Hn. nat_math. reflexivity. reflexivity.

      destruct Ht as (Y & Hfy & Hyp).
      rewrite Forall_to_conj_1 in Hfy.
      ∃ (a, abs_subst q´ Y). splits¬.
      repeat (apply andb_true_intro; split).
      symmetry. apply beq_nat_refl.
      apply HI. unfold wfp_size; simpl; lets Hin´ : Hin.
      apply size_in with (m:=(wfp_Gvar (var_gen (GV p \u GV q)))) in Hin´.
      rewrite Hin´ in Hn. nat_math. reflexivity.
      rewrite <- inst_abs_subst_eq with (p := q) (a := a); auto.
      apply Hio. unfolds¬ fresh_gvar. applys¬ notin_var_gen.
      unfolds¬ fresh_gvar. applys¬ notin_var_gen.
      simpl; lets Hin´ : Hin.
      apply size_in with (m:=(wfp_Gvar (var_gen (GV p \u GV q)))) in Hin´.
      rewrite Hin´ in Hn. nat_math. reflexivity. reflexivity.

intros [a q´] Hin. apply in_der_ok_rl in Hin.
    symmetry in Hio. apply IObis_in in Hio; auto. specialize (Hio _ _ Hin).
    destruct Hio as [p´ [Ht Hio]].
    apply existsb_exists. lets Ht´ : Ht.
    apply in_der_ok_lr with (forbidden := nil) in Ht.
    inverts Ht as Ht.
      ∃ (a,p´). splits¬.
      repeat (apply andb_true_intro; split).
      symmetry. apply beq_nat_refl.
      apply HI. unfold wfp_size; simpl. lets Ht´´ : Ht.
      apply size_in with (m:=(wfp_Gvar (var_gen (GV p \u GV q)))) in Ht´.
      nat_math. reflexivity.
      symmetry. apply Hio.
      unfolds¬ fresh_gvar. applys¬ notin_var_gen.
      unfolds¬ fresh_gvar. applys¬ notin_var_gen.
      lets Ht´´ : Ht; apply size_in with (m:=(wfp_Gvar (var_gen (GV p \u GV q)))) in Ht´.
      simpl; rewrite Ht´ in Hn. nat_math. reflexivity. reflexivity.

      destruct Ht as (Y & Hfy & Hyp).
      rewrite Forall_to_conj_1 in Hfy.
      ∃ (a, abs_subst p´ Y). splits¬.
      repeat (apply andb_true_intro; splits).
      symmetry. apply beq_nat_refl.
      rewrite <- inst_abs_subst_eq with (p := p) (a := a); auto.
      apply HI. unfold wfp_size; simpl; lets Ht´´ : Ht´.
      apply size_in with (m:=(wfp_Gvar (var_gen (GV p \u GV q)))) in Ht´´.
      nat_math. reflexivity.
      symmetry. apply Hio. unfolds¬ fresh_gvar. applys¬ notin_var_gen.
      unfolds¬ fresh_gvar. applys¬ notin_var_gen.
      simpl; lets Ht´´ : Ht´.
      apply size_in with (m:=(wfp_Gvar (var_gen (GV p \u GV q)))) in Ht´´.
      rewrite Ht´´ in Hn. nat_math. reflexivity. reflexivity.
intros [X p´] Hin.
    apply X_der_ok in Hin.
    apply IObis_var in Hio; auto. specialize (Hio _ p´ Hin).
    destruct Hio as [q´ [Ht Hio]].
    apply existsb_exists. ∃ (X, q´). split.
    now apply X_der_ok.
    applys andb_true_intro. split.
    cases_if¬.
    cases_if¬.
    rewrite <- H.
    apply (HI p´).
    unfold wfp_size; simpl; apply size_remove in Hin. nat_math.
    intuition. simpl; apply size_remove in Hin. nat_math.
intros [X q´] Hin.
    apply X_der_ok in Hin.
    symmetry in Hio. apply IObis_var in Hio; auto. specialize (Hio _ q´ Hin).
    destruct Hio as [p´ [Ht Hio]].
    apply existsb_exists. ∃ (X, p´). split.
    now apply X_der_ok.
    applys andb_true_intro. split.
    cases_if¬.
    cases_if¬. rewrite <- H.
    eapply (HI _ _ q´).
    symmetry. intuition. apply size_remove in Ht. nat_math.

Grab Existential Variables.
  unfold wfp_size; apply size_remove in Ht. nat_math.
  unfold wfp_size; apply size_out in Ht. nat_math.
  unfold wfp_size; apply size_out in Ht. nat_math.
Qed.

Lemma bio_ok : ∀ p q,
  p ≈ q ↔ bio p q = true.
Proof.
  intros p q. unfold bio. split; intros Hio.
  apply bio_aux_ok2; trivial. unfold wfp_size; nat_math.
  rewrite IObis_IObis_ex. rewrite IObis_ex_eq_IObisC_ex.
  apply bio_aux_ok1 with (n:=(S (size p))); trivial. nat_math.
Qed.

Theorem IObis_constructive_decidable : ∀ p q, {p ≈ q} + {~(p ≈ q)}.
Proof.
  introv; tests: (bio p q = true); [left | right];
  [ | introv Hio; apply C]; applys¬ bio_ok.
Qed.

Theorem IObis_decidable : ∀ p q, decidable (p ≈ q).
Proof.
  introv; elim (IObis_constructive_decidable p q); unfold decidable; intuition.
Qed.