From VLSM.Lib Require Import Itauto.
From Coq Require Import FunctionalExtensionality.
From stdpp Require Import prelude finite.
From VLSM.Lib Require Import Preamble StdppExtras StdppListSet.
From VLSM.Core Require Import VLSM VLSMProjections Composition Equivocation ProjectionTraces.
From VLSM.Examples Require Import BaseELMO.

ELMO: Protocol Definitions and Properties for UMO

This module contains definitions and properties of UMO components and the UMO protocol.

Section sec_UMO.

Context
  {Address : Type}
  `{EqDecision Address}
  (State := @State Address)
  (Observation := @Observation Address)
  (Message := @Message Address).

Component definition

The initial state has no observations and the same address as the component.

Definition UMO_component_initial_state_prop (i : Address) (st : State) : Prop :=
  obs st = [] /\ adr st = i.

Definition UMO_component_initial_state_type (i : Address) : Type :=
  {st : State | UMO_component_initial_state_prop i st}.

Program Definition UMO_component_initial_state
  (i : Address) : UMO_component_initial_state_type i := MkState [] i.
Next Obligation.
Proof.
  by compute.
Defined.

#[export] Instance Inhabited_UMO_component_initial_state_type (i : Address) :
  Inhabited (UMO_component_initial_state_type i) :=
    populate (UMO_component_initial_state i).

Definition UMO_component_transition
  (l : Label) (s : State) (om : option Message)
  : State * option Message :=
  match l, om with
  | Send, Some m => (s, om)
  | Send, None =>
      let ob := MkObservation Send (MkMessage s) in
      let st := s <+> ob in
      let msg := Some (MkMessage s) in
        (st, msg)
  | Receive, None => (s, None)
  | Receive, Some m =>
      let ob := MkObservation Receive m in
      let st := s <+> ob in
      let msg := None in
        (st, msg)
  end.

Inductive UMO_component_valid : Label -> State -> option Message -> Prop :=
| OCV_Send : forall st : State, UMO_component_valid Send st None
| OCV_Receive : forall (st : State) (msg : Message), UMO_component_valid Receive st (Some msg).

Ltac invert_UMO_component_valid :=
repeat match goal with
| H : UMO_component_valid Receive _ None |- _ => inversion H; subst; clear H
| H : UMO_component_valid Send _ (Some _) |- _ => inversion H; subst; clear H
end.

Definition UMO_component_machine (i : Address) : VLSMMachine ELMO_component_type :=
{|
  initial_state_prop := UMO_component_initial_state_prop i;
  initial_message_prop := const False;
  s0 := Inhabited_UMO_component_initial_state_type i;
  transition := fun l '(st, om) => UMO_component_transition l st om;
  valid := fun l '(st, om) => UMO_component_valid l st om;
|}.

Definition UMO_component (i : Address) : VLSM Message :=
{|
  vlsm_type := ELMO_component_type;
  vlsm_machine := UMO_component_machine i;
|}.

UMO components have a unique initial state.
Lemma UMO_component_initial_state_unique :
  forall {i : Address} {s1 s2 : State},
    UMO_component_initial_state_prop i s1 ->
    UMO_component_initial_state_prop i s2 ->
      s1 = s2.
Proof.
  by do 2 inversion 1; destruct s1, s2; cbn in *; subst.
Qed.

Lemma UMO_component_initial_state_spec :
  forall {i : Address} {s : State},
    UMO_component_initial_state_prop i s -> s = MkState [] i.
Proof.
  by inversion 1; destruct s; cbn in *; subst.
Qed.

#[export] Instance HasBeenSentCapability_UMO_component
  (i : Address) : HasBeenSentCapability (UMO_component i).
Proof.
  apply Build_HasBeenSentCapability with (fun s m => m ∈ sentMessages s)
  ; [by intros s m; typeclasses eauto |].
  split.
  - by intros [] []; cbn in *; subst; cbn; apply not_elem_of_nil.
  - intros l s im s' om [(Hvsp & Hovmp & Hv) Ht] m; cbn in *.
    destruct l, im; cbn in *; invert_UMO_component_valid
    ; inversion Ht; subst; clear Ht; cbn.
    + by rewrite decide_False; cbn; firstorder congruence.
    + rewrite decide_True by done; cbn.
      unfold Message; rewrite elem_of_cons.
      by firstorder congruence.
Defined.

#[export] Instance HasBeenReceivedCapability_UMO_component
  (i : Address) : HasBeenReceivedCapability (UMO_component i).
Proof.
  eapply Build_HasBeenReceivedCapability with (fun s m => m ∈ receivedMessages s)
  ; [intros s m; typeclasses eauto | split].
  - by intros [] []; cbn in *; subst; cbn; apply not_elem_of_nil.
  - intros l s im s' om [(Hvsp & Hovmp & Hv) Ht] m; cbn in *.
    destruct l, im; cbn in *; invert_UMO_component_valid
    ; inversion Ht; subst; clear Ht; cbn.
    + rewrite decide_True by done; cbn.
      unfold Message; rewrite elem_of_cons.
      by firstorder congruence.
    + by rewrite decide_False; cbn; firstorder congruence.
Defined.

#[export] Instance HasBeenDirectlyObservedCapability_UMO_component
  (i : Address) : HasBeenDirectlyObservedCapability (UMO_component i) :=
    HasBeenDirectlyObservedCapability_from_sent_received (UMO_component i).

A reachability predicate specialized for VLSMs refining UMO. UMO_reachable C s is equivalent to constrained_state_prop V s if the valid transitions of VLSM V follow UMO_component_transition and the validity predicate is a refinement of UMO_component_valid which does not further restrict the Send case.
Inductive UMO_reachable (C : State -> Message -> Prop) : State -> Prop :=
| reach_init :
    forall a, UMO_reachable C (MkState [] a)
| reach_send :
    forall s, UMO_reachable C s -> UMO_reachable C (s <+> MkObservation Send (MkMessage s))
| reach_recv :
    forall s msg, C s msg -> UMO_reachable C s ->
      UMO_reachable C (s <+> MkObservation Receive msg).

An alternative induction principle for UMO_reachable which has a single case for addObservation that covers both Send and Receive. The hypotheses available in that case use a match on the label to cover the differences between the cases. This is useful for proofs where the Send and Receive cases share some reasoning.
Lemma UMO_reachable_ind'
  (C : State -> Message -> Prop) (P : State -> Prop)
  (Hinit : forall a, P (MkState [] a))
  (Hextend : forall s l msg,
      UMO_reachable C s ->
      match l with
      | Send => msg = MkMessage s
      | Receive => C s msg
      end ->
      P s -> P (s <+> MkObservation l msg)) :
  forall s, UMO_reachable C s -> P s.
Proof.
  intros s Hs; induction Hs.
  - by apply Hinit.
  - by apply Hextend.
  - by apply Hextend.
Qed.

A specialized induction principle for UMO_reachable when the conclusion begins with forall m, m ∈ messages s -> .... This handles splitting m ∈ messages (s <+> ob) into cases for m ∈ messages s and for the new observation, and uses a new case HPrev to handle the m ∈ messages s parts for both Send and Receive. Unfortunately the induction _ using _ variant of the induction tactic cannot recognize this lemma as an induction principle, so it must be used with refine or apply.
Lemma UMO_reachable_elem_of_messages_ind
  (C : State -> Message -> Prop)
  (P : State -> Message -> Prop)
  (HPrev : forall s (Hs : UMO_reachable C s) m ob,
    m ∈ messages s ->
    P s m -> P (s <+> ob) m)
  (HSend : forall s (Hs : UMO_reachable C s),
    (forall m', m' ∈ messages s -> P s m') ->
    P (s <+> MkObservation Send (MkMessage s)) (MkMessage s))
  (HRecv : forall s (Hs : UMO_reachable C s) mr,
    C s mr ->
    (forall m', m' ∈ messages s -> P s m') ->
    P (s <+> MkObservation Receive mr) mr) :
  forall s, UMO_reachable C s ->
    forall m', m' ∈ messages s -> P s m'.
Proof.
  intros s Hs; induction Hs.
  - by inversion 1.
  - by intros m' [-> | Hm']%elem_of_messages_addObservation; eauto.
  - by intros m' [-> | Hm']%elem_of_messages_addObservation; eauto.
Qed.

Lemma UMO_reachable_impl (P Q : State -> Message -> Prop) (HPQ : forall s m, P s m -> Q s m) :
  forall s, UMO_reachable P s -> UMO_reachable Q s.
Proof.
  by induction 1; constructor; auto.
Qed.

Send transitions in a constrained state are ok.
Lemma input_constrained_transition_Send :
  forall (i : Address) (m : Message),
    constrained_state_prop (UMO_component i) (state m) ->
      input_constrained_transition (UMO_component i)
        Send (state m, None) (state m <+> MkObservation Send m, Some m).
Proof.
  intros; do 2 (red; cbn); split_and!.
  - done.
  - by apply option_valid_message_None.
  - by constructor.
  - by do 3 f_equal; apply eq_Message.
Qed.

Receive transitions in a constrained state are ok.
Lemma input_constrained_transition_Receive :
  forall (i : Address) (s : State) (m : Message),
    constrained_state_prop (UMO_component i) s ->
    input_constrained_transition (UMO_component i)
      Receive (s, Some m) (s <+> MkObservation Receive m, None).
Proof.
  intros; do 2 (red; cbn); split_and!; [done | | | done].
  - by apply any_message_is_valid_in_preloaded.
  - by constructor.
Qed.

This lemma shows that for a VLSM based on UMO reachability in the VLSM according to constrained_state_prop is equivalent to UMO_reachable with a predicate based on the VLSM's valid predicate, plus a condition on the address.
In particular the VLSM must work over the same VLSMType as UMO, of Message, State, and Label, the transition function must be UMO_component_transition, and the valid and initial_state_prop must be restrictions of UMO's predicates.
This lemma usually should not be used directly, but instead used to prove a "view" lemma for a specific VLSM, such as ELMO_reachable_view in the VLSM.ELMO.ELMO module.
Lemma UMO_based_valid_reachable
  (VM : VLSMMachine (Build_VLSMType Message State Label))
  (V := mk_vlsm VM)
  (Hinit_empty : forall si, initial_state_prop V si -> obs si = [])
  (Hsend_spec : forall s om, constrained_state_prop V s -> valid V Send (s, om) <-> om = None)
  (Htransition : forall l s om, transition V l (s, om) = UMO_component_transition l s om) :
  forall (s : State),
    constrained_state_prop V s
      <->
    UMO_reachable (fun s m => VM.(valid) Receive (s, Some m)) s
      /\ initial_state_prop V (MkState [] (adr s)).
Proof.
  split.
  - intros Hs; induction Hs using valid_state_prop_ind.
    + destruct s as [ol a].
      cbn in *; replace ol with (@nil Observation) in * by (specialize (Hinit_empty _ Hs); done).
      by split; [apply reach_init |].
    + destruct Ht as [(_ & _ & Hvalid) Ht].
      cbn in Ht; rewrite Htransition in Ht.
      destruct IHHs as [IH Hadr].
      by destruct l, om; inversion Ht; subst; auto using @UMO_reachable.
  - intros [Hs Hadr].
    induction Hs.
    + by apply initial_state_is_valid.
    + apply input_valid_transition_destination
        with (l := Send) (s := s) (om := None) (om' := Some (MkMessage s)).
      repeat split.
      * by apply IHHs.
      * by apply option_valid_message_None.
      * by apply Hsend_spec; [apply IHHs |].
      * by cbn; rewrite Htransition.
    + apply input_valid_transition_destination
        with (l := Receive) (s := s) (om := Some msg) (om' := None).
      repeat split; [| | done |].
      * by apply IHHs.
      * by apply any_message_is_valid_in_preloaded.
      * by cbn; rewrite Htransition.
Qed.

Every valid state contains a unique valid trace leading to it

To prove this, we will need some basic properties of UMO components.

Section sec_UMO_component_lemmas.

Ui is a notation for an UMO_component of address i.

Context
  {i : Address}
  (Ui : VLSM Message := UMO_component i)
  .

Lemma UMO_reachable_valid_state_prop :
  forall s, valid_state_prop Ui s ->
  UMO_reachable (const (const True)) s /\ adr s = i.
Proof.
  induction 1 using valid_state_prop_ind;
    [by destruct s, Hs as [Hobs Hadr]; cbn in *; subst; split; [constructor 1 |] |].
  by destruct Ht as [(_ & _ & Hv) Ht]; inversion Hv; subst; inversion Ht; subst;
    destruct_and!; (split; [constructor |]).
Qed.

Lemma UMO_reachable_constrained_state_prop :
  forall (s : State),
    constrained_state_prop (UMO_component i) s
      <->
    UMO_reachable (fun _ _ => True) s /\ adr s = i.
Proof.
  split.
  - induction 1 using valid_state_prop_ind;
      [by destruct s, Hs as [Hobs Hadr]; cbn in *; subst; split; [constructor 1 |] |].
    by destruct Ht as [(_ & _ & Hv) Ht]; inversion Hv; subst; inversion Ht; subst;
      destruct_and!; (split; [constructor |]).
  - intros [Hur Hadr].
    induction Hur; red; cbn in Hadr.
    + by apply initial_state_is_valid; cbv.
    + by eapply input_valid_transition_destination, input_constrained_transition_Send, IHHur.
    + by eapply input_valid_transition_destination, input_constrained_transition_Receive, IHHur.
Qed.

The initial state of Ui is unique.
Lemma vs0_uniqueness :
  forall is : State,
    UMO_component_initial_state_prop i is ->
      is = ``(vs0 Ui).
Proof.
  by intros []; inversion 1; cbv in *; by subst.
Qed.

Transitions of an UMO component preserve the address of the component.
Lemma UMO_component_transition_adr :
  forall (s1 s2 : State) (iom oom : option Message) (lbl : Label),
    UMO_component_transition lbl s1 iom = (s2, oom) ->
      adr s2 = adr s1.
Proof.
  by intros s1 s2 [im |] oom []; inversion_clear 1.
Qed.

For every trace segment, the initial and final state have the same address.

Lemma adr_of_states_within_constrained_trace :
  forall (is s : State) (tr : list transition_item),
    finite_constrained_trace_from_to Ui is s tr ->
      adr s = adr is.
Proof.
  induction 1; [done |].
  transitivity (adr s); [done |].
  eapply UMO_component_transition_adr.
  by destruct Ht as [_ Ht]; cbn in Ht.
Qed.

Lemma adr_of_states_within_valid_trace :
  forall (is s : State) (tr : list transition_item),
    finite_valid_trace_from_to Ui is s tr ->
      adr s = adr is.
Proof.
  induction 1; [done |].
  transitivity (adr s); [done |].
  eapply UMO_component_transition_adr.
  by destruct Ht as [_ Ht]; cbn in Ht.
Qed.

If a state is reachable, its address is the same as the address of the component.

Lemma adr_of_constrained_trace :
  forall (is s : State) (tr : list transition_item),
    finite_constrained_trace_init_to Ui is s tr ->
      adr s = i.
Proof.
  intros is s tr [Hfvt Hinit].
  transitivity (adr is).
  - by eapply adr_of_states_within_constrained_trace.
  - by destruct Hinit, is; cbn in *.
Qed.

Lemma adr_of_valid_trace :
  forall (is s : State) (tr : list transition_item),
    finite_valid_trace_init_to Ui is s tr ->
      adr s = i.
Proof.
  intros is s tr [Hfvt Hinit].
  transitivity (adr is).
  - by eapply adr_of_states_within_valid_trace.
  - by destruct Hinit, is; cbn in *.
Qed.

The address of a valid state is the same as the address of the component.
Lemma adr_of_constrained_state :
  forall s : State,
    constrained_state_prop Ui s -> adr s = i.
Proof.
  intros s Hvsp.
  apply valid_state_has_trace in Hvsp as (is & tr & Hfvti).
  by eapply adr_of_constrained_trace.
Qed.

Lemma adr_of_valid_state :
  forall s : State,
    valid_state_prop Ui s -> adr s = i.
Proof.
  intros s Hvsp.
  apply valid_state_has_trace in Hvsp as (is & tr & Hfvti).
  by eapply adr_of_valid_trace.
Qed.

Valid transitions lead to bigger states.

Lemma UMO_component_valid_transition_size :
  forall (s1 s2 : State) (iom oom : option Message) (lbl : Label),
    UMO_component_valid lbl s1 iom ->
    UMO_component_transition lbl s1 iom = (s2, oom) ->
      sizeState s1 < sizeState s2.
Proof.
  by intros [] s2 [im |] oom []; do 2 inversion_clear 1; cbn; lia.
Qed.

Lemma input_constrained_transition_size :
  forall (s1 s2 : State) (iom oom : option Message) (lbl : Label),
    input_constrained_transition Ui lbl (s1, iom) (s2, oom) ->
      sizeState s1 < sizeState s2.
Proof.
  intros s1 s2 iom oom lbl [(_ & _ & Hvalid) Ht]; cbn in *.
  by eapply UMO_component_valid_transition_size.
Qed.

A finite_valid_trace is either empty or its final state is bigger than its initial state.

Lemma finite_constrained_trace_from_to_size :
  forall (s1 s2 : State) (tr : list transition_item),
    finite_constrained_trace_from_to Ui s1 s2 tr ->
      s1 = s2 /\ tr = []
        \/
      sizeState s1 < sizeState s2.
Proof.
  induction 1; [by left |].
  assert (sizeState s' < sizeState s)
      by (eapply input_constrained_transition_size; done).
  by destruct IHfinite_valid_trace_from_to; [itauto congruence | itauto lia].
Qed.

If a trace leads from a state to itself, then it is empty.

Lemma finite_constrained_trace_from_to_inv :
  forall (s : State) (tr : list transition_item),
    finite_constrained_trace_from_to Ui s s tr -> tr = [].
Proof.
  by intros s tr Hfvt; apply finite_constrained_trace_from_to_size in Hfvt; itauto lia.
Qed.

The same lemmas as above, but for the component Ui. They follow from the above lemmas because there is a VLSM inclusion from Ui to Ui preloaded with all messages.

Lemma input_valid_transition_size :
  forall (s1 s2 : State) (iom oom : option Message) (lbl : Label),
    input_valid_transition Ui lbl (s1, iom) (s2, oom) ->
      sizeState s1 < sizeState s2.
Proof.
  intros s1 s2 iom oom lbl Hivt.
  eapply input_constrained_transition_size.
  apply (@VLSM_incl_input_valid_transition _ Ui Ui); [| done].
  by apply vlsm_incl_preloaded_with_all_messages_vlsm.
Qed.

Lemma finite_valid_trace_from_to_size :
  forall (s1 s2 : State) (tr : list transition_item),
    finite_valid_trace_from_to Ui s1 s2 tr ->
      s1 = s2 /\ tr = []
        \/
      sizeState s1 < sizeState s2.
Proof.
  intros s1 s2 tr Hfvt.
  eapply finite_constrained_trace_from_to_size.
  apply (@VLSM_incl_finite_valid_trace_from_to _ Ui Ui); [| done].
  by apply vlsm_incl_preloaded_with_all_messages_vlsm.
Qed.

Lemma finite_valid_trace_from_to_inv :
  forall (s : State) (tr : list transition_item),
    finite_valid_trace_from_to Ui s s tr -> tr = [].
Proof.
  intros s tr Hfvt.
  eapply finite_constrained_trace_from_to_inv.
  apply (@VLSM_incl_finite_valid_trace_from_to _ Ui Ui); [| done].
  by apply vlsm_incl_preloaded_with_all_messages_vlsm.
Qed.

transitions in any VLSM are deterministic, i.e., the final state and output message are determined by the label, initial state and input message.
For UMO components, an extremely strong converse property also holds: the label, initial state, input message and output message are all determined by the final state of a valid transition. Basically, this is true because every state contains the whole trace/history.

Lemma input_constrained_transition_deterministic_conv :
  forall (s1 s2 f : State) (iom1 iom2 oom1 oom2 : option Message) (lbl1 lbl2 : Label),
    input_constrained_transition Ui lbl1 (s1, iom1) (f, oom1) ->
    input_constrained_transition Ui lbl2 (s2, iom2) (f, oom2) ->
      lbl1 = lbl2 /\ s1 = s2 /\ iom1 = iom2 /\ oom1 = oom2.
Proof.
  intros s1 s2 f iom1 iom2 oom1 oom2 lbl1 lbl2 Hivt1 Hivt2
  ; inversion Hivt1 as [(_ & _ & Hvalid1) Ht1]; subst
  ; inversion Hivt2 as [(_ & _ & Hvalid2) Ht2]; subst.
  destruct lbl1, lbl2, iom1, iom2; cbn in *
  ; inversion Ht1; subst; clear Ht1
  ; inversion Ht2; subst; clear Ht2
  ; invert_UMO_component_valid; auto.
  by destruct s1, s2; cbn in *; subst; itauto.
Qed.

Lemma input_valid_transition_deterministic_conv :
  forall (s1 s2 f : State) (iom1 iom2 oom1 oom2 : option Message) (lbl1 lbl2 : Label),
    input_valid_transition Ui lbl1 (s1, iom1) (f, oom1) ->
    input_valid_transition Ui lbl2 (s2, iom2) (f, oom2) ->
      lbl1 = lbl2 /\ s1 = s2 /\ iom1 = iom2 /\ oom1 = oom2.
Proof.
  intros s1 s2 f iom1 iom2 oom1 oom2 lbl1 lbl2 Hivt1 Hivt2.
  by eapply input_constrained_transition_deterministic_conv;
    apply (@VLSM_incl_input_valid_transition _ Ui Ui); [| done | | done];
    apply vlsm_incl_preloaded_with_all_messages_vlsm.
Qed.

Every trace segment is fully determined by its initial and final state.

Lemma finite_constrained_trace_from_to_unique :
  forall (s1 s2 : State) (l1 l2 : list transition_item),
    finite_constrained_trace_from_to Ui s1 s2 l1 ->
    finite_constrained_trace_from_to Ui s1 s2 l2 ->
      l1 = l2.
Proof.
  intros s1 s2 l1 l2 Hfvt1 Hfvt2; revert l2 Hfvt2.
  induction Hfvt1 using finite_valid_trace_from_to_rev_ind; intros.
  - by apply finite_constrained_trace_from_to_size in Hfvt2; itauto (congruence + lia).
  - destruct Hfvt2 using finite_valid_trace_from_to_rev_ind; [| clear IHHfvt2].
    + apply finite_constrained_trace_from_to_size in Hfvt1.
      apply input_constrained_transition_size in Ht.
      by decompose [and or] Hfvt1; subst; clear Hfvt1; lia.
    + assert (l = l0 /\ s = s0 /\ iom = iom0 /\ oom = oom0)
          by (eapply input_constrained_transition_deterministic_conv; done).
      decompose [and] H; subst; clear H.
      by f_equal; apply IHHfvt1.
Qed.

Lemma finite_valid_trace_from_to_unique :
  forall (s1 s2 : State) (l1 l2 : list transition_item),
    finite_valid_trace_from_to Ui s1 s2 l1 ->
    finite_valid_trace_from_to Ui s1 s2 l2 ->
      l1 = l2.
Proof.
  by intros s1 s2 l1 l2 Hfvt1 Hfvt2;
    eapply finite_constrained_trace_from_to_unique;
    apply VLSM_incl_finite_valid_trace_from_to; [| done | | done];
    apply vlsm_incl_preloaded_with_all_messages_vlsm.
Qed.

Every trace is determined by its final state.
Uniqueness
Lemma finite_constrained_trace_init_to_unique :
  forall (s f : State) (l1 l2 : list transition_item),
    finite_constrained_trace_init_to Ui s f l1 ->
    finite_constrained_trace_init_to Ui s f l2 ->
      l1 = l2.
Proof.
  intros s f l1 l2 [Ht1 _] [Ht2 _].
  by eapply finite_constrained_trace_from_to_unique.
Qed.

Lemma finite_valid_trace_init_to_unique :
  forall (s f : State) (l1 l2 : list transition_item),
    finite_valid_trace_init_to Ui s f l1 ->
    finite_valid_trace_init_to Ui s f l2 ->
      l1 = l2.
Proof.
  by intros s f l1 l2 Hfvit1 Hfvit2;
    eapply finite_constrained_trace_init_to_unique;
    apply VLSM_incl_finite_valid_trace_init_to; [| done | | done];
    apply vlsm_incl_preloaded_with_all_messages_vlsm.
Qed.

If a valid trace leads to state s, the trace extracted from s also leads to s.
Lemma finite_constrained_trace_init_to_state2trace :
  forall (is s : State) (tr : list transition_item),
    finite_constrained_trace_init_to Ui is s tr ->
      finite_constrained_trace_init_to Ui is s (state2trace s).
Proof.
  intros is s tr [Hfv Hinit]; cbn in *; revert Hinit.
  induction Hfv using finite_valid_trace_from_to_rev_ind; intros.
  - inversion Hinit; clear Hinit.
    destruct si; cbn in *; subst; cbn.
    repeat constructor. exists None.
    by repeat constructor.
  - specialize (IHHfv Hinit).
    destruct Ht as [Hvalid Ht]; cbn in Ht.
    destruct s as [obs adr], l, iom as [im |]
    ; inversion Ht; subst; clear Ht; cbn in *
    ; cycle 1; [done | done | |].
    + constructor; [| done].
      by eapply extend_right_finite_trace_from_to; [apply IHHfv |]; auto.
    + constructor; [| done].
      by eapply extend_right_finite_trace_from_to; [apply IHHfv |]; auto.
Qed.

Lemma finite_valid_trace_init_to_state2trace :
  forall (is s : State) (tr : list transition_item),
    finite_valid_trace_init_to Ui is s tr ->
      finite_valid_trace_init_to Ui is s (state2trace s).
Proof.
  intros is s tr [Hfv Hinit]; cbn in *; revert Hinit.
  induction Hfv using finite_valid_trace_from_to_rev_ind; intros.
  - inversion Hinit; clear Hinit.
    destruct si; cbn in *; subst; cbn.
    repeat constructor. exists None.
    by repeat constructor.
  - specialize (IHHfv Hinit).
    destruct Ht as [Hvalid Ht]; cbn in Ht.
    destruct s as [obs adr], l, iom as [im |]
    ; inversion Ht; subst; clear Ht; cbn in *
    ; cycle 1; [done | done | |].
    + constructor; [| done].
      by eapply extend_right_finite_trace_from_to; [apply IHHfv |]; auto.
    + constructor; [| done].
      by eapply extend_right_finite_trace_from_to; [apply IHHfv |]; auto.
Qed.

The trace extracted from the final state of another trace is equal to that trace.

Lemma finite_constrained_trace_init_to_state2trace_inv :
  forall (is s : State) (tr : list transition_item),
    finite_constrained_trace_init_to Ui is s tr ->
      state2trace s = tr.
Proof.
  intros is s tr Hfvti.
  assert (Hfvti' : finite_constrained_trace_init_to Ui is s (state2trace s))
      by (eapply finite_constrained_trace_init_to_state2trace; done).
  by eapply finite_constrained_trace_init_to_unique.
Qed.

Lemma finite_valid_trace_init_to_state2trace_inv :
  forall (is s : State) (tr : list transition_item),
    finite_valid_trace_init_to Ui is s tr ->
      state2trace s = tr.
Proof.
  by intros is s tr Hfvti;
    eapply finite_constrained_trace_init_to_state2trace_inv;
    apply VLSM_incl_finite_valid_trace_init_to; [| done];
    apply vlsm_incl_preloaded_with_all_messages_vlsm.
Qed.

The trace extracted from a reachable state s leads to s.
Existence
Lemma finite_constrained_trace_init_to_state2trace' :
  forall (s : State),
    constrained_state_prop Ui s ->
      finite_constrained_trace_init_to Ui (``(vs0 Ui)) s (state2trace s).
Proof.
  intros s Hs.
  apply valid_state_has_trace in Hs as (is & tr & Htr).
  apply finite_constrained_trace_init_to_state2trace_inv in Htr as Heqtr; subst.
  replace (``(vs0 Ui)) with is; [done |].
  by apply vs0_uniqueness, Htr.
Qed.

Lemma constrained_state_contains_unique_constrained_trace :
  forall s : State,
    constrained_state_prop Ui s ->
      exists tr : list transition_item,
        finite_constrained_trace_init_to Ui (``(vs0 Ui)) s tr
          /\
        forall tr' : list transition_item,
          finite_constrained_trace_init_to Ui (``(vs0 Ui)) s tr' -> tr' = tr.
Proof.
  intros s Hvsp.
  exists (state2trace s); split.
  - by eapply finite_constrained_trace_init_to_state2trace'.
  - intros tr' Hfvt. symmetry.
    by eapply finite_constrained_trace_init_to_state2trace_inv.
Qed.

Existence
Lemma finite_valid_trace_init_to_state2trace' :
  forall (s : State),
    valid_state_prop Ui s ->
      finite_valid_trace_init_to Ui (``(vs0 Ui)) s (state2trace s).
Proof.
  intros s Hs.
  apply valid_state_has_trace in Hs as (is & tr & Htr).
  apply finite_valid_trace_init_to_state2trace_inv in Htr as Heqtr; subst.
  replace (``(vs0 Ui)) with is; [done |].
  by apply vs0_uniqueness, Htr.
Qed.

Lemma valid_state_contains_unique_valid_trace :
  forall s : State,
    valid_state_prop Ui s ->
      exists tr : list transition_item,
        finite_valid_trace_init_to Ui (``(vs0 Ui)) s tr
          /\
        forall tr' : list transition_item,
          finite_valid_trace_init_to Ui (``(vs0 Ui)) s tr' -> tr' = tr.
Proof.
  intros s Hvsp.
  exists (state2trace s); split.
  - by eapply finite_valid_trace_init_to_state2trace'.
  - intros tr' Hfvt. symmetry.
    by eapply finite_valid_trace_init_to_state2trace_inv.
Qed.

The suffix ordering on states is a strict total order

s1 is a state-suffix of s2 if they have the same address and s1's observations are a strict suffix of s2's observations.

Record state_suffix (s1 s2 : State) : Prop :=
{
  adrs_eq : adr s1 = adr s2;
  obs_prefix : strict suffix (obs s1) (obs s2);
}.

#[export] Instance state_suffix_dec : RelDecision state_suffix :=
  fun s1 s2 =>
    match decide (adr s1 = adr s2) with
    | left addr_eq =>
        match decide (strict suffix (obs s1) (obs s2)) with
        | left is_suffix => left (Build_state_suffix _ _ addr_eq is_suffix)
        | right Hnot_suffix => right (fun H => Hnot_suffix (obs_prefix _ _ H))
        end
    | right Hnot_addr => right (fun H => Hnot_addr (adrs_eq _ _ H))
    end.

We also define a variant of the suffix relation for messages.
Definition message_suffix (m1 m2 : Message) : Prop :=
  state_suffix (state m1) (state m2).

The state-prefix relation is a strict partial order.

#[export] Instance Irreflexive_state_suffix :
  Irreflexive state_suffix.
Proof.
  by intros s (Hadr & Hobs1 & Hobs2).
Qed.

#[export] Instance Transitive_state_suffix :
  Transitive state_suffix.
Proof.
  intros s1 s2 s3 (Hadr12 & Hobs12 & Hobs12') (Hadr23 & Hobs23 & Hobs23').
  split; [by congruence |].
  by transitivity (obs s2).
Qed.

#[export] Instance StrictOrder_state_suffix :
  StrictOrder state_suffix.
Proof.
  by split; typeclasses eauto.
Qed.

Lemma state_suffix_empty_minimal :
  forall (s : State) (a : Address), ~ state_suffix s (MkState [] a).
Proof.
  intros s a [_ [[os Hsuf] Hstrict]]; contradict Hstrict.
  by symmetry in Hsuf; apply app_nil in Hsuf as [-> ->]; exists [].
Qed.

Lemma state_suffix_empty_minimum :
  forall (s : State), s = MkState [] (adr s) \/ state_suffix (MkState [] (adr s)) s.
Proof.
  intros [[| ob obs] a]; cbn; [by left | right].
  split; cbn; [done |].
  split; cbn; [by apply suffix_nil |].
  by intros H; apply suffix_nil_inv in H; subst.
Qed.

If we add an observation to a state s, s is a suffix of the resulting state.

Lemma state_suffix_addObservation :
  forall (s : State) (ob : Observation),
    state_suffix s (s <+> ob).
Proof.
  intros s ob.
  constructor; cbn; [done |].
  unfold addObservation; split.
  - by apply suffix_cons_r.
  - by apply suffix_cons_not.
Qed.

Lemma state_suffix_addObservations :
  forall (s : State) (obs' : list Observation),
    obs' <> [] -> state_suffix s (s <++> obs').
Proof.
  intros s obs'.
  constructor; cbn; [done |].
  split.
  - by apply suffix_app_r.
  - by intros Hsuf; apply (suffix_app_inv obs' []), suffix_nil_inv in Hsuf.
Qed.

The initial state of a valid transition is a state_suffix of the final state.
Lemma state_suffix_of_UMO_component_valid_transition :
  forall (lbl : Label) (s1 s2 : State) (iom oom : option Message),
    UMO_component_valid lbl s1 iom ->
    UMO_component_transition lbl s1 iom = (s2, oom) ->
      state_suffix s1 s2.
Proof.
  intros [] s1 s2 [im |] oom HValid; cbn
  ; intros H; inversion H; subst; clear H.
  - by apply state_suffix_addObservation.
  - by invert_UMO_component_valid.
  - by invert_UMO_component_valid.
  - by apply state_suffix_addObservation.
Qed.

The previous property carries over from transitions to valid transitions.
Lemma state_suffix_of_input_constrained_transition :
  forall (lbl : Label) (s1 s2 : State) (iom oom : option Message),
    input_constrained_transition Ui lbl (s1, iom) (s2, oom) ->
      state_suffix s1 s2.
Proof.
  intros lbl s1 s2 iom oom [(Hvsp & Hovmp & Hvalid) Ht]; cbn in Ht.
  by eapply state_suffix_of_UMO_component_valid_transition; cycle 1.
Qed.

If there is a trace segment from s1 to s2, then either the states are equal (because the trace is empty), or s1 is a state-suffix of s2.
Lemma state_suffix_of_finite_constrained_trace_from_to :
  forall (s1 s2 : State) (tr : list transition_item),
    finite_constrained_trace_from_to Ui s1 s2 tr ->
      s1 = s2 \/ state_suffix s1 s2.
Proof.
  induction 1; [by left |].
  destruct IHfinite_valid_trace_from_to as [-> | IH]; right.
  - by eapply state_suffix_of_input_constrained_transition; eauto.
  - transitivity s; [| done].
    by eapply state_suffix_of_input_constrained_transition; eauto.
Qed.

state_suffix_of_finite_constrained_trace_from_to carries over from trace segments to traces.
Lemma state_suffix_of_finite_constrained_trace_init_to :
  forall (s1 s2 : State) (tr : list transition_item),
    finite_constrained_trace_init_to Ui s1 s2 tr ->
      s1 = s2 \/ state_suffix s1 s2.
Proof.
  intros s1 s2 tr [Hfvt Hinit].
  by eapply state_suffix_of_finite_constrained_trace_from_to.
Qed.

Every reachable state is either initial or the target of some transition. This transition comes from a source state which is also reachable. Additionally, if the label of the transition is Send, we know that the observation contains the source state.
Lemma UMO_reachable_inv P :
  forall s : State,
    UMO_reachable P s ->
      obs s = [] \/
      exists (lbl : Label) (iom oom : option Message) (s' : State) (ob : Observation),
        UMO_component_transition lbl s' iom = (s, oom) /\
        s = s' <+> ob /\
        UMO_reachable P s' /\
        (lbl = Send -> message ob = MkMessage s').
Proof.
  intros s Hs.
  inversion Hs; [by left | right..].
  - by eexists Send, None, (Some (MkMessage s0)), s0, _.
  - by eexists Receive, (Some msg), None, s0, _.
Qed.

If a reachable state s2 is a result of adding an observation to a state s1, then s1 is also reachable. Additionally, if the observation's label is Send, then we can characterize the state s1.

Lemma UMO_reachable_addObservation_inv P :
  forall (s : State) (ob : Observation),
    UMO_reachable P (s <+> ob) -> UMO_reachable P s.
Proof.
  intros s ob Hvsp.
  apply UMO_reachable_inv in Hvsp
     as [[=] | (lbl & iom & oom & s' & ob' & Ht & Hadd & Hvsp & Hss')]; cbn in *.
  by apply addObservation_inj in Hadd as [_ ->].
Qed.

Lemma UMO_reachable_addObservation_inv_Send_state P :
  forall (s : State) (m : Message),
    UMO_reachable P (s <+> MkObservation Send m) ->
      s = state m.
Proof.
  intros s m Hvsp.
  apply UMO_reachable_inv in Hvsp
     as [[=] | (lbl & iom & oom & s' & ob' & Ht & Hadd & Hvsp & Hlbl)]; cbn in *.
  inversion Hadd.
  replace (state m) with (state (message ob')) by (rewrite <- H0; cbn; done).
  rewrite Hlbl; [by apply eq_State |].
  by destruct lbl, iom; cbn in *; inversion Ht; subst; [| | done]
  ; apply (f_equal (fun x => length (obs x))) in Hadd; cbn in Hadd; lia.
Qed.

Lemma UMO_reachable_addObservation_inv_Send P :
  forall (s : State) (m : Message),
    UMO_reachable P (s <+> MkObservation Send m) ->
      UMO_reachable P (state m).
Proof.
  intros s m Hvsp.
  erewrite <- UMO_reachable_addObservation_inv_Send_state; [| done].
  by eapply UMO_reachable_addObservation_inv.
Qed.

Lemma UMO_reachable_addObservation_inv_message P :
  forall (s : State) (ob : Observation),
    UMO_reachable P (s <+> ob) -> label ob = Send ->
      message ob = MkMessage s.
Proof.
  intros s ob Hvsp Heq.
  apply UMO_reachable_inv in Hvsp
     as [[=] | (lbl & iom & oom & s' & ob' & Ht & Hadd & Hvsp & Hss')]; cbn in *.
  apply addObservation_inj in Hadd as [-> ->].
  apply Hss'. destruct lbl, iom; inversion Ht; subst; clear Ht; cbn in *; [done | | done | done].
  by symmetry in H0; apply addObservation_acyclic in H0.
Qed.

If a reachable state s2 results from adding observations to a state s1, then s1 is also reachable.
Lemma UMO_reachable_addObservations_inv P :
  forall (s : State) (obs' : list Observation),
    UMO_reachable P (s <++> obs') -> UMO_reachable P s.
Proof.
  intros s obs'; revert s.
  induction obs' as [| ob' obs']; cbn; intros s Hvsp.
  - by rewrite <- addObservations_nil.
  - by apply IHobs', UMO_reachable_addObservation_inv with ob'.
Qed.

If a state is constrained, after sending a message it's still constrained.
Lemma constrained_state_prop_Send :
  forall (m : Message),
    constrained_state_prop (UMO_component i) (state m) ->
    constrained_state_prop (UMO_component i) (state m <+> MkObservation Send m).
Proof.
  setoid_rewrite UMO_reachable_constrained_state_prop; cbn.
  intros m [Hur Hadr]; split; [| done].
  by destruct m; constructor.
Qed.

If a state is constrained, after receiving a message it's still constrained.
Lemma constrained_state_prop_Receive :
  forall (s : State) (m : Message),
    constrained_state_prop (UMO_component i) s ->
    constrained_state_prop (UMO_component i) (s <+> MkObservation Receive m).
Proof.
  setoid_rewrite UMO_reachable_constrained_state_prop; cbn.
  intros s m [Hur Hadr]; split; [| done].
  by destruct m; constructor.
Qed.

If a state is constrained after adding an observation, it must have been constrained before adding it.
Lemma constrained_state_prop_addObservation_inv :
  forall (s : State) (ob : Observation),
    constrained_state_prop (UMO_component i) (s <+> ob) ->
    constrained_state_prop (UMO_component i) s.
Proof.
  setoid_rewrite UMO_reachable_constrained_state_prop; cbn.
  intros s ob [Hur Hadr]; split; [| done].
  by eapply UMO_reachable_addObservation_inv.
Qed.

If a state is constrained after adding some observations, it must have been constrained before adding them.
Lemma constrained_state_prop_addObservations_inv :
  forall (s : State) (obs : list Observation),
    constrained_state_prop (UMO_component i) (s <++> obs) ->
    constrained_state_prop (UMO_component i) s.
Proof.
  setoid_rewrite UMO_reachable_constrained_state_prop; cbn.
  intros s ob [Hur Hadr]; split; [| done].
  by eapply UMO_reachable_addObservations_inv.
Qed.

The lemma just below essentially states that for every reachable state s, messages sent earlier are suffixes of messages sent later and that the messages are suffixes of the state s.
More technically: if the observations of a reachable state s contain two sent messages m1 and m2 (with potentially some more observations in-between), then the state of m1 is a state-suffix of the state of m2 and also the state of m2 is a state-suffix of s.
Lemma state_suffix_totally_orders_sent_messages_UMO_reachable_aux P :
  forall (s : State) (m1 m2 : Message) (obs1 obs2 obs3 : list Observation),
    s = MkState [] (adr s) <++>
      obs1 <+> MkObservation Send m1 <++> obs2 <+> MkObservation Send m2 <++> obs3 ->
    UMO_reachable P s ->
      state_suffix (state m1) (state m2) /\ state_suffix (state m2) s.
Proof.
  intros s m1 m2 obs1 obs2 obs3 -> Hvsp.
  apply UMO_reachable_addObservations_inv in Hvsp.
  assert (Hm2 := UMO_reachable_addObservation_inv_message _ _ _ Hvsp).
  apply UMO_reachable_addObservation_inv in Hvsp.
  apply UMO_reachable_addObservations_inv in Hvsp.
  assert (Hm1 := UMO_reachable_addObservation_inv_message _ _ _ Hvsp).
  cbn in *; rewrite Hm1, Hm2 by done;
  cbn in *; rewrite <- Hm1, <- Hm2 by done
  ; clear Hvsp Hm1 Hm2; split.
  - rewrite addObservations_app.
    by apply state_suffix_addObservations, ListExtras.last_not_null.
  - rewrite (addObservations_app _ _ obs3).
    by apply state_suffix_addObservations, ListExtras.last_not_null.
Qed.

state_suffix_totally_orders_sent_messages_UMO_reachable_aux easily carries over to valid states.
Lemma state_suffix_totally_orders_sent_messages_valid_state_prop_aux :
  forall (s : State) (m1 m2 : Message) (obs1 obs2 obs3 : list Observation),
    s = MkState [] (adr s) <++>
      obs1 <+> MkObservation Send m1 <++> obs2 <+> MkObservation Send m2 <++> obs3 ->
    valid_state_prop Ui s ->
      state_suffix (state m1) (state m2) /\ state_suffix (state m2) s.
Proof.
  intros s m1 m2 obs1 obs2 obs3 Heq Hvsp.
  eapply state_suffix_totally_orders_sent_messages_UMO_reachable_aux; [done |].
  by apply UMO_reachable_valid_state_prop.
Qed.

The message_suffix relation is trichotomous on the sentMessages of any reachable state.
Lemma state_suffix_totally_orders_sent_messages_UMO_reachable P :
  forall (s : State) (m1 m2 : Message),
    UMO_reachable P s -> m1 ∈ sentMessages s -> m2 ∈ sentMessages s ->
      message_suffix m1 m2 \/ m1 = m2 \/ message_suffix m2 m1.
Proof.
  intros s m1 m2 Hvalid H1 H2.
  apply elem_of_sentMessages in H1, H2.
  destruct (elem_of_list_split_2 _ _ _ H1 H2) as [Heq | (obs1 & obs2 & obs3 & [H | H])]
  ; [right; left | right; right | left].
  - by congruence.
  - eapply state_suffix_totally_orders_sent_messages_UMO_reachable_aux with (s := s); [| done].
    by apply eq_State; cbn; [rewrite app_nil_r |].
  - eapply state_suffix_totally_orders_sent_messages_UMO_reachable_aux with (s := s); [| done].
    by apply eq_State; cbn; [rewrite app_nil_r |].
Qed.

state_suffix_totally_orders_sent_messages_UMO_reachable transfers to sentMessages of valid states.
Lemma state_suffix_totally_orders_sent_messages_valid_state_prop :
  forall (s : State) (m1 m2 : Message),
    valid_state_prop Ui s -> m1 ∈ sentMessages s -> m2 ∈ sentMessages s ->
      message_suffix m1 m2 \/ m1 = m2 \/ message_suffix m2 m1.
Proof.
  intros s m1 m2 Hvsp Hin1 Hin2.
  by eapply state_suffix_totally_orders_sent_messages_UMO_reachable;
    [apply UMO_reachable_valid_state_prop | ..].
Qed.

Observability

Message m1 is directly observable in message m2 if m1 is an element of the list of observation of m2's state.
It would be possible to use a different definition of directly_observable, which goes by cases on whether the message was sent or received.
Definition directly_observable (m1 m2 : Message) : Prop :=
  m1 ∈ map message (obs (state m2)).

Our definition is equivalent to the alternative definition.
Lemma directly_observable_spec_other :
  forall m1 m2 : Message,
    m1 ∈ map message (obs (state m2))
      <->
    m1 ∈ sentMessages (state m2) \/ m1 ∈ receivedMessages (state m2).
Proof.
  intros m1 m2.
  unfold sentMessages, sentMessages', receivedMessages, receivedMessages'.
  unfold Message; rewrite !elem_of_list_fmap.
  setoid_rewrite elem_of_list_filter.
  split.
  - intros (ob & Hm & Hin); subst.
    destruct (label ob) eqn: Hlob.
    + by right; exists ob; unfold isReceive; rewrite Hlob.
    + by left; exists ob; unfold isSend; rewrite Hlob.
  - intros [(ob & -> & Hs & Hin) | (ob & -> & Hs & Hin)].
    + by exists ob.
    + by exists ob.
Qed.

observable is the transitive closure of directly_observable.
Definition observable : relation Message :=
  tc directly_observable.

If m1 is directly observable in a suffix of m3, then it is also directly observable in m3.
Lemma message_suffix_directly_observable :
  forall m1 m2 m3 : Message,
    message_suffix m2 m3 -> directly_observable m1 m2 -> directly_observable m1 m3.
Proof.
  unfold directly_observable.
  intros [s1] [s2] [s3] (_ & [obs' Hsuf] & _) Hdo; cbn in *.
  by unfold Message; rewrite Hsuf, map_app, elem_of_app; right.
Qed.

m is directly observable in state s extended with new observation ob iff m is the message of ob or m is directly observable in s.
Lemma directly_observable_addObservation :
  forall (m : Message) (s : State) (ob : Observation),
    directly_observable m (MkMessage (s <+> ob))
      <->
    directly_observable m (MkMessage s) \/ m = message ob.
Proof.
  unfold directly_observable, Message.
  by intros m s ob; cbn; rewrite elem_of_cons; itauto.
Qed.

directly_observable_addObservation easily transfers to a situation in which we add multiple observations at once.
Lemma directly_observable_addObservations :
  forall (m : Message) (s : State) (obs' : list Observation),
    directly_observable m (MkMessage (s <++> obs'))
      <->
    directly_observable m (MkMessage s) \/ m ∈ map message obs'.
Proof.
  unfold directly_observable, Message.
  by intros m s obs'; cbn; rewrite map_app, elem_of_app; itauto.
Qed.

In a reachable state, messages sent earlier are directly observable in messages sent later.
Lemma directly_observable_totally_orders_sent_messages_UMO_reachable P :
  forall (s : State) (m1 m2 : Message) (obs1 obs2 obs3 : list Observation),
    s = MkState [] (adr s) <++>
      obs1 <+> MkObservation Send m1 <++> obs2 <+> MkObservation Send m2 <++> obs3 ->
    UMO_reachable P s ->
      directly_observable m1 m2.
Proof.
  intros s m1 m2 obs1 obs2 obs3 Heq Hvsp.
  rewrite Heq in Hvsp.
  apply UMO_reachable_addObservations_inv in Hvsp.
  apply UMO_reachable_addObservation_inv_message in Hvsp as Heq'; [| done].
  cbn in Heq'; subst; clear Heq Hvsp.
  repeat (rewrite ?directly_observable_addObservations, ?directly_observable_addObservation); cbn.
  by itauto.
Qed.

directly_observable_totally_orders_sent_messages_UMO_reachable can be transferred to valid states.
Lemma directly_observable_totally_orders_sent_messages_valid_state_prop :
  forall (s : State) (m1 m2 : Message) (obs1 obs2 obs3 : list Observation),
    s = MkState [] (adr s) <++>
      obs1 <+> MkObservation Send m1 <++> obs2 <+> MkObservation Send m2 <++> obs3 ->
    valid_state_prop Ui s ->
      directly_observable m1 m2.
Proof.
  intros s m1 m2 obs1 obs2 obs3 Heq Hvsp.
  by eapply directly_observable_totally_orders_sent_messages_UMO_reachable,
    UMO_reachable_valid_state_prop.
Qed.

If ob belongs to the observations of a state s, we can decompose s into some state s' followed by ob and then possibly some more observations obs'.
Moreover, if the observation was a sent message m, then we know that s' is state m.

Lemma elem_of_obs_split :
  forall (s : State) (ob : Observation),
    ob ∈ obs s ->
      exists (s' : State) (obs' : list Observation),
        s = s' <+> ob <++> obs'.
Proof.
  intros s m Hin.
  apply elem_of_list_split in Hin as (obs1 & obs2 & Hobs); cbn.
  exists (MkState obs2 (adr s)), obs1.
  by apply eq_State; cbn.
Qed.

Lemma elem_of_UMO_reachable_obs_Send_split P :
  forall (s : State) (m : Message),
    MkObservation Send m ∈ obs s -> UMO_reachable P s ->
      exists obs' : list Observation,
        s = state m <+> MkObservation Send m <++> obs'.
Proof.
  intros s m Hin Hvsp.
  apply elem_of_obs_split in Hin as (s' & obs' & ->).
  exists obs'; cbn.
  do 2 f_equal.
  by apply UMO_reachable_addObservations_inv, UMO_reachable_addObservation_inv_Send_state in Hvsp.
Qed.

Lemma elem_of_UMO_reachable_obs_Send_UMO_reachable P :
  forall (s : State) (m : Message),
    MkObservation Send m ∈ obs s -> UMO_reachable P s ->
      UMO_reachable P (state m).
Proof.
  intros s m Hin Hvsp.
  destruct (elem_of_UMO_reachable_obs_Send_split _ _ _ Hin Hvsp) as [obs ->].
  by apply UMO_reachable_addObservations_inv, UMO_reachable_addObservation_inv_Send in Hvsp.
Qed.

elem_of_obs_split and elem_of_UMO_reachable_obs_Send_split can be generalized to two observations ob1 and ob2 and from there to any numbers of observations.

Lemma elem_of_obs_split_2 :
  forall (s : State) (ob1 ob2 : Observation),
    ob1 ∈ obs s -> ob2 ∈ obs s ->
      ob1 = ob2
        \/
      exists (s' : State) (obs1 obs2 : list Observation),
        s = s' <+> ob1 <++> obs1 <+> ob2 <++> obs2
          \/
        s = s' <+> ob2 <++> obs1 <+> ob1 <++> obs2.
Proof.
  intros s ob1 ob2 Hin1 Hin2.
  destruct (elem_of_list_split_2 _ _ _ Hin1 Hin2)
    as [Heq | (obs1 & obs2 & obs3 & [Heq | Heq])].
  - by left.
  - right; exists (MkState obs3 (adr s)), obs2, obs1.
    by right; apply eq_State; cbn.
  - right; exists (MkState obs3 (adr s)), obs2, obs1.
    by left; apply eq_State; cbn.
Qed.

Lemma elem_of_UMO_reachable_obs_Send_split_2 P :
  forall (s : State) (m1 m2 : Message),
    MkObservation Send m1 ∈ obs s -> MkObservation Send m2 ∈ obs s ->
    UMO_reachable P s ->
      m1 = m2
        \/
      exists obs1 obs2 : list Observation,
        s = state m1 <+> MkObservation Send m1 <++> obs1 <+> MkObservation Send m2 <++> obs2
          \/
        s = state m2 <+> MkObservation Send m2 <++> obs1 <+> MkObservation Send m1 <++> obs2.
Proof.
  intros s m1 m2 Hin1 Hin2 Hvsp.
  destruct (elem_of_obs_split_2 _ _ _ Hin1 Hin2) as [Heq | (s' & obs1 & obs2 & [Heq | Heq])].
  - by left; congruence.
  - right; exists obs1, obs2; left; subst.
    do 4 f_equal.
    by eapply UMO_reachable_addObservation_inv_Send_state,
      UMO_reachable_addObservations_inv,
      UMO_reachable_addObservation_inv,
      UMO_reachable_addObservations_inv.
  - right; exists obs1, obs2; right; subst.
    do 4 f_equal.
    by eapply UMO_reachable_addObservation_inv_Send_state,
      UMO_reachable_addObservations_inv,
      UMO_reachable_addObservation_inv,
      UMO_reachable_addObservations_inv.
Qed.

If m belongs to sentMessages of s, then its state has the same address as s.
Lemma adr_of_sentMessages P :
  forall (s : State) (m : Message),
    UMO_reachable P s -> m ∈ sentMessages s ->
      adr (state m) = adr s.
Proof.
  intros s m Hvsp Hin.
  apply elem_of_sentMessages, elem_of_obs_split in Hin as (s' & obs' & ->); cbn.
  apply UMO_reachable_addObservations_inv in Hvsp.
  by destruct s'; inversion Hvsp.
Qed.

A message m belongs to the sentMessages of state s if and only if the state state m <+> MkObservation Send m is a (possibly improper) state suffix of s.
Lemma sentMessages_characterization P :
  forall (s : State) (m : Message),
    UMO_reachable P s ->
      m ∈ sentMessages s
        <->
      let s' := state m <+> MkObservation Send m in
        state_suffix s' s \/ s' = s.
Proof.
  intros s m Hvsp; setoid_rewrite elem_of_sentMessages; split.
  - intros Hin; eapply elem_of_UMO_reachable_obs_Send_split in Hin as (obs' & ->); [| done].
    destruct obs' as [| ob obs'].
    + by right.
    + by left; apply state_suffix_addObservations; inversion 1.
  - cbn; intros [(Hadr & (ob & ->) & Hobs2) | <-].
    + by apply elem_of_app; right; constructor.
    + by constructor.
Qed.

A message m1 was sent before another message m2 if they have the same address and m1 appears in sentMessages of the state of m2.
Definition was_sent_before (m1 m2 : Message) : Prop :=
  adr (state m1) = adr (state m2) /\ m1 ∈ sentMessages (state m2).

We can characterize was_sent_before in terms of state_suffix in two different ways, provided that the state of m2 is reachable.

Lemma was_sent_before_characterization_1 P :
  forall m1 m2 : Message,
    UMO_reachable P (state m2) ->
      was_sent_before m1 m2
        <->
      let s := state m1 <+> MkObservation Send m1 in
        state_suffix s (state m2) \/ s = state m2.
Proof.
  intros m1 m2 Hvsp; split.
  - intros [Hadr Hsent].
    apply elem_of_sentMessages in Hsent.
    eapply elem_of_UMO_reachable_obs_Send_split in Hsent as (obs' & ->); [| done].
    destruct obs' as [| ob' obs']; cbn.
    + by right.
    + by left; apply state_suffix_addObservations; inversion 1.
  - intros [(Hadr & Hsuf & Hnsuf) | Heq]; cbn in *.
    + constructor; [done |].
      apply elem_of_sentMessages.
      destruct Hsuf as [obs' ->].
      unfold addObservation'.
      by rewrite elem_of_app, elem_of_cons; right; left.
    + constructor.
      * by apply (f_equal adr) in Heq; cbn in Heq.
      * by rewrite <- Heq; setoid_rewrite elem_of_sentMessages; left.
Qed.

Lemma was_sent_before_characterization_2 P :
  forall m1 m2 : Message,
    UMO_reachable P (state m2) ->
      was_sent_before m1 m2
        <->
      state_suffix (state m1 <+> MkObservation Send m1) (state m2 <+> MkObservation Send m2).
Proof.
  intros m1 m2 Hvsp; split.
  - intros [Hadr Hsent].
    eapply elem_of_sentMessages, elem_of_UMO_reachable_obs_Send_split
      in Hsent as (obs' & ->); [| done].
    cbn; rewrite addObservation_cons.
    by apply state_suffix_addObservations; inversion 1.
  - intros (Hadr & Hsuf & Hnsuf).
    constructor; [done |].
    apply elem_of_sentMessages.
    destruct Hsuf as [obs' Heq].
    cbn in Heq; unfold addObservation' in Heq.
    unfold addObservation'.
    destruct obs' as [| ob' obs']; inversion Heq; subst.
    + by contradiction Hnsuf.
    + by rewrite H1, elem_of_app, elem_of_cons; right; left.
Qed.

The relation was_sent_before is trichotomous on the sentMessages of any reachable state.
Lemma was_sent_before_totally_orders_sentMessages_UMO_reachable P :
  forall (s : State) (m1 m2 : Message),
    UMO_reachable P s -> m1 ∈ sentMessages s -> m2 ∈ sentMessages s ->
      was_sent_before m1 m2 \/ m1 = m2 \/ was_sent_before m2 m1.
Proof.
  intros s m1 m2 Hvsp Hin1 Hin2.
  apply elem_of_sentMessages in Hin1, Hin2.
  assert (Hvsp1 : UMO_reachable P (state m1))
    by (eapply elem_of_UMO_reachable_obs_Send_UMO_reachable; done).
  assert (Hvsp2 : UMO_reachable P (state m2))
    by (eapply elem_of_UMO_reachable_obs_Send_UMO_reachable; done).
  destruct (elem_of_UMO_reachable_obs_Send_split_2 P s m1 m2 Hin1 Hin2)
    as [Heq | (obs1 & obs2 & [-> | ->])]; [done | | |]; clear Hin1 Hin2.
  - by right; left.
  - left.
    rewrite was_sent_before_characterization_2; [| done].
    apply UMO_reachable_addObservations_inv,
          UMO_reachable_addObservation_inv_Send_state in Hvsp.
    rewrite <- Hvsp, addObservation_cons.
    by apply state_suffix_addObservations; inversion 1.
  - right; right.
    rewrite was_sent_before_characterization_2; [| done].
    apply UMO_reachable_addObservations_inv,
          UMO_reachable_addObservation_inv_Send_state in Hvsp.
    rewrite <- Hvsp, addObservation_cons.
    by apply state_suffix_addObservations; inversion 1.
Qed.

Messages m1 and m2 are sent_comparable when m1 = m2 or was_sent_before m1 m2 or was_sent_before m2 m1.
Inductive sent_comparable : Message -> Message -> Prop :=
| sc_refl : forall m : Message, sent_comparable m m
| sc_wsb_l : forall m1 m2 : Message, was_sent_before m1 m2 -> sent_comparable m1 m2
| sc_wsb_r : forall m1 m2 : Message, was_sent_before m2 m1 -> sent_comparable m1 m2.

Messages m1 and m2 are incomparable if they have the same sender and are not sent_comparable.
Note that incomparable is not simply a negation of sent_comparable, so that there can be messages which are neither sent_comparable nor incomparable.
Definition incomparable (m1 m2 : Message) : Prop :=
  adr (state m1) = adr (state m2) /\ ~ sent_comparable m1 m2.

End sec_UMO_component_lemmas.

#[export] Instance sent_comparable_sym : Symmetric sent_comparable.
Proof. by intros x y []; constructor. Defined.

#[export] Instance sent_comparable_dec : RelDecision sent_comparable.
Proof.
  intros m1 m2.
  destruct (decide (adr (state m1) = adr (state m2)));
    [| by right; destruct 1; apply n; firstorder congruence].
  destruct (decide (obs (state m1) = obs (state m2)));
    [by left; replace m2 with m1 by (apply eq_Message; done); constructor |].
  destruct (decide (m1 ∈ sentMessages (state m2)));
    [by left; constructor; constructor |].
  destruct (decide (m2 ∈ sentMessages (state m1)));
    [by left; constructor; constructor |].
  by right; destruct 1; firstorder.
Defined.

#[export] Instance incomparable_sym : Symmetric incomparable.
Proof. by intros x y []; constructor. Defined.

Section sec_UMOProtocol.

Context
  (index : Type)
  `{finite.Finite index}
  (idx : index -> Address)
  `{!Inj (=) (=) idx}
  (U : index -> VLSM Message := fun i => UMO_component (idx i))
  .

Protocol

The UMO protocol is a free composition of finitely many UMO components.

Definition UMO : VLSM Message := free_composite_vlsm U.

We set up aliases for some functions operating on free VLSM composition.

Definition UMO_state : Type := composite_state U.
Definition UMO_label : Type := composite_label U.
Definition UMO_transition_item : Type := composite_transition_item U.

We can lift labels, states and traces from an UMO component to the UMO protocol.

Definition lift_to_UMO_label
  (i : index) (li : VLSM.label (U i)) : UMO_label :=
    lift_to_composite_label U i li.

Definition lift_to_UMO_state
  (us : UMO_state) (i : index) (si : VLSM.state (U i)) : UMO_state :=
    lift_to_composite_state U us i si.

Definition lift_to_UMO_trace
  (us : UMO_state) (i : index) (tr : list (transition_item (U i)))
  : list UMO_transition_item :=
    pre_VLSM_embedding_finite_trace_project
      _ _ (lift_to_UMO_label i) (lift_to_UMO_state us i) tr.

We can also lift properties from UMO components to the UMO protocol, among them valid_state_prop, valid_message_prop, input_valid_transition and the various kinds of traces.

Lemma lift_to_UMO :
  forall (us : UMO_state) (Hus : valid_state_prop UMO us) (i : index),
    VLSM_weak_embedding (U i) UMO (lift_to_UMO_label i) (lift_to_UMO_state us i).
Proof. by intros; apply lift_to_free_weak_embedding. Qed.

Lemma lift_to_UMO_valid_state_prop :
  forall (i : index) (s : State) (us : UMO_state),
    valid_state_prop UMO us -> valid_state_prop (U i) s ->
      valid_state_prop UMO (lift_to_UMO_state us i s).
Proof.
  intros is s us Hvsp.
  by eapply VLSM_weak_embedding_valid_state, lift_to_UMO.
Qed.

Lemma lift_to_UMO_valid_message_prop :
  forall (i : index) (om : option Message),
    option_valid_message_prop (U i) om ->
      option_valid_message_prop UMO om.
Proof.
  intros i [] Hovmp; cycle 1.
  - exists (fun i => MkState [] (idx i)). by constructor; compute.
  - eapply VLSM_weak_embedding_valid_message.
    + by apply (lift_to_UMO (fun i => MkState [] (idx i))); exists None; constructor.
    + by inversion 1.
    + by apply Hovmp.
Qed.

Lemma lift_to_UMO_input_valid_transition :
  forall (i : index) (lbl : Label) (s1 s2 : State) (iom oom : option Message) (us : UMO_state),
    valid_state_prop UMO us ->
    input_valid_transition (U i) lbl (s1, iom) (s2, oom) ->
      input_valid_transition UMO
        (lift_to_UMO_label i lbl)
        (lift_to_UMO_state us i s1, iom)
        (lift_to_UMO_state us i s2, oom).
Proof.
  intros i lbl s1 s2 iom oom us Hivt.
  by apply @VLSM_weak_embedding_input_valid_transition, lift_to_UMO.
Qed.

Lemma lift_to_UMO_finite_valid_trace_from_to :
  forall (i : index) (s1 s2 : State) (tr : list (transition_item (U i))) (us : UMO_state),
    valid_state_prop UMO us ->
    finite_valid_trace_from_to (U i) s1 s2 tr ->
      finite_valid_trace_from_to
        UMO (lift_to_UMO_state us i s1) (lift_to_UMO_state us i s2) (lift_to_UMO_trace us i tr).
Proof.
  intros i s1 s2 tr us Hvsp Hfvt.
  by eapply (VLSM_weak_embedding_finite_valid_trace_from_to (lift_to_UMO _ Hvsp i)).
Qed.

Lemma lift_to_UMO_finite_constrained_trace_from_to :
  forall (i : index) (s1 s2 : State) (tr : list (transition_item (U i))) (us : UMO_state),
    constrained_state_prop UMO us ->
    finite_constrained_trace_from_to (U i) s1 s2 tr ->
      finite_constrained_trace_from_to UMO
        (lift_to_UMO_state us i s1) (lift_to_UMO_state us i s2) (lift_to_UMO_trace us i tr).
Proof.
  intros i s1 s2 tr us Hvsp Hfvt.
  unshelve eapply (@VLSM_weak_embedding_finite_valid_trace_from_to _
    (preloaded_with_all_messages_vlsm (U i))
    (preloaded_with_all_messages_vlsm UMO) _ _); [| done].
  by eapply lift_to_preloaded_free_weak_embedding.
Qed.

Lemma lift_to_UMO_constrained_state_prop :
  forall (i : index) (s : State) (us : UMO_state),
    constrained_state_prop UMO us ->
    constrained_state_prop (U i) s ->
    constrained_state_prop UMO (lift_to_UMO_state us i s).
Proof.
  unfold constrained_state_prop.
  intros is s us Hcsp.
  by eapply VLSM_weak_embedding_valid_state, lift_to_preloaded_free_weak_embedding.
Qed.

Every state in a UMO component gives rise to a unique trace leading to this state, which we can then lift to the UMO protocol.
Definition UMO_component_state2trace
  (s : UMO_state) (i : index) : list UMO_transition_item :=
    lift_to_UMO_trace s i (state2trace (s i)).

Iterating UMO_component_state2trace shows that every reachable UMO state contains a trace that leads to this state. However, this trace is not unique, because we can concatenate the lifted traces in any order.
Fixpoint UMO_state2trace_aux
  (us : UMO_state) (is : list index) : list UMO_transition_item :=
  match is with
  | [] => []
  | i :: is' =>
    UMO_state2trace_aux (state_update _ us i (MkState [] (idx i))) is' ++
    UMO_component_state2trace us i
  end.

Definition UMO_state2trace
  (us : UMO_state) : list UMO_transition_item :=
    UMO_state2trace_aux us (enum index).

Lemma finite_constrained_trace_init_to_UMO_state2trace :
  forall us : UMO_state,
    constrained_state_prop UMO us ->
      finite_constrained_trace_init_to UMO (``(vs0 UMO)) us (UMO_state2trace us).
Proof.
  intros us Hvsp; split; [| done].
  unfold UMO_state2trace.
  assert (Hall : forall i, i ∉ enum index -> us i = MkState [] (idx i))
      by (intros i Hin; contradict Hin; apply elem_of_enum).
  revert us Hall Hvsp.
  generalize (enum index) as is.
  induction is as [| i is']; cbn; intros us Hall Hvsp.
  - replace us with (fun n : index => MkState [] (idx n)).
    + by constructor; apply initial_state_is_valid; compute.
    + extensionality i; rewrite Hall; [done |].
      by apply not_elem_of_nil.
  - eapply finite_valid_trace_from_to_app.
    + apply IHis'.
      * intros j Hj. destruct (decide (i = j)); subst; state_update_simpl; [done |].
        apply Hall. rewrite elem_of_cons. by intros [].
      * by apply pre_composite_free_update_state_with_initial.
    + replace us with (state_update U us i (us i)) at 2 by (state_update_simpl; done).
      apply lift_to_UMO_finite_constrained_trace_from_to; [done |].
      apply (composite_constrained_state_project _ us i) in Hvsp as Hvsp'.
      apply valid_state_has_trace in Hvsp' as (s & tr & [Hfvt Hinit]).
      replace s with (MkState [] (idx i)) in *; cycle 1.
      * by inversion Hinit; destruct s; cbn in *; subst.
      * by eapply finite_constrained_trace_init_to_state2trace.
Qed.

It turns out that finite_constrained_trace_init_to_UMO_state2trace also holds for valid states.
Lemma finite_valid_trace_from_to_UMO_state2trace :
  forall us : UMO_state,
    valid_state_prop UMO us ->
      finite_valid_trace_init_to UMO (``(vs0 UMO)) us (UMO_state2trace us).
Proof.
  intros us Hvsp.
  apply all_pre_traces_to_valid_state_are_valid_free; [typeclasses eauto | done |].
  apply finite_constrained_trace_init_to_UMO_state2trace.
  eapply (@VLSM_incl_valid_state _ UMO UMO); [| done].
  by apply vlsm_incl_preloaded_with_all_messages_vlsm.
Qed.

Fixpoint UMO_obs_aux (us : UMO_state) (is : list index) : list Observation :=
  match is with
  | [] => []
  | i :: is' => UMO_obs_aux (state_update _ us i (MkState [] (idx i))) is' ++ obs (us i)
  end.

Definition UMO_obs (us : UMO_state) : list Observation :=
  UMO_obs_aux us (enum index).

Fixpoint UMO_sentMessages_aux (us : UMO_state) (is : list index) : set Message :=
  match is with
  | [] => []
  | i :: is' =>
    UMO_sentMessages_aux (state_update _ us i (MkState [] (idx i))) is' ++ sentMessages (us i)
  end.

Definition UMO_sentMessages (us : UMO_state) : set Message :=
  UMO_sentMessages_aux us (enum index).

Fixpoint UMO_receivedMessages_aux (us : UMO_state) (is : list index) : set Message :=
  match is with
  | [] => []
  | i :: is' =>
    UMO_receivedMessages_aux (state_update _ us i (MkState [] (idx i))) is' ++ receivedMessages (us i)
  end.

Definition UMO_receivedMessages (us : UMO_state) : set Message :=
  UMO_receivedMessages_aux us (enum index).

Fixpoint UMO_messages_aux (us : UMO_state) (is : list index) : set Message :=
  match is with
  | [] => []
  | i :: is' =>
    UMO_messages_aux (state_update _ us i (MkState [] (idx i))) is' ++ messages (us i)
  end.

Definition UMO_messages (us : UMO_state) : set Message :=
  UMO_messages_aux us (enum index).

Lemma constrained_state_prop_state_update_init :
  forall (us : UMO_state) (i : index),
    constrained_state_prop UMO us ->
      constrained_state_prop UMO (state_update U us i (MkState [] (idx i))).
Proof.
  intros us i Hvsp.
  by apply pre_composite_free_update_state_with_initial.
Qed.

Lemma elem_of_UMO_sentMessages :
  forall (us : UMO_state) (m : Message) (i : index),
    constrained_state_prop UMO us -> idx i = adr (state m) ->
      m ∈ UMO_sentMessages us <-> m ∈ sentMessages (us i).
Proof.
  intros us m i Hvsp Hidx.
  assert (Hall : forall i, i ∉ enum index -> us i = MkState [] (idx i))
    by (intros j Hin; contradict Hin; apply elem_of_enum).
  revert us m i Hvsp Hidx Hall.
  unfold UMO_sentMessages; generalize (enum index) as is.
  induction is as [| i' is']; intros; [by rewrite Hall; [| apply not_elem_of_nil] |].
  cbn in *; unfold State, Observation, Message in *; rewrite elem_of_app.
  assert (Hvsp' :
    forall j, constrained_state_prop (UMO_component (idx j)) (us j))
    by (intro j; apply (preloaded_valid_state_projection _ _ _ Hvsp); done).
  split; cycle 1.
  - intros Hin.
    destruct (decide (i = i')); subst; [by right |].
    left. unfold Message, State, Observation in *; cbn.
    rewrite (IHis' (state_update U us i' (MkState [] (idx i'))) m i).
    + by state_update_simpl.
    + by apply constrained_state_prop_state_update_init.
    + erewrite adr_of_sentMessages, adr_of_constrained_state; [done | .. | done].
      * by rewrite <- Hidx; apply Hvsp'.
      * by eapply UMO_reachable_constrained_state_prop, Hvsp'.
    + intros j Hnin. destruct (decide (i' = j)); subst.
      * by state_update_simpl.
      * by state_update_simpl; apply Hall; inversion 1.
  - intros [Hin | Hin]; cycle 1.
    + eapply adr_of_sentMessages in Hin as Hin';
        [| by eapply UMO_reachable_constrained_state_prop, Hvsp'].
      erewrite Hin', adr_of_constrained_state in Hidx by apply Hvsp'.
      by apply Inj0 in Hidx; subst.
    + rewrite (IHis' _ _ i) in Hin; [| | done |].
      * by destruct (decide (i = i')); subst; state_update_simpl; [inversion Hin |].
      * by apply constrained_state_prop_state_update_init.
      * intros j Hnin. destruct (decide (i' = j)); subst; state_update_simpl; [done |].
        by apply Hall; inversion 1.
Qed.

Lemma UMO_sentMessages_characterization :
  forall (us : UMO_state) (m : Message) (i : index),
    constrained_state_prop UMO us -> idx i = adr (state m) ->
      m ∈ UMO_sentMessages us
        <->
      let s' := state m <+> MkObservation Send m in
        state_suffix s' (us i) \/ s' = us i.
Proof.
  intros us m i Hvsp Hidx.
  rewrite elem_of_UMO_sentMessages by done.
  rewrite <- sentMessages_characterization; [done |].
  by apply @UMO_reachable_constrained_state_prop with (idx i),
    (preloaded_valid_state_projection _ _ _ Hvsp).
Qed.

End sec_UMOProtocol.

End sec_UMO.

Arguments UMO_reachable_ind' [Address]%type_scope (C P Hinit Hextend)%function_scope s Hs.