Require Import Relations Ensembles Basics. Set Implicit Arguments. (** ** Transition System over a type C of configurations The following class definition is parameterized by a type $C$ of configurations and a type _even_t_ of events. Transition systems are composed of two fields: - _TS_tr_ maps any event to a binary relation on $C$ - _TS_Init_ is a set of _initial configurations_ *) Section Definitions. Variables C event_t : Type. Class TS : Type:= { TS_tr : event_t -> relation C; (* transition relation *) TS_Init: Ensemble C (* initial set of states *) }. Context (S : TS). (** T c e c' : there is a transition from c to c' labelled with e *) Notation T c e c' := (TS_tr e c c'). (** string similarity and bisimilarity *) CoInductive simulates : relation C := simulates_i : forall (c c1:C), (forall e c', T c e c' -> exists c1', T c1 e c1' /\ simulates c' c1') -> simulates c c1. CoInductive bisimulates : relation C := bisimulates_i : forall (c c1:C), (forall e c', T c e c' -> exists c1', T c1 e c1' /\ bisimulates c' c1') -> (forall e c1', T c1 e c1' -> exists c', T c e c' /\ bisimulates c' c1') -> bisimulates c c1. (** simulations and bisimulations *) Definition simulation (R: relation C) : Prop := forall (c c1 c':C) (e:event_t), T c e c' -> R c c1 -> exists c1', T c1 e c1' /\ R c' c1'. Definition bisimulation (R: relation C) : Prop := simulation R /\ simulation (flip R). (** An introduction rule for simulates *) Lemma simulation_simulates : forall (R:relation C), simulation R -> forall c c', R c c' -> simulates c c'. intros R H;cofix. intros c c';constructor. intros e c'0 H1; destruct (H _ _ _ _ H1 H0) as [c1' [H2 H3]]. exists c1';auto. Guarded. Qed. (** Reciprocal *) Lemma simulates_simulation : simulation simulates. red;intros. inversion H0. destruct (H1 _ _ H) as [c1' [H4 H5]]. exists c1';split;auto. Qed. (** Introduction for bisimulates *) Lemma bisimulation_bisimulates : forall (R:relation C), bisimulation R -> forall c c', R c c' -> bisimulates c c'. intros R H;cofix. intros c c';split. intros e c'0 H1;destruct H. destruct (H _ _ _ _ H1 H0) as [c1' [H3 H4]]. exists c1'. split;auto. Guarded. intros e c1' H1. destruct H. destruct (H2 _ _ _ _ H1 H0) as [c1 [H3 H4]]. exists c1;split;auto. Qed. (** Reciprocal *) Lemma bisimulates_bisimulation : bisimulation bisimulates. split;red;intros. inversion H0. destruct (H1 _ _ H) as [c1' [H5 H6]]. exists c1';split;auto. inversion H0. red in H0. destruct (H2 _ _ H) as [c1' [H5 H6]]. exists c1';split;auto. Qed. End Definitions. Notation T c e c' := (TS_tr e c c'). Section Example. Inductive event_t : Type := a | b. Inductive C : Type := q0 | q1 | q2. Instance S : TS C event_t := Build_TS (fun e q q' => match e,q, q' with | a,q0,q1 | b,q1,q2 | a,q2,q1 => True |_,_,_ => False end) (fun q => True). (** Let's consider a relation between states *) Let R := fun (q q':C) => match q,q' with q0,q0 => True | q0,q2 | q2, q0 => True | q1,q1 | q2, q2 => True | _,_ => False end. Lemma B1: bisimulation S R. split;unfold simulation;intros. destruct c,c1,c',e; try contradiction. exists q1;split;auto. exists q1;split;auto. exists q2;split;auto. exists q1;split;auto. exists q1;split;auto. destruct c,c1,c',e; try contradiction. exists q1;split;auto. exists q1;split;auto. exists q2;split;auto. exists q1;split;auto. exists q1;split;auto. Qed. Corollary B2 : bisimulates S q0 q2. Proof. apply bisimulation_bisimulates with (R:=R). apply B1. now red. Qed. Fact B3 : ~ bisimulates S q0 q1. Proof. intro H. inversion H. destruct (H0 a q1). now red. destruct H4 as [H4 _]. inversion H4. Qed. End Example.