From VLSM.Lib Require Import Itauto.
From stdpp Require Import prelude.
From VLSM.Lib Require Import Preamble ListExtras StreamExtras StreamFilters StdppExtras.
From VLSM.Core Require Import VLSM VLSMProjections.VLSMPartialProjection.

Core: VLSM Total Projections

A VLSM projection guaranteeing the existence of projection for all states and traces. We say that VLSM X projects to VLSM Y (sharing the same messages) if there exists maps state_project taking X-states to Y-states, and trace_project, taking list of transitions from X to Y, such that:

state and trace_project_preserves_valid_traces
trace_project_app: trace projection commutes with concatenation of traces
final_state_project: state projection commutes with finite_trace_last

Proper examples of total projections (which are not VLSM_embeddings) are projections in which some of transitions might be dropped, such as the projection of a composition to one of the components (component_projection) or the projection of the compositions of equivocators to the composition of regular components using the particular MachineDescriptor which select the first (original) component instance for each equivocator (e.g., equivocators_no_equivocations_vlsm_X_vlsm_projection).

Projection definitions and properties

Section sec_projection_type_properties.

Definition VLSM_partial_trace_project_from_projection
  {message : Type}
  {X : VLSM message}
  {TY : VLSMType message}
  (label_project : label X -> option (label TY))
  (state_project : state X -> state TY)
  (trace_project := pre_VLSM_projection_finite_trace_project _ _ label_project state_project)
  := fun str : state X * list (transition_item X) =>
      let (s, tr) := str in Some (state_project s , trace_project tr ).

Context
  {message : Type}
  {X Y : VLSM message}
  {label_project : label X -> option (label Y)}
  {state_project : state X -> state Y}
  (trace_project := pre_VLSM_projection_finite_trace_project _ _ label_project state_project)
  (Hsimul : VLSM_projection_type X Y label_project state_project)
  .

Any VLSM_projection_type determines a VLSM_partial_projection_type, allowing us to lift to VLSM projection the generic results proved about VLSM partial projections.

Lemma VLSM_partial_projection_type_from_projection :
  VLSM_partial_projection_type X Y
    (VLSM_partial_trace_project_from_projection label_project state_project).
