CCS.v

(*
TODO
- Improve readability and naming
- Complete proofs
*)

Inductive Action :=
| Out : nat -> Action
| In : nat -> Action
| Tau : Action.

(*
Inductive Action :=
| IO : bool -> nat -> Action
| Tau : Action.
*)

(* de Bruijn index *)
Inductive CCS :=
| Zero : CCS
| Send : Action -> CCS -> CCS
| Par : CCS -> CCS -> CCS
| Choice : CCS -> CCS -> CCS
| Nu : CCS -> CCS.

Inductive Transition : CCS -> Action -> CCS -> Prop :=
| SendT : forall (a : Action) (P : CCS), Transition (Send a P) a P
| Comm0T : forall (n : nat) (P P' Q Q' : CCS), Transition P (Out n) P' -> Transition Q (In n) Q' -> Transition (Par P Q) Tau (Par P' Q')
| Comm1T : forall (n : nat) (P P' Q Q' : CCS), Transition P (In n) P' -> Transition Q (Out n) Q' -> Transition (Par P Q) Tau (Par P' Q')
| ParLT : forall (a : Action) (P P' Q : CCS), Transition P a P' -> Transition (Par P Q) a (Par P' Q)
| ParRT : forall (a : Action) (P P' Q : CCS), Transition P a P' -> Transition (Par Q P) a (Par Q P')
| ChoiceLT : forall (a : Action) (P0 P1 P : CCS), Transition P0 a P -> Transition (Choice P0 P1) a P
| ChoiceRT : forall (a : Action) (P0 P1 P : CCS), Transition P1 a P -> Transition (Choice P0 P1) a P
| NuOutT : forall (n : nat) (P Q : CCS), Transition P (Out (S n)) Q -> Transition (Nu P) (Out n) (Nu Q)
| NuInT : forall (n : nat) (P Q : CCS), Transition P (In (S n)) Q -> Transition (Nu P) (In n) (Nu Q)
| NuTauT : forall (P Q : CCS), Transition P Tau Q -> Transition (Nu P) Tau (Nu Q).
Hint Constructors Transition.

Inductive Transition' : CCS -> Action -> CCS -> Prop :=
| Tau0 : forall (P : CCS), Transition' P Tau P
| Act1 : forall (a : Action) (P Q : CCS), Transition P a Q -> Transition' P a Q
| TauPre : forall (a : Action) (P Q R : CCS), Transition P Tau Q -> Transition' Q a R -> Transition' P a R
| TauPost : forall (a : Action) (P Q R : CCS), Transition' P a Q -> Transition Q Tau R -> Transition' P a R.


Definition Simulation (rel : CCS -> CCS -> Prop) := forall (P P' Q : CCS) (a : Action),
rel P Q -> Transition P a P' -> exists (Q' : CCS), Transition Q a Q' /\ rel P' Q'.

Definition WeakSimulation (rel : CCS -> CCS -> Prop) := forall (P P' Q : CCS) (a : Action),
rel P Q -> Transition P a P' -> exists (Q' : CCS), Transition' Q a Q' /\ rel P' Q'.

Definition inv {T} (rel : T -> T -> Prop) := fun x y => rel y x.

Definition Bisimulation (rel : CCS -> CCS -> Prop) := Simulation rel /\ Simulation (inv rel).

Definition WeakBisimulation (rel : CCS -> CCS -> Prop) := WeakSimulation rel /\ WeakSimulation (inv rel).

Definition Bisimilar (P Q : CCS) : Prop := exists (rel : CCS -> CCS -> Prop), Bisimulation rel /\ rel P Q.

Definition WeakBisimilar (P Q : CCS) : Prop := exists (rel : CCS -> CCS -> Prop), WeakBisimulation rel /\ rel P Q.

Lemma inv_bisim : forall (rel : CCS -> CCS -> Prop), Bisimulation rel -> Bisimulation (inv rel).
intros rel H.
destruct H as [H0 H1].
split.
assumption.
unfold Simulation.
unfold inv.
assumption.
Qed.

Lemma bisimilar_simulation : Simulation Bisimilar.
Proof.
intros P P' Q a Hrel HTrans.
destruct Hrel as [rel [[Hrelsim Hinvrelsim] Hrel]].
destruct (Hrelsim P P' Q a Hrel HTrans) as [Q' [H0 H1]].
exists Q'.
split.
assumption.
exists rel.
split;[split|];assumption.
Qed.

Inductive assoc_par : CCS -> CCS -> Prop :=
assoc_par0 : forall (P Q R : CCS), assoc_par (Par P (Par Q R)) (Par (Par P Q) R).
Hint Constructors assoc_par.

Inductive comm_par : CCS -> CCS -> Prop :=
comm_par0 : forall (P Q : CCS), comm_par (Par P Q) (Par Q P).
Hint Constructors comm_par.

Inductive zero_right_unit_par : CCS -> CCS -> Prop :=
zero_right_unit_par0 : forall (P : CCS), zero_right_unit_par (Par P Zero) P.
Hint Constructors zero_right_unit_par.

Fixpoint contain_var (n : nat) (P : CCS) : bool :=
match P with
| Zero => false
| Send (Out n) _ => true
| Send (In n) _ => true
| Send _ P' => contain_var n P'
| Par Q R => contain_var n Q || contain_var n R
| Choice Q R => contain_var n Q || contain_var n R
| Nu P' => contain_var (S n) P'
end.

From mathcomp.ssreflect Require Import ssreflect ssrbool ssrnat.

Definition inc_var_index (n level: nat) := if n >= level then S n else n.

Fixpoint inc_var_level (level : nat) (P : CCS) : CCS :=
match P with
| Zero => Zero
| Send (Out n) P' => Send (Out (inc_var_index n level)) (inc_var_level level P')
| Send (In n) P' => Send (In (inc_var_index n level)) (inc_var_level level P')
| Send Tau P' => Send Tau (inc_var_level level P')
| Par Q R => Par (inc_var_level level Q) (inc_var_level level R)
| Choice Q R => Choice (inc_var_level level Q) (inc_var_level level R)
| Nu P' => Nu (inc_var_level (S level) P')
end.

