Section picalc_syntax.


Parameter name : Set.


Inductive Nlist : Set :=
  | empty : Nlist
  | cons : name → Nlist → Nlist.


Inductive Nlist_notin (x : name) : Nlist → Prop :=
  | Nlist_notin_empty : Nlist_notin x empty
  | Nlist_notin_cons :
      ∀ (y : name) (l : Nlist),
      x ≠ y → Nlist_notin x l → Nlist_notin x (cons y l).


Inductive proc : Set :=
  | nil : proc
  | bang : proc → proc
  | tau_pref : proc → proc
  | par : proc → proc → proc
  | sum : proc → proc → proc
  | nu : (name → proc) → proc
  | match_ : name → name → proc → proc
  | mismatch : name → name → proc → proc
  | in_pref : name → (name → proc) → proc
  | out_pref : name → name → proc → proc.


Inductive isin (x : name) : proc → Prop :=
  | isin_bang : ∀ p : proc, isin x p → isin x (bang p)
  | isin_tau : ∀ p : proc, isin x p → isin x (tau_pref p)
  | isin_par1 : ∀ p q : proc, isin x p → isin x (par p q)
  | isin_par2 : ∀ p q : proc, isin x q → isin x (par p q)
  | isin_sum1 : ∀ p q : proc, isin x p → isin x (sum p q)
  | isin_sum2 : ∀ p q : proc, isin x q → isin x (sum p q)
  | isin_nu :
      ∀ p : name → proc,
      (∀ z : name, isin x (p z)) → isin x (nu p)
  | isin_match1 :
      ∀ (p : proc) (y z : name), isin x p → isin x (match_ y z p)
  | isin_match2 : ∀ (p : proc) (y : name), isin x (match_ x y p)
  | isin_match3 : ∀ (p : proc) (y : name), isin x (match_ y x p)
  | isin_mismatch1 :
      ∀ (p : proc) (y z : name), isin x p → isin x (mismatch y z p)
  | isin_mismatch2 : ∀ (p : proc) (y : name), isin x (mismatch x y p)
  | isin_mismatch3 : ∀ (p : proc) (y : name), isin x (mismatch y x p)
  | isin_in1 :
      ∀ (p : name → proc) (y : name),
      (∀ z : name, isin x (p z)) → isin x (in_pref y p)
  | isin_in2 : ∀ p : name → proc, isin x (in_pref x p)
  | isin_out1 :
      ∀ (p : proc) (y z : name), isin x p → isin x (out_pref y z p)
  | isin_out2 : ∀ (p : proc) (y : name), isin x (out_pref x y p)
  | isin_out3 : ∀ (p : proc) (y : name), isin x (out_pref y x p).


Inductive notin (x : name) : proc → Prop :=
  | notin_nil : notin x nil
  | notin_bang : ∀ p : proc, notin x p → notin x (bang p)
  | notin_tau : ∀ p : proc, notin x p → notin x (tau_pref p)
  | notin_par :
      ∀ p q : proc, notin x p → notin x q → notin x (par p q)
  | notin_sum :
      ∀ p q : proc, notin x p → notin x q → notin x (sum p q)
  | notin_nu :
      ∀ p : name → proc,
      (∀ z : name, x ≠ z → notin x (p z)) → notin x (nu p)
  | notin_match :
      ∀ (p : proc) (y z : name),
      x ≠ y → x ≠ z → notin x p → notin x (match_ y z p)
  | notin_mismatch :
      ∀ (p : proc) (y z : name),
      x ≠ y → x ≠ z → notin x p → notin x (mismatch y z p)
  | notin_in :
      ∀ (p : name → proc) (y : name),
      x ≠ y →
      (∀ z : name, x ≠ z → notin x (p z)) → notin x (in_pref y p)
  | notin_out :
      ∀ (p : proc) (y z : name),
      x ≠ y → x ≠ z → notin x p → notin x (out_pref y z p).


Axiom LEM_OC : ∀ (p : proc) (x : name), isin x p ∨ notin x p.


Lemma LEM_name : ∀ x y : name, x = y ∨ x ≠ y.

Proof.

intros; elim (LEM_OC (match_ y y nil) x); intro;
 [ left; inversion_clear H; [ inversion_clear H0 | trivial | trivial ]
 | right; inversion_clear H; assumption ].

