From VLSM.Lib Require Import Itauto.[Loading ML file ring_plugin.cmxs (using legacy method) ... done]
[Loading ML file zify_plugin.cmxs (using legacy method) ... done]
[Loading ML file micromega_plugin.cmxs (using legacy method) ... done]
[Loading ML file btauto_plugin.cmxs (using legacy method) ... done]
[Loading ML file coq-itauto.plugin ... done]
From stdpp Require Import prelude.
From VLSM.Core Require Import VLSM.
From VLSM.Core.VLSMProjections Require Import VLSMEmbedding VLSMTotalProjection.

Core: VLSM Inclusion

When both VLSMs have the same state and label types they also share the same Trace type, and sets of traces can be compared without conversion. Then VLSM X is included in VLSM Y if every valid_trace available to X is also available to Y.

Section sec_VLSM_inclusion.

Context
  {message : Type}
  {T : VLSMType message}
  .

Definition VLSM_incl_part
  (MX MY : VLSMMachine T)
  (X := mk_vlsm MX) (Y := mk_vlsm MY)
  :=
  forall t : Trace,
    valid_trace_prop X t -> valid_trace_prop Y t.

#[local] Notation VLSM_incl X Y := (VLSM_incl_part (vlsm_machine X) (vlsm_machine Y)).

Lemma VLSM_incl_refl
  (MX : VLSMMachine T)
  (X := mk_vlsm MX)
  : VLSM_incl X X.message: Type
T: VLSMType message
MX: VLSMMachine T
X:= {| vlsm_type := T; vlsm_machine := MX |}: VLSM message
VLSM_incl X X
Proof.message: Type
T: VLSMType message
MX: VLSMMachine T
X:= {| vlsm_type := T; vlsm_machine := MX |}: VLSM message
VLSM_incl X X
  by firstorder.
Qed.

Lemma VLSM_incl_trans
  (MX MY MZ : VLSMMachine T)
  (X := mk_vlsm MX) (Y := mk_vlsm MY) (Z := mk_vlsm MZ)
  : VLSM_incl X Y -> VLSM_incl Y Z -> VLSM_incl X Z.message: Type
T: VLSMType message
MX, MY, MZ: VLSMMachine T
X:= {| vlsm_type := T; vlsm_machine := MX |}: VLSM message
Y:= {| vlsm_type := T; vlsm_machine := MY |}: VLSM message
Z:= {| vlsm_type := T; vlsm_machine := MZ |}: VLSM message
VLSM_incl X Y → VLSM_incl Y Z → VLSM_incl X Z
Proof.message: Type
T: VLSMType message
MX, MY, MZ: VLSMMachine T
X:= {| vlsm_type := T; vlsm_machine := MX |}: VLSM message
Y:= {| vlsm_type := T; vlsm_machine := MY |}: VLSM message
Z:= {| vlsm_type := T; vlsm_machine := MZ |}: VLSM message
VLSM_incl X Y → VLSM_incl Y Z → VLSM_incl X Z
  by firstorder.
Qed.

Lemma VLSM_incl_finite_traces_characterization
  (MX MY : VLSMMachine T)
  (X := mk_vlsm MX) (Y := mk_vlsm MY)
  : VLSM_incl X Y <->
    forall (s : state X)
    (tr : list (transition_item X)),
    finite_valid_trace X s tr -> finite_valid_trace Y s tr.message: Type
T: VLSMType message
MX, MY: VLSMMachine T
X:= {| vlsm_type := T; vlsm_machine := MX |}: VLSM message
Y:= {| vlsm_type := T; vlsm_machine := MY |}: VLSM message
VLSM_incl X Y
↔ (∀ (s : state X) (tr : list transition_item),
     finite_valid_trace X s tr
     → finite_valid_trace Y s tr)
Proof.message: Type
T: VLSMType message
MX, MY: VLSMMachine T
X:= {| vlsm_type := T; vlsm_machine := MX |}: VLSM message
Y:= {| vlsm_type := T; vlsm_machine := MY |}: VLSM message
VLSM_incl X Y
↔ (∀ (s : state X) (tr : list transition_item),
     finite_valid_trace X s tr
     → finite_valid_trace Y s tr)
  split; intros Hincl.message: Type
T: VLSMType message
MX, MY: VLSMMachine T
X:= {| vlsm_type := T; vlsm_machine := MX |}: VLSM message
Y:= {| vlsm_type := T; vlsm_machine := MY |}: VLSM message
Hincl: VLSM_incl X Y
∀ (s : state X) (tr : list transition_item),
  finite_valid_trace X s tr
  → finite_valid_trace Y s tr
message: Type
T: VLSMType message
MX, MY: VLSMMachine T
X:= {| vlsm_type := T; vlsm_machine := MX |}: VLSM message
Y:= {| vlsm_type := T; vlsm_machine := MY |}: VLSM message
Hincl: ∀ (s : state X) (tr : list transition_item),
  finite_valid_trace X s tr
  → finite_valid_trace Y s tr
VLSM_incl X Y
  -message: Type
T: VLSMType message
MX, MY: VLSMMachine T
X:= {| vlsm_type := T; vlsm_machine := MX |}: VLSM message
Y:= {| vlsm_type := T; vlsm_machine := MY |}: VLSM message
Hincl: VLSM_incl X Y
∀ (s : state X) (tr : list transition_item),
  finite_valid_trace X s tr
  → finite_valid_trace Y s tr by intros; apply (Hincl (Finite s tr)).
  -message: Type
T: VLSMType message
MX, MY: VLSMMachine T
X:= {| vlsm_type := T; vlsm_machine := MX |}: VLSM message
Y:= {| vlsm_type := T; vlsm_machine := MY |}: VLSM message
Hincl: ∀ (s : state X) (tr : list transition_item),
  finite_valid_trace X s tr
  → finite_valid_trace Y s tr
VLSM_incl X Y intros tr Htr.message: Type
T: VLSMType message
MX, MY: VLSMMachine T
X:= {| vlsm_type := T; vlsm_machine := MX |}: VLSM message
Y:= {| vlsm_type := T; vlsm_machine := MY |}: VLSM message
Hincl: ∀ (s : state X) (tr : list transition_item),
  finite_valid_trace X s tr
  → finite_valid_trace Y s tr
tr: Trace
Htr: valid_trace_prop
  {| vlsm_type := T; vlsm_machine := X |} tr
valid_trace_prop
  {| vlsm_type := T; vlsm_machine := Y |} tr
    destruct tr as [is tr | is tr]; simpl in *.message: Type
T: VLSMType message
MX, MY: VLSMMachine T
X:= {| vlsm_type := T; vlsm_machine := MX |}: VLSM message
Y:= {| vlsm_type := T; vlsm_machine := MY |}: VLSM message
Hincl: ∀ (s : state T) (tr : list transition_item),
  finite_valid_trace X s tr
  → finite_valid_trace Y s tr
is: state T
tr: list transition_item
Htr: finite_valid_trace
  {| vlsm_type := T; vlsm_machine := MX |} is tr
finite_valid_trace
  {| vlsm_type := T; vlsm_machine := MY |} is tr
message: Type
T: VLSMType message
MX, MY: VLSMMachine T
X:= {| vlsm_type := T; vlsm_machine := MX |}: VLSM message
Y:= {| vlsm_type := T; vlsm_machine := MY |}: VLSM message
Hincl: ∀ (s : state T) (tr : list transition_item),
  finite_valid_trace X s tr
  → finite_valid_trace Y s tr
is: state T
tr: Streams.Stream transition_item
Htr: infinite_valid_trace
  {| vlsm_type := T; vlsm_machine := MX |} is tr
infinite_valid_trace
  {| vlsm_type := T; vlsm_machine := MY |} is tr
    +message: Type
T: VLSMType message
MX, MY: VLSMMachine T
X:= {| vlsm_type := T; vlsm_machine := MX |}: VLSM message
Y:= {| vlsm_type := T; vlsm_machine := MY |}: VLSM message
Hincl: ∀ (s : state T) (tr : list transition_item),
  finite_valid_trace X s tr
  → finite_valid_trace Y s tr
is: state T
tr: list transition_item
Htr: finite_valid_trace
  {| vlsm_type := T; vlsm_machine := MX |} is tr
finite_valid_trace
  {| vlsm_type := T; vlsm_machine := MY |} is tr by apply Hincl.
    +message: Type
