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

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.

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.

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.