# Transition Systems

We use transition systems as models for K+

Record ts : Type := TS {
ts_state :> Type ;
ts_trans : ts_state -> ts_state -> Prop ;
ts_label : var -> ts_state -> Prop
}.

## Transitive Closure

The meaning of PBox will be defined using the inductively defined transitive closure operation.

Prenex Implicits ts_trans.

Implicit Arguments Relation_Operators.clos_trans_n1 [A].
Notation "'plus'" := Relation_Operators.clos_trans_n1.
Definition plus1 := Relation_Operators.tn1_step.
Definition plus_n1 := Relation_Operators.tn1_trans.

Section TC.
Variables (T:Type) (R : T -> T -> Prop).
Lemma plus1n x y z: R x y -> plus R y z -> plus R x z.
Proof.
move => H1 H2. elim: H2 H1 => {z}.
- move => z yz xy. apply: plus_n1 yz _. exact: plus1.
- move => z z'. firstorder. exact: plus_n1 H _.
Qed.

Lemma plus1Vstep x y: plus R x y -> R x y \/ exists2 z, R x z & plus R z y.
Proof.
elim; first by firstorder.
move => z z' zz' xz [rxz|[u Hu Hu']]; right.
exists z => //. exact: plus1. exists u => //. exact: plus_n1 zz' Hu'.
Qed.

End TC.

Definition plusb (T:finType) (e:rel T) x y := existsb z, connect e x z && e z y.

Lemma plusP (T:finType) (e : rel T) w v: reflect (plus e w v) (plusb e w v).
Proof.
apply: introP'.
- elim => {v} [v R | v v' R _ P]; apply/exists_inP.
+ exists w => //. exact: connect0.
+ exists v => //. case/exists_inP : P => w' H /connect1. exact: connect_trans.
- case/exists_inP => w' /connectP [p pth ->] {w'}. elim/last_ind: p pth v => //=. move => _. exact: plus1.
move => p x IH. rewrite last_rcons path_rcons => /andP [H1 H2] v H3. apply: plus_n1 H3 _. exact: IH.
Qed.

## Satisfaction and Models

Fixpoint satisfies (M : ts) (w : M) s :=
match s with
| Var p => ts_label p w
| Bot => False
| s ---> t => satisfies w s -> satisfies w t
| Box s => forall v, ts_trans w v -> satisfies v s
| PBox s => forall v, plus ts_trans w v -> satisfies v s
end.

Definition stable (X Y : Type) (R : X -> Y -> Prop) :=
forall x y , ~ ~ R x y -> R x y.

Record model : Type := Model { ts_of :> ts ; modelP : stable (@satisfies ts_of) }.
Definition valid s := forall (M : model) (w : M), satisfies w s.

Theorem soundness s: prv s -> valid s.
Proof.
elim => {s} /=; try by rewrite /valid /= ; firstorder.
- move => s M w. exact: modelP.
- move => s M w /= H w' ww' v P. apply: H. exact: plus1n ww' P.
- move => s M w /= H w' T. apply: H. exact: plus1.
- move => s M w /= pB v wv H. case (plus1Vstep H); firstorder.
- move => s M w.
rewrite [PBox (s ---> Box s)]lock [Box s]lock /= -!lock => H1 H2 v H.
by elim: H H1 H2; simpl;firstorder.
Qed.

## Finite Models

We show that we can turn any boolean transiton relation and labeling ober a fintype into a model. We obtain stability by giving a boolean evaluation function which reflects the satisfaction relation.

Section FiniteModels.
Variables (T: finType) (e : rel T) (label: var -> pred T).

Definition fin_ts := {| ts_state := T ; ts_trans := e ; ts_label := label |}.

Fixpoint evalb w s :=
match s with
| Var p => label p w
| Bot => false
| s ---> t => evalb w s ==> evalb w t
| Box s => forallb v, e w v ==> evalb v s
| PBox s => forallb v, plusb e w v ==> evalb v s
end.

Lemma evalP (w:fin_ts) s : reflect (satisfies w s) (evalb w s).
Proof.
elim: s w => //=.
- move => * ; exact: idP.
- by constructor.
- move => s IHs t IHt w.
apply: iffP (@implyP _ _) _ _ => ? /IHs ?; apply/IHt; firstorder.
- move => s IHs w.
apply: iffP (@forall_inP _ _ _) _ _ => H v /H /IHs; done.
- move => s IHs w.
apply: iffP (@forall_inP _ _ _) _ _ => H v /plusP /H /IHs; done.
Qed.

Lemma fin_modelP : stable (@satisfies fin_ts).
Proof. move => w s. case : (decP (evalP w s)); tauto. Qed.

Definition fin_model := {| ts_of := fin_ts ; modelP := fin_modelP |}.
End FiniteModels.