T: VLSMType message
MX, MY: VLSMMachine T
X:= {| vlsm_type := T; vlsm_machine := MX |}: VLSM message
Y:= {| vlsm_type := T; vlsm_machine := MY |}: VLSM message
Hincl: ∀ (s : state T) (tr : list transition_item),
  finite_valid_trace X s tr
  → finite_valid_trace Y s tr
is: state T
tr: Streams.Stream transition_item
Htr: infinite_valid_trace
  {| vlsm_type := T; vlsm_machine := MX |} is tr
infinite_valid_trace
  {| vlsm_type := T; vlsm_machine := MY |} is tr destruct Htr as [HtrX HisX].message: Type
T: VLSMType message
MX, MY: VLSMMachine T
X:= {| vlsm_type := T; vlsm_machine := MX |}: VLSM message
Y:= {| vlsm_type := T; vlsm_machine := MY |}: VLSM message
Hincl: ∀ (s : state T) (tr : list transition_item),
  finite_valid_trace X s tr
  → finite_valid_trace Y s tr
is: state T
tr: Streams.Stream transition_item
HtrX: infinite_valid_trace_from
  {| vlsm_type := T; vlsm_machine := MX |} is
  tr
HisX: initial_state_prop is
infinite_valid_trace
  {| vlsm_type := T; vlsm_machine := MY |} is tr
      assert (His_tr : finite_valid_trace X is []).message: Type
T: VLSMType message
MX, MY: VLSMMachine T
X:= {| vlsm_type := T; vlsm_machine := MX |}: VLSM message
Y:= {| vlsm_type := T; vlsm_machine := MY |}: VLSM message
Hincl: ∀ (s : state T) (tr : list transition_item),
  finite_valid_trace X s tr
  → finite_valid_trace Y s tr
is: state T
tr: Streams.Stream transition_item
HtrX: infinite_valid_trace_from
  {| vlsm_type := T; vlsm_machine := MX |} is
  tr
HisX: initial_state_prop is
finite_valid_trace X is []
message: Type
T: VLSMType message
MX, MY: VLSMMachine T
X:= {| vlsm_type := T; vlsm_machine := MX |}: VLSM message
Y:= {| vlsm_type := T; vlsm_machine := MY |}: VLSM message
Hincl: ∀ (s : state T) (tr : list transition_item),
  finite_valid_trace X s tr
  → finite_valid_trace Y s tr
is: state T
tr: Streams.Stream transition_item
HtrX: infinite_valid_trace_from
  {| vlsm_type := T; vlsm_machine := MX |} is
  tr
HisX: initial_state_prop is
His_tr: finite_valid_trace X is []
infinite_valid_trace
  {| vlsm_type := T; vlsm_machine := MY |} is tr
      {message: Type
T: VLSMType message
MX, MY: VLSMMachine T
X:= {| vlsm_type := T; vlsm_machine := MX |}: VLSM message
Y:= {| vlsm_type := T; vlsm_machine := MY |}: VLSM message
Hincl: ∀ (s : state T) (tr : list transition_item),
  finite_valid_trace X s tr
  → finite_valid_trace Y s tr
is: state T
tr: Streams.Stream transition_item
HtrX: infinite_valid_trace_from
  {| vlsm_type := T; vlsm_machine := MX |} is
  tr
HisX: initial_state_prop is
finite_valid_trace X is []
        split; [| done].message: Type
T: VLSMType message
MX, MY: VLSMMachine T
X:= {| vlsm_type := T; vlsm_machine := MX |}: VLSM message
Y:= {| vlsm_type := T; vlsm_machine := MY |}: VLSM message
Hincl: ∀ (s : state T) (tr : list transition_item),
  finite_valid_trace X s tr
  → finite_valid_trace Y s tr
is: state T
tr: Streams.Stream transition_item
HtrX: infinite_valid_trace_from
  {| vlsm_type := T; vlsm_machine := MX |} is
  tr
HisX: initial_state_prop is
finite_valid_trace_from X is []
        by constructor; apply initial_state_is_valid.
      }message: Type
T: VLSMType message
MX, MY: VLSMMachine T
X:= {| vlsm_type := T; vlsm_machine := MX |}: VLSM message
Y:= {| vlsm_type := T; vlsm_machine := MY |}: VLSM message
Hincl: ∀ (s : state T) (tr : list transition_item),
  finite_valid_trace X s tr
  → finite_valid_trace Y s tr
is: state T
tr: Streams.Stream transition_item
HtrX: infinite_valid_trace_from
  {| vlsm_type := T; vlsm_machine := MX |} is
  tr
HisX: initial_state_prop is
His_tr: finite_valid_trace X is []
infinite_valid_trace
  {| vlsm_type := T; vlsm_machine := MY |} is tr
      apply Hincl in His_tr.message: Type
T: VLSMType message
MX, MY: VLSMMachine T
X:= {| vlsm_type := T; vlsm_machine := MX |}: VLSM message
Y:= {| vlsm_type := T; vlsm_machine := MY |}: VLSM message
Hincl: ∀ (s : state T) (tr : list transition_item),
  finite_valid_trace X s tr
  → finite_valid_trace Y s tr
is: state T
tr: Streams.Stream transition_item
HtrX: infinite_valid_trace_from
  {| vlsm_type := T; vlsm_machine := MX |} is
  tr
HisX: initial_state_prop is
His_tr: finite_valid_trace Y is []
infinite_valid_trace
  {| vlsm_type := T; vlsm_machine := MY |} is tr
      destruct His_tr as [_ HisY].message: Type
T: VLSMType message
MX, MY: VLSMMachine T
X:= {| vlsm_type := T; vlsm_machine := MX |}: VLSM message
Y:= {| vlsm_type := T; vlsm_machine := MY |}: VLSM message
Hincl: ∀ (s : state T) (tr : list transition_item),
  finite_valid_trace X s tr
  → finite_valid_trace Y s tr
is: state T
tr: Streams.Stream transition_item
HtrX: infinite_valid_trace_from
  {| vlsm_type := T; vlsm_machine := MX |} is
  tr
HisX, HisY: initial_state_prop is
infinite_valid_trace
  {| vlsm_type := T; vlsm_machine := MY |} is tr
      split; [| done].message: Type
T: VLSMType message
MX, MY: VLSMMachine T
X:= {| vlsm_type := T; vlsm_machine := MX |}: VLSM message
Y:= {| vlsm_type := T; vlsm_machine := MY |}: VLSM message
Hincl: ∀ (s : state T) (tr : list transition_item),
  finite_valid_trace X s tr
  → finite_valid_trace Y s tr
is: state T
tr: Streams.Stream transition_item
HtrX: infinite_valid_trace_from
  {| vlsm_type := T; vlsm_machine := MX |} is
  tr
HisX, HisY: initial_state_prop is
infinite_valid_trace_from
  {| vlsm_type := T; vlsm_machine := MY |} is tr
      apply infinite_valid_trace_from_prefix_rev.message: Type
T: VLSMType message
MX, MY: VLSMMachine T
X:= {| vlsm_type := T; vlsm_machine := MX |}: VLSM message
Y:= {| vlsm_type := T; vlsm_machine := MY |}: VLSM message
Hincl: ∀ (s : state T) (tr : list transition_item),
  finite_valid_trace X s tr
  → finite_valid_trace Y s tr
is: state T
tr: Streams.Stream transition_item
HtrX: infinite_valid_trace_from
  {| vlsm_type := T; vlsm_machine := MX |} is
  tr
HisX, HisY: initial_state_prop is
∀ n : nat,
  finite_valid_trace_from
    {| vlsm_type := T; vlsm_machine := MY |} is
    (StreamExtras.stream_prefix tr n)
      intros.message: Type
T: VLSMType message
MX, MY: VLSMMachine T
X:= {| vlsm_type := T; vlsm_machine := MX |}: VLSM message
Y:= {| vlsm_type := T; vlsm_machine := MY |}: VLSM message
Hincl: ∀ (s : state T) (tr : list transition_item),
  finite_valid_trace X s tr
  → finite_valid_trace Y s tr
is: state T
tr: Streams.Stream transition_item
HtrX: infinite_valid_trace_from
  {| vlsm_type := T; vlsm_machine := MX |} is
  tr
HisX, HisY: initial_state_prop is
n: nat
finite_valid_trace_from
  {| vlsm_type := T; vlsm_machine := MY |} is
  (StreamExtras.stream_prefix tr n)
      pose proof (infinite_valid_trace_from_prefix _ _ _ HtrX n) as HfinX.message: Type
