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

Core: VLSM Plans

A plan is a (sequence of actions) which can be attempted on a given state to yield a trace.

Section sec_plans.

Context
  {message : Type}
  {T : VLSMType message}.

A plan_item is a singleton plan, and contains a label and an input which would allow to transition from any given state (note that we don't address validity for now).

Record plan_item : Type :=
{
  label_a : label T;
  input_a : option message;
}.

End sec_plans.

Arguments plan_item {message T}, {message} T.
Arguments Build_plan_item {message T}, {message} T.

Section sec_apply_plans.

Context
  {message : Type}
  {T : VLSMType message}
  {transition : label T -> state T * option message -> state T * option message}
  .

If we don't concern ourselves with the validity of the traces obtained upon applying a plan, then a VLSMType and a transition function suffice for defining plan application and related results. The advantage of this approach is that the same definition works for preloaded versions as well as for all constrained variants of a composition.

Applying a plan (list of plan_items) to a state we obtain a final state and a trace. We define that in the _apply_plan definition below using a folding operation on the _apply_plan_folder function.

Definition _apply_plan_folder
  (a : plan_item)
  (sl : state T * list transition_item)
  : state T * list transition_item
  :=
  let (s, items) := sl in
  match a with {| label_a := l'; input_a := input' |} =>
    let (dest, out) := (transition l' (s, input')) in
    (dest
    , {| l := l';
         input := input';
         output := out;
         destination := dest
       |} :: items)
  end.

Lemma _apply_plan_folder_additive
  (start : state T)
  (aitems : list plan_item)
  (seed_items : list transition_item)
  : let (final, items) := fold_right _apply_plan_folder (start, []) aitems in
    fold_right _apply_plan_folder (start, seed_items) aitems = (final, items ++ seed_items).message: Type
T: VLSMType message
transition: label T
→ state T * option message
  → state T * option message
start: state T
aitems: list plan_item
seed_items: list transition_item
let (final, items) :=
  foldr _apply_plan_folder (start, []) aitems in
foldr _apply_plan_folder (start, seed_items) aitems =
(final, items ++ seed_items)
Proof.message: Type
T: VLSMType message
transition: label T
→ state T * option message
  → state T * option message
start: state T
aitems: list plan_item
seed_items: list transition_item
let (final, items) :=
  foldr _apply_plan_folder (start, []) aitems in
foldr _apply_plan_folder (start, seed_items) aitems =
(final, items ++ seed_items)
  generalize dependent seed_items.message: Type
T: VLSMType message
transition: label T
→ state T * option message
  → state T * option message
start: state T
aitems: list plan_item
∀ seed_items : list transition_item,
  let (final, items) :=
    foldr _apply_plan_folder (start, []) aitems in
  foldr _apply_plan_folder (start, seed_items) aitems =
  (final, items ++ seed_items)
  induction aitems; simpl; intros; [done |].message: Type
T: VLSMType message
transition: label T
→ state T * option message
  → state T * option message
start: state T
a: plan_item
aitems: list plan_item
IHaitems: ∀ seed_items : list transition_item,
  let (final, items) :=
    foldr _apply_plan_folder (
      start, []) aitems in
  foldr _apply_plan_folder
    (start, seed_items) aitems =
  (final, items ++ seed_items)
seed_items: list transition_item
let (final, items) :=
  _apply_plan_folder a
    (foldr _apply_plan_folder (start, []) aitems) in
_apply_plan_folder a
  (foldr _apply_plan_folder (start, seed_items) aitems) =
(final, items ++ seed_items)
  destruct (fold_right _apply_plan_folder (start, []) aitems) as (afinal, aitemsX).message: Type
T: VLSMType message
transition: label T
→ state T * option message
  → state T * option message
start: state T
a: plan_item
aitems: list plan_item
afinal: state T
aitemsX: list transition_item
IHaitems: ∀ seed_items : list transition_item,
  foldr _apply_plan_folder
    (start, seed_items) aitems =
  (afinal, aitemsX ++ seed_items)
seed_items: list transition_item
let (final, items) :=
  _apply_plan_folder a (afinal, aitemsX) in
_apply_plan_folder a
  (foldr _apply_plan_folder (start, seed_items) aitems) =
(final, items ++ seed_items)
  rewrite IHaitems; cbn.message: Type
T: VLSMType message
transition: label T
→ state T * option message
  → state T * option message
start: state T
a: plan_item
aitems: list plan_item
afinal: state T
aitemsX: list transition_item
IHaitems: ∀ seed_items : list transition_item,
  foldr _apply_plan_folder
    (start, seed_items) aitems =
  (afinal, aitemsX ++ seed_items)
seed_items: list transition_item
let (final, items) :=
  match a with
  | {| label_a := l'; input_a := input' |} =>
      let (dest, out) :=
        transition l' (afinal, input') in
      (dest,
       {|
         l := l';
         input := input';
         destination := dest;
         output := out
       |} :: aitemsX)
  end in
match a with
| {| label_a := l'; input_a := input' |} =>
    let (dest, out) :=
      transition l' (afinal, input') in
    (dest,
     {|
       l := l';
       input := input';
       destination := dest;
       output := out
     |} :: aitemsX ++ seed_items)
end = (final, items ++ seed_items)
  by destruct a, (transition label_a0 (afinal, input_a0)) as [dest out].
Qed.

Definition _apply_plan
  (start : state T)
  (a : list plan_item)
  : list transition_item * state T
  :=
  let (final, items) :=
    fold_right _apply_plan_folder (@pair (state T) _ start []) (rev a) in
  (rev items, final).

Lemma _apply_plan_last
  (start : state T)
  (a : list plan_item)
  (after_a := _apply_plan start a)
  : finite_trace_last start (fst after_a) = snd after_a.message: Type
T: VLSMType message
transition: label T
→ state T * option message
  → state T * option message
start: state T
a: list plan_item
after_a:= _apply_plan start a: (list transition_item * state T)%type
finite_trace_last start after_a.1 = after_a.2
Proof.message: Type
T: VLSMType message
transition: label T
→ state T * option message
  → state T * option message
start: state T
a: list plan_item
after_a:= _apply_plan start a: (list transition_item * state T)%type
finite_trace_last start after_a.1 = after_a.2
  induction a using rev_ind; [done |].message: Type
T: VLSMType message
transition: label T
→ state T * option message
  → state T * option message
start: state T
x: plan_item
a: list plan_item
after_a:= _apply_plan start (a ++ [x]): (list transition_item * state T)%type
IHa: let after_a := _apply_plan start a in
finite_trace_last start after_a.1 = after_a.2
finite_trace_last start after_a.1 = after_a.2
  unfold after_a.message: Type
T: VLSMType message
transition: label T
→ state T * option message
  → state T * option message
start: state T
x: plan_item
a: list plan_item
after_a:= _apply_plan start (a ++ [x]): (list transition_item * state T)%type
IHa: let after_a := _apply_plan start a in
finite_trace_last start after_a.1 = after_a.2
finite_trace_last start
  (_apply_plan start (a ++ [x])).1 =
(_apply_plan start (a ++ [x])).2 clear after_a.message: Type
T: VLSMType message
transition: label T
→ state T * option message
  → state T * option message
start: state T
x: plan_item
a: list plan_item
IHa: let after_a := _apply_plan start a in
finite_trace_last start after_a.1 = after_a.2
finite_trace_last start
  (_apply_plan start (a ++ [x])).1 =
(_apply_plan start (a ++ [x])).2 unfold _apply_plan.message: Type
T: VLSMType message
transition: label T
→ state T * option message
  → state T * option message
start: state T
x: plan_item
a: list plan_item
IHa: let after_a := _apply_plan start a in
finite_trace_last start after_a.1 = after_a.2
finite_trace_last start
  (let (final, items) :=
     foldr _apply_plan_folder (start, [])
       (rev (a ++ [x])) in
   (rev items, final)).1 =
(let (final, items) :=
   foldr _apply_plan_folder (start, [])
     (rev (a ++ [x])) in
 (rev items, final)).2
  rewrite rev_unit.message: Type
T: VLSMType message
transition: label T
→ state T * option message
  → state T * option message
start: state T
x: plan_item
a: list plan_item
IHa: let after_a := _apply_plan start a in
finite_trace_last start after_a.1 = after_a.2
finite_trace_last start
  (let (final, items) :=
     foldr _apply_plan_folder (start, []) (x :: rev a) in
   (rev items, final)).1 =
(let (final, items) :=
   foldr _apply_plan_folder (start, []) (x :: rev a) in
 (rev items, final)).2 unfold _apply_plan in IHa.message: Type
T: VLSMType message
transition: label T
→ state T * option message
  → state T * option message
start: state T
x: plan_item
a: list plan_item
IHa: finite_trace_last start
  (let (final, items) :=
     foldr _apply_plan_folder (
       start, []) (rev a) in
   (rev items, final)).1 =
(let (final, items) :=
   foldr _apply_plan_folder (start, []) (rev a) in
 (rev items, final)).2
finite_trace_last start
  (let (final, items) :=
     foldr _apply_plan_folder (start, []) (x :: rev a) in
   (rev items, final)).1 =
(let (final, items) :=
   foldr _apply_plan_folder (start, []) (x :: rev a) in
 (rev items, final)).2
  simpl in *.message: Type
T: VLSMType message
transition: label T
→ state T * option message
  → state T * option message
start: state T
x: plan_item
a: list plan_item
IHa: finite_trace_last start
  (let (final, items) :=
     foldr _apply_plan_folder (
       start, []) (rev a) in
   (rev items, final)).1 =
(let (final, items) :=
   foldr _apply_plan_folder (start, []) (rev a) in
 (rev items, final)).2
finite_trace_last start
  (let (final, items) :=
     _apply_plan_folder x
       (foldr _apply_plan_folder (start, []) (rev a)) in
   (rev items, final)).1 =
(let (final, items) :=
   _apply_plan_folder x
     (foldr _apply_plan_folder (start, []) (rev a)) in
 (rev items, final)).2
  destruct (fold_right _apply_plan_folder (start, []) (rev a)) as (final, items)
    eqn: Happly.message: Type
T: VLSMType message
transition: label T
→ state T * option message
  → state T * option message
start: state T
x: plan_item
a: list plan_item
final: state T
items: list transition_item
Happly: foldr _apply_plan_folder (start, []) (rev a) =
(final, items)
IHa: finite_trace_last start (rev items, final).1 =
(rev items, final).2
finite_trace_last start
  (let (final, items) :=
     _apply_plan_folder x (final, items) in
   (rev items, final)).1 =
(let (final, items) :=
   _apply_plan_folder x (final, items) in
 (rev items, final)).2
  simpl in IHa.message: Type
T: VLSMType message
transition: label T
→ state T * option message
  → state T * option message
start: state T
x: plan_item
a: list plan_item
final: state T
items: list transition_item
Happly: foldr _apply_plan_folder (start, []) (rev a) =
(final, items)
IHa: finite_trace_last start (rev items) = final
finite_trace_last start
  (let (final, items) :=
     _apply_plan_folder x (final, items) in
   (rev items, final)).1 =
(let (final, items) :=
   _apply_plan_folder x (final, items) in
 (rev items, final)).2
  simpl.message: Type
T: VLSMType message
transition: label T
→ state T * option message
  → state T * option message
start: state T
x: plan_item
a: list plan_item
final: state T
items: list transition_item
Happly: foldr _apply_plan_folder (start, []) (rev a) =
(final, items)
IHa: finite_trace_last start (rev items) = final
finite_trace_last start
  (let (final, items) :=
     match x with
     | {| label_a := l'; input_a := input' |} =>
         let (dest, out) :=
           transition l' (final, input') in
         (dest,
          {|
            l := l';
            input := input';
            destination := dest;
            output := out
          |} :: items)
     end in
   (rev items, final)).1 =
(let (final, items) :=
   match x with
   | {| label_a := l'; input_a := input' |} =>
       let (dest, out) :=
         transition l' (final, input') in
       (dest,
        {|
          l := l';
          input := input';
          destination := dest;
          output := out
        |} :: items)
   end in
 (rev items, final)).2
  destruct x.message: Type
T: VLSMType message
transition: label T
→ state T * option message
  → state T * option message
start: state T
label_a0: label T
input_a0: option message
a: list plan_item
final: state T
items: list transition_item
Happly: foldr _apply_plan_folder (start, []) (rev a) =
(final, items)
IHa: finite_trace_last start (rev items) = final
finite_trace_last start
  (let (final, items) :=
     let (dest, out) :=
       transition label_a0 (final, input_a0) in
     (dest,
      {|
        l := label_a0;
        input := input_a0;
        destination := dest;
        output := out
      |} :: items) in
   (rev items, final)).1 =
(let (final, items) :=
   let (dest, out) :=
     transition label_a0 (final, input_a0) in
   (dest,
    {|
      l := label_a0;
      input := input_a0;
      destination := dest;
      output := out
    |} :: items) in
 (rev items, final)).2
  destruct (transition label_a0 (final, input_a0)) as (dest, out) eqn: Ht.message: Type
T: VLSMType message
transition: label T
→ state T * option message
  → state T * option message
start: state T
label_a0: label T
input_a0: option message
a: list plan_item
final: state T
items: list transition_item
Happly: foldr _apply_plan_folder (start, []) (rev a) =
(final, items)
IHa: finite_trace_last start (rev items) = final
dest: state T
out: option message
Ht: transition label_a0 (final, input_a0) =
(dest, out)
finite_trace_last start
  (rev
     ({|
        l := label_a0;
        input := input_a0;
        destination := dest;
        output := out
      |} :: items), dest).1 =
(rev
   ({|
      l := label_a0;
      input := input_a0;
      destination := dest;
      output := out
    |} :: items), dest).2
  by simpl; rewrite finite_trace_last_is_last.
Qed.

