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.