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.Lib Require Import Preamble.
From VLSM.Core Require Import VLSM.

Core: VLSM Partial Projections

A generic notion of VLSM projection. We say that VLSM X partially projects to VLSM Y (sharing the same messages) if there exists a partial map partial_trace_project from traces over X (pairs of state and list of transitions from that state) to traces over Y such that:

partial_trace_project_preserves_valid_traces, if the projection is defined.
The projection operation is stable to adding valid prefixes (property

partial_trace_project_extends_left). More precisely, if the projection of a trace (sX, tX) yields (sY, tY), then for any trace (s'X, preX) ending in sX such that (s'X, preX ++ tX) is a valid trace, then there exists a trace (s'Y, preY) ending in sY such that (s'X, preX ++ tX) projects to (s'Y, preY ++ tY).

Proper examples of partial projections (which are not VLSM_projections) are the projections from the compositions of equivocators to the composition of regular components guided by a specific start MachineDescriptor (see, e.g., equivocators_no_equivocations_vlsm_X_vlsm_partial_projection).

Section sec_VLSM_partial_projection.

Record VLSM_partial_projection_type
  {message : Type}
  (X Y : VLSM message)
  (partial_trace_project :
    state X * list (transition_item X) -> option (state Y * list (transition_item Y)))
  : Prop :=
{
  partial_trace_project_extends_left :
    forall sX trX sY trY,
    partial_trace_project (sX, trX) = Some (sY, trY) ->
    forall s'X preX,
      finite_trace_last s'X preX = sX ->
      finite_valid_trace_from X s'X (preX ++ trX) ->
      exists s'Y preY,
        partial_trace_project (s'X, preX ++ trX) = Some (s'Y, preY ++ trY) /\
        finite_trace_last s'Y preY = sY;
}.

We define two kinds of partial projection: VLSM_weak_partial_projection and VLSM_partial_projection, the main difference between them being that the "weak" one is not required to preserve initial states.

Although there are no current examples of proper VLSM_weak_partial_projections, their definition serves as a support base for VLSM_weak_projections.

Record VLSM_weak_partial_projection
  {message : Type}
  (X Y : VLSM message)
  (partial_trace_project :
    state X * list (transition_item X) -> option (state Y * list (transition_item Y)))
  : Prop :=
{
  weak_partial_projection_type :> VLSM_partial_projection_type X Y partial_trace_project;
  weak_partial_trace_project_preserves_valid_trace :
    forall sX trX sY trY,
      partial_trace_project (sX, trX) = Some (sY, trY) ->
      finite_valid_trace_from X sX trX -> finite_valid_trace_from Y sY trY;
}.

Record VLSM_partial_projection
  {message : Type}
  (X Y : VLSM message)
  (partial_trace_project :
    state X * list (transition_item X) -> option (state Y * list (transition_item Y)))
  : Prop :=
{
  partial_projection_type :> VLSM_partial_projection_type X Y partial_trace_project;
  partial_trace_project_preserves_valid_trace :
    forall sX trX sY trY,
      partial_trace_project (sX, trX) = Some (sY, trY) ->
      finite_valid_trace X sX trX -> finite_valid_trace Y sY trY;
}.

Section sec_weak_partial_projection_properties.

Weak partial projection properties

Context
  {message : Type}
  {X Y : VLSM message}
  {trace_project :
    state X * list (transition_item X) -> option (state Y * list (transition_item Y))}
  (Hsimul : VLSM_weak_partial_projection X Y trace_project)
  .

Lemma VLSM_weak_partial_projection_finite_valid_trace_from :
  forall sX trX sY trY,
    trace_project (sX, trX) = Some (sY, trY) ->
    finite_valid_trace_from X sX trX -> finite_valid_trace_from Y sY trY.message: Type
X, Y: VLSM message
trace_project: state X * list transition_item
→ option
    (state Y * list transition_item)
Hsimul: VLSM_weak_partial_projection X Y
  trace_project
∀ (sX : state X) (trX : list transition_item) (sY : 
                                               state Y) 
  (trY : list transition_item),
  trace_project (sX, trX) = Some (sY, trY)
  → finite_valid_trace_from X sX trX
    → finite_valid_trace_from Y sY trY
Proof.message: Type
X, Y: VLSM message
trace_project: state X * list transition_item
→ option
    (state Y * list transition_item)
Hsimul: VLSM_weak_partial_projection X Y
  trace_project
∀ (sX : state X) (trX : list transition_item) (sY : 
                                               state Y) 
  (trY : list transition_item),
  trace_project (sX, trX) = Some (sY, trY)
  → finite_valid_trace_from X sX trX
    → finite_valid_trace_from Y sY trY
  exact (weak_partial_trace_project_preserves_valid_trace _ _ _ Hsimul).
Qed.

Lemma VLSM_weak_partial_projection_valid_state
  : forall sX sY trY,
    trace_project (sX, []) = Some (sY, trY) ->
    valid_state_prop X sX -> valid_state_prop Y sY.message: Type
X, Y: VLSM message
trace_project: state X * list transition_item
→ option
    (state Y * list transition_item)
Hsimul: VLSM_weak_partial_projection X Y
  trace_project
∀ (sX : state X) (sY : state Y) (trY : list
                                         transition_item),
  trace_project (sX, []) = Some (sY, trY)
  → valid_state_prop X sX → valid_state_prop Y sY
Proof.message: Type
X, Y: VLSM message
trace_project: state X * list transition_item
→ option
    (state Y * list transition_item)
Hsimul: VLSM_weak_partial_projection X Y
  trace_project
∀ (sX : state X) (sY : state Y) (trY : list
                                         transition_item),
  trace_project (sX, []) = Some (sY, trY)
  → valid_state_prop X sX → valid_state_prop Y sY
  intros sX sY trY Hpr HsX.message: Type
X, Y: VLSM message
trace_project: state X * list transition_item
→ option
    (state Y * list transition_item)
Hsimul: VLSM_weak_partial_projection X Y
  trace_project
sX: state X
sY: state Y
trY: list transition_item
Hpr: trace_project (sX, []) = Some (sY, trY)
HsX: valid_state_prop X sX
valid_state_prop Y sY
  apply valid_state_has_trace in HsX.message: Type
X, Y: VLSM message
trace_project: state X * list transition_item
→ option
    (state Y * list transition_item)
Hsimul: VLSM_weak_partial_projection X Y
  trace_project
sX: state X
sY: state Y
trY: list transition_item
Hpr: trace_project (sX, []) = Some (sY, trY)
HsX: ∃ (is : state X) (tr : list transition_item),
  finite_valid_trace_init_to X is sX tr
valid_state_prop Y sY
  destruct HsX as [isX [trX HtrX]].message: Type
X, Y: VLSM message
trace_project: state X * list transition_item
→ option
    (state Y * list transition_item)
Hsimul: VLSM_weak_partial_projection X Y
  trace_project
sX: state X
sY: state Y
trY: list transition_item
Hpr: trace_project (sX, []) = Some (sY, trY)
isX: state X
trX: list transition_item
HtrX: finite_valid_trace_init_to X isX sX trX
valid_state_prop Y sY
  apply finite_valid_trace_init_to_last in HtrX as HsX.message: Type
X, Y: VLSM message
trace_project: state X * list transition_item
→ option
    (state Y * list transition_item)
Hsimul: VLSM_weak_partial_projection X Y
  trace_project
sX: state X
sY: state Y
trY: list transition_item
Hpr: trace_project (sX, []) = Some (sY, trY)
isX: state X
trX: list transition_item
HtrX: finite_valid_trace_init_to X isX sX trX
HsX: finite_trace_last isX trX = sX
valid_state_prop Y sY
  apply finite_valid_trace_init_to_forget_last, proj1 in HtrX.message: Type
X, Y: VLSM message
trace_project: state X * list transition_item
→ option
    (state Y * list transition_item)
Hsimul: VLSM_weak_partial_projection X Y
  trace_project
sX: state X
sY: state Y
trY: list transition_item
Hpr: trace_project (sX, []) = Some (sY, trY)
isX: state X
trX: list transition_item
HtrX: finite_valid_trace_from X isX trX
HsX: finite_trace_last isX trX = sX
valid_state_prop Y sY
  specialize (partial_trace_project_extends_left _ _ _ Hsimul _ _ _ _ Hpr _ _ HsX)
    as Hpr_extends_left.message: Type
X, Y: VLSM message
trace_project: state X * list transition_item
→ option
    (state Y * list transition_item)
Hsimul: VLSM_weak_partial_projection X Y
  trace_project
sX: state X
sY: state Y
trY: list transition_item
Hpr: trace_project (sX, []) = Some (sY, trY)
isX: state X
trX: list transition_item
HtrX: finite_valid_trace_from X isX trX
HsX: finite_trace_last isX trX = sX
Hpr_extends_left: finite_valid_trace_from X isX
  (trX ++ [])
→ ∃ (s'Y : state Y) (preY : 
                     list
                      transition_item),
    trace_project (isX, trX ++ []) =
    Some (s'Y, preY ++ trY)
    ∧ finite_trace_last s'Y preY =
      sY
valid_state_prop Y sY
  spec Hpr_extends_left; [by rewrite app_nil_r |].message: Type
X, Y: VLSM message
trace_project: state X * list transition_item
→ option
    (state Y * list transition_item)
Hsimul: VLSM_weak_partial_projection X Y
  trace_project
sX: state X
sY: state Y
trY: list transition_item
Hpr: trace_project (sX, []) = Some (sY, trY)
isX: state X
trX: list transition_item
HtrX: finite_valid_trace_from X isX trX
HsX: finite_trace_last isX trX = sX
Hpr_extends_left: ∃ (s'Y : state Y) (preY : 
                   list
                     transition_item),
  trace_project (isX, trX ++ []) =
  Some (s'Y, preY ++ trY)
  ∧ finite_trace_last s'Y preY = sY
valid_state_prop Y sY
  destruct Hpr_extends_left as [isY [preY [Hpr_tr HsY]]].message: Type
X, Y: VLSM message
trace_project: state X * list transition_item
→ option
    (state Y * list transition_item)
Hsimul: VLSM_weak_partial_projection X Y
  trace_project
sX: state X
sY: state Y
trY: list transition_item
Hpr: trace_project (sX, []) = Some (sY, trY)
isX: state X
trX: list transition_item
HtrX: finite_valid_trace_from X isX trX
HsX: finite_trace_last isX trX = sX
isY: state Y
preY: list transition_item
Hpr_tr: trace_project (isX, trX ++ []) =
Some (isY, preY ++ trY)
HsY: finite_trace_last isY preY = sY
valid_state_prop Y sY
  rewrite !app_nil_r in Hpr_tr.message: Type
X, Y: VLSM message
trace_project: state X * list transition_item
→ option
    (state Y * list transition_item)
Hsimul: VLSM_weak_partial_projection X Y
  trace_project
sX: state X
sY: state Y
trY: list transition_item
Hpr: trace_project (sX, []) = Some (sY, trY)
isX: state X
trX: list transition_item
HtrX: finite_valid_trace_from X isX trX
HsX: finite_trace_last isX trX = sX
isY: state Y
preY: list transition_item
Hpr_tr: trace_project (isX, trX) =
Some (isY, preY ++ trY)
HsY: finite_trace_last isY preY = sY
valid_state_prop Y sY
  specialize (VLSM_weak_partial_projection_finite_valid_trace_from _ _ _ _ Hpr_tr HtrX)
    as Hinit_to.message: Type
X, Y: VLSM message
trace_project: state X * list transition_item
→ option
    (state Y * list transition_item)
Hsimul: VLSM_weak_partial_projection X Y
  trace_project
sX: state X
sY: state Y
trY: list transition_item
Hpr: trace_project (sX, []) = Some (sY, trY)
isX: state X
trX: list transition_item
HtrX: finite_valid_trace_from X isX trX
HsX: finite_trace_last isX trX = sX
isY: state Y
preY: list transition_item
Hpr_tr: trace_project (isX, trX) =
Some (isY, preY ++ trY)
HsY: finite_trace_last isY preY = sY
Hinit_to: finite_valid_trace_from Y isY (preY ++ trY)
valid_state_prop Y sY
  by apply finite_valid_trace_from_app_iff, proj1, finite_valid_trace_last_pstate in Hinit_to; subst.
Qed.

Lemma VLSM_weak_partial_projection_input_valid_transition
  : forall sX itemX sY itemY,
    trace_project (sX, [itemX]) = Some (sY, [itemY]) ->
    input_valid_transition X (l itemX) (sX, input itemX) (destination itemX, output itemX) ->
    input_valid_transition Y (l itemY) (sY, input itemY) (destination itemY, output itemY).message: Type
X, Y: VLSM message
trace_project: state X * list transition_item
→ option
    (state Y * list transition_item)
Hsimul: VLSM_weak_partial_projection X Y
  trace_project
∀ (sX : state X) (itemX : transition_item) (sY : state
                                                 Y) 
  (itemY : transition_item),
  trace_project (sX, [itemX]) = Some (sY, [itemY])
  → input_valid_transition X (l itemX)
      (sX, input itemX)
      (destination itemX, output itemX)
    → input_valid_transition Y (l itemY)
        (sY, input itemY)
        (destination itemY, output itemY)
Proof.message: Type
X, Y: VLSM message
trace_project: state X * list transition_item
→ option
    (state Y * list transition_item)
Hsimul: VLSM_weak_partial_projection X Y
  trace_project
∀ (sX : state X) (itemX : transition_item) (sY : state
                                                 Y) 
  (itemY : transition_item),
  trace_project (sX, [itemX]) = Some (sY, [itemY])
  → input_valid_transition X (l itemX)
      (sX, input itemX)
      (destination itemX, output itemX)
    → input_valid_transition Y (l itemY)
        (sY, input itemY)
        (destination itemY, output itemY)
  intros sX itemX sY itemY Hpr HtX.message: Type
X, Y: VLSM message
trace_project: state X * list transition_item
→ option
    (state Y * list transition_item)
Hsimul: VLSM_weak_partial_projection X Y
  trace_project
sX: state X
itemX: transition_item
sY: state Y
itemY: transition_item
Hpr: trace_project (sX, [itemX]) = Some (sY, [itemY])
HtX: input_valid_transition X 
  (l itemX) (sX, input itemX)
  (destination itemX, output itemX)
input_valid_transition Y (l itemY) (sY, input itemY)
  (destination itemY, output itemY)
  apply finite_valid_trace_singleton in HtX.message: Type
X, Y: VLSM message
trace_project: state X * list transition_item
→ option
    (state Y * list transition_item)
Hsimul: VLSM_weak_partial_projection X Y
  trace_project
sX: state X
itemX: transition_item
sY: state Y
itemY: transition_item
Hpr: trace_project (sX, [itemX]) = Some (sY, [itemY])
HtX: finite_valid_trace_from X sX
  [{|
     l := l itemX;
     input := input itemX;
     destination := destination itemX;
     output := output itemX
   |}]
input_valid_transition Y (l itemY) (sY, input itemY)
  (destination itemY, output itemY)
  apply VLSM_weak_partial_projection_finite_valid_trace_from with (sY := sY) (trY := [itemY]) in HtX
  ; [| by destruct itemX].message: Type
X, Y: VLSM message
trace_project: state X * list transition_item
→ option
    (state Y * list transition_item)
Hsimul: VLSM_weak_partial_projection X Y
  trace_project
sX: state X
itemX: transition_item
sY: state Y
itemY: transition_item
Hpr: trace_project (sX, [itemX]) = Some (sY, [itemY])
HtX: finite_valid_trace_from Y sY [itemY]
input_valid_transition Y (l itemY) (sY, input itemY)
  (destination itemY, output itemY)
  by inversion_clear HtX.
Qed.

Lemma VLSM_weak_partial_projection_input_valid
  : forall sX itemX, input_valid_transition_item X sX itemX ->
    forall sY itemY, trace_project (sX, [itemX]) = Some (sY, [itemY]) ->
    input_valid Y (l itemY) (sY, input itemY).message: Type
X, Y: VLSM message
trace_project: state X * list transition_item
→ option
    (state Y * list transition_item)
Hsimul: VLSM_weak_partial_projection X Y
  trace_project
∀ (sX : state X) (itemX : transition_item),
  input_valid_transition_item X sX itemX
  → ∀ (sY : state Y) (itemY : transition_item),
      trace_project (sX, [itemX]) = Some (sY, [itemY])
      → input_valid Y (l itemY) (sY, input itemY)
Proof.message: Type
X, Y: VLSM message
trace_project: state X * list transition_item
→ option
    (state Y * list transition_item)
Hsimul: VLSM_weak_partial_projection X Y
  trace_project
∀ (sX : state X) (itemX : transition_item),
  input_valid_transition_item X sX itemX
  → ∀ (sY : state Y) (itemY : transition_item),
      trace_project (sX, [itemX]) = Some (sY, [itemY])
      → input_valid Y (l itemY) (sY, input itemY)
  intros sX itemX HitemX sY itemY Hpr.message: Type
X, Y: VLSM message
trace_project: state X * list transition_item
→ option
    (state Y * list transition_item)
Hsimul: VLSM_weak_partial_projection X Y
  trace_project
sX: state X
itemX: transition_item
HitemX: input_valid_transition_item X sX itemX
sY: state Y
itemY: transition_item
Hpr: trace_project (sX, [itemX]) = Some (sY, [itemY])
input_valid Y (l itemY) (sY, input itemY)
  by eapply VLSM_weak_partial_projection_input_valid_transition.
Qed.

End sec_weak_partial_projection_properties.

Section sec_partial_projection_properties.

Partial projection properties

Context
  {message : Type}
  {X Y : VLSM message}
  {trace_project :
    state X * list (transition_item X) -> option (state Y * list (transition_item Y))}
  (Hsimul : VLSM_partial_projection X Y trace_project)
  .

Lemma VLSM_partial_projection_finite_valid_trace :
  forall sX trX sY trY,
    trace_project (sX, trX) = Some (sY, trY) ->
    finite_valid_trace X sX trX -> finite_valid_trace Y sY trY.message: Type
X, Y: VLSM message
trace_project: state X * list transition_item
→ option
    (state Y * list transition_item)
Hsimul: VLSM_partial_projection X Y trace_project
∀ (sX : state X) (trX : list transition_item) (sY : 
                                               state Y) 
  (trY : list transition_item),
  trace_project (sX, trX) = Some (sY, trY)
  → finite_valid_trace X sX trX
    → finite_valid_trace Y sY trY
Proof.message: Type
X, Y: VLSM message
trace_project: state X * list transition_item
→ option
    (state Y * list transition_item)
Hsimul: VLSM_partial_projection X Y trace_project
∀ (sX : state X) (trX : list transition_item) (sY : 
                                               state Y) 
  (trY : list transition_item),
  trace_project (sX, trX) = Some (sY, trY)
  → finite_valid_trace X sX trX
    → finite_valid_trace Y sY trY
  exact (partial_trace_project_preserves_valid_trace _ _ _ Hsimul).
Qed.

Lemma VLSM_partial_projection_finite_valid_trace_from
  : forall sX trX sY trY,
    trace_project (sX, trX) = Some (sY, trY) ->
    finite_valid_trace_from X sX trX -> finite_valid_trace_from Y sY trY.message: Type
X, Y: VLSM message
trace_project: state X * list transition_item
→ option
    (state Y * list transition_item)
Hsimul: VLSM_partial_projection X Y trace_project
∀ (sX : state X) (trX : list transition_item) (sY : 
                                               state Y) 
  (trY : list transition_item),
  trace_project (sX, trX) = Some (sY, trY)
  → finite_valid_trace_from X sX trX
    → finite_valid_trace_from Y sY trY
Proof.message: Type
X, Y: VLSM message
trace_project: state X * list transition_item
→ option
    (state Y * list transition_item)
Hsimul: VLSM_partial_projection X Y trace_project
∀ (sX : state X) (trX : list transition_item) (sY : 
                                               state Y) 
  (trY : list transition_item),
  trace_project (sX, trX) = Some (sY, trY)
  → finite_valid_trace_from X sX trX
    → finite_valid_trace_from Y sY trY
  intros sX trX sY trY Hpr_tr HtrX.message: Type
X, Y: VLSM message
trace_project: state X * list transition_item
→ option
    (state Y * list transition_item)
Hsimul: VLSM_partial_projection X Y trace_project
sX: state X
trX: list transition_item
sY: state Y
trY: list transition_item
Hpr_tr: trace_project (sX, trX) = Some (sY, trY)
HtrX: finite_valid_trace_from X sX trX
finite_valid_trace_from Y sY trY
  apply (finite_valid_trace_from_complete_left X) in HtrX
    as [isX [preX [Htr'X HsX]]].message: Type
X, Y: VLSM message
trace_project: state X * list transition_item
→ option
    (state Y * list transition_item)
Hsimul: VLSM_partial_projection X Y trace_project
sX: state X
trX: list transition_item
sY: state Y
trY: list transition_item
Hpr_tr: trace_project (sX, trX) = Some (sY, trY)
isX: state X
preX: list transition_item
Htr'X: finite_valid_trace X isX (preX ++ trX)
HsX: finite_trace_last isX preX = sX
finite_valid_trace_from Y sY trY
  specialize (partial_trace_project_extends_left _ _ _ Hsimul _ _ _ _ Hpr_tr _ _ HsX)
    as Hpr_extends_left.message: Type
X, Y: VLSM message
trace_project: state X * list transition_item
→ option
    (state Y * list transition_item)
Hsimul: VLSM_partial_projection X Y trace_project
sX: state X
trX: list transition_item
sY: state Y
trY: list transition_item
Hpr_tr: trace_project (sX, trX) = Some (sY, trY)
isX: state X
preX: list transition_item
Htr'X: finite_valid_trace X isX (preX ++ trX)
HsX: finite_trace_last isX preX = sX
Hpr_extends_left: finite_valid_trace_from X isX
  (preX ++ trX)
→ ∃ (s'Y : state Y) (preY : 
                     list
                      transition_item),
    trace_project
      (isX, preX ++ trX) =
    Some (s'Y, preY ++ trY)
    ∧ finite_trace_last s'Y preY =
      sY
finite_valid_trace_from Y sY trY
  spec Hpr_extends_left; [by apply proj1 in Htr'X |].message: Type
X, Y: VLSM message
trace_project: state X * list transition_item
→ option
    (state Y * list transition_item)
Hsimul: VLSM_partial_projection X Y trace_project
sX: state X
trX: list transition_item
sY: state Y
trY: list transition_item
Hpr_tr: trace_project (sX, trX) = Some (sY, trY)
isX: state X
preX: list transition_item
Htr'X: finite_valid_trace X isX (preX ++ trX)
HsX: finite_trace_last isX preX = sX
Hpr_extends_left: ∃ (s'Y : state Y) (preY : 
                   list
                     transition_item),
  trace_project (isX, preX ++ trX) =
  Some (s'Y, preY ++ trY)
  ∧ finite_trace_last s'Y preY = sY
finite_valid_trace_from Y sY trY
  destruct Hpr_extends_left as [isY [preY [Hpr_tr' HsY]]].message: Type
X, Y: VLSM message
trace_project: state X * list transition_item
→ option
    (state Y * list transition_item)
Hsimul: VLSM_partial_projection X Y trace_project
sX: state X
trX: list transition_item
sY: state Y
trY: list transition_item
Hpr_tr: trace_project (sX, trX) = Some (sY, trY)
isX: state X
preX: list transition_item
Htr'X: finite_valid_trace X isX (preX ++ trX)
HsX: finite_trace_last isX preX = sX
isY: state Y
preY: list transition_item
Hpr_tr': trace_project (isX, preX ++ trX) =
Some (isY, preY ++ trY)
HsY: finite_trace_last isY preY = sY
finite_valid_trace_from Y sY trY
  specialize (VLSM_partial_projection_finite_valid_trace _ _ _ _ Hpr_tr' Htr'X)
    as Hinit_to.message: Type
X, Y: VLSM message
trace_project: state X * list transition_item
→ option
    (state Y * list transition_item)
Hsimul: VLSM_partial_projection X Y trace_project
sX: state X
trX: list transition_item
sY: state Y
trY: list transition_item
Hpr_tr: trace_project (sX, trX) = Some (sY, trY)
isX: state X
preX: list transition_item
Htr'X: finite_valid_trace X isX (preX ++ trX)
HsX: finite_trace_last isX preX = sX
isY: state Y
preY: list transition_item
Hpr_tr': trace_project (isX, preX ++ trX) =
Some (isY, preY ++ trY)
HsY: finite_trace_last isY preY = sY
Hinit_to: finite_valid_trace Y isY (preY ++ trY)
finite_valid_trace_from Y sY trY
  by apply proj1, finite_valid_trace_from_app_iff, proj2 in Hinit_to; subst.
Qed.

Lemma VLSM_partial_projection_initial_state
  : forall sX sY trY,
    trace_project (sX, []) = Some (sY, trY) ->
    initial_state_prop X sX -> initial_state_prop Y sY.message: Type
X, Y: VLSM message
trace_project: state X * list transition_item
→ option
    (state Y * list transition_item)
Hsimul: VLSM_partial_projection X Y trace_project
∀ (sX : state X) (sY : state Y) (trY : list
                                         transition_item),
  trace_project (sX, []) = Some (sY, trY)
  → initial_state_prop sX → initial_state_prop sY
Proof.message: Type
X, Y: VLSM message
trace_project: state X * list transition_item
→ option
    (state Y * list transition_item)
Hsimul: VLSM_partial_projection X Y trace_project
∀ (sX : state X) (sY : state Y) (trY : list
                                         transition_item),
  trace_project (sX, []) = Some (sY, trY)
  → initial_state_prop sX → initial_state_prop sY
  intros sX sY trY Hpr HsX.message: Type
X, Y: VLSM message
trace_project: state X * list transition_item
→ option
    (state Y * list transition_item)
Hsimul: VLSM_partial_projection X Y trace_project
sX: state X
sY: state Y
trY: list transition_item
Hpr: trace_project (sX, []) = Some (sY, trY)
HsX: initial_state_prop sX
initial_state_prop sY
  eapply VLSM_partial_projection_finite_valid_trace; [done |].message: Type
X, Y: VLSM message
trace_project: state X * list transition_item
→ option
    (state Y * list transition_item)
Hsimul: VLSM_partial_projection X Y trace_project
sX: state X
sY: state Y
trY: list transition_item
Hpr: trace_project (sX, []) = Some (sY, trY)
HsX: initial_state_prop sX
finite_valid_trace X sX []
  split; [| done].message: Type
X, Y: VLSM message
trace_project: state X * list transition_item
→ option
    (state Y * list transition_item)
Hsimul: VLSM_partial_projection X Y trace_project
sX: state X
sY: state Y
trY: list transition_item
Hpr: trace_project (sX, []) = Some (sY, trY)
HsX: initial_state_prop sX
finite_valid_trace_from X sX []
  by constructor; apply initial_state_is_valid.
Qed.

Definition VLSM_partial_projection_weaken : VLSM_weak_partial_projection X Y trace_project :=
  {| weak_partial_projection_type := partial_projection_type _ _ _ Hsimul
  ;  weak_partial_trace_project_preserves_valid_trace :=
       VLSM_partial_projection_finite_valid_trace_from
  |}.

Lemma VLSM_partial_projection_valid_state :
  forall sX sY trY,
    trace_project (sX, []) = Some (sY, trY) ->
    valid_state_prop X sX -> valid_state_prop Y sY.message: Type
X, Y: VLSM message
trace_project: state X * list transition_item
→ option
    (state Y * list transition_item)
Hsimul: VLSM_partial_projection X Y trace_project
∀ (sX : state X) (sY : state Y) (trY : list
                                         transition_item),
  trace_project (sX, []) = Some (sY, trY)
  → valid_state_prop X sX → valid_state_prop Y sY
Proof.message: Type
X, Y: VLSM message
trace_project: state X * list transition_item
→ option
    (state Y * list transition_item)
Hsimul: VLSM_partial_projection X Y trace_project
∀ (sX : state X) (sY : state Y) (trY : list
                                         transition_item),
  trace_project (sX, []) = Some (sY, trY)
  → valid_state_prop X sX → valid_state_prop Y sY
  exact (VLSM_weak_partial_projection_valid_state VLSM_partial_projection_weaken).
Qed.

Lemma  VLSM_partial_projection_input_valid_transition :
  forall sX itemX sY itemY,
    trace_project (sX, [itemX]) = Some (sY, [itemY]) ->
    input_valid_transition X (l itemX) (sX, input itemX) (destination itemX, output itemX) ->
    input_valid_transition Y (l itemY) (sY, input itemY) (destination itemY, output itemY).message: Type
X, Y: VLSM message
trace_project: state X * list transition_item
→ option
    (state Y * list transition_item)
Hsimul: VLSM_partial_projection X Y trace_project
∀ (sX : state X) (itemX : transition_item) (sY : state
                                                 Y) 
  (itemY : transition_item),
  trace_project (sX, [itemX]) = Some (sY, [itemY])
  → input_valid_transition X (l itemX)
      (sX, input itemX)
      (destination itemX, output itemX)
    → input_valid_transition Y (l itemY)
        (sY, input itemY)
        (destination itemY, output itemY)
Proof.message: Type
X, Y: VLSM message
trace_project: state X * list transition_item
→ option
    (state Y * list transition_item)
Hsimul: VLSM_partial_projection X Y trace_project
∀ (sX : state X) (itemX : transition_item) (sY : state
                                                 Y) 
  (itemY : transition_item),
  trace_project (sX, [itemX]) = Some (sY, [itemY])
  → input_valid_transition X (l itemX)
      (sX, input itemX)
      (destination itemX, output itemX)
    → input_valid_transition Y (l itemY)
        (sY, input itemY)
        (destination itemY, output itemY)
  exact (VLSM_weak_partial_projection_input_valid_transition VLSM_partial_projection_weaken).
Qed.

Lemma VLSM_partial_projection_input_valid :
  forall (sX : state X) (itemX : transition_item),
    input_valid_transition_item X sX itemX ->
  forall (sY : state Y) (itemY : transition_item),
    trace_project (sX, [itemX]) = Some (sY, [itemY]) ->
      input_valid Y (l itemY) (sY, input itemY).message: Type
X, Y: VLSM message
trace_project: state X * list transition_item
→ option
    (state Y * list transition_item)
Hsimul: VLSM_partial_projection X Y trace_project
∀ (sX : state X) (itemX : transition_item),
  input_valid_transition_item X sX itemX
  → ∀ (sY : state Y) (itemY : transition_item),
      trace_project (sX, [itemX]) = Some (sY, [itemY])
      → input_valid Y (l itemY) (sY, input itemY)
Proof.message: Type
X, Y: VLSM message
trace_project: state X * list transition_item
→ option
    (state Y * list transition_item)
Hsimul: VLSM_partial_projection X Y trace_project
∀ (sX : state X) (itemX : transition_item),
  input_valid_transition_item X sX itemX
  → ∀ (sY : state Y) (itemY : transition_item),
      trace_project (sX, [itemX]) = Some (sY, [itemY])
      → input_valid Y (l itemY) (sY, input itemY)
  exact (VLSM_weak_partial_projection_input_valid VLSM_partial_projection_weaken).
Qed.

End sec_partial_projection_properties.

End sec_VLSM_partial_projection.