Qed.


Axiom
  unsat :
    ∀ (p : proc) (l : Nlist),
    ∃ x : name, notin x p ∧ Nlist_notin x l.


Lemma isin_to_notin : ∀ (p : proc) (x : name), ¬ notin x p → isin x p.

Proof.

intros; elim (LEM_OC p x); intro;
 [ assumption | absurd (notin x p); assumption ].

Qed.

Lemma notin_to_isin : ∀ (p : proc) (x : name), ¬ isin x p → notin x p.

Proof.

intros; elim (LEM_OC p x); intro;
 [ absurd (isin x p); assumption | assumption ].

Qed.


Lemma Sep_proc :
 ∀ (x y : name) (p : proc), isin x p → notin y p → x ≠ y.

Proof.

simple induction p; intros.

inversion_clear H.

inversion_clear H0.
inversion_clear H1.
apply H; assumption.

inversion_clear H0.
inversion_clear H1.
apply H; assumption.

inversion_clear H2.
inversion_clear H1.
apply H; assumption.
apply H0; assumption.

inversion_clear H2.
inversion_clear H1.
apply H; assumption.
apply H0; assumption.

inversion_clear H1.
inversion_clear H0.

elim (unsat (nu p0) (cons x (cons y empty))); intros.
inversion_clear H0.
inversion_clear H4.
inversion_clear H5.
clear H6; apply H with x0; [ apply H1 | apply H2; auto ].

inversion_clear H1.
inversion_clear H0; [ apply H; assumption | auto | auto ].

inversion_clear H1.
inversion_clear H0; [ apply H; assumption | auto | auto ].

inversion_clear H1.
inversion_clear H0.
elim (unsat (nu p0) (cons x (cons y (cons n empty)))); intros.
inversion_clear H0.
inversion_clear H5.
inversion_clear H6.
inversion_clear H7.
clear H8; apply H with x0; [ apply H1 | apply H3; auto ].
auto.

inversion_clear H1.
inversion_clear H0; [ apply H; assumption | auto | auto ].

Qed.


Inductive f_act : Set :=
  | tau : f_act
  | Out : name → name → f_act.


Inductive f_act_isin (x : name) : f_act → Prop :=
  | f_act_isin_Out1 : ∀ y : name, f_act_isin x (Out x y)
  | f_act_isin_Out2 : ∀ y : name, f_act_isin x (Out y x).

Inductive f_act_notin (x : name) : f_act → Prop :=
  | f_act_notin_tau : f_act_notin x tau
  | f_act_notin_Out :
      ∀ y z : name, x ≠ y → x ≠ z → f_act_notin x (Out y z).

Definition f_act_notin_ho (x : name) (a : name → f_act) :=
  ∀ y : name, x ≠ y → f_act_notin x (a y).


Lemma Sep_f_act :
 ∀ (a : f_act) (x y : name), f_act_isin x a → f_act_notin y a → x ≠ y.

Proof.

simple induction a; intros.

inversion_clear H.

inversion_clear H0.
inversion_clear H; auto.

Qed.


Inductive b_act : Set :=
  | In : name → b_act
  | bOut : name → b_act.


Inductive b_act_isin (x : name) : b_act → Prop :=
  | b_act_isin_In : b_act_isin x (In x)
  | b_act_isin_bOut : b_act_isin x (bOut x).

Inductive b_act_notin (x : name) : b_act → Prop :=
  | b_act_notin_In : ∀ y : name, x ≠ y → b_act_notin x (In y)
  | b_act_notin_bOut : ∀ y : name, x ≠ y → b_act_notin x (bOut y).

Definition b_act_notin_ho (x : name) (a : name → b_act) :=
  ∀ y : name, x ≠ y → b_act_notin x (a y).


Lemma Sep_b_act :
 ∀ (a : b_act) (x y : name), b_act_isin x a → b_act_notin y a → x ≠ y.

Proof.

simple induction a; intros.

inversion_clear H0.
inversion_clear H; auto.

inversion_clear H0.
inversion_clear H; auto.

Qed.

End picalc_syntax.


Section picalc_LTS.