Proof.
  split; intros; inversion H; subst; clear H.
  exists (state_project s'X), (trace_project preX). split.
  - by cbn; rewrite pre_VLSM_projection_finite_trace_project_app.
  - symmetry. apply (final_state_project _ _ _ _ Hsimul).
    by apply (finite_valid_trace_from_app_iff X) in H1; apply H1.
Qed.

End sec_projection_type_properties.

Section sec_projection_transition_consistency_None.

Context
  {message : Type}
  (X : VLSM message)
  (TY : VLSMType message)
  (label_project : label X -> option (label TY))
  (state_project : state X -> state TY)
  .

When a label cannot be projected, and thus the transition will not be preserved by the projection, the state projections of the states between and after the transition must coincide.

Definition weak_projection_transition_consistency_None : Prop :=
  forall lX, label_project lX = None ->
  forall s om s' om', input_valid_transition X lX (s , om ) (s', om') ->
      state_project s' = state_project s.

Definition strong_projection_transition_consistency_None : Prop :=
  forall lX, label_project lX = None ->
  forall s om s' om', transition X lX (s , om ) = (s', om') ->
    state_project s' = state_project s.

Lemma strong_projection_transition_consistency_None_weaken
  : strong_projection_transition_consistency_None ->
    weak_projection_transition_consistency_None.
Proof.
  intros Hstrong lX Hl s om s' om' Ht.
  by apply (Hstrong lX Hl _ _ _ _ (proj2 Ht)).
Qed.

End sec_projection_transition_consistency_None.

Section sec_VLSM_projection_definitions.

Context
  {message : Type}
  (X Y : VLSM message)
  (label_project : label X -> option (label Y))
  (state_project : state X -> state Y)
  (trace_project := pre_VLSM_projection_finite_trace_project _ _ label_project state_project)
  .

Similarly to the VLSM_partial_projection case we distinguish two types of projections: VLSM_weak_projection and VLSM_projection, distinguished by the fact that the weak projections are not required to preserve initial states.

Although we don't have proper examples of VLSM_weak_projections, they are a support base for VLSM_weak_embeddings for which we have proper examples.

Any VLSM_projection determines a VLSM_partial_projection, allowing us to lift to VLSM projection the generic results proved about VLSM partial projections.

Any VLSM_projection determines a VLSM_partial_projection, allowing us to lift to VLSM projection the generic results proved about VLSM partial projections.

Projection friendliness

A projection is friendly if all the valid traces of the projection are projections of the valid traces of the source VLSM.

Section sec_projection_friendliness.

We axiomatize projection friendliness as the converse of VLSM_projection_finite_valid_trace

Definition projection_friendly_prop
  := forall
    (sY : state Y)
    (trY : list (transition_item Y))
    (HtrY : finite_valid_trace Y sY trY),
    exists (sX : state X) (trX : list (transition_item X)),
      finite_valid_trace X sX trX
      /\ state_project sX = sY
      /\ VLSM_projection_finite_trace_project Hsimul trX = trY.

Lemma projection_friendly_in_futures
  (Hfr : projection_friendly_prop)
  (s1 s2 : state Y)
  (Hfuture : in_futures Y s1 s2)
  : exists (sX1 sX2 : state X ),
    state_project sX1 = s1 /\ state_project sX2 = s2 /\ in_futures X sX1 sX2.
Proof.
  destruct Hfuture as [tr_s2 Hfuture].
  apply finite_valid_trace_from_to_complete_left in Hfuture
    as [is [tr_s1 [Htr Heq_s1]]].
  apply valid_trace_get_last in Htr as Heq_s2.
  apply valid_trace_forget_last in Htr.
  apply Hfr in Htr as [isX [trX [Htr [His Htr_pr]]]].
  apply VLSM_projection_finite_trace_project_app_rev in Htr_pr
    as (trX_s1 & trX_s2 & HeqtrX & Htr_s1_pr & Htr_s2_pr).
  subst.
  destruct Htr as [HtrX HisX].
  apply finite_valid_trace_from_app_iff in HtrX as HtrX12.
  destruct HtrX12 as [HtrX1 HtrX2].
  apply valid_trace_add_default_last in HtrX2.
  exists (finite_trace_last isX trX_s1).
  exists (finite_trace_last isX (trX_s1 ++ trX_s2)).
  rewrite !VLSM_projection_finite_trace_last,
    VLSM_projection_finite_trace_project_app; [| done | done].
  repeat split.
  by rewrite finite_trace_last_app; eexists.
Qed.

A consequence of the projection_friendly_property is that the valid traces of the projection are precisely the projections of all the valid traces of the source VLSM.

Lemma projection_friendly_trace_char
  (Hfriendly : projection_friendly_prop)
  : forall sY trY, finite_valid_trace Y sY trY <->
    exists (sX : state X) (trX : list (transition_item X)),
      finite_valid_trace X sX trX
      /\ state_project sX = sY
      /\ VLSM_projection_finite_trace_project Hsimul trX = trY.
Proof.
  split; [by apply Hfriendly |].
  intros [sX [trX [HtrX [<- <-]]]].
  by apply VLSM_projection_finite_valid_trace.
Qed.

End sec_projection_friendliness.

End sec_projection_properties.

End sec_VLSM_projection.

For VLSM X to project to a VLSM Y, the following set of conditions is sufficient:

X's initial_states project to Y's initial states
Every message m (including the empty one) which can be input to a projectable input_valid transition in X, is a valid_message in Y
X's input_valid is included in Y's valid.
For all projectable input_valid inputs (in X), Y's transition acts like X's transition.
All non-projectable transitions preserve the projected state