Built with
Alectryon , running Coq+SerAPI v8.18.0+0.18.1. Bubbles (
) indicate interactive fragments: hover for details, tap to reveal contents. Use
Ctrl+↑ Ctrl+↓ to navigate,
Ctrl+🖱️ to focus. On Mac, use
⌘ instead of
Ctrl .
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 ListExtras.
From VLSM.Core Require Import VLSM PreloadedVLSM VLSMProjections Validator Composition.
From VLSM.Core Require Import ConstrainedVLSM.
Core: State-Annotated VLSMs
This module describes the VLSM obtained by augmenting the states of an existing
VLSM with annotations and providing additional validity constraints taking into
account the annotations, and a function for updating the annotations following a
transition.
Section sec_annotated_vlsm .
Context
{message : Type }
(X : VLSM message)
(annotation : Type )
.
Record annotated_state : Type := mk_annotated_state
{
original_state : state X;
state_annotation : annotation;
}.
Definition annotated_type : VLSMType message :=
{| label := label X;
state := annotated_state
|}.
Context
(initial_annotation_prop : annotation -> Prop )
`{Inhabited (sig initial_annotation_prop)}
.
Definition annotated_initial_state_prop (sa : annotated_state) : Prop :=
initial_state_prop X (original_state sa) /\ initial_annotation_prop (state_annotation sa).
#[export] Program Instance annotated_initial_state_prop_inhabited :
Inhabited {sa : annotated_state | annotated_initial_state_prop sa} :=
populate (exist _ {| original_state := `(vs0 X); state_annotation := `inhabitant; |} _).
Next Obligation .message : Type X : VLSM message annotation : Type initial_annotation_prop : annotation → Prop H : Inhabited
{x : annotation | initial_annotation_prop x}
(λ sa : annotated_state,
annotated_initial_state_prop sa)
{|
original_state := `(vs0 X);
state_annotation := `inhabitant
|}
Proof .message : Type X : VLSM message annotation : Type initial_annotation_prop : annotation → Prop H : Inhabited
{x : annotation | initial_annotation_prop x}
(λ sa : annotated_state,
annotated_initial_state_prop sa)
{|
original_state := `(vs0 X);
state_annotation := `inhabitant
|}
split ; cbn .message : Type X : VLSM message annotation : Type initial_annotation_prop : annotation → Prop H : Inhabited
{x : annotation | initial_annotation_prop x}
initial_state_prop (`(vs0 X))
- message : Type X : VLSM message annotation : Type initial_annotation_prop : annotation → Prop H : Inhabited
{x : annotation | initial_annotation_prop x}
initial_state_prop (`(vs0 X))
by destruct (vs0 X).
- message : Type X : VLSM message annotation : Type initial_annotation_prop : annotation → Prop H : Inhabited
{x : annotation | initial_annotation_prop x}
initial_annotation_prop (`inhabitant)
by destruct inhabitant.
Qed .
Context
(annotated_transition_state :
label annotated_type -> annotated_state * option message -> annotation)
.
Definition annotated_valid
(l : label annotated_type)
(som : annotated_state * option message)
: Prop :=
valid X l (original_state som.1 , som.2 ).
Definition annotated_transition
(l : label annotated_type)
(som : annotated_state * option message)
: annotated_state * option message :=
let (s' , om') := transition X l (original_state som.1 , som.2 ) in
({| original_state := s'; state_annotation := annotated_transition_state l som |}, om').
Definition annotated_vlsm_machine : VLSMMachine annotated_type :=
{| initial_state_prop := fun s : state annotated_type => annotated_initial_state_prop s
; initial_message_prop := fun m : message => initial_message_prop X m
; valid := annotated_valid
; transition := annotated_transition
|}.
Definition annotated_vlsm : VLSM message := mk_vlsm annotated_vlsm_machine.
Definition annotate_trace_item
(item : transition_item X)
(k : annotated_state -> list (transition_item annotated_type))
(sa : annotated_state)
: list (transition_item annotated_type) :=
let sa' :=
{|
original_state := destination item;
state_annotation := annotated_transition_state (l item) (sa, input item);
|}
in
Build_transition_item annotated_type (l item) (input item) sa' (output item) :: k sa'.
Lemma annotate_trace_item_project
(item : transition_item X)
(k : annotated_state -> list (transition_item annotated_type))
(sa : annotated_state)
: pre_VLSM_embedding_finite_trace_project
annotated_type X id original_state
(annotate_trace_item item k sa)
= item ::
pre_VLSM_embedding_finite_trace_project
annotated_type X id original_state
(k {| original_state := destination item;
state_annotation := annotated_transition_state (l item) (sa, input item) |}).message : Type X : VLSM message annotation : Type initial_annotation_prop : annotation → Prop H : Inhabited
{x : annotation | initial_annotation_prop x} annotated_transition_state : label annotated_type
→ annotated_state *
option message
→ annotation item : transition_item k : annotated_state → list transition_item sa : annotated_state
pre_VLSM_embedding_finite_trace_project annotated_type
X id original_state (annotate_trace_item item k sa) =
item
:: pre_VLSM_embedding_finite_trace_project
annotated_type X id original_state
(k
{|
original_state := destination item;
state_annotation :=
annotated_transition_state (l item)
(sa, input item)
|})
Proof .message : Type X : VLSM message annotation : Type initial_annotation_prop : annotation → Prop H : Inhabited
{x : annotation | initial_annotation_prop x} annotated_transition_state : label annotated_type
→ annotated_state *
option message
→ annotation item : transition_item k : annotated_state → list transition_item sa : annotated_state
pre_VLSM_embedding_finite_trace_project annotated_type
X id original_state (annotate_trace_item item k sa) =
item
:: pre_VLSM_embedding_finite_trace_project
annotated_type X id original_state
(k
{|
original_state := destination item;
state_annotation :=
annotated_transition_state (l item)
(sa, input item)
|})
by destruct item.
Qed .
Definition annotate_trace_from (sa : state annotated_type) (tr : list (transition_item X))
: list (transition_item annotated_type) :=
fold_right annotate_trace_item (fun sa => []) tr sa.
Lemma annotate_trace_from_unroll sa item tr
: annotate_trace_from sa (item :: tr) =
let sa' :=
{|
original_state := destination item;
state_annotation := annotated_transition_state (l item) (sa, input item)
|}
in
Build_transition_item annotated_type (l item) (input item) sa' (output item)
::
annotate_trace_from sa' tr.message : Type X : VLSM message annotation : Type initial_annotation_prop : annotation → Prop H : Inhabited
{x : annotation | initial_annotation_prop x} annotated_transition_state : label annotated_type
→ annotated_state *
option message
→ annotation sa : state annotated_type item : transition_item tr : list transition_item
annotate_trace_from sa (item :: tr) =
(let sa' :=
{|
original_state := destination item;
state_annotation :=
annotated_transition_state (l item)
(sa, input item)
|} in
{|
l := l item;
input := input item;
destination := sa';
output := output item
|} :: annotate_trace_from sa' tr)
Proof .message : Type X : VLSM message annotation : Type initial_annotation_prop : annotation → Prop H : Inhabited
{x : annotation | initial_annotation_prop x} annotated_transition_state : label annotated_type
→ annotated_state *
option message
→ annotation sa : state annotated_type item : transition_item tr : list transition_item
annotate_trace_from sa (item :: tr) =
(let sa' :=
{|
original_state := destination item;
state_annotation :=
annotated_transition_state (l item)
(sa, input item)
|} in
{|
l := l item;
input := input item;
destination := sa';
output := output item
|} :: annotate_trace_from sa' tr)
by destruct item.
Qed .
Lemma annotate_trace_from_app sa tr1 tr2
: annotate_trace_from sa (tr1 ++ tr2) =
annotate_trace_from sa tr1 ++
annotate_trace_from (finite_trace_last sa (annotate_trace_from sa tr1)) tr2.message : Type X : VLSM message annotation : Type initial_annotation_prop : annotation → Prop H : Inhabited
{x : annotation | initial_annotation_prop x} annotated_transition_state : label annotated_type
→ annotated_state *
option message
→ annotation sa : state annotated_type tr1, tr2 : list transition_item
annotate_trace_from sa (tr1 ++ tr2) =
annotate_trace_from sa tr1 ++
annotate_trace_from
(finite_trace_last sa (annotate_trace_from sa tr1))
tr2
Proof .message : Type X : VLSM message annotation : Type initial_annotation_prop : annotation → Prop H : Inhabited
{x : annotation | initial_annotation_prop x} annotated_transition_state : label annotated_type
→ annotated_state *
option message
→ annotation sa : state annotated_type tr1, tr2 : list transition_item
annotate_trace_from sa (tr1 ++ tr2) =
annotate_trace_from sa tr1 ++
annotate_trace_from
(finite_trace_last sa (annotate_trace_from sa tr1))
tr2
revert sa.message : Type X : VLSM message annotation : Type initial_annotation_prop : annotation → Prop H : Inhabited
{x : annotation | initial_annotation_prop x} annotated_transition_state : label annotated_type
→ annotated_state *
option message
→ annotation tr1, tr2 : list transition_item
∀ sa : state annotated_type,
annotate_trace_from sa (tr1 ++ tr2) =
annotate_trace_from sa tr1 ++
annotate_trace_from
(finite_trace_last sa (annotate_trace_from sa tr1))
tr2
induction tr1 as [| item tr1]; [done |].message : Type X : VLSM message annotation : Type initial_annotation_prop : annotation → Prop H : Inhabited
{x : annotation | initial_annotation_prop x} annotated_transition_state : label annotated_type
→ annotated_state *
option message
→ annotation item : transition_item tr1, tr2 : list transition_item IHtr1 : ∀ sa : state annotated_type,
annotate_trace_from sa (tr1 ++ tr2) =
annotate_trace_from sa tr1 ++
annotate_trace_from
(finite_trace_last sa
(annotate_trace_from sa tr1)) tr2
∀ sa : state annotated_type,
annotate_trace_from sa ((item :: tr1) ++ tr2) =
annotate_trace_from sa (item :: tr1) ++
annotate_trace_from
(finite_trace_last sa
(annotate_trace_from sa (item :: tr1))) tr2
by intro sa; rewrite <- app_comm_cons, !annotate_trace_from_unroll
; simpl ; rewrite IHtr1, finite_trace_last_cons.
Qed .
Lemma annotate_trace_from_last_original_state sa sa' tr
: original_state (finite_trace_last sa (annotate_trace_from sa' tr)) =
finite_trace_last (original_state sa) tr.message : Type X : VLSM message annotation : Type initial_annotation_prop : annotation → Prop H : Inhabited
{x : annotation | initial_annotation_prop x} annotated_transition_state : label annotated_type
→ annotated_state *
option message
→ annotation sa, sa' : state annotated_type tr : list transition_item
original_state
(finite_trace_last sa (annotate_trace_from sa' tr)) =
finite_trace_last (original_state sa) tr
Proof .message : Type X : VLSM message annotation : Type initial_annotation_prop : annotation → Prop H : Inhabited
{x : annotation | initial_annotation_prop x} annotated_transition_state : label annotated_type
→ annotated_state *
option message
→ annotation sa, sa' : state annotated_type tr : list transition_item
original_state
(finite_trace_last sa (annotate_trace_from sa' tr)) =
finite_trace_last (original_state sa) tr
destruct_list_last tr tr' item Heqtr; subst ; [done |]. message : Type X : VLSM message annotation : Type initial_annotation_prop : annotation → Prop H : Inhabited
{x : annotation | initial_annotation_prop x} annotated_transition_state : label annotated_type
→ annotated_state *
option message
→ annotation sa, sa' : state annotated_type tr' : list transition_item item : transition_item
original_state
(finite_trace_last sa
(annotate_trace_from sa' (tr' ++ [item]))) =
finite_trace_last (original_state sa) (tr' ++ [item])
rewrite annotate_trace_from_app.message : Type X : VLSM message annotation : Type initial_annotation_prop : annotation → Prop H : Inhabited
{x : annotation | initial_annotation_prop x} annotated_transition_state : label annotated_type
→ annotated_state *
option message
→ annotation sa, sa' : state annotated_type tr' : list transition_item item : transition_item
original_state
(finite_trace_last sa
(annotate_trace_from sa' tr' ++
annotate_trace_from
(finite_trace_last sa'
(annotate_trace_from sa' tr')) [item])) =
finite_trace_last (original_state sa) (tr' ++ [item])
cbn ; unfold annotate_trace_item.message : Type X : VLSM message annotation : Type initial_annotation_prop : annotation → Prop H : Inhabited
{x : annotation | initial_annotation_prop x} annotated_transition_state : label annotated_type
→ annotated_state *
option message
→ annotation sa, sa' : state annotated_type tr' : list transition_item item : transition_item
original_state
(finite_trace_last sa
(annotate_trace_from sa' tr' ++
[{|
l := l item;
input := input item;
destination :=
{|
original_state := destination item;
state_annotation :=
annotated_transition_state (l item)
(finite_trace_last sa'
(annotate_trace_from sa' tr'),
input item)
|};
output := output item
|}])) =
finite_trace_last (original_state sa) (tr' ++ [item])
by rewrite ! finite_trace_last_is_last.
Qed .
Definition annotate_trace (s : state X) (tr : list (transition_item X))
: list (transition_item annotated_type) :=
annotate_trace_from {| original_state := s; state_annotation := ` inhabitant |} tr.
Lemma annotate_trace_last_original_state s s' tr
: original_state (finite_trace_last s (annotate_trace s' tr)) =
finite_trace_last (original_state s) tr.message : Type X : VLSM message annotation : Type initial_annotation_prop : annotation → Prop H : Inhabited
{x : annotation | initial_annotation_prop x} annotated_transition_state : label annotated_type
→ annotated_state *
option message
→ annotation s : state annotated_type s' : state X tr : list transition_item
original_state
(finite_trace_last s (annotate_trace s' tr)) =
finite_trace_last (original_state s) tr
Proof .message : Type X : VLSM message annotation : Type initial_annotation_prop : annotation → Prop H : Inhabited
{x : annotation | initial_annotation_prop x} annotated_transition_state : label annotated_type
→ annotated_state *
option message
→ annotation s : state annotated_type s' : state X tr : list transition_item
original_state
(finite_trace_last s (annotate_trace s' tr)) =
finite_trace_last (original_state s) tr
by apply annotate_trace_from_last_original_state. Qed .
Lemma annotate_trace_project is tr
: pre_VLSM_embedding_finite_trace_project
annotated_type X id original_state
(annotate_trace is tr)
= tr.message : Type X : VLSM message annotation : Type initial_annotation_prop : annotation → Prop H : Inhabited
{x : annotation | initial_annotation_prop x} annotated_transition_state : label annotated_type
→ annotated_state *
option message
→ annotation is : state X tr : list transition_item
pre_VLSM_embedding_finite_trace_project annotated_type
X id original_state (annotate_trace is tr) = tr
Proof .message : Type X : VLSM message annotation : Type initial_annotation_prop : annotation → Prop H : Inhabited
{x : annotation | initial_annotation_prop x} annotated_transition_state : label annotated_type
→ annotated_state *
option message
→ annotation is : state X tr : list transition_item
pre_VLSM_embedding_finite_trace_project annotated_type
X id original_state (annotate_trace is tr) = tr
unfold annotate_trace
; remember {| original_state := is |} as sa; clear Heqsa; revert sa.message : Type X : VLSM message annotation : Type initial_annotation_prop : annotation → Prop H : Inhabited
{x : annotation | initial_annotation_prop x} annotated_transition_state : label annotated_type
→ annotated_state *
option message
→ annotation is : state X tr : list transition_item
∀ sa : annotated_state,
pre_VLSM_embedding_finite_trace_project
annotated_type X id original_state
(annotate_trace_from sa tr) = tr
induction tr as [| item]; [done | intro sa].message : Type X : VLSM message annotation : Type initial_annotation_prop : annotation → Prop H : Inhabited
{x : annotation | initial_annotation_prop x} annotated_transition_state : label annotated_type
→ annotated_state *
option message
→ annotation is : state X item : transition_item tr : list transition_item IHtr : ∀ sa : annotated_state,
pre_VLSM_embedding_finite_trace_project
annotated_type X id original_state
(annotate_trace_from sa tr) = trsa : annotated_state
pre_VLSM_embedding_finite_trace_project annotated_type
X id original_state
(annotate_trace_from sa (item :: tr)) = item :: tr
setoid_rewrite annotate_trace_item_project; f_equal .message : Type X : VLSM message annotation : Type initial_annotation_prop : annotation → Prop H : Inhabited
{x : annotation | initial_annotation_prop x} annotated_transition_state : label annotated_type
→ annotated_state *
option message
→ annotation is : state X item : transition_item tr : list transition_item IHtr : ∀ sa : annotated_state,
pre_VLSM_embedding_finite_trace_project
annotated_type X id original_state
(annotate_trace_from sa tr) = trsa : annotated_state
pre_VLSM_embedding_finite_trace_project annotated_type
X id original_state
((fix fold_right (l : list transition_item) :
annotated_state → list transition_item :=
match l with
| [] => λ _ : annotated_state, []
| b :: t => annotate_trace_item b (fold_right t)
end ) tr
{|
original_state := destination item;
state_annotation :=
annotated_transition_state (l item)
(sa, input item)
|}) = tr
by apply IHtr.
Qed .
End sec_annotated_vlsm .
Arguments original_state {_ _ _} _ : assert .
Arguments state_annotation {_ _ _} _ : assert .
Section sec_annotated_vlsm_projections .
Context
{message : Type }
(X : VLSM message)
{annotation : Type }
(initial_annotation_prop : annotation -> Prop )
`{Inhabited (sig initial_annotation_prop)}
(annotated_constraint :
label (annotated_type X annotation) ->
annotated_state X annotation * option message -> Prop )
(annotated_transition_state :
label (annotated_type X annotation) ->
annotated_state X annotation * option message -> annotation)
(AnnotatedX : VLSM message :=
constrained_vlsm (annotated_vlsm X annotation initial_annotation_prop annotated_transition_state)
annotated_constraint)
.
Definition forget_annotations_projection
: VLSM_embedding AnnotatedX X id original_state.message : Type X : VLSM message annotation : Type initial_annotation_prop : annotation → Prop H : Inhabited
{x : annotation | initial_annotation_prop x} annotated_constraint : label
(annotated_type X annotation)
→ annotated_state X annotation *
option message → Prop annotated_transition_state : label
(annotated_type X
annotation)
→ annotated_state X
annotation *
option message
→ annotation AnnotatedX := constrained_vlsm
(annotated_vlsm X annotation
initial_annotation_prop
annotated_transition_state)
annotated_constraint : VLSM message
VLSM_embedding AnnotatedX X id original_state
Proof .message : Type X : VLSM message annotation : Type initial_annotation_prop : annotation → Prop H : Inhabited
{x : annotation | initial_annotation_prop x} annotated_constraint : label
(annotated_type X annotation)
→ annotated_state X annotation *
option message → Prop annotated_transition_state : label
(annotated_type X
annotation)
→ annotated_state X
annotation *
option message
→ annotation AnnotatedX := constrained_vlsm
(annotated_vlsm X annotation
initial_annotation_prop
annotated_transition_state)
annotated_constraint : VLSM message
VLSM_embedding AnnotatedX X id original_state
apply basic_VLSM_strong_embedding; cycle 1 ; [| by cbv ; itauto..].message : Type X : VLSM message annotation : Type initial_annotation_prop : annotation → Prop H : Inhabited
{x : annotation | initial_annotation_prop x} annotated_constraint : label
(annotated_type X annotation)
→ annotated_state X annotation *
option message → Prop annotated_transition_state : label
(annotated_type X
annotation)
→ annotated_state X
annotation *
option message
→ annotation AnnotatedX := constrained_vlsm
(annotated_vlsm X annotation
initial_annotation_prop
annotated_transition_state)
annotated_constraint : VLSM message
strong_embedding_transition_preservation AnnotatedX X
id original_state
intros l [s a] om [s' a'] om'.message : Type X : VLSM message annotation : Type initial_annotation_prop : annotation → Prop H : Inhabited
{x : annotation | initial_annotation_prop x} annotated_constraint : label
(annotated_type X annotation)
→ annotated_state X annotation *
option message → Prop annotated_transition_state : label
(annotated_type X
annotation)
→ annotated_state X
annotation *
option message
→ annotation AnnotatedX := constrained_vlsm
(annotated_vlsm X annotation
initial_annotation_prop
annotated_transition_state)
annotated_constraint : VLSM message l : label AnnotatedX s : state X a : annotation om : option message s' : state X a' : annotation om' : option message
transition l
({| original_state := s; state_annotation := a |},
om) =
({| original_state := s'; state_annotation := a' |},
om')
→ transition (id l)
(original_state
{|
original_state := s; state_annotation := a
|}, om) =
(original_state
{|
original_state := s'; state_annotation := a'
|}, om')
cbn ; unfold annotated_transition; cbn
; destruct (transition _ _ _) as (_s', _om').message : Type X : VLSM message annotation : Type initial_annotation_prop : annotation → Prop H : Inhabited
{x : annotation | initial_annotation_prop x} annotated_constraint : label
(annotated_type X annotation)
→ annotated_state X annotation *
option message → Prop annotated_transition_state : label
(annotated_type X
annotation)
→ annotated_state X
annotation *
option message
→ annotation AnnotatedX := constrained_vlsm
(annotated_vlsm X annotation
initial_annotation_prop
annotated_transition_state)
annotated_constraint : VLSM message l : label AnnotatedX s : state X a : annotation om : option message s' : state X a' : annotation om' : option message _s' : state X _om' : option message
({|
original_state := _s';
state_annotation :=
annotated_transition_state l
({|
original_state := s; state_annotation := a
|}, om)
|}, _om') =
({| original_state := s'; state_annotation := a' |},
om') → (_s', _om') = (s', om')
by inversion 1 .
Qed .
End sec_annotated_vlsm_projections .
Section sec_composite_annotated_vlsm_projections .
Specializing projection validator properties to annotated compositions
Context
{message : Type }
`{EqDecision index}
(IM : index -> VLSM message)
(Free := free_composite_vlsm IM)
{annotation : Type }
(initial_annotation_prop : annotation -> Prop )
`{Inhabited (sig initial_annotation_prop)}
(annotated_constraint :
label (annotated_type Free annotation) ->
annotated_state Free annotation * option message -> Prop )
(annotated_transition_state :
label (annotated_type Free annotation) ->
annotated_state Free annotation * option message -> annotation)
(AnnotatedFree : VLSM message :=
constrained_vlsm
(annotated_vlsm Free annotation initial_annotation_prop annotated_transition_state)
annotated_constraint)
(i : index)
.
Definition annotated_composite_label_project : label AnnotatedFree -> option (label (IM i))
:= composite_project_label IM i.
Definition annotated_composite_state_project : state AnnotatedFree -> state (IM i)
:= fun s => original_state s i.
Definition annotated_projection_validator_prop : Prop :=
projection_validator_prop (IM i)
annotated_composite_label_project annotated_composite_state_project.
Definition annotated_message_validator_prop : Prop :=
@message_validator_prop _ AnnotatedFree (IM i).
Definition annotated_composite_label_lift : label (IM i) -> label AnnotatedFree
:= lift_to_composite_label IM i.
Definition annotated_composite_state_lift : state (IM i) -> state AnnotatedFree
:= fun si =>
mk_annotated_state (free_composite_vlsm IM) _
(lift_to_composite_state' IM i si) (` inhabitant).
Definition annotated_projection_validator_prop_alt : Prop :=
projection_validator_prop_alt (IM i)
annotated_composite_label_project annotated_composite_state_project
annotated_composite_label_lift annotated_composite_state_lift.
Lemma preloaded_annotated_composite_preloaded_projection :
VLSM_projection
(preloaded_with_all_messages_vlsm AnnotatedFree)
(preloaded_with_all_messages_vlsm (IM i))
annotated_composite_label_project annotated_composite_state_project.message, index : Type EqDecision0 : EqDecision index IM : index → VLSM message Free := free_composite_vlsm IM : VLSM message annotation : Type initial_annotation_prop : annotation → Prop H : Inhabited
{x : annotation | initial_annotation_prop x} annotated_constraint : label
(annotated_type Free
annotation)
→ annotated_state Free
annotation * option message
→ Prop annotated_transition_state : label
(annotated_type Free
annotation)
→ annotated_state Free
annotation *
option message
→ annotation AnnotatedFree := constrained_vlsm
(annotated_vlsm Free annotation
initial_annotation_prop
annotated_transition_state)
annotated_constraint : VLSM message i : index
VLSM_projection
(preloaded_with_all_messages_vlsm AnnotatedFree)
(preloaded_with_all_messages_vlsm (IM i))
annotated_composite_label_project
annotated_composite_state_project
Proof .message, index : Type EqDecision0 : EqDecision index IM : index → VLSM message Free := free_composite_vlsm IM : VLSM message annotation : Type initial_annotation_prop : annotation → Prop H : Inhabited
{x : annotation | initial_annotation_prop x} annotated_constraint : label
(annotated_type Free
annotation)
→ annotated_state Free
annotation * option message
→ Prop annotated_transition_state : label
(annotated_type Free
annotation)
→ annotated_state Free
annotation *
option message
→ annotation AnnotatedFree := constrained_vlsm
(annotated_vlsm Free annotation
initial_annotation_prop
annotated_transition_state)
annotated_constraint : VLSM message i : index
VLSM_projection
(preloaded_with_all_messages_vlsm AnnotatedFree)
(preloaded_with_all_messages_vlsm (IM i))
annotated_composite_label_project
annotated_composite_state_project
apply basic_VLSM_projection.message, index : Type EqDecision0 : EqDecision index IM : index → VLSM message Free := free_composite_vlsm IM : VLSM message annotation : Type initial_annotation_prop : annotation → Prop H : Inhabited
{x : annotation | initial_annotation_prop x} annotated_constraint : label
(annotated_type Free
annotation)
→ annotated_state Free
annotation * option message
→ Prop annotated_transition_state : label
(annotated_type Free
annotation)
→ annotated_state Free
annotation *
option message
→ annotation AnnotatedFree := constrained_vlsm
(annotated_vlsm Free annotation
initial_annotation_prop
annotated_transition_state)
annotated_constraint : VLSM message i : index
weak_projection_valid_preservation
(preloaded_with_all_messages_vlsm AnnotatedFree)
(preloaded_with_all_messages_vlsm (IM i))
annotated_composite_label_project
annotated_composite_state_project
- message, index : Type EqDecision0 : EqDecision index IM : index → VLSM message Free := free_composite_vlsm IM : VLSM message annotation : Type initial_annotation_prop : annotation → Prop H : Inhabited
{x : annotation | initial_annotation_prop x} annotated_constraint : label
(annotated_type Free
annotation)
→ annotated_state Free
annotation * option message
→ Prop annotated_transition_state : label
(annotated_type Free
annotation)
→ annotated_state Free
annotation *
option message
→ annotation AnnotatedFree := constrained_vlsm
(annotated_vlsm Free annotation
initial_annotation_prop
annotated_transition_state)
annotated_constraint : VLSM message i : index
weak_projection_valid_preservation
(preloaded_with_all_messages_vlsm AnnotatedFree)
(preloaded_with_all_messages_vlsm (IM i))
annotated_composite_label_project
annotated_composite_state_project
intros [_i _li] li.message, index : Type EqDecision0 : EqDecision index IM : index → VLSM message Free := free_composite_vlsm IM : VLSM message annotation : Type initial_annotation_prop : annotation → Prop H : Inhabited
{x : annotation | initial_annotation_prop x} annotated_constraint : label
(annotated_type Free
annotation)
→ annotated_state Free
annotation * option message
→ Prop annotated_transition_state : label
(annotated_type Free
annotation)
→ annotated_state Free
annotation *
option message
→ annotation AnnotatedFree := constrained_vlsm
(annotated_vlsm Free annotation
initial_annotation_prop
annotated_transition_state)
annotated_constraint : VLSM message i, _i : index _li : label (IM _i) li : label (preloaded_with_all_messages_vlsm (IM i))
annotated_composite_label_project (existT _i _li) =
Some li
→ ∀ (s : state
(preloaded_with_all_messages_vlsm
AnnotatedFree)) (om : option message),
input_valid
(preloaded_with_all_messages_vlsm AnnotatedFree)
(existT _i _li) (s, om)
→ valid_state_prop
(preloaded_with_all_messages_vlsm (IM i))
(annotated_composite_state_project s)
→ option_valid_message_prop
(preloaded_with_all_messages_vlsm (IM i)) om
→ valid li
(annotated_composite_state_project s, om)
unfold annotated_composite_label_project, composite_project_label; cbn .message, index : Type EqDecision0 : EqDecision index IM : index → VLSM message Free := free_composite_vlsm IM : VLSM message annotation : Type initial_annotation_prop : annotation → Prop H : Inhabited
{x : annotation | initial_annotation_prop x} annotated_constraint : label
(annotated_type Free
annotation)
→ annotated_state Free
annotation * option message
→ Prop annotated_transition_state : label
(annotated_type Free
annotation)
→ annotated_state Free
annotation *
option message
→ annotation AnnotatedFree := constrained_vlsm
(annotated_vlsm Free annotation
initial_annotation_prop
annotated_transition_state)
annotated_constraint : VLSM message i, _i : index _li : label (IM _i) li : label (preloaded_with_all_messages_vlsm (IM i))
match decide (i = _i) with
| left e =>
Some (eq_rect_r (λ n : index, label (IM n)) _li e)
| right _ => None
end = Some li
→ ∀ (s : annotated_state Free annotation) (om : option
message),
valid_state_prop
(preloaded_with_all_messages_vlsm AnnotatedFree)
s
∧ option_valid_message_prop
(preloaded_with_all_messages_vlsm
AnnotatedFree) om
∧ valid _li (original_state s _i, om)
∧ annotated_constraint (existT _i _li) (s, om)
→ valid_state_prop
(preloaded_with_all_messages_vlsm (IM i))
(annotated_composite_state_project s)
→ option_valid_message_prop
(preloaded_with_all_messages_vlsm (IM i)) om
→ valid li
(annotated_composite_state_project s, om)
case_decide; [| congruence ]. message, index : Type EqDecision0 : EqDecision index IM : index → VLSM message Free := free_composite_vlsm IM : VLSM message annotation : Type initial_annotation_prop : annotation → Prop H : Inhabited
{x : annotation | initial_annotation_prop x} annotated_constraint : label
(annotated_type Free
annotation)
→ annotated_state Free
annotation * option message
→ Prop annotated_transition_state : label
(annotated_type Free
annotation)
→ annotated_state Free
annotation *
option message
→ annotation AnnotatedFree := constrained_vlsm
(annotated_vlsm Free annotation
initial_annotation_prop
annotated_transition_state)
annotated_constraint : VLSM message i, _i : index _li : label (IM _i) li : label (preloaded_with_all_messages_vlsm (IM i)) H0 : i = _i
Some (eq_rect_r (λ n : index, label (IM n)) _li H0) =
Some li
→ ∀ (s : annotated_state Free annotation) (om : option
message),
valid_state_prop
(preloaded_with_all_messages_vlsm AnnotatedFree)
s
∧ option_valid_message_prop
(preloaded_with_all_messages_vlsm
AnnotatedFree) om
∧ valid _li (original_state s _i, om)
∧ annotated_constraint (existT _i _li) (s, om)
→ valid_state_prop
(preloaded_with_all_messages_vlsm (IM i))
(annotated_composite_state_project s)
→ option_valid_message_prop
(preloaded_with_all_messages_vlsm (IM i)) om
→ valid li
(annotated_composite_state_project s, om)
subst _i; cbn ; inversion_clear 1 .message, index : Type EqDecision0 : EqDecision index IM : index → VLSM message Free := free_composite_vlsm IM : VLSM message annotation : Type initial_annotation_prop : annotation → Prop H : Inhabited
{x : annotation | initial_annotation_prop x} annotated_constraint : label
(annotated_type Free
annotation)
→ annotated_state Free
annotation * option message
→ Prop annotated_transition_state : label
(annotated_type Free
annotation)
→ annotated_state Free
annotation *
option message
→ annotation AnnotatedFree := constrained_vlsm
(annotated_vlsm Free annotation
initial_annotation_prop
annotated_transition_state)
annotated_constraint : VLSM message i : index _li : label (IM i) li : label (preloaded_with_all_messages_vlsm (IM i))
∀ (s : annotated_state Free annotation) (om : option
message),
valid_state_prop
(preloaded_with_all_messages_vlsm AnnotatedFree) s
∧ option_valid_message_prop
(preloaded_with_all_messages_vlsm AnnotatedFree)
om
∧ valid li (original_state s i, om)
∧ annotated_constraint (existT i li) (s, om)
→ valid_state_prop
(preloaded_with_all_messages_vlsm (IM i))
(annotated_composite_state_project s)
→ option_valid_message_prop
(preloaded_with_all_messages_vlsm (IM i)) om
→ valid li
(annotated_composite_state_project s, om)
by intros (s, ann) om (_ & _ & Hv & _) _ _.
- message, index : Type EqDecision0 : EqDecision index IM : index → VLSM message Free := free_composite_vlsm IM : VLSM message annotation : Type initial_annotation_prop : annotation → Prop H : Inhabited
{x : annotation | initial_annotation_prop x} annotated_constraint : label
(annotated_type Free
annotation)
→ annotated_state Free
annotation * option message
→ Prop annotated_transition_state : label
(annotated_type Free
annotation)
→ annotated_state Free
annotation *
option message
→ annotation AnnotatedFree := constrained_vlsm
(annotated_vlsm Free annotation
initial_annotation_prop
annotated_transition_state)
annotated_constraint : VLSM message i : index
weak_projection_transition_preservation_Some
(preloaded_with_all_messages_vlsm AnnotatedFree)
(preloaded_with_all_messages_vlsm (IM i))
annotated_composite_label_project
annotated_composite_state_project
intros [_i _li] li.message, index : Type EqDecision0 : EqDecision index IM : index → VLSM message Free := free_composite_vlsm IM : VLSM message annotation : Type initial_annotation_prop : annotation → Prop H : Inhabited
{x : annotation | initial_annotation_prop x} annotated_constraint : label
(annotated_type Free
annotation)
→ annotated_state Free
annotation * option message
→ Prop annotated_transition_state : label
(annotated_type Free
annotation)
→ annotated_state Free
annotation *
option message
→ annotation AnnotatedFree := constrained_vlsm
(annotated_vlsm Free annotation
initial_annotation_prop
annotated_transition_state)
annotated_constraint : VLSM message i, _i : index _li : label (IM _i) li : label (preloaded_with_all_messages_vlsm (IM i))
annotated_composite_label_project (existT _i _li) =
Some li
→ ∀ (s : state
(preloaded_with_all_messages_vlsm
AnnotatedFree)) (om : option message)
(s' : state
(preloaded_with_all_messages_vlsm
AnnotatedFree)) (om' : option message),
input_valid_transition
(preloaded_with_all_messages_vlsm AnnotatedFree)
(existT _i _li) (s, om) (s', om')
→ transition li
(annotated_composite_state_project s, om) =
(annotated_composite_state_project s', om')
unfold annotated_composite_label_project, composite_project_label; cbn .message, index : Type EqDecision0 : EqDecision index IM : index → VLSM message Free := free_composite_vlsm IM : VLSM message annotation : Type initial_annotation_prop : annotation → Prop H : Inhabited
{x : annotation | initial_annotation_prop x} annotated_constraint : label
(annotated_type Free
annotation)
→ annotated_state Free
annotation * option message
→ Prop annotated_transition_state : label
(annotated_type Free
annotation)
→ annotated_state Free
annotation *
option message
→ annotation AnnotatedFree := constrained_vlsm
(annotated_vlsm Free annotation
initial_annotation_prop
annotated_transition_state)
annotated_constraint : VLSM message i, _i : index _li : label (IM _i) li : label (preloaded_with_all_messages_vlsm (IM i))
match decide (i = _i) with
| left e =>
Some (eq_rect_r (λ n : index, label (IM n)) _li e)
| right _ => None
end = Some li
→ ∀ (s : annotated_state Free annotation) (om : option
message)
(s' : annotated_state Free annotation) (om' :
option
message),
input_valid_transition
(preloaded_with_all_messages_vlsm AnnotatedFree)
(existT _i _li) (s, om) (s', om')
→ transition li
(annotated_composite_state_project s, om) =
(annotated_composite_state_project s', om')
case_decide; [| congruence ]. message, index : Type EqDecision0 : EqDecision index IM : index → VLSM message Free := free_composite_vlsm IM : VLSM message annotation : Type initial_annotation_prop : annotation → Prop H : Inhabited
{x : annotation | initial_annotation_prop x} annotated_constraint : label
(annotated_type Free
annotation)
→ annotated_state Free
annotation * option message
→ Prop annotated_transition_state : label
(annotated_type Free
annotation)
→ annotated_state Free
annotation *
option message
→ annotation AnnotatedFree := constrained_vlsm
(annotated_vlsm Free annotation
initial_annotation_prop
annotated_transition_state)
annotated_constraint : VLSM message i, _i : index _li : label (IM _i) li : label (preloaded_with_all_messages_vlsm (IM i)) H0 : i = _i
Some (eq_rect_r (λ n : index, label (IM n)) _li H0) =
Some li
→ ∀ (s : annotated_state Free annotation) (om : option
message)
(s' : annotated_state Free annotation) (om' :
option
message),
input_valid_transition
(preloaded_with_all_messages_vlsm AnnotatedFree)
(existT _i _li) (s, om) (s', om')
→ transition li
(annotated_composite_state_project s, om) =
(annotated_composite_state_project s', om')
subst _i; cbn ; inversion_clear 1 .message, index : Type EqDecision0 : EqDecision index IM : index → VLSM message Free := free_composite_vlsm IM : VLSM message annotation : Type initial_annotation_prop : annotation → Prop H : Inhabited
{x : annotation | initial_annotation_prop x} annotated_constraint : label
(annotated_type Free
annotation)
→ annotated_state Free
annotation * option message
→ Prop annotated_transition_state : label
(annotated_type Free
annotation)
→ annotated_state Free
annotation *
option message
→ annotation AnnotatedFree := constrained_vlsm
(annotated_vlsm Free annotation
initial_annotation_prop
annotated_transition_state)
annotated_constraint : VLSM message i : index _li : label (IM i) li : label (preloaded_with_all_messages_vlsm (IM i))
∀ (s : annotated_state Free annotation) (om : option
message)
(s' : annotated_state Free annotation) (om' : option
message),
input_valid_transition
(preloaded_with_all_messages_vlsm AnnotatedFree)
(existT i li) (s, om) (s', om')
→ transition li
(annotated_composite_state_project s, om) =
(annotated_composite_state_project s', om')
intros [s ann] iom [s' ann'] oom.message, index : Type EqDecision0 : EqDecision index IM : index → VLSM message Free := free_composite_vlsm IM : VLSM message annotation : Type initial_annotation_prop : annotation → Prop H : Inhabited
{x : annotation | initial_annotation_prop x} annotated_constraint : label
(annotated_type Free
annotation)
→ annotated_state Free
annotation * option message
→ Prop annotated_transition_state : label
(annotated_type Free
annotation)
→ annotated_state Free
annotation *
option message
→ annotation AnnotatedFree := constrained_vlsm
(annotated_vlsm Free annotation
initial_annotation_prop
annotated_transition_state)
annotated_constraint : VLSM message i : index _li : label (IM i) li : label (preloaded_with_all_messages_vlsm (IM i)) s : state Free ann : annotation iom : option message s' : state Free ann' : annotation oom : option message
input_valid_transition
(preloaded_with_all_messages_vlsm AnnotatedFree)
(existT i li)
({| original_state := s; state_annotation := ann |},
iom)
({|
original_state := s'; state_annotation := ann'
|}, oom)
→ transition li
(annotated_composite_state_project
{|
original_state := s; state_annotation := ann
|}, iom) =
(annotated_composite_state_project
{|
original_state := s'; state_annotation := ann'
|}, oom)
unfold input_valid_transition; cbn
; unfold annotated_transition; cbn
; destruct (transition _ _ _) as (si', om').message, index : Type EqDecision0 : EqDecision index IM : index → VLSM message Free := free_composite_vlsm IM : VLSM message annotation : Type initial_annotation_prop : annotation → Prop H : Inhabited
{x : annotation | initial_annotation_prop x} annotated_constraint : label
(annotated_type Free
annotation)
→ annotated_state Free
annotation * option message
→ Prop annotated_transition_state : label
(annotated_type Free
annotation)
→ annotated_state Free
annotation *
option message
→ annotation AnnotatedFree := constrained_vlsm
(annotated_vlsm Free annotation
initial_annotation_prop
annotated_transition_state)
annotated_constraint : VLSM message i : index _li : label (IM i) li : label (preloaded_with_all_messages_vlsm (IM i)) s : state Free ann : annotation iom : option message s' : state Free ann' : annotation oom : option message si' : state (IM i) om' : option message
(valid_state_prop
(preloaded_with_all_messages_vlsm AnnotatedFree)
{| original_state := s; state_annotation := ann |}
∧ option_valid_message_prop
(preloaded_with_all_messages_vlsm AnnotatedFree)
iom
∧ valid li (s i, iom)
∧ annotated_constraint (existT i li)
({|
original_state := s;
state_annotation := ann
|}, iom))
∧ ({|
original_state := state_update IM s i si';
state_annotation :=
annotated_transition_state (existT i li)
({|
original_state := s;
state_annotation := ann
|}, iom)
|}, om') =
({|
original_state := s'; state_annotation := ann'
|}, oom) → (si', om') = (s' i, oom)
intros [_ Ht]; inversion Ht.message, index : Type EqDecision0 : EqDecision index IM : index → VLSM message Free := free_composite_vlsm IM : VLSM message annotation : Type initial_annotation_prop : annotation → Prop H : Inhabited
{x : annotation | initial_annotation_prop x} annotated_constraint : label
(annotated_type Free
annotation)
→ annotated_state Free
annotation * option message
→ Prop annotated_transition_state : label
(annotated_type Free
annotation)
→ annotated_state Free
annotation *
option message
→ annotation AnnotatedFree := constrained_vlsm
(annotated_vlsm Free annotation
initial_annotation_prop
annotated_transition_state)
annotated_constraint : VLSM message i : index _li : label (IM i) li : label (preloaded_with_all_messages_vlsm (IM i)) s : state Free ann : annotation iom : option message s' : state Free ann' : annotation oom : option message si' : state (IM i) om' : option message Ht : ({|
original_state := state_update IM s i si';
state_annotation :=
annotated_transition_state
(existT i li)
({|
original_state := s;
state_annotation := ann
|}, iom)
|}, om') =
({|
original_state := s'; state_annotation := ann'
|}, oom) H1 : state_update IM s i si' = s' H2 : annotated_transition_state
(existT i li)
({|
original_state := s; state_annotation := ann
|}, iom) = ann' H3 : om' = oom
(si', oom) = (state_update IM s i si' i, oom)
by state_update_simpl.
- message, index : Type EqDecision0 : EqDecision index IM : index → VLSM message Free := free_composite_vlsm IM : VLSM message annotation : Type initial_annotation_prop : annotation → Prop H : Inhabited
{x : annotation | initial_annotation_prop x} annotated_constraint : label
(annotated_type Free
annotation)
→ annotated_state Free
annotation * option message
→ Prop annotated_transition_state : label
(annotated_type Free
annotation)
→ annotated_state Free
annotation *
option message
→ annotation AnnotatedFree := constrained_vlsm
(annotated_vlsm Free annotation
initial_annotation_prop
annotated_transition_state)
annotated_constraint : VLSM message i : index
weak_projection_transition_consistency_None
(preloaded_with_all_messages_vlsm AnnotatedFree)
(preloaded_with_all_messages_vlsm (IM i))
annotated_composite_label_project
annotated_composite_state_project
intros [j lj].message, index : Type EqDecision0 : EqDecision index IM : index → VLSM message Free := free_composite_vlsm IM : VLSM message annotation : Type initial_annotation_prop : annotation → Prop H : Inhabited
{x : annotation | initial_annotation_prop x} annotated_constraint : label
(annotated_type Free
annotation)
→ annotated_state Free
annotation * option message
→ Prop annotated_transition_state : label
(annotated_type Free
annotation)
→ annotated_state Free
annotation *
option message
→ annotation AnnotatedFree := constrained_vlsm
(annotated_vlsm Free annotation
initial_annotation_prop
annotated_transition_state)
annotated_constraint : VLSM message i, j : index lj : label (IM j)
annotated_composite_label_project (existT j lj) = None
→ ∀ (s : state
(preloaded_with_all_messages_vlsm
AnnotatedFree)) (om : option message)
(s' : state
(preloaded_with_all_messages_vlsm
AnnotatedFree)) (om' : option message),
input_valid_transition
(preloaded_with_all_messages_vlsm AnnotatedFree)
(existT j lj) (s, om) (s', om')
→ annotated_composite_state_project s' =
annotated_composite_state_project s
unfold annotated_composite_label_project, composite_project_label; cbn .message, index : Type EqDecision0 : EqDecision index IM : index → VLSM message Free := free_composite_vlsm IM : VLSM message annotation : Type initial_annotation_prop : annotation → Prop H : Inhabited
{x : annotation | initial_annotation_prop x} annotated_constraint : label
(annotated_type Free
annotation)
→ annotated_state Free
annotation * option message
→ Prop annotated_transition_state : label
(annotated_type Free
annotation)
→ annotated_state Free
annotation *
option message
→ annotation AnnotatedFree := constrained_vlsm
(annotated_vlsm Free annotation
initial_annotation_prop
annotated_transition_state)
annotated_constraint : VLSM message i, j : index lj : label (IM j)
match decide (i = j) with
| left e =>
Some (eq_rect_r (λ n : index, label (IM n)) lj e)
| right _ => None
end = None
→ ∀ (s : annotated_state Free annotation) (om : option
message)
(s' : annotated_state Free annotation) (om' :
option
message),
input_valid_transition
(preloaded_with_all_messages_vlsm AnnotatedFree)
(existT j lj) (s, om) (s', om')
→ annotated_composite_state_project s' =
annotated_composite_state_project s
case_decide as Hij; [by congruence |]. message, index : Type EqDecision0 : EqDecision index IM : index → VLSM message Free := free_composite_vlsm IM : VLSM message annotation : Type initial_annotation_prop : annotation → Prop H : Inhabited
{x : annotation | initial_annotation_prop x} annotated_constraint : label
(annotated_type Free
annotation)
→ annotated_state Free
annotation * option message
→ Prop annotated_transition_state : label
(annotated_type Free
annotation)
→ annotated_state Free
annotation *
option message
→ annotation AnnotatedFree := constrained_vlsm
(annotated_vlsm Free annotation
initial_annotation_prop
annotated_transition_state)
annotated_constraint : VLSM message i, j : index lj : label (IM j) Hij : i ≠ j
None = None
→ ∀ (s : annotated_state Free annotation) (om : option
message)
(s' : annotated_state Free annotation) (om' :
option
message),
input_valid_transition
(preloaded_with_all_messages_vlsm AnnotatedFree)
(existT j lj) (s, om) (s', om')
→ annotated_composite_state_project s' =
annotated_composite_state_project s
intros _ [s ann] iom [s' ann'] oom.message, index : Type EqDecision0 : EqDecision index IM : index → VLSM message Free := free_composite_vlsm IM : VLSM message annotation : Type initial_annotation_prop : annotation → Prop H : Inhabited
{x : annotation | initial_annotation_prop x} annotated_constraint : label
(annotated_type Free
annotation)
→ annotated_state Free
annotation * option message
→ Prop annotated_transition_state : label
(annotated_type Free
annotation)
→ annotated_state Free
annotation *
option message
→ annotation AnnotatedFree := constrained_vlsm
(annotated_vlsm Free annotation
initial_annotation_prop
annotated_transition_state)
annotated_constraint : VLSM message i, j : index lj : label (IM j) Hij : i ≠ j s : state Free ann : annotation iom : option message s' : state Free ann' : annotation oom : option message
input_valid_transition
(preloaded_with_all_messages_vlsm AnnotatedFree)
(existT j lj)
({| original_state := s; state_annotation := ann |},
iom)
({|
original_state := s'; state_annotation := ann'
|}, oom)
→ annotated_composite_state_project
{|
original_state := s'; state_annotation := ann'
|} =
annotated_composite_state_project
{| original_state := s; state_annotation := ann |}
unfold input_valid_transition; cbn
; unfold annotated_transition; cbn
; destruct (transition _ _ _) as (si', om').message, index : Type EqDecision0 : EqDecision index IM : index → VLSM message Free := free_composite_vlsm IM : VLSM message annotation : Type initial_annotation_prop : annotation → Prop H : Inhabited
{x : annotation | initial_annotation_prop x} annotated_constraint : label
(annotated_type Free
annotation)
→ annotated_state Free
annotation * option message
→ Prop annotated_transition_state : label
(annotated_type Free
annotation)
→ annotated_state Free
annotation *
option message
→ annotation AnnotatedFree := constrained_vlsm
(annotated_vlsm Free annotation
initial_annotation_prop
annotated_transition_state)
annotated_constraint : VLSM message i, j : index lj : label (IM j) Hij : i ≠ j s : state Free ann : annotation iom : option message s' : state Free ann' : annotation oom : option message si' : state (IM j) om' : option message
(valid_state_prop
(preloaded_with_all_messages_vlsm AnnotatedFree)
{| original_state := s; state_annotation := ann |}
∧ option_valid_message_prop
(preloaded_with_all_messages_vlsm AnnotatedFree)
iom
∧ valid lj (s j, iom)
∧ annotated_constraint (existT j lj)
({|
original_state := s;
state_annotation := ann
|}, iom))
∧ ({|
original_state := state_update IM s j si';
state_annotation :=
annotated_transition_state (existT j lj)
({|
original_state := s;
state_annotation := ann
|}, iom)
|}, om') =
({|
original_state := s'; state_annotation := ann'
|}, oom) → s' i = s i
intros [_ Ht]; inversion Ht.message, index : Type EqDecision0 : EqDecision index IM : index → VLSM message Free := free_composite_vlsm IM : VLSM message annotation : Type initial_annotation_prop : annotation → Prop H : Inhabited
{x : annotation | initial_annotation_prop x} annotated_constraint : label
(annotated_type Free
annotation)
→ annotated_state Free
annotation * option message
→ Prop annotated_transition_state : label
(annotated_type Free
annotation)
→ annotated_state Free
annotation *
option message
→ annotation AnnotatedFree := constrained_vlsm
(annotated_vlsm Free annotation
initial_annotation_prop
annotated_transition_state)
annotated_constraint : VLSM message i, j : index lj : label (IM j) Hij : i ≠ j s : state Free ann : annotation iom : option message s' : state Free ann' : annotation oom : option message si' : state (IM j) om' : option message Ht : ({|
original_state := state_update IM s j si';
state_annotation :=
annotated_transition_state
(existT j lj)
({|
original_state := s;
state_annotation := ann
|}, iom)
|}, om') =
({|
original_state := s'; state_annotation := ann'
|}, oom) H1 : state_update IM s j si' = s' H2 : annotated_transition_state
(existT j lj)
({|
original_state := s; state_annotation := ann
|}, iom) = ann' H3 : om' = oom
state_update IM s j si' i = s i
by state_update_simpl.
- message, index : Type EqDecision0 : EqDecision index IM : index → VLSM message Free := free_composite_vlsm IM : VLSM message annotation : Type initial_annotation_prop : annotation → Prop H : Inhabited
{x : annotation | initial_annotation_prop x} annotated_constraint : label
(annotated_type Free
annotation)
→ annotated_state Free
annotation * option message
→ Prop annotated_transition_state : label
(annotated_type Free
annotation)
→ annotated_state Free
annotation *
option message
→ annotation AnnotatedFree := constrained_vlsm
(annotated_vlsm Free annotation
initial_annotation_prop
annotated_transition_state)
annotated_constraint : VLSM message i : index
strong_projection_initial_state_preservation
(preloaded_with_all_messages_vlsm AnnotatedFree)
(preloaded_with_all_messages_vlsm (IM i))
annotated_composite_state_project
by intros [s ann] [Hs _]; cbn ; apply Hs.
- message, index : Type EqDecision0 : EqDecision index IM : index → VLSM message Free := free_composite_vlsm IM : VLSM message annotation : Type initial_annotation_prop : annotation → Prop H : Inhabited
{x : annotation | initial_annotation_prop x} annotated_constraint : label
(annotated_type Free
annotation)
→ annotated_state Free
annotation * option message
→ Prop annotated_transition_state : label
(annotated_type Free
annotation)
→ annotated_state Free
annotation *
option message
→ annotation AnnotatedFree := constrained_vlsm
(annotated_vlsm Free annotation
initial_annotation_prop
annotated_transition_state)
annotated_constraint : VLSM message i : index
weak_projection_valid_message_preservation
(preloaded_with_all_messages_vlsm AnnotatedFree)
(preloaded_with_all_messages_vlsm (IM i))
annotated_composite_label_project
annotated_composite_state_project
by intro ; intros ; apply any_message_is_valid_in_preloaded.
Qed .
Lemma annotated_composite_preloaded_projection :
VLSM_projection AnnotatedFree (preloaded_with_all_messages_vlsm (IM i))
annotated_composite_label_project annotated_composite_state_project.message, index : Type EqDecision0 : EqDecision index IM : index → VLSM message Free := free_composite_vlsm IM : VLSM message annotation : Type initial_annotation_prop : annotation → Prop H : Inhabited
{x : annotation | initial_annotation_prop x} annotated_constraint : label
(annotated_type Free
annotation)
→ annotated_state Free
annotation * option message
→ Prop annotated_transition_state : label
(annotated_type Free
annotation)
→ annotated_state Free
annotation *
option message
→ annotation AnnotatedFree := constrained_vlsm
(annotated_vlsm Free annotation
initial_annotation_prop
annotated_transition_state)
annotated_constraint : VLSM message i : index
VLSM_projection AnnotatedFree
(preloaded_with_all_messages_vlsm (IM i))
annotated_composite_label_project
annotated_composite_state_project
Proof .message, index : Type EqDecision0 : EqDecision index IM : index → VLSM message Free := free_composite_vlsm IM : VLSM message annotation : Type initial_annotation_prop : annotation → Prop H : Inhabited
{x : annotation | initial_annotation_prop x} annotated_constraint : label
(annotated_type Free
annotation)
→ annotated_state Free
annotation * option message
→ Prop annotated_transition_state : label
(annotated_type Free
annotation)
→ annotated_state Free
annotation *
option message
→ annotation AnnotatedFree := constrained_vlsm
(annotated_vlsm Free annotation
initial_annotation_prop
annotated_transition_state)
annotated_constraint : VLSM message i : index
VLSM_projection AnnotatedFree
(preloaded_with_all_messages_vlsm (IM i))
annotated_composite_label_project
annotated_composite_state_project
apply @VLSM_incl_projection_trans
with (MY := (preloaded_with_all_messages_vlsm AnnotatedFree)).message, index : Type EqDecision0 : EqDecision index IM : index → VLSM message Free := free_composite_vlsm IM : VLSM message annotation : Type initial_annotation_prop : annotation → Prop H : Inhabited
{x : annotation | initial_annotation_prop x} annotated_constraint : label
(annotated_type Free
annotation)
→ annotated_state Free
annotation * option message
→ Prop annotated_transition_state : label
(annotated_type Free
annotation)
→ annotated_state Free
annotation *
option message
→ annotation AnnotatedFree := constrained_vlsm
(annotated_vlsm Free annotation
initial_annotation_prop
annotated_transition_state)
annotated_constraint : VLSM message i : index
VLSM_incl
{|
vlsm_type :=
preloaded_with_all_messages_vlsm AnnotatedFree;
vlsm_machine :=
constrained_vlsm_machine
(annotated_vlsm Free annotation
initial_annotation_prop
annotated_transition_state)
annotated_constraint
|}
{|
vlsm_type :=
preloaded_with_all_messages_vlsm AnnotatedFree;
vlsm_machine :=
preloaded_with_all_messages_vlsm AnnotatedFree
|}
- message, index : Type EqDecision0 : EqDecision index IM : index → VLSM message Free := free_composite_vlsm IM : VLSM message annotation : Type initial_annotation_prop : annotation → Prop H : Inhabited
{x : annotation | initial_annotation_prop x} annotated_constraint : label
(annotated_type Free
annotation)
→ annotated_state Free
annotation * option message
→ Prop annotated_transition_state : label
(annotated_type Free
annotation)
→ annotated_state Free
annotation *
option message
→ annotation AnnotatedFree := constrained_vlsm
(annotated_vlsm Free annotation
initial_annotation_prop
annotated_transition_state)
annotated_constraint : VLSM message i : index
VLSM_incl
{|
vlsm_type :=
preloaded_with_all_messages_vlsm AnnotatedFree;
vlsm_machine :=
constrained_vlsm_machine
(annotated_vlsm Free annotation
initial_annotation_prop
annotated_transition_state)
annotated_constraint
|}
{|
vlsm_type :=
preloaded_with_all_messages_vlsm AnnotatedFree;
vlsm_machine :=
preloaded_with_all_messages_vlsm AnnotatedFree
|}
by apply (vlsm_incl_preloaded_with_all_messages_vlsm AnnotatedFree).
- message, index : Type EqDecision0 : EqDecision index IM : index → VLSM message Free := free_composite_vlsm IM : VLSM message annotation : Type initial_annotation_prop : annotation → Prop H : Inhabited
{x : annotation | initial_annotation_prop x} annotated_constraint : label
(annotated_type Free
annotation)
→ annotated_state Free
annotation * option message
→ Prop annotated_transition_state : label
(annotated_type Free
annotation)
→ annotated_state Free
annotation *
option message
→ annotation AnnotatedFree := constrained_vlsm
(annotated_vlsm Free annotation
initial_annotation_prop
annotated_transition_state)
annotated_constraint : VLSM message i : index
VLSM_projection
{|
vlsm_type :=
preloaded_with_all_messages_vlsm AnnotatedFree;
vlsm_machine :=
preloaded_with_all_messages_vlsm AnnotatedFree
|} (preloaded_with_all_messages_vlsm (IM i))
annotated_composite_label_project
annotated_composite_state_project
by apply preloaded_annotated_composite_preloaded_projection.
Qed .
Definition annotated_composite_induced_validator : VLSM message
:= projection_induced_validator AnnotatedFree (IM i)
annotated_composite_label_project annotated_composite_state_project
annotated_composite_label_lift annotated_composite_state_lift.
Lemma annotated_composite_induced_validator_transition_None :
weak_projection_transition_consistency_None _ _ annotated_composite_label_project
annotated_composite_state_project.message, index : Type EqDecision0 : EqDecision index IM : index → VLSM message Free := free_composite_vlsm IM : VLSM message annotation : Type initial_annotation_prop : annotation → Prop H : Inhabited
{x : annotation | initial_annotation_prop x} annotated_constraint : label
(annotated_type Free
annotation)
→ annotated_state Free
annotation * option message
→ Prop annotated_transition_state : label
(annotated_type Free
annotation)
→ annotated_state Free
annotation *
option message
→ annotation AnnotatedFree := constrained_vlsm
(annotated_vlsm Free annotation
initial_annotation_prop
annotated_transition_state)
annotated_constraint : VLSM message i : index
weak_projection_transition_consistency_None
AnnotatedFree (IM i)
annotated_composite_label_project
annotated_composite_state_project
Proof .message, index : Type EqDecision0 : EqDecision index IM : index → VLSM message Free := free_composite_vlsm IM : VLSM message annotation : Type initial_annotation_prop : annotation → Prop H : Inhabited
{x : annotation | initial_annotation_prop x} annotated_constraint : label
(annotated_type Free
annotation)
→ annotated_state Free
annotation * option message
→ Prop annotated_transition_state : label
(annotated_type Free
annotation)
→ annotated_state Free
annotation *
option message
→ annotation AnnotatedFree := constrained_vlsm
(annotated_vlsm Free annotation
initial_annotation_prop
annotated_transition_state)
annotated_constraint : VLSM message i : index
weak_projection_transition_consistency_None
AnnotatedFree (IM i)
annotated_composite_label_project
annotated_composite_state_project
intros [j lj].message, index : Type EqDecision0 : EqDecision index IM : index → VLSM message Free := free_composite_vlsm IM : VLSM message annotation : Type initial_annotation_prop : annotation → Prop H : Inhabited
{x : annotation | initial_annotation_prop x} annotated_constraint : label
(annotated_type Free
annotation)
→ annotated_state Free
annotation * option message
→ Prop annotated_transition_state : label
(annotated_type Free
annotation)
→ annotated_state Free
annotation *
option message
→ annotation AnnotatedFree := constrained_vlsm
(annotated_vlsm Free annotation
initial_annotation_prop
annotated_transition_state)
annotated_constraint : VLSM message i, j : index lj : label (IM j)
annotated_composite_label_project (existT j lj) = None
→ ∀ (s : state AnnotatedFree) (om : option message)
(s' : state AnnotatedFree) (om' : option message),
input_valid_transition AnnotatedFree (existT j lj)
(s, om) (s', om')
→ annotated_composite_state_project s' =
annotated_composite_state_project s
unfold annotated_composite_label_project, composite_project_label; cbn .message, index : Type EqDecision0 : EqDecision index IM : index → VLSM message Free := free_composite_vlsm IM : VLSM message annotation : Type initial_annotation_prop : annotation → Prop H : Inhabited
{x : annotation | initial_annotation_prop x} annotated_constraint : label
(annotated_type Free
annotation)
→ annotated_state Free
annotation * option message
→ Prop annotated_transition_state : label
(annotated_type Free
annotation)
→ annotated_state Free
annotation *
option message
→ annotation AnnotatedFree := constrained_vlsm
(annotated_vlsm Free annotation
initial_annotation_prop
annotated_transition_state)
annotated_constraint : VLSM message i, j : index lj : label (IM j)
match decide (i = j) with
| left e =>
Some (eq_rect_r (λ n : index, label (IM n)) lj e)
| right _ => None
end = None
→ ∀ (s : annotated_state Free annotation) (om : option
message)
(s' : annotated_state Free annotation) (om' :
option
message),
input_valid_transition AnnotatedFree (existT j lj)
(s, om) (s', om')
→ annotated_composite_state_project s' =
annotated_composite_state_project s
case_decide as Hij; [by congruence |]. message, index : Type EqDecision0 : EqDecision index IM : index → VLSM message Free := free_composite_vlsm IM : VLSM message annotation : Type initial_annotation_prop : annotation → Prop H : Inhabited
{x : annotation | initial_annotation_prop x} annotated_constraint : label
(annotated_type Free
annotation)
→ annotated_state Free
annotation * option message
→ Prop annotated_transition_state : label
(annotated_type Free
annotation)
→ annotated_state Free
annotation *
option message
→ annotation AnnotatedFree := constrained_vlsm
(annotated_vlsm Free annotation
initial_annotation_prop
annotated_transition_state)
annotated_constraint : VLSM message i, j : index lj : label (IM j) Hij : i ≠ j
None = None
→ ∀ (s : annotated_state Free annotation) (om : option
message)
(s' : annotated_state Free annotation) (om' :
option
message),
input_valid_transition AnnotatedFree (existT j lj)
(s, om) (s', om')
→ annotated_composite_state_project s' =
annotated_composite_state_project s
intros _ sX omX s'X om'X [_ Ht]; revert Ht; cbn .message, index : Type EqDecision0 : EqDecision index IM : index → VLSM message Free := free_composite_vlsm IM : VLSM message annotation : Type initial_annotation_prop : annotation → Prop H : Inhabited
{x : annotation | initial_annotation_prop x} annotated_constraint : label
(annotated_type Free
annotation)
→ annotated_state Free
annotation * option message
→ Prop annotated_transition_state : label
(annotated_type Free
annotation)
→ annotated_state Free
annotation *
option message
→ annotation AnnotatedFree := constrained_vlsm
(annotated_vlsm Free annotation
initial_annotation_prop
annotated_transition_state)
annotated_constraint : VLSM message i, j : index lj : label (IM j) Hij : i ≠ j sX : annotated_state Free annotation omX : option message s'X : annotated_state Free annotation om'X : option message
annotated_transition Free annotation
annotated_transition_state (existT j lj) (sX, omX) =
(s'X, om'X)
→ annotated_composite_state_project s'X =
annotated_composite_state_project sX
unfold annotated_transition; cbn
; destruct (transition _ _ _) as (si', om')
; inversion 1 ; clear Ht; subst om' s'X; cbn .message, index : Type EqDecision0 : EqDecision index IM : index → VLSM message Free := free_composite_vlsm IM : VLSM message annotation : Type initial_annotation_prop : annotation → Prop H : Inhabited
{x : annotation | initial_annotation_prop x} annotated_constraint : label
(annotated_type Free
annotation)
→ annotated_state Free
annotation * option message
→ Prop annotated_transition_state : label
(annotated_type Free
annotation)
→ annotated_state Free
annotation *
option message
→ annotation AnnotatedFree := constrained_vlsm
(annotated_vlsm Free annotation
initial_annotation_prop
annotated_transition_state)
annotated_constraint : VLSM message i, j : index lj : label (IM j) Hij : i ≠ j sX : annotated_state Free annotation omX, om'X : option message si' : state (IM j)
state_update IM (original_state sX) j si' i =
annotated_composite_state_project sX
by state_update_simpl.
Qed .
Lemma annotated_composite_induced_validator_label_lift
: induced_validator_label_lift_prop annotated_composite_label_project annotated_composite_label_lift.message, index : Type EqDecision0 : EqDecision index IM : index → VLSM message Free := free_composite_vlsm IM : VLSM message annotation : Type initial_annotation_prop : annotation → Prop H : Inhabited
{x : annotation | initial_annotation_prop x} annotated_constraint : label
(annotated_type Free
annotation)
→ annotated_state Free
annotation * option message
→ Prop annotated_transition_state : label
(annotated_type Free
annotation)
→ annotated_state Free
annotation *
option message
→ annotation AnnotatedFree := constrained_vlsm
(annotated_vlsm Free annotation
initial_annotation_prop
annotated_transition_state)
annotated_constraint : VLSM message i : index
induced_validator_label_lift_prop
annotated_composite_label_project
annotated_composite_label_lift
Proof .message, index : Type EqDecision0 : EqDecision index IM : index → VLSM message Free := free_composite_vlsm IM : VLSM message annotation : Type initial_annotation_prop : annotation → Prop H : Inhabited
{x : annotation | initial_annotation_prop x} annotated_constraint : label
(annotated_type Free
annotation)
→ annotated_state Free
annotation * option message
→ Prop annotated_transition_state : label
(annotated_type Free
annotation)
→ annotated_state Free
annotation *
option message
→ annotation AnnotatedFree := constrained_vlsm
(annotated_vlsm Free annotation
initial_annotation_prop
annotated_transition_state)
annotated_constraint : VLSM message i : index
induced_validator_label_lift_prop
annotated_composite_label_project
annotated_composite_label_lift
by apply component_label_projection_lift. Qed .
Lemma annotated_composite_induced_validator_state_lift
: induced_validator_state_lift_prop annotated_composite_state_project annotated_composite_state_lift.message, index : Type EqDecision0 : EqDecision index IM : index → VLSM message Free := free_composite_vlsm IM : VLSM message annotation : Type initial_annotation_prop : annotation → Prop H : Inhabited
{x : annotation | initial_annotation_prop x} annotated_constraint : label
(annotated_type Free
annotation)
→ annotated_state Free
annotation * option message
→ Prop annotated_transition_state : label
(annotated_type Free
annotation)
→ annotated_state Free
annotation *
option message
→ annotation AnnotatedFree := constrained_vlsm
(annotated_vlsm Free annotation
initial_annotation_prop
annotated_transition_state)
annotated_constraint : VLSM message i : index
induced_validator_state_lift_prop
annotated_composite_state_project
annotated_composite_state_lift
Proof .message, index : Type EqDecision0 : EqDecision index IM : index → VLSM message Free := free_composite_vlsm IM : VLSM message annotation : Type initial_annotation_prop : annotation → Prop H : Inhabited
{x : annotation | initial_annotation_prop x} annotated_constraint : label
(annotated_type Free
annotation)
→ annotated_state Free
annotation * option message
→ Prop annotated_transition_state : label
(annotated_type Free
annotation)
→ annotated_state Free
annotation *
option message
→ annotation AnnotatedFree := constrained_vlsm
(annotated_vlsm Free annotation
initial_annotation_prop
annotated_transition_state)
annotated_constraint : VLSM message i : index
induced_validator_state_lift_prop
annotated_composite_state_project
annotated_composite_state_lift
by intros si; apply state_update_eq. Qed .
Lemma annotated_composite_induced_validator_initial_lift
: strong_projection_initial_state_preservation (IM i) AnnotatedFree
annotated_composite_state_lift.message, index : Type EqDecision0 : EqDecision index IM : index → VLSM message Free := free_composite_vlsm IM : VLSM message annotation : Type initial_annotation_prop : annotation → Prop H : Inhabited
{x : annotation | initial_annotation_prop x} annotated_constraint : label
(annotated_type Free
annotation)
→ annotated_state Free
annotation * option message
→ Prop annotated_transition_state : label
(annotated_type Free
annotation)
→ annotated_state Free
annotation *
option message
→ annotation AnnotatedFree := constrained_vlsm
(annotated_vlsm Free annotation
initial_annotation_prop
annotated_transition_state)
annotated_constraint : VLSM message i : index
strong_projection_initial_state_preservation (IM i)
AnnotatedFree annotated_composite_state_lift
Proof .message, index : Type EqDecision0 : EqDecision index IM : index → VLSM message Free := free_composite_vlsm IM : VLSM message annotation : Type initial_annotation_prop : annotation → Prop H : Inhabited
{x : annotation | initial_annotation_prop x} annotated_constraint : label
(annotated_type Free
annotation)
→ annotated_state Free
annotation * option message
→ Prop annotated_transition_state : label
(annotated_type Free
annotation)
→ annotated_state Free
annotation *
option message
→ annotation AnnotatedFree := constrained_vlsm
(annotated_vlsm Free annotation
initial_annotation_prop
annotated_transition_state)
annotated_constraint : VLSM message i : index
strong_projection_initial_state_preservation (IM i)
AnnotatedFree annotated_composite_state_lift
split ; cbn .message, index : Type EqDecision0 : EqDecision index IM : index → VLSM message Free := free_composite_vlsm IM : VLSM message annotation : Type initial_annotation_prop : annotation → Prop H : Inhabited
{x : annotation | initial_annotation_prop x} annotated_constraint : label
(annotated_type Free
annotation)
→ annotated_state Free
annotation * option message
→ Prop annotated_transition_state : label
(annotated_type Free
annotation)
→ annotated_state Free
annotation *
option message
→ annotation AnnotatedFree := constrained_vlsm
(annotated_vlsm Free annotation
initial_annotation_prop
annotated_transition_state)
annotated_constraint : VLSM message i : index s : state (IM i) H0 : initial_state_prop s
composite_initial_state_prop IM
(lift_to_composite_state' IM i s)
- message, index : Type EqDecision0 : EqDecision index IM : index → VLSM message Free := free_composite_vlsm IM : VLSM message annotation : Type initial_annotation_prop : annotation → Prop H : Inhabited
{x : annotation | initial_annotation_prop x} annotated_constraint : label
(annotated_type Free
annotation)
→ annotated_state Free
annotation * option message
→ Prop annotated_transition_state : label
(annotated_type Free
annotation)
→ annotated_state Free
annotation *
option message
→ annotation AnnotatedFree := constrained_vlsm
(annotated_vlsm Free annotation
initial_annotation_prop
annotated_transition_state)
annotated_constraint : VLSM message i : index s : state (IM i) H0 : initial_state_prop s
composite_initial_state_prop IM
(lift_to_composite_state' IM i s)
by apply composite_initial_state_prop_lift.
- message, index : Type EqDecision0 : EqDecision index IM : index → VLSM message Free := free_composite_vlsm IM : VLSM message annotation : Type initial_annotation_prop : annotation → Prop H : Inhabited
{x : annotation | initial_annotation_prop x} annotated_constraint : label
(annotated_type Free
annotation)
→ annotated_state Free
annotation * option message
→ Prop annotated_transition_state : label
(annotated_type Free
annotation)
→ annotated_state Free
annotation *
option message
→ annotation AnnotatedFree := constrained_vlsm
(annotated_vlsm Free annotation
initial_annotation_prop
annotated_transition_state)
annotated_constraint : VLSM message i : index s : state (IM i) H0 : initial_state_prop s
initial_annotation_prop (`inhabitant)
by destruct inhabitant.
Qed .
Lemma annotated_composite_induced_validator_transition_consistency
: induced_validator_transition_consistency_Some _ _
annotated_composite_label_project annotated_composite_state_project.message, index : Type EqDecision0 : EqDecision index IM : index → VLSM message Free := free_composite_vlsm IM : VLSM message annotation : Type initial_annotation_prop : annotation → Prop H : Inhabited
{x : annotation | initial_annotation_prop x} annotated_constraint : label
(annotated_type Free
annotation)
→ annotated_state Free
annotation * option message
→ Prop annotated_transition_state : label
(annotated_type Free
annotation)
→ annotated_state Free
annotation *
option message
→ annotation AnnotatedFree := constrained_vlsm
(annotated_vlsm Free annotation
initial_annotation_prop
annotated_transition_state)
annotated_constraint : VLSM message i : index
induced_validator_transition_consistency_Some
AnnotatedFree (IM i)
annotated_composite_label_project
annotated_composite_state_project
Proof .message, index : Type EqDecision0 : EqDecision index IM : index → VLSM message Free := free_composite_vlsm IM : VLSM message annotation : Type initial_annotation_prop : annotation → Prop H : Inhabited
{x : annotation | initial_annotation_prop x} annotated_constraint : label
(annotated_type Free
annotation)
→ annotated_state Free
annotation * option message
→ Prop annotated_transition_state : label
(annotated_type Free
annotation)
→ annotated_state Free
annotation *
option message
→ annotation AnnotatedFree := constrained_vlsm
(annotated_vlsm Free annotation
initial_annotation_prop
annotated_transition_state)
annotated_constraint : VLSM message i : index
induced_validator_transition_consistency_Some
AnnotatedFree (IM i)
annotated_composite_label_project
annotated_composite_state_project
intros [i1 li1] [i2 li2] li.message, index : Type EqDecision0 : EqDecision index IM : index → VLSM message Free := free_composite_vlsm IM : VLSM message annotation : Type initial_annotation_prop : annotation → Prop H : Inhabited
{x : annotation | initial_annotation_prop x} annotated_constraint : label
(annotated_type Free
annotation)
→ annotated_state Free
annotation * option message
→ Prop annotated_transition_state : label
(annotated_type Free
annotation)
→ annotated_state Free
annotation *
option message
→ annotation AnnotatedFree := constrained_vlsm
(annotated_vlsm Free annotation
initial_annotation_prop
annotated_transition_state)
annotated_constraint : VLSM message i, i1 : index li1 : label (IM i1) i2 : index li2 : label (IM i2) li : label (IM i)
annotated_composite_label_project (existT i1 li1) =
Some li
→ annotated_composite_label_project (existT i2 li2) =
Some li
→ ∀ sX1 sX2 : state AnnotatedFree,
annotated_composite_state_project sX1 =
annotated_composite_state_project sX2
→ ∀ (iom : option message) (sX1' : state
AnnotatedFree)
(oom1 : option message),
transition (existT i1 li1) (sX1, iom) =
(sX1', oom1)
→ ∀ (sX2' : state AnnotatedFree) (oom2 :
option
message),
transition (existT i2 li2) (sX2, iom) =
(sX2', oom2)
→ annotated_composite_state_project sX1' =
annotated_composite_state_project sX2'
∧ oom1 = oom2
unfold annotated_composite_label_project, composite_project_label; cbn .message, index : Type EqDecision0 : EqDecision index IM : index → VLSM message Free := free_composite_vlsm IM : VLSM message annotation : Type initial_annotation_prop : annotation → Prop H : Inhabited
{x : annotation | initial_annotation_prop x} annotated_constraint : label
(annotated_type Free
annotation)
→ annotated_state Free
annotation * option message
→ Prop annotated_transition_state : label
(annotated_type Free
annotation)
→ annotated_state Free
annotation *
option message
→ annotation AnnotatedFree := constrained_vlsm
(annotated_vlsm Free annotation
initial_annotation_prop
annotated_transition_state)
annotated_constraint : VLSM message i, i1 : index li1 : label (IM i1) i2 : index li2 : label (IM i2) li : label (IM i)
match decide (i = i1) with
| left e =>
Some (eq_rect_r (λ n : index, label (IM n)) li1 e)
| right _ => None
end = Some li
→ match decide (i = i2) with
| left e =>
Some
(eq_rect_r (λ n : index, label (IM n)) li2 e)
| right _ => None
end = Some li
→ ∀ sX1 sX2 : annotated_state Free annotation,
annotated_composite_state_project sX1 =
annotated_composite_state_project sX2
→ ∀ (iom : option message) (sX1' : annotated_state
Free
annotation)
(oom1 : option message),
annotated_transition Free annotation
annotated_transition_state (existT i1 li1)
(sX1, iom) = (sX1', oom1)
→ ∀ (sX2' : annotated_state Free annotation)
(oom2 : option message),
annotated_transition Free annotation
annotated_transition_state
(existT i2 li2) (sX2, iom) =
(sX2', oom2)
→ annotated_composite_state_project sX1' =
annotated_composite_state_project sX2'
∧ oom1 = oom2
case_decide as Hi1; [| by congruence ]. message, index : Type EqDecision0 : EqDecision index IM : index → VLSM message Free := free_composite_vlsm IM : VLSM message annotation : Type initial_annotation_prop : annotation → Prop H : Inhabited
{x : annotation | initial_annotation_prop x} annotated_constraint : label
(annotated_type Free
annotation)
→ annotated_state Free
annotation * option message
→ Prop annotated_transition_state : label
(annotated_type Free
annotation)
→ annotated_state Free
annotation *
option message
→ annotation AnnotatedFree := constrained_vlsm
(annotated_vlsm Free annotation
initial_annotation_prop
annotated_transition_state)
annotated_constraint : VLSM message i, i1 : index li1 : label (IM i1) i2 : index li2 : label (IM i2) li : label (IM i) Hi1 : i = i1
Some (eq_rect_r (λ n : index, label (IM n)) li1 Hi1) =
Some li
→ match decide (i = i2) with
| left e =>
Some
(eq_rect_r (λ n : index, label (IM n)) li2 e)
| right _ => None
end = Some li
→ ∀ sX1 sX2 : annotated_state Free annotation,
annotated_composite_state_project sX1 =
annotated_composite_state_project sX2
→ ∀ (iom : option message) (sX1' : annotated_state
Free
annotation)
(oom1 : option message),
annotated_transition Free annotation
annotated_transition_state (existT i1 li1)
(sX1, iom) = (sX1', oom1)
→ ∀ (sX2' : annotated_state Free annotation)
(oom2 : option message),
annotated_transition Free annotation
annotated_transition_state
(existT i2 li2) (sX2, iom) =
(sX2', oom2)
→ annotated_composite_state_project sX1' =
annotated_composite_state_project sX2'
∧ oom1 = oom2
subst i1; cbn ; inversion_clear 1 .message, index : Type EqDecision0 : EqDecision index IM : index → VLSM message Free := free_composite_vlsm IM : VLSM message annotation : Type initial_annotation_prop : annotation → Prop H : Inhabited
{x : annotation | initial_annotation_prop x} annotated_constraint : label
(annotated_type Free
annotation)
→ annotated_state Free
annotation * option message
→ Prop annotated_transition_state : label
(annotated_type Free
annotation)
→ annotated_state Free
annotation *
option message
→ annotation AnnotatedFree := constrained_vlsm
(annotated_vlsm Free annotation
initial_annotation_prop
annotated_transition_state)
annotated_constraint : VLSM message i : index li1 : label (IM i) i2 : index li2 : label (IM i2) li : label (IM i)
match decide (i = i2) with
| left e =>
Some (eq_rect_r (λ n : index, label (IM n)) li2 e)
| right _ => None
end = Some li
→ ∀ sX1 sX2 : annotated_state Free annotation,
annotated_composite_state_project sX1 =
annotated_composite_state_project sX2
→ ∀ (iom : option message) (sX1' : annotated_state
Free
annotation)
(oom1 : option message),
annotated_transition Free annotation
annotated_transition_state (existT i li)
(sX1, iom) = (sX1', oom1)
→ ∀ (sX2' : annotated_state Free annotation)
(oom2 : option message),
annotated_transition Free annotation
annotated_transition_state
(existT i2 li2) (sX2, iom) =
(sX2', oom2)
→ annotated_composite_state_project sX1' =
annotated_composite_state_project sX2'
∧ oom1 = oom2
case_decide as Hi2; [| by congruence ]. message, index : Type EqDecision0 : EqDecision index IM : index → VLSM message Free := free_composite_vlsm IM : VLSM message annotation : Type initial_annotation_prop : annotation → Prop H : Inhabited
{x : annotation | initial_annotation_prop x} annotated_constraint : label
(annotated_type Free
annotation)
→ annotated_state Free
annotation * option message
→ Prop annotated_transition_state : label
(annotated_type Free
annotation)
→ annotated_state Free
annotation *
option message
→ annotation AnnotatedFree := constrained_vlsm
(annotated_vlsm Free annotation
initial_annotation_prop
annotated_transition_state)
annotated_constraint : VLSM message i : index li1 : label (IM i) i2 : index li2 : label (IM i2) li : label (IM i) Hi2 : i = i2
Some (eq_rect_r (λ n : index, label (IM n)) li2 Hi2) =
Some li
→ ∀ sX1 sX2 : annotated_state Free annotation,
annotated_composite_state_project sX1 =
annotated_composite_state_project sX2
→ ∀ (iom : option message) (sX1' : annotated_state
Free
annotation)
(oom1 : option message),
annotated_transition Free annotation
annotated_transition_state (existT i li)
(sX1, iom) = (sX1', oom1)
→ ∀ (sX2' : annotated_state Free annotation)
(oom2 : option message),
annotated_transition Free annotation
annotated_transition_state
(existT i2 li2) (sX2, iom) =
(sX2', oom2)
→ annotated_composite_state_project sX1' =
annotated_composite_state_project sX2'
∧ oom1 = oom2
subst i2; cbn ; inversion_clear 1 .message, index : Type EqDecision0 : EqDecision index IM : index → VLSM message Free := free_composite_vlsm IM : VLSM message annotation : Type initial_annotation_prop : annotation → Prop H : Inhabited
{x : annotation | initial_annotation_prop x} annotated_constraint : label
(annotated_type Free
annotation)
→ annotated_state Free
annotation * option message
→ Prop annotated_transition_state : label
(annotated_type Free
annotation)
→ annotated_state Free
annotation *
option message
→ annotation AnnotatedFree := constrained_vlsm
(annotated_vlsm Free annotation
initial_annotation_prop
annotated_transition_state)
annotated_constraint : VLSM message i : index li1, li2, li : label (IM i)
∀ sX1 sX2 : annotated_state Free annotation,
annotated_composite_state_project sX1 =
annotated_composite_state_project sX2
→ ∀ (iom : option message) (sX1' : annotated_state
Free annotation)
(oom1 : option message),
annotated_transition Free annotation
annotated_transition_state (existT i li)
(sX1, iom) = (sX1', oom1)
→ ∀ (sX2' : annotated_state Free annotation)
(oom2 : option message),
annotated_transition Free annotation
annotated_transition_state (existT i li)
(sX2, iom) = (sX2', oom2)
→ annotated_composite_state_project sX1' =
annotated_composite_state_project sX2'
∧ oom1 = oom2
intros [s1 ann1] [s2 ann2]
; unfold annotated_transition; cbn
; intros <- iom sX1' oom1
; destruct (transition _ _ _) as (si', om').message, index : Type EqDecision0 : EqDecision index IM : index → VLSM message Free := free_composite_vlsm IM : VLSM message annotation : Type initial_annotation_prop : annotation → Prop H : Inhabited
{x : annotation | initial_annotation_prop x} annotated_constraint : label
(annotated_type Free
annotation)
→ annotated_state Free
annotation * option message
→ Prop annotated_transition_state : label
(annotated_type Free
annotation)
→ annotated_state Free
annotation *
option message
→ annotation AnnotatedFree := constrained_vlsm
(annotated_vlsm Free annotation
initial_annotation_prop
annotated_transition_state)
annotated_constraint : VLSM message i : index li1, li2, li : label (IM i) s1 : state Free ann1 : annotation s2 : state Free ann2 : annotation iom : option message sX1' : annotated_state Free annotation oom1 : option message si' : state (IM i) om' : option message
({|
original_state := state_update IM s1 i si';
state_annotation :=
annotated_transition_state (existT i li)
({|
original_state := s1;
state_annotation := ann1
|}, iom)
|}, om') = (sX1', oom1)
→ ∀ (sX2' : annotated_state Free annotation) (oom2 :
option
message),
({|
original_state := state_update IM s2 i si';
state_annotation :=
annotated_transition_state (existT i li)
({|
original_state := s2;
state_annotation := ann2
|}, iom)
|}, om') = (sX2', oom2)
→ annotated_composite_state_project sX1' =
annotated_composite_state_project sX2'
∧ oom1 = oom2
inversion_clear 1 ; intros sX2' oom2; inversion_clear 1 .message, index : Type EqDecision0 : EqDecision index IM : index → VLSM message Free := free_composite_vlsm IM : VLSM message annotation : Type initial_annotation_prop : annotation → Prop H : Inhabited
{x : annotation | initial_annotation_prop x} annotated_constraint : label
(annotated_type Free
annotation)
→ annotated_state Free
annotation * option message
→ Prop annotated_transition_state : label
(annotated_type Free
annotation)
→ annotated_state Free
annotation *
option message
→ annotation AnnotatedFree := constrained_vlsm
(annotated_vlsm Free annotation
initial_annotation_prop
annotated_transition_state)
annotated_constraint : VLSM message i : index li1, li2, li : label (IM i) s1 : state Free ann1 : annotation s2 : state Free ann2 : annotation iom : option message sX1' : annotated_state Free annotation oom1 : option message si' : state (IM i) om' : option message sX2' : annotated_state Free annotation oom2 : option message
annotated_composite_state_project
{|
original_state := state_update IM s1 i si';
state_annotation :=
annotated_transition_state (existT i li)
({|
original_state := s1;
state_annotation := ann1
|}, iom)
|} =
annotated_composite_state_project
{|
original_state := state_update IM s2 i si';
state_annotation :=
annotated_transition_state (existT i li)
({|
original_state := s2;
state_annotation := ann2
|}, iom)
|} ∧ oom2 = oom2
by cbn ; state_update_simpl.
Qed .
Definition annotated_composite_induced_validator_is_projection :=
projection_induced_validator_is_projection _ _ _ _ _ _
annotated_composite_induced_validator_label_lift
annotated_composite_induced_validator_state_lift
annotated_composite_induced_validator_transition_consistency
annotated_composite_induced_validator_transition_None.
Lemma annotated_projection_validator_prop_alt_iff
: annotated_projection_validator_prop_alt <-> annotated_projection_validator_prop.message, index : Type EqDecision0 : EqDecision index IM : index → VLSM message Free := free_composite_vlsm IM : VLSM message annotation : Type initial_annotation_prop : annotation → Prop H : Inhabited
{x : annotation | initial_annotation_prop x} annotated_constraint : label
(annotated_type Free
annotation)
→ annotated_state Free
annotation * option message
→ Prop annotated_transition_state : label
(annotated_type Free
annotation)
→ annotated_state Free
annotation *
option message
→ annotation AnnotatedFree := constrained_vlsm
(annotated_vlsm Free annotation
initial_annotation_prop
annotated_transition_state)
annotated_constraint : VLSM message i : index
annotated_projection_validator_prop_alt
↔ annotated_projection_validator_prop
Proof .message, index : Type EqDecision0 : EqDecision index IM : index → VLSM message Free := free_composite_vlsm IM : VLSM message annotation : Type initial_annotation_prop : annotation → Prop H : Inhabited
{x : annotation | initial_annotation_prop x} annotated_constraint : label
(annotated_type Free
annotation)
→ annotated_state Free
annotation * option message
→ Prop annotated_transition_state : label
(annotated_type Free
annotation)
→ annotated_state Free
annotation *
option message
→ annotation AnnotatedFree := constrained_vlsm
(annotated_vlsm Free annotation
initial_annotation_prop
annotated_transition_state)
annotated_constraint : VLSM message i : index
annotated_projection_validator_prop_alt
↔ annotated_projection_validator_prop
apply projection_validator_prop_alt_iff.message, index : Type EqDecision0 : EqDecision index IM : index → VLSM message Free := free_composite_vlsm IM : VLSM message annotation : Type initial_annotation_prop : annotation → Prop H : Inhabited
{x : annotation | initial_annotation_prop x} annotated_constraint : label
(annotated_type Free
annotation)
→ annotated_state Free
annotation * option message
→ Prop annotated_transition_state : label
(annotated_type Free
annotation)
→ annotated_state Free
annotation *
option message
→ annotation AnnotatedFree := constrained_vlsm
(annotated_vlsm Free annotation
initial_annotation_prop
annotated_transition_state)
annotated_constraint : VLSM message i : index
weak_projection_transition_consistency_None
AnnotatedFree (IM i)
annotated_composite_label_project
annotated_composite_state_project
- message, index : Type EqDecision0 : EqDecision index IM : index → VLSM message Free := free_composite_vlsm IM : VLSM message annotation : Type initial_annotation_prop : annotation → Prop H : Inhabited
{x : annotation | initial_annotation_prop x} annotated_constraint : label
(annotated_type Free
annotation)
→ annotated_state Free
annotation * option message
→ Prop annotated_transition_state : label
(annotated_type Free
annotation)
→ annotated_state Free
annotation *
option message
→ annotation AnnotatedFree := constrained_vlsm
(annotated_vlsm Free annotation
initial_annotation_prop
annotated_transition_state)
annotated_constraint : VLSM message i : index
weak_projection_transition_consistency_None
AnnotatedFree (IM i)
annotated_composite_label_project
annotated_composite_state_project
by apply annotated_composite_induced_validator_transition_None.
- message, index : Type EqDecision0 : EqDecision index IM : index → VLSM message Free := free_composite_vlsm IM : VLSM message annotation : Type initial_annotation_prop : annotation → Prop H : Inhabited
{x : annotation | initial_annotation_prop x} annotated_constraint : label
(annotated_type Free
annotation)
→ annotated_state Free
annotation * option message
→ Prop annotated_transition_state : label
(annotated_type Free
annotation)
→ annotated_state Free
annotation *
option message
→ annotation AnnotatedFree := constrained_vlsm
(annotated_vlsm Free annotation
initial_annotation_prop
annotated_transition_state)
annotated_constraint : VLSM message i : index
induced_validator_label_lift_prop
annotated_composite_label_project
annotated_composite_label_lift
by apply annotated_composite_induced_validator_label_lift.
- message, index : Type EqDecision0 : EqDecision index IM : index → VLSM message Free := free_composite_vlsm IM : VLSM message annotation : Type initial_annotation_prop : annotation → Prop H : Inhabited
{x : annotation | initial_annotation_prop x} annotated_constraint : label
(annotated_type Free
annotation)
→ annotated_state Free
annotation * option message
→ Prop annotated_transition_state : label
(annotated_type Free
annotation)
→ annotated_state Free
annotation *
option message
→ annotation AnnotatedFree := constrained_vlsm
(annotated_vlsm Free annotation
initial_annotation_prop
annotated_transition_state)
annotated_constraint : VLSM message i : index
induced_validator_state_lift_prop
annotated_composite_state_project
annotated_composite_state_lift
by apply annotated_composite_induced_validator_state_lift.
- message, index : Type EqDecision0 : EqDecision index IM : index → VLSM message Free := free_composite_vlsm IM : VLSM message annotation : Type initial_annotation_prop : annotation → Prop H : Inhabited
{x : annotation | initial_annotation_prop x} annotated_constraint : label
(annotated_type Free
annotation)
→ annotated_state Free
annotation * option message
→ Prop annotated_transition_state : label
(annotated_type Free
annotation)
→ annotated_state Free
annotation *
option message
→ annotation AnnotatedFree := constrained_vlsm
(annotated_vlsm Free annotation
initial_annotation_prop
annotated_transition_state)
annotated_constraint : VLSM message i : index
strong_projection_initial_state_preservation (IM i)
AnnotatedFree annotated_composite_state_lift
by apply annotated_composite_induced_validator_initial_lift.
- message, index : Type EqDecision0 : EqDecision index IM : index → VLSM message Free := free_composite_vlsm IM : VLSM message annotation : Type initial_annotation_prop : annotation → Prop H : Inhabited
{x : annotation | initial_annotation_prop x} annotated_constraint : label
(annotated_type Free
annotation)
→ annotated_state Free
annotation * option message
→ Prop annotated_transition_state : label
(annotated_type Free
annotation)
→ annotated_state Free
annotation *
option message
→ annotation AnnotatedFree := constrained_vlsm
(annotated_vlsm Free annotation
initial_annotation_prop
annotated_transition_state)
annotated_constraint : VLSM message i : index
induced_validator_transition_consistency_Some
AnnotatedFree (IM i)
annotated_composite_label_project
annotated_composite_state_project
by apply annotated_composite_induced_validator_transition_consistency.
- message, index : Type EqDecision0 : EqDecision index IM : index → VLSM message Free := free_composite_vlsm IM : VLSM message annotation : Type initial_annotation_prop : annotation → Prop H : Inhabited
{x : annotation | initial_annotation_prop x} annotated_constraint : label
(annotated_type Free
annotation)
→ annotated_state Free
annotation * option message
→ Prop annotated_transition_state : label
(annotated_type Free
annotation)
→ annotated_state Free
annotation *
option message
→ annotation AnnotatedFree := constrained_vlsm
(annotated_vlsm Free annotation
initial_annotation_prop
annotated_transition_state)
annotated_constraint : VLSM message i : index
VLSM_projection AnnotatedFree
(preloaded_with_all_messages_vlsm (IM i))
annotated_composite_label_project
annotated_composite_state_project
by apply annotated_composite_preloaded_projection.
Qed .
End sec_composite_annotated_vlsm_projections .