Inductive ftrans : proc → f_act → proc → Prop :=
  | TAU : ∀ p : proc, ftrans (tau_pref p) tau p
  | OUT : ∀ (p : proc) (x y : name), ftrans (out_pref x y p) (Out x y) p
  | fSUM1 :
      ∀ (p1 p2 p : proc) (a : f_act),
      ftrans p1 a p → ftrans (sum p1 p2) a p
  | fSUM2 :
      ∀ (p1 p2 p : proc) (a : f_act),
      ftrans p2 a p → ftrans (sum p1 p2) a p
  | fPAR1 :
      ∀ (p1 p2 p : proc) (a : f_act),
      ftrans p1 a p → ftrans (par p1 p2) a (par p p2)
  | fPAR2 :
      ∀ (p1 p2 p : proc) (a : f_act),
      ftrans p2 a p → ftrans (par p1 p2) a (par p1 p)
  | fMATCH :
      ∀ (x : name) (p q : proc) (a : f_act),
      ftrans p a q → ftrans (match_ x x p) a q
  | fMISMATCH :
      ∀ (x y : name) (p q : proc) (a : f_act),
      x ≠ y → ftrans p a q → ftrans (mismatch x y p) a q
  | fBANG :
      ∀ (p q : proc) (a : f_act),
      ftrans (par p (bang p)) a q → ftrans (bang p) a q
  | COM1 :
      ∀ (p1 p2 q2 : proc) (q1 : name → proc) (x y : name),
      btrans p1 (In x) q1 →
      ftrans p2 (Out x y) q2 → ftrans (par p1 p2) tau (par (q1 y) q2)
  | COM2 :
      ∀ (p1 p2 q1 : proc) (q2 : name → proc) (x y : name),
      ftrans p1 (Out x y) q1 →
      btrans p2 (In x) q2 → ftrans (par p1 p2) tau (par q1 (q2 y))
  | fRES :
      ∀ (p1 p2 : name → proc) (a : f_act) (l : Nlist),
      (∀ y : name,
       notin y (nu p1) →
       notin y (nu p2) →
       Nlist_notin y l → f_act_notin y a → ftrans (p1 y) a (p2 y)) →
      ftrans (nu p1) a (nu p2)
  | CLOSE1 :
      ∀ (p1 p2 : proc) (q1 q2 : name → proc) (x : name),
      btrans p1 (In x) q1 →
      btrans p2 (bOut x) q2 →
      ftrans (par p1 p2) tau (nu (fun z : name ⇒ par (q1 z) (q2 z)))
  | CLOSE2 :
      ∀ (p1 p2 : proc) (q1 q2 : name → proc) (x : name),
      btrans p1 (bOut x) q1 →
      btrans p2 (In x) q2 →
      ftrans (par p1 p2) tau (nu (fun z : name ⇒ par (q1 z) (q2 z)))
with btrans : proc → b_act → (name → proc) → Prop :=
  | IN : ∀ (p : name → proc) (x : name), btrans (in_pref x p) (In x) p
  | bSUM1 :
      ∀ (p1 p2 : proc) (a : b_act) (p : name → proc),
      btrans p1 a p → btrans (sum p1 p2) a p
  | bSUM2 :
      ∀ (p1 p2 : proc) (a : b_act) (p : name → proc),
      btrans p2 a p → btrans (sum p1 p2) a p
  | bPAR1 :
      ∀ (p1 p2 : proc) (a : b_act) (p : name → proc),
      btrans p1 a p → btrans (par p1 p2) a (fun x : name ⇒ par (p x) p2)
  | bPAR2 :
      ∀ (p1 p2 : proc) (a : b_act) (p : name → proc),
      btrans p2 a p → btrans (par p1 p2) a (fun x : name ⇒ par p1 (p x))
  | bMATCH :
      ∀ (x : name) (p : proc) (a : b_act) (q : name → proc),
      btrans p a q → btrans (match_ x x p) a q
  | bMISMATCH :
      ∀ (x y : name) (p : proc) (a : b_act) (q : name → proc),
      x ≠ y → btrans p a q → btrans (mismatch x y p) a q
  | bBANG :
      ∀ (p : proc) (a : b_act) (q : name → proc),
      btrans (par p (bang p)) a q → btrans (bang p) a q
  | bRES :
      ∀ (p1 : name → proc) (a : b_act) (p2 : name → name → proc)
        (l : Nlist),
      (∀ y : name,
       notin y (nu p1) →
       notin y (nu (fun z : name ⇒ nu (p2 z))) →
       b_act_notin y a → Nlist_notin y l → btrans (p1 y) a (p2 y)) →
      btrans (nu p1) a (fun y : name ⇒ nu (fun z : name ⇒ p2 z y))
  | OPEN :
      ∀ (p1 p2 : name → proc) (x : name) (l : Nlist),
      (∀ y : name,
       notin y (nu p1) →
       notin y (nu p2) →
       x ≠ y → Nlist_notin y l → ftrans (p1 y) (Out x y) (p2 y)) →
      btrans (nu p1) (bOut x) p2.