T: VLSMType message
MX, MY: VLSMMachine T
X:= {| vlsm_type := T; vlsm_machine := MX |}: VLSM message
Y:= {| vlsm_type := T; vlsm_machine := MY |}: VLSM message
Hincl: ∀ (s : state T) (tr : list transition_item),
  finite_valid_trace X s tr
  → finite_valid_trace Y s tr
is: state T
tr: Streams.Stream transition_item
HtrX: infinite_valid_trace_from
  {| vlsm_type := T; vlsm_machine := MX |} is
  tr
HisX, HisY: initial_state_prop is
n: nat
HfinX: finite_valid_trace_from
  {| vlsm_type := T; vlsm_machine := MX |} is
  (StreamExtras.stream_prefix tr n)
finite_valid_trace_from
  {| vlsm_type := T; vlsm_machine := MY |} is
  (StreamExtras.stream_prefix tr n)
      by apply Hincl.
Qed.

A VLSM_inclusion is equivalent to a VLSM_embedding in which both the label and state projection functions are identities.

Lemma VLSM_incl_embedding_iff
  (MX MY : VLSMMachine T)
  (X := mk_vlsm MX) (Y := mk_vlsm MY)
  : VLSM_incl X Y <-> VLSM_embedding X Y id id.message: Type
T: VLSMType message
MX, MY: VLSMMachine T
X:= {| vlsm_type := T; vlsm_machine := MX |}: VLSM message
Y:= {| vlsm_type := T; vlsm_machine := MY |}: VLSM message
VLSM_incl X Y ↔ VLSM_embedding X Y id id
Proof.message: Type
T: VLSMType message
MX, MY: VLSMMachine T
X:= {| vlsm_type := T; vlsm_machine := MX |}: VLSM message
Y:= {| vlsm_type := T; vlsm_machine := MY |}: VLSM message
VLSM_incl X Y ↔ VLSM_embedding X Y id id
  assert (Hid : forall tr : list (transition_item T),
    tr = pre_VLSM_embedding_finite_trace_project _ _ id id tr).message: Type
T: VLSMType message
MX, MY: VLSMMachine T
X:= {| vlsm_type := T; vlsm_machine := MX |}: VLSM message
Y:= {| vlsm_type := T; vlsm_machine := MY |}: VLSM message
∀ tr : list transition_item,
  tr =
  pre_VLSM_embedding_finite_trace_project T T id id tr
message: Type
T: VLSMType message
MX, MY: VLSMMachine T
X:= {| vlsm_type := T; vlsm_machine := MX |}: VLSM message
Y:= {| vlsm_type := T; vlsm_machine := MY |}: VLSM message
Hid: ∀ tr : list transition_item,
  tr =
  pre_VLSM_embedding_finite_trace_project T T id
    id tr
VLSM_incl X Y ↔ VLSM_embedding X Y id id
  {message: Type
T: VLSMType message
MX, MY: VLSMMachine T
X:= {| vlsm_type := T; vlsm_machine := MX |}: VLSM message
Y:= {| vlsm_type := T; vlsm_machine := MY |}: VLSM message
∀ tr : list transition_item,
  tr =
  pre_VLSM_embedding_finite_trace_project T T id id tr
    induction tr; [done |].message: Type
T: VLSMType message
MX, MY: VLSMMachine T
X:= {| vlsm_type := T; vlsm_machine := MX |}: VLSM message
Y:= {| vlsm_type := T; vlsm_machine := MY |}: VLSM message
a: transition_item
tr: list transition_item
IHtr: tr =
pre_VLSM_embedding_finite_trace_project T T id
  id tr
a :: tr =
pre_VLSM_embedding_finite_trace_project T T id id
  (a :: tr)
    by destruct a; cbn; f_equal.
  }message: Type
T: VLSMType message
MX, MY: VLSMMachine T
X:= {| vlsm_type := T; vlsm_machine := MX |}: VLSM message
Y:= {| vlsm_type := T; vlsm_machine := MY |}: VLSM message
Hid: ∀ tr : list transition_item,
  tr =
  pre_VLSM_embedding_finite_trace_project T T id
    id tr
VLSM_incl X Y ↔ VLSM_embedding X Y id id
  split.message: Type
T: VLSMType message
MX, MY: VLSMMachine T
X:= {| vlsm_type := T; vlsm_machine := MX |}: VLSM message
Y:= {| vlsm_type := T; vlsm_machine := MY |}: VLSM message
Hid: ∀ tr : list transition_item,
  tr =
  pre_VLSM_embedding_finite_trace_project T T id
    id tr
VLSM_incl X Y → VLSM_embedding X Y id id
message: Type
T: VLSMType message
MX, MY: VLSMMachine T
X:= {| vlsm_type := T; vlsm_machine := MX |}: VLSM message
Y:= {| vlsm_type := T; vlsm_machine := MY |}: VLSM message
Hid: ∀ tr : list transition_item,
  tr =
  pre_VLSM_embedding_finite_trace_project T T id
    id tr
VLSM_embedding X Y id id → VLSM_incl X Y
  -message: Type
T: VLSMType message
MX, MY: VLSMMachine T
X:= {| vlsm_type := T; vlsm_machine := MX |}: VLSM message
Y:= {| vlsm_type := T; vlsm_machine := MY |}: VLSM message
Hid: ∀ tr : list transition_item,
  tr =
  pre_VLSM_embedding_finite_trace_project T T id
    id tr
VLSM_incl X Y → VLSM_embedding X Y id id constructor; intros.message: Type
T: VLSMType message
MX, MY: VLSMMachine T
X:= {| vlsm_type := T; vlsm_machine := MX |}: VLSM message
Y:= {| vlsm_type := T; vlsm_machine := MY |}: VLSM message
Hid: ∀ tr : list transition_item,
  tr =
  pre_VLSM_embedding_finite_trace_project T T id
    id tr
H: VLSM_incl X Y
sX: state X
trX: list transition_item
H0: finite_valid_trace X sX trX
finite_valid_trace Y (id sX)
  (pre_VLSM_embedding_finite_trace_project X Y id id
     trX)
    apply (proj1 (VLSM_incl_finite_traces_characterization X Y) H) in H0.message: Type
T: VLSMType message
MX, MY: VLSMMachine T
X:= {| vlsm_type := T; vlsm_machine := MX |}: VLSM message
Y:= {| vlsm_type := T; vlsm_machine := MY |}: VLSM message
Hid: ∀ tr : list transition_item,
  tr =
  pre_VLSM_embedding_finite_trace_project T T id
    id tr
H: VLSM_incl X Y
sX: state X
trX: list transition_item
H0: finite_valid_trace
  {| vlsm_type := T; vlsm_machine := Y |} sX trX
finite_valid_trace Y (id sX)
  (pre_VLSM_embedding_finite_trace_project X Y id id
     trX)
    replace (pre_VLSM_embedding_finite_trace_project _ _ _ _ trX) with trX; [done |].message: Type
T: VLSMType message
MX, MY: VLSMMachine T
X:= {| vlsm_type := T; vlsm_machine := MX |}: VLSM message
Y:= {| vlsm_type := T; vlsm_machine := MY |}: VLSM message
Hid: ∀ tr : list transition_item,
  tr =
  pre_VLSM_embedding_finite_trace_project T T id
    id tr
H: VLSM_incl X Y
sX: state X
trX: list transition_item
H0: finite_valid_trace
  {| vlsm_type := T; vlsm_machine := Y |} sX trX
trX =
pre_VLSM_embedding_finite_trace_project X X id id trX
    by apply Hid.
  -message: Type
T: VLSMType message
MX, MY: VLSMMachine T
X:= {| vlsm_type := T; vlsm_machine := MX |}: VLSM message
Y:= {| vlsm_type := T; vlsm_machine := MY |}: VLSM message
Hid: ∀ tr : list transition_item,
  tr =
  pre_VLSM_embedding_finite_trace_project T T id
    id tr
VLSM_embedding X Y id id → VLSM_incl X Y intro Hproject.message: Type
T: VLSMType message
MX, MY: VLSMMachine T
X:= {| vlsm_type := T; vlsm_machine := MX |}: VLSM message
Y:= {| vlsm_type := T; vlsm_machine := MY |}: VLSM message
Hid: ∀ tr : list transition_item,
  tr =
  pre_VLSM_embedding_finite_trace_project T T id
    id tr