Definition inc_free_var := inc_var_level 0.

Inductive nu_par : CCS -> CCS -> Prop :=
nu_par0 : forall (P Q : CCS), contain_var 0 Q = false -> nu_par (Par (Nu P) Q) (Nu (Par P (inc_free_var Q))).
Hint Constructors nu_par.


Goal forall (P P' : CCS) (n : nat) , contain_var n P = false -> Transition P (Out n) P' -> False.
elim.
move => P' n _ HTrans.
inversion HTrans.
move => a P H P' /= n.
case a => //.
move => H0 HTrans.
inversion HTrans.
move => P HP Q HQ PQ /= n Hor HTrans.
inversion HTrans as [| | |a P0 P' Q0|a P0 Q' Q0| | | | |];subst P0 Q0 a PQ;move: (Bool.orb_false_elim _ _ Hor) => [Pfalse Qfalse].
by apply (HP P' n).
by apply (HQ Q' n).
move => P HP Q HQ PQ /= n Hor HTrans.
inversion HTrans as [| | | | |a P0 Q0 P'|a P0 Q0 Q'| | |];subst P0 Q0 a PQ;move: (Bool.orb_false_elim _ _ Hor) => [Pfalse Qfalse].
by apply (HP P' n).
by apply (HQ Q' n).
move => P HP Q /= n H0 HTrans.
inversion HTrans as [| | | | | | | |n0 P0 Q0|].
subst P0 n0 Q.
rename Q0 into Q.
by apply (HP Q (S n)).
Qed.

Lemma sim_weaksim : forall (rel : CCS -> CCS -> Prop), Simulation rel -> WeakSimulation rel.
intros rel H P P' Q a Hrel HTransP.
destruct (H P P' Q a Hrel HTransP) as [Q' [HTransQ Hrel']].
exists Q'.
split => //.
by apply Act1.
Qed.


Goal Simulation assoc_par.
Proof.
move => P P' Q a Hrel HTrans.
destruct Hrel.
move : P' HTrans => PQR HTrans.
inversion HTrans as [|n P0 P' Q0 QR HP HQR H0 H1 H2|n P0 P' Q0 QR HP HQR H0 H1 H2|b P0 P' QR HP|b QR QR' P0 HQR| | | | |].
subst P0 Q0 a PQR.
inversion HQR as [ | | |a Q0 Q' R0 HQ|a Q0 R' R0 HQ| | | | |];subst Q0 R0 a QR.
exists (Par (Par P' Q') R).
split => //.
apply ParLT.
by apply (Comm0T n).
exists (Par (Par P' Q) R').
split => //.
by apply (Comm0T n);[apply ParLT|].
subst P0 Q0 a PQR.
inversion HQR as [ | | |a Q0 Q' R0 HQ|a R0 R' Q0 HQ| | | | |];subst Q0 R0 a QR.
exists (Par (Par P' Q') R).
split => //.
by apply ParLT;apply (Comm1T n).
exists (Par (Par P' Q) R').
split => //.
by apply (Comm1T n);[apply ParLT|].
subst P0 QR b PQR.
exists (Par (Par P' Q) R).
split => //.
by apply ParLT;apply ParLT.
subst P0 QR b PQR.
inversion HQR as [ |n Q0 Q' R0 R' HQ HR|n Q0 Q' R0 R' HQ HR|b Q0 Q' R0 HQ|b Q0 R' R0 HR| | | | |].
subst Q0 R0 a QR'.
exists (Par (Par P Q') R').
split => //.
by apply (Comm0T n);[apply ParRT|].
subst Q0 R0 a QR'.
exists (Par (Par P Q') R').
split => //.
by apply (Comm1T n);[apply ParRT|].
subst Q0 R0 b QR'.
exists (Par (Par P Q') R).
split => //.
by apply ParLT;apply ParRT.
subst Q0 R0 b QR'.
exists (Par (Par P Q) R').
split => //.
by apply ParRT.
Qed.

Lemma Sinc_incS: forall (n level : nat), S (inc_var_index n level) = inc_var_index (S n) (S level).
Proof.
move => n level.
rewrite /inc_var_index -[level.+1]addn1 -{2}[n.+1]addn1 leq_add2r.
by case : (n >= level).
Qed.

Definition inc_action (level : nat) (a : Action) :=
match a with
| Out n => Out (inc_var_index n level)
| In n => In (inc_var_index n level)
| Tau => Tau
end.

Lemma inc_var_trans : forall (P P' : CCS) (level : nat) (a : Action), Transition P a P' -> Transition (inc_var_level level P) (inc_action level a) (inc_var_level level P').
elim => [|b P IH|P IHP Q IHQ|P IHP Q IHQ|P IHP] P' level a HTrans.
inversion HTrans.
inversion HTrans.
subst a0 P0 b P'.
move : a HTrans.
case.
by rewrite /inc_var_level => //.
by rewrite /inc_var_level => //.
move => HTrans.
apply SendT.
inversion HTrans;subst P0 Q0 a P'.
rename P'0 into P'.
apply (Comm0T (inc_var_index n level));rewrite -/inc_var_level.
rewrite (_: Out (inc_var_index n level) = inc_action level (Out n)) => //.
by apply IHP.
rewrite (_: In (inc_var_index n level) = inc_action level (In n)) => //.
by apply IHQ.
rename P'0 into P'.
apply (Comm1T (inc_var_index n level));rewrite -/inc_var_level.
rewrite (_: In (inc_var_index n level) = inc_action level (In n)) => //.
by apply IHP.
rewrite (_: Out (inc_var_index n level) = inc_action level (Out n)) => //.
by apply IHQ.
rename a0 into a; rename P'0 into P'.
apply ParLT.
by apply IHP.
rename a0 into a; rename P'0 into Q'.
apply ParRT.
by apply IHQ.
inversion HTrans;subst P0 P1 a P2;rename a0 into a.
apply ChoiceLT.
by apply IHP.
apply ChoiceRT.
by apply IHQ.
inversion HTrans;subst P0 a P'.
apply NuOutT.
rewrite -/inc_var_level.
rewrite Sinc_incS.
rewrite (_: Out (inc_var_index n.+1 level.+1) = inc_action level.+1 (Out n.+1)) => //.
by apply IHP.
apply NuInT.
rewrite -/inc_var_level Sinc_incS.
rewrite (_: In (inc_var_index n.+1 level.+1) = inc_action level.+1 (In n.+1)) => //.
by apply IHP.
apply NuTauT.
by apply (IHP _ _ Tau).
Qed.

Lemma par_no_occurence : forall (P Q : CCS) (n : nat), contain_var n (Par P Q) = false <-> contain_var n P = false /\ contain_var n Q = false.
move => P Q n.
split => [H|[HP HQ]].
by apply Bool.orb_false_elim.
by rewrite /contain_var -/contain_var HP HQ.
Qed.

Lemma choice_no_occurence : forall (P Q : CCS) (n : nat), contain_var n (Choice P Q) = false <-> contain_var n P = false /\ contain_var n Q = false.
move => P Q n.
split => [H|[HP HQ]].
by apply Bool.orb_false_elim.
by rewrite /contain_var -/contain_var HP HQ.
Qed.

Lemma no_occurence : forall (n : nat) (a : Action) (P P' : CCS), contain_var n P = false -> Transition P a P' -> contain_var n P' = false.
Proof.
move => n a P.
move : n a.
elim: P => [|b P H|P HP Q HQ|P HP Q HQ|P H] n a P' H0 H1;inversion H1.
subst a0 b P0 P'.
move : a H1 H0.
case => //.
subst P0 Q0 a P'.
move : H0.
rewrite 2!par_no_occurence => [[Ha Hb]].
by split;[apply (HP _ (Out n0))|apply (HQ _ (In n0))].
subst P0 Q0 a P'.
move : H0.
rewrite 2!par_no_occurence => [[Ha Hb]].
by split;[apply (HP _ (In n0))|apply (HQ _ (Out n0))].
subst P0 Q0 a0 P'.
move : H0.
rewrite 2!par_no_occurence => [[Ha Hb]].
by split;[apply (HP _ a)|].
subst P0 Q0 a0 P'.
move : H0.
rewrite 2!par_no_occurence => [[Ha Hb]].
by split;[|apply (HQ _ a)].
subst P0 P1 a0 P2.
move : H0.
rewrite par_no_occurence => [[Ha Hb]].
by apply (HP _ a).
subst P0 P1 a0 P2.
move : H0.
rewrite par_no_occurence => [[Ha Hb]].
by apply (HQ _ a).
subst P0 a P'.
move : H0.
rewrite /contain_var -/contain_var => H0.
by apply (H _ (Out n0.+1)).
subst P0 a P'.
move : H0.
rewrite /contain_var -/contain_var => H0.
by apply (H _ (In n0.+1)).
subst P0 a P'.
move : H0.
rewrite /contain_var -/contain_var => H0.
by apply (H _ Tau).
Qed.

Lemma sim_nu_par : Simulation nu_par.
Proof.
move => P P' Q a Hrel HTrans.
destruct Hrel.
inversion HTrans.
subst P0 Q0 a P'.
inversion H2.
subst P0 n0 P'0.
rename Q0 into P'.
exists (Nu (Par P' (inc_free_var Q'))).
split.
apply NuTauT.
apply (Comm0T n.+1) => //.
rewrite (_ : In n.+1 = inc_action 0 (In n)) //.
by apply inc_var_trans.
apply nu_par0.
by apply (no_occurence _ (In n) Q).
subst P0 Q0 a P'.
inversion H2.
subst P0 n0 P'0.
rename Q0 into P'.
exists (Nu (Par P' (inc_free_var Q'))).
split.
apply NuTauT.
apply (Comm1T n.+1) => //.
rewrite (_ : Out n.+1 = inc_action 0 (Out n)) //.
by apply inc_var_trans.
apply nu_par0.
by apply (no_occurence _ (Out n) Q).
subst P0 Q0 a0 P'.
inversion H4;subst P0 a P'0;rename Q0 into P';exists (Nu (Par P' (inc_free_var Q)));split => //.
apply NuOutT.
by apply ParLT.
apply NuInT.
by apply ParLT.
apply NuTauT.
by apply ParLT.
subst P0 Q0 a0 P'.
rename P'0 into Q'.
exists (Nu (Par P (inc_free_var Q'))).
split.
move : a HTrans H4.
case => [n|n|] HTrans HQ;[apply NuOutT|apply NuInT|apply NuTauT];apply ParRT.
rewrite (_ : Out n.+1 = inc_action 0 (Out n)) //.
by apply inc_var_trans.
rewrite (_ : In n.+1 = inc_action 0 (In n)) //.
by apply inc_var_trans.
by apply (inc_var_trans _ _ _ Tau).
apply nu_par0.
by apply (no_occurence _ a Q).
Qed.

Require Import Omega.

Lemma lem_b : forall (n n' level : nat), inc_var_index n level = inc_var_index n' level -> n = n'.
Proof.
move => n n' level.
rewrite /inc_var_index.
move Hb: (n >= level) => b.
move Hb': (n' >= level) => b'.
move: Hb Hb'.
elim b => Hb;elim b' => Hb' //.
case => //.
move : Hb => /leP Hb.
move : Hb' => /leP Hb'.
omega.
move : Hb => /leP Hb.
move : Hb' => /leP Hb'.
omega.
Qed.

Lemma lem_a : forall {P Q : CCS} {a : Action} {level : nat}, Transition (inc_var_level level P) a Q -> exists (Q' : CCS) (a' : Action), Q = inc_var_level level Q' /\ a = inc_action level a' /\ Transition P a' Q'.
Proof.
elim => [|[n|n|] P' HP'|R HR S HS|R HR S HS|R HR] Q a level HT;inversion HT.
by subst a0 P a Q;exists P';exists (Out n).
by subst a0 P a Q;exists P';exists (In n).
by subst a0 P a Q;exists P';exists Tau.
subst a Q0 P Q;rename P' into R';rename Q' into S'.
move : (HR R' (Out n) level H1) => [R'' [b [H2 [H3 H5]]]].
move : (HS S' (In n) level H4) => [S'' [c [H6 [H7 H8]]]].
exists (Par R'' S'').
exists Tau.
split.
rewrite /inc_var_level -/inc_var_level.
by move : H2 H6 => <- <-.
split => //.
move : b H3 H5.
case => // n'.
case => H3 H5.
move : c H7 H8.
case => // n''.
case => H7 H8.
have : n' = n''.
apply (lem_b n' n'' level).
by move : H3 H7 => <- <-.
move => H.
subst n''.
by apply (Comm0T n').

admit.

subst a0 Q0 Q P;rename P' into R'.
move : (HR R' a level H3) => [R'' [a' [-> [-> H]]]].
exists (Par R'' S).
exists a'.
split => //.
split => //.
by apply ParLT.

admit.

subst a0 P0 P1 Q;rename P into R'.
move : (HR R' a level H3) => [R'' [a' [-> [-> H]]]].
exists R''.
exists a'.
split => //.
split => //.
by apply ChoiceLT.

admit.

subst a Q P;rename Q0 into R'.
move : (HR R' (Out n.+1) level.+1 H0) => [R'' []].
case => [n'|n'|] [H []] //.
case.
move : n' => [] // n'.
rewrite <-Sinc_incS.
case => H1 H2.
exists (Nu R'').
exists (Out n').
move : H => ->.
split => //.
split.
move: H1 => -> //.
by apply NuOutT.

admit.

subst a P Q;rename Q0 into R'.
move : (HR R' Tau level.+1 H0) => [R''] [] [n|n|] [H] [] // _ H1.
exists (Nu R'').
exists Tau.
move : H => ->.
split => //.
split => //.
by apply NuTauT.
Admitted.

Lemma sim_inv_nu_par : Simulation (inv nu_par).
rewrite /inv => P P' Q a [] {P Q} P Q H0 HT.
inversion HT;subst P0 a P';rename Q0 into P';clear HT;inversion H1.
subst P0 Q0 a P';rename P'0 into P';clear H1.
exists (Par (Nu P') Q).
split.
apply ParLT.
by apply NuOutT.
by apply nu_par0.

subst P0 Q0 a P';rename P'0 into Q'.

Focus 2.
subst P0 Q0 a P';rename P'0 into P'.
exists (Par (Nu P') Q).
split.
apply ParLT.
by apply NuInT.
by apply nu_par0.

Focus 2.
subst P0 Q0 a P';rename P'0 into Q'.
Unfocus.

Focus 3.
subst P0 Q0 P'.
Check lem_a.
move : (lem_a H4) => [Q''] [] [n'|n'|] [H] [] //.
case => H5 H6.
exists (Par (Nu P'0) Q'').
split.
apply (Comm0T n').
apply NuOutT.
by rewrite (_: n'.+1 = n).
by [].
move : H => ->.
apply nu_par0.
by apply (no_occurence 0 (In n') Q Q'').

Focus 3.
subst P0 Q0 P'.
Unfocus.

Focus 4.
subst P0 Q0 a P';rename P'0 into P'.
exists (Par (Nu P') Q).
split.
apply ParLT.
by apply NuTauT.
by apply nu_par0.

Focus 4.
subst Q0 P0 a P';rename P'0 into Q'.
move: (lem_a H5) => [Q''] [] [n|n|] [H] [] // _ HT.
exists (Par (Nu P) Q'').
split.
by apply ParRT.
rewrite H.
apply nu_par0.
by apply (no_occurence 0 Tau Q Q'').
Admitted.

Corollary bisimilar_nu_par : forall (P Q : CCS), contain_var 0 Q = false -> Bisimilar (Par (Nu P) Q) (Nu (Par P (inc_free_var Q))).
move => P Q H.
exists nu_par.
split.
split.
by apply sim_nu_par.
by apply sim_inv_nu_par.
by apply nu_par0.
Qed.


Require Import Coq.Classes.RelationClasses.
Lemma equiv_bisim : Equivalence Bisimilar.
Proof.
split.
move => P.
exists eq.
split => // {P}.
split => P P' Q a.
move => <- H.
by exists P'.
move => -> H.
by exists P'.
move => P Q [rel [Hbisim Hrel]].
move: (inv_bisim rel Hbisim) => H.
by exists (inv rel).
move => P Q R [relPQ [HrelPQbisim HrelPQ]] [relQR [HrelQRbisim HrelQR]].
exists (fun x y => exists z, relPQ x z /\ relQR z y).
split.
move => {P Q R HrelPQ HrelQR}.
split => P P' Q a [R []].
move => HPR HRQ HTP.
move :HrelPQbisim => [] Hsim _.
move : (Hsim P P' R a HPR HTP) => [R' [HTR HPR']] {Hsim}.
move : HrelQRbisim => [] Hsim _.
move : (Hsim R R' Q a HRQ HTR) => [Q' [HTQ HRQ']] {Hsim}.
exists Q'.
split => //.
by exists R'.

move => HQR HRP HTP.
move : HrelQRbisim => [] _ Hsim.
move : (Hsim P P' R a HRP HTP) => [R' [HTR HPR']] {Hsim}.
move :HrelPQbisim => [] _ Hsim.
move : (Hsim R R' Q a HQR HTR) => [Q' [HTQ HPQ']] {Hsim}.
exists Q'.
split => //.
by exists R'.

by exists Q.
Qed.

Definition UpToBisimilarity (rel : CCS -> CCS -> Prop) := fun P Q => exists (P' Q' : CCS), Bisimilar P P' /\ rel P' Q' /\ Bisimilar Q' Q.

Definition SimulationUpToBisimilarity (rel : CCS -> CCS -> Prop) := forall (P P' Q : CCS) (a : Action),
rel P Q -> Transition P a P' -> exists (Q' : CCS), Transition Q a Q' /\ UpToBisimilarity rel P' Q'.

Definition BisimulationUpToBisimilarity (rel : CCS -> CCS -> Prop) := SimulationUpToBisimilarity rel /\ SimulationUpToBisimilarity (inv rel).

Lemma upto_sim : forall (rel : CCS -> CCS -> Prop), SimulationUpToBisimilarity rel -> Simulation (UpToBisimilarity rel).
Proof.
move => rel H P P' Q a [R] [S] [HPR [Hrel HSQ]] HTP.
move : (bisimilar_simulation P P' R a HPR HTP) => [R'] [HTR HPR'].
move : (H R R' S a) => [] // S' [HTS] [R''] [S''] [HbisimR [Hrel'' HbisimS]].
move : (bisimilar_simulation S S' Q a HSQ HTS) => [Q'] [HTQ HSQ'].
exists Q'.
split => //.
exists R'';exists S''.
split.
move : equiv_bisim => [_ _].
apply.
apply HPR'.
by [].
split => //.
move : equiv_bisim => [_ _].
apply.
apply HbisimS.
by [].
Qed.

Lemma upto_bisim : forall (rel : CCS -> CCS -> Prop), BisimulationUpToBisimilarity rel -> Bisimulation (UpToBisimilarity rel).
move => rel [H Hinv].
split.
by apply upto_sim.
have : Simulation (UpToBisimilarity (inv rel)) by apply upto_sim.
move => {H Hinv} H.
suffices : (forall P Q, inv (UpToBisimilarity rel) P Q <-> UpToBisimilarity (inv rel) P Q).
move => H0 P P' Q a.
rewrite H0 => H1 H2.
move : (H _ _ _ _ H1 H2) => [Q' H3].
exists Q'.
by rewrite H0.
move => {H} P Q.
split;rewrite /inv /UpToBisimilarity;move => [R] [S] [H0 [H1 H2]];exists S;exists R;move : equiv_bisim => [_ H3 _];by split;[apply H3|split => //;apply H3].
Qed.

Corollary upto_bisimilar : forall (P Q : CCS), (exists (rel : CCS -> CCS -> Prop), BisimulationUpToBisimilarity rel /\ rel P Q) -> Bisimilar P Q.
Proof.
move => P Q [rel [H0 H1]].
exists (UpToBisimilarity rel).
split.
by apply upto_bisim.
exists P;exists Q.
by move : equiv_bisim => [H2 _ _].
Qed.

CCS2.v

From mathcomp.ssreflect Require Import ssreflect ssrbool ssrnat finfun fintype tuple.
Require Import Omega Coq.Classes.RelationClasses Relation_Definitions.

Set Implicit Arguments.
Set Contextual Implicit.

Section CCS.

Inductive Action :=
| IO : bool -> nat -> Action
| Tau : Action.

Variable Pname : finType.

Inductive CCS :=
| Zero : CCS
| Send : Action -> CCS -> CCS
| Par : CCS -> CCS -> CCS
| Choice : CCS -> CCS -> CCS
| Nu : CCS -> CCS
| Invoke : Pname -> (nat -> nat) -> CCS.

Definition substitute_action (a : Action) (s : nat -> nat) :=
match a with
| IO b n => IO b (s n)
| Tau => Tau
end.

Definition inc_action (a : Action) := substitute_action a S.

Fixpoint substitute (P : CCS) (s : nat -> nat) :=
match P with 
| Zero => Zero
| Send a P' => Send (substitute_action a s) (substitute P' s)
| Par Q R => Par (substitute Q s) (substitute R s)
| Choice Q R => Choice (substitute Q s) (substitute R s)
| Nu P' => Nu (substitute P' (fun n => match n with 0 => 0 | S n' => s n' end))
| Invoke name t => Invoke name (fun n => s (t n))
end.

Variable f : {ffun Pname -> CCS}.
Inductive Transition : CCS -> Action -> CCS -> Prop :=
| SendT : forall (a : Action) (P : CCS), Transition (Send a P) a P
| CommT : forall (b : bool) (n : nat) (P P' Q Q' : CCS), Transition P (IO b n) P' -> Transition Q (IO (~~b) n) Q' -> Transition (Par P Q) Tau (Par P' Q')
| ParLT : forall (a : Action) (P P' Q : CCS), Transition P a P' -> Transition (Par P Q) a (Par P' Q)
| ParRT : forall (a : Action) (P P' Q : CCS), Transition P a P' -> Transition (Par Q P) a (Par Q P')
| ChoiceLT : forall (a : Action) (P0 P1 P : CCS), Transition P0 a P -> Transition (Choice P0 P1) a P
| ChoiceRT : forall (a : Action) (P0 P1 P : CCS), Transition P1 a P -> Transition (Choice P0 P1) a P
| NuT : forall (a : Action) (P Q : CCS), Transition P (inc_action a) Q -> Transition (Nu P) a (Nu Q)
| InvokeT : forall (s : nat -> nat) (name : Pname) (a : Action) (P : CCS), Transition (substitute (f name) s) a P -> Transition (Invoke name s) a P.
Hint Constructors Transition.

Lemma zero_trans : forall (a : Action) (P : CCS), ~Transition Zero a P.
Proof.
move => a P H.
by inversion H.
Qed.

Lemma send_trans : forall (a a' : Action) (P P' : CCS), Transition (Send a P) a' P' -> a' = a /\ P' = P.
Proof.
move => a a' P P' H.
by inversion H.
Qed.

Lemma par_trans : forall (a : Action) (P Q R : CCS), Transition (Par P Q) a R ->
(exists (b : bool) (n : nat) (P' Q' : CCS), Transition P (IO b n) P' /\ Transition Q (IO (~~b) n) Q' /\ R = Par P' Q' /\ a = Tau) \/
(exists (P' : CCS), Transition P a P') \/ (exists (Q' : CCS), Transition Q a Q').
Proof.
move => a P Q R H.
inversion H.
left.
by exists b;exists n;exists P';exists Q'.
right;left.
by exists P'.
right;right.
by exists P'.
Qed.

Lemma choice_trans : forall (a : Action) (P Q R : CCS), Transition (Choice P Q) a R ->
(exists (P' : CCS), Transition P a P' /\ R = P') \/ (exists (Q' : CCS), Transition Q a Q' /\ R = Q').
Proof.
move => a P Q R H.
inversion H.
left.
by exists R.
right.
by exists R.
Qed.

Lemma nu_trans : forall (a : Action) (P Q : CCS), Transition (Nu P) a Q ->
exists Q' : CCS, Transition P (inc_action a) Q' /\ Q = Nu Q'.
Proof.
move => a P Q H.
inversion H.
by exists Q0.
Qed.

Lemma invoke_trans : forall (s : nat -> nat)  (name : Pname) (a : Action) (P : CCS), Transition (Invoke name s) a P -> Transition (substitute (f name) s) a P.
Proof.
move => s a P name H.
by inversion H.
Qed.

End CCS.

Section LTS.

Record LTS := {
aT : Type; sT : Type;
transition : sT -> aT -> sT -> Prop
}.

Example ccs_lts (Pname : finType) (f : {ffun Pname -> CCS Pname}) : LTS := {|
aT := Action;
sT := CCS Pname;
transition := Transition f
|}.

Variable lts : LTS.

Definition Simulation (rel : relation (sT lts)) := forall (P P' Q : sT lts) (a : (aT lts)),
rel P Q -> (transition lts) P a P' -> exists (Q' : sT lts), (transition lts) Q a Q' /\ rel P' Q'.

Definition flip {A B C} (f : A -> B -> C) x y := f y x.

Definition rel_compose {A B C} (r : A -> B -> Prop) (s : B -> C -> Prop) := fun a c => exists (b : B), r a b /\ s b c.

Definition Bisimulation (rel : relation (sT lts)) := Simulation rel /\ Simulation (flip rel).

Definition Bisimilar (P Q : (sT lts)) : Prop := exists (rel : relation (sT lts)), Bisimulation rel /\ rel P Q.

Lemma eq_sim : Simulation eq.
Abort.

Lemma refl_bisim : Reflexive Bisimilar.
Abort.

Lemma sym_bisim : Symmetric Bisimilar.
Abort.

Lemma trans_bisim : Transitive Bisimilar.
Abort.

Lemma equiv_bisim : Equivalence Bisimilar.
Abort.

Lemma bisimilar_simulation : Simulation Bisimilar.
move => P P' Q a [] rel [] HBisim Hrel Htrans.
have: Simulation rel by move: HBisim => [].
move => HSim.
move : (HSim _ _ _ _ Hrel Htrans) => [] Q' [] HtransQ Hrel'.
exists Q'.
split => //=.
by exists rel.
Qed.

Lemma flip_bisimilar_simulation : Simulation (flip Bisimilar).
move => Q Q' P a [] rel [] HBisim Hrel Htrans.
have: Simulation (flip rel) by move: HBisim => [].
move => HSim.
move : (HSim _ _ _ _ Hrel Htrans) => [] P' [] HtransP Hrel'.
exists P'.
split => //=.
by exists rel.
Qed.

Lemma bisimilar_bisimulation : Bisimulation Bisimilar.
split.
by apply bisimilar_simulation.
by apply flip_bisimilar_simulation.
Qed.

Definition image_finite (P : sT lts) : Prop := exists (l : list ((aT lts) * (sT lts))), forall (a : aT lts) (Q : sT lts), transition lts P a Q <-> List.In (a, Q) l.

CoInductive CoindBisimilar : (sT lts) -> (sT lts) -> Prop :=
| Cons : forall (P Q : (sT lts)), (forall (P' : sT lts) (a : (aT lts)), (transition lts) P a P' -> exists (Q' : sT lts), (transition lts) Q a Q' /\ CoindBisimilar P' Q') ->
(forall (Q' : sT lts) (a : (aT lts)), (transition lts) Q a Q' -> exists (P' : sT lts), (transition lts) P a P' /\ CoindBisimilar P' Q') ->
CoindBisimilar P Q.

Goal forall (P Q : sT lts), CoindBisimilar P Q <-> Bisimilar P Q.
Proof.
move => P Q.
split.
move => H.
exists CoindBisimilar.
split => //=.
split => {P Q H}.
{
move => P P' Q a H Htrans.
destruct H.
by apply H.
}
{
move => P Q' Q a H Htrans.
destruct H.
by apply H0.
}
move : P Q.
cofix H => P Q H0.
apply Cons => [P' a Htrans|Q' a Htrans].
{
move : (bisimilar_simulation a H0 Htrans) => [] Q' [H1 H2].
exists Q'.
split => //=.
by apply H.
}
{
move : (flip_bisimilar_simulation a H0 Htrans) => [] P' [H1 H2].
exists P'.
split => //=.
by apply H.
}
Qed.

Definition SimF (rel : relation (sT lts)) : relation (sT lts) :=
fun (P Q : sT lts) => forall (P' : sT lts) (a : (aT lts)), (transition lts) P a P' -> exists (Q' : sT lts), (transition lts) Q a Q' /\ rel P' Q'.

Goal forall (rel : relation (sT lts)), Simulation rel <-> (forall (P Q : sT lts), rel P Q -> SimF rel P Q).
Abort.

End LTS.

Example Pname : finType := ordinal_finType 2.

Example P : CCS Pname := Invoke ord0 id.

Example f : (CCS Pname)^2 :=  (finfun (fun i : 'I_2 => tnth [tuple Send Tau P; Zero] i)).
(*
Open Scope fun_scope.
Example f : (CCS Pname)^2 :=  [ffun i => tnth [tuple Send Tau P; Zero] i].
Close Scope fun_scope.
*)

Ltac trans_ltac T :=
match type of T with
| Transition _ Zero _ _ => exfalso;exact (zero_trans T)
| Transition _ (Send _ _) ?a ?P => move: (send_trans T) => [];do 2 intro;subst a P;clear T => //
| Transition _ (Nu _) _ ?P => let Q := fresh "Q" in let H := fresh "H" in move: (nu_trans T) => [];rename P into Q => P {T} [T H];subst Q => //
| Transition _ (Par _ _) _ _ => move : (par_trans T) => [|[]] {T} //
| Transition _ (Choice _ _) _ _ => move : (choice_trans T) => [] {T} //
| Transition _ (Invoke _ _) _ _ => move : (invoke_trans T) => {T} T //
| _ => fail
end.

Goal forall (a b: Action) (P Q : CCS Pname), Transition f (Send a P) b Q -> b = a /\ False.
Proof.
move => a b P Q H.
trans_ltac H.
Abort.

Goal forall (a: Action) (P Q : CCS Pname), Transition f (Nu P) a Q -> False.
Proof.
move => a P Q H.
move: (nu_trans H).
trans_ltac H.
Abort.

Goal forall (a: Action) (P Q R : CCS Pname), Transition f (Par P Q) a R -> False.
Proof.
move => a P Q R H.
trans_ltac H.
Abort.

Goal forall (a: Action) (P Q R : CCS Pname), Transition f (Choice P Q) a R -> False.
Proof.
move => a P Q R H.
trans_ltac H.
Abort.

Goal forall (name : Pname) (s : nat -> nat) (a : Action) (P : CCS Pname), Transition f (Invoke name s) a P -> False.
Proof.
move => name s a P H.
trans_ltac H.
Abort.

Goal Transition f P Tau P.
Proof.
apply InvokeT => //.
rewrite ffunE tnth0.
by apply SendT.
Qed.

Goal f (inord 1) = Zero.
rewrite ffunE.
by rewrite -(tnth_behead _ ord0).
Qed.

Goal image_finite (ccs_lts f) (Zero).
exists nil.
move => a Q.
split => //=.
move => H.
trans_ltac H.
Qed.