Module device

Require Import List.
Import ListNotations.
Require Import Relations.

Module Type DEV_Sig.

Device state, and initial state
  Parameter t : Type.
  Parameter init : t.

Device operations interface
  Parameter ops_query: Type.
  Parameter ops_response: ops_query -> Type.
  Parameter op_sem: forall q: ops_query, t -> ops_response q -> t -> Prop.

Equivalence relation on device states. In the paper, we simplify the presentation, and we abstract from that equivalence relation, using bare equality.
  Parameter equiv : relation t.
  Parameter equiv_equiv: equivalence t equiv.
  Parameter op_sem_equiv: forall op_q op_r dev1 dev1' dev2 dev2',
    op_sem op_q dev1 op_r dev1' ->
    equiv dev1 dev2 ->
    op_sem op_q dev2 op_r dev2' ->
    equiv dev1' dev2'.

End DEV_Sig.

Module DEV_Utils (D: DEV_Sig).

  Import D.

Reflexive transitive closure of opsem
  Definition ops := { q: ops_query & ops_response q }.

  Inductive ops_sem : list ops -> t -> t -> Prop :=
  | ops_sem_nil: forall dev, ops_sem [] dev dev
  | ops_sem_trans: forall o ol dev1 dev2 dev3,
      op_sem (projT1 o) dev1 (projT2 o) dev2 ->
      ops_sem ol dev2 dev3 ->
      ops_sem (o::ol) dev1 dev3.

  Lemma ops_sem_equiv : forall t dev1 dev1',
      ops_sem t dev1 dev1' ->
      forall dev2 dev2',
        equiv dev1 dev2 ->
        ops_sem t dev2 dev2' ->
        equiv dev1' dev2'.
  Proof.
    induction 1 ; intros.
    - inversion H0. subst. auto.
    - inversion H2. subst. eapply IHops_sem; eauto.
      eapply op_sem_equiv; eauto.
  Qed.

End DEV_Utils.