# Library CCS.Trans_Sys

Section TS.

Variable process action : Set.
Variable T : action.
Variable transition : process action process Prop.
Hypothesis eqT_dec : a : action, a = T a T.

Inductive weak_derivative : process action process Prop :=
| eps : p : process, weak_derivative p T p
| w_single :
(a : action) (p q : process),
transition p a q weak_derivative p a q
| w_tau_left :
(a : action) (p p' q : process),
transition p T p' weak_derivative p' a q weak_derivative p a q
| w_tau_right :
(a : action) (p q q' : process),
transition q' T q weak_derivative p a q' weak_derivative p a q.
Hint Resolve w_single eps.

Inductive derivative : process action process Prop :=
| single :
(a : action) (p q : process),
transition p a q derivative p a q
| tau_left :
(a : action) (p p' q : process),
transition p T p' derivative p' a q derivative p a q
| tau_right :
(a : action) (p q q' : process),
transition q' T q derivative p a q' derivative p a q.

Hint Resolve single.

Lemma deriv_weak_deriv :
(p p' : process) (a : action),
derivative p a p' weak_derivative p a p'.

intros p p' a H; elim H; clear H; auto with v62.
clear p p' a.
intros a p p' q tr de we.
apply w_tau_left with p'; try trivial with v62.

clear p p' a; intros a p q q' tr de we.
apply w_tau_right with q'; try trivial with v62.

Qed.

Hint Resolve deriv_weak_deriv.

Lemma weak_deriv_deriv :
(p p' : process) (a : action),
weak_derivative p a p' a T derivative p a p'.
intros p p' a H; elim H; clear H p p' a.
unfold not in |- ×.
intros p H; cut False; auto with v62.
intros H1; elim H1.

intros a p q tr H; auto with v62.

intros a p p' q tr we H_ind not_eq.
apply tau_left with p'; auto with v62.

intros a p q q' tr we H_ind notEq.
apply tau_right with q'; auto with v62.
Qed.

Hint Resolve weak_deriv_deriv.

Lemma weak_deriv_tau_left :
(p p' p'' : process) (a : action),
weak_derivative p T p'
weak_derivative p' a p'' weak_derivative p a p''.

cut
( (p : process) (a : action) (p' : process),
weak_derivative p a p'
a = T
(p'' : process) (b : action),
weak_derivative p' b p'' weak_derivative p b p'').
intros H p p' p'' a we we'; apply (H p T p'); auto with v62.

simple induction 1.
simple induction 1; auto with v62.

clear H p' a p.
intros a p q Tpq eqT p'' b we.
rewrite eqT in Tpq.
apply w_tau_left with q; auto with v62.

clear H p p' a.
intros a p p' q Tpq we H_rec eqT p'' b we'.
apply w_tau_left with p'; auto with v62.

clear H p a p'.
intros a p q q' Tr we H_rec eqT p'' b we'.
apply (H_rec eqT).
apply w_tau_left with q; auto with v62.

Qed.

Lemma weak_deriv_tau_right :
(p p' p'' : process) (a : action),
weak_derivative p a p'
weak_derivative p' T p'' weak_derivative p a p''.

cut
( (p' : process) (a : action) (p'' : process),
weak_derivative p' a p''
a = T
(p : process) (b : action),
weak_derivative p b p' weak_derivative p b p'').
intros H p p' p'' a we we1; apply (H p' T p''); auto with v62.

intros p' a p'' H; elim H; clear H a p' p''; auto with v62.
intros a p q tr eqT p0 b we.
apply w_tau_right with p; auto with v62.
rewrite eqT in tr; auto with v62.

intros a p q q' tr we H_rec eqT p0 b we'.
apply (H_rec eqT).
apply w_tau_right with p; auto with v62.

intros a p q q' tr we H_rec eqT p0 b we'.
apply w_tau_right with q'; auto with v62.

Qed.

Lemma w_deriv_tau_left :
(p p' p'' : process) (a : action),
weak_derivative p T p' derivative p' a p'' derivative p a p''.

cut
( (p : process) (a : action) (p' : process),
weak_derivative p a p'
a = T
(p'' : process) (b : action),
derivative p' b p'' derivative p b p'').
intros H p p' p'' a de de1; apply (H p T p'); auto with v62.

intros p a p' H; elim H; clear H a p p'; auto with v62.
intros a p q Tpq eqT p'' b de.
rewrite eqT in Tpq.
apply tau_left with q; auto with v62.

intros a p p' q tr de H_ind eqT p'' d de'.
apply tau_left with p'; auto with v62.

intros a p q q' Tr de H_ind eqT p'' b de'.
apply (H_ind eqT).
apply tau_left with q; auto with v62.

Qed.

Lemma w_deriv_tau_right :
(p p' p'' : process) (a : action),
derivative p a p' weak_derivative p' T p'' derivative p a p''.

cut
( (p' : process) (a : action) (p'' : process),
weak_derivative p' a p''
a = T
(p : process) (b : action), derivative p b p' derivative p b p'').
intros H p p' p'' a de de1; apply (H p' T p''); auto with v62.

intros p' a p'' H; elim H; clear H a p' p''.
auto with v62.

intros a p q tr eqT p0 b we.
apply tau_right with p; auto with v62.
rewrite eqT in tr; auto with v62.

intros a p q q' tr we H_rec eqT p0 b we'.
apply (H_rec eqT).
apply tau_right with p; auto with v62.

intros a p q q' tr we H_rec eqT p0 b we'.
apply tau_right with q'; auto with v62.

Qed.

Lemma deriv_tau_left :
(p p' p'' : process) (a : action),
derivative p T p' derivative p' a p'' derivative p a p''.

intros p p' p'' a pp' p_p''.
apply w_deriv_tau_left with p'; auto with v62.
Qed.

Lemma deriv_tau_right :
(p p' p'' : process) (a : action),
derivative p a p' derivative p' T p'' derivative p a p''.

intros p p' p'' a de1 de2.
apply w_deriv_tau_right with p'; auto with v62.
Qed.

CoInductive strong_eq : process process Prop :=
str_eq :
p q : process,
( (a : action) (p' : process),
transition p a p'
q' : process, transition q a q' strong_eq p' q')
( (a : action) (q' : process),
transition q a q'
p' : process, transition p a p' strong_eq p' q')
strong_eq p q.

Lemma refl_strong_eq : p : process, strong_eq p p.
cofix.
intros p; apply str_eq.
intros a p' trans; p'; split; auto with v62.
intros a p' trans; p'; split; auto with v62.
Qed.

Hint Resolve refl_strong_eq.

Lemma sym_strong_eq : p q : process, strong_eq p q strong_eq q p.
cofix.
intros p q H; inversion_clear H.
apply str_eq.
intros a q'.
intros trans.
elim (H1 a q' trans); clear H1.
intros p' H; elim H; p'; split; auto with v62.
intros a p' trans.
elim (H0 a p' trans); clear H0.
intros q' H; elim H; clear H.
intros trans1 str.
q'; split; auto with v62.
Qed.

Hint Immediate sym_strong_eq.

Lemma trans_strong_eq :
p q r : process, strong_eq p q strong_eq q r strong_eq p r.

cofix.
intros p q r pq qr.
inversion_clear pq; inversion_clear qr.
apply str_eq.
intros a p' tp.
cut ( q' : process, transition q a q' strong_eq p' q').
intros G; elim G; clear G.
intros q' G; elim G.
intros tq pq'; elim (H1 a q' tq).
clear G.
intros r' G; elim G; clear G.
intros tr qr'; r'; split; auto with v62.
apply trans_strong_eq with q'; auto with v62.
elim (H a p' tp).
intros q' G; elim G; clear G.
intros tq pq'.
q'; split; auto with v62.
intros a r' tr.
cut ( q' : process, transition q a q' strong_eq q' r').
intros G; elim G; clear G.
intros q' G; elim G; clear G.
intros tq qr'.
elim (H0 a q' tq).
intros p' G; elim G; clear G.
intros tp pq'; p'; split; auto with v62.
apply trans_strong_eq with q'; auto with v62.
elim (H2 a r' tr).
intros q' G; elim G; clear G.
intros tq qr'; q'; split; auto with v62.
Qed.

CoInductive weak_eq : process process Prop :=
w_eq :
p q : process,
( (a : action) (p' : process),
transition p a p'
q' : process, weak_derivative q a q' weak_eq p' q')
( (a : action) (q' : process),
transition q a q'
p' : process, weak_derivative p a p' weak_eq p' q')
weak_eq p q.

Lemma refl_weak_eq : p : process, weak_eq p p.
cofix.
intros p; apply w_eq.
intros a p' trans; p'; split; auto with v62.
intros a p' trans; p'; split; auto with v62.
Qed.

Hint Resolve refl_weak_eq.

Lemma sym_weak_eq : p q : process, weak_eq p q weak_eq q p.
cofix.
intros p q H; inversion_clear H.
apply w_eq.
intros a q'.
intros trans.
elim (H1 a q' trans); clear H1.
intros p' H; elim H; p'; split; auto with v62.
intros a p' trans.
elim (H0 a p' trans); clear H0.
intros q' H; elim H; clear H.
intros trans1 str.
q'; split; auto with v62.
Qed.

Hint Immediate sym_weak_eq.

Remark Hint_Trans :
(q q' r : process) (a : action),
weak_derivative q a q'
weak_eq q r r' : process, weak_derivative r a r' weak_eq q' r'.

intros q q' r a H.
generalize r; clear r.
elim H; clear H.
intros p r we; r; split; auto with v62.

clear a q q'; intros a p q tr r we.
inversion_clear we.
apply (H a q tr).

clear q q' a; intros a p p' q tr wd H_ind r we.
cut ( r'' : process, weak_derivative r T r'' weak_eq p' r'').
intros H.
elim H; clear H.
intros r'' Hr''; elim Hr''; clear Hr''; intros rTr'' we'.
cut ( r' : process, weak_derivative r'' a r' weak_eq q r').
intros H; elim H; clear H.
intros r' Hr'; elim Hr'; clear Hr'; intros wde we''.
r'; split; auto with v62.
apply (weak_deriv_tau_left r r'' r' a); auto with v62.

apply (H_ind r''); auto with v62.

inversion_clear we.
apply (H T p' tr); auto with v62.

clear q q' a; intros a p q q' tr wd H_ind r we.
cut ( r'' : process, weak_derivative r a r'' weak_eq q' r'').
intros H; elim H; clear H.
intros r'' Hr''; elim Hr''; clear Hr''; intros wd' we'.
cut ( r' : process, weak_derivative r'' T r' weak_eq q r').
intros H; elim H; clear H.
intros r' Hr'; elim Hr'; intros wd'' we''.
r'; split; auto with v62.
apply (weak_deriv_tau_right r r'' r' a); auto with v62.

inversion_clear we'; auto with v62.

apply (H_ind r we); auto with v62.

Qed.

Lemma trans_weak_eq :
p q r : process, weak_eq p q weak_eq q r weak_eq p r.
cofix.
intros p q r pq qr.
apply w_eq.

intros a p' tr.
cut ( q' : process, weak_derivative q a q' weak_eq p' q').
intros H; elim H; clear H; intros q' Hq'; elim Hq'; clear Hq'; intros wd we.
cut ( r' : process, weak_derivative r a r' weak_eq q' r').
intros Hr'; elim Hr'; clear Hr'; intros r' Hr'; elim Hr'; clear Hr';
intros wd' we'.
r'; split; auto with v62.
apply trans_weak_eq with q'; auto with v62.
apply (Hint_Trans q q' r); auto with v62.
inversion_clear pq; auto with v62.

intros a r' tr.
cut ( q' : process, weak_derivative q a q' weak_eq q' r').
intros H; elim H; clear H; intros q' Hq'; elim Hq'; clear Hq'; intros wd we.
cut ( p' : process, weak_derivative p a p' weak_eq q' p').
intros H; elim H; clear H; intros p' Hp'; elim Hp'; clear Hp'; intros wd' we'.
p'; split; auto with v62.
apply trans_weak_eq with q'; auto with v62.
apply (Hint_Trans q q' p a); auto with v62.
inversion_clear qr; auto with v62.
Qed.

CoInductive weak_eq1 : process process Prop :=
w_eq1 :
p q : process,
( (a : action) (p' : process),
derivative p a p'
q' : process, weak_derivative q a q' weak_eq1 p' q')
( (a : action) (q' : process),
derivative q a q'
p' : process, weak_derivative p a p' weak_eq1 p' q')
weak_eq1 p q.

Lemma weak_eq_deriv :
p q : process,
weak_eq p q
(a : action) (p' : process),
derivative p a p'
q' : process, weak_derivative q a q' weak_eq p' q'.

intros p q we a p' de.
generalize we.
generalize q.
elim de; clear de we a p p' q.
intros a p p' tr q we.
inversion we.
elim (H a p' tr); clear H H0.
intros q' H; elim H; clear H; intros wde we'.
q'; split; assumption.

intros a p p1 p' tr de H_ind q we.
cut ( q1 : process, weak_derivative q T q1 weak_eq p1 q1).
intros H; elim H; clear H.
intros q1 H; elim H; clear H; intros wde we'.
cut ( q' : process, weak_derivative q1 a q' weak_eq p' q').
intros H; elim H; clear H.
intros q' H; elim H; clear H; intros wde1 we1.
q'; split; try try try trivial with v62.
apply weak_deriv_tau_left with q1; try try trivial with v62.

apply (H_ind q1); try try trivial with v62.

inversion_clear we.
apply (H T p1); try try trivial with v62.

intros a p p' p1 tr de H_ind q we.
cut ( q1 : process, weak_derivative q a q1 weak_eq p1 q1).
intros H; elim H; clear H.
intros q1 H; elim H; clear H; intros wde we1.
cut ( q' : process, weak_derivative q1 T q' weak_eq p' q').
intros H; elim H; clear H.
intros q' H; elim H; clear H; intros wde1 we'.
q'; split; try try try trivial with v62.
apply weak_deriv_tau_right with q1; try try trivial with v62.

inversion_clear we1.
apply (H T p'); try try trivial with v62.

apply (H_ind q we).
Qed.

Lemma weak_eq_deriv_sym :
p q : process,
weak_eq p q
(a : action) (q' : process),
derivative q a q'
p' : process, weak_derivative p a p' weak_eq p' q'.

intros p q we a q' de.
cut (weak_eq q p); auto with v62.
intros we'.
elim (weak_eq_deriv q p we' a q' de).
intros p' H; elim H; intros w_de we''.
p'; split; auto with v62.

Qed.

Lemma weak_eq1_weak_eq : p q : process, weak_eq1 p q weak_eq p q.
cofix.
intros p q we1.
apply w_eq.
intros a p' tr.
inversion we1.
elim (H a p').
intros q' G; elim G; clear G; intros wde we1'.
q'; split; try try try trivial with v62.
apply weak_eq1_weak_eq; assumption.

apply single; assumption.

intros a q' tr.
inversion we1.
elim (H0 a q').
intros p' G; elim G; intros wde we1'.
p'; split; try try try trivial with v62.
apply weak_eq1_weak_eq; assumption.

apply single; try try trivial with v62.
Qed.

Hint Immediate weak_eq1_weak_eq.

Lemma weak_eq_weak_eq1 : p q : process, weak_eq p q weak_eq1 p q.

cofix.
intros p q we.
apply w_eq1.
intros a p' de.
cut ( q' : process, weak_derivative q a q' weak_eq p' q').
intros H; elim H; clear H.
intros q' H; elim H; clear H; intros wde we'.
q'; split; try try try trivial with v62.
apply weak_eq_weak_eq1; try try trivial with v62.

elim (weak_eq_deriv p q we a p' de).
intros q' H; q'; assumption.

intros a q' de.
cut ( p' : process, weak_derivative p a p' weak_eq p' q').
intros H; elim H; clear H.
intros p' H; elim H; clear H; intros wde we'.
p'; split; try try try try trivial with v62.
apply weak_eq_weak_eq1; try try try trivial with v62.

elim (weak_eq_deriv_sym p q we a q' de).
intros p' H; p'; assumption.

Qed.

Hint Immediate weak_eq_weak_eq1.

Lemma refl_weak_eq1 : p : process, weak_eq1 p p.

auto with v62.
Qed.

Lemma sym_weak_eq1 : p q : process, weak_eq1 p q weak_eq1 q p.

intros.
apply weak_eq_weak_eq1.
apply sym_weak_eq; auto with v62.

Qed.

Lemma trans_weak_eq1 :
p q r : process, weak_eq1 p q weak_eq1 q r weak_eq1 p r.

intros p q r pq qr.
apply weak_eq_weak_eq1.
apply trans_weak_eq with q; auto with v62.

Qed.

Definition obs_eq (p q : process) : Prop :=
( (a : action) (p' : process),
transition p a p'
q' : process, derivative q a q' weak_eq p' q')
( (a : action) (q' : process),
transition q a q'
p' : process, derivative p a p' weak_eq p' q').

Lemma refl_obs_eq : p : process, obs_eq p p.
unfold obs_eq in |- ×.
split; intros a p' trans; p'; split; auto with v62.
Qed.

Hint Immediate refl_obs_eq.

Lemma sym_obs_eq : p q : process, obs_eq p q obs_eq q p.
unfold obs_eq in |- ×.
intros p q.
intros H; elim H; clear H; intros Hp Hq.
split.
auto with v62.
intros a q' tr.
elim (Hq a q' tr); clear Hq.
intros p' H; elim H; clear H; intros de we; p'; split; auto with v62.
intros a p' tr.
elim (Hp a p' tr); clear Hp.
intros q' H; elim H; clear H; intros de we; q'; split; auto with v62.
Qed.

Hint Immediate sym_obs_eq.

Definition obs_eq1 (p q : process) : Prop :=
( (a : action) (p' : process),
derivative p a p'
q' : process, derivative q a q' weak_eq p' q')
( (a : action) (q' : process),
derivative q a q'
p' : process, derivative p a p' weak_eq p' q').

Lemma obs_eq1_obs_eq : p q : process, obs_eq1 p q obs_eq p q.
intros p q oe.
unfold obs_eq in |- *; split; elim oe; auto with v62.
Qed.

Hint Resolve obs_eq1_obs_eq.

Remark half_obs_eq_obs_eq1 :
p q : process,
obs_eq p q
(a : action) (p' : process),
derivative p a p' q' : process, derivative q a q' weak_eq p' q'.

intros p q oe a p' de; generalize oe; generalize q; clear oe q.
elim de; clear de a p p'.
intros a p p' tr q oe.
unfold obs_eq in oe; elim oe; clear oe; intros oe_l oe_r; clear oe_r.
auto with v62.

intros a p p1 p' tr de H_ind q oe.
cut ( q1 : process, derivative q T q1 weak_eq p1 q1).
intros H; elim H; clear H.
intros q1 H; elim H; clear H; intros de' we.
cut ( q' : process, weak_derivative q1 a q' weak_eq p' q').
intros H; elim H; clear H.
intros q' H; elim H; intros de'' we'.
q'; split; auto with v62.
elim eqT_dec with a.
intros a_T.
rewrite a_T in de''.
rewrite a_T.
apply w_deriv_tau_right with q1; auto with v62.

intros dif_a_T.
apply weak_deriv_deriv.
apply weak_deriv_tau_left with q1; auto with v62.

auto with v62.

cut (weak_eq1 p1 q1); auto with v62.
intros we1.
cut ( q' : process, weak_derivative q1 a q' weak_eq1 p' q').
intros H; elim H; clear H; intros q' H; elim H; intros de'' we1'; q';
split; auto with v62.

inversion_clear we1; auto with v62.

unfold obs_eq in oe; elim oe; auto with v62.

intros a p p' p1 tr de H_ind q oe.
cut ( q1 : process, derivative q a q1 weak_eq p1 q1).
intros H; elim H; clear H.
intros q1 H; elim H; clear H; intros de1 we1.
cut ( q' : process, weak_derivative q1 T q' weak_eq p' q').
intros H; elim H; clear H; intros q' H; elim H; intros de2 we.
q'; split; auto with v62.
apply w_deriv_tau_right with q1; auto with v62.

inversion_clear we1; auto with v62.

apply (H_ind q); auto with v62.

Qed.

Lemma obs_eq_obs_eq1 : p q : process, obs_eq p q obs_eq1 p q.

intros p q oe.
unfold obs_eq1 in |- *; split.
exact (half_obs_eq_obs_eq1 p q oe).

cut
( (a : action) (q' : process),
derivative q a q'
p' : process, derivative p a p' weak_eq q' p').
intros H a q' de.
elim (H a q' de); clear H.
intros p' H; elim H; clear H; intros; p'; split; auto with v62.

cut (obs_eq q p); auto with v62.
exact (half_obs_eq_obs_eq1 q p).

Qed.

Hint Resolve obs_eq_obs_eq1.

Lemma refl_obs_eq1 : p : process, obs_eq1 p p.

auto with v62.
Qed.

Hint Immediate refl_obs_eq1.

Lemma sym_obs_eq1 : p q : process, obs_eq1 p q obs_eq1 q p.
intros.
apply obs_eq_obs_eq1.
apply sym_obs_eq.
auto with v62.
Qed.

Hint Immediate sym_obs_eq1.

Remark half_trans_obs_eq1 :
p q r : process,
obs_eq1 p q
obs_eq1 q r
(a : action) (p' : process),
derivative p a p' r' : process, derivative r a r' weak_eq p' r'.

intros p q r pq qr a p' de.
cut ( q' : process, derivative q a q' weak_eq p' q').
intros H; elim H; clear H; intros q' H; elim H; intros de' we; clear H.
elim qr; clear qr; intros qr_l qr_r; clear qr_r.
elim (qr_l a q' de').
intros r' H; elim H; clear H; intros de'' we'; r'; split;
auto with v62.
apply trans_weak_eq with q'; auto with v62.

elim pq; intros pq_l pq_r; clear pq_r; auto with v62.

Qed.

Lemma trans_obs_eq1 :
p q r : process, obs_eq1 p q obs_eq1 q r obs_eq1 p r.

intros p q r pq qr; unfold obs_eq in |- *; split.
exact (half_trans_obs_eq1 p q r pq qr).

cut
( (a : action) (r' : process),
derivative r a r'
p' : process, derivative p a p' weak_eq r' p').
intros H a r' de.
elim (H a r' de); clear H; intros p' H; elim H; clear H; intros; p';
split; auto with v62.

cut (obs_eq1 q p); auto with v62.
cut (obs_eq1 r q); auto with v62.
exact (half_trans_obs_eq1 r q p).
Qed.

Lemma trans_obs_eq :
p q r : process, obs_eq p q obs_eq q r obs_eq p r.
intros p q r pq qr.
apply obs_eq1_obs_eq.
apply trans_obs_eq1 with q; auto with v62.

Qed.

Lemma strong_weak : p q : process, strong_eq p q weak_eq p q.
cofix.
intros p q.
intros H.
inversion_clear H.
apply w_eq.
intros a p' trans.
elim (H0 a p' trans).
clear H0.
intros q' H; elim H; clear H.
intros trans1 Str.
q'.
split.
apply w_single.
try try trivial with v62.

apply strong_weak; try try trivial with v62.

clear H0.
intros a q' trans.
elim (H1 a q' trans); clear H1.
intros p' H; elim H; clear H.
intros trans1 Str; p'; split.
apply w_single; try try trivial with v62.

apply strong_weak; try try trivial with v62.
Qed.

Hint Resolve strong_weak.

Lemma strong_obs : p q : process, strong_eq p q obs_eq p q.

intros p q H.
inversion_clear H.
unfold obs_eq in |- *; split.
clear H1; intros a p' trans.
elim (H0 a p' trans); clear H0.
intros q' H; elim H; clear H.
intros trans1 Str; q'; auto with v62.
clear H0; intros a q' trans.
elim (H1 a q' trans); clear H1.
intros p' H; elim H; clear H.
intros trans1 Str; p'; split; auto with v62.
Qed.

Hint Resolve strong_obs.

Lemma obs_weak : p q : process, obs_eq p q weak_eq p q.

unfold obs_eq in |- ×.
intros p q H; elim H; clear H; intros H1 H2.
apply w_eq.
intros a p' tr.
elim (H1 a p' tr).
intros q' H; elim H; clear H; intros de we.
q'; split; auto with v62.
intros a q' tr.
elim (H2 a q' tr).
intros p' H; elim H; clear H; intros de we.
p'; split; auto with v62.
Qed.

End TS.