Hproject: VLSM_embedding X Y id id
VLSM_incl X Y apply VLSM_incl_finite_traces_characterization.message: Type
T: VLSMType message
MX, MY: VLSMMachine T
X:= {| vlsm_type := T; vlsm_machine := MX |}: VLSM message
Y:= {| vlsm_type := T; vlsm_machine := MY |}: VLSM message
Hid: ∀ tr : list transition_item,
  tr =
  pre_VLSM_embedding_finite_trace_project T T id
    id tr
Hproject: VLSM_embedding X Y id id
∀ (s : state {| vlsm_type := T; vlsm_machine := MX |}) 
  (tr : list transition_item),
  finite_valid_trace
    {| vlsm_type := T; vlsm_machine := MX |} s tr
  → finite_valid_trace
      {| vlsm_type := T; vlsm_machine := MY |} s tr
    intros.message: Type
T: VLSMType message
MX, MY: VLSMMachine T
X:= {| vlsm_type := T; vlsm_machine := MX |}: VLSM message
Y:= {| vlsm_type := T; vlsm_machine := MY |}: VLSM message
Hid: ∀ tr : list transition_item,
  tr =
  pre_VLSM_embedding_finite_trace_project T T id
    id tr
Hproject: VLSM_embedding X Y id id
s: state {| vlsm_type := T; vlsm_machine := MX |}
tr: list transition_item
H: finite_valid_trace
  {| vlsm_type := T; vlsm_machine := MX |} s tr
finite_valid_trace
  {| vlsm_type := T; vlsm_machine := MY |} s tr apply (VLSM_embedding_finite_valid_trace Hproject) in H.message: Type
T: VLSMType message
MX, MY: VLSMMachine T
X:= {| vlsm_type := T; vlsm_machine := MX |}: VLSM message
Y:= {| vlsm_type := T; vlsm_machine := MY |}: VLSM message
Hid: ∀ tr : list transition_item,
  tr =
  pre_VLSM_embedding_finite_trace_project T T id
    id tr
Hproject: VLSM_embedding X Y id id
s: state {| vlsm_type := T; vlsm_machine := MX |}
tr: list transition_item
H: finite_valid_trace Y (id s)
  (VLSM_embedding_finite_trace_project Hproject tr)
finite_valid_trace
  {| vlsm_type := T; vlsm_machine := MY |} s tr
    replace (VLSM_embedding_finite_trace_project Hproject _) with tr in H; [done |].message: Type
T: VLSMType message
MX, MY: VLSMMachine T
X:= {| vlsm_type := T; vlsm_machine := MX |}: VLSM message
Y:= {| vlsm_type := T; vlsm_machine := MY |}: VLSM message
Hid: ∀ tr : list transition_item,
  tr =
  pre_VLSM_embedding_finite_trace_project T T id
    id tr
Hproject: VLSM_embedding X Y id id
s: state {| vlsm_type := T; vlsm_machine := MX |}
tr: list transition_item
H: finite_valid_trace Y (id s)
  (VLSM_embedding_finite_trace_project Hproject tr)
tr = VLSM_embedding_finite_trace_project Hproject tr
    by apply Hid.
Qed.

Lemma VLSM_incl_is_embedding
  {MX MY : VLSMMachine T}
  (X := mk_vlsm MX) (Y := mk_vlsm MY) :
    VLSM_incl X Y -> VLSM_embedding X Y id id.message: Type
T: VLSMType message
MX, MY: VLSMMachine T
X:= {| vlsm_type := T; vlsm_machine := MX |}: VLSM message
Y:= {| vlsm_type := T; vlsm_machine := MY |}: VLSM message
VLSM_incl X Y → VLSM_embedding X Y id id
Proof.message: Type
T: VLSMType message
MX, MY: VLSMMachine T
X:= {| vlsm_type := T; vlsm_machine := MX |}: VLSM message
Y:= {| vlsm_type := T; vlsm_machine := MY |}: VLSM message
VLSM_incl X Y → VLSM_embedding X Y id id
  exact (proj1 (VLSM_incl_embedding_iff MX MY)).
Qed.

Lemma VLSM_incl_is_embedding_finite_trace_project
  {MX MY : VLSMMachine T}
  (X := mk_vlsm MX) (Y := mk_vlsm MY)
  (Hincl : VLSM_incl X Y)
  : forall tr,
    VLSM_embedding_finite_trace_project (VLSM_incl_is_embedding Hincl) tr = tr.message: Type
T: VLSMType message
MX, MY: VLSMMachine T
X:= {| vlsm_type := T; vlsm_machine := MX |}: VLSM message
Y:= {| vlsm_type := T; vlsm_machine := MY |}: VLSM message
Hincl: VLSM_incl X Y
∀ tr : list transition_item,
  VLSM_embedding_finite_trace_project
    (VLSM_incl_is_embedding Hincl) tr = tr
Proof.message: Type
T: VLSMType message
MX, MY: VLSMMachine T
X:= {| vlsm_type := T; vlsm_machine := MX |}: VLSM message
Y:= {| vlsm_type := T; vlsm_machine := MY |}: VLSM message
Hincl: VLSM_incl X Y
∀ tr : list transition_item,
  VLSM_embedding_finite_trace_project
    (VLSM_incl_is_embedding Hincl) tr = tr
  induction tr; [done |].message: Type
T: VLSMType message
MX, MY: VLSMMachine T
X:= {| vlsm_type := T; vlsm_machine := MX |}: VLSM message
Y:= {| vlsm_type := T; vlsm_machine := MY |}: VLSM message
Hincl: VLSM_incl X Y
a: transition_item
tr: list transition_item
IHtr: VLSM_embedding_finite_trace_project
  (VLSM_incl_is_embedding Hincl) tr = tr
VLSM_embedding_finite_trace_project
  (VLSM_incl_is_embedding Hincl) (a :: tr) = a :: tr
  simpl.message: Type
T: VLSMType message
MX, MY: VLSMMachine T
X:= {| vlsm_type := T; vlsm_machine := MX |}: VLSM message
Y:= {| vlsm_type := T; vlsm_machine := MY |}: VLSM message
Hincl: VLSM_incl X Y
a: transition_item
tr: list transition_item
IHtr: VLSM_embedding_finite_trace_project
  (VLSM_incl_is_embedding Hincl) tr = tr
pre_VLSM_embedding_transition_item_project T T id id a
:: VLSM_embedding_finite_trace_project
     (VLSM_incl_is_embedding Hincl) tr = a :: tr f_equal; [| done].message: Type
T: VLSMType message
MX, MY: VLSMMachine T
X:= {| vlsm_type := T; vlsm_machine := MX |}: VLSM message
Y:= {| vlsm_type := T; vlsm_machine := MY |}: VLSM message
Hincl: VLSM_incl X Y
a: transition_item
tr: list transition_item
IHtr: VLSM_embedding_finite_trace_project
  (VLSM_incl_is_embedding Hincl) tr = tr
pre_VLSM_embedding_transition_item_project T T id id a =
a
  by destruct a.
Qed.

End sec_VLSM_inclusion.

Notation VLSM_incl X Y := (VLSM_incl_part (vlsm_machine X) (vlsm_machine Y)).

Section sec_VLSM_incl_preservation.

VLSM inclusion preservation

Context
  {message : Type}
  {T : VLSMType message}
  (MX MY : VLSMMachine T)
  (X := mk_vlsm MX)
  (Y := mk_vlsm MY)
  .

Definition weak_incl_valid_preservation : Prop :=
  weak_embedding_valid_preservation X Y id id.

Definition strong_incl_valid_preservation : Prop :=
  strong_embedding_valid_preservation X Y id id.

Definition weak_incl_transition_preservation : Prop :=
  weak_embedding_transition_preservation X Y id id.

Definition strong_incl_transition_preservation : Prop :=
  strong_embedding_transition_preservation X Y id id.

Definition strong_incl_initial_state_preservation : Prop :=
  strong_projection_initial_state_preservation X Y id.

Definition weak_incl_initial_message_preservation : Prop :=
  weak_embedding_initial_message_preservation X Y id.

Definition strong_incl_initial_message_preservation : Prop :=
  strong_embedding_initial_message_preservation X Y.

End sec_VLSM_incl_preservation.

Section sec_VLSM_incl_properties.

VLSM inclusion properties

Context
  {message : Type} [T : VLSMType message]
  [MX MY : VLSMMachine T]
  (Hincl : VLSM_incl_part MX MY)
  (X := mk_vlsm MX)
  (Y := mk_vlsm MY)
  .