Lemma _apply_plan_app
  (start : state T)
  (a a' : list plan_item)
  : _apply_plan start (a ++ a') =
    let (aitems, afinal) := _apply_plan start a in
    let (a'items, a'final) := _apply_plan afinal a' in
     (aitems ++ a'items, a'final).message: Type
T: VLSMType message
transition: label T
→ state T * option message
  → state T * option message
start: state T
a, a': list plan_item
_apply_plan start (a ++ a') =
(let (aitems, afinal) := _apply_plan start a in
 let (a'items, a'final) := _apply_plan afinal a' in
 (aitems ++ a'items, a'final))
Proof.message: Type
T: VLSMType message
transition: label T
→ state T * option message
  → state T * option message
start: state T
a, a': list plan_item
_apply_plan start (a ++ a') =
(let (aitems, afinal) := _apply_plan start a in
 let (a'items, a'final) := _apply_plan afinal a' in
 (aitems ++ a'items, a'final))
  unfold _apply_plan.message: Type
T: VLSMType message
transition: label T
→ state T * option message
  → state T * option message
start: state T
a, a': list plan_item
(let (final, items) :=
   foldr _apply_plan_folder (start, [])
     (rev (a ++ a')) in
 (rev items, final)) =
(let (aitems, afinal) :=
   let (final, items) :=
     foldr _apply_plan_folder (start, []) (rev a) in
   (rev items, final) in
 let (a'items, a'final) :=
   let (final, items) :=
     foldr _apply_plan_folder (afinal, []) (rev a') in
   (rev items, final) in
 (aitems ++ a'items, a'final))
  rewrite rev_app_distr.message: Type
T: VLSMType message
transition: label T
→ state T * option message
  → state T * option message
start: state T
a, a': list plan_item
(let (final, items) :=
   foldr _apply_plan_folder (start, [])
     (rev a' ++ rev a) in
 (rev items, final)) =
(let (aitems, afinal) :=
   let (final, items) :=
     foldr _apply_plan_folder (start, []) (rev a) in
   (rev items, final) in
 let (a'items, a'final) :=
   let (final, items) :=
     foldr _apply_plan_folder (afinal, []) (rev a') in
   (rev items, final) in
 (aitems ++ a'items, a'final))
  rewrite fold_right_app.message: Type
T: VLSMType message
transition: label T
→ state T * option message
  → state T * option message
start: state T
a, a': list plan_item
(let (final, items) :=
   foldr _apply_plan_folder
     (foldr _apply_plan_folder (start, []) (rev a))
     (rev a') in
 (rev items, final)) =
(let (aitems, afinal) :=
   let (final, items) :=
     foldr _apply_plan_folder (start, []) (rev a) in
   (rev items, final) in
 let (a'items, a'final) :=
   let (final, items) :=
     foldr _apply_plan_folder (afinal, []) (rev a') in
   (rev items, final) in
 (aitems ++ a'items, a'final)) simpl.message: Type
T: VLSMType message
transition: label T
→ state T * option message
  → state T * option message
start: state T
a, a': list plan_item
(let (final, items) :=
   foldr _apply_plan_folder
     (foldr _apply_plan_folder (start, []) (rev a))
     (rev a') in
 (rev items, final)) =
(let (aitems, afinal) :=
   let (final, items) :=
     foldr _apply_plan_folder (start, []) (rev a) in
   (rev items, final) in
 let (a'items, a'final) :=
   let (final, items) :=
     foldr _apply_plan_folder (afinal, []) (rev a') in
   (rev items, final) in
 (aitems ++ a'items, a'final))
  destruct
    (fold_right _apply_plan_folder (@pair (state T) _ start []) (rev  a))
    as (afinal, aitems) eqn: Ha.message: Type
T: VLSMType message
transition: label T
→ state T * option message
  → state T * option message
start: state T
a, a': list plan_item
afinal: state T
aitems: list transition_item
Ha: foldr _apply_plan_folder (start, []) (rev a) =
(afinal, aitems)
(let (final, items) :=
   foldr _apply_plan_folder (afinal, aitems) (rev a') in
 (rev items, final)) =
(let (a'items, a'final) :=
   let (final, items) :=
     foldr _apply_plan_folder (afinal, []) (rev a') in
   (rev items, final) in
 (rev aitems ++ a'items, a'final))
  destruct
    (fold_right _apply_plan_folder (@pair (state T) _ afinal []) (rev a'))
    as (final, items) eqn: Ha'.message: Type
T: VLSMType message
transition: label T
→ state T * option message
  → state T * option message
start: state T
a, a': list plan_item
afinal: state T
aitems: list transition_item
Ha: foldr _apply_plan_folder (start, []) (rev a) =
(afinal, aitems)
final: state T
items: list transition_item
Ha': foldr _apply_plan_folder (afinal, []) (rev a') =
(final, items)
(let (final, items) :=
   foldr _apply_plan_folder (afinal, aitems) (rev a') in
 (rev items, final)) =
(rev aitems ++ rev items, final)
  clear - Ha'.message: Type
T: VLSMType message
transition: label T
→ state T * option message
  → state T * option message
a': list plan_item
afinal: state T
aitems: list transition_item
final: state T
items: list transition_item
Ha': foldr _apply_plan_folder (afinal, []) (rev a') =
(final, items)
(let (final, items) :=
   foldr _apply_plan_folder (afinal, aitems) (rev a') in
 (rev items, final)) =
(rev aitems ++ rev items, final)
  specialize (_apply_plan_folder_additive afinal (rev a') aitems) as Hadd.message: Type
T: VLSMType message
transition: label T
→ state T * option message
  → state T * option message
a': list plan_item
afinal: state T
aitems: list transition_item
final: state T
items: list transition_item
Ha': foldr _apply_plan_folder (afinal, []) (rev a') =
(final, items)
Hadd: let (final, items) :=
  foldr _apply_plan_folder (
    afinal, []) (rev a') in
foldr _apply_plan_folder (
  afinal, aitems) (rev a') =
(final, items ++ aitems)
(let (final, items) :=
   foldr _apply_plan_folder (afinal, aitems) (rev a') in
 (rev items, final)) =
(rev aitems ++ rev items, final)
  rewrite Ha' in Hadd.message: Type
T: VLSMType message
transition: label T
→ state T * option message
  → state T * option message
a': list plan_item
afinal: state T
aitems: list transition_item
final: state T
items: list transition_item
Ha': foldr _apply_plan_folder (afinal, []) (rev a') =
(final, items)
Hadd: foldr _apply_plan_folder (
  afinal, aitems) (rev a') =
(final, items ++ aitems)
(let (final, items) :=
   foldr _apply_plan_folder (afinal, aitems) (rev a') in
 (rev items, final)) =
(rev aitems ++ rev items, final)
  by rewrite Hadd, rev_app_distr.
Qed.

Lemma _apply_plan_cons
  (start : state T)
  (ai : plan_item)
  (a' : list plan_item)
  : _apply_plan start (ai :: a') =
    let (aitems, afinal) := _apply_plan start [ai] in
    let (a'items, a'final) := _apply_plan afinal a' in
     (aitems ++ a'items, a'final).message: Type
T: VLSMType message
transition: label T
→ state T * option message
  → state T * option message
start: state T
ai: plan_item
a': list plan_item
_apply_plan start (ai :: a') =
(let (aitems, afinal) := _apply_plan start [ai] in
 let (a'items, a'final) := _apply_plan afinal a' in
 (aitems ++ a'items, a'final))
Proof.message: Type
T: VLSMType message
transition: label T
→ state T * option message
  → state T * option message
start: state T
ai: plan_item
a': list plan_item
_apply_plan start (ai :: a') =
(let (aitems, afinal) := _apply_plan start [ai] in
 let (a'items, a'final) := _apply_plan afinal a' in
 (aitems ++ a'items, a'final))
  replace (ai :: a') with ([ai] ++ a').message: Type
T: VLSMType message
transition: label T
→ state T * option message
  → state T * option message
start: state T
ai: plan_item
a': list plan_item
_apply_plan start ([ai] ++ a') =
(let (aitems, afinal) := _apply_plan start [ai] in
 let (a'items, a'final) := _apply_plan afinal a' in
 (aitems ++ a'items, a'final))
message: Type
T: VLSMType message
transition: label T
→ state T * option message
  → state T * option message
start: state T
ai: plan_item
a': list plan_item
[ai] ++ a' = ai :: a'
  -message: Type
T: VLSMType message
transition: label T
→ state T * option message
  → state T * option message
start: state T
ai: plan_item
a': list plan_item
_apply_plan start ([ai] ++ a') =
(let (aitems, afinal) := _apply_plan start [ai] in
 let (a'items, a'final) := _apply_plan afinal a' in
 (aitems ++ a'items, a'final)) by apply _apply_plan_app.
  -message: Type
T: VLSMType message
transition: label T
→ state T * option message
  → state T * option message
start: state T
ai: plan_item
a': list plan_item
[ai] ++ a' = ai :: a' by itauto.
Qed.

We can forget information from a trace to obtain a plan.

Definition _transition_item_to_plan_item
  (item : transition_item T)
  : plan_item
  := {| label_a := l item; input_a := input item |}.

Definition _trace_to_plan
  (items : list transition_item)
  : list plan_item
  := map _transition_item_to_plan_item items.

Definition _messages_a
  (a : list (plan_item T)) :
  list message :=
  ListExtras.cat_option (List.map input_a a).

End sec_apply_plans.

Section sec_valid_plans.

Context
  {message : Type}
  (X : VLSM message)
  .

We define several notations useful when we want to use the results above for a specific VLSM, by instantiating the generic definitions with the corresponding type and transition.

Definition plan : Type := list (plan_item X).
Definition apply_plan := (@_apply_plan _ X (@transition _ _ X)).
Definition trace_to_plan := (@_trace_to_plan _ X).
Definition apply_plan_app
  (start : state X)
  (a a' : plan)
  : apply_plan start (a ++ a') =
    let (aitems, afinal) := apply_plan start a in
    let (a'items, a'final) := apply_plan afinal a' in
     (aitems ++ a'items, a'final)
  := (@_apply_plan_app _ X (@transition _ _ X) start a a').
Definition apply_plan_last
  (start : state X)
  (a : plan)
  (after_a := apply_plan start a)
  : finite_trace_last start (fst after_a) = snd after_a
  := (@_apply_plan_last _ X (@transition _ _ X) start a).

A plan is valid w.r.t. a state if by applying it to that state we obtain a valid trace sequence.

Definition finite_valid_plan_from
  (s : state X)
  (a : plan)
  : Prop :=
  finite_valid_trace_from _ s (fst (apply_plan s a)).

Lemma finite_valid_plan_from_app_iff
  (s : state X)
  (a b : plan)
  (s_a := snd (apply_plan s a))
  : finite_valid_plan_from s a /\ finite_valid_plan_from s_a b <-> finite_valid_plan_from s (a ++ b).message: Type
X: VLSM message
s: state X
a, b: plan
s_a:= (apply_plan s a).2: state X
finite_valid_plan_from s a
∧ finite_valid_plan_from s_a b
↔ finite_valid_plan_from s (a ++ b)
Proof.message: Type
X: VLSM message
s: state X
a, b: plan
s_a:= (apply_plan s a).2: state X
finite_valid_plan_from s a
∧ finite_valid_plan_from s_a b
↔ finite_valid_plan_from s (a ++ b)
  unfold finite_valid_plan_from.message: Type
X: VLSM message
s: state X
a, b: plan
s_a:= (apply_plan s a).2: state X
finite_valid_trace_from X s (apply_plan s a).1
∧ finite_valid_trace_from X s_a (apply_plan s_a b).1
↔ finite_valid_trace_from X s
    (apply_plan s (a ++ b)).1
  specialize (apply_plan_app s a b) as Happ.message: Type
X: VLSM message
s: state X
a, b: plan
s_a:= (apply_plan s a).2: state X
Happ: apply_plan s (a ++ b) =
(let (aitems, afinal) := apply_plan s a in
 let (a'items, a'final) :=
   apply_plan afinal b in
 (aitems ++ a'items, a'final))
finite_valid_trace_from X s (apply_plan s a).1
∧ finite_valid_trace_from X s_a (apply_plan s_a b).1
↔ finite_valid_trace_from X s
    (apply_plan s (a ++ b)).1
  specialize (apply_plan_last s a) as Hlst.message: Type
X: VLSM message
s: state X
a, b: plan
s_a:= (apply_plan s a).2: state X
Happ: apply_plan s (a ++ b) =
(let (aitems, afinal) := apply_plan s a in
 let (a'items, a'final) :=
   apply_plan afinal b in
 (aitems ++ a'items, a'final))
Hlst: let after_a := apply_plan s a in
finite_trace_last s after_a.1 = after_a.2
finite_valid_trace_from X s (apply_plan s a).1
∧ finite_valid_trace_from X s_a (apply_plan s_a b).1
↔ finite_valid_trace_from X s
    (apply_plan s (a ++ b)).1
  destruct (apply_plan s a) as (aitems, afinal) eqn: Ha.message: Type
X: VLSM message
s: state X
a, b: plan
aitems: list transition_item
afinal: state X
Ha: apply_plan s a = (aitems, afinal)
s_a:= (aitems, afinal).2: state X
Happ: apply_plan s (a ++ b) =
(let (a'items, a'final) :=
   apply_plan afinal b in
 (aitems ++ a'items, a'final))
Hlst: let after_a := (aitems, afinal) in
finite_trace_last s after_a.1 = after_a.2
finite_valid_trace_from X s (aitems, afinal).1
∧ finite_valid_trace_from X s_a (apply_plan s_a b).1
↔ finite_valid_trace_from X s
    (apply_plan s (a ++ b)).1
  subst s_a.message: Type
X: VLSM message
s: state X
a, b: plan
aitems: list transition_item
afinal: state X
Ha: apply_plan s a = (aitems, afinal)
Happ: apply_plan s (a ++ b) =
(let (a'items, a'final) :=
   apply_plan afinal b in
 (aitems ++ a'items, a'final))
Hlst: let after_a := (aitems, afinal) in
finite_trace_last s after_a.1 = after_a.2
finite_valid_trace_from X s (aitems, afinal).1
∧ finite_valid_trace_from X (aitems, afinal).2
    (apply_plan (aitems, afinal).2 b).1
↔ finite_valid_trace_from X s
    (apply_plan s (a ++ b)).1
  simpl in *.message: Type
X: VLSM message
s: state X
a, b: plan
aitems: list transition_item
afinal: state X
Ha: apply_plan s a = (aitems, afinal)
Happ: apply_plan s (a ++ b) =
(let (a'items, a'final) :=
   apply_plan afinal b in
 (aitems ++ a'items, a'final))
Hlst: finite_trace_last s aitems = afinal
finite_valid_trace_from X s aitems
∧ finite_valid_trace_from X afinal
    (apply_plan afinal b).1
↔ finite_valid_trace_from X s
    (apply_plan s (a ++ b)).1
  destruct (apply_plan afinal b) as (bitems, bfinal).message: Type
X: VLSM message
s: state X
a, b: plan
aitems: list transition_item
afinal: state X
Ha: apply_plan s a = (aitems, afinal)
bitems: list transition_item
bfinal: state X
Happ: apply_plan s (a ++ b) =
(aitems ++ bitems, bfinal)
Hlst: finite_trace_last s aitems = afinal
finite_valid_trace_from X s aitems
∧ finite_valid_trace_from X afinal (bitems, bfinal).1
↔ finite_valid_trace_from X s
    (apply_plan s (a ++ b)).1
  rewrite Happ.message: Type
X: VLSM message
s: state X
a, b: plan
aitems: list transition_item
afinal: state X
Ha: apply_plan s a = (aitems, afinal)
bitems: list transition_item
bfinal: state X
Happ: apply_plan s (a ++ b) =
(aitems ++ bitems, bfinal)
Hlst: finite_trace_last s aitems = afinal
finite_valid_trace_from X s aitems
∧ finite_valid_trace_from X afinal (bitems, bfinal).1
↔ finite_valid_trace_from X s
    (aitems ++ bitems, bfinal).1 simpl.message: Type
X: VLSM message
s: state X
a, b: plan
aitems: list transition_item
afinal: state X
Ha: apply_plan s a = (aitems, afinal)
bitems: list transition_item
bfinal: state X
Happ: apply_plan s (a ++ b) =
(aitems ++ bitems, bfinal)
Hlst: finite_trace_last s aitems = afinal
finite_valid_trace_from X s aitems
∧ finite_valid_trace_from X afinal bitems
↔ finite_valid_trace_from X s (aitems ++ bitems) clear Happ.message: Type
X: VLSM message
s: state X
a, b: plan
aitems: list transition_item
afinal: state X
Ha: apply_plan s a = (aitems, afinal)
bitems: list transition_item
bfinal: state X
Hlst: finite_trace_last s aitems = afinal
finite_valid_trace_from X s aitems
∧ finite_valid_trace_from X afinal bitems
↔ finite_valid_trace_from X s (aitems ++ bitems) subst afinal.message: Type
X: VLSM message
s: state X
a, b: plan
aitems: list transition_item
Ha: apply_plan s a =
(aitems, finite_trace_last s aitems)
bitems: list transition_item
bfinal: state X
finite_valid_trace_from X s aitems
∧ finite_valid_trace_from X
    (finite_trace_last s aitems) bitems
↔ finite_valid_trace_from X s (aitems ++ bitems)
  by apply finite_valid_trace_from_app_iff.
Qed.

Lemma finite_valid_plan_empty
  (s : state X)
  (Hpr : valid_state_prop X s)  :
  finite_valid_plan_from s [].message: Type
X: VLSM message
s: state X
Hpr: valid_state_prop X s
finite_valid_plan_from s []
Proof.message: Type
X: VLSM message
s: state X
Hpr: valid_state_prop X s
finite_valid_plan_from s []
  by apply finite_valid_trace_from_empty.
Qed.

Lemma apply_plan_last_valid
  (s : state X)
  (a : plan)
  (Hpra : finite_valid_plan_from s a)
  (after_a := apply_plan s a) :
  valid_state_prop X (snd after_a).message: Type
X: VLSM message
s: state X
a: plan
Hpra: finite_valid_plan_from s a
after_a:= apply_plan s a: (list transition_item * state X)%type
valid_state_prop X after_a.2
Proof.message: Type
X: VLSM message
s: state X
a: plan
Hpra: finite_valid_plan_from s a
after_a:= apply_plan s a: (list transition_item * state X)%type
valid_state_prop X after_a.2
  subst after_a.message: Type
X: VLSM message
s: state X
a: plan
Hpra: finite_valid_plan_from s a
valid_state_prop X (apply_plan s a).2
  rewrite <- apply_plan_last.message: Type
X: VLSM message
s: state X
a: plan
Hpra: finite_valid_plan_from s a
valid_state_prop X
  (finite_trace_last s (apply_plan s a).1)
  by apply finite_valid_trace_last_pstate.
Qed.

Definition finite_valid_plan_from_to (s : state X) (a : plan) : Prop :=
  finite_valid_trace_from_to _ s (apply_plan s a).2 (apply_plan s a).1.

Lemma finite_valid_plan_from_to_app_iff :
  forall (s : state X) (a b : plan),
    finite_valid_plan_from_to s (a ++ b)
      <->
    finite_valid_plan_from_to s a /\ finite_valid_plan_from_to (apply_plan s a).2 b.message: Type
X: VLSM message
∀ (s : state X) (a b : plan),
  finite_valid_plan_from_to s (a ++ b)
  ↔ finite_valid_plan_from_to s a
    ∧ finite_valid_plan_from_to (apply_plan s a).2 b
Proof.message: Type
X: VLSM message
∀ (s : state X) (a b : plan),
  finite_valid_plan_from_to s (a ++ b)
  ↔ finite_valid_plan_from_to s a
    ∧ finite_valid_plan_from_to (apply_plan s a).2 b
  intros s a b.message: Type
X: VLSM message
s: state X
a, b: plan
finite_valid_plan_from_to s (a ++ b)
↔ finite_valid_plan_from_to s a
  ∧ finite_valid_plan_from_to (apply_plan s a).2 b
  unfold finite_valid_plan_from_to.message: Type
X: VLSM message
s: state X
a, b: plan
finite_valid_trace_from_to X s
  (apply_plan s (a ++ b)).2 (apply_plan s (a ++ b)).1
↔ finite_valid_trace_from_to X s (apply_plan s a).2
    (apply_plan s a).1
  ∧ finite_valid_trace_from_to X (apply_plan s a).2
      (apply_plan (apply_plan s a).2 b).2
      (apply_plan (apply_plan s a).2 b).1
  rewrite apply_plan_app.message: Type
X: VLSM message
s: state X
a, b: plan
finite_valid_trace_from_to X s
  (let (aitems, afinal) := apply_plan s a in
   let (a'items, a'final) := apply_plan afinal b in
   (aitems ++ a'items, a'final)).2
  (let (aitems, afinal) := apply_plan s a in
   let (a'items, a'final) := apply_plan afinal b in
   (aitems ++ a'items, a'final)).1
↔ finite_valid_trace_from_to X s (apply_plan s a).2
    (apply_plan s a).1
  ∧ finite_valid_trace_from_to X (apply_plan s a).2
      (apply_plan (apply_plan s a).2 b).2
      (apply_plan (apply_plan s a).2 b).1
  destruct (apply_plan _ a) as [aitems afinal] eqn: Ha,
    (apply_plan _ b) as [bitems bfinal] eqn: Hb; cbn.message: Type
X: VLSM message
s: state X
a, b: plan
aitems: list transition_item
afinal: state X
Ha: apply_plan s a = (aitems, afinal)
bitems: list transition_item
bfinal: state X
Hb: apply_plan afinal b = (bitems, bfinal)
finite_valid_trace_from_to X s bfinal
  (aitems ++ bitems)
↔ finite_valid_trace_from_to X s afinal aitems
  ∧ finite_valid_trace_from_to X afinal bfinal bitems
  replace aitems with (apply_plan s a).1 by (rewrite Ha; done).message: Type
X: VLSM message
s: state X
a, b: plan
aitems: list transition_item
afinal: state X
Ha: apply_plan s a = (aitems, afinal)
bitems: list transition_item
bfinal: state X
Hb: apply_plan afinal b = (bitems, bfinal)
finite_valid_trace_from_to X s bfinal
  ((apply_plan s a).1 ++ bitems)
↔ finite_valid_trace_from_to X s afinal
    (apply_plan s a).1
  ∧ finite_valid_trace_from_to X afinal bfinal bitems
  replace afinal with (apply_plan s a).2 by (rewrite Ha; done).message: Type
X: VLSM message
s: state X
a, b: plan
aitems: list transition_item
afinal: state X
Ha: apply_plan s a = (aitems, afinal)
bitems: list transition_item
bfinal: state X
Hb: apply_plan afinal b = (bitems, bfinal)
finite_valid_trace_from_to X s bfinal
  ((apply_plan s a).1 ++ bitems)
↔ finite_valid_trace_from_to X s (apply_plan s a).2
    (apply_plan s a).1
  ∧ finite_valid_trace_from_to X (apply_plan s a).2
      bfinal bitems cbn.message: Type
X: VLSM message
s: state X
a, b: plan
aitems: list transition_item
afinal: state X
Ha: apply_plan s a = (aitems, afinal)
bitems: list transition_item
bfinal: state X
Hb: apply_plan afinal b = (bitems, bfinal)
finite_valid_trace_from_to X s bfinal
  ((apply_plan s a).1 ++ bitems)
↔ finite_valid_trace_from_to X s (apply_plan s a).2
    (apply_plan s a).1
  ∧ finite_valid_trace_from_to X (apply_plan s a).2
      bfinal bitems
  rewrite <- apply_plan_last.message: Type
X: VLSM message
s: state X
a, b: plan
aitems: list transition_item
afinal: state X
Ha: apply_plan s a = (aitems, afinal)
bitems: list transition_item
bfinal: state X
Hb: apply_plan afinal b = (bitems, bfinal)
finite_valid_trace_from_to X s bfinal
  ((apply_plan s a).1 ++ bitems)
↔ finite_valid_trace_from_to X s
    (finite_trace_last s (apply_plan s a).1)
    (apply_plan s a).1
  ∧ finite_valid_trace_from_to X
      (finite_trace_last s (apply_plan s a).1) bfinal
      bitems
  split.message: Type
X: VLSM message
s: state X
a, b: plan
aitems: list transition_item
afinal: state X
Ha: apply_plan s a = (aitems, afinal)
bitems: list transition_item
bfinal: state X
Hb: apply_plan afinal b = (bitems, bfinal)
finite_valid_trace_from_to X s bfinal
  ((apply_plan s a).1 ++ bitems)
→ finite_valid_trace_from_to X s
    (finite_trace_last s (apply_plan s a).1)
    (apply_plan s a).1
  ∧ finite_valid_trace_from_to X
      (finite_trace_last s (apply_plan s a).1) bfinal
      bitems
message: Type
X: VLSM message
s: state X
a, b: plan
aitems: list transition_item
afinal: state X
Ha: apply_plan s a = (aitems, afinal)
bitems: list transition_item
bfinal: state X
Hb: apply_plan afinal b = (bitems, bfinal)
finite_valid_trace_from_to X s
  (finite_trace_last s (apply_plan s a).1)
  (apply_plan s a).1
∧ finite_valid_trace_from_to X
    (finite_trace_last s (apply_plan s a).1) bfinal
    bitems
→ finite_valid_trace_from_to X s bfinal
    ((apply_plan s a).1 ++ bitems)
  -message: Type
X: VLSM message
s: state X
a, b: plan
aitems: list transition_item
afinal: state X
Ha: apply_plan s a = (aitems, afinal)
bitems: list transition_item
bfinal: state X
Hb: apply_plan afinal b = (bitems, bfinal)
finite_valid_trace_from_to X s bfinal
  ((apply_plan s a).1 ++ bitems)
→ finite_valid_trace_from_to X s
    (finite_trace_last s (apply_plan s a).1)
    (apply_plan s a).1
  ∧ finite_valid_trace_from_to X
      (finite_trace_last s (apply_plan s a).1) bfinal
      bitems by apply finite_valid_trace_from_to_app_split.
  -message: Type
X: VLSM message
s: state X
a, b: plan
aitems: list transition_item
afinal: state X
Ha: apply_plan s a = (aitems, afinal)
bitems: list transition_item
bfinal: state X
Hb: apply_plan afinal b = (bitems, bfinal)
finite_valid_trace_from_to X s
  (finite_trace_last s (apply_plan s a).1)
  (apply_plan s a).1
∧ finite_valid_trace_from_to X
    (finite_trace_last s (apply_plan s a).1) bfinal
    bitems
→ finite_valid_trace_from_to X s bfinal
    ((apply_plan s a).1 ++ bitems) by intros []; eapply finite_valid_trace_from_to_app.
Qed.

By extracting a plan from a valid_trace based on a state s and reapplying the plan to the same state s we obtain the original trace.

Lemma trace_to_plan_to_trace_from_to
  (s s' : state X)
  (tr : list (transition_item X))
  (Htr : finite_valid_trace_from_to X s s' tr)
  : apply_plan s (trace_to_plan tr) = (tr, s').message: Type
X: VLSM message
s, s': state X
tr: list transition_item
Htr: finite_valid_trace_from_to X s s' tr
apply_plan s (trace_to_plan tr) = (tr, s')
Proof.message: Type
X: VLSM message
s, s': state X
tr: list transition_item
Htr: finite_valid_trace_from_to X s s' tr
apply_plan s (trace_to_plan tr) = (tr, s')
  induction Htr using finite_valid_trace_from_to_rev_ind; [done |].message: Type
X: VLSM message
si, s: state X
tr: list transition_item
Htr: finite_valid_trace_from_to X si s tr
sf: state X
iom, oom: option message
l: label X
Ht: input_valid_transition X l (s, iom) (sf, oom)
IHHtr: apply_plan si (trace_to_plan tr) = (tr, s)
apply_plan si
  (trace_to_plan
     (tr ++
      [{|
         l := l;
         input := iom;
         destination := sf;
         output := oom
       |}])) =
(tr ++
 [{|
    l := l;
    input := iom;
    destination := sf;
    output := oom
  |}], sf)
  unfold trace_to_plan, _trace_to_plan.message: Type
X: VLSM message
si, s: state X
tr: list transition_item
Htr: finite_valid_trace_from_to X si s tr
sf: state X
iom, oom: option message
l: label X
Ht: input_valid_transition X l (s, iom) (sf, oom)
IHHtr: apply_plan si (trace_to_plan tr) = (tr, s)
apply_plan si
  (map _transition_item_to_plan_item
     (tr ++
      [{|
         l := l;
         input := iom;
         destination := sf;
         output := oom
       |}])) =
(tr ++
 [{|
    l := l;
    input := iom;
    destination := sf;
    output := oom
  |}], sf)
  rewrite map_last, apply_plan_app.message: Type
X: VLSM message
si, s: state X
tr: list transition_item
Htr: finite_valid_trace_from_to X si s tr
sf: state X
iom, oom: option message
l: label X
Ht: input_valid_transition X l (s, iom) (sf, oom)
IHHtr: apply_plan si (trace_to_plan tr) = (tr, s)
(let (aitems, afinal) :=
   apply_plan si
     (map _transition_item_to_plan_item tr) in
 let (a'items, a'final) :=
   apply_plan afinal
     [_transition_item_to_plan_item
        {|
          l := l;
          input := iom;
          destination := sf;
          output := oom
        |}] in
 (aitems ++ a'items, a'final)) =
(tr ++
 [{|
    l := l;
    input := iom;
    destination := sf;
    output := oom
  |}], sf)
  change (map _ tr) with (trace_to_plan tr).message: Type
X: VLSM message
si, s: state X
tr: list transition_item
Htr: finite_valid_trace_from_to X si s tr
sf: state X
iom, oom: option message
l: label X
Ht: input_valid_transition X l (s, iom) (sf, oom)
IHHtr: apply_plan si (trace_to_plan tr) = (tr, s)
(let (aitems, afinal) :=
   apply_plan si (trace_to_plan tr) in
 let (a'items, a'final) :=
   apply_plan afinal
     [_transition_item_to_plan_item
        {|
          l := l;
          input := iom;
          destination := sf;
          output := oom
        |}] in
 (aitems ++ a'items, a'final)) =
(tr ++
 [{|
    l := l;
    input := iom;
    destination := sf;
    output := oom
  |}], sf)
  rewrite IHHtr.message: Type
X: VLSM message
si, s: state X
tr: list transition_item
Htr: finite_valid_trace_from_to X si s tr
sf: state X
iom, oom: option message
l: label X
Ht: input_valid_transition X l (s, iom) (sf, oom)
IHHtr: apply_plan si (trace_to_plan tr) = (tr, s)
(let (a'items, a'final) :=
   apply_plan s
     [_transition_item_to_plan_item
        {|
          l := l;
          input := iom;
          destination := sf;
          output := oom
        |}] in
 (tr ++ a'items, a'final)) =
(tr ++
 [{|
    l := l;
    input := iom;
    destination := sf;
    output := oom
  |}], sf)
  unfold _transition_item_to_plan_item, apply_plan, _apply_plan.message: Type
X: VLSM message
si, s: state X
tr: list transition_item
Htr: finite_valid_trace_from_to X si s tr
sf: state X
iom, oom: option message
l: label X
Ht: input_valid_transition X l (s, iom) (sf, oom)
IHHtr: apply_plan si (trace_to_plan tr) = (tr, s)
(let (a'items, a'final) :=
   let (final, items) :=
     foldr _apply_plan_folder (s, [])
       (rev
          [{|
             label_a :=
               VLSM.l
                 {|
                   l := l;
                   input := iom;
                   destination := sf;
                   output := oom
                 |};
             input_a :=
               input
                 {|
                   l := l;
                   input := iom;
                   destination := sf;
                   output := oom
                 |}
           |}]) in
   (rev items, final) in
 (tr ++ a'items, a'final)) =
(tr ++
 [{|
    l := l;
    input := iom;
    destination := sf;
    output := oom
  |}], sf)
  simpl.message: Type
X: VLSM message
si, s: state X
tr: list transition_item
Htr: finite_valid_trace_from_to X si s tr
sf: state X
iom, oom: option message
l: label X
Ht: input_valid_transition X l (s, iom) (sf, oom)
IHHtr: apply_plan si (trace_to_plan tr) = (tr, s)
(let (a'items, a'final) :=
   let (final, items) :=
     let (dest, out) := transition l (s, iom) in
     (dest,
      [{|
         l := l;
         input := iom;
         destination := dest;
         output := out
       |}]) in
   (rev items, final) in
 (tr ++ a'items, a'final)) =
(tr ++
 [{|
    l := l;
    input := iom;
    destination := sf;
    output := oom
  |}], sf)
  destruct Ht as [Hvx Hx].message: Type
X: VLSM message
si, s: state X
tr: list transition_item
Htr: finite_valid_trace_from_to X si s tr
sf: state X
iom, oom: option message
l: label X
Hvx: input_valid X l (s, iom)
Hx: transition l (s, iom) = (sf, oom)
IHHtr: apply_plan si (trace_to_plan tr) = (tr, s)
(let (a'items, a'final) :=
   let (final, items) :=
     let (dest, out) := transition l (s, iom) in
     (dest,
      [{|
         l := l;
         input := iom;
         destination := dest;
         output := out
       |}]) in
   (rev items, final) in
 (tr ++ a'items, a'final)) =
(tr ++
 [{|
    l := l;
    input := iom;
    destination := sf;
    output := oom
  |}], sf)
  by rewrite Hx.
Qed.

Lemma trace_to_plan_to_trace
  (s : state X)
  (tr : list (transition_item X))
  (Htr : finite_valid_trace_from X s tr)
  : fst (apply_plan s (trace_to_plan tr)) = tr.message: Type
X: VLSM message
s: state X
tr: list transition_item
Htr: finite_valid_trace_from X s tr
(apply_plan s (trace_to_plan tr)).1 = tr
Proof.message: Type
X: VLSM message
s: state X
tr: list transition_item
Htr: finite_valid_trace_from X s tr
(apply_plan s (trace_to_plan tr)).1 = tr
  apply valid_trace_add_default_last, trace_to_plan_to_trace_from_to in Htr.message: Type
X: VLSM message
s: state X
tr: list transition_item
Htr: apply_plan s (trace_to_plan tr) =
(tr, finite_trace_last s tr)
(apply_plan s (trace_to_plan tr)).1 = tr
  by rewrite Htr.
Qed.

The plan extracted from a valid trace is valid w.r.t. the starting state of the trace.

Lemma finite_valid_trace_from_to_plan
  (s : state X)
  (tr : list (transition_item X))
  (Htr : finite_valid_trace_from X s tr)
  : finite_valid_plan_from s (trace_to_plan tr).message: Type
X: VLSM message
s: state X
tr: list transition_item
Htr: finite_valid_trace_from X s tr
finite_valid_plan_from s (trace_to_plan tr)
Proof.message: Type
X: VLSM message
s: state X
tr: list transition_item
Htr: finite_valid_trace_from X s tr
finite_valid_plan_from s (trace_to_plan tr)
  by unfold finite_valid_plan_from; rewrite trace_to_plan_to_trace.
Qed.

Characterization of valid plans.

Lemma finite_valid_plan_iff
  (s : state X)
  (a : plan)
  : finite_valid_plan_from s a
  <-> valid_state_prop X s
  /\ Forall (fun ai => option_valid_message_prop X (input_a ai)) a
  /\ forall
      (prefa suffa : plan)
      (ai : plan_item)
      (Heqa : a = prefa ++ [ai] ++ suffa)
      (lst := snd (apply_plan s prefa)),
      valid X (label_a ai) (lst, input_a ai).message: Type
X: VLSM message
s: state X
a: plan
finite_valid_plan_from s a
↔ valid_state_prop X s
  ∧ Forall
      (λ ai : plan_item,
         option_valid_message_prop X (input_a ai)) a
    ∧ (∀ (prefa suffa : plan) (ai : plan_item),
         a = prefa ++ [ai] ++ suffa
         → let lst := (apply_plan s prefa).2 in
           valid (label_a ai) (lst, input_a ai))
Proof.message: Type
X: VLSM message
s: state X
a: plan
finite_valid_plan_from s a
↔ valid_state_prop X s
  ∧ Forall
      (λ ai : plan_item,
         option_valid_message_prop X (input_a ai)) a
    ∧ (∀ (prefa suffa : plan) (ai : plan_item),
         a = prefa ++ [ai] ++ suffa
         → let lst := (apply_plan s prefa).2 in
           valid (label_a ai) (lst, input_a ai))
  induction a using rev_ind; repeat split; intros
  ; try
    (apply finite_valid_plan_from_app_iff in H
    ; destruct H as [Ha Hx]; apply IHa in Ha as Ha').message: Type
X: VLSM message
s: state X
H: finite_valid_plan_from s []
valid_state_prop X s
message: Type
X: VLSM message
s: state X
H: finite_valid_plan_from s []
Forall
  (λ ai : plan_item,
     option_valid_message_prop X (input_a ai)) []
message: Type
X: VLSM message
s: state X
H: finite_valid_plan_from s []
prefa, suffa: plan
ai: plan_item
Heqa: [] = prefa ++ [ai] ++ suffa
lst:= (apply_plan s prefa).2: state X
valid (label_a ai) (lst, input_a ai)
message: Type
X: VLSM message
s: state X
H: valid_state_prop X s
∧ Forall
    (λ ai : plan_item,
       option_valid_message_prop X (input_a ai))
    []
  ∧ (∀ (prefa suffa : plan) (ai : plan_item),
       [] = prefa ++ [ai] ++ suffa
       → let lst := (apply_plan s prefa).2 in
         valid (label_a ai) (lst, input_a ai))
finite_valid_plan_from s []
message: Type
X: VLSM message
s: state X
x: plan_item
a: list plan_item
IHa: finite_valid_plan_from s a
↔ valid_state_prop X s
  ∧ Forall
      (λ ai : plan_item,
         option_valid_message_prop X
           (input_a ai)) a
    ∧ (∀ (prefa suffa : plan) (ai : plan_item),
         a = prefa ++ [ai] ++ suffa
         → let lst := (apply_plan s prefa).2 in
           valid (label_a ai) (lst, input_a ai))
Ha: finite_valid_plan_from s a
Hx: finite_valid_plan_from (apply_plan s a).2 [x]
Ha': valid_state_prop X s
∧ Forall
    (λ ai : plan_item,
       option_valid_message_prop X (input_a ai))
    a
  ∧ (∀ (prefa suffa : plan) (ai : plan_item),
       a = prefa ++ [ai] ++ suffa
       → let lst := (apply_plan s prefa).2 in
         valid (label_a ai) (lst, input_a ai))
valid_state_prop X s
message: Type
X: VLSM message
s: state X
x: plan_item
a: list plan_item
IHa: finite_valid_plan_from s a
↔ valid_state_prop X s
  ∧ Forall
      (λ ai : plan_item,
         option_valid_message_prop X
           (input_a ai)) a
    ∧ (∀ (prefa suffa : plan) (ai : plan_item),
         a = prefa ++ [ai] ++ suffa
         → let lst := (apply_plan s prefa).2 in
           valid (label_a ai) (lst, input_a ai))
Ha: finite_valid_plan_from s a
Hx: finite_valid_plan_from (apply_plan s a).2 [x]
Ha': valid_state_prop X s
∧ Forall
    (λ ai : plan_item,
       option_valid_message_prop X (input_a ai))
    a
  ∧ (∀ (prefa suffa : plan) (ai : plan_item),
       a = prefa ++ [ai] ++ suffa
       → let lst := (apply_plan s prefa).2 in
         valid (label_a ai) (lst, input_a ai))
Forall
  (λ ai : plan_item,
     option_valid_message_prop X (input_a ai))
  (a ++ [x])
message: Type
X: VLSM message
s: state X
x: plan_item
a: list plan_item
IHa: finite_valid_plan_from s a
↔ valid_state_prop X s
  ∧ Forall
      (λ ai : plan_item,
         option_valid_message_prop X
           (input_a ai)) a
    ∧ (∀ (prefa suffa : plan) (ai : plan_item),
         a = prefa ++ [ai] ++ suffa
         → let lst := (apply_plan s prefa).2 in
           valid (label_a ai) (lst, input_a ai))
Ha: finite_valid_plan_from s a
Hx: finite_valid_plan_from (apply_plan s a).2 [x]
prefa, suffa: plan
ai: plan_item
Heqa: a ++ [x] = prefa ++ [ai] ++ suffa
lst:= (apply_plan s prefa).2: state X
Ha': valid_state_prop X s
∧ Forall
    (λ ai : plan_item,
       option_valid_message_prop X (input_a ai))
    a
  ∧ (∀ (prefa suffa : plan) (ai : plan_item),
       a = prefa ++ [ai] ++ suffa
       → let lst := (apply_plan s prefa).2 in
         valid (label_a ai) (lst, input_a ai))
valid (label_a ai) (lst, input_a ai)
message: Type
X: VLSM message
s: state X
x: plan_item
a: list plan_item
IHa: finite_valid_plan_from s a
↔ valid_state_prop X s
  ∧ Forall
      (λ ai : plan_item,
         option_valid_message_prop X
           (input_a ai)) a
    ∧ (∀ (prefa suffa : plan) (ai : plan_item),
         a = prefa ++ [ai] ++ suffa
         → let lst := (apply_plan s prefa).2 in
           valid (label_a ai) (lst, input_a ai))
H: valid_state_prop X s
∧ Forall
    (λ ai : plan_item,
       option_valid_message_prop X (input_a ai))
    (a ++ [x])
  ∧ (∀ (prefa suffa : plan) (ai : plan_item),
       a ++ [x] = prefa ++ [ai] ++ suffa
       → let lst := (apply_plan s prefa).2 in
         valid (label_a ai) (lst, input_a ai))
finite_valid_plan_from s (a ++ [x])
  -message: Type
X: VLSM message
s: state X
H: finite_valid_plan_from s []
valid_state_prop X s by inversion H.
  -message: Type
X: VLSM message
s: state X
H: finite_valid_plan_from s []
Forall
  (λ ai : plan_item,
     option_valid_message_prop X (input_a ai)) [] by constructor.
  -message: Type
X: VLSM message
s: state X
H: finite_valid_plan_from s []
prefa, suffa: plan
ai: plan_item
Heqa: [] = prefa ++ [ai] ++ suffa
lst:= (apply_plan s prefa).2: state X
valid (label_a ai) (lst, input_a ai) by destruct prefa; simpl in Heqa.
  -message: Type
X: VLSM message
s: state X
H: valid_state_prop X s
∧ Forall
    (λ ai : plan_item,
       option_valid_message_prop X (input_a ai))
    []
  ∧ (∀ (prefa suffa : plan) (ai : plan_item),
       [] = prefa ++ [ai] ++ suffa
       → let lst := (apply_plan s prefa).2 in
         valid (label_a ai) (lst, input_a ai))
finite_valid_plan_from s [] by destruct H as [Hs _]; constructor.
  -message: Type
X: VLSM message
s: state X
x: plan_item
a: list plan_item
IHa: finite_valid_plan_from s a
↔ valid_state_prop X s
  ∧ Forall
      (λ ai : plan_item,
         option_valid_message_prop X
           (input_a ai)) a
    ∧ (∀ (prefa suffa : plan) (ai : plan_item),
         a = prefa ++ [ai] ++ suffa
         → let lst := (apply_plan s prefa).2 in
           valid (label_a ai) (lst, input_a ai))
Ha: finite_valid_plan_from s a
Hx: finite_valid_plan_from (apply_plan s a).2 [x]
Ha': valid_state_prop X s
∧ Forall
    (λ ai : plan_item,
       option_valid_message_prop X (input_a ai))
    a
  ∧ (∀ (prefa suffa : plan) (ai : plan_item),
       a = prefa ++ [ai] ++ suffa
       → let lst := (apply_plan s prefa).2 in
         valid (label_a ai) (lst, input_a ai))
valid_state_prop X s by destruct Ha' as [Hs _].
  -message: Type
X: VLSM message
s: state X
x: plan_item
a: list plan_item
IHa: finite_valid_plan_from s a
↔ valid_state_prop X s
  ∧ Forall
      (λ ai : plan_item,
         option_valid_message_prop X
           (input_a ai)) a
    ∧ (∀ (prefa suffa : plan) (ai : plan_item),
         a = prefa ++ [ai] ++ suffa
         → let lst := (apply_plan s prefa).2 in
           valid (label_a ai) (lst, input_a ai))
Ha: finite_valid_plan_from s a
Hx: finite_valid_plan_from (apply_plan s a).2 [x]
Ha': valid_state_prop X s
∧ Forall
    (λ ai : plan_item,
       option_valid_message_prop X (input_a ai))
    a
  ∧ (∀ (prefa suffa : plan) (ai : plan_item),
       a = prefa ++ [ai] ++ suffa
       → let lst := (apply_plan s prefa).2 in
         valid (label_a ai) (lst, input_a ai))
Forall
  (λ ai : plan_item,
     option_valid_message_prop X (input_a ai))
  (a ++ [x]) destruct Ha' as [_ [Hmsgs _]].message: Type
X: VLSM message
s: state X
x: plan_item
a: list plan_item
IHa: finite_valid_plan_from s a
↔ valid_state_prop X s
  ∧ Forall
      (λ ai : plan_item,
         option_valid_message_prop X
           (input_a ai)) a
    ∧ (∀ (prefa suffa : plan) (ai : plan_item),
         a = prefa ++ [ai] ++ suffa
         → let lst := (apply_plan s prefa).2 in
           valid (label_a ai) (lst, input_a ai))
Ha: finite_valid_plan_from s a
Hx: finite_valid_plan_from (apply_plan s a).2 [x]
Hmsgs: Forall
  (λ ai : plan_item,
     option_valid_message_prop X (input_a ai))
  a
Forall
  (λ ai : plan_item,
     option_valid_message_prop X (input_a ai))
  (a ++ [x])
    apply Forall_app.message: Type
X: VLSM message
s: state X
x: plan_item
a: list plan_item
IHa: finite_valid_plan_from s a
↔ valid_state_prop X s
  ∧ Forall
      (λ ai : plan_item,
         option_valid_message_prop X
           (input_a ai)) a
    ∧ (∀ (prefa suffa : plan) (ai : plan_item),
         a = prefa ++ [ai] ++ suffa
         → let lst := (apply_plan s prefa).2 in
           valid (label_a ai) (lst, input_a ai))
Ha: finite_valid_plan_from s a
Hx: finite_valid_plan_from (apply_plan s a).2 [x]
Hmsgs: Forall
  (λ ai : plan_item,
     option_valid_message_prop X (input_a ai))
  a
Forall
  (λ ai : plan_item,
     option_valid_message_prop X (input_a ai)) a
∧ Forall
    (λ ai : plan_item,
       option_valid_message_prop X (input_a ai)) [x] split; [done |].message: Type
X: VLSM message
s: state X
x: plan_item
a: list plan_item
IHa: finite_valid_plan_from s a
↔ valid_state_prop X s
  ∧ Forall
      (λ ai : plan_item,
         option_valid_message_prop X
           (input_a ai)) a
    ∧ (∀ (prefa suffa : plan) (ai : plan_item),
         a = prefa ++ [ai] ++ suffa
         → let lst := (apply_plan s prefa).2 in
           valid (label_a ai) (lst, input_a ai))
Ha: finite_valid_plan_from s a
Hx: finite_valid_plan_from (apply_plan s a).2 [x]
Hmsgs: Forall
  (λ ai : plan_item,
     option_valid_message_prop X (input_a ai))
  a
Forall
  (λ ai : plan_item,
     option_valid_message_prop X (input_a ai)) [x]
    repeat constructor.message: Type
X: VLSM message
s: state X
x: plan_item
a: list plan_item
IHa: finite_valid_plan_from s a
↔ valid_state_prop X s
  ∧ Forall
      (λ ai : plan_item,
         option_valid_message_prop X
           (input_a ai)) a
    ∧ (∀ (prefa suffa : plan) (ai : plan_item),
         a = prefa ++ [ai] ++ suffa
         → let lst := (apply_plan s prefa).2 in
           valid (label_a ai) (lst, input_a ai))
Ha: finite_valid_plan_from s a
Hx: finite_valid_plan_from (apply_plan s a).2 [x]
Hmsgs: Forall
  (λ ai : plan_item,
     option_valid_message_prop X (input_a ai))
  a
option_valid_message_prop X (input_a x) unfold finite_valid_plan_from in Hx.message: Type
X: VLSM message
s: state X
x: plan_item
a: list plan_item
IHa: finite_valid_plan_from s a
↔ valid_state_prop X s
  ∧ Forall
      (λ ai : plan_item,
         option_valid_message_prop X
           (input_a ai)) a
    ∧ (∀ (prefa suffa : plan) (ai : plan_item),
         a = prefa ++ [ai] ++ suffa
         → let lst := (apply_plan s prefa).2 in
           valid (label_a ai) (lst, input_a ai))
Ha: finite_valid_plan_from s a
Hx: finite_valid_trace_from X 
  (apply_plan s a).2
  (apply_plan (apply_plan s a).2 [x]).1
Hmsgs: Forall
  (λ ai : plan_item,
     option_valid_message_prop X (input_a ai))
  a
option_valid_message_prop X (input_a x)
    remember (snd (apply_plan s a)) as lst.message: Type
X: VLSM message
s: state X
x: plan_item
a: list plan_item
IHa: finite_valid_plan_from s a
↔ valid_state_prop X s
  ∧ Forall
      (λ ai : plan_item,
         option_valid_message_prop X
           (input_a ai)) a
    ∧ (∀ (prefa suffa : plan) (ai : plan_item),
         a = prefa ++ [ai] ++ suffa
         → let lst := (apply_plan s prefa).2 in
           valid (label_a ai) (lst, input_a ai))
Ha: finite_valid_plan_from s a
lst: state X
Heqlst: lst = (apply_plan s a).2
Hx: finite_valid_trace_from X lst
  (apply_plan lst [x]).1
Hmsgs: Forall
  (λ ai : plan_item,
     option_valid_message_prop X (input_a ai))
  a
option_valid_message_prop X (input_a x)
    unfold apply_plan, _apply_plan in Hx.message: Type
X: VLSM message
s: state X
x: plan_item
a: list plan_item
IHa: finite_valid_plan_from s a
↔ valid_state_prop X s
  ∧ Forall
      (λ ai : plan_item,
         option_valid_message_prop X
           (input_a ai)) a
    ∧ (∀ (prefa suffa : plan) (ai : plan_item),
         a = prefa ++ [ai] ++ suffa
         → let lst := (apply_plan s prefa).2 in
           valid (label_a ai) (lst, input_a ai))
Ha: finite_valid_plan_from s a
lst: state X
Heqlst: lst = (apply_plan s a).2
Hx: finite_valid_trace_from X lst
  (let (final, items) :=
     foldr _apply_plan_folder (lst, []) (rev [x]) in
   (rev items, final)).1
Hmsgs: Forall
  (λ ai : plan_item,
     option_valid_message_prop X (input_a ai))
  a
option_valid_message_prop X (input_a x) simpl in Hx.message: Type
X: VLSM message
s: state X
x: plan_item
a: list plan_item
IHa: finite_valid_plan_from s a
↔ valid_state_prop X s
  ∧ Forall
      (λ ai : plan_item,
         option_valid_message_prop X
           (input_a ai)) a
    ∧ (∀ (prefa suffa : plan) (ai : plan_item),
         a = prefa ++ [ai] ++ suffa
         → let lst := (apply_plan s prefa).2 in
           valid (label_a ai) (lst, input_a ai))
Ha: finite_valid_plan_from s a
lst: state X
Heqlst: lst = (apply_plan s a).2
Hx: finite_valid_trace_from X lst
  (let (final, items) :=
     match x with
     | {| label_a := l'; input_a := input' |} =>
         let (dest, out) :=
           transition l' (lst, input') in
         (dest,
          [{|
             l := l';
             input := input';
             destination := dest;
             output := out
           |}])
     end in
   (rev items, final)).1
Hmsgs: Forall
  (λ ai : plan_item,
     option_valid_message_prop X (input_a ai))
  a
option_valid_message_prop X (input_a x)
    destruct x.message: Type
X: VLSM message
s: state X
label_a0: label X
input_a0: option message
a: list plan_item
IHa: finite_valid_plan_from s a
↔ valid_state_prop X s
  ∧ Forall
      (λ ai : plan_item,
         option_valid_message_prop X
           (input_a ai)) a
    ∧ (∀ (prefa suffa : plan) (ai : plan_item),
         a = prefa ++ [ai] ++ suffa
         → let lst := (apply_plan s prefa).2 in
           valid (label_a ai) (lst, input_a ai))
Ha: finite_valid_plan_from s a
lst: state X
Heqlst: lst = (apply_plan s a).2
Hx: finite_valid_trace_from X lst
  (let (final, items) :=
     let (dest, out) :=
       transition label_a0 (lst, input_a0) in
     (dest,
      [{|
         l := label_a0;
         input := input_a0;
         destination := dest;
         output := out
       |}]) in
   (rev items, final)).1
Hmsgs: Forall
  (λ ai : plan_item,
     option_valid_message_prop X (input_a ai))
  a
option_valid_message_prop X
  (input_a
     {| label_a := label_a0; input_a := input_a0 |})
    destruct (transition X label_a0 (lst, input_a0)) as (dest, out).message: Type
X: VLSM message
s: state X
label_a0: label X
input_a0: option message
a: list plan_item
IHa: finite_valid_plan_from s a
↔ valid_state_prop X s
  ∧ Forall
      (λ ai : plan_item,
         option_valid_message_prop X
           (input_a ai)) a
    ∧ (∀ (prefa suffa : plan) (ai : plan_item),
         a = prefa ++ [ai] ++ suffa
         → let lst := (apply_plan s prefa).2 in
           valid (label_a ai) (lst, input_a ai))
Ha: finite_valid_plan_from s a
lst: state X
Heqlst: lst = (apply_plan s a).2
dest: state X
out: option message
Hx: finite_valid_trace_from X lst
  (rev
     [{|
        l := label_a0;
        input := input_a0;
        destination := dest;
        output := out
      |}], dest).1
Hmsgs: Forall
  (λ ai : plan_item,
     option_valid_message_prop X (input_a ai))
  a
option_valid_message_prop X
  (input_a
     {| label_a := label_a0; input_a := input_a0 |})
    simpl.message: Type
X: VLSM message
s: state X
label_a0: label X
input_a0: option message
a: list plan_item
IHa: finite_valid_plan_from s a
↔ valid_state_prop X s
  ∧ Forall
      (λ ai : plan_item,
         option_valid_message_prop X
           (input_a ai)) a
    ∧ (∀ (prefa suffa : plan) (ai : plan_item),
         a = prefa ++ [ai] ++ suffa
         → let lst := (apply_plan s prefa).2 in
           valid (label_a ai) (lst, input_a ai))
Ha: finite_valid_plan_from s a
lst: state X
Heqlst: lst = (apply_plan s a).2
dest: state X
out: option message
Hx: finite_valid_trace_from X lst
  (rev
     [{|
        l := label_a0;
        input := input_a0;
        destination := dest;
        output := out
      |}], dest).1
Hmsgs: Forall
  (λ ai : plan_item,
     option_valid_message_prop X (input_a ai))
  a
option_valid_message_prop X input_a0 simpl in Hx.message: Type
X: VLSM message
s: state X
label_a0: label X
input_a0: option message
a: list plan_item
IHa: finite_valid_plan_from s a
↔ valid_state_prop X s
  ∧ Forall
      (λ ai : plan_item,
         option_valid_message_prop X
           (input_a ai)) a
    ∧ (∀ (prefa suffa : plan) (ai : plan_item),
         a = prefa ++ [ai] ++ suffa
         → let lst := (apply_plan s prefa).2 in
           valid (label_a ai) (lst, input_a ai))
Ha: finite_valid_plan_from s a
lst: state X
Heqlst: lst = (apply_plan s a).2
dest: state X
out: option message
Hx: finite_valid_trace_from X lst
  [{|
     l := label_a0;
     input := input_a0;
     destination := dest;
     output := out
   |}]
Hmsgs: Forall
  (λ ai : plan_item,
     option_valid_message_prop X (input_a ai))
  a
option_valid_message_prop X input_a0 inversion Hx.message: Type
X: VLSM message
s: state X
label_a0: label X
input_a0: option message
a: list plan_item
IHa: finite_valid_plan_from s a
↔ valid_state_prop X s
  ∧ Forall
      (λ ai : plan_item,
         option_valid_message_prop X
           (input_a ai)) a
    ∧ (∀ (prefa suffa : plan) (ai : plan_item),
         a = prefa ++ [ai] ++ suffa
         → let lst := (apply_plan s prefa).2 in
           valid (label_a ai) (lst, input_a ai))
Ha: finite_valid_plan_from s a
lst: state X
Heqlst: lst = (apply_plan s a).2
dest: state X
out: option message
Hx: finite_valid_trace_from X lst
  [{|
     l := label_a0;
     input := input_a0;
     destination := dest;
     output := out
   |}]
Hmsgs: Forall
  (λ ai : plan_item,
     option_valid_message_prop X (input_a ai))
  a
s0: state X
tl: list transition_item
s': state X
iom, oom: option message
l: label X
Htl: finite_valid_trace_from X dest []
Ht: input_valid_transition X label_a0 (
  lst, input_a0) (dest, out)
H: s' = lst
H1: l = label_a0
H2: iom = input_a0
H3: s0 = dest
H4: oom = out
H5: tl = []
option_valid_message_prop X input_a0 subst.message: Type
X: VLSM message
s: state X
label_a0: label X
input_a0: option message
a: list plan_item
IHa: finite_valid_plan_from s a
↔ valid_state_prop X s
  ∧ Forall
      (λ ai : plan_item,
         option_valid_message_prop X
           (input_a ai)) a
    ∧ (∀ (prefa suffa : plan) (ai : plan_item),
         a = prefa ++ [ai] ++ suffa
         → let lst := (apply_plan s prefa).2 in
           valid (label_a ai) (lst, input_a ai))
Ha: finite_valid_plan_from s a
dest: state X
out: option message
Hx: finite_valid_trace_from X 
  (apply_plan s a).2
  [{|
     l := label_a0;
     input := input_a0;
     destination := dest;
     output := out
   |}]
Hmsgs: Forall
  (λ ai : plan_item,
     option_valid_message_prop X (input_a ai))
  a
Htl: finite_valid_trace_from X dest []
Ht: input_valid_transition X label_a0
  ((apply_plan s a).2, input_a0) (
  dest, out)
option_valid_message_prop X input_a0
    by apply Ht.
  -message: Type
X: VLSM message
s: state X
x: plan_item
a: list plan_item
IHa: finite_valid_plan_from s a
↔ valid_state_prop X s
  ∧ Forall
      (λ ai : plan_item,
         option_valid_message_prop X
           (input_a ai)) a
    ∧ (∀ (prefa suffa : plan) (ai : plan_item),
         a = prefa ++ [ai] ++ suffa
         → let lst := (apply_plan s prefa).2 in
           valid (label_a ai) (lst, input_a ai))
Ha: finite_valid_plan_from s a
Hx: finite_valid_plan_from (apply_plan s a).2 [x]
prefa, suffa: plan
ai: plan_item
Heqa: a ++ [x] = prefa ++ [ai] ++ suffa
lst:= (apply_plan s prefa).2: state X
Ha': valid_state_prop X s
∧ Forall
    (λ ai : plan_item,
       option_valid_message_prop X (input_a ai))
    a
  ∧ (∀ (prefa suffa : plan) (ai : plan_item),
       a = prefa ++ [ai] ++ suffa
       → let lst := (apply_plan s prefa).2 in
         valid (label_a ai) (lst, input_a ai))
valid (label_a ai) (lst, input_a ai) assert (Hsuffa : suffa = [] \/ suffa <> []) by
      (destruct suffa; try (left; congruence); right; congruence).message: Type
X: VLSM message
s: state X
x: plan_item
a: list plan_item
IHa: finite_valid_plan_from s a
↔ valid_state_prop X s
  ∧ Forall
      (λ ai : plan_item,
         option_valid_message_prop X
           (input_a ai)) a
    ∧ (∀ (prefa suffa : plan) (ai : plan_item),
         a = prefa ++ [ai] ++ suffa
         → let lst := (apply_plan s prefa).2 in
           valid (label_a ai) (lst, input_a ai))
Ha: finite_valid_plan_from s a
Hx: finite_valid_plan_from (apply_plan s a).2 [x]
prefa, suffa: plan
ai: plan_item
Heqa: a ++ [x] = prefa ++ [ai] ++ suffa
lst:= (apply_plan s prefa).2: state X
Ha': valid_state_prop X s
∧ Forall
    (λ ai : plan_item,
       option_valid_message_prop X (input_a ai))
    a
  ∧ (∀ (prefa suffa : plan) (ai : plan_item),
       a = prefa ++ [ai] ++ suffa
       → let lst := (apply_plan s prefa).2 in
         valid (label_a ai) (lst, input_a ai))
Hsuffa: suffa = [] ∨ suffa ≠ []
valid (label_a ai) (lst, input_a ai)
    destruct Hsuffa.message: Type
X: VLSM message
s: state X
x: plan_item
a: list plan_item
IHa: finite_valid_plan_from s a
↔ valid_state_prop X s
  ∧ Forall
      (λ ai : plan_item,
         option_valid_message_prop X
           (input_a ai)) a
    ∧ (∀ (prefa suffa : plan) (ai : plan_item),
         a = prefa ++ [ai] ++ suffa
         → let lst := (apply_plan s prefa).2 in
           valid (label_a ai) (lst, input_a ai))
Ha: finite_valid_plan_from s a
Hx: finite_valid_plan_from (apply_plan s a).2 [x]
prefa, suffa: plan
ai: plan_item
Heqa: a ++ [x] = prefa ++ [ai] ++ suffa
lst:= (apply_plan s prefa).2: state X
Ha': valid_state_prop X s
∧ Forall
    (λ ai : plan_item,
       option_valid_message_prop X (input_a ai))
    a
  ∧ (∀ (prefa suffa : plan) (ai : plan_item),
       a = prefa ++ [ai] ++ suffa
       → let lst := (apply_plan s prefa).2 in
         valid (label_a ai) (lst, input_a ai))
H: suffa = []
valid (label_a ai) (lst, input_a ai)
message: Type
X: VLSM message
s: state X
x: plan_item
a: list plan_item
IHa: finite_valid_plan_from s a
↔ valid_state_prop X s
  ∧ Forall
      (λ ai : plan_item,
         option_valid_message_prop X
           (input_a ai)) a
    ∧ (∀ (prefa suffa : plan) (ai : plan_item),
         a = prefa ++ [ai] ++ suffa
         → let lst := (apply_plan s prefa).2 in
           valid (label_a ai) (lst, input_a ai))
Ha: finite_valid_plan_from s a
Hx: finite_valid_plan_from (apply_plan s a).2 [x]
prefa, suffa: plan
ai: plan_item
Heqa: a ++ [x] = prefa ++ [ai] ++ suffa
lst:= (apply_plan s prefa).2: state X
Ha': valid_state_prop X s
∧ Forall
    (λ ai : plan_item,
       option_valid_message_prop X (input_a ai))
    a
  ∧ (∀ (prefa suffa : plan) (ai : plan_item),
       a = prefa ++ [ai] ++ suffa
       → let lst := (apply_plan s prefa).2 in
         valid (label_a ai) (lst, input_a ai))
H: suffa ≠ []
valid (label_a ai) (lst, input_a ai)
    +message: Type
X: VLSM message
s: state X
x: plan_item
a: list plan_item
IHa: finite_valid_plan_from s a
↔ valid_state_prop X s
  ∧ Forall
      (λ ai : plan_item,
         option_valid_message_prop X
           (input_a ai)) a
    ∧ (∀ (prefa suffa : plan) (ai : plan_item),
         a = prefa ++ [ai] ++ suffa
         → let lst := (apply_plan s prefa).2 in
           valid (label_a ai) (lst, input_a ai))
Ha: finite_valid_plan_from s a
Hx: finite_valid_plan_from (apply_plan s a).2 [x]
prefa, suffa: plan
ai: plan_item
Heqa: a ++ [x] = prefa ++ [ai] ++ suffa
lst:= (apply_plan s prefa).2: state X
Ha': valid_state_prop X s
∧ Forall
    (λ ai : plan_item,
       option_valid_message_prop X (input_a ai))
    a
  ∧ (∀ (prefa suffa : plan) (ai : plan_item),
       a = prefa ++ [ai] ++ suffa
       → let lst := (apply_plan s prefa).2 in
         valid (label_a ai) (lst, input_a ai))
H: suffa = []
valid (label_a ai) (lst, input_a ai) subst.message: Type
X: VLSM message
s: state X
x: plan_item
a: list plan_item
IHa: finite_valid_plan_from s a
↔ valid_state_prop X s
  ∧ Forall
      (λ ai : plan_item,
         option_valid_message_prop X
           (input_a ai)) a
    ∧ (∀ (prefa suffa : plan) (ai : plan_item),
         a = prefa ++ [ai] ++ suffa
         → let lst := (apply_plan s prefa).2 in
           valid (label_a ai) (lst, input_a ai))
Ha: finite_valid_plan_from s a
Hx: finite_valid_plan_from (apply_plan s a).2 [x]
prefa: plan
ai: plan_item
Heqa: a ++ [x] = prefa ++ [ai] ++ []
lst:= (apply_plan s prefa).2: state X
Ha': valid_state_prop X s
∧ Forall
    (λ ai : plan_item,
       option_valid_message_prop X (input_a ai))
    a
  ∧ (∀ (prefa suffa : plan) (ai : plan_item),
       a = prefa ++ [ai] ++ suffa
       → let lst := (apply_plan s prefa).2 in
         valid (label_a ai) (lst, input_a ai))
valid (label_a ai) (lst, input_a ai) rewrite app_assoc in Heqa.message: Type
X: VLSM message
s: state X
x: plan_item
a: list plan_item
IHa: finite_valid_plan_from s a
↔ valid_state_prop X s
  ∧ Forall
      (λ ai : plan_item,
         option_valid_message_prop X
           (input_a ai)) a
    ∧ (∀ (prefa suffa : plan) (ai : plan_item),
         a = prefa ++ [ai] ++ suffa
         → let lst := (apply_plan s prefa).2 in
           valid (label_a ai) (lst, input_a ai))
Ha: finite_valid_plan_from s a
Hx: finite_valid_plan_from (apply_plan s a).2 [x]
prefa: plan
ai: plan_item
Heqa: a ++ [x] = (prefa ++ [ai]) ++ []
lst:= (apply_plan s prefa).2: state X
Ha': valid_state_prop X s
∧ Forall
    (λ ai : plan_item,
       option_valid_message_prop X (input_a ai))
    a
  ∧ (∀ (prefa suffa : plan) (ai : plan_item),
       a = prefa ++ [ai] ++ suffa
       → let lst := (apply_plan s prefa).2 in
         valid (label_a ai) (lst, input_a ai))
valid (label_a ai) (lst, input_a ai) rewrite app_nil_r in Heqa.message: Type
X: VLSM message
s: state X
x: plan_item
a: list plan_item
IHa: finite_valid_plan_from s a
↔ valid_state_prop X s
  ∧ Forall
      (λ ai : plan_item,
         option_valid_message_prop X
           (input_a ai)) a
    ∧ (∀ (prefa suffa : plan) (ai : plan_item),
         a = prefa ++ [ai] ++ suffa
         → let lst := (apply_plan s prefa).2 in
           valid (label_a ai) (lst, input_a ai))
Ha: finite_valid_plan_from s a
Hx: finite_valid_plan_from (apply_plan s a).2 [x]
prefa: plan
ai: plan_item
Heqa: a ++ [x] = prefa ++ [ai]
lst:= (apply_plan s prefa).2: state X
Ha': valid_state_prop X s
∧ Forall
    (λ ai : plan_item,
       option_valid_message_prop X (input_a ai))
    a
  ∧ (∀ (prefa suffa : plan) (ai : plan_item),
       a = prefa ++ [ai] ++ suffa
       → let lst := (apply_plan s prefa).2 in
         valid (label_a ai) (lst, input_a ai))
valid (label_a ai) (lst, input_a ai)
      apply app_inj_tail in Heqa.message: Type
X: VLSM message
s: state X
x: plan_item
a: list plan_item
IHa: finite_valid_plan_from s a
↔ valid_state_prop X s
  ∧ Forall
      (λ ai : plan_item,
         option_valid_message_prop X
           (input_a ai)) a
    ∧ (∀ (prefa suffa : plan) (ai : plan_item),
         a = prefa ++ [ai] ++ suffa
         → let lst := (apply_plan s prefa).2 in
           valid (label_a ai) (lst, input_a ai))
Ha: finite_valid_plan_from s a
Hx: finite_valid_plan_from (apply_plan s a).2 [x]
prefa: plan
ai: plan_item
Heqa: a = prefa ∧ x = ai
lst:= (apply_plan s prefa).2: state X
Ha': valid_state_prop X s
∧ Forall
    (λ ai : plan_item,
       option_valid_message_prop X (input_a ai))
    a
  ∧ (∀ (prefa suffa : plan) (ai : plan_item),
       a = prefa ++ [ai] ++ suffa
       → let lst := (apply_plan s prefa).2 in
         valid (label_a ai) (lst, input_a ai))
valid (label_a ai) (lst, input_a ai) destruct Heqa; subst.message: Type
X: VLSM message
s: state X
prefa: plan
ai: plan_item
Hx: finite_valid_plan_from 
  (apply_plan s prefa).2 [ai]
Ha: finite_valid_plan_from s prefa
IHa: finite_valid_plan_from s prefa
↔ valid_state_prop X s
  ∧ Forall
      (λ ai : plan_item,
         option_valid_message_prop X
           (input_a ai)) prefa
    ∧ (∀ (prefa0 suffa : plan) (ai : plan_item),
         prefa = prefa0 ++ [ai] ++ suffa
         → let lst := (apply_plan s prefa0).2 in
           valid (label_a ai) (lst, input_a ai))
lst:= (apply_plan s prefa).2: state X
Ha': valid_state_prop X s
∧ Forall
    (λ ai : plan_item,
       option_valid_message_prop X (input_a ai))
    prefa
  ∧ (∀ (prefa0 suffa : plan) (ai : plan_item),
       prefa = prefa0 ++ [ai] ++ suffa
       → let lst := (apply_plan s prefa0).2 in
         valid (label_a ai) (lst, input_a ai))
valid (label_a ai) (lst, input_a ai)
      unfold lst.message: Type
X: VLSM message
s: state X
prefa: plan
ai: plan_item
Hx: finite_valid_plan_from 
  (apply_plan s prefa).2 [ai]
Ha: finite_valid_plan_from s prefa
IHa: finite_valid_plan_from s prefa
↔ valid_state_prop X s
  ∧ Forall
      (λ ai : plan_item,
         option_valid_message_prop X
           (input_a ai)) prefa
    ∧ (∀ (prefa0 suffa : plan) (ai : plan_item),
         prefa = prefa0 ++ [ai] ++ suffa
         → let lst := (apply_plan s prefa0).2 in
           valid (label_a ai) (lst, input_a ai))
lst:= (apply_plan s prefa).2: state X
Ha': valid_state_prop X s
∧ Forall
    (λ ai : plan_item,
       option_valid_message_prop X (input_a ai))
    prefa
  ∧ (∀ (prefa0 suffa : plan) (ai : plan_item),
       prefa = prefa0 ++ [ai] ++ suffa
       → let lst := (apply_plan s prefa0).2 in
         valid (label_a ai) (lst, input_a ai))
valid (label_a ai)
  ((apply_plan s prefa).2, input_a ai) clear lst.message: Type
X: VLSM message
s: state X
prefa: plan
ai: plan_item
Hx: finite_valid_plan_from 
  (apply_plan s prefa).2 [ai]
Ha: finite_valid_plan_from s prefa
IHa: finite_valid_plan_from s prefa
↔ valid_state_prop X s
  ∧ Forall
      (λ ai : plan_item,
         option_valid_message_prop X
           (input_a ai)) prefa
    ∧ (∀ (prefa0 suffa : plan) (ai : plan_item),
         prefa = prefa0 ++ [ai] ++ suffa
         → let lst := (apply_plan s prefa0).2 in
           valid (label_a ai) (lst, input_a ai))
Ha': valid_state_prop X s
∧ Forall
    (λ ai : plan_item,
       option_valid_message_prop X (input_a ai))
    prefa
  ∧ (∀ (prefa0 suffa : plan) (ai : plan_item),
       prefa = prefa0 ++ [ai] ++ suffa
       → let lst := (apply_plan s prefa0).2 in
         valid (label_a ai) (lst, input_a ai))
valid (label_a ai)
  ((apply_plan s prefa).2, input_a ai)
      remember (snd (apply_plan s prefa)) as lst.message: Type
X: VLSM message
s: state X
prefa: plan
ai: plan_item
lst: state X
Heqlst: lst = (apply_plan s prefa).2
Hx: finite_valid_plan_from lst [ai]
Ha: finite_valid_plan_from s prefa
IHa: finite_valid_plan_from s prefa
↔ valid_state_prop X s
  ∧ Forall
      (λ ai : plan_item,
         option_valid_message_prop X
           (input_a ai)) prefa
    ∧ (∀ (prefa0 suffa : plan) (ai : plan_item),
         prefa = prefa0 ++ [ai] ++ suffa
         → let lst := (apply_plan s prefa0).2 in
           valid (label_a ai) (lst, input_a ai))
Ha': valid_state_prop X s
∧ Forall
    (λ ai : plan_item,
       option_valid_message_prop X (input_a ai))
    prefa
  ∧ (∀ (prefa0 suffa : plan) (ai : plan_item),
       prefa = prefa0 ++ [ai] ++ suffa
       → let lst := (apply_plan s prefa0).2 in
         valid (label_a ai) (lst, input_a ai))
valid (label_a ai) (lst, input_a ai)
      unfold finite_valid_plan_from in Hx.message: Type
X: VLSM message
s: state X
prefa: plan
ai: plan_item
lst: state X
Heqlst: lst = (apply_plan s prefa).2
Hx: finite_valid_trace_from X lst
  (apply_plan lst [ai]).1
Ha: finite_valid_plan_from s prefa
IHa: finite_valid_plan_from s prefa
↔ valid_state_prop X s
  ∧ Forall
      (λ ai : plan_item,
         option_valid_message_prop X
           (input_a ai)) prefa
    ∧ (∀ (prefa0 suffa : plan) (ai : plan_item),
         prefa = prefa0 ++ [ai] ++ suffa
         → let lst := (apply_plan s prefa0).2 in
           valid (label_a ai) (lst, input_a ai))
Ha': valid_state_prop X s
∧ Forall
    (λ ai : plan_item,
       option_valid_message_prop X (input_a ai))
    prefa
  ∧ (∀ (prefa0 suffa : plan) (ai : plan_item),
       prefa = prefa0 ++ [ai] ++ suffa
       → let lst := (apply_plan s prefa0).2 in
         valid (label_a ai) (lst, input_a ai))
valid (label_a ai) (lst, input_a ai)
      unfold apply_plan, _apply_plan in Hx.message: Type
X: VLSM message
s: state X
prefa: plan
ai: plan_item
lst: state X
Heqlst: lst = (apply_plan s prefa).2
Hx: finite_valid_trace_from X lst
  (let (final, items) :=
     foldr _apply_plan_folder (
       lst, []) (rev [ai]) in
   (rev items, final)).1
Ha: finite_valid_plan_from s prefa
IHa: finite_valid_plan_from s prefa
↔ valid_state_prop X s
  ∧ Forall
      (λ ai : plan_item,
         option_valid_message_prop X
           (input_a ai)) prefa
    ∧ (∀ (prefa0 suffa : plan) (ai : plan_item),
         prefa = prefa0 ++ [ai] ++ suffa
         → let lst := (apply_plan s prefa0).2 in
           valid (label_a ai) (lst, input_a ai))
Ha': valid_state_prop X s
∧ Forall
    (λ ai : plan_item,
       option_valid_message_prop X (input_a ai))
    prefa
  ∧ (∀ (prefa0 suffa : plan) (ai : plan_item),
       prefa = prefa0 ++ [ai] ++ suffa
       → let lst := (apply_plan s prefa0).2 in
         valid (label_a ai) (lst, input_a ai))
valid (label_a ai) (lst, input_a ai) simpl in Hx.message: Type
X: VLSM message
s: state X
prefa: plan
ai: plan_item
lst: state X
Heqlst: lst = (apply_plan s prefa).2
Hx: finite_valid_trace_from X lst
  (let (final, items) :=
     match ai with
     | {| label_a := l'; input_a := input' |} =>
         let (dest, out) :=
           transition l' (lst, input') in
         (dest,
          [{|
             l := l';
             input := input';
             destination := dest;
             output := out
           |}])
     end in
   (rev items, final)).1
Ha: finite_valid_plan_from s prefa
IHa: finite_valid_plan_from s prefa
↔ valid_state_prop X s
  ∧ Forall
      (λ ai : plan_item,
         option_valid_message_prop X
           (input_a ai)) prefa
    ∧ (∀ (prefa0 suffa : plan) (ai : plan_item),
         prefa = prefa0 ++ [ai] ++ suffa
         → let lst := (apply_plan s prefa0).2 in
           valid (label_a ai) (lst, input_a ai))
Ha': valid_state_prop X s
∧ Forall
    (λ ai : plan_item,
       option_valid_message_prop X (input_a ai))
    prefa
  ∧ (∀ (prefa0 suffa : plan) (ai : plan_item),
       prefa = prefa0 ++ [ai] ++ suffa
       → let lst := (apply_plan s prefa0).2 in
         valid (label_a ai) (lst, input_a ai))
valid (label_a ai) (lst, input_a ai)
      destruct ai.message: Type
X: VLSM message
s: state X
prefa: plan
label_a0: label X
input_a0: option message
lst: state X
Heqlst: lst = (apply_plan s prefa).2
Hx: finite_valid_trace_from X lst
  (let (final, items) :=
     let (dest, out) :=
       transition label_a0 (lst, input_a0) in
     (dest,
      [{|
         l := label_a0;
         input := input_a0;
         destination := dest;
         output := out
       |}]) in
   (rev items, final)).1
Ha: finite_valid_plan_from s prefa
IHa: finite_valid_plan_from s prefa
↔ valid_state_prop X s
  ∧ Forall
      (λ ai : plan_item,
         option_valid_message_prop X
           (input_a ai)) prefa
    ∧ (∀ (prefa0 suffa : plan) (ai : plan_item),
         prefa = prefa0 ++ [ai] ++ suffa
         → let lst := (apply_plan s prefa0).2 in
           valid (label_a ai) (lst, input_a ai))
Ha': valid_state_prop X s
∧ Forall
    (λ ai : plan_item,
       option_valid_message_prop X (input_a ai))
    prefa
  ∧ (∀ (prefa0 suffa : plan) (ai : plan_item),
       prefa = prefa0 ++ [ai] ++ suffa
       → let lst := (apply_plan s prefa0).2 in
         valid (label_a ai) (lst, input_a ai))
valid
  (label_a
     {| label_a := label_a0; input_a := input_a0 |})
  (lst,
   input_a
     {| label_a := label_a0; input_a := input_a0 |})
      destruct (transition X label_a0 (lst, input_a0)) as (dest, out).message: Type
X: VLSM message
s: state X
prefa: plan
label_a0: label X
input_a0: option message
lst: state X
Heqlst: lst = (apply_plan s prefa).2
dest: state X
out: option message
Hx: finite_valid_trace_from X lst
  (rev
     [{|
        l := label_a0;
        input := input_a0;
        destination := dest;
        output := out
      |}], dest).1
Ha: finite_valid_plan_from s prefa
IHa: finite_valid_plan_from s prefa
↔ valid_state_prop X s
  ∧ Forall
      (λ ai : plan_item,
         option_valid_message_prop X
           (input_a ai)) prefa
    ∧ (∀ (prefa0 suffa : plan) (ai : plan_item),
         prefa = prefa0 ++ [ai] ++ suffa
         → let lst := (apply_plan s prefa0).2 in
           valid (label_a ai) (lst, input_a ai))
Ha': valid_state_prop X s
∧ Forall
    (λ ai : plan_item,
       option_valid_message_prop X (input_a ai))
    prefa
  ∧ (∀ (prefa0 suffa : plan) (ai : plan_item),
       prefa = prefa0 ++ [ai] ++ suffa
       → let lst := (apply_plan s prefa0).2 in
         valid (label_a ai) (lst, input_a ai))
valid
  (label_a
     {| label_a := label_a0; input_a := input_a0 |})
  (lst,
   input_a
     {| label_a := label_a0; input_a := input_a0 |})
      simpl.message: Type
X: VLSM message
s: state X
prefa: plan
label_a0: label X
input_a0: option message
lst: state X
Heqlst: lst = (apply_plan s prefa).2
dest: state X
out: option message
Hx: finite_valid_trace_from X lst
  (rev
     [{|
        l := label_a0;
        input := input_a0;
        destination := dest;
        output := out
      |}], dest).1
Ha: finite_valid_plan_from s prefa
IHa: finite_valid_plan_from s prefa
↔ valid_state_prop X s
  ∧ Forall
      (λ ai : plan_item,
         option_valid_message_prop X
           (input_a ai)) prefa
    ∧ (∀ (prefa0 suffa : plan) (ai : plan_item),
         prefa = prefa0 ++ [ai] ++ suffa
         → let lst := (apply_plan s prefa0).2 in
           valid (label_a ai) (lst, input_a ai))
Ha': valid_state_prop X s
∧ Forall
    (λ ai : plan_item,
       option_valid_message_prop X (input_a ai))
    prefa
  ∧ (∀ (prefa0 suffa : plan) (ai : plan_item),
       prefa = prefa0 ++ [ai] ++ suffa
       → let lst := (apply_plan s prefa0).2 in
         valid (label_a ai) (lst, input_a ai))
valid label_a0 (lst, input_a0) simpl in Hx.message: Type
X: VLSM message
s: state X
prefa: plan
label_a0: label X
input_a0: option message
lst: state X
Heqlst: lst = (apply_plan s prefa).2
dest: state X
out: option message
Hx: finite_valid_trace_from X lst
  [{|
     l := label_a0;
     input := input_a0;
     destination := dest;
     output := out
   |}]
Ha: finite_valid_plan_from s prefa
IHa: finite_valid_plan_from s prefa
↔ valid_state_prop X s
  ∧ Forall
      (λ ai : plan_item,
         option_valid_message_prop X
           (input_a ai)) prefa
    ∧ (∀ (prefa0 suffa : plan) (ai : plan_item),
         prefa = prefa0 ++ [ai] ++ suffa
         → let lst := (apply_plan s prefa0).2 in
           valid (label_a ai) (lst, input_a ai))
Ha': valid_state_prop X s
∧ Forall
    (λ ai : plan_item,
       option_valid_message_prop X (input_a ai))
    prefa
  ∧ (∀ (prefa0 suffa : plan) (ai : plan_item),
       prefa = prefa0 ++ [ai] ++ suffa
       → let lst := (apply_plan s prefa0).2 in
         valid (label_a ai) (lst, input_a ai))
valid label_a0 (lst, input_a0) inversion Hx.message: Type
X: VLSM message
s: state X
prefa: plan
label_a0: label X
input_a0: option message
lst: state X
Heqlst: lst = (apply_plan s prefa).2
dest: state X
out: option message
Hx: finite_valid_trace_from X lst
  [{|
     l := label_a0;
     input := input_a0;
     destination := dest;
     output := out
   |}]
Ha: finite_valid_plan_from s prefa
IHa: finite_valid_plan_from s prefa
↔ valid_state_prop X s
  ∧ Forall
      (λ ai : plan_item,
         option_valid_message_prop X
           (input_a ai)) prefa
    ∧ (∀ (prefa0 suffa : plan) (ai : plan_item),
         prefa = prefa0 ++ [ai] ++ suffa
         → let lst := (apply_plan s prefa0).2 in
           valid (label_a ai) (lst, input_a ai))
Ha': valid_state_prop X s
∧ Forall
    (λ ai : plan_item,
       option_valid_message_prop X (input_a ai))
    prefa
  ∧ (∀ (prefa0 suffa : plan) (ai : plan_item),
       prefa = prefa0 ++ [ai] ++ suffa
       → let lst := (apply_plan s prefa0).2 in
         valid (label_a ai) (lst, input_a ai))
s0: state X
tl: list transition_item
s': state X
iom, oom: option message
l: label X
Htl: finite_valid_trace_from X dest []
Ht: input_valid_transition X label_a0 (
  lst, input_a0) (dest, out)
H: s' = lst
H1: l = label_a0
H2: iom = input_a0
H3: s0 = dest
H4: oom = out
H5: tl = []
valid label_a0 (lst, input_a0) subst.message: Type
X: VLSM message
s: state X
prefa: plan
label_a0: label X
input_a0: option message
dest: state X
out: option message
Hx: finite_valid_trace_from X 
  (apply_plan s prefa).2
  [{|
     l := label_a0;
     input := input_a0;
     destination := dest;
     output := out
   |}]
Ha: finite_valid_plan_from s prefa
IHa: finite_valid_plan_from s prefa
↔ valid_state_prop X s
  ∧ Forall
      (λ ai : plan_item,
         option_valid_message_prop X
           (input_a ai)) prefa
    ∧ (∀ (prefa0 suffa : plan) (ai : plan_item),
         prefa = prefa0 ++ [ai] ++ suffa
         → let lst := (apply_plan s prefa0).2 in
           valid (label_a ai) (lst, input_a ai))
Ha': valid_state_prop X s
∧ Forall
    (λ ai : plan_item,
       option_valid_message_prop X (input_a ai))
    prefa
  ∧ (∀ (prefa0 suffa : plan) (ai : plan_item),
       prefa = prefa0 ++ [ai] ++ suffa
       → let lst := (apply_plan s prefa0).2 in
         valid (label_a ai) (lst, input_a ai))
Htl: finite_valid_trace_from X dest []
Ht: input_valid_transition X label_a0
  ((apply_plan s prefa).2, input_a0) (
  dest, out)
valid label_a0 ((apply_plan s prefa).2, input_a0)
      by apply Ht.
    +message: Type
X: VLSM message
s: state X
x: plan_item
a: list plan_item
IHa: finite_valid_plan_from s a
↔ valid_state_prop X s
  ∧ Forall
      (λ ai : plan_item,
         option_valid_message_prop X
           (input_a ai)) a
    ∧ (∀ (prefa suffa : plan) (ai : plan_item),
         a = prefa ++ [ai] ++ suffa
         → let lst := (apply_plan s prefa).2 in
           valid (label_a ai) (lst, input_a ai))
Ha: finite_valid_plan_from s a
Hx: finite_valid_plan_from (apply_plan s a).2 [x]
prefa, suffa: plan
ai: plan_item
Heqa: a ++ [x] = prefa ++ [ai] ++ suffa
lst:= (apply_plan s prefa).2: state X
Ha': valid_state_prop X s
∧ Forall
    (λ ai : plan_item,
       option_valid_message_prop X (input_a ai))
    a
  ∧ (∀ (prefa suffa : plan) (ai : plan_item),
       a = prefa ++ [ai] ++ suffa
       → let lst := (apply_plan s prefa).2 in
         valid (label_a ai) (lst, input_a ai))
H: suffa ≠ []
valid (label_a ai) (lst, input_a ai) apply exists_last in H.message: Type
X: VLSM message
s: state X
x: plan_item
a: list plan_item
IHa: finite_valid_plan_from s a
↔ valid_state_prop X s
  ∧ Forall
      (λ ai : plan_item,
         option_valid_message_prop X
           (input_a ai)) a
    ∧ (∀ (prefa suffa : plan) (ai : plan_item),
         a = prefa ++ [ai] ++ suffa
         → let lst := (apply_plan s prefa).2 in
           valid (label_a ai) (lst, input_a ai))
Ha: finite_valid_plan_from s a
Hx: finite_valid_plan_from (apply_plan s a).2 [x]
prefa, suffa: plan
ai: plan_item
Heqa: a ++ [x] = prefa ++ [ai] ++ suffa
lst:= (apply_plan s prefa).2: state X
Ha': valid_state_prop X s
∧ Forall
    (λ ai : plan_item,
       option_valid_message_prop X (input_a ai))
    a
  ∧ (∀ (prefa suffa : plan) (ai : plan_item),
       a = prefa ++ [ai] ++ suffa
       → let lst := (apply_plan s prefa).2 in
         valid (label_a ai) (lst, input_a ai))
H: {l' : list plan_item &
{a : plan_item | suffa = l' ++ [a]}}
valid (label_a ai) (lst, input_a ai) destruct H as [suffa' [x' Heq]].message: Type
X: VLSM message
s: state X
x: plan_item
a: list plan_item
IHa: finite_valid_plan_from s a
↔ valid_state_prop X s
  ∧ Forall
      (λ ai : plan_item,
         option_valid_message_prop X
           (input_a ai)) a
    ∧ (∀ (prefa suffa : plan) (ai : plan_item),
         a = prefa ++ [ai] ++ suffa
         → let lst := (apply_plan s prefa).2 in
           valid (label_a ai) (lst, input_a ai))
Ha: finite_valid_plan_from s a
Hx: finite_valid_plan_from (apply_plan s a).2 [x]
prefa, suffa: plan
ai: plan_item
Heqa: a ++ [x] = prefa ++ [ai] ++ suffa
lst:= (apply_plan s prefa).2: state X
Ha': valid_state_prop X s
∧ Forall
    (λ ai : plan_item,
       option_valid_message_prop X (input_a ai))
    a
  ∧ (∀ (prefa suffa : plan) (ai : plan_item),
       a = prefa ++ [ai] ++ suffa
       → let lst := (apply_plan s prefa).2 in
         valid (label_a ai) (lst, input_a ai))
suffa': list plan_item
x': plan_item
Heq: suffa = suffa' ++ [x']
valid (label_a ai) (lst, input_a ai) subst.message: Type
X: VLSM message
s: state X
x: plan_item
a: list plan_item
IHa: finite_valid_plan_from s a
↔ valid_state_prop X s
  ∧ Forall
      (λ ai : plan_item,
         option_valid_message_prop X
           (input_a ai)) a
    ∧ (∀ (prefa suffa : plan) (ai : plan_item),
         a = prefa ++ [ai] ++ suffa
         → let lst := (apply_plan s prefa).2 in
           valid (label_a ai) (lst, input_a ai))
Ha: finite_valid_plan_from s a
Hx: finite_valid_plan_from (apply_plan s a).2 [x]
prefa: plan
ai: plan_item
suffa': list plan_item
x': plan_item
Heqa: a ++ [x] = prefa ++ [ai] ++ suffa' ++ [x']
lst:= (apply_plan s prefa).2: state X
Ha': valid_state_prop X s
∧ Forall
    (λ ai : plan_item,
       option_valid_message_prop X (input_a ai))
    a
  ∧ (∀ (prefa suffa : plan) (ai : plan_item),
       a = prefa ++ [ai] ++ suffa
       → let lst := (apply_plan s prefa).2 in
         valid (label_a ai) (lst, input_a ai))
valid (label_a ai) (lst, input_a ai)
      repeat rewrite app_assoc in Heqa.message: Type
X: VLSM message
s: state X
x: plan_item
a: list plan_item
IHa: finite_valid_plan_from s a
↔ valid_state_prop X s
  ∧ Forall
      (λ ai : plan_item,
         option_valid_message_prop X
           (input_a ai)) a
    ∧ (∀ (prefa suffa : plan) (ai : plan_item),
         a = prefa ++ [ai] ++ suffa
         → let lst := (apply_plan s prefa).2 in
           valid (label_a ai) (lst, input_a ai))
Ha: finite_valid_plan_from s a
Hx: finite_valid_plan_from (apply_plan s a).2 [x]
prefa: plan
ai: plan_item
suffa': list plan_item
x': plan_item
Heqa: a ++ [x] = ((prefa ++ [ai]) ++ suffa') ++ [x']
lst:= (apply_plan s prefa).2: state X
Ha': valid_state_prop X s
∧ Forall
    (λ ai : plan_item,
       option_valid_message_prop X (input_a ai))
    a
  ∧ (∀ (prefa suffa : plan) (ai : plan_item),
       a = prefa ++ [ai] ++ suffa
       → let lst := (apply_plan s prefa).2 in
         valid (label_a ai) (lst, input_a ai))
valid (label_a ai) (lst, input_a ai)
      apply app_inj_tail in Heqa.message: Type
X: VLSM message
s: state X
x: plan_item
a: list plan_item
IHa: finite_valid_plan_from s a
↔ valid_state_prop X s
  ∧ Forall
      (λ ai : plan_item,
         option_valid_message_prop X
           (input_a ai)) a
    ∧ (∀ (prefa suffa : plan) (ai : plan_item),
         a = prefa ++ [ai] ++ suffa
         → let lst := (apply_plan s prefa).2 in
           valid (label_a ai) (lst, input_a ai))
Ha: finite_valid_plan_from s a
Hx: finite_valid_plan_from (apply_plan s a).2 [x]
prefa: plan
ai: plan_item
suffa': list plan_item
x': plan_item
Heqa: a = (prefa ++ [ai]) ++ suffa' ∧ x = x'
lst:= (apply_plan s prefa).2: state X
Ha': valid_state_prop X s
∧ Forall
    (λ ai : plan_item,
       option_valid_message_prop X (input_a ai))
    a
  ∧ (∀ (prefa suffa : plan) (ai : plan_item),
       a = prefa ++ [ai] ++ suffa
       → let lst := (apply_plan s prefa).2 in
         valid (label_a ai) (lst, input_a ai))
valid (label_a ai) (lst, input_a ai) rewrite <- app_assoc in Heqa.message: Type
X: VLSM message
s: state X
x: plan_item
a: list plan_item
IHa: finite_valid_plan_from s a
↔ valid_state_prop X s
  ∧ Forall
      (λ ai : plan_item,
         option_valid_message_prop X
           (input_a ai)) a
    ∧ (∀ (prefa suffa : plan) (ai : plan_item),
         a = prefa ++ [ai] ++ suffa
         → let lst := (apply_plan s prefa).2 in
           valid (label_a ai) (lst, input_a ai))
Ha: finite_valid_plan_from s a
Hx: finite_valid_plan_from (apply_plan s a).2 [x]
prefa: plan
ai: plan_item
suffa': list plan_item
x': plan_item
Heqa: a = prefa ++ [ai] ++ suffa' ∧ x = x'
lst:= (apply_plan s prefa).2: state X
Ha': valid_state_prop X s
∧ Forall
    (λ ai : plan_item,
       option_valid_message_prop X (input_a ai))
    a
  ∧ (∀ (prefa suffa : plan) (ai : plan_item),
       a = prefa ++ [ai] ++ suffa
       → let lst := (apply_plan s prefa).2 in
         valid (label_a ai) (lst, input_a ai))
valid (label_a ai) (lst, input_a ai) destruct Heqa; subst.message: Type
X: VLSM message
s: state X
prefa: plan
ai: plan_item
suffa': list plan_item
x': plan_item
Hx: finite_valid_plan_from
  (apply_plan s (prefa ++ [ai] ++ suffa')).2 [x']
Ha: finite_valid_plan_from s
  (prefa ++ [ai] ++ suffa')
IHa: finite_valid_plan_from s
  (prefa ++ [ai] ++ suffa')
↔ valid_state_prop X s
  ∧ Forall
      (λ ai : plan_item,
         option_valid_message_prop X
           (input_a ai))
      (prefa ++ [ai] ++ suffa')
    ∧ (∀ (prefa0 suffa : plan) (ai0 : plan_item),
         prefa ++ [ai] ++ suffa' =
         prefa0 ++ [ai0] ++ suffa
         → let lst := (apply_plan s prefa0).2 in
           valid (label_a ai0)
             (lst, input_a ai0))
lst:= (apply_plan s prefa).2: state X
Ha': valid_state_prop X s
∧ Forall
    (λ ai : plan_item,
       option_valid_message_prop X (input_a ai))
    (prefa ++ [ai] ++ suffa')
  ∧ (∀ (prefa0 suffa : plan) (ai0 : plan_item),
       prefa ++ [ai] ++ suffa' =
       prefa0 ++ [ai0] ++ suffa
       → let lst := (apply_plan s prefa0).2 in
         valid (label_a ai0) (lst, input_a ai0))
valid (label_a ai) (lst, input_a ai)
      destruct Ha' as [_ [_ Ha']].message: Type
X: VLSM message
s: state X
prefa: plan
ai: plan_item
suffa': list plan_item
x': plan_item
Hx: finite_valid_plan_from
  (apply_plan s (prefa ++ [ai] ++ suffa')).2 [x']
Ha: finite_valid_plan_from s
  (prefa ++ [ai] ++ suffa')
IHa: finite_valid_plan_from s
  (prefa ++ [ai] ++ suffa')
↔ valid_state_prop X s
  ∧ Forall
      (λ ai : plan_item,
         option_valid_message_prop X
           (input_a ai))
      (prefa ++ [ai] ++ suffa')
    ∧ (∀ (prefa0 suffa : plan) (ai0 : plan_item),
         prefa ++ [ai] ++ suffa' =
         prefa0 ++ [ai0] ++ suffa
         → let lst := (apply_plan s prefa0).2 in
           valid (label_a ai0)
             (lst, input_a ai0))
lst:= (apply_plan s prefa).2: state X
Ha': ∀ (prefa0 suffa : plan) (ai0 : plan_item),
  prefa ++ [ai] ++ suffa' =
  prefa0 ++ [ai0] ++ suffa
  → let lst := (apply_plan s prefa0).2 in
    valid (label_a ai0) (lst, input_a ai0)
valid (label_a ai) (lst, input_a ai)
      by eapply IHa.
  -message: Type
X: VLSM message
s: state X
x: plan_item
a: list plan_item
IHa: finite_valid_plan_from s a
↔ valid_state_prop X s
  ∧ Forall
      (λ ai : plan_item,
         option_valid_message_prop X
           (input_a ai)) a
    ∧ (∀ (prefa suffa : plan) (ai : plan_item),
         a = prefa ++ [ai] ++ suffa
         → let lst := (apply_plan s prefa).2 in
           valid (label_a ai) (lst, input_a ai))
H: valid_state_prop X s
∧ Forall
    (λ ai : plan_item,
       option_valid_message_prop X (input_a ai))
    (a ++ [x])
  ∧ (∀ (prefa suffa : plan) (ai : plan_item),
       a ++ [x] = prefa ++ [ai] ++ suffa
       → let lst := (apply_plan s prefa).2 in
         valid (label_a ai) (lst, input_a ai))
finite_valid_plan_from s (a ++ [x]) destruct H as [Hs [Hinput Hvalid]].message: Type
X: VLSM message
s: state X
x: plan_item
a: list plan_item
IHa: finite_valid_plan_from s a
↔ valid_state_prop X s
  ∧ Forall
      (λ ai : plan_item,
         option_valid_message_prop X
           (input_a ai)) a
    ∧ (∀ (prefa suffa : plan) (ai : plan_item),
         a = prefa ++ [ai] ++ suffa
         → let lst := (apply_plan s prefa).2 in
           valid (label_a ai) (lst, input_a ai))
Hs: valid_state_prop X s
Hinput: Forall
  (λ ai : plan_item,
     option_valid_message_prop X (input_a ai))
  (a ++ [x])
Hvalid: ∀ (prefa suffa : plan) (ai : plan_item),
  a ++ [x] = prefa ++ [ai] ++ suffa
  → let lst := (apply_plan s prefa).2 in
    valid (label_a ai) (lst, input_a ai)
finite_valid_plan_from s (a ++ [x])
    apply Forall_app in Hinput.message: Type
X: VLSM message
s: state X
x: plan_item
a: list plan_item
IHa: finite_valid_plan_from s a
↔ valid_state_prop X s
  ∧ Forall
      (λ ai : plan_item,
         option_valid_message_prop X
           (input_a ai)) a
    ∧ (∀ (prefa suffa : plan) (ai : plan_item),
         a = prefa ++ [ai] ++ suffa
         → let lst := (apply_plan s prefa).2 in
           valid (label_a ai) (lst, input_a ai))
Hs: valid_state_prop X s
Hinput: Forall
  (λ ai : plan_item,
     option_valid_message_prop X (input_a ai))
  a
∧ Forall
    (λ ai : plan_item,
       option_valid_message_prop X
         (input_a ai)) [x]
Hvalid: ∀ (prefa suffa : plan) (ai : plan_item),
  a ++ [x] = prefa ++ [ai] ++ suffa
  → let lst := (apply_plan s prefa).2 in
    valid (label_a ai) (lst, input_a ai)
finite_valid_plan_from s (a ++ [x]) destruct Hinput as [Hinput Hinput_ai].message: Type
X: VLSM message
s: state X
x: plan_item
a: list plan_item
IHa: finite_valid_plan_from s a
↔ valid_state_prop X s
  ∧ Forall
      (λ ai : plan_item,
         option_valid_message_prop X
           (input_a ai)) a
    ∧ (∀ (prefa suffa : plan) (ai : plan_item),
         a = prefa ++ [ai] ++ suffa
         → let lst := (apply_plan s prefa).2 in
           valid (label_a ai) (lst, input_a ai))
Hs: valid_state_prop X s
Hinput: Forall
  (λ ai : plan_item,
     option_valid_message_prop X (input_a ai))
  a
Hinput_ai: Forall
  (λ ai : plan_item,
     option_valid_message_prop X
       (input_a ai)) [x]
Hvalid: ∀ (prefa suffa : plan) (ai : plan_item),
  a ++ [x] = prefa ++ [ai] ++ suffa
  → let lst := (apply_plan s prefa).2 in
    valid (label_a ai) (lst, input_a ai)
finite_valid_plan_from s (a ++ [x])
    apply finite_valid_plan_from_app_iff.message: Type
X: VLSM message
s: state X
x: plan_item
a: list plan_item
IHa: finite_valid_plan_from s a
↔ valid_state_prop X s
  ∧ Forall
      (λ ai : plan_item,
         option_valid_message_prop X
           (input_a ai)) a
    ∧ (∀ (prefa suffa : plan) (ai : plan_item),
         a = prefa ++ [ai] ++ suffa
         → let lst := (apply_plan s prefa).2 in
           valid (label_a ai) (lst, input_a ai))
Hs: valid_state_prop X s
Hinput: Forall
  (λ ai : plan_item,
     option_valid_message_prop X (input_a ai))
  a
Hinput_ai: Forall
  (λ ai : plan_item,
     option_valid_message_prop X
       (input_a ai)) [x]
Hvalid: ∀ (prefa suffa : plan) (ai : plan_item),
  a ++ [x] = prefa ++ [ai] ++ suffa
  → let lst := (apply_plan s prefa).2 in
    valid (label_a ai) (lst, input_a ai)
finite_valid_plan_from s a
∧ finite_valid_plan_from (apply_plan s a).2 [x]
    assert (Ha : finite_valid_plan_from s a); try (by split)
    ; try apply IHa; repeat split; try done.message: Type
X: VLSM message
s: state X
x: plan_item
a: list plan_item
IHa: finite_valid_plan_from s a
↔ valid_state_prop X s
  ∧ Forall
      (λ ai : plan_item,
         option_valid_message_prop X
           (input_a ai)) a
    ∧ (∀ (prefa suffa : plan) (ai : plan_item),
         a = prefa ++ [ai] ++ suffa
         → let lst := (apply_plan s prefa).2 in
           valid (label_a ai) (lst, input_a ai))
Hs: valid_state_prop X s
Hinput: Forall
  (λ ai : plan_item,
     option_valid_message_prop X (input_a ai))
  a
Hinput_ai: Forall
  (λ ai : plan_item,
     option_valid_message_prop X
       (input_a ai)) [x]
Hvalid: ∀ (prefa suffa : plan) (ai : plan_item),
  a ++ [x] = prefa ++ [ai] ++ suffa
  → let lst := (apply_plan s prefa).2 in
    valid (label_a ai) (lst, input_a ai)
∀ (prefa suffa : plan) (ai : plan_item),
  a = prefa ++ [ai] ++ suffa
  → let lst := (apply_plan s prefa).2 in
    valid (label_a ai) (lst, input_a ai)
message: Type
X: VLSM message
s: state X
x: plan_item
a: list plan_item
IHa: finite_valid_plan_from s a
↔ valid_state_prop X s
  ∧ Forall
      (λ ai : plan_item,
         option_valid_message_prop X
           (input_a ai)) a
    ∧ (∀ (prefa suffa : plan) (ai : plan_item),
         a = prefa ++ [ai] ++ suffa
         → let lst := (apply_plan s prefa).2 in
           valid (label_a ai) (lst, input_a ai))
Hs: valid_state_prop X s
Hinput: Forall
  (λ ai : plan_item,
     option_valid_message_prop X (input_a ai))
  a
Hinput_ai: Forall
  (λ ai : plan_item,
     option_valid_message_prop X
       (input_a ai)) [x]
Hvalid: ∀ (prefa suffa : plan) (ai : plan_item),
  a ++ [x] = prefa ++ [ai] ++ suffa
  → let lst := (apply_plan s prefa).2 in
    valid (label_a ai) (lst, input_a ai)
Ha: finite_valid_plan_from s a
finite_valid_plan_from (apply_plan s a).2 [x]
    +message: Type
X: VLSM message
s: state X
x: plan_item
a: list plan_item
IHa: finite_valid_plan_from s a
↔ valid_state_prop X s
  ∧ Forall
      (λ ai : plan_item,
         option_valid_message_prop X
           (input_a ai)) a
    ∧ (∀ (prefa suffa : plan) (ai : plan_item),
         a = prefa ++ [ai] ++ suffa
         → let lst := (apply_plan s prefa).2 in
           valid (label_a ai) (lst, input_a ai))
Hs: valid_state_prop X s
Hinput: Forall
  (λ ai : plan_item,
     option_valid_message_prop X (input_a ai))
  a
Hinput_ai: Forall
  (λ ai : plan_item,
     option_valid_message_prop X
       (input_a ai)) [x]
Hvalid: ∀ (prefa suffa : plan) (ai : plan_item),
  a ++ [x] = prefa ++ [ai] ++ suffa
  → let lst := (apply_plan s prefa).2 in
    valid (label_a ai) (lst, input_a ai)
∀ (prefa suffa : plan) (ai : plan_item),
  a = prefa ++ [ai] ++ suffa
  → let lst := (apply_plan s prefa).2 in
    valid (label_a ai) (lst, input_a ai) intros.message: Type
X: VLSM message
s: state X
x: plan_item
a: list plan_item
IHa: finite_valid_plan_from s a
↔ valid_state_prop X s
  ∧ Forall
      (λ ai : plan_item,
         option_valid_message_prop X
           (input_a ai)) a
    ∧ (∀ (prefa suffa : plan) (ai : plan_item),
         a = prefa ++ [ai] ++ suffa
         → let lst := (apply_plan s prefa).2 in
           valid (label_a ai) (lst, input_a ai))
Hs: valid_state_prop X s
Hinput: Forall
  (λ ai : plan_item,
     option_valid_message_prop X (input_a ai))
  a
Hinput_ai: Forall
  (λ ai : plan_item,
     option_valid_message_prop X
       (input_a ai)) [x]
Hvalid: ∀ (prefa suffa : plan) (ai : plan_item),
  a ++ [x] = prefa ++ [ai] ++ suffa
  → let lst := (apply_plan s prefa).2 in
    valid (label_a ai) (lst, input_a ai)
prefa, suffa: plan
ai: plan_item
Heqa: a = prefa ++ [ai] ++ suffa
lst:= (apply_plan s prefa).2: state X
valid (label_a ai) (lst, input_a ai)
      specialize (Hvalid prefa (suffa ++ [x]) ai).message: Type
X: VLSM message
s: state X
x: plan_item
a: list plan_item
IHa: finite_valid_plan_from s a
↔ valid_state_prop X s
  ∧ Forall
      (λ ai : plan_item,
         option_valid_message_prop X
           (input_a ai)) a
    ∧ (∀ (prefa suffa : plan) (ai : plan_item),
         a = prefa ++ [ai] ++ suffa
         → let lst := (apply_plan s prefa).2 in
           valid (label_a ai) (lst, input_a ai))
Hs: valid_state_prop X s
Hinput: Forall
  (λ ai : plan_item,
     option_valid_message_prop X (input_a ai))
  a
Hinput_ai: Forall
  (λ ai : plan_item,
     option_valid_message_prop X
       (input_a ai)) [x]
prefa, suffa: plan
ai: plan_item
Hvalid: a ++ [x] = prefa ++ [ai] ++ suffa ++ [x]
→ let lst := (apply_plan s prefa).2 in
  valid (label_a ai) (lst, input_a ai)
Heqa: a = prefa ++ [ai] ++ suffa
lst:= (apply_plan s prefa).2: state X
valid (label_a ai) (lst, input_a ai)
      repeat rewrite app_assoc in *.message: Type
X: VLSM message
s: state X
x: plan_item
a: list plan_item
IHa: finite_valid_plan_from s a
↔ valid_state_prop X s
  ∧ Forall
      (λ ai : plan_item,
         option_valid_message_prop X
           (input_a ai)) a
    ∧ (∀ (prefa suffa : plan) (ai : plan_item),
         a = prefa ++ [ai] ++ suffa
         → let lst := (apply_plan s prefa).2 in
           valid (label_a ai) (lst, input_a ai))
Hs: valid_state_prop X s
Hinput: Forall
  (λ ai : plan_item,
     option_valid_message_prop X (input_a ai))
  a
Hinput_ai: Forall
  (λ ai : plan_item,
     option_valid_message_prop X
       (input_a ai)) [x]
prefa, suffa: plan
ai: plan_item
Hvalid: a ++ [x] = ((prefa ++ [ai]) ++ suffa) ++ [x]
→ let lst := (apply_plan s prefa).2 in
  valid (label_a ai) (lst, input_a ai)
Heqa: a = (prefa ++ [ai]) ++ suffa
lst:= (apply_plan s prefa).2: state X
valid (label_a ai) (lst, input_a ai)
      by subst a; apply Hvalid.
    +message: Type
X: VLSM message
s: state X
x: plan_item
a: list plan_item
IHa: finite_valid_plan_from s a
↔ valid_state_prop X s
  ∧ Forall
      (λ ai : plan_item,
         option_valid_message_prop X
           (input_a ai)) a
    ∧ (∀ (prefa suffa : plan) (ai : plan_item),
         a = prefa ++ [ai] ++ suffa
         → let lst := (apply_plan s prefa).2 in
           valid (label_a ai) (lst, input_a ai))
Hs: valid_state_prop X s
Hinput: Forall
  (λ ai : plan_item,
     option_valid_message_prop X (input_a ai))
  a
Hinput_ai: Forall
  (λ ai : plan_item,
     option_valid_message_prop X
       (input_a ai)) [x]
Hvalid: ∀ (prefa suffa : plan) (ai : plan_item),
  a ++ [x] = prefa ++ [ai] ++ suffa
  → let lst := (apply_plan s prefa).2 in
    valid (label_a ai) (lst, input_a ai)
Ha: finite_valid_plan_from s a
finite_valid_plan_from (apply_plan s a).2 [x] unfold finite_valid_plan_from.message: Type
X: VLSM message
s: state X
x: plan_item
a: list plan_item
IHa: finite_valid_plan_from s a
↔ valid_state_prop X s
  ∧ Forall
      (λ ai : plan_item,
         option_valid_message_prop X
           (input_a ai)) a
    ∧ (∀ (prefa suffa : plan) (ai : plan_item),
         a = prefa ++ [ai] ++ suffa
         → let lst := (apply_plan s prefa).2 in
           valid (label_a ai) (lst, input_a ai))
Hs: valid_state_prop X s
Hinput: Forall
  (λ ai : plan_item,
     option_valid_message_prop X (input_a ai))
  a
Hinput_ai: Forall
  (λ ai : plan_item,
     option_valid_message_prop X
       (input_a ai)) [x]
Hvalid: ∀ (prefa suffa : plan) (ai : plan_item),
  a ++ [x] = prefa ++ [ai] ++ suffa
  → let lst := (apply_plan s prefa).2 in
    valid (label_a ai) (lst, input_a ai)
Ha: finite_valid_plan_from s a
finite_valid_trace_from X (apply_plan s a).2
  (apply_plan (apply_plan s a).2 [x]).1
      specialize (Hvalid a [] x).message: Type
X: VLSM message
s: state X
x: plan_item
a: list plan_item
IHa: finite_valid_plan_from s a
↔ valid_state_prop X s
  ∧ Forall
      (λ ai : plan_item,
         option_valid_message_prop X
           (input_a ai)) a
    ∧ (∀ (prefa suffa : plan) (ai : plan_item),
         a = prefa ++ [ai] ++ suffa
         → let lst := (apply_plan s prefa).2 in
           valid (label_a ai) (lst, input_a ai))
Hs: valid_state_prop X s
Hinput: Forall
  (λ ai : plan_item,
     option_valid_message_prop X (input_a ai))
  a
Hinput_ai: Forall
  (λ ai : plan_item,
     option_valid_message_prop X
       (input_a ai)) [x]
Hvalid: a ++ [x] = a ++ [x] ++ []
→ let lst := (apply_plan s a).2 in
  valid (label_a x) (lst, input_a x)
Ha: finite_valid_plan_from s a
finite_valid_trace_from X (apply_plan s a).2
  (apply_plan (apply_plan s a).2 [x]).1
      rewrite app_assoc in Hvalid.message: Type
X: VLSM message
s: state X
x: plan_item
a: list plan_item
IHa: finite_valid_plan_from s a
↔ valid_state_prop X s
  ∧ Forall
      (λ ai : plan_item,
         option_valid_message_prop X
           (input_a ai)) a
    ∧ (∀ (prefa suffa : plan) (ai : plan_item),
         a = prefa ++ [ai] ++ suffa
         → let lst := (apply_plan s prefa).2 in
           valid (label_a ai) (lst, input_a ai))
Hs: valid_state_prop X s
Hinput: Forall
  (λ ai : plan_item,
     option_valid_message_prop X (input_a ai))
  a
Hinput_ai: Forall
  (λ ai : plan_item,
     option_valid_message_prop X
       (input_a ai)) [x]
Hvalid: a ++ [x] = (a ++ [x]) ++ []
→ let lst := (apply_plan s a).2 in
  valid (label_a x) (lst, input_a x)
Ha: finite_valid_plan_from s a
finite_valid_trace_from X (apply_plan s a).2
  (apply_plan (apply_plan s a).2 [x]).1 rewrite app_nil_r in Hvalid.message: Type
X: VLSM message
s: state X
x: plan_item
a: list plan_item
IHa: finite_valid_plan_from s a
↔ valid_state_prop X s
  ∧ Forall
      (λ ai : plan_item,
         option_valid_message_prop X
           (input_a ai)) a
    ∧ (∀ (prefa suffa : plan) (ai : plan_item),
         a = prefa ++ [ai] ++ suffa
         → let lst := (apply_plan s prefa).2 in
           valid (label_a ai) (lst, input_a ai))
Hs: valid_state_prop X s
Hinput: Forall
  (λ ai : plan_item,
     option_valid_message_prop X (input_a ai))
  a
Hinput_ai: Forall
  (λ ai : plan_item,
     option_valid_message_prop X
       (input_a ai)) [x]
Hvalid: a ++ [x] = a ++ [x]
→ let lst := (apply_plan s a).2 in
  valid (label_a x) (lst, input_a x)
Ha: finite_valid_plan_from s a
finite_valid_trace_from X (apply_plan s a).2
  (apply_plan (apply_plan s a).2 [x]).1
      specialize (Hvalid eq_refl).message: Type
X: VLSM message
s: state X
x: plan_item
a: list plan_item
IHa: finite_valid_plan_from s a
↔ valid_state_prop X s
  ∧ Forall
      (λ ai : plan_item,
         option_valid_message_prop X
           (input_a ai)) a
    ∧ (∀ (prefa suffa : plan) (ai : plan_item),
         a = prefa ++ [ai] ++ suffa
         → let lst := (apply_plan s prefa).2 in
           valid (label_a ai) (lst, input_a ai))
Hs: valid_state_prop X s
Hinput: Forall
  (λ ai : plan_item,
     option_valid_message_prop X (input_a ai))
  a
Hinput_ai: Forall
  (λ ai : plan_item,
     option_valid_message_prop X
       (input_a ai)) [x]
Hvalid: let lst := (apply_plan s a).2 in
valid (label_a x) (lst, input_a x)
Ha: finite_valid_plan_from s a
finite_valid_trace_from X (apply_plan s a).2
  (apply_plan (apply_plan s a).2 [x]).1
      remember (snd (apply_plan s a)) as sa.message: Type
X: VLSM message
s: state X
x: plan_item
a: list plan_item
IHa: finite_valid_plan_from s a
↔ valid_state_prop X s
  ∧ Forall
      (λ ai : plan_item,
         option_valid_message_prop X
           (input_a ai)) a
    ∧ (∀ (prefa suffa : plan) (ai : plan_item),
         a = prefa ++ [ai] ++ suffa
         → let lst := (apply_plan s prefa).2 in
           valid (label_a ai) (lst, input_a ai))
Hs: valid_state_prop X s
Hinput: Forall
  (λ ai : plan_item,
     option_valid_message_prop X (input_a ai))
  a
Hinput_ai: Forall
  (λ ai : plan_item,
     option_valid_message_prop X
       (input_a ai)) [x]
sa: state X
Heqsa: sa = (apply_plan s a).2
Hvalid: let lst := sa in
valid (label_a x) (lst, input_a x)
Ha: finite_valid_plan_from s a
finite_valid_trace_from X sa (apply_plan sa [x]).1
      unfold apply_plan, _apply_plan.message: Type
X: VLSM message
s: state X
x: plan_item
a: list plan_item
IHa: finite_valid_plan_from s a
↔ valid_state_prop X s
  ∧ Forall
      (λ ai : plan_item,
         option_valid_message_prop X
           (input_a ai)) a
    ∧ (∀ (prefa suffa : plan) (ai : plan_item),
         a = prefa ++ [ai] ++ suffa
         → let lst := (apply_plan s prefa).2 in
           valid (label_a ai) (lst, input_a ai))
Hs: valid_state_prop X s
Hinput: Forall
  (λ ai : plan_item,
     option_valid_message_prop X (input_a ai))
  a
Hinput_ai: Forall
  (λ ai : plan_item,
     option_valid_message_prop X
       (input_a ai)) [x]
sa: state X
Heqsa: sa = (apply_plan s a).2
Hvalid: let lst := sa in
valid (label_a x) (lst, input_a x)
Ha: finite_valid_plan_from s a
finite_valid_trace_from X sa
  (let (final, items) :=
     foldr _apply_plan_folder (sa, []) (rev [x]) in
   (rev items, final)).1 simpl.message: Type
X: VLSM message
s: state X
x: plan_item
a: list plan_item
IHa: finite_valid_plan_from s a
↔ valid_state_prop X s
  ∧ Forall
      (λ ai : plan_item,
         option_valid_message_prop X
           (input_a ai)) a
    ∧ (∀ (prefa suffa : plan) (ai : plan_item),
         a = prefa ++ [ai] ++ suffa
         → let lst := (apply_plan s prefa).2 in
           valid (label_a ai) (lst, input_a ai))
Hs: valid_state_prop X s
Hinput: Forall
  (λ ai : plan_item,
     option_valid_message_prop X (input_a ai))
  a
Hinput_ai: Forall
  (λ ai : plan_item,
     option_valid_message_prop X
       (input_a ai)) [x]
sa: state X
Heqsa: sa = (apply_plan s a).2
Hvalid: let lst := sa in
valid (label_a x) (lst, input_a x)
Ha: finite_valid_plan_from s a
finite_valid_trace_from X sa
  (let (final, items) :=
     match x with
     | {| label_a := l'; input_a := input' |} =>
         let (dest, out) :=
           transition l' (sa, input') in
         (dest,
          [{|
             l := l';
             input := input';
             destination := dest;
             output := out
           |}])
     end in
   (rev items, final)).1
      destruct x.message: Type
X: VLSM message
s: state X
label_a0: label X
input_a0: option message
a: list plan_item
IHa: finite_valid_plan_from s a
↔ valid_state_prop X s
  ∧ Forall
      (λ ai : plan_item,
         option_valid_message_prop X
           (input_a ai)) a
    ∧ (∀ (prefa suffa : plan) (ai : plan_item),
         a = prefa ++ [ai] ++ suffa
         → let lst := (apply_plan s prefa).2 in
           valid (label_a ai) (lst, input_a ai))
Hs: valid_state_prop X s
Hinput: Forall
  (λ ai : plan_item,
     option_valid_message_prop X (input_a ai))
  a
Hinput_ai: Forall
  (λ ai : plan_item,
     option_valid_message_prop X
       (input_a ai))
  [{|
     label_a := label_a0;
     input_a := input_a0
   |}]
sa: state X
Heqsa: sa = (apply_plan s a).2
Hvalid: let lst := sa in
valid
  (label_a
     {|
       label_a := label_a0;
       input_a := input_a0
     |})
  (lst,
   input_a
     {|
       label_a := label_a0;
       input_a := input_a0
     |})
Ha: finite_valid_plan_from s a
finite_valid_trace_from X sa
  (let (final, items) :=
     let (dest, out) :=
       transition label_a0 (sa, input_a0) in
     (dest,
      [{|
         l := label_a0;
         input := input_a0;
         destination := dest;
         output := out
       |}]) in
   (rev items, final)).1
      destruct (transition X label_a0 (sa, input_a0)) as (dest, out) eqn: Ht.message: Type
X: VLSM message
s: state X
label_a0: label X
input_a0: option message
a: list plan_item
IHa: finite_valid_plan_from s a
↔ valid_state_prop X s
  ∧ Forall
      (λ ai : plan_item,
         option_valid_message_prop X
           (input_a ai)) a
    ∧ (∀ (prefa suffa : plan) (ai : plan_item),
         a = prefa ++ [ai] ++ suffa
         → let lst := (apply_plan s prefa).2 in
           valid (label_a ai) (lst, input_a ai))
Hs: valid_state_prop X s
Hinput: Forall
  (λ ai : plan_item,
     option_valid_message_prop X (input_a ai))
  a
Hinput_ai: Forall
  (λ ai : plan_item,
     option_valid_message_prop X
       (input_a ai))
  [{|
     label_a := label_a0;
     input_a := input_a0
   |}]
sa: state X
Heqsa: sa = (apply_plan s a).2
Hvalid: let lst := sa in
valid
  (label_a
     {|
       label_a := label_a0;
       input_a := input_a0
     |})
  (lst,
   input_a
     {|
       label_a := label_a0;
       input_a := input_a0
     |})
Ha: finite_valid_plan_from s a
dest: state X
out: option message
Ht: transition label_a0 (sa, input_a0) = (dest, out)
finite_valid_trace_from X sa
  (rev
     [{|
        l := label_a0;
        input := input_a0;
        destination := dest;
        output := out
      |}], dest).1
      simpl.message: Type
X: VLSM message
s: state X
label_a0: label X
input_a0: option message
a: list plan_item
IHa: finite_valid_plan_from s a
↔ valid_state_prop X s
  ∧ Forall
      (λ ai : plan_item,
         option_valid_message_prop X
           (input_a ai)) a
    ∧ (∀ (prefa suffa : plan) (ai : plan_item),
         a = prefa ++ [ai] ++ suffa
         → let lst := (apply_plan s prefa).2 in
           valid (label_a ai) (lst, input_a ai))
Hs: valid_state_prop X s
Hinput: Forall
  (λ ai : plan_item,
     option_valid_message_prop X (input_a ai))
  a
Hinput_ai: Forall
  (λ ai : plan_item,
     option_valid_message_prop X
       (input_a ai))
  [{|
     label_a := label_a0;
     input_a := input_a0
   |}]
sa: state X
Heqsa: sa = (apply_plan s a).2
Hvalid: let lst := sa in
valid
  (label_a
     {|
       label_a := label_a0;
       input_a := input_a0
     |})
  (lst,
   input_a
     {|
       label_a := label_a0;
       input_a := input_a0
     |})
Ha: finite_valid_plan_from s a
dest: state X
out: option message
Ht: transition label_a0 (sa, input_a0) = (dest, out)
finite_valid_trace_from X sa
  [{|
     l := label_a0;
     input := input_a0;
     destination := dest;
     output := out
   |}]
      apply Forall_inv in Hinput_ai.message: Type
X: VLSM message
s: state X
label_a0: label X
input_a0: option message
a: list plan_item
IHa: finite_valid_plan_from s a
↔ valid_state_prop X s
  ∧ Forall
      (λ ai : plan_item,
         option_valid_message_prop X
           (input_a ai)) a
    ∧ (∀ (prefa suffa : plan) (ai : plan_item),
         a = prefa ++ [ai] ++ suffa
         → let lst := (apply_plan s prefa).2 in
           valid (label_a ai) (lst, input_a ai))
Hs: valid_state_prop X s
Hinput: Forall
  (λ ai : plan_item,
     option_valid_message_prop X (input_a ai))
  a
Hinput_ai: option_valid_message_prop X
  (input_a
     {|
       label_a := label_a0;
       input_a := input_a0
     |})
sa: state X
Heqsa: sa = (apply_plan s a).2
Hvalid: let lst := sa in
valid
  (label_a
     {|
       label_a := label_a0;
       input_a := input_a0
     |})
  (lst,
   input_a
     {|
       label_a := label_a0;
       input_a := input_a0
     |})
Ha: finite_valid_plan_from s a
dest: state X
out: option message
Ht: transition label_a0 (sa, input_a0) = (dest, out)
finite_valid_trace_from X sa
  [{|
     l := label_a0;
     input := input_a0;
     destination := dest;
     output := out
   |}] simpl in Hinput_ai.message: Type
X: VLSM message
s: state X
label_a0: label X
input_a0: option message
a: list plan_item
IHa: finite_valid_plan_from s a
↔ valid_state_prop X s
  ∧ Forall
      (λ ai : plan_item,
         option_valid_message_prop X
           (input_a ai)) a
    ∧ (∀ (prefa suffa : plan) (ai : plan_item),
         a = prefa ++ [ai] ++ suffa
         → let lst := (apply_plan s prefa).2 in
           valid (label_a ai) (lst, input_a ai))
Hs: valid_state_prop X s
Hinput: Forall
  (λ ai : plan_item,
     option_valid_message_prop X (input_a ai))
  a
Hinput_ai: option_valid_message_prop X input_a0
sa: state X
Heqsa: sa = (apply_plan s a).2
Hvalid: let lst := sa in
valid
  (label_a
     {|
       label_a := label_a0;
       input_a := input_a0
     |})
  (lst,
   input_a
     {|
       label_a := label_a0;
       input_a := input_a0
     |})
Ha: finite_valid_plan_from s a
dest: state X
out: option message
Ht: transition label_a0 (sa, input_a0) = (dest, out)
finite_valid_trace_from X sa
  [{|
     l := label_a0;
     input := input_a0;
     destination := dest;
     output := out
   |}]
      unfold finite_valid_plan_from in Ha.message: Type
X: VLSM message
s: state X
label_a0: label X
input_a0: option message
a: list plan_item
IHa: finite_valid_plan_from s a
↔ valid_state_prop X s
  ∧ Forall
      (λ ai : plan_item,
         option_valid_message_prop X
           (input_a ai)) a
    ∧ (∀ (prefa suffa : plan) (ai : plan_item),
         a = prefa ++ [ai] ++ suffa
         → let lst := (apply_plan s prefa).2 in
           valid (label_a ai) (lst, input_a ai))
Hs: valid_state_prop X s
Hinput: Forall
  (λ ai : plan_item,
     option_valid_message_prop X (input_a ai))
  a
Hinput_ai: option_valid_message_prop X input_a0
sa: state X
Heqsa: sa = (apply_plan s a).2
Hvalid: let lst := sa in
valid
  (label_a
     {|
       label_a := label_a0;
       input_a := input_a0
     |})
  (lst,
   input_a
     {|
       label_a := label_a0;
       input_a := input_a0
     |})
Ha: finite_valid_trace_from X s (apply_plan s a).1
dest: state X
out: option message
Ht: transition label_a0 (sa, input_a0) = (dest, out)
finite_valid_trace_from X sa
  [{|
     l := label_a0;
     input := input_a0;
     destination := dest;
     output := out
   |}]
      apply finite_valid_trace_last_pstate in Ha.message: Type
X: VLSM message
s: state X
label_a0: label X
input_a0: option message
a: list plan_item
IHa: finite_valid_plan_from s a
↔ valid_state_prop X s
  ∧ Forall
      (λ ai : plan_item,
         option_valid_message_prop X
           (input_a ai)) a
    ∧ (∀ (prefa suffa : plan) (ai : plan_item),
         a = prefa ++ [ai] ++ suffa
         → let lst := (apply_plan s prefa).2 in
           valid (label_a ai) (lst, input_a ai))
Hs: valid_state_prop X s
Hinput: Forall
  (λ ai : plan_item,
     option_valid_message_prop X (input_a ai))
  a
Hinput_ai: option_valid_message_prop X input_a0
sa: state X
Heqsa: sa = (apply_plan s a).2
Hvalid: let lst := sa in
valid
  (label_a
     {|
       label_a := label_a0;
       input_a := input_a0
     |})
  (lst,
   input_a
     {|
       label_a := label_a0;
       input_a := input_a0
     |})
Ha: valid_state_prop X
  (finite_trace_last s (apply_plan s a).1)
dest: state X
out: option message
Ht: transition label_a0 (sa, input_a0) = (dest, out)
finite_valid_trace_from X sa
  [{|
     l := label_a0;
     input := input_a0;
     destination := dest;
     output := out
   |}]
      specialize (apply_plan_last s a) as Hlst.message: Type
X: VLSM message
s: state X
label_a0: label X
input_a0: option message
a: list plan_item
IHa: finite_valid_plan_from s a
↔ valid_state_prop X s
  ∧ Forall
      (λ ai : plan_item,
         option_valid_message_prop X
           (input_a ai)) a
    ∧ (∀ (prefa suffa : plan) (ai : plan_item),
         a = prefa ++ [ai] ++ suffa
         → let lst := (apply_plan s prefa).2 in
           valid (label_a ai) (lst, input_a ai))
Hs: valid_state_prop X s
Hinput: Forall
  (λ ai : plan_item,
     option_valid_message_prop X (input_a ai))
  a
Hinput_ai: option_valid_message_prop X input_a0
sa: state X
Heqsa: sa = (apply_plan s a).2
Hvalid: let lst := sa in
valid
  (label_a
     {|
       label_a := label_a0;
       input_a := input_a0
     |})
  (lst,
   input_a
     {|
       label_a := label_a0;
       input_a := input_a0
     |})
Ha: valid_state_prop X
  (finite_trace_last s (apply_plan s a).1)
dest: state X
out: option message
Ht: transition label_a0 (sa, input_a0) = (dest, out)
Hlst: let after_a := apply_plan s a in
finite_trace_last s after_a.1 = after_a.2
finite_valid_trace_from X sa
  [{|
     l := label_a0;
     input := input_a0;
     destination := dest;
     output := out
   |}]
      simpl in Hlst, Ha.message: Type
X: VLSM message
s: state X
label_a0: label X
input_a0: option message
a: list plan_item
IHa: finite_valid_plan_from s a
↔ valid_state_prop X s
  ∧ Forall
      (λ ai : plan_item,
         option_valid_message_prop X
           (input_a ai)) a
    ∧ (∀ (prefa suffa : plan) (ai : plan_item),
         a = prefa ++ [ai] ++ suffa
         → let lst := (apply_plan s prefa).2 in
           valid (label_a ai) (lst, input_a ai))
Hs: valid_state_prop X s
Hinput: Forall
  (λ ai : plan_item,
     option_valid_message_prop X (input_a ai))
  a
Hinput_ai: option_valid_message_prop X input_a0
sa: state X
Heqsa: sa = (apply_plan s a).2
Hvalid: let lst := sa in
valid
  (label_a
     {|
       label_a := label_a0;
       input_a := input_a0
     |})
  (lst,
   input_a
     {|
       label_a := label_a0;
       input_a := input_a0
     |})
Ha: valid_state_prop X
  (finite_trace_last s (apply_plan s a).1)
dest: state X
out: option message
Ht: transition label_a0 (sa, input_a0) = (dest, out)
Hlst: finite_trace_last s (apply_plan s a).1 =
(apply_plan s a).2
finite_valid_trace_from X sa
  [{|
     l := label_a0;
     input := input_a0;
     destination := dest;
     output := out
   |}]
      setoid_rewrite Hlst in Ha.message: Type
X: VLSM message
s: state X
label_a0: label X
input_a0: option message
a: list plan_item
IHa: finite_valid_plan_from s a
↔ valid_state_prop X s
  ∧ Forall
      (λ ai : plan_item,
         option_valid_message_prop X
           (input_a ai)) a
    ∧ (∀ (prefa suffa : plan) (ai : plan_item),
         a = prefa ++ [ai] ++ suffa
         → let lst := (apply_plan s prefa).2 in
           valid (label_a ai) (lst, input_a ai))
Hs: valid_state_prop X s
Hinput: Forall
  (λ ai : plan_item,
     option_valid_message_prop X (input_a ai))
  a
Hinput_ai: option_valid_message_prop X input_a0
sa: state X
Heqsa: sa = (apply_plan s a).2
Hvalid: let lst := sa in
valid
  (label_a
     {|
       label_a := label_a0;
       input_a := input_a0
     |})
  (lst,
   input_a
     {|
       label_a := label_a0;
       input_a := input_a0
     |})
Ha: valid_state_prop X (apply_plan s a).2
dest: state X
out: option message
Ht: transition label_a0 (sa, input_a0) = (dest, out)
Hlst: finite_trace_last s (apply_plan s a).1 =
(apply_plan s a).2
finite_valid_trace_from X sa
  [{|
     l := label_a0;
     input := input_a0;
     destination := dest;
     output := out
   |}] setoid_rewrite <- Heqsa in Ha.message: Type
X: VLSM message
s: state X
label_a0: label X
input_a0: option message
a: list plan_item
IHa: finite_valid_plan_from s a
↔ valid_state_prop X s
  ∧ Forall
      (λ ai : plan_item,
         option_valid_message_prop X
           (input_a ai)) a
    ∧ (∀ (prefa suffa : plan) (ai : plan_item),
         a = prefa ++ [ai] ++ suffa
         → let lst := (apply_plan s prefa).2 in
           valid (label_a ai) (lst, input_a ai))
Hs: valid_state_prop X s
Hinput: Forall
  (λ ai : plan_item,
     option_valid_message_prop X (input_a ai))
  a
Hinput_ai: option_valid_message_prop X input_a0
sa: state X
Heqsa: sa = (apply_plan s a).2
Hvalid: let lst := sa in
valid
  (label_a
     {|
       label_a := label_a0;
       input_a := input_a0
     |})
  (lst,
   input_a
     {|
       label_a := label_a0;
       input_a := input_a0
     |})
Ha: valid_state_prop X sa
dest: state X
out: option message
Ht: transition label_a0 (sa, input_a0) = (dest, out)
Hlst: finite_trace_last s (apply_plan s a).1 =
(apply_plan s a).2
finite_valid_trace_from X sa
  [{|
     l := label_a0;
     input := input_a0;
     destination := dest;
     output := out
   |}]
      repeat constructor; [| done ..].message: Type
X: VLSM message
s: state X
label_a0: label X
input_a0: option message
a: list plan_item
IHa: finite_valid_plan_from s a
↔ valid_state_prop X s
  ∧ Forall
      (λ ai : plan_item,
         option_valid_message_prop X
           (input_a ai)) a
    ∧ (∀ (prefa suffa : plan) (ai : plan_item),
         a = prefa ++ [ai] ++ suffa
         → let lst := (apply_plan s prefa).2 in
           valid (label_a ai) (lst, input_a ai))
Hs: valid_state_prop X s
Hinput: Forall
  (λ ai : plan_item,
     option_valid_message_prop X (input_a ai))
  a
Hinput_ai: option_valid_message_prop X input_a0
sa: state X
Heqsa: sa = (apply_plan s a).2
Hvalid: let lst := sa in
valid
  (label_a
     {|
       label_a := label_a0;
       input_a := input_a0
     |})
  (lst,
   input_a
     {|
       label_a := label_a0;
       input_a := input_a0
     |})
Ha: valid_state_prop X sa
dest: state X
out: option message
Ht: transition label_a0 (sa, input_a0) = (dest, out)
Hlst: finite_trace_last s (apply_plan s a).1 =
(apply_plan s a).2
valid_state_prop X dest
      exists out.message: Type
X: VLSM message
s: state X
label_a0: label X
input_a0: option message
a: list plan_item
IHa: finite_valid_plan_from s a
↔ valid_state_prop X s
  ∧ Forall
      (λ ai : plan_item,
         option_valid_message_prop X
           (input_a ai)) a
    ∧ (∀ (prefa suffa : plan) (ai : plan_item),
         a = prefa ++ [ai] ++ suffa
         → let lst := (apply_plan s prefa).2 in
           valid (label_a ai) (lst, input_a ai))
Hs: valid_state_prop X s
Hinput: Forall
  (λ ai : plan_item,
     option_valid_message_prop X (input_a ai))
  a
Hinput_ai: option_valid_message_prop X input_a0
sa: state X
Heqsa: sa = (apply_plan s a).2
Hvalid: let lst := sa in
valid
  (label_a
     {|
       label_a := label_a0;
       input_a := input_a0
     |})
  (lst,
   input_a
     {|
       label_a := label_a0;
       input_a := input_a0
     |})
Ha: valid_state_prop X sa
dest: state X
out: option message
Ht: transition label_a0 (sa, input_a0) = (dest, out)
Hlst: finite_trace_last s (apply_plan s a).1 =
(apply_plan s a).2
valid_state_message_prop X dest out
      destruct Ha as [_oma Hsa].message: Type
X: VLSM message
s: state X
label_a0: label X
input_a0: option message
a: list plan_item
IHa: finite_valid_plan_from s a
↔ valid_state_prop X s
  ∧ Forall
      (λ ai : plan_item,
         option_valid_message_prop X
           (input_a ai)) a
    ∧ (∀ (prefa suffa : plan) (ai : plan_item),
         a = prefa ++ [ai] ++ suffa
         → let lst := (apply_plan s prefa).2 in
           valid (label_a ai) (lst, input_a ai))
Hs: valid_state_prop X s
Hinput: Forall
  (λ ai : plan_item,
     option_valid_message_prop X (input_a ai))
  a
Hinput_ai: option_valid_message_prop X input_a0
sa: state X
Heqsa: sa = (apply_plan s a).2
Hvalid: let lst := sa in
valid
  (label_a
     {|
       label_a := label_a0;
       input_a := input_a0
     |})
  (lst,
   input_a
     {|
       label_a := label_a0;
       input_a := input_a0
     |})
_oma: option message
Hsa: valid_state_message_prop X sa _oma
dest: state X
out: option message
Ht: transition label_a0 (sa, input_a0) = (dest, out)
Hlst: finite_trace_last s (apply_plan s a).1 =
(apply_plan s a).2
valid_state_message_prop X dest out
      destruct Hinput_ai as [_s Hinput_a0].message: Type
X: VLSM message
s: state X
label_a0: label X
input_a0: option message
a: list plan_item
IHa: finite_valid_plan_from s a
↔ valid_state_prop X s
  ∧ Forall
      (λ ai : plan_item,
         option_valid_message_prop X
           (input_a ai)) a
    ∧ (∀ (prefa suffa : plan) (ai : plan_item),
         a = prefa ++ [ai] ++ suffa
         → let lst := (apply_plan s prefa).2 in
           valid (label_a ai) (lst, input_a ai))
Hs: valid_state_prop X s
Hinput: Forall
  (λ ai : plan_item,
     option_valid_message_prop X (input_a ai))
  a
_s: state X
Hinput_a0: valid_state_message_prop X _s input_a0
sa: state X
Heqsa: sa = (apply_plan s a).2
Hvalid: let lst := sa in
valid
  (label_a
     {|
       label_a := label_a0;
       input_a := input_a0
     |})
  (lst,
   input_a
     {|
       label_a := label_a0;
       input_a := input_a0
     |})
_oma: option message
Hsa: valid_state_message_prop X sa _oma
dest: state X
out: option message
Ht: transition label_a0 (sa, input_a0) = (dest, out)
Hlst: finite_trace_last s (apply_plan s a).1 =
(apply_plan s a).2
valid_state_message_prop X dest out
      by apply valid_generated_state_message with sa _oma _s input_a0 label_a0.
Qed.

Characterizing a singleton valid plan as a input valid transition.

Lemma finite_valid_plan_from_one
  (s : state X)
  (a : plan_item) :
  let res := transition X (label_a a) (s, input_a a) in
  finite_valid_plan_from s [a] <-> input_valid_transition X (label_a a) (s, input_a a) res.message: Type
X: VLSM message
s: state X
a: plan_item
let res := transition (label_a a) (s, input_a a) in
finite_valid_plan_from s [a]
↔ input_valid_transition X (label_a a) (s, input_a a)
    res
Proof.message: Type
X: VLSM message
s: state X
a: plan_item
let res := transition (label_a a) (s, input_a a) in
finite_valid_plan_from s [a]
↔ input_valid_transition X (label_a a) (s, input_a a)
    res
  split;
  intros;
  destruct a;
  unfold apply_plan, _apply_plan in *; simpl in *;
  unfold finite_valid_plan_from in *;
  unfold apply_plan, _apply_plan in *; simpl in *.message: Type
X: VLSM message
s: state X
label_a0: label X
input_a0: option message
H: finite_valid_trace_from X s
  (let (final, items) :=
     let (dest, out) :=
       transition label_a0 (s, input_a0) in
     (dest,
      [{|
         l := label_a0;
         input := input_a0;
         destination := dest;
         output := out
       |}]) in
   (rev items, final)).1
input_valid_transition X label_a0 (s, input_a0)
  (transition label_a0 (s, input_a0))
message: Type
X: VLSM message
s: state X
label_a0: label X
input_a0: option message
H: input_valid_transition X label_a0 (
  s, input_a0) (transition label_a0 (s, input_a0))
finite_valid_trace_from X s
  (let (final, items) :=
     let (dest, out) :=
       transition label_a0 (s, input_a0) in
     (dest,
      [{|
         l := label_a0;
         input := input_a0;
         destination := dest;
         output := out
       |}]) in
   (rev items, final)).1
  -message: Type
X: VLSM message
s: state X
label_a0: label X
input_a0: option message
H: finite_valid_trace_from X s
  (let (final, items) :=
     let (dest, out) :=
       transition label_a0 (s, input_a0) in
     (dest,
      [{|
         l := label_a0;
         input := input_a0;
         destination := dest;
         output := out
       |}]) in
   (rev items, final)).1
input_valid_transition X label_a0 (s, input_a0)
  (transition label_a0 (s, input_a0)) destruct (transition label_a0 (s, input_a0)); cbn in H.message: Type
X: VLSM message
s: state X
label_a0: label X
input_a0: option message
s0: state X
o: option message
H: finite_valid_trace_from X s
  [{|
     l := label_a0;
     input := input_a0;
     destination := s0;
     output := o
   |}]
input_valid_transition X label_a0 (s, input_a0)
  (s0, o)
    by inversion H; subst.
  -message: Type
X: VLSM message
s: state X
label_a0: label X
input_a0: option message
H: input_valid_transition X label_a0 (
  s, input_a0) (transition label_a0 (s, input_a0))
finite_valid_trace_from X s
  (let (final, items) :=
     let (dest, out) :=
       transition label_a0 (s, input_a0) in
     (dest,
      [{|
         l := label_a0;
         input := input_a0;
         destination := dest;
         output := out
       |}]) in
   (rev items, final)).1 destruct (transition label_a0 (s, input_a0)); cbn in H |- *.message: Type
X: VLSM message
s: state X
label_a0: label X
input_a0: option message
s0: state X
o: option message
H: input_valid_transition X label_a0 (
  s, input_a0) (s0, o)
finite_valid_trace_from X s
  [{|
     l := label_a0;
     input := input_a0;
     destination := s0;
     output := o
   |}]
    apply finite_valid_trace_from_extend; [| done].message: Type
X: VLSM message
s: state X
label_a0: label X
input_a0: option message
s0: state X
o: option message
H: input_valid_transition X label_a0 (
  s, input_a0) (s0, o)
finite_valid_trace_from X s0 []
    apply finite_valid_trace_from_empty.message: Type
X: VLSM message
s: state X
label_a0: label X
input_a0: option message
s0: state X
o: option message
H: input_valid_transition X label_a0 (
  s, input_a0) (s0, o)
valid_state_prop X s0
    by apply input_valid_transition_destination in H.
Qed.

Definition preserves
  (a : plan)
  (P : state X -> Prop) :
  Prop :=
  forall (s : state X),
  (P s -> valid_state_prop X s -> finite_valid_plan_from s a -> P (snd (apply_plan s a))).

Definition ensures
  (a : plan)
  (P : state X -> Prop) :
  Prop :=
  forall (s : state X),
  (valid_state_prop X s -> P s -> finite_valid_plan_from s a).

(*
  If some property of a state guarantees a plan `b` applied to the state is valid,
  and this property is preserved by the application of some other plan `a`,
  then these two plans can be composed and the application of `a ++ b` will also
  be valid.
*)

Lemma plan_independence
  (a b : plan)
  (Pb : state X -> Prop)
  (s : state X)
  (Hpr : valid_state_prop X s)
  (Ha : finite_valid_plan_from s a)
  (Hhave : Pb s)
  (Hensures : ensures b Pb)
  (Hpreserves : preserves a Pb) :
    finite_valid_plan_from s (a ++ b).message: Type
X: VLSM message
a, b: plan
Pb: state X → Prop
s: state X
Hpr: valid_state_prop X s
Ha: finite_valid_plan_from s a
Hhave: Pb s
Hensures: ensures b Pb
Hpreserves: preserves a Pb
finite_valid_plan_from s (a ++ b)
Proof.message: Type
X: VLSM message
a, b: plan
Pb: state X → Prop
s: state X
Hpr: valid_state_prop X s
Ha: finite_valid_plan_from s a
Hhave: Pb s
Hensures: ensures b Pb
Hpreserves: preserves a Pb
finite_valid_plan_from s (a ++ b)
  unfold ensures, preserves in *.message: Type
X: VLSM message
a, b: plan
Pb: state X → Prop
s: state X
Hpr: valid_state_prop X s
Ha: finite_valid_plan_from s a
Hhave: Pb s
Hensures: ∀ s : state X,
  valid_state_prop X s
  → Pb s → finite_valid_plan_from s b
Hpreserves: ∀ s : state X,
  Pb s
  → valid_state_prop X s
    → finite_valid_plan_from s a
      → Pb (apply_plan s a).2
finite_valid_plan_from s (a ++ b)
  apply finite_valid_plan_from_app_iff.message: Type
X: VLSM message
a, b: plan
Pb: state X → Prop
s: state X
Hpr: valid_state_prop X s
Ha: finite_valid_plan_from s a
Hhave: Pb s
Hensures: ∀ s : state X,
  valid_state_prop X s
  → Pb s → finite_valid_plan_from s b
Hpreserves: ∀ s : state X,
  Pb s
  → valid_state_prop X s
    → finite_valid_plan_from s a
      → Pb (apply_plan s a).2
finite_valid_plan_from s a
∧ finite_valid_plan_from (apply_plan s a).2 b
  split; [done |].message: Type
X: VLSM message
a, b: plan
Pb: state X → Prop
s: state X
Hpr: valid_state_prop X s
Ha: finite_valid_plan_from s a
Hhave: Pb s
Hensures: ∀ s : state X,
  valid_state_prop X s
  → Pb s → finite_valid_plan_from s b
Hpreserves: ∀ s : state X,
  Pb s
  → valid_state_prop X s
    → finite_valid_plan_from s a
      → Pb (apply_plan s a).2
finite_valid_plan_from (apply_plan s a).2 b
  remember (snd (apply_plan s a)) as s'.message: Type
X: VLSM message
a, b: plan
Pb: state X → Prop
s: state X
Hpr: valid_state_prop X s
Ha: finite_valid_plan_from s a
Hhave: Pb s
Hensures: ∀ s : state X,
  valid_state_prop X s
  → Pb s → finite_valid_plan_from s b
Hpreserves: ∀ s : state X,
  Pb s
  → valid_state_prop X s
    → finite_valid_plan_from s a
      → Pb (apply_plan s a).2
s': state X
Heqs': s' = (apply_plan s a).2
finite_valid_plan_from s' b
  rewrite Heqs'.message: Type
X: VLSM message
a, b: plan
Pb: state X → Prop
s: state X
Hpr: valid_state_prop X s
Ha: finite_valid_plan_from s a
Hhave: Pb s
Hensures: ∀ s : state X,
  valid_state_prop X s
  → Pb s → finite_valid_plan_from s b
Hpreserves: ∀ s : state X,
  Pb s
  → valid_state_prop X s
    → finite_valid_plan_from s a
      → Pb (apply_plan s a).2
s': state X
Heqs': s' = (apply_plan s a).2
finite_valid_plan_from (apply_plan s a).2 b apply Hensures.message: Type
X: VLSM message
a, b: plan
Pb: state X → Prop
s: state X
Hpr: valid_state_prop X s
Ha: finite_valid_plan_from s a
Hhave: Pb s
Hensures: ∀ s : state X,
  valid_state_prop X s
  → Pb s → finite_valid_plan_from s b
Hpreserves: ∀ s : state X,
  Pb s
  → valid_state_prop X s
    → finite_valid_plan_from s a
      → Pb (apply_plan s a).2
s': state X
Heqs': s' = (apply_plan s a).2
valid_state_prop X (apply_plan s a).2
message: Type
X: VLSM message
a, b: plan
Pb: state X → Prop
s: state X
Hpr: valid_state_prop X s
Ha: finite_valid_plan_from s a
Hhave: Pb s
Hensures: ∀ s : state X,
  valid_state_prop X s
  → Pb s → finite_valid_plan_from s b
Hpreserves: ∀ s : state X,
  Pb s
  → valid_state_prop X s
    → finite_valid_plan_from s a
      → Pb (apply_plan s a).2
s': state X
Heqs': s' = (apply_plan s a).2
Pb (apply_plan s a).2
  -message: Type
X: VLSM message
a, b: plan
Pb: state X → Prop
s: state X
Hpr: valid_state_prop X s
Ha: finite_valid_plan_from s a
Hhave: Pb s
Hensures: ∀ s : state X,
  valid_state_prop X s
  → Pb s → finite_valid_plan_from s b
Hpreserves: ∀ s : state X,
  Pb s
  → valid_state_prop X s
    → finite_valid_plan_from s a
      → Pb (apply_plan s a).2
s': state X
Heqs': s' = (apply_plan s a).2
valid_state_prop X (apply_plan s a).2 by apply apply_plan_last_valid.
  -message: Type
X: VLSM message
a, b: plan
Pb: state X → Prop
s: state X
Hpr: valid_state_prop X s
Ha: finite_valid_plan_from s a
Hhave: Pb s
Hensures: ∀ s : state X,
  valid_state_prop X s
  → Pb s → finite_valid_plan_from s b
Hpreserves: ∀ s : state X,
  Pb s
  → valid_state_prop X s
    → finite_valid_plan_from s a
      → Pb (apply_plan s a).2
s': state X
Heqs': s' = (apply_plan s a).2
Pb (apply_plan s a).2 by apply Hpreserves.
Qed.

End sec_valid_plans.