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 Coq Require Import FunctionalExtensionality.
From VLSM.Core Require Import VLSM.
From VLSM.Core Require Export VLSMPartialProjection VLSMStutteringEmbedding.
From VLSM.Core Require Export VLSMTotalProjection VLSMEmbedding.
From VLSM.Core Require Export VLSMInclusion VLSMEquality.

Core: VLSM Projection Properties

Section sec_same_VLSM_embedding.

Same VLSM embedding

Context
  {message : Type}
  (X1 X2 : VLSM message)
  (Heq : X1 = X2)
  .

Lemma same_VLSM_embedding
  : VLSM_embedding X1 X2 (same_VLSM_label_rew Heq) (same_VLSM_state_rew Heq).message: Type
X1, X2: VLSM message
Heq: X1 = X2
VLSM_embedding X1 X2 (same_VLSM_label_rew Heq)
  (same_VLSM_state_rew Heq)
Proof.message: Type
X1, X2: VLSM message
Heq: X1 = X2
VLSM_embedding X1 X2 (same_VLSM_label_rew Heq)
  (same_VLSM_state_rew Heq)
  apply basic_VLSM_strong_embedding; intro.message: Type
X1, X2: VLSM message
Heq: X1 = X2
l: label X1
∀ (s : state X1) (om : option message),
  valid l (s, om)
  → valid (same_VLSM_label_rew Heq l)
      (same_VLSM_state_rew Heq s, om)
message: Type
X1, X2: VLSM message
Heq: X1 = X2
l: label X1
∀ (s : state X1) (om : option message) 
  (s' : state X1) (om' : option message),
  transition l (s, om) = (s', om')
  → transition (same_VLSM_label_rew Heq l)
      (same_VLSM_state_rew Heq s, om) =
    (same_VLSM_state_rew Heq s', om')
message: Type
X1, X2: VLSM message
Heq: X1 = X2
s: state X1
initial_state_prop s
→ initial_state_prop (same_VLSM_state_rew Heq s)
message: Type
X1, X2: VLSM message
Heq: X1 = X2
m: message
initial_message_prop m → initial_message_prop m
  -message: Type
X1, X2: VLSM message
Heq: X1 = X2
l: label X1
∀ (s : state X1) (om : option message),
  valid l (s, om)
  → valid (same_VLSM_label_rew Heq l)
      (same_VLSM_state_rew Heq s, om) by apply same_VLSM_valid_preservation.
  -message: Type