VLSM inclusion specialized to finite trace.

Lemma VLSM_incl_finite_valid_trace
  (s : state X)
  (tr : list (transition_item X))
  (Htr : finite_valid_trace X s tr)
  : finite_valid_trace Y s tr.message: Type
T: VLSMType message
MX, MY: VLSMMachine T
Hincl: VLSM_incl_part MX MY
X:= {| vlsm_type := T; vlsm_machine := MX |}: VLSM message
Y:= {| vlsm_type := T; vlsm_machine := MY |}: VLSM message
s: state X
tr: list transition_item
Htr: finite_valid_trace X s tr
finite_valid_trace Y s tr
Proof.message: Type
T: VLSMType message
MX, MY: VLSMMachine T
Hincl: VLSM_incl_part MX MY
X:= {| vlsm_type := T; vlsm_machine := MX |}: VLSM message
Y:= {| vlsm_type := T; vlsm_machine := MY |}: VLSM message
s: state X
tr: list transition_item
Htr: finite_valid_trace X s tr
finite_valid_trace Y s tr
  apply (VLSM_embedding_finite_valid_trace (VLSM_incl_is_embedding Hincl))
    in Htr.message: Type
T: VLSMType message
MX, MY: VLSMMachine T
Hincl: VLSM_incl_part MX MY
X:= {| vlsm_type := T; vlsm_machine := MX |}: VLSM message
Y:= {| vlsm_type := T; vlsm_machine := MY |}: VLSM message
s: state X
tr: list transition_item
Htr: finite_valid_trace
  {| vlsm_type := T; vlsm_machine := MY |}
  (id s)
  (VLSM_embedding_finite_trace_project
     (VLSM_incl_is_embedding Hincl) tr)
finite_valid_trace Y s tr
  by rewrite (VLSM_incl_is_embedding_finite_trace_project Hincl) in Htr.
Qed.

Lemma VLSM_incl_finite_valid_trace_init_to
  (s f : state X)
  (tr : list (transition_item X))
  (Htr : finite_valid_trace_init_to X s f tr)
  : finite_valid_trace_init_to Y s f tr.message: Type
T: VLSMType message
MX, MY: VLSMMachine T
Hincl: VLSM_incl_part MX MY
X:= {| vlsm_type := T; vlsm_machine := MX |}: VLSM message
Y:= {| vlsm_type := T; vlsm_machine := MY |}: VLSM message
s, f: state X
tr: list transition_item
Htr: finite_valid_trace_init_to X s f tr
finite_valid_trace_init_to Y s f tr
Proof.message: Type
T: VLSMType message
MX, MY: VLSMMachine T
Hincl: VLSM_incl_part MX MY
X:= {| vlsm_type := T; vlsm_machine := MX |}: VLSM message
Y:= {| vlsm_type := T; vlsm_machine := MY |}: VLSM message
s, f: state X
tr: list transition_item
Htr: finite_valid_trace_init_to X s f tr
finite_valid_trace_init_to Y s f tr
  apply (VLSM_embedding_finite_valid_trace_init_to (VLSM_incl_is_embedding Hincl))
    in Htr.message: Type
T: VLSMType message
MX, MY: VLSMMachine T
Hincl: VLSM_incl_part MX MY
X:= {| vlsm_type := T; vlsm_machine := MX |}: VLSM message
Y:= {| vlsm_type := T; vlsm_machine := MY |}: VLSM message
s, f: state X
tr: list transition_item
Htr: finite_valid_trace_init_to
  {| vlsm_type := T; vlsm_machine := MY |}
  (id s) (id f)
  (VLSM_embedding_finite_trace_project
     (VLSM_incl_is_embedding Hincl) tr)
finite_valid_trace_init_to Y s f tr
  by rewrite (VLSM_incl_is_embedding_finite_trace_project Hincl) in Htr.
Qed.

Lemma VLSM_incl_valid_state
  (s : state X)
  (Hs : valid_state_prop X s)
  : valid_state_prop Y s.message: Type
T: VLSMType message
MX, MY: VLSMMachine T
Hincl: VLSM_incl_part MX MY
X:= {| vlsm_type := T; vlsm_machine := MX |}: VLSM message
Y:= {| vlsm_type := T; vlsm_machine := MY |}: VLSM message
s: state X
Hs: valid_state_prop X s
valid_state_prop Y s
Proof.message: Type
T: VLSMType message
MX, MY: VLSMMachine T
Hincl: VLSM_incl_part MX MY
X:= {| vlsm_type := T; vlsm_machine := MX |}: VLSM message
Y:= {| vlsm_type := T; vlsm_machine := MY |}: VLSM message
s: state X
Hs: valid_state_prop X s
valid_state_prop Y s
  by apply (VLSM_embedding_valid_state (VLSM_incl_is_embedding Hincl)).
Qed.

Lemma VLSM_incl_initial_state
  (is : state X)
  : initial_state_prop X is -> initial_state_prop Y is.message: Type
T: VLSMType message
MX, MY: VLSMMachine T
Hincl: VLSM_incl_part MX MY
X:= {| vlsm_type := T; vlsm_machine := MX |}: VLSM message
Y:= {| vlsm_type := T; vlsm_machine := MY |}: VLSM message
is: state X
initial_state_prop is → initial_state_prop is
Proof.message: Type
T: VLSMType message
MX, MY: VLSMMachine T
Hincl: VLSM_incl_part MX MY
X:= {| vlsm_type := T; vlsm_machine := MX |}: VLSM message
Y:= {| vlsm_type := T; vlsm_machine := MY |}: VLSM message
is: state X
initial_state_prop is → initial_state_prop is
  by apply (VLSM_embedding_initial_state (VLSM_incl_is_embedding Hincl)).
Qed.

Lemma VLSM_incl_finite_valid_trace_from
  (s : state X)
  (tr : list (transition_item X))
  (Htr : finite_valid_trace_from X s tr)
  : finite_valid_trace_from Y s tr.message: Type
T: VLSMType message
MX, MY: VLSMMachine T
Hincl: VLSM_incl_part MX MY
X:= {| vlsm_type := T; vlsm_machine := MX |}: VLSM message
Y:= {| vlsm_type := T; vlsm_machine := MY |}: VLSM message
s: state X
tr: list transition_item
Htr: finite_valid_trace_from X s tr
finite_valid_trace_from Y s tr
Proof.message: Type
T: VLSMType message
MX, MY: VLSMMachine T
Hincl: VLSM_incl_part MX MY
X:= {| vlsm_type := T; vlsm_machine := MX |}: VLSM message
Y:= {| vlsm_type := T; vlsm_machine := MY |}: VLSM message
s: state X
tr: list transition_item
Htr: finite_valid_trace_from X s tr
finite_valid_trace_from Y s tr
  apply (VLSM_embedding_finite_valid_trace_from (VLSM_incl_is_embedding Hincl))
    in Htr.message: Type
T: VLSMType message
MX, MY: VLSMMachine T
Hincl: VLSM_incl_part MX MY
X:= {| vlsm_type := T; vlsm_machine := MX |}: VLSM message
Y:= {| vlsm_type := T; vlsm_machine := MY |}: VLSM message
s: state X
tr: list transition_item
Htr: finite_valid_trace_from
  {| vlsm_type := T; vlsm_machine := MY |}
  (id s)
  (VLSM_embedding_finite_trace_project
     (VLSM_incl_is_embedding Hincl) tr)
finite_valid_trace_from Y s tr
  by rewrite (VLSM_incl_is_embedding_finite_trace_project Hincl) in Htr.
Qed.

Lemma VLSM_incl_finite_valid_trace_from_to
  (s f : state X)
  (tr : list (transition_item X))
  (Htr : finite_valid_trace_from_to X s f tr)
  : finite_valid_trace_from_to Y s f tr.message: Type
T: VLSMType message
MX, MY: VLSMMachine T
Hincl: VLSM_incl_part MX MY
X:= {| vlsm_type := T; vlsm_machine := MX |}: VLSM message
Y:= {| vlsm_type := T; vlsm_machine := MY |}: VLSM message
s, f: state X
tr: list transition_item
Htr: finite_valid_trace_from_to X s f tr
finite_valid_trace_from_to Y s f tr
Proof.message: Type
T: VLSMType message
MX, MY: VLSMMachine T
Hincl: VLSM_incl_part MX MY
X:= {| vlsm_type := T; vlsm_machine := MX |}: VLSM message
Y:= {| vlsm_type := T; vlsm_machine := MY |}: VLSM message
s, f: state X
tr: list transition_item
Htr: finite_valid_trace_from_to X s f tr
finite_valid_trace_from_to Y s f tr
  apply (VLSM_embedding_finite_valid_trace_from_to (VLSM_incl_is_embedding Hincl))
    in Htr.message: Type
