Library models
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.
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.
Lemma plus1Vstep x y: plus R x y -> R x y \/ exists2 z, R x z & plus R z y.
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).
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.
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).
Lemma fin_modelP : stable (@satisfies fin_ts).
Definition fin_model := {| ts_of := fin_ts ; modelP := fin_modelP |}.
End FiniteModels.