End picalc_LTS.


Section picalc_SLB.


CoInductive StBisim : proc → proc → Prop :=
    sb :
      ∀ p q : proc,
      (∀ a : f_act,
       (∀ p1 : proc,
        ftrans p a p1 → ∃ q1 : proc, ftrans q a q1 ∧ StBisim p1 q1) ∧
       (∀ q1 : proc,
        ftrans q a q1 → ∃ p1 : proc, ftrans p a p1 ∧ StBisim p1 q1)) ∧
      (∀ x : name,
       (∀ p1 : name → proc,
        btrans p (In x) p1 →
        ∃ q1 : name → proc,
          btrans q (In x) q1 ∧ (∀ y : name, StBisim (p1 y) (q1 y))) ∧
       (∀ q1 : name → proc,
        btrans q (In x) q1 →
        ∃ p1 : name → proc,
          btrans p (In x) p1 ∧ (∀ y : name, StBisim (p1 y) (q1 y)))) ∧
      (∀ x : name,
       (∀ p1 : name → proc,
        btrans p (bOut x) p1 →
        ∃ q1 : name → proc,
          btrans q (bOut x) q1 ∧
          (∀ y : name,
           notin y (nu p1) → notin y (nu q1) → StBisim (p1 y) (q1 y))) ∧
       (∀ q1 : name → proc,
        btrans q (bOut x) q1 →
        ∃ p1 : name → proc,
          btrans p (bOut x) p1 ∧
          (∀ y : name,
           notin y (nu p1) → notin y (nu q1) → StBisim (p1 y) (q1 y)))) →
      StBisim p q.


Inductive Op_StBisim (R : proc → proc → Prop) (p q : proc) : Prop :=
    op_sb :
      (∀ a : f_act,
       (∀ p1 : proc,
        ftrans p a p1 → ∃ q1 : proc, ftrans q a q1 ∧ R p1 q1) ∧
       (∀ q1 : proc,
        ftrans q a q1 → ∃ p1 : proc, ftrans p a p1 ∧ R p1 q1)) ∧
      (∀ x : name,
       (∀ p1 : name → proc,
        btrans p (In x) p1 →
        ∃ q1 : name → proc,
          btrans q (In x) q1 ∧ (∀ y : name, R (p1 y) (q1 y))) ∧
       (∀ q1 : name → proc,
        btrans q (In x) q1 →
        ∃ p1 : name → proc,
          btrans p (In x) p1 ∧ (∀ y : name, R (p1 y) (q1 y)))) ∧
      (∀ x : name,
       (∀ p1 : name → proc,
        btrans p (bOut x) p1 →
        ∃ q1 : name → proc,
          btrans q (bOut x) q1 ∧
          (∀ y : name,
           notin y (nu p1) → notin y (nu q1) → R (p1 y) (q1 y))) ∧
       (∀ q1 : name → proc,
        btrans q (bOut x) q1 →
        ∃ p1 : name → proc,
          btrans p (bOut x) p1 ∧
          (∀ y : name,
           notin y (nu p1) → notin y (nu q1) → R (p1 y) (q1 y)))) →
      Op_StBisim R p q.


Definition Inclus (R1 R2 : proc → proc → Prop) :=
  ∀ p1 p2 : proc, R1 p1 p2 → R2 p1 p2.


Inductive StBisim' (p1 p2 : proc) : Prop :=
    Co_Ind :
      ∀ R : proc → proc → Prop,
      Inclus R (Op_StBisim R) → R p1 p2 → StBisim' p1 p2.

End picalc_SLB.