T: VLSMType message
MX, MY: VLSMMachine T
Hincl: VLSM_incl_part MX MY
X:= {| vlsm_type := T; vlsm_machine := MX |}: VLSM message
Y:= {| vlsm_type := T; vlsm_machine := MY |}: VLSM message
s, f: state X
tr: list transition_item
Htr: finite_valid_trace_from_to
  {| vlsm_type := T; vlsm_machine := MY |}
  (id s) (id f)
  (VLSM_embedding_finite_trace_project
     (VLSM_incl_is_embedding Hincl) tr)
finite_valid_trace_from_to Y s f tr
  by rewrite (VLSM_incl_is_embedding_finite_trace_project Hincl) in Htr.
Qed.

Lemma VLSM_incl_in_futures
  (s1 s2 : state X)
  : in_futures X s1 s2 -> in_futures Y s1 s2.message: Type
T: VLSMType message
MX, MY: VLSMMachine T
Hincl: VLSM_incl_part MX MY
X:= {| vlsm_type := T; vlsm_machine := MX |}: VLSM message
Y:= {| vlsm_type := T; vlsm_machine := MY |}: VLSM message
s1, s2: state X
in_futures X s1 s2 → in_futures Y s1 s2
Proof.message: Type
T: VLSMType message
MX, MY: VLSMMachine T
Hincl: VLSM_incl_part MX MY
X:= {| vlsm_type := T; vlsm_machine := MX |}: VLSM message
Y:= {| vlsm_type := T; vlsm_machine := MY |}: VLSM message
s1, s2: state X
in_futures X s1 s2 → in_futures Y s1 s2
  by apply (VLSM_embedding_in_futures (VLSM_incl_is_embedding Hincl)).
Qed.