X1, X2: VLSM message
Heq: X1 = X2
l: label X1
∀ (s : state X1) (om : option message) (s' : state X1) 
  (om' : option message),
  transition l (s, om) = (s', om')
  → transition (same_VLSM_label_rew Heq l)
      (same_VLSM_state_rew Heq s, om) =
    (same_VLSM_state_rew Heq s', om') by apply same_VLSM_transition_preservation.
  -message: Type
X1, X2: VLSM message
Heq: X1 = X2
s: state X1
initial_state_prop s
→ initial_state_prop (same_VLSM_state_rew Heq s) by apply same_VLSM_initial_state_preservation.
  -message: Type
X1, X2: VLSM message
Heq: X1 = X2
m: message
initial_message_prop m → initial_message_prop m by apply same_VLSM_initial_message_preservation.
Qed.

End sec_same_VLSM_embedding.

Section sec_transitivity_props.

Transitivity properties

Lemma pre_VLSM_projection_finite_trace_project_trans
  {message : Type}
  (TX TY TZ : VLSMType message)
  (project_labelXY : label TX -> option (label TY))
  (project_stateXY : state TX -> state TY)
  (project_labelYZ : label TY -> option (label TZ))
  (project_stateYZ : state TY -> state TZ)
  : forall trX,
    pre_VLSM_projection_finite_trace_project TX TZ
      (mbind project_labelYZ ∘ project_labelXY)
      (project_stateYZ ∘ project_stateXY)
      trX
      =
    pre_VLSM_projection_finite_trace_project TY TZ project_labelYZ project_stateYZ
      (pre_VLSM_projection_finite_trace_project TX TY project_labelXY project_stateXY
        trX).message: Type
TX, TY, TZ: VLSMType message
project_labelXY: label TX → option (label TY)
project_stateXY: state TX → state TY
project_labelYZ: label TY → option (label TZ)
project_stateYZ: state TY → state TZ
∀ trX : list transition_item,
  pre_VLSM_projection_finite_trace_project TX TZ
    (mbind project_labelYZ ∘ project_labelXY)
    (project_stateYZ ∘ project_stateXY) trX =
  pre_VLSM_projection_finite_trace_project TY TZ
    project_labelYZ project_stateYZ
    (pre_VLSM_projection_finite_trace_project TX TY
       project_labelXY project_stateXY trX)
Proof.message: Type
TX, TY, TZ: VLSMType message
project_labelXY: label TX → option (label TY)
project_stateXY: state TX → state TY
project_labelYZ: label TY → option (label TZ)
project_stateYZ: state TY → state TZ
∀ trX : list transition_item,
  pre_VLSM_projection_finite_trace_project TX TZ
    (mbind project_labelYZ ∘ project_labelXY)
    (project_stateYZ ∘ project_stateXY) trX =
  pre_VLSM_projection_finite_trace_project TY TZ
    project_labelYZ project_stateYZ
    (pre_VLSM_projection_finite_trace_project TX TY
       project_labelXY project_stateXY trX)
  induction trX; [done |]; destruct a; cbn;
    unfold pre_VLSM_projection_transition_item_project; cbn;
    unfold mbind, option_bind; cbn.message: Type
TX, TY, TZ: VLSMType message
project_labelXY: label TX → option (label TY)
project_stateXY: state TX → state TY
project_labelYZ: label TY → option (label TZ)
project_stateYZ: state TY → state TZ
l: label TX
input: option message
destination: state TX
output: option message
trX: list transition_item
IHtrX: pre_VLSM_projection_finite_trace_project TX TZ
  (mbind project_labelYZ ∘ project_labelXY)
  (project_stateYZ ∘ project_stateXY) trX =
pre_VLSM_projection_finite_trace_project TY TZ
  project_labelYZ project_stateYZ
  (pre_VLSM_projection_finite_trace_project TX
     TY project_labelXY project_stateXY trX)
match
  match
    match project_labelXY l with
    | Some x => project_labelYZ x
    | None => None
    end
  with
  | Some lY =>
      Some
        {|
          l := lY;
          input := input;
          destination :=
            project_stateYZ
              (project_stateXY destination);
          output := output
        |}
  | None => None
  end
with
| Some y =>
    y
    :: pre_VLSM_projection_finite_trace_project TX TZ
         ((λ mx : option (label TY),
             match mx with
             | Some x => project_labelYZ x
             | None => None
             end) ∘ project_labelXY)
         (project_stateYZ ∘ project_stateXY) trX
| None =>
    pre_VLSM_projection_finite_trace_project TX TZ
      ((λ mx : option (label TY),
          match mx with
          | Some x => project_labelYZ x
          | None => None
          end) ∘ project_labelXY)
      (project_stateYZ ∘ project_stateXY) trX
end =
pre_VLSM_projection_finite_trace_project TY TZ
  project_labelYZ project_stateYZ
  match
    match project_labelXY l with
    | Some lY =>
        Some
          {|
            l := lY;
            input := input;
            destination := project_stateXY destination;
            output := output
          |}
    | None => None
    end
  with
  | Some y =>
      y
      :: pre_VLSM_projection_finite_trace_project TX
           TY project_labelXY project_stateXY trX
  | None =>
      pre_VLSM_projection_finite_trace_project TX TY
        project_labelXY project_stateXY trX
  end
  destruct (project_labelXY l) as [lY |]; [| done]; cbn;
    unfold pre_VLSM_projection_transition_item_project; cbn.message: Type
TX, TY, TZ: VLSMType message
project_labelXY: label TX → option (label TY)
project_stateXY: state TX → state TY
project_labelYZ: label TY → option (label TZ)
project_stateYZ: state TY → state TZ
l: label TX
input: option message
destination: state TX
output: option message
trX: list transition_item
IHtrX: pre_VLSM_projection_finite_trace_project TX TZ
  (mbind project_labelYZ ∘ project_labelXY)
  (project_stateYZ ∘ project_stateXY) trX =
pre_VLSM_projection_finite_trace_project TY TZ
  project_labelYZ project_stateYZ
  (pre_VLSM_projection_finite_trace_project TX
     TY project_labelXY project_stateXY trX)
lY: label TY
match
  match project_labelYZ lY with
  | Some lY =>
      Some
        {|
          l := lY;
          input := input;
          destination :=
            project_stateYZ
              (project_stateXY destination);
          output := output
        |}
  | None => None
  end
with
| Some y =>
    y
    :: pre_VLSM_projection_finite_trace_project TX TZ
         ((λ mx : option (label TY),
             match mx with
             | Some x => project_labelYZ x
             | None => None
             end) ∘ project_labelXY)
         (project_stateYZ ∘ project_stateXY) trX
| None =>
    pre_VLSM_projection_finite_trace_project TX TZ
      ((λ mx : option (label TY),
          match mx with
          | Some x => project_labelYZ x
          | None => None
          end) ∘ project_labelXY)
      (project_stateYZ ∘ project_stateXY) trX
end =
match
  match project_labelYZ lY with
  | Some lY =>
      Some
        {|
          l := lY;
          input := input;
          destination :=
            project_stateYZ
              (project_stateXY destination);
          output := output
        |}
  | None => None
  end
with
| Some y =>
    y
    :: pre_VLSM_projection_finite_trace_project TY TZ
         project_labelYZ project_stateYZ
         (pre_VLSM_projection_finite_trace_project TX
            TY project_labelXY project_stateXY trX)
| None =>
    pre_VLSM_projection_finite_trace_project TY TZ
      project_labelYZ project_stateYZ
      (pre_VLSM_projection_finite_trace_project TX TY
         project_labelXY project_stateXY trX)
end
  destruct (project_labelYZ lY) as [lZ |]; [| done]; cbn.message: Type
TX, TY, TZ: VLSMType message
project_labelXY: label TX → option (label TY)
project_stateXY: state TX → state TY
project_labelYZ: label TY → option (label TZ)
project_stateYZ: state TY → state TZ
l: label TX
input: option message
destination: state TX
output: option message
trX: list transition_item
IHtrX: pre_VLSM_projection_finite_trace_project TX TZ
  (mbind project_labelYZ ∘ project_labelXY)
  (project_stateYZ ∘ project_stateXY) trX =
pre_VLSM_projection_finite_trace_project TY TZ
  project_labelYZ project_stateYZ
  (pre_VLSM_projection_finite_trace_project TX
     TY project_labelXY project_stateXY trX)
lY: label TY
lZ: label TZ
{|
  l := lZ;
  input := input;
  destination :=
    project_stateYZ (project_stateXY destination);
  output := output
|}
:: pre_VLSM_projection_finite_trace_project TX TZ
     ((λ mx : option (label TY),
         match mx with
         | Some x => project_labelYZ x
         | None => None
         end) ∘ project_labelXY)
     (project_stateYZ ∘ project_stateXY) trX =
{|
  l := lZ;
  input := input;
  destination :=
    project_stateYZ (project_stateXY destination);
  output := output
|}
:: pre_VLSM_projection_finite_trace_project TY TZ
     project_labelYZ project_stateYZ
     (pre_VLSM_projection_finite_trace_project TX TY
        project_labelXY project_stateXY trX)
  by f_equal.
Qed.

Lemma VLSM_projection_trans
  {message}
  (X Y Z : VLSM message)
  (project_labelXY : label X -> option (label Y))
  (project_stateXY : state X -> state Y)
  (ProjXY : VLSM_projection X Y project_labelXY project_stateXY)
  (project_labelYZ : label Y -> option (label Z))
  (project_stateYZ : state Y -> state Z)
  (ProjYZ : VLSM_projection Y Z project_labelYZ project_stateYZ)
  : VLSM_projection X Z
    (mbind project_labelYZ ∘ project_labelXY)
    (project_stateYZ ∘ project_stateXY).message: Type
X, Y, Z: VLSM message
project_labelXY: label X → option (label Y)
project_stateXY: state X → state Y
ProjXY: VLSM_projection X Y project_labelXY
  project_stateXY
project_labelYZ: label Y → option (label Z)
project_stateYZ: state Y → state Z
ProjYZ: VLSM_projection Y Z project_labelYZ
  project_stateYZ
VLSM_projection X Z
  (mbind project_labelYZ ∘ project_labelXY)
  (project_stateYZ ∘ project_stateXY)
Proof.message: Type
X, Y, Z: VLSM message
project_labelXY: label X → option (label Y)
project_stateXY: state X → state Y
ProjXY: VLSM_projection X Y project_labelXY
  project_stateXY
project_labelYZ: label Y → option (label Z)
project_stateYZ: state Y → state Z
ProjYZ: VLSM_projection Y Z project_labelYZ
  project_stateYZ
VLSM_projection X Z
  (mbind project_labelYZ ∘ project_labelXY)
  (project_stateYZ ∘ project_stateXY)
  constructor; [split |]; intros sX trX HtrX; cbn;
    setoid_rewrite pre_VLSM_projection_finite_trace_project_trans.message: Type
X, Y, Z: VLSM message
project_labelXY: label X → option (label Y)
project_stateXY: state X → state Y
ProjXY: VLSM_projection X Y project_labelXY
  project_stateXY
project_labelYZ: label Y → option (label Z)
project_stateYZ: state Y → state Z
ProjYZ: VLSM_projection Y Z project_labelYZ
  project_stateYZ
sX: state X
trX: list transition_item
HtrX: finite_valid_trace_from X sX trX
project_stateYZ
  (project_stateXY (finite_trace_last sX trX)) =
finite_trace_last
  (project_stateYZ (project_stateXY sX))
  (pre_VLSM_projection_finite_trace_project Y Z
     project_labelYZ project_stateYZ
     (pre_VLSM_projection_finite_trace_project X Y
        project_labelXY project_stateXY trX))
message: Type
X, Y, Z: VLSM message
project_labelXY: label X → option (label Y)
project_stateXY: state X → state Y
ProjXY: VLSM_projection X Y project_labelXY
  project_stateXY
project_labelYZ: label Y → option (label Z)
project_stateYZ: state Y → state Z
ProjYZ: VLSM_projection Y Z project_labelYZ
  project_stateYZ
sX: state X
trX: list transition_item
HtrX: finite_valid_trace X sX trX
finite_valid_trace Z
  (project_stateYZ (project_stateXY sX))
  (pre_VLSM_projection_finite_trace_project Y Z
     project_labelYZ project_stateYZ
     (pre_VLSM_projection_finite_trace_project X Y
        project_labelXY project_stateXY trX))
  -message: Type
X, Y, Z: VLSM message
project_labelXY: label X → option (label Y)
project_stateXY: state X → state Y
ProjXY: VLSM_projection X Y project_labelXY
  project_stateXY
project_labelYZ: label Y → option (label Z)
project_stateYZ: state Y → state Z
ProjYZ: VLSM_projection Y Z project_labelYZ
  project_stateYZ
sX: state X
trX: list transition_item
HtrX: finite_valid_trace_from X sX trX
project_stateYZ
  (project_stateXY (finite_trace_last sX trX)) =
finite_trace_last
  (project_stateYZ (project_stateXY sX))
  (pre_VLSM_projection_finite_trace_project Y Z
     project_labelYZ project_stateYZ
     (pre_VLSM_projection_finite_trace_project X Y
        project_labelXY project_stateXY trX)) rewrite <- !final_state_project; [done | apply ProjXY | done | apply ProjYZ |].message: Type
X, Y, Z: VLSM message
project_labelXY: label X → option (label Y)
project_stateXY: state X → state Y
ProjXY: VLSM_projection X Y project_labelXY
  project_stateXY
project_labelYZ: label Y → option (label Z)
project_stateYZ: state Y → state Z
ProjYZ: VLSM_projection Y Z project_labelYZ
  project_stateYZ
sX: state X
trX: list transition_item
HtrX: finite_valid_trace_from X sX trX
finite_valid_trace_from Y (project_stateXY sX)
  (pre_VLSM_projection_finite_trace_project X Y
     project_labelXY project_stateXY trX)
    by eapply (VLSM_projection_finite_valid_trace_from ProjXY).
  -message: Type
X, Y, Z: VLSM message
project_labelXY: label X → option (label Y)
project_stateXY: state X → state Y
ProjXY: VLSM_projection X Y project_labelXY
  project_stateXY
project_labelYZ: label Y → option (label Z)
project_stateYZ: state Y → state Z
ProjYZ: VLSM_projection Y Z project_labelYZ
  project_stateYZ
sX: state X
trX: list transition_item
HtrX: finite_valid_trace X sX trX
finite_valid_trace Z
  (project_stateYZ (project_stateXY sX))
  (pre_VLSM_projection_finite_trace_project Y Z
     project_labelYZ project_stateYZ
     (pre_VLSM_projection_finite_trace_project X Y
        project_labelXY project_stateXY trX)) by eapply (VLSM_projection_finite_valid_trace ProjYZ),
              (VLSM_projection_finite_valid_trace ProjXY).
Qed.

Lemma VLSM_projection_embedding_trans
  {message}
  (X Y Z : VLSM message)
  (project_labelXY : label X -> option (label Y))
  (project_stateXY : state X -> state Y)
  (ProjXY : VLSM_projection X Y project_labelXY project_stateXY)
  (project_labelYZ : label Y -> label Z)
  (project_stateYZ : state Y -> state Z)
  (ProjYZ : VLSM_embedding Y Z project_labelYZ project_stateYZ)
  : VLSM_projection X Z
    (fmap project_labelYZ ∘ project_labelXY)
    (project_stateYZ ∘ project_stateXY).message: Type
X, Y, Z: VLSM message
project_labelXY: label X → option (label Y)
project_stateXY: state X → state Y
ProjXY: VLSM_projection X Y project_labelXY
  project_stateXY
project_labelYZ: label Y → label Z
project_stateYZ: state Y → state Z
ProjYZ: VLSM_embedding Y Z project_labelYZ
  project_stateYZ
VLSM_projection X Z
  (fmap project_labelYZ ∘ project_labelXY)
  (project_stateYZ ∘ project_stateXY)
Proof.message: Type
X, Y, Z: VLSM message
project_labelXY: label X → option (label Y)
project_stateXY: state X → state Y
ProjXY: VLSM_projection X Y project_labelXY
  project_stateXY
project_labelYZ: label Y → label Z
project_stateYZ: state Y → state Z
ProjYZ: VLSM_embedding Y Z project_labelYZ
  project_stateYZ
VLSM_projection X Z
  (fmap project_labelYZ ∘ project_labelXY)
  (project_stateYZ ∘ project_stateXY)
  apply VLSM_embedding_is_projection in ProjYZ.message: Type
X, Y, Z: VLSM message
project_labelXY: label X → option (label Y)
project_stateXY: state X → state Y
ProjXY: VLSM_projection X Y project_labelXY
  project_stateXY
project_labelYZ: label Y → label Z
project_stateYZ: state Y → state Z
ProjYZ: VLSM_projection Y Z (Some ∘ project_labelYZ)
  project_stateYZ
VLSM_projection X Z
  (fmap project_labelYZ ∘ project_labelXY)
  (project_stateYZ ∘ project_stateXY)
  replace (fmap project_labelYZ ∘ project_labelXY)
     with (mbind (Some ∘ project_labelYZ) ∘ project_labelXY).message: Type
X, Y, Z: VLSM message
project_labelXY: label X → option (label Y)
project_stateXY: state X → state Y
ProjXY: VLSM_projection X Y project_labelXY
  project_stateXY
project_labelYZ: label Y → label Z
project_stateYZ: state Y → state Z
ProjYZ: VLSM_projection Y Z (Some ∘ project_labelYZ)
  project_stateYZ
VLSM_projection X Z
  (mbind (Some ∘ project_labelYZ) ∘ project_labelXY)
  (project_stateYZ ∘ project_stateXY)
message: Type
X, Y, Z: VLSM message
project_labelXY: label X → option (label Y)
project_stateXY: state X → state Y
ProjXY: VLSM_projection X Y project_labelXY
  project_stateXY
project_labelYZ: label Y → label Z
project_stateYZ: state Y → state Z
ProjYZ: VLSM_projection Y Z (Some ∘ project_labelYZ)
  project_stateYZ
mbind (Some ∘ project_labelYZ) ∘ project_labelXY =
fmap project_labelYZ ∘ project_labelXY
  -message: Type
X, Y, Z: VLSM message
project_labelXY: label X → option (label Y)
project_stateXY: state X → state Y
ProjXY: VLSM_projection X Y project_labelXY
  project_stateXY
project_labelYZ: label Y → label Z
project_stateYZ: state Y → state Z
ProjYZ: VLSM_projection Y Z (Some ∘ project_labelYZ)
  project_stateYZ
VLSM_projection X Z
  (mbind (Some ∘ project_labelYZ) ∘ project_labelXY)
  (project_stateYZ ∘ project_stateXY) by apply VLSM_projection_trans.
  -message: Type
X, Y, Z: VLSM message
project_labelXY: label X → option (label Y)
project_stateXY: state X → state Y
ProjXY: VLSM_projection X Y project_labelXY
  project_stateXY
project_labelYZ: label Y → label Z
project_stateYZ: state Y → state Z
ProjYZ: VLSM_projection Y Z (Some ∘ project_labelYZ)
  project_stateYZ
mbind (Some ∘ project_labelYZ) ∘ project_labelXY =
fmap project_labelYZ ∘ project_labelXY by extensionality x.
Qed.

Lemma VLSM_embedding_projection_trans
  {message}
  (X Y Z : VLSM message)
  (project_labelXY : label X -> label Y)
  (project_stateXY : state X -> state Y)
  (ProjXY : VLSM_embedding X Y project_labelXY project_stateXY)
  (project_labelYZ : label Y -> option (label Z))
  (project_stateYZ : state Y -> state Z)
  (ProjYZ : VLSM_projection Y Z project_labelYZ project_stateYZ)
  : VLSM_projection X Z
    (project_labelYZ ∘ project_labelXY)
    (project_stateYZ ∘ project_stateXY).message: Type
X, Y, Z: VLSM message
project_labelXY: label X → label Y
project_stateXY: state X → state Y
ProjXY: VLSM_embedding X Y project_labelXY
  project_stateXY
project_labelYZ: label Y → option (label Z)
project_stateYZ: state Y → state Z
ProjYZ: VLSM_projection Y Z project_labelYZ
  project_stateYZ
VLSM_projection X Z
  (project_labelYZ ∘ project_labelXY)
  (project_stateYZ ∘ project_stateXY)
Proof.message: Type
X, Y, Z: VLSM message
project_labelXY: label X → label Y
project_stateXY: state X → state Y
ProjXY: VLSM_embedding X Y project_labelXY
  project_stateXY
project_labelYZ: label Y → option (label Z)
project_stateYZ: state Y → state Z
ProjYZ: VLSM_projection Y Z project_labelYZ
  project_stateYZ
VLSM_projection X Z
  (project_labelYZ ∘ project_labelXY)
  (project_stateYZ ∘ project_stateXY)
  apply VLSM_embedding_is_projection in ProjXY.message: Type
X, Y, Z: VLSM message
project_labelXY: label X → label Y
project_stateXY: state X → state Y
ProjXY: VLSM_projection X Y (Some ∘ project_labelXY)
  project_stateXY
project_labelYZ: label Y → option (label Z)
project_stateYZ: state Y → state Z
ProjYZ: VLSM_projection Y Z project_labelYZ
  project_stateYZ
VLSM_projection X Z
  (project_labelYZ ∘ project_labelXY)
  (project_stateYZ ∘ project_stateXY)
  replace (project_labelYZ ∘ project_labelXY)
     with (mbind project_labelYZ ∘ (Some ∘ project_labelXY)).message: Type
X, Y, Z: VLSM message
project_labelXY: label X → label Y
project_stateXY: state X → state Y
ProjXY: VLSM_projection X Y (Some ∘ project_labelXY)
  project_stateXY
project_labelYZ: label Y → option (label Z)
project_stateYZ: state Y → state Z
ProjYZ: VLSM_projection Y Z project_labelYZ
  project_stateYZ
VLSM_projection X Z
  (mbind project_labelYZ ∘ (Some ∘ project_labelXY))
  (project_stateYZ ∘ project_stateXY)
message: Type
X, Y, Z: VLSM message
project_labelXY: label X → label Y
project_stateXY: state X → state Y
ProjXY: VLSM_projection X Y (Some ∘ project_labelXY)
  project_stateXY
project_labelYZ: label Y → option (label Z)
project_stateYZ: state Y → state Z
ProjYZ: VLSM_projection Y Z project_labelYZ
  project_stateYZ
mbind project_labelYZ ∘ (Some ∘ project_labelXY) =
project_labelYZ ∘ project_labelXY
  -message: Type
X, Y, Z: VLSM message
project_labelXY: label X → label Y
project_stateXY: state X → state Y
ProjXY: VLSM_projection X Y (Some ∘ project_labelXY)
  project_stateXY
project_labelYZ: label Y → option (label Z)
project_stateYZ: state Y → state Z
ProjYZ: VLSM_projection Y Z project_labelYZ
  project_stateYZ
VLSM_projection X Z
  (mbind project_labelYZ ∘ (Some ∘ project_labelXY))
  (project_stateYZ ∘ project_stateXY) by apply VLSM_projection_trans.
  -message: Type
X, Y, Z: VLSM message
project_labelXY: label X → label Y
project_stateXY: state X → state Y
ProjXY: VLSM_projection X Y (Some ∘ project_labelXY)
  project_stateXY
project_labelYZ: label Y → option (label Z)
project_stateYZ: state Y → state Z
ProjYZ: VLSM_projection Y Z project_labelYZ
  project_stateYZ
mbind project_labelYZ ∘ (Some ∘ project_labelXY) =
project_labelYZ ∘ project_labelXY by extensionality x.
Qed.

Lemma pre_VLSM_embedding_finite_trace_project_trans
  {message}
  (TX TY TZ : VLSMType message)
  (project_labelXY : label TX -> label TY)
  (project_stateXY : state TX -> state TY)
  (project_labelYZ : label TY -> label TZ)
  (project_stateYZ : state TY -> state TZ)
  : forall trX,
    pre_VLSM_embedding_finite_trace_project TX TZ
      (project_labelYZ ∘ project_labelXY)
      (project_stateYZ ∘ project_stateXY)
      trX
      =
    pre_VLSM_embedding_finite_trace_project  TY TZ project_labelYZ project_stateYZ
      (pre_VLSM_embedding_finite_trace_project  TX TY project_labelXY project_stateXY
        trX).message: Type
TX, TY, TZ: VLSMType message
project_labelXY: label TX → label TY
project_stateXY: state TX → state TY
project_labelYZ: label TY → label TZ
project_stateYZ: state TY → state TZ
∀ trX : list transition_item,
  pre_VLSM_embedding_finite_trace_project TX TZ
    (project_labelYZ ∘ project_labelXY)
    (project_stateYZ ∘ project_stateXY) trX =
  pre_VLSM_embedding_finite_trace_project TY TZ
    project_labelYZ project_stateYZ
    (pre_VLSM_embedding_finite_trace_project TX TY
       project_labelXY project_stateXY trX)
Proof.message: Type
TX, TY, TZ: VLSMType message
project_labelXY: label TX → label TY
project_stateXY: state TX → state TY
project_labelYZ: label TY → label TZ
project_stateYZ: state TY → state TZ
∀ trX : list transition_item,
  pre_VLSM_embedding_finite_trace_project TX TZ
    (project_labelYZ ∘ project_labelXY)
    (project_stateYZ ∘ project_stateXY) trX =
  pre_VLSM_embedding_finite_trace_project TY TZ
    project_labelYZ project_stateYZ
    (pre_VLSM_embedding_finite_trace_project TX TY
       project_labelXY project_stateXY trX) by induction trX; [| destruct a; cbn; f_equal]. Qed.

Lemma VLSM_embedding_trans
  {message}
  (X Y Z : VLSM message)
  (project_labelXY : label X -> label Y)
  (project_stateXY : state X -> state Y)
  (ProjXY : VLSM_embedding X Y project_labelXY project_stateXY)
  (project_labelYZ : label Y -> label Z)
  (project_stateYZ : state Y -> state Z)
  (ProjYZ : VLSM_embedding Y Z project_labelYZ project_stateYZ)
  : VLSM_embedding X Z
    (project_labelYZ ∘ project_labelXY)
    (project_stateYZ ∘ project_stateXY).message: Type
X, Y, Z: VLSM message
project_labelXY: label X → label Y
project_stateXY: state X → state Y
ProjXY: VLSM_embedding X Y project_labelXY
  project_stateXY
project_labelYZ: label Y → label Z
project_stateYZ: state Y → state Z
ProjYZ: VLSM_embedding Y Z project_labelYZ
  project_stateYZ
VLSM_embedding X Z (project_labelYZ ∘ project_labelXY)
  (project_stateYZ ∘ project_stateXY)
Proof.message: Type
X, Y, Z: VLSM message
project_labelXY: label X → label Y
project_stateXY: state X → state Y
ProjXY: VLSM_embedding X Y project_labelXY
  project_stateXY
project_labelYZ: label Y → label Z
project_stateYZ: state Y → state Z
ProjYZ: VLSM_embedding Y Z project_labelYZ
  project_stateYZ
VLSM_embedding X Z (project_labelYZ ∘ project_labelXY)
  (project_stateYZ ∘ project_stateXY)
  constructor; intros sX trX HtrX.message: Type
X, Y, Z: VLSM message
project_labelXY: label X → label Y
project_stateXY: state X → state Y
ProjXY: VLSM_embedding X Y project_labelXY
  project_stateXY
project_labelYZ: label Y → label Z
project_stateYZ: state Y → state Z
ProjYZ: VLSM_embedding Y Z project_labelYZ
  project_stateYZ
sX: state X
trX: list transition_item
HtrX: finite_valid_trace X sX trX
finite_valid_trace Z
  ((project_stateYZ ∘ project_stateXY) sX)
  (pre_VLSM_embedding_finite_trace_project X Z
     (project_labelYZ ∘ project_labelXY)
     (project_stateYZ ∘ project_stateXY) trX)
  setoid_rewrite pre_VLSM_embedding_finite_trace_project_trans.message: Type
X, Y, Z: VLSM message
project_labelXY: label X → label Y
project_stateXY: state X → state Y
ProjXY: VLSM_embedding X Y project_labelXY
  project_stateXY
project_labelYZ: label Y → label Z
project_stateYZ: state Y → state Z
ProjYZ: VLSM_embedding Y Z project_labelYZ
  project_stateYZ
sX: state X
trX: list transition_item
HtrX: finite_valid_trace X sX trX
finite_valid_trace Z
  ((project_stateYZ ∘ project_stateXY) sX)
  (pre_VLSM_embedding_finite_trace_project Y Z
     project_labelYZ project_stateYZ
     (pre_VLSM_embedding_finite_trace_project X Y
        project_labelXY project_stateXY trX))
  by eapply (VLSM_embedding_finite_valid_trace ProjYZ),
            (VLSM_embedding_finite_valid_trace ProjXY).
Qed.

Lemma VLSM_projection_incl_trans
  {message}
  (X : VLSM message)
  {T : VLSMType message}
  {MY MZ : VLSMMachine T}
  (Y := mk_vlsm MY)
  (Z := mk_vlsm MZ)
  (project_labelXY : label X -> option (label Y))
  (project_stateXY : state X -> state Y)
  (ProjXY : VLSM_projection X Y project_labelXY project_stateXY)
  (ProjYZ : VLSM_incl Y Z)
  : VLSM_projection X Z project_labelXY project_stateXY.message: Type
X: VLSM message
T: VLSMType message
MY, MZ: VLSMMachine T
Y:= {| vlsm_type := T; vlsm_machine := MY |}: VLSM message
Z:= {| vlsm_type := T; vlsm_machine := MZ |}: VLSM message
project_labelXY: label X → option (label Y)
project_stateXY: state X → state Y
ProjXY: VLSM_projection X Y project_labelXY
  project_stateXY
ProjYZ: VLSM_incl Y Z
VLSM_projection X Z project_labelXY project_stateXY
Proof.message: Type
X: VLSM message
T: VLSMType message
MY, MZ: VLSMMachine T
Y:= {| vlsm_type := T; vlsm_machine := MY |}: VLSM message
Z:= {| vlsm_type := T; vlsm_machine := MZ |}: VLSM message
project_labelXY: label X → option (label Y)
project_stateXY: state X → state Y
ProjXY: VLSM_projection X Y project_labelXY
  project_stateXY
ProjYZ: VLSM_incl Y Z
VLSM_projection X Z project_labelXY project_stateXY
  replace project_labelXY with (fmap id ∘ project_labelXY)
    by (extensionality lX; cbv; destruct (project_labelXY lX); done).message: Type
X: VLSM message
T: VLSMType message
MY, MZ: VLSMMachine T
Y:= {| vlsm_type := T; vlsm_machine := MY |}: VLSM message
Z:= {| vlsm_type := T; vlsm_machine := MZ |}: VLSM message
project_labelXY: label X → option (label Y)
project_stateXY: state X → state Y
ProjXY: VLSM_projection X Y project_labelXY
  project_stateXY
ProjYZ: VLSM_incl Y Z
VLSM_projection X Z (fmap id ∘ project_labelXY)
  project_stateXY
  change project_stateXY with (id ∘ project_stateXY).message: Type
X: VLSM message
T: VLSMType message
MY, MZ: VLSMMachine T
Y:= {| vlsm_type := T; vlsm_machine := MY |}: VLSM message
Z:= {| vlsm_type := T; vlsm_machine := MZ |}: VLSM message
project_labelXY: label X → option (label Y)
project_stateXY: state X → state Y
ProjXY: VLSM_projection X Y project_labelXY
  project_stateXY
ProjYZ: VLSM_incl Y Z
VLSM_projection X Z (fmap id ∘ project_labelXY)
  (id ∘ project_stateXY)
  by apply (VLSM_projection_embedding_trans X Y Z); [| apply VLSM_incl_is_embedding].
Qed.

Lemma VLSM_embedding_incl_trans
  {message}
  (X : VLSM message)
  {T : VLSMType message}
  {MY MZ : VLSMMachine T}
  (Y := mk_vlsm MY)
  (Z := mk_vlsm MZ)
  (project_labelXY : label X -> label Y)
  (project_stateXY : state X -> state Y)
  (ProjXY : VLSM_embedding X Y project_labelXY project_stateXY)
  (ProjYZ : VLSM_incl Y Z)
  : VLSM_embedding X Z project_labelXY project_stateXY.message: Type
X: VLSM message
T: VLSMType message
MY, MZ: VLSMMachine T
Y:= {| vlsm_type := T; vlsm_machine := MY |}: VLSM message
Z:= {| vlsm_type := T; vlsm_machine := MZ |}: VLSM message
project_labelXY: label X → label Y
project_stateXY: state X → state Y
ProjXY: VLSM_embedding X Y project_labelXY
  project_stateXY
ProjYZ: VLSM_incl Y Z
VLSM_embedding X Z project_labelXY project_stateXY
Proof.message: Type
X: VLSM message
T: VLSMType message
MY, MZ: VLSMMachine T
Y:= {| vlsm_type := T; vlsm_machine := MY |}: VLSM message
Z:= {| vlsm_type := T; vlsm_machine := MZ |}: VLSM message
project_labelXY: label X → label Y
project_stateXY: state X → state Y
ProjXY: VLSM_embedding X Y project_labelXY
  project_stateXY
ProjYZ: VLSM_incl Y Z
VLSM_embedding X Z project_labelXY project_stateXY
  change project_labelXY with (id ∘ project_labelXY).message: Type
X: VLSM message
T: VLSMType message
MY, MZ: VLSMMachine T
Y:= {| vlsm_type := T; vlsm_machine := MY |}: VLSM message
Z:= {| vlsm_type := T; vlsm_machine := MZ |}: VLSM message
project_labelXY: label X → label Y
project_stateXY: state X → state Y
ProjXY: VLSM_embedding X Y project_labelXY
  project_stateXY
ProjYZ: VLSM_incl Y Z
VLSM_embedding X Z (id ∘ project_labelXY)
  project_stateXY
  change project_stateXY with (id ∘ project_stateXY).message: Type
X: VLSM message
T: VLSMType message
MY, MZ: VLSMMachine T
Y:= {| vlsm_type := T; vlsm_machine := MY |}: VLSM message
Z:= {| vlsm_type := T; vlsm_machine := MZ |}: VLSM message
project_labelXY: label X → label Y
project_stateXY: state X → state Y
ProjXY: VLSM_embedding X Y project_labelXY
  project_stateXY
ProjYZ: VLSM_incl Y Z
VLSM_embedding X Z (id ∘ project_labelXY)
  (id ∘ project_stateXY)
  by apply (VLSM_embedding_trans X Y Z); [| apply VLSM_incl_is_embedding].
Qed.

Lemma VLSM_incl_projection_trans
  {message}
  {T : VLSMType message}
  {MX MY : VLSMMachine T}
  (X := mk_vlsm MX)
  (Y := mk_vlsm MY)
  (Z : VLSM message)
  (ProjXY : VLSM_incl X Y)
  (project_labelYZ : label Y -> option (label Z))
  (project_stateYZ : state Y -> state Z)
  (ProjYZ : VLSM_projection Y Z project_labelYZ project_stateYZ)
  : VLSM_projection X Z project_labelYZ project_stateYZ.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
Z: VLSM message
ProjXY: VLSM_incl X Y
project_labelYZ: label Y → option (label Z)
project_stateYZ: state Y → state Z
ProjYZ: VLSM_projection Y Z project_labelYZ
  project_stateYZ
VLSM_projection X Z project_labelYZ project_stateYZ
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
Z: VLSM message
ProjXY: VLSM_incl X Y
project_labelYZ: label Y → option (label Z)
project_stateYZ: state Y → state Z
ProjYZ: VLSM_projection Y Z project_labelYZ
  project_stateYZ
VLSM_projection X Z project_labelYZ project_stateYZ
  apply (VLSM_embedding_projection_trans X Y Z); [| 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
Z: VLSM message
ProjXY: VLSM_incl X Y
project_labelYZ: label Y → option (label Z)
project_stateYZ: state Y → state Z
ProjYZ: VLSM_projection Y Z project_labelYZ
  project_stateYZ
VLSM_embedding X Y (λ x : label X, x)
  (λ x : state X, x)
  by apply VLSM_incl_is_embedding in ProjXY.
Qed.

Lemma VLSM_incl_embedding_trans
  {message}
  {T : VLSMType message}
  {MX MY : VLSMMachine T}
  (X := mk_vlsm MX)
  (Y := mk_vlsm MY)
  (Z : VLSM message)
  (ProjXY : VLSM_incl X Y)
  (project_labelYZ : label Y -> label Z)
  (project_stateYZ : state Y -> state Z)
  (ProjYZ : VLSM_embedding Y Z project_labelYZ project_stateYZ)
  : VLSM_embedding X Z project_labelYZ project_stateYZ.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
Z: VLSM message
ProjXY: VLSM_incl X Y
project_labelYZ: label Y → label Z
project_stateYZ: state Y → state Z
ProjYZ: VLSM_embedding Y Z project_labelYZ
  project_stateYZ
VLSM_embedding X Z project_labelYZ project_stateYZ
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
Z: VLSM message
ProjXY: VLSM_incl X Y
project_labelYZ: label Y → label Z
project_stateYZ: state Y → state Z
ProjYZ: VLSM_embedding Y Z project_labelYZ
  project_stateYZ
VLSM_embedding X Z project_labelYZ project_stateYZ
  apply (VLSM_embedding_trans X Y Z); [| 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
Z: VLSM message
ProjXY: VLSM_incl X Y
project_labelYZ: label Y → label Z
project_stateYZ: state Y → state Z
ProjYZ: VLSM_embedding Y Z project_labelYZ
  project_stateYZ
VLSM_embedding X Y (λ x : label X, x)
  (λ x : state X, x)
  by apply VLSM_incl_is_embedding in ProjXY.
Qed.

Lemma VLSM_projection_eq_trans
  {message}
  (X : VLSM message)
  {T : VLSMType message}
  {MY MZ : VLSMMachine T}
  (Y := mk_vlsm MY)
  (Z := mk_vlsm MZ)
  (project_labelXY : label X -> option (label Y))
  (project_stateXY : state X -> state Y)
  (ProjXY : VLSM_projection X Y project_labelXY project_stateXY)
  (ProjYZ : VLSM_eq Y Z)
  : VLSM_projection X Z project_labelXY project_stateXY.message: Type
X: VLSM message
T: VLSMType message
MY, MZ: VLSMMachine T
Y:= {| vlsm_type := T; vlsm_machine := MY |}: VLSM message
Z:= {| vlsm_type := T; vlsm_machine := MZ |}: VLSM message
project_labelXY: label X → option (label Y)
project_stateXY: state X → state Y
ProjXY: VLSM_projection X Y project_labelXY
  project_stateXY
ProjYZ: VLSM_eq Y Z
VLSM_projection X Z project_labelXY project_stateXY
Proof.message: Type
X: VLSM message
T: VLSMType message
MY, MZ: VLSMMachine T
Y:= {| vlsm_type := T; vlsm_machine := MY |}: VLSM message
Z:= {| vlsm_type := T; vlsm_machine := MZ |}: VLSM message
project_labelXY: label X → option (label Y)
project_stateXY: state X → state Y
ProjXY: VLSM_projection X Y project_labelXY
  project_stateXY
ProjYZ: VLSM_eq Y Z
VLSM_projection X Z project_labelXY project_stateXY by apply VLSM_projection_incl_trans; [| apply ProjYZ]. Qed.

Lemma VLSM_embedding_eq_trans
  {message}
  (X : VLSM message)
  {T : VLSMType message}
  {MY MZ : VLSMMachine T}
  (Y := mk_vlsm MY)
  (Z := mk_vlsm MZ)
  (project_labelXY : label X -> label Y)
  (project_stateXY : state X -> state Y)
  (ProjXY : VLSM_embedding X Y project_labelXY project_stateXY)
  (ProjYZ : VLSM_eq Y Z)
  : VLSM_embedding X Z project_labelXY project_stateXY.message: Type
X: VLSM message
T: VLSMType message
MY, MZ: VLSMMachine T
Y:= {| vlsm_type := T; vlsm_machine := MY |}: VLSM message
Z:= {| vlsm_type := T; vlsm_machine := MZ |}: VLSM message
project_labelXY: label X → label Y
project_stateXY: state X → state Y
ProjXY: VLSM_embedding X Y project_labelXY
  project_stateXY
ProjYZ: VLSM_eq Y Z
VLSM_embedding X Z project_labelXY project_stateXY
Proof.message: Type
X: VLSM message
T: VLSMType message
MY, MZ: VLSMMachine T
Y:= {| vlsm_type := T; vlsm_machine := MY |}: VLSM message
Z:= {| vlsm_type := T; vlsm_machine := MZ |}: VLSM message
project_labelXY: label X → label Y
project_stateXY: state X → state Y
ProjXY: VLSM_embedding X Y project_labelXY
  project_stateXY
ProjYZ: VLSM_eq Y Z
VLSM_embedding X Z project_labelXY project_stateXY by apply VLSM_embedding_incl_trans; [| apply ProjYZ]. Qed.

Lemma VLSM_eq_projection_trans
  {message}
  {T : VLSMType message}
  {MX MY : VLSMMachine T}
  (X := mk_vlsm MX)
  (Y := mk_vlsm MY)
  (Z : VLSM message)
  (ProjXY : VLSM_eq X Y)
  (project_labelYZ : label Y -> option (label Z))
  (project_stateYZ : state Y -> state Z)
  (ProjYZ : VLSM_projection Y Z project_labelYZ project_stateYZ)
  : VLSM_projection X Z project_labelYZ project_stateYZ.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
Z: VLSM message
ProjXY: VLSM_eq X Y
project_labelYZ: label Y → option (label Z)
project_stateYZ: state Y → state Z
ProjYZ: VLSM_projection Y Z project_labelYZ
  project_stateYZ
VLSM_projection X Z project_labelYZ project_stateYZ
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
Z: VLSM message
ProjXY: VLSM_eq X Y
project_labelYZ: label Y → option (label Z)
project_stateYZ: state Y → state Z
ProjYZ: VLSM_projection Y Z project_labelYZ
  project_stateYZ
VLSM_projection X Z project_labelYZ project_stateYZ by apply VLSM_incl_projection_trans; [apply ProjXY |]. Qed.

Lemma VLSM_eq_embedding_trans
  {message}
  {T : VLSMType message}
  {MX MY : VLSMMachine T}
  (X := mk_vlsm MX)
  (Y := mk_vlsm MY)
  (Z : VLSM message)
  (ProjXY : VLSM_eq X Y)
  (project_labelYZ : label Y -> label Z)
  (project_stateYZ : state Y -> state Z)
  (ProjYZ : VLSM_embedding Y Z project_labelYZ project_stateYZ)
  : VLSM_embedding X Z project_labelYZ project_stateYZ.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
Z: VLSM message
ProjXY: VLSM_eq X Y
project_labelYZ: label Y → label Z
project_stateYZ: state Y → state Z
ProjYZ: VLSM_embedding Y Z project_labelYZ
  project_stateYZ
VLSM_embedding X Z project_labelYZ project_stateYZ
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
Z: VLSM message
ProjXY: VLSM_eq X Y
project_labelYZ: label Y → label Z
project_stateYZ: state Y → state Z
ProjYZ: VLSM_embedding Y Z project_labelYZ
  project_stateYZ
VLSM_embedding X Z project_labelYZ project_stateYZ by apply VLSM_incl_embedding_trans; [apply ProjXY |]. Qed.

End sec_transitivity_props.