Lemma VLSM_incl_input_valid_transition
  : forall l s im s' om,
  input_valid_transition X l (s, im) (s', om) ->
  input_valid_transition Y l (s, im) (s', om).message: Type
T: VLSMType message
MX, MY: VLSMMachine T
Hincl: VLSM_incl_part MX MY
X:= {| vlsm_type := T; vlsm_machine := MX |}: VLSM message
Y:= {| vlsm_type := T; vlsm_machine := MY |}: VLSM message
∀ (l : label X) (s : state X) (im : option message) 
  (s' : state X) (om : option message),
  input_valid_transition X l (s, im) (s', om)
  → input_valid_transition Y l (s, im) (s', om)
Proof.message: Type
T: VLSMType message
MX, MY: VLSMMachine T
Hincl: VLSM_incl_part MX MY
X:= {| vlsm_type := T; vlsm_machine := MX |}: VLSM message
Y:= {| vlsm_type := T; vlsm_machine := MY |}: VLSM message
∀ (l : label X) (s : state X) (im : option message) 
  (s' : state X) (om : option message),
  input_valid_transition X l (s, im) (s', om)
  → input_valid_transition Y l (s, im) (s', om)
  by apply (VLSM_embedding_input_valid_transition (VLSM_incl_is_embedding Hincl)).
Qed.

Lemma VLSM_incl_input_valid
  : forall l s im,
  input_valid X l (s, im) ->
  input_valid Y l (s, im).message: Type
T: VLSMType message
MX, MY: VLSMMachine T
Hincl: VLSM_incl_part MX MY
X:= {| vlsm_type := T; vlsm_machine := MX |}: VLSM message
Y:= {| vlsm_type := T; vlsm_machine := MY |}: VLSM message
∀ (l : label X) (s : state X) (im : option message),
  input_valid X l (s, im) → input_valid Y l (s, im)
Proof.message: Type
T: VLSMType message
MX, MY: VLSMMachine T
Hincl: VLSM_incl_part MX MY
X:= {| vlsm_type := T; vlsm_machine := MX |}: VLSM message
Y:= {| vlsm_type := T; vlsm_machine := MY |}: VLSM message
∀ (l : label X) (s : state X) (im : option message),
  input_valid X l (s, im) → input_valid Y l (s, im)
  by apply (VLSM_embedding_input_valid (VLSM_incl_is_embedding Hincl)).
Qed.

VLSM_incl almost implies inclusion of the valid_state_message_prop sets. Some additional hypotheses are required because VLSM_incl only refers to traces, and valid_initial_state_message means that valid_state_message_prop includes some pairs that do not appear in any transition.

Lemma VLSM_incl_valid_state_message
  (Hmessage : strong_incl_initial_message_preservation MX MY)
  : forall s om, valid_state_message_prop X s om -> valid_state_message_prop Y s om.message: Type
T: VLSMType message
MX, MY: VLSMMachine T
Hincl: VLSM_incl_part MX MY
X:= {| vlsm_type := T; vlsm_machine := MX |}: VLSM message
Y:= {| vlsm_type := T; vlsm_machine := MY |}: VLSM message
Hmessage: strong_incl_initial_message_preservation MX
  MY
∀ (s : state X) (om : option message),
  valid_state_message_prop X s om
  → valid_state_message_prop Y s om
Proof.message: Type
T: VLSMType message
MX, MY: VLSMMachine T
Hincl: VLSM_incl_part MX MY
X:= {| vlsm_type := T; vlsm_machine := MX |}: VLSM message
Y:= {| vlsm_type := T; vlsm_machine := MY |}: VLSM message
Hmessage: strong_incl_initial_message_preservation MX
  MY
∀ (s : state X) (om : option message),
  valid_state_message_prop X s om
  → valid_state_message_prop Y s om
  intros s om.message: Type
T: VLSMType message
MX, MY: VLSMMachine T
Hincl: VLSM_incl_part MX MY
X:= {| vlsm_type := T; vlsm_machine := MX |}: VLSM message
Y:= {| vlsm_type := T; vlsm_machine := MY |}: VLSM message
Hmessage: strong_incl_initial_message_preservation MX
  MY
s: state X
om: option message
valid_state_message_prop X s om
→ valid_state_message_prop Y s om
  by apply (VLSM_embedding_valid_state_message (VLSM_incl_is_embedding Hincl)).
Qed.

Lemma VLSM_incl_can_produce
  (s : state T)
  (om : option message)
  : option_can_produce X s om -> option_can_produce Y s om.message: Type
T: VLSMType message
MX, MY: VLSMMachine T
Hincl: VLSM_incl_part MX MY
X:= {| vlsm_type := T; vlsm_machine := MX |}: VLSM message
Y:= {| vlsm_type := T; vlsm_machine := MY |}: VLSM message
s: state T
om: option message
option_can_produce X s om → option_can_produce Y s om
Proof.message: Type
T: VLSMType message
MX, MY: VLSMMachine T
Hincl: VLSM_incl_part MX MY
X:= {| vlsm_type := T; vlsm_machine := MX |}: VLSM message
Y:= {| vlsm_type := T; vlsm_machine := MY |}: VLSM message
s: state T
om: option message
option_can_produce X s om → option_can_produce Y s om
  by apply (VLSM_embedding_can_produce (VLSM_incl_is_embedding Hincl)).
Qed.

Lemma VLSM_incl_can_emit
  (m : message)
  : can_emit X m -> can_emit Y m.message: Type
T: VLSMType message
MX, MY: VLSMMachine T
Hincl: VLSM_incl_part MX MY
X:= {| vlsm_type := T; vlsm_machine := MX |}: VLSM message
Y:= {| vlsm_type := T; vlsm_machine := MY |}: VLSM message
m: message
can_emit X m → can_emit Y m
Proof.message: Type
T: VLSMType message
MX, MY: VLSMMachine T
Hincl: VLSM_incl_part MX MY
X:= {| vlsm_type := T; vlsm_machine := MX |}: VLSM message
Y:= {| vlsm_type := T; vlsm_machine := MY |}: VLSM message
m: message
can_emit X m → can_emit Y m
  by apply (VLSM_embedding_can_emit (VLSM_incl_is_embedding Hincl)).
Qed.

Lemma VLSM_incl_valid_message :
  strong_incl_initial_message_preservation MX MY ->
  forall (m : message),
    valid_message_prop X m -> valid_message_prop Y m.message: Type
T: VLSMType message
MX, MY: VLSMMachine T
Hincl: VLSM_incl_part MX MY
X:= {| vlsm_type := T; vlsm_machine := MX |}: VLSM message
Y:= {| vlsm_type := T; vlsm_machine := MY |}: VLSM message
strong_incl_initial_message_preservation MX MY
→ ∀ m : message,
    valid_message_prop X m → valid_message_prop Y m
Proof.message: Type
T: VLSMType message
MX, MY: VLSMMachine T
Hincl: VLSM_incl_part MX MY
X:= {| vlsm_type := T; vlsm_machine := MX |}: VLSM message
Y:= {| vlsm_type := T; vlsm_machine := MY |}: VLSM message
strong_incl_initial_message_preservation MX MY
→ ∀ m : message,
    valid_message_prop X m → valid_message_prop Y m
  intros Hinitial_valid_message m [s Hm].message: Type
T: VLSMType message
MX, MY: VLSMMachine T
Hincl: VLSM_incl_part MX MY
X:= {| vlsm_type := T; vlsm_machine := MX |}: VLSM message
Y:= {| vlsm_type := T; vlsm_machine := MY |}: VLSM message
Hinitial_valid_message: strong_incl_initial_message_preservation
  MX MY
m: message
s: state X
Hm: valid_state_message_prop X s (Some m)
valid_message_prop Y m
  by exists s; revert Hm; apply VLSM_incl_valid_state_message.
Qed.

Lemma VLSM_incl_infinite_valid_trace_from
  s ls
  : infinite_valid_trace_from X s ls ->
    infinite_valid_trace_from Y s ls.message: Type
T: VLSMType message
MX, MY: VLSMMachine T
Hincl: VLSM_incl_part MX MY
X:= {| vlsm_type := T; vlsm_machine := MX |}: VLSM message
Y:= {| vlsm_type := T; vlsm_machine := MY |}: VLSM message
s: state X
ls: Streams.Stream transition_item
infinite_valid_trace_from X s ls
→ infinite_valid_trace_from Y s ls
Proof.message: Type
T: VLSMType message
MX, MY: VLSMMachine T
Hincl: VLSM_incl_part MX MY
X:= {| vlsm_type := T; vlsm_machine := MX |}: VLSM message
Y:= {| vlsm_type := T; vlsm_machine := MY |}: VLSM message
s: state X
ls: Streams.Stream transition_item
infinite_valid_trace_from X s ls
→ infinite_valid_trace_from Y s ls
  intros Hls.message: Type
T: VLSMType message
MX, MY: VLSMMachine T
Hincl: VLSM_incl_part MX MY
X:= {| vlsm_type := T; vlsm_machine := MX |}: VLSM message
Y:= {| vlsm_type := T; vlsm_machine := MY |}: VLSM message
s: state X
ls: Streams.Stream transition_item
Hls: infinite_valid_trace_from X s ls
infinite_valid_trace_from Y s ls
  apply (VLSM_embedding_infinite_valid_trace_from (VLSM_incl_is_embedding Hincl)) in Hls.message: Type
T: VLSMType message
MX, MY: VLSMMachine T
Hincl: VLSM_incl_part MX MY
X:= {| vlsm_type := T; vlsm_machine := MX |}: VLSM message
Y:= {| vlsm_type := T; vlsm_machine := MY |}: VLSM message
s: state X
ls: Streams.Stream transition_item
Hls: infinite_valid_trace_from
  {| vlsm_type := T; vlsm_machine := MY |}
  (id s)
  (VLSM_embedding_infinite_trace_project
     (VLSM_incl_is_embedding Hincl) ls)
infinite_valid_trace_from Y s ls
  revert Hls.message: Type
T: VLSMType message
MX, MY: VLSMMachine T
Hincl: VLSM_incl_part MX MY
X:= {| vlsm_type := T; vlsm_machine := MX |}: VLSM message
Y:= {| vlsm_type := T; vlsm_machine := MY |}: VLSM message
s: state X
ls: Streams.Stream transition_item
infinite_valid_trace_from
  {| vlsm_type := T; vlsm_machine := MY |} (id s)
  (VLSM_embedding_infinite_trace_project
     (VLSM_incl_is_embedding Hincl) ls)
→ infinite_valid_trace_from Y s ls
  apply infinite_valid_trace_from_EqSt.message: Type
T: VLSMType message
MX, MY: VLSMMachine T
Hincl: VLSM_incl_part MX MY
X:= {| vlsm_type := T; vlsm_machine := MX |}: VLSM message
Y:= {| vlsm_type := T; vlsm_machine := MY |}: VLSM message
s: state X
ls: Streams.Stream transition_item
Streams.EqSt
  (VLSM_embedding_infinite_trace_project
     (VLSM_incl_is_embedding Hincl) ls) ls
  apply Streams.ntheq_eqst.message: Type
T: VLSMType message
MX, MY: VLSMMachine T
Hincl: VLSM_incl_part MX MY
X:= {| vlsm_type := T; vlsm_machine := MX |}: VLSM message
Y:= {| vlsm_type := T; vlsm_machine := MY |}: VLSM message
s: state X
ls: Streams.Stream transition_item
∀ n : nat,
  Streams.Str_nth n
    (VLSM_embedding_infinite_trace_project
       (VLSM_incl_is_embedding Hincl) ls) =
  Streams.Str_nth n ls
  unfold VLSM_embedding_infinite_trace_project, pre_VLSM_embedding_infinite_trace_project.message: Type
T: VLSMType message
MX, MY: VLSMMachine T
Hincl: VLSM_incl_part MX MY
X:= {| vlsm_type := T; vlsm_machine := MX |}: VLSM message
Y:= {| vlsm_type := T; vlsm_machine := MY |}: VLSM message
s: state X
ls: Streams.Stream transition_item
∀ n : nat,
  Streams.Str_nth n
    (Streams.map
       (pre_VLSM_embedding_transition_item_project
          {| vlsm_type := T; vlsm_machine := MX |}
          {| vlsm_type := T; vlsm_machine := MY |} id
          id) ls) = Streams.Str_nth n ls
  intro n.message: Type
T: VLSMType message
MX, MY: VLSMMachine T
Hincl: VLSM_incl_part MX MY
X:= {| vlsm_type := T; vlsm_machine := MX |}: VLSM message
Y:= {| vlsm_type := T; vlsm_machine := MY |}: VLSM message
s: state X
ls: Streams.Stream transition_item
n: nat
Streams.Str_nth n
  (Streams.map
     (pre_VLSM_embedding_transition_item_project
        {| vlsm_type := T; vlsm_machine := MX |}
        {| vlsm_type := T; vlsm_machine := MY |} id id)
     ls) = Streams.Str_nth n ls rewrite Streams.Str_nth_map.message: Type
T: VLSMType message
MX, MY: VLSMMachine T
Hincl: VLSM_incl_part MX MY
X:= {| vlsm_type := T; vlsm_machine := MX |}: VLSM message
Y:= {| vlsm_type := T; vlsm_machine := MY |}: VLSM message
s: state X
ls: Streams.Stream transition_item
n: nat
pre_VLSM_embedding_transition_item_project
  {| vlsm_type := T; vlsm_machine := MX |}
  {| vlsm_type := T; vlsm_machine := MY |} id id
  (Streams.Str_nth n ls) = Streams.Str_nth n ls
  by destruct (Streams.Str_nth _ _).
Qed.

Lemma VLSM_incl_infinite_valid_trace
  s ls
  : infinite_valid_trace X s ls -> infinite_valid_trace Y s ls.message: Type
T: VLSMType message
MX, MY: VLSMMachine T
Hincl: VLSM_incl_part MX MY
X:= {| vlsm_type := T; vlsm_machine := MX |}: VLSM message
Y:= {| vlsm_type := T; vlsm_machine := MY |}: VLSM message
s: state X
ls: Streams.Stream transition_item
infinite_valid_trace X s ls
→ infinite_valid_trace Y s ls
Proof.message: Type
T: VLSMType message
MX, MY: VLSMMachine T
Hincl: VLSM_incl_part MX MY
X:= {| vlsm_type := T; vlsm_machine := MX |}: VLSM message
Y:= {| vlsm_type := T; vlsm_machine := MY |}: VLSM message
s: state X
ls: Streams.Stream transition_item
infinite_valid_trace X s ls
→ infinite_valid_trace Y s ls
  intros [Htr His].message: Type
T: VLSMType message
MX, MY: VLSMMachine T
Hincl: VLSM_incl_part MX MY
X:= {| vlsm_type := T; vlsm_machine := MX |}: VLSM message
Y:= {| vlsm_type := T; vlsm_machine := MY |}: VLSM message
s: state X
ls: Streams.Stream transition_item
Htr: infinite_valid_trace_from X s ls
His: initial_state_prop s
infinite_valid_trace Y s ls split.message: Type
T: VLSMType message
MX, MY: VLSMMachine T
Hincl: VLSM_incl_part MX MY
X:= {| vlsm_type := T; vlsm_machine := MX |}: VLSM message
Y:= {| vlsm_type := T; vlsm_machine := MY |}: VLSM message
s: state X
ls: Streams.Stream transition_item
Htr: infinite_valid_trace_from X s ls
His: initial_state_prop s
infinite_valid_trace_from Y s ls
message: Type
T: VLSMType message
MX, MY: VLSMMachine T
Hincl: VLSM_incl_part MX MY
X:= {| vlsm_type := T; vlsm_machine := MX |}: VLSM message
Y:= {| vlsm_type := T; vlsm_machine := MY |}: VLSM message
s: state X
ls: Streams.Stream transition_item
Htr: infinite_valid_trace_from X s ls
His: initial_state_prop s
initial_state_prop s
  -message: Type
T: VLSMType message
MX, MY: VLSMMachine T
Hincl: VLSM_incl_part MX MY
X:= {| vlsm_type := T; vlsm_machine := MX |}: VLSM message
Y:= {| vlsm_type := T; vlsm_machine := MY |}: VLSM message
s: state X
ls: Streams.Stream transition_item
Htr: infinite_valid_trace_from X s ls
His: initial_state_prop s
infinite_valid_trace_from Y s ls by apply VLSM_incl_infinite_valid_trace_from.
  -message: Type
T: VLSMType message
MX, MY: VLSMMachine T
Hincl: VLSM_incl_part MX MY
X:= {| vlsm_type := T; vlsm_machine := MX |}: VLSM message
Y:= {| vlsm_type := T; vlsm_machine := MY |}: VLSM message
s: state X
ls: Streams.Stream transition_item
Htr: infinite_valid_trace_from X s ls
His: initial_state_prop s
initial_state_prop s by apply VLSM_incl_initial_state.
Qed.

Lemma VLSM_incl_valid_trace
  : forall t, valid_trace_prop X t -> valid_trace_prop Y t.message: Type
T: VLSMType message
MX, MY: VLSMMachine T
Hincl: VLSM_incl_part MX MY
X:= {| vlsm_type := T; vlsm_machine := MX |}: VLSM message
Y:= {| vlsm_type := T; vlsm_machine := MY |}: VLSM message
∀ t : Trace,
  valid_trace_prop X t → valid_trace_prop Y t
Proof.message: Type
T: VLSMType message
MX, MY: VLSMMachine T
Hincl: VLSM_incl_part MX MY
X:= {| vlsm_type := T; vlsm_machine := MX |}: VLSM message
Y:= {| vlsm_type := T; vlsm_machine := MY |}: VLSM message
∀ t : Trace,
  valid_trace_prop X t → valid_trace_prop Y t
  intros [s tr | s tr]; simpl.message: Type
T: VLSMType message
MX, MY: VLSMMachine T
Hincl: VLSM_incl_part MX MY
X:= {| vlsm_type := T; vlsm_machine := MX |}: VLSM message
Y:= {| vlsm_type := T; vlsm_machine := MY |}: VLSM message
s: state X
tr: list transition_item
finite_valid_trace X s tr → finite_valid_trace Y s tr
message: Type
T: VLSMType message
MX, MY: VLSMMachine T
Hincl: VLSM_incl_part MX MY
X:= {| vlsm_type := T; vlsm_machine := MX |}: VLSM message
Y:= {| vlsm_type := T; vlsm_machine := MY |}: VLSM message
s: state X
tr: Streams.Stream transition_item
infinite_valid_trace X s tr
→ infinite_valid_trace Y s tr
  -message: Type
T: VLSMType message
MX, MY: VLSMMachine T
Hincl: VLSM_incl_part MX MY
X:= {| vlsm_type := T; vlsm_machine := MX |}: VLSM message
Y:= {| vlsm_type := T; vlsm_machine := MY |}: VLSM message
s: state X
tr: list transition_item
finite_valid_trace X s tr → finite_valid_trace Y s tr by apply VLSM_incl_finite_valid_trace.
  -message: Type
T: VLSMType message
MX, MY: VLSMMachine T
Hincl: VLSM_incl_part MX MY
X:= {| vlsm_type := T; vlsm_machine := MX |}: VLSM message
Y:= {| vlsm_type := T; vlsm_machine := MY |}: VLSM message
s: state X
tr: Streams.Stream transition_item
infinite_valid_trace X s tr
→ infinite_valid_trace Y s tr by apply VLSM_incl_infinite_valid_trace.
Qed.

End sec_VLSM_incl_properties.

We instantiate the above for VLSM inclusions

Section sec_basic_VLSM_incl.

Context
  {message : Type}
  {T : VLSMType message}
  (MX MY : VLSMMachine T)
  (X := mk_vlsm MX)
  (Y := mk_vlsm MY)
  .

Lemma basic_VLSM_incl
  (Hinitial_state : strong_incl_initial_state_preservation MX MY)
  (Hinitial_valid_message : weak_incl_initial_message_preservation MX MY)
  (Hvalid : weak_incl_valid_preservation MX MY)
  (Htransition : weak_incl_transition_preservation MX MY)
  : VLSM_incl X Y.message: Type
T: VLSMType message
MX, MY: VLSMMachine T
X:= {| vlsm_type := T; vlsm_machine := MX |}: VLSM message
Y:= {| vlsm_type := T; vlsm_machine := MY |}: VLSM message
Hinitial_state: strong_incl_initial_state_preservation
  MX MY
Hinitial_valid_message: weak_incl_initial_message_preservation
  MX MY
Hvalid: weak_incl_valid_preservation MX MY
Htransition: weak_incl_transition_preservation MX MY
VLSM_incl X Y
Proof.message: Type
T: VLSMType message
MX, MY: VLSMMachine T
X:= {| vlsm_type := T; vlsm_machine := MX |}: VLSM message
Y:= {| vlsm_type := T; vlsm_machine := MY |}: VLSM message
Hinitial_state: strong_incl_initial_state_preservation
  MX MY
Hinitial_valid_message: weak_incl_initial_message_preservation
  MX MY
Hvalid: weak_incl_valid_preservation MX MY
Htransition: weak_incl_transition_preservation MX MY
VLSM_incl X Y
  by apply VLSM_incl_embedding_iff, basic_VLSM_embedding.
Qed.

Lemma basic_VLSM_strong_incl
  (Hinitial_state : strong_incl_initial_state_preservation MX MY)
  (Hinitial_valid_message : strong_incl_initial_message_preservation MX MY)
  (Hvalid : strong_incl_valid_preservation MX MY)
  (Htransition : strong_incl_transition_preservation MX MY)
  : VLSM_incl X Y.message: Type
T: VLSMType message
MX, MY: VLSMMachine T
X:= {| vlsm_type := T; vlsm_machine := MX |}: VLSM message
Y:= {| vlsm_type := T; vlsm_machine := MY |}: VLSM message
Hinitial_state: strong_incl_initial_state_preservation
  MX MY
Hinitial_valid_message: strong_incl_initial_message_preservation
  MX MY
Hvalid: strong_incl_valid_preservation MX MY
Htransition: strong_incl_transition_preservation MX
  MY
VLSM_incl X Y
Proof.message: Type
T: VLSMType message
MX, MY: VLSMMachine T
X:= {| vlsm_type := T; vlsm_machine := MX |}: VLSM message
Y:= {| vlsm_type := T; vlsm_machine := MY |}: VLSM message
Hinitial_state: strong_incl_initial_state_preservation
  MX MY
Hinitial_valid_message: strong_incl_initial_message_preservation
  MX MY
Hvalid: strong_incl_valid_preservation MX MY
Htransition: strong_incl_transition_preservation MX
  MY
VLSM_incl X Y
  by apply VLSM_incl_embedding_iff, basic_VLSM_strong_embedding.
Qed.

End sec_basic_VLSM_incl.