From Coq Require Import FunctionalExtensionality.
From stdpp Require Import prelude.[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]
From VLSM.Lib Require Import ListExtras.[Loading ML file coq-itauto.plugin ... done]
From VLSM.Core Require Import VLSM Composition ProjectionTraces.

Tutorial: VLSMs that Generate Logical Formulas

This module shows how VLSMs can be used to generate propositional logic formulas. To achieve this, we define a family of VLSMs, one for each formula grammar rule, which generates messages according to the given rule. By composition, we obtain that the valid messages are precisely the "strings" which can be produced by the formula grammar.

To strengthen the connection between formulas and VLSMs, we also define formulas as an inductive type and prove an equivalence between the inductively defined formulas and those obtained as valid messages of the composition of VLSMs from above.

To simplify the presentation, the grammar we consider for formulas is unambiguous and uses prefix notation:

f ::= ⊤ | ⊥ | x | ¬ f | ∧ f f | ∨ f f | → f f | ↔ f f

Section sec_formula.

Context
  `{EqDecision Var}
  `{base.Infinite Var}
  .

Inductive symbol : Type :=
| Top
| Bot
| PVar (x : Var)
| Neg
| Conj
| Disj
| Impl
| Iff.

#[export] Instance symbol_dec : EqDecision symbol.Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
EqDecision symbol
Proof.Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
EqDecision symbol
  unfold EqDecision, Decision; decide equality.Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
x, y: symbol
x0, x1: Var
{x0 = x1} + {x0 ≠ x1}
  by destruct (decide (x0 = x1)); [left | right].
Qed.

Definition expression : Type := list symbol.

Inductive Formula : Type :=
| FTop
| FBot
| FVar (x : Var)
| FNeg (f : Formula)
| FConj (f1 f2 : Formula)
| FDisj (f1 f2 : Formula)
| FImpl (f1 f2 : Formula)
| FIff (f1 f2 : Formula).

We introduce the following notations to allow us to more easily write formulas.

#[local] Notation "⊤" := FTop.
#[local] Notation "⊥" := FBot.
#[local] Notation "x ∨ y" := (FDisj x y) (at level 85, right associativity).
#[local] Notation "x ∧ y" := (FConj x y) (at level 80, right associativity).
#[local] Notation "x → y" := (FImpl x y) (at level 99, y at level 200, right associativity).
#[local] Notation "x ↔ y" := (FIff x y) (at level 95, no associativity).
#[local] Notation "¬ x" := (FNeg x) (at level 75, right associativity).

Similarly to the notations above, the purpose of this coercion is to allow using variables directly as formulas.

Coercion FVar : Var >-> Formula.

A Formula is flattened to an expression using prefix notation.

Fixpoint flatten_formula (f : Formula) : expression :=
  match f with
  | FTop => [Top]
  | FBot => [Bot]
  | FVar x => [PVar x]
  | ¬ f => Neg :: flatten_formula f
  | f1 ∧ f2 => Conj :: flatten_formula f1 ++ flatten_formula f2
  | f1 ∨ f2 => Disj :: flatten_formula f1 ++ flatten_formula f2
  | f1 → f2 => Impl :: flatten_formula f1 ++ flatten_formula f2
  | f1 ↔ f2 => Iff :: flatten_formula f1 ++ flatten_formula f2
  end.

Lemma flatten_formula_nzlen :
  forall (f : Formula),
    length (flatten_formula f) > 0.Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
∀ f : Formula, length (flatten_formula f) > 0
Proof.Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
∀ f : Formula, length (flatten_formula f) > 0 by intros []; cbn; lia. Qed.

Encoding formulas as VLSMs

VLSM for top and bottom rules

This is a very simple VLSM, with a single state and a single label, accepting no input and outputing the expression containing just the symbol parameter.

Section sec_expression_const_vlsm.

Context
  (ct : symbol)
  .

Definition expression_const_vlsm_type : VLSMType expression :=
{|
  state := unit;
  label := unit;
|}.

Definition expression_const_vlsm_machine : VLSMMachine expression_const_vlsm_type :=
{|
  initial_state_prop := const True;
  s0 := populate (exist _ () I);
  initial_message_prop := const False;
  transition := fun _ _ => ((), Some [ct]);
  valid := fun _ som => som.2 = None;
|}.

Definition expression_const_vlsm : VLSM expression :=
  mk_vlsm expression_const_vlsm_machine.

End sec_expression_const_vlsm.

VLSM for the variable rule

This VLSM has a single state and its labels are the variables. Its behavior is to accept no input and to output the expression containing just the variable specified by the label of the transition.

Section sec_expression_var_vlsm.

Definition expression_var_vlsm_type : VLSMType expression :=
{|
  state := unit;
  label := Var;
|}.

Definition expression_var_vlsm_machine : VLSMMachine expression_var_vlsm_type :=
{|
  initial_state_prop := const True;
  s0 := populate (exist _ () I);
  initial_message_prop := const False;
  transition := fun l _ => ((), Some [PVar l]);
  valid := fun _ som => som.2 = None;
|}.

Definition expression_var_vlsm : VLSM expression :=
  mk_vlsm expression_var_vlsm_machine.

End sec_expression_var_vlsm.

VLSM for the negation rule

This VLSM has a single state and a single label, accepts as input an expression and outputs the expression obtained by prefixing the input with the negation symbol.

Section sec_expression_neg_vlsm.

Definition expression_neg_vlsm_type : VLSMType expression :=
{|
  state := unit;
  label := unit;
|}.

Definition expression_neg_vlsm_transition (_ : unit)
  (som : unit * option expression) : unit * option expression :=
  match som.2 with
  | None => som
  | Some m => ((), Some (Neg :: m))
  end.

Definition expression_neg_vlsm_machine : VLSMMachine expression_neg_vlsm_type :=
{|
  initial_state_prop := const True;
  s0 := populate (exist _ () I);
  initial_message_prop := const False;
  transition := expression_neg_vlsm_transition;
  valid := fun _ som => is_Some som.2;
|}.

Definition expression_neg_vlsm : VLSM expression :=
  mk_vlsm expression_neg_vlsm_machine.

End sec_expression_neg_vlsm.

VLSM for binary connective rules

This VLSM has a single label and its states are option expression with None being the initial state. From the initial state it accepts as input an expression and transitions to the state holding that expression. From a state holding an expression it accepts as input an expression and outputs the connective symbol (parameter) followed by the concatenation of the expression in the state and that in the input.

Section sec_expression_binop_vlsm.

Context
  (binop : symbol)
  .

Definition expression_binop_vlsm_type : VLSMType expression :=
{|
  state := option expression;
  label := unit;
|}.

Definition expression_binop_vlsm_transition (_ : unit)
  (som : option expression * option expression) :
  option expression * option expression :=
  match som with
  | (_, None) => som
  | (None, Some f) => (Some f, None)
  | (Some f1, Some f2) => (None, Some (binop :: f1 ++ f2))
  end.

Definition expression_binop_vlsm_machine : VLSMMachine expression_binop_vlsm_type :=
{|
  initial_state_prop := fun o => o = None;
  s0 := populate (exist _ None eq_refl);
  initial_message_prop := const False;
  transition := expression_binop_vlsm_transition;
  valid := fun _ som => is_Some som.2;
|}.

Definition expression_binop_vlsm : VLSM expression :=
  mk_vlsm expression_binop_vlsm_machine.

End sec_expression_binop_vlsm.

VLSM for expressions

Section sec_expression_vlsm.

Inductive index :=
| ITop
| IBot
| IVar
| INeg
| IConj
| IDisj
| IImpl
| IIff.

#[export] Instance index_dec : EqDecision index.Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
EqDecision index
Proof.Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
EqDecision index by intros ? ?; unfold Decision; decide equality. Qed.

Definition symbol_to_index (s : symbol) : index :=
  match s with
  | Top => ITop
  | Bot => IBot
  | PVar _ => IVar
  | Neg => INeg
  | Conj => IConj
  | Disj => IDisj
  | Impl => IImpl
  | Iff => IIff
  end.

Definition expression_components (i : index) : VLSM expression :=
  match i with
  | ITop => expression_const_vlsm Top
  | IBot => expression_const_vlsm Bot
  | IVar => expression_var_vlsm
  | INeg => expression_neg_vlsm
  | IConj => expression_binop_vlsm Conj
  | IDisj => expression_binop_vlsm Disj
  | IImpl => expression_binop_vlsm Impl
  | IIff => expression_binop_vlsm Iff
  end.

Definition default_label (i : index) : label (expression_components i) :=
  match i with
  | IVar => fresh []
  | _ => ()
  end.

Definition default_composite_label
  (i : index) : composite_label expression_components :=
    existT i (default_label i).

Definition expression_vlsm : VLSM expression :=
  free_composite_vlsm expression_components.

End sec_expression_vlsm.

Characterization of valid messages as formulas

Section sec_valid_message_char.

Definition well_formed_expression : expression -> Prop :=
  valid_message_prop expression_vlsm.

We will show below (lemma flatten_formula_prefix) that no (strict) prefix of a flattened formula can be the flattening of another formula, which is a key result for establishing the injectivity of the flatten_formula function.

To reach this result, we first define this property and prove several results about formulas satisfying it.

Definition formula_prefix_is_not_formula_prop (f1 : Formula) : Prop :=
  forall (s : expression), strict prefix s (flatten_formula f1) ->
  forall (f2 : Formula), flatten_formula f2 <> s.

Lemma flatten_formula_formula_prefix_is_not_formula_prop_app :
  forall (fa : Formula), formula_prefix_is_not_formula_prop fa ->
  forall (fb : Formula), formula_prefix_is_not_formula_prop fb ->
  forall (sufa sufb : expression),
    flatten_formula fa ++ sufa = flatten_formula fb ++ sufb ->
    flatten_formula fa = flatten_formula fb /\ sufa = sufb.Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
∀ fa : Formula,
  formula_prefix_is_not_formula_prop fa
  → ∀ fb : Formula,
      formula_prefix_is_not_formula_prop fb
      → ∀ sufa sufb : expression,
          flatten_formula fa ++ sufa =
          flatten_formula fb ++ sufb
          → flatten_formula fa = flatten_formula fb
            ∧ sufa = sufb
Proof.Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
∀ fa : Formula,
  formula_prefix_is_not_formula_prop fa
  → ∀ fb : Formula,
      formula_prefix_is_not_formula_prop fb
      → ∀ sufa sufb : expression,
          flatten_formula fa ++ sufa =
          flatten_formula fb ++ sufb
          → flatten_formula fa = flatten_formula fb
            ∧ sufa = sufb
  intros fa Hfa fb Hfb sufa sufb Heq.Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
fa: Formula
Hfa: formula_prefix_is_not_formula_prop fa
fb: Formula
Hfb: formula_prefix_is_not_formula_prop fb
sufa, sufb: expression
Heq: flatten_formula fa ++ sufa =
flatten_formula fb ++ sufb
(flatten_formula fa = flatten_formula fb ∧ sufa = sufb)%type
  cut (flatten_formula fa = flatten_formula fb);
    [by inversion 1; simplify_list_eq |].Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
fa: Formula
Hfa: formula_prefix_is_not_formula_prop fa
fb: Formula
Hfb: formula_prefix_is_not_formula_prop fb
sufa, sufb: expression
Heq: flatten_formula fa ++ sufa =
flatten_formula fb ++ sufb
flatten_formula fa = flatten_formula fb
  destruct (decide (prefix (flatten_formula fa) (flatten_formula fb))) as [Hab | Hab],
    (decide (prefix (flatten_formula fb) (flatten_formula fa))) as [Hba | Hba].Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
fa: Formula
Hfa: formula_prefix_is_not_formula_prop fa
fb: Formula
Hfb: formula_prefix_is_not_formula_prop fb
sufa, sufb: expression
Heq: flatten_formula fa ++ sufa =
flatten_formula fb ++ sufb
Hab: flatten_formula fa
`prefix_of` flatten_formula fb
Hba: flatten_formula fb
`prefix_of` flatten_formula fa
flatten_formula fa = flatten_formula fb
Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
fa: Formula
Hfa: formula_prefix_is_not_formula_prop fa
fb: Formula
Hfb: formula_prefix_is_not_formula_prop fb
sufa, sufb: expression
Heq: flatten_formula fa ++ sufa =
flatten_formula fb ++ sufb
Hab: flatten_formula fa
`prefix_of` flatten_formula fb
Hba: (¬ flatten_formula fb
   `prefix_of` flatten_formula fa)%type
flatten_formula fa = flatten_formula fb
Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
fa: Formula
Hfa: formula_prefix_is_not_formula_prop fa
fb: Formula
Hfb: formula_prefix_is_not_formula_prop fb
sufa, sufb: expression
Heq: flatten_formula fa ++ sufa =
flatten_formula fb ++ sufb
Hab: (¬ flatten_formula fa
   `prefix_of` flatten_formula fb)%type
Hba: flatten_formula fb
`prefix_of` flatten_formula fa
flatten_formula fa = flatten_formula fb
Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
fa: Formula
Hfa: formula_prefix_is_not_formula_prop fa
fb: Formula
Hfb: formula_prefix_is_not_formula_prop fb
sufa, sufb: expression
Heq: flatten_formula fa ++ sufa =
flatten_formula fb ++ sufb
Hab: (¬ flatten_formula fa
   `prefix_of` flatten_formula fb)%type
Hba: (¬ flatten_formula fb
   `prefix_of` flatten_formula fa)%type
flatten_formula fa = flatten_formula fb
  -Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
fa: Formula
Hfa: formula_prefix_is_not_formula_prop fa
fb: Formula
Hfb: formula_prefix_is_not_formula_prop fb
sufa, sufb: expression
Heq: flatten_formula fa ++ sufa =
flatten_formula fb ++ sufb
Hab: flatten_formula fa
`prefix_of` flatten_formula fb
Hba: flatten_formula fb
`prefix_of` flatten_formula fa
flatten_formula fa = flatten_formula fb apply prefix_length_eq; [done |].Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
fa: Formula
Hfa: formula_prefix_is_not_formula_prop fa
fb: Formula
Hfb: formula_prefix_is_not_formula_prop fb
sufa, sufb: expression
Heq: flatten_formula fa ++ sufa =
flatten_formula fb ++ sufb
Hab: flatten_formula fa
`prefix_of` flatten_formula fb
Hba: flatten_formula fb
`prefix_of` flatten_formula fa
length (flatten_formula fb)
≤ length (flatten_formula fa)
    by destruct Hba as [suf ->]; rewrite app_length; lia.
  -Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
fa: Formula
Hfa: formula_prefix_is_not_formula_prop fa
fb: Formula
Hfb: formula_prefix_is_not_formula_prop fb
sufa, sufb: expression
Heq: flatten_formula fa ++ sufa =
flatten_formula fb ++ sufb
Hab: flatten_formula fa
`prefix_of` flatten_formula fb
Hba: (¬ flatten_formula fb
   `prefix_of` flatten_formula fa)%type
flatten_formula fa = flatten_formula fb by exfalso; eapply Hfb.
  -Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
fa: Formula
Hfa: formula_prefix_is_not_formula_prop fa
fb: Formula
Hfb: formula_prefix_is_not_formula_prop fb
sufa, sufb: expression
Heq: flatten_formula fa ++ sufa =
flatten_formula fb ++ sufb
Hab: (¬ flatten_formula fa
   `prefix_of` flatten_formula fb)%type
Hba: flatten_formula fb
`prefix_of` flatten_formula fa
flatten_formula fa = flatten_formula fb by exfalso; eapply Hfa.
  -Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
fa: Formula
Hfa: formula_prefix_is_not_formula_prop fa
fb: Formula
Hfb: formula_prefix_is_not_formula_prop fb
sufa, sufb: expression
Heq: flatten_formula fa ++ sufa =
flatten_formula fb ++ sufb
Hab: (¬ flatten_formula fa
   `prefix_of` flatten_formula fb)%type
Hba: (¬ flatten_formula fb
   `prefix_of` flatten_formula fa)%type
flatten_formula fa = flatten_formula fb exfalso; revert sufb Heq.Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
fa: Formula
Hfa: formula_prefix_is_not_formula_prop fa
fb: Formula
Hfb: formula_prefix_is_not_formula_prop fb
sufa: expression
Hab: (¬ flatten_formula fa
   `prefix_of` flatten_formula fb)%type
Hba: (¬ flatten_formula fb
   `prefix_of` flatten_formula fa)%type
∀ sufb : expression,
  flatten_formula fa ++ sufa =
  flatten_formula fb ++ sufb → False
    induction sufa using rev_ind; intros;
      [by simplify_list_eq; contradict Hba; eexists |].Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
fa: Formula
Hfa: formula_prefix_is_not_formula_prop fa
fb: Formula
Hfb: formula_prefix_is_not_formula_prop fb
x: symbol
sufa: list symbol
Hab: (¬ flatten_formula fa
   `prefix_of` flatten_formula fb)%type
Hba: (¬ flatten_formula fb
   `prefix_of` flatten_formula fa)%type
IHsufa: ∀ sufb : expression,
  flatten_formula fa ++ sufa =
  flatten_formula fb ++ sufb → False
sufb: expression
Heq: flatten_formula fa ++ sufa ++ [x] =
flatten_formula fb ++ sufb
False
    destruct_list_last sufb sufb' b Hsufb; simplify_list_eq.Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
fa: Formula
Hfa: formula_prefix_is_not_formula_prop fa
fb: Formula
Hfb: formula_prefix_is_not_formula_prop fb
x: symbol
sufa: list symbol
Hab: (¬ flatten_formula fa
   `prefix_of` flatten_formula fb)%type
Hba: (¬ flatten_formula fb
   `prefix_of` flatten_formula fa)%type
IHsufa: ∀ sufb : expression,
  flatten_formula fa ++ sufa =
  flatten_formula fb ++ sufb → False
Heq: flatten_formula fa ++ sufa ++ [x] =
flatten_formula fb
False
Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
fa: Formula
Hfa: formula_prefix_is_not_formula_prop fa
fb: Formula
Hfb: formula_prefix_is_not_formula_prop fb
sufa: list symbol
Hab: (¬ flatten_formula fa
   `prefix_of` flatten_formula fb)%type
Hba: (¬ flatten_formula fb
   `prefix_of` flatten_formula fa)%type
IHsufa: ∀ sufb : expression,
  flatten_formula fa ++ sufa =
  flatten_formula fb ++ sufb → False
sufb': list symbol
b: symbol
H0: flatten_formula fa ++ sufa =
flatten_formula fb ++ sufb'
False
    +Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
fa: Formula
Hfa: formula_prefix_is_not_formula_prop fa
fb: Formula
Hfb: formula_prefix_is_not_formula_prop fb
x: symbol
sufa: list symbol
Hab: (¬ flatten_formula fa
   `prefix_of` flatten_formula fb)%type
Hba: (¬ flatten_formula fb
   `prefix_of` flatten_formula fa)%type
IHsufa: ∀ sufb : expression,
  flatten_formula fa ++ sufa =
  flatten_formula fb ++ sufb → False
Heq: flatten_formula fa ++ sufa ++ [x] =
flatten_formula fb
False by contradict Hab; eexists.
    +Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
fa: Formula
Hfa: formula_prefix_is_not_formula_prop fa
fb: Formula
Hfb: formula_prefix_is_not_formula_prop fb
sufa: list symbol
Hab: (¬ flatten_formula fa
   `prefix_of` flatten_formula fb)%type
Hba: (¬ flatten_formula fb
   `prefix_of` flatten_formula fa)%type
IHsufa: ∀ sufb : expression,
  flatten_formula fa ++ sufa =
  flatten_formula fb ++ sufb → False
sufb': list symbol
b: symbol
H0: flatten_formula fa ++ sufa =
flatten_formula fb ++ sufb'
False by eapply IHsufa.
Qed.

Lemma flatten_formula_formula_prefix_is_not_formula_prop_app_prefix :
  forall (fa1 : Formula), formula_prefix_is_not_formula_prop fa1 ->
  forall (fa2 : Formula), formula_prefix_is_not_formula_prop fa2 ->
  forall (fb1 : Formula), formula_prefix_is_not_formula_prop fb1 ->
  forall (fb2 : Formula), formula_prefix_is_not_formula_prop fb2 ->
    flatten_formula fb1 ++ flatten_formula fb2 `prefix_of`
      flatten_formula fa1 ++ flatten_formula fa2 ->
    flatten_formula fa1 ++ flatten_formula fa2
      =
    flatten_formula fb1 ++ flatten_formula fb2.Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
∀ fa1 : Formula,
  formula_prefix_is_not_formula_prop fa1
  → ∀ fa2 : Formula,
      formula_prefix_is_not_formula_prop fa2
      → ∀ fb1 : Formula,
          formula_prefix_is_not_formula_prop fb1
          → ∀ fb2 : Formula,
              formula_prefix_is_not_formula_prop fb2
              → flatten_formula fb1 ++
                flatten_formula fb2
                `prefix_of` flatten_formula fa1 ++
                            flatten_formula fa2
                → flatten_formula fa1 ++
                  flatten_formula fa2 =
                  flatten_formula fb1 ++
                  flatten_formula fb2
Proof.Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
∀ fa1 : Formula,
  formula_prefix_is_not_formula_prop fa1
  → ∀ fa2 : Formula,
      formula_prefix_is_not_formula_prop fa2
      → ∀ fb1 : Formula,
          formula_prefix_is_not_formula_prop fb1
          → ∀ fb2 : Formula,
              formula_prefix_is_not_formula_prop fb2
              → flatten_formula fb1 ++
                flatten_formula fb2
                `prefix_of` flatten_formula fa1 ++
                            flatten_formula fa2
                → flatten_formula fa1 ++
                  flatten_formula fa2 =
                  flatten_formula fb1 ++
                  flatten_formula fb2
  intros fa1 Hfa1 fa2 Hfa2 fb1 Hfb1 fb2 Hfb2 [suf Hpre].Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
fa1: Formula
Hfa1: formula_prefix_is_not_formula_prop fa1
fa2: Formula
Hfa2: formula_prefix_is_not_formula_prop fa2
fb1: Formula
Hfb1: formula_prefix_is_not_formula_prop fb1
fb2: Formula
Hfb2: formula_prefix_is_not_formula_prop fb2
suf: list symbol
Hpre: flatten_formula fa1 ++ flatten_formula fa2 =
(flatten_formula fb1 ++ flatten_formula fb2) ++
suf
flatten_formula fa1 ++ flatten_formula fa2 =
flatten_formula fb1 ++ flatten_formula fb2
  rewrite <- app_assoc, <- (app_nil_r (flatten_formula fa2)) in Hpre.Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
fa1: Formula
Hfa1: formula_prefix_is_not_formula_prop fa1
fa2: Formula
Hfa2: formula_prefix_is_not_formula_prop fa2
fb1: Formula
Hfb1: formula_prefix_is_not_formula_prop fb1
fb2: Formula
Hfb2: formula_prefix_is_not_formula_prop fb2
suf: list symbol
Hpre: flatten_formula fa1 ++
flatten_formula fa2 ++ [] =
flatten_formula fb1 ++
flatten_formula fb2 ++ suf
flatten_formula fa1 ++ flatten_formula fa2 =
flatten_formula fb1 ++ flatten_formula fb2
  apply flatten_formula_formula_prefix_is_not_formula_prop_app in Hpre as [-> Hpre]; [| done..].Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
fa1: Formula
Hfa1: formula_prefix_is_not_formula_prop fa1
fa2: Formula
Hfa2: formula_prefix_is_not_formula_prop fa2
fb1: Formula
Hfb1: formula_prefix_is_not_formula_prop fb1
fb2: Formula
Hfb2: formula_prefix_is_not_formula_prop fb2
suf: list symbol
Hpre: flatten_formula fa2 ++ [] =
flatten_formula fb2 ++ suf
flatten_formula fb1 ++ flatten_formula fa2 =
flatten_formula fb1 ++ flatten_formula fb2
  by apply flatten_formula_formula_prefix_is_not_formula_prop_app in Hpre as [-> _].
Qed.

Lemma flatten_formula_prefix_helper
  (f1_1 f1_2 : Formula)
  (IHn : forall (y : nat),
    y < S (length (flatten_formula f1_1 ++ flatten_formula f1_2)) ->
    forall (f1 : Formula), y = length (flatten_formula f1) ->
    formula_prefix_is_not_formula_prop f1)
  (suf : list symbol)
  (f2_1 f2_2 : Formula)
  (Hpre : flatten_formula f1_1 ++ flatten_formula f1_2 =
    flatten_formula f2_1 ++ flatten_formula f2_2 ++ suf)
  (s : symbol) :
    s :: flatten_formula f1_1 ++ flatten_formula f1_2
      `prefix_of`
    s :: flatten_formula f2_1 ++ flatten_formula f2_2.Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
f1_1, f1_2: Formula
IHn: ∀ y : nat,
  y <
  S
    (length
       (flatten_formula f1_1 ++
        flatten_formula f1_2))
  → ∀ f1 : Formula,
      y = length (flatten_formula f1)
      → formula_prefix_is_not_formula_prop f1
suf: list symbol
f2_1, f2_2: Formula
Hpre: flatten_formula f1_1 ++ flatten_formula f1_2 =
flatten_formula f2_1 ++
flatten_formula f2_2 ++ suf
s: symbol
s :: flatten_formula f1_1 ++ flatten_formula f1_2
`prefix_of` s
            :: flatten_formula f2_1 ++
               flatten_formula f2_2
Proof.Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
f1_1, f1_2: Formula
IHn: ∀ y : nat,
  y <
  S
    (length
       (flatten_formula f1_1 ++
        flatten_formula f1_2))
  → ∀ f1 : Formula,
      y = length (flatten_formula f1)
      → formula_prefix_is_not_formula_prop f1
suf: list symbol
f2_1, f2_2: Formula
Hpre: flatten_formula f1_1 ++ flatten_formula f1_2 =
flatten_formula f2_1 ++
flatten_formula f2_2 ++ suf
s: symbol
s :: flatten_formula f1_1 ++ flatten_formula f1_2
`prefix_of` s
            :: flatten_formula f2_1 ++
               flatten_formula f2_2
  rewrite app_assoc in Hpre.Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
f1_1, f1_2: Formula
IHn: ∀ y : nat,
  y <
  S
    (length
       (flatten_formula f1_1 ++
        flatten_formula f1_2))
  → ∀ f1 : Formula,
      y = length (flatten_formula f1)
      → formula_prefix_is_not_formula_prop f1
suf: list symbol
f2_1, f2_2: Formula
Hpre: flatten_formula f1_1 ++ flatten_formula f1_2 =
(flatten_formula f2_1 ++ flatten_formula f2_2) ++
suf
s: symbol
s :: flatten_formula f1_1 ++ flatten_formula f1_2
`prefix_of` s
            :: flatten_formula f2_1 ++
               flatten_formula f2_2
  erewrite flatten_formula_formula_prefix_is_not_formula_prop_app_prefix;
    [done | .. | by eexists]; (eapply IHn; [| done]).Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
f1_1, f1_2: Formula
IHn: ∀ y : nat,
  y <
  S
    (length
       (flatten_formula f1_1 ++
        flatten_formula f1_2))
  → ∀ f1 : Formula,
      y = length (flatten_formula f1)
      → formula_prefix_is_not_formula_prop f1
suf: list symbol
f2_1, f2_2: Formula
Hpre: flatten_formula f1_1 ++ flatten_formula f1_2 =
(flatten_formula f2_1 ++ flatten_formula f2_2) ++
suf
s: symbol
length (flatten_formula f1_1) <
S
  (length
     (flatten_formula f1_1 ++ flatten_formula f1_2))
Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
f1_1, f1_2: Formula
IHn: ∀ y : nat,
  y <
  S
    (length
       (flatten_formula f1_1 ++
        flatten_formula f1_2))
  → ∀ f1 : Formula,
      y = length (flatten_formula f1)
      → formula_prefix_is_not_formula_prop f1
suf: list symbol
f2_1, f2_2: Formula
Hpre: flatten_formula f1_1 ++ flatten_formula f1_2 =
(flatten_formula f2_1 ++ flatten_formula f2_2) ++
suf
s: symbol
length (flatten_formula f1_2) <
S
  (length
     (flatten_formula f1_1 ++ flatten_formula f1_2))
Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
f1_1, f1_2: Formula
IHn: ∀ y : nat,
  y <
  S
    (length
       (flatten_formula f1_1 ++
        flatten_formula f1_2))
  → ∀ f1 : Formula,
      y = length (flatten_formula f1)
      → formula_prefix_is_not_formula_prop f1
suf: list symbol
f2_1, f2_2: Formula
Hpre: flatten_formula f1_1 ++ flatten_formula f1_2 =
(flatten_formula f2_1 ++ flatten_formula f2_2) ++
suf
s: symbol
length (flatten_formula f2_1) <
S
  (length
     (flatten_formula f1_1 ++ flatten_formula f1_2))
Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
f1_1, f1_2: Formula
IHn: ∀ y : nat,
  y <
  S
    (length
       (flatten_formula f1_1 ++
        flatten_formula f1_2))
  → ∀ f1 : Formula,
      y = length (flatten_formula f1)
      → formula_prefix_is_not_formula_prop f1
suf: list symbol
f2_1, f2_2: Formula
Hpre: flatten_formula f1_1 ++ flatten_formula f1_2 =
(flatten_formula f2_1 ++ flatten_formula f2_2) ++
suf
s: symbol
length (flatten_formula f2_2) <
S
  (length
     (flatten_formula f1_1 ++ flatten_formula f1_2))
  -Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
f1_1, f1_2: Formula
IHn: ∀ y : nat,
  y <
  S
    (length
       (flatten_formula f1_1 ++
        flatten_formula f1_2))
  → ∀ f1 : Formula,
      y = length (flatten_formula f1)
      → formula_prefix_is_not_formula_prop f1
suf: list symbol
f2_1, f2_2: Formula
Hpre: flatten_formula f1_1 ++ flatten_formula f1_2 =
(flatten_formula f2_1 ++ flatten_formula f2_2) ++
suf
s: symbol
length (flatten_formula f1_1) <
S
  (length
     (flatten_formula f1_1 ++ flatten_formula f1_2)) by rewrite app_length; lia.
  -Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
f1_1, f1_2: Formula
IHn: ∀ y : nat,
  y <
  S
    (length
       (flatten_formula f1_1 ++
        flatten_formula f1_2))
  → ∀ f1 : Formula,
      y = length (flatten_formula f1)
      → formula_prefix_is_not_formula_prop f1
suf: list symbol
f2_1, f2_2: Formula
Hpre: flatten_formula f1_1 ++ flatten_formula f1_2 =
(flatten_formula f2_1 ++ flatten_formula f2_2) ++
suf
s: symbol
length (flatten_formula f1_2) <
S
  (length
     (flatten_formula f1_1 ++ flatten_formula f1_2)) by rewrite app_length; lia.
  -Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
f1_1, f1_2: Formula
IHn: ∀ y : nat,
  y <
  S
    (length
       (flatten_formula f1_1 ++
        flatten_formula f1_2))
  → ∀ f1 : Formula,
      y = length (flatten_formula f1)
      → formula_prefix_is_not_formula_prop f1
suf: list symbol
f2_1, f2_2: Formula
Hpre: flatten_formula f1_1 ++ flatten_formula f1_2 =
(flatten_formula f2_1 ++ flatten_formula f2_2) ++
suf
s: symbol
length (flatten_formula f2_1) <
S
  (length
     (flatten_formula f1_1 ++ flatten_formula f1_2)) by rewrite Hpre, !app_length; lia.
  -Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
f1_1, f1_2: Formula
IHn: ∀ y : nat,
  y <
  S
    (length
       (flatten_formula f1_1 ++
        flatten_formula f1_2))
  → ∀ f1 : Formula,
      y = length (flatten_formula f1)
      → formula_prefix_is_not_formula_prop f1
suf: list symbol
f2_1, f2_2: Formula
Hpre: flatten_formula f1_1 ++ flatten_formula f1_2 =
(flatten_formula f2_1 ++ flatten_formula f2_2) ++
suf
s: symbol
length (flatten_formula f2_2) <
S
  (length
     (flatten_formula f1_1 ++ flatten_formula f1_2)) by rewrite Hpre, !app_length; lia.
Qed.

Lemma flatten_formula_prefix :
  forall (f1 : Formula),
    formula_prefix_is_not_formula_prop f1.Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
∀ f1 : Formula, formula_prefix_is_not_formula_prop f1
Proof.Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
∀ f1 : Formula, formula_prefix_is_not_formula_prop f1
  intros f1.Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
f1: Formula
formula_prefix_is_not_formula_prop f1
  remember (length (flatten_formula f1)) as n.Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
f1: Formula
n: nat
Heqn: n = length (flatten_formula f1)
formula_prefix_is_not_formula_prop f1
  revert f1 Heqn; induction n as [n IHn] using (well_founded_induction lt_wf).Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
n: nat
IHn: ∀ y : nat,
  y < n
  → ∀ f1 : Formula,
      y = length (flatten_formula f1)
      → formula_prefix_is_not_formula_prop f1
∀ f1 : Formula,
  n = length (flatten_formula f1)
  → formula_prefix_is_not_formula_prop f1
  intros f1 -> s [[suf Hpre] Hproper] f2 <-.Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
f1: Formula
IHn: ∀ y : nat,
  y < length (flatten_formula f1)
  → ∀ f1 : Formula,
      y = length (flatten_formula f1)
      → formula_prefix_is_not_formula_prop f1
suf: list symbol
f2: Formula
Hproper: (¬ flatten_formula f1
   `prefix_of` flatten_formula f2)%type
Hpre: flatten_formula f1 = flatten_formula f2 ++ suf
False
  destruct f1, f2; cbn in *; try congruence; simplify_list_eq;
    [done | done | done | | by contradict Hproper; eapply flatten_formula_prefix_helper..].Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
f1: Formula
IHn: ∀ y : nat,
  y < S (length (flatten_formula f1))
  → ∀ f1 : Formula,
      y = length (flatten_formula f1)
      → formula_prefix_is_not_formula_prop f1
suf: list symbol
f2: Formula
Hproper: (¬ Neg :: flatten_formula f1
   `prefix_of` Neg :: flatten_formula f2)%type
Hpre: flatten_formula f1 = flatten_formula f2 ++ suf
False
  eapply IHn with (f1 := f1) (f2 := f2); cycle 1; [done | | done | by lia].Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
f1: Formula
IHn: ∀ y : nat,
  y < S (length (flatten_formula f1))
  → ∀ f1 : Formula,
      y = length (flatten_formula f1)
      → formula_prefix_is_not_formula_prop f1
suf: list symbol
f2: Formula
Hproper: (¬ Neg :: flatten_formula f1
   `prefix_of` Neg :: flatten_formula f2)%type
Hpre: flatten_formula f1 = flatten_formula f2 ++ suf
strict prefix (flatten_formula f2)
  (flatten_formula f1)
  split; [by eexists |].Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
f1: Formula
IHn: ∀ y : nat,
  y < S (length (flatten_formula f1))
  → ∀ f1 : Formula,
      y = length (flatten_formula f1)
      → formula_prefix_is_not_formula_prop f1
suf: list symbol
f2: Formula
Hproper: (¬ Neg :: flatten_formula f1
   `prefix_of` Neg :: flatten_formula f2)%type
Hpre: flatten_formula f1 = flatten_formula f2 ++ suf
(¬ flatten_formula f1 `prefix_of` flatten_formula f2)%type
  intros [suf' Hsuf']; contradict Hproper.Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
f1: Formula
IHn: ∀ y : nat,
  y < S (length (flatten_formula f1))
  → ∀ f1 : Formula,
      y = length (flatten_formula f1)
      → formula_prefix_is_not_formula_prop f1
suf: list symbol
f2: Formula
Hpre: flatten_formula f1 = flatten_formula f2 ++ suf
suf': list symbol
Hsuf': flatten_formula f2 =
flatten_formula f1 ++ suf'
Neg :: flatten_formula f1
`prefix_of` Neg :: flatten_formula f2
  by exists suf'; rewrite Hsuf'.
Qed.

Lemma flatten_formula_common_prefix :
  forall (fa fb : Formula) (sufa sufb : expression),
    flatten_formula fa ++ sufa = flatten_formula fb ++ sufb ->
    flatten_formula fa = flatten_formula fb /\ sufa = sufb.Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
∀ (fa fb : Formula) (sufa sufb : expression),
  flatten_formula fa ++ sufa =
  flatten_formula fb ++ sufb
  → flatten_formula fa = flatten_formula fb
    ∧ sufa = sufb
Proof.Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
∀ (fa fb : Formula) (sufa sufb : expression),
  flatten_formula fa ++ sufa =
  flatten_formula fb ++ sufb
  → flatten_formula fa = flatten_formula fb
    ∧ sufa = sufb
  intros * Hpre.Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
fa, fb: Formula
sufa, sufb: expression
Hpre: flatten_formula fa ++ sufa =
flatten_formula fb ++ sufb
(flatten_formula fa = flatten_formula fb ∧ sufa = sufb)%type
  by apply flatten_formula_formula_prefix_is_not_formula_prop_app;
    [apply flatten_formula_prefix.. |].
Qed.

#[export] Instance flatten_formula_inj : Inj (=) (=) flatten_formula.Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
Inj eq eq flatten_formula
Proof.Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
Inj eq eq flatten_formula
  by intros f; induction f; intros []; cbn; inversion 1 as [Heq];
    [| | | by apply IHf in Heq as ->
    | apply flatten_formula_common_prefix in Heq as []; erewrite IHf1, IHf2..].
Qed.

Definition binop_state_cast
  (si : expression) (j : index) : state (expression_components j) :=
  match j with
  | ITop | IBot | IVar | INeg => ()
  | _ => Some si
  end.

Inductive BinOp : symbol -> Prop :=
| bin_op_conj : BinOp Conj
| bin_op_disj : BinOp Disj
| bin_op_impl : BinOp Impl
| bin_op_iff : BinOp Iff.

Lemma well_formed_flatten_formula_helper :
  forall (binop : symbol), BinOp binop ->
  forall (f1 f2 : Formula),
    well_formed_expression (flatten_formula f1) ->
    well_formed_expression (flatten_formula f2) ->
    well_formed_expression (binop :: flatten_formula f1 ++ flatten_formula f2).Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
∀ binop : symbol,
  BinOp binop
  → ∀ f1 f2 : Formula,
      well_formed_expression (flatten_formula f1)
      → well_formed_expression (flatten_formula f2)
        → well_formed_expression
            (binop
             :: flatten_formula f1 ++
                flatten_formula f2)
Proof.Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
∀ binop : symbol,
  BinOp binop
  → ∀ f1 f2 : Formula,
      well_formed_expression (flatten_formula f1)
      → well_formed_expression (flatten_formula f2)
        → well_formed_expression
            (binop
             :: flatten_formula f1 ++
                flatten_formula f2)
  intros binop Hbinop f1 f2 Hf1 Hf2.Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
binop: symbol
Hbinop: BinOp binop
f1, f2: Formula
Hf1: well_formed_expression (flatten_formula f1)
Hf2: well_formed_expression (flatten_formula f2)
well_formed_expression
  (binop :: flatten_formula f1 ++ flatten_formula f2)
  pose (i := symbol_to_index binop).Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
binop: symbol
Hbinop: BinOp binop
f1, f2: Formula
Hf1: well_formed_expression (flatten_formula f1)
Hf2: well_formed_expression (flatten_formula f2)
i:= symbol_to_index binop: index
well_formed_expression
  (binop :: flatten_formula f1 ++ flatten_formula f2)
  pose (s0 := ` (composite_s0 expression_components)).Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
binop: symbol
Hbinop: BinOp binop
f1, f2: Formula
Hf1: well_formed_expression (flatten_formula f1)
Hf2: well_formed_expression (flatten_formula f2)
i:= symbol_to_index binop: index
s0:= `(composite_s0 expression_components): composite_state expression_components
well_formed_expression
  (binop :: flatten_formula f1 ++ flatten_formula f2)
  pose (s1 := state_update expression_components s0 i
    (binop_state_cast (flatten_formula f1) i)).Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
binop: symbol
Hbinop: BinOp binop
f1, f2: Formula
Hf1: well_formed_expression (flatten_formula f1)
Hf2: well_formed_expression (flatten_formula f2)
i:= symbol_to_index binop: index
s0:= `(composite_s0 expression_components): composite_state expression_components
s1:= state_update expression_components s0 i
  (binop_state_cast (flatten_formula f1) i): ∀ j : index, state (expression_components j)
well_formed_expression
  (binop :: flatten_formula f1 ++ flatten_formula f2)
  assert (Ht1 : input_valid_transition expression_vlsm
    (default_composite_label i) (s0, Some (flatten_formula f1)) (s1, None)).Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
binop: symbol
Hbinop: BinOp binop
f1, f2: Formula
Hf1: well_formed_expression (flatten_formula f1)
Hf2: well_formed_expression (flatten_formula f2)
i:= symbol_to_index binop: index
s0:= `(composite_s0 expression_components): composite_state expression_components
s1:= state_update expression_components s0 i
  (binop_state_cast (flatten_formula f1) i): ∀ j : index, state (expression_components j)
input_valid_transition expression_vlsm
  (default_composite_label i)
  (s0, Some (flatten_formula f1)) (s1, None)
Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
binop: symbol
Hbinop: BinOp binop
f1, f2: Formula
Hf1: well_formed_expression (flatten_formula f1)
Hf2: well_formed_expression (flatten_formula f2)
i:= symbol_to_index binop: index
s0:= `(composite_s0 expression_components): composite_state expression_components
s1:= state_update expression_components s0 i
  (binop_state_cast (flatten_formula f1) i): ∀ j : index, state (expression_components j)
Ht1: input_valid_transition expression_vlsm
  (default_composite_label i)
  (s0, Some (flatten_formula f1)) (
  s1, None)
well_formed_expression
  (binop :: flatten_formula f1 ++ flatten_formula f2)
  {Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
binop: symbol
Hbinop: BinOp binop
f1, f2: Formula
Hf1: well_formed_expression (flatten_formula f1)
Hf2: well_formed_expression (flatten_formula f2)
i:= symbol_to_index binop: index
s0:= `(composite_s0 expression_components): composite_state expression_components
s1:= state_update expression_components s0 i
  (binop_state_cast (flatten_formula f1) i): ∀ j : index, state (expression_components j)
input_valid_transition expression_vlsm
  (default_composite_label i)
  (s0, Some (flatten_formula f1)) (s1, None)
    repeat split.Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
binop: symbol
Hbinop: BinOp binop
f1, f2: Formula
Hf1: well_formed_expression (flatten_formula f1)
Hf2: well_formed_expression (flatten_formula f2)
i:= symbol_to_index binop: index
s0:= `(composite_s0 expression_components): composite_state expression_components
s1:= state_update expression_components s0 i
  (binop_state_cast (flatten_formula f1) i): ∀ j : index, state (expression_components j)
valid_state_prop expression_vlsm s0
Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
binop: symbol
Hbinop: BinOp binop
f1, f2: Formula
Hf1: well_formed_expression (flatten_formula f1)
Hf2: well_formed_expression (flatten_formula f2)
i:= symbol_to_index binop: index
s0:= `(composite_s0 expression_components): composite_state expression_components
s1:= state_update expression_components s0 i
  (binop_state_cast (flatten_formula f1) i): ∀ j : index, state (expression_components j)
option_valid_message_prop expression_vlsm
  (Some (flatten_formula f1))
Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
binop: symbol
Hbinop: BinOp binop
f1, f2: Formula
Hf1: well_formed_expression (flatten_formula f1)
Hf2: well_formed_expression (flatten_formula f2)
i:= symbol_to_index binop: index
s0:= `(composite_s0 expression_components): composite_state expression_components
s1:= state_update expression_components s0 i
  (binop_state_cast (flatten_formula f1) i): ∀ j : index, state (expression_components j)
valid (default_composite_label i)
  (s0, Some (flatten_formula f1))
Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
binop: symbol
Hbinop: BinOp binop
f1, f2: Formula
Hf1: well_formed_expression (flatten_formula f1)
Hf2: well_formed_expression (flatten_formula f2)
i:= symbol_to_index binop: index
s0:= `(composite_s0 expression_components): composite_state expression_components
s1:= state_update expression_components s0 i
  (binop_state_cast (flatten_formula f1) i): ∀ j : index, state (expression_components j)
transition (default_composite_label i)
  (s0, Some (flatten_formula f1)) = (
s1, None)
    -Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
binop: symbol
Hbinop: BinOp binop
f1, f2: Formula
Hf1: well_formed_expression (flatten_formula f1)
Hf2: well_formed_expression (flatten_formula f2)
i:= symbol_to_index binop: index
s0:= `(composite_s0 expression_components): composite_state expression_components
s1:= state_update expression_components s0 i
  (binop_state_cast (flatten_formula f1) i): ∀ j : index, state (expression_components j)
valid_state_prop expression_vlsm s0 by apply initial_state_is_valid; destruct composite_s0.
    -Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
binop: symbol
Hbinop: BinOp binop
f1, f2: Formula
Hf1: well_formed_expression (flatten_formula f1)
Hf2: well_formed_expression (flatten_formula f2)
i:= symbol_to_index binop: index
s0:= `(composite_s0 expression_components): composite_state expression_components
s1:= state_update expression_components s0 i
  (binop_state_cast (flatten_formula f1) i): ∀ j : index, state (expression_components j)
option_valid_message_prop expression_vlsm
  (Some (flatten_formula f1)) done.
    -Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
binop: symbol
Hbinop: BinOp binop
f1, f2: Formula
Hf1: well_formed_expression (flatten_formula f1)
Hf2: well_formed_expression (flatten_formula f2)
i:= symbol_to_index binop: index
s0:= `(composite_s0 expression_components): composite_state expression_components
s1:= state_update expression_components s0 i
  (binop_state_cast (flatten_formula f1) i): ∀ j : index, state (expression_components j)
valid (default_composite_label i)
  (s0, Some (flatten_formula f1)) by inversion Hbinop; subst; eexists.
    -Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
binop: symbol
Hbinop: BinOp binop
f1, f2: Formula
Hf1: well_formed_expression (flatten_formula f1)
Hf2: well_formed_expression (flatten_formula f2)
i:= symbol_to_index binop: index
s0:= `(composite_s0 expression_components): composite_state expression_components
s1:= state_update expression_components s0 i
  (binop_state_cast (flatten_formula f1) i): ∀ j : index, state (expression_components j)
transition (default_composite_label i)
  (s0, Some (flatten_formula f1)) = (s1, None) by inversion Hbinop; subst.
  }Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
binop: symbol
Hbinop: BinOp binop
f1, f2: Formula
Hf1: well_formed_expression (flatten_formula f1)
Hf2: well_formed_expression (flatten_formula f2)
i:= symbol_to_index binop: index
s0:= `(composite_s0 expression_components): composite_state expression_components
s1:= state_update expression_components s0 i
  (binop_state_cast (flatten_formula f1) i): ∀ j : index, state (expression_components j)
Ht1: input_valid_transition expression_vlsm
  (default_composite_label i)
  (s0, Some (flatten_formula f1)) (
  s1, None)
well_formed_expression
  (binop :: flatten_formula f1 ++ flatten_formula f2)
  cut (input_valid_transition expression_vlsm
    (default_composite_label i) (s1, Some (flatten_formula f2))
    (s0, Some (binop :: flatten_formula f1 ++ flatten_formula f2)));
    [by eapply input_valid_transition_out |].Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
binop: symbol
Hbinop: BinOp binop
f1, f2: Formula
Hf1: well_formed_expression (flatten_formula f1)
Hf2: well_formed_expression (flatten_formula f2)
i:= symbol_to_index binop: index
s0:= `(composite_s0 expression_components): composite_state expression_components
s1:= state_update expression_components s0 i
  (binop_state_cast (flatten_formula f1) i): ∀ j : index, state (expression_components j)
Ht1: input_valid_transition expression_vlsm
  (default_composite_label i)
  (s0, Some (flatten_formula f1)) (
  s1, None)
input_valid_transition expression_vlsm
  (default_composite_label i)
  (s1, Some (flatten_formula f2))
  (s0,
   Some
     (binop
      :: flatten_formula f1 ++ flatten_formula f2))
  repeat split.Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
binop: symbol
Hbinop: BinOp binop
f1, f2: Formula
Hf1: well_formed_expression (flatten_formula f1)
Hf2: well_formed_expression (flatten_formula f2)
i:= symbol_to_index binop: index
s0:= `(composite_s0 expression_components): composite_state expression_components
s1:= state_update expression_components s0 i
  (binop_state_cast (flatten_formula f1) i): ∀ j : index, state (expression_components j)
Ht1: input_valid_transition expression_vlsm
  (default_composite_label i)
  (s0, Some (flatten_formula f1)) (
  s1, None)
valid_state_prop expression_vlsm s1
Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
binop: symbol
Hbinop: BinOp binop
f1, f2: Formula
Hf1: well_formed_expression (flatten_formula f1)
Hf2: well_formed_expression (flatten_formula f2)
i:= symbol_to_index binop: index
s0:= `(composite_s0 expression_components): composite_state expression_components
s1:= state_update expression_components s0 i
  (binop_state_cast (flatten_formula f1) i): ∀ j : index, state (expression_components j)
Ht1: input_valid_transition expression_vlsm
  (default_composite_label i)
  (s0, Some (flatten_formula f1)) (
  s1, None)
option_valid_message_prop expression_vlsm
  (Some (flatten_formula f2))
Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
binop: symbol
Hbinop: BinOp binop
f1, f2: Formula
Hf1: well_formed_expression (flatten_formula f1)
Hf2: well_formed_expression (flatten_formula f2)
i:= symbol_to_index binop: index
s0:= `(composite_s0 expression_components): composite_state expression_components
s1:= state_update expression_components s0 i
  (binop_state_cast (flatten_formula f1) i): ∀ j : index, state (expression_components j)
Ht1: input_valid_transition expression_vlsm
  (default_composite_label i)
  (s0, Some (flatten_formula f1)) (
  s1, None)
valid (default_composite_label i)
  (s1, Some (flatten_formula f2))
Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
binop: symbol
Hbinop: BinOp binop
f1, f2: Formula
Hf1: well_formed_expression (flatten_formula f1)
Hf2: well_formed_expression (flatten_formula f2)
i:= symbol_to_index binop: index
s0:= `(composite_s0 expression_components): composite_state expression_components
s1:= state_update expression_components s0 i
  (binop_state_cast (flatten_formula f1) i): ∀ j : index, state (expression_components j)
Ht1: input_valid_transition expression_vlsm
  (default_composite_label i)
  (s0, Some (flatten_formula f1)) (
  s1, None)
transition (default_composite_label i)
  (s1, Some (flatten_formula f2)) =
(s0,
 Some
   (binop :: flatten_formula f1 ++ flatten_formula f2))
  -Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
binop: symbol
Hbinop: BinOp binop
f1, f2: Formula
Hf1: well_formed_expression (flatten_formula f1)
Hf2: well_formed_expression (flatten_formula f2)
i:= symbol_to_index binop: index
s0:= `(composite_s0 expression_components): composite_state expression_components
s1:= state_update expression_components s0 i
  (binop_state_cast (flatten_formula f1) i): ∀ j : index, state (expression_components j)
Ht1: input_valid_transition expression_vlsm
  (default_composite_label i)
  (s0, Some (flatten_formula f1)) (
  s1, None)
valid_state_prop expression_vlsm s1 by eapply input_valid_transition_destination.
  -Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
binop: symbol
Hbinop: BinOp binop
f1, f2: Formula
Hf1: well_formed_expression (flatten_formula f1)
Hf2: well_formed_expression (flatten_formula f2)
i:= symbol_to_index binop: index
s0:= `(composite_s0 expression_components): composite_state expression_components
s1:= state_update expression_components s0 i
  (binop_state_cast (flatten_formula f1) i): ∀ j : index, state (expression_components j)
Ht1: input_valid_transition expression_vlsm
  (default_composite_label i)
  (s0, Some (flatten_formula f1)) (
  s1, None)
option_valid_message_prop expression_vlsm
  (Some (flatten_formula f2)) done.
  -Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
binop: symbol
Hbinop: BinOp binop
f1, f2: Formula
Hf1: well_formed_expression (flatten_formula f1)
Hf2: well_formed_expression (flatten_formula f2)
i:= symbol_to_index binop: index
s0:= `(composite_s0 expression_components): composite_state expression_components
s1:= state_update expression_components s0 i
  (binop_state_cast (flatten_formula f1) i): ∀ j : index, state (expression_components j)
Ht1: input_valid_transition expression_vlsm
  (default_composite_label i)
  (s0, Some (flatten_formula f1)) (
  s1, None)
valid (default_composite_label i)
  (s1, Some (flatten_formula f2)) by inversion Hbinop; subst; eexists.
  -Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
binop: symbol
Hbinop: BinOp binop
f1, f2: Formula
Hf1: well_formed_expression (flatten_formula f1)
Hf2: well_formed_expression (flatten_formula f2)
i:= symbol_to_index binop: index
s0:= `(composite_s0 expression_components): composite_state expression_components
s1:= state_update expression_components s0 i
  (binop_state_cast (flatten_formula f1) i): ∀ j : index, state (expression_components j)
Ht1: input_valid_transition expression_vlsm
  (default_composite_label i)
  (s0, Some (flatten_formula f1)) (
  s1, None)
transition (default_composite_label i)
  (s1, Some (flatten_formula f2)) =
(s0,
 Some
   (binop :: flatten_formula f1 ++ flatten_formula f2)) by inversion Hbinop; subst binop i s1; cbn in *;
      rewrite state_update_eq, state_update_twice, state_update_id.
Qed.

The flattening of a Formula is a well_formed_expression.

Theorem flatten_formulas_are_well_formed_expressions :
  forall (f : Formula),
    well_formed_expression (flatten_formula f).Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
∀ f : Formula,
  well_formed_expression (flatten_formula f)
Proof.Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
∀ f : Formula,
  well_formed_expression (flatten_formula f)
  induction f; cbn.Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
well_formed_expression [Top]
Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
well_formed_expression [Bot]
Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
x: Var
well_formed_expression [PVar x]
Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
f: Formula
IHf: well_formed_expression (flatten_formula f)
well_formed_expression (Neg :: flatten_formula f)
Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
f1, f2: Formula
IHf1: well_formed_expression (flatten_formula f1)
IHf2: well_formed_expression (flatten_formula f2)
well_formed_expression
  (Conj :: flatten_formula f1 ++ flatten_formula f2)
Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
f1, f2: Formula
IHf1: well_formed_expression (flatten_formula f1)
IHf2: well_formed_expression (flatten_formula f2)
well_formed_expression
  (Disj :: flatten_formula f1 ++ flatten_formula f2)
Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
f1, f2: Formula
IHf1: well_formed_expression (flatten_formula f1)
IHf2: well_formed_expression (flatten_formula f2)
well_formed_expression
  (Impl :: flatten_formula f1 ++ flatten_formula f2)
Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
f1, f2: Formula
IHf1: well_formed_expression (flatten_formula f1)
IHf2: well_formed_expression (flatten_formula f2)
well_formed_expression
  (Iff :: flatten_formula f1 ++ flatten_formula f2)
  -Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
well_formed_expression [Top] cut (input_valid_transition expression_vlsm (existT ITop ())
      (` (composite_s0 expression_components), None)
      (` (composite_s0 expression_components), Some ([Top])));
      [by eapply input_valid_transition_out |].Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
input_valid_transition expression_vlsm
  (existT ITop ())
  (`(composite_s0 expression_components), None)
  (`(composite_s0 expression_components), Some [Top])
    repeat split.Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
valid_state_prop expression_vlsm
  (`(composite_s0 expression_components))
Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
option_valid_message_prop expression_vlsm None
Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
transition (existT ITop ())
  (`(composite_s0 expression_components), None) =
(`(composite_s0 expression_components), Some [Top])
    +Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
valid_state_prop expression_vlsm
  (`(composite_s0 expression_components)) by apply initial_state_is_valid; destruct composite_s0.
    +Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
option_valid_message_prop expression_vlsm None by apply option_valid_message_None.
    +Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
transition (existT ITop ())
  (`(composite_s0 expression_components), None) =
(`(composite_s0 expression_components), Some [Top]) by cbn; rewrite state_update_id.
  -Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
well_formed_expression [Bot] cut (input_valid_transition expression_vlsm (existT IBot ())
      (` (composite_s0 expression_components), None)
      (` (composite_s0 expression_components), Some ([Bot])));
      [by eapply input_valid_transition_out |].Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
input_valid_transition expression_vlsm
  (existT IBot ())
  (`(composite_s0 expression_components), None)
  (`(composite_s0 expression_components), Some [Bot])
    repeat split.Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
valid_state_prop expression_vlsm
  (`(composite_s0 expression_components))
Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
option_valid_message_prop expression_vlsm None
Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
transition (existT IBot ())
  (`(composite_s0 expression_components), None) =
(`(composite_s0 expression_components), Some [Bot])
    +Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
valid_state_prop expression_vlsm
  (`(composite_s0 expression_components)) by apply initial_state_is_valid; destruct composite_s0.
    +Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
option_valid_message_prop expression_vlsm None by apply option_valid_message_None.
    +Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
transition (existT IBot ())
  (`(composite_s0 expression_components), None) =
(`(composite_s0 expression_components), Some [Bot]) by cbn; rewrite state_update_id.
  -Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
x: Var
well_formed_expression [PVar x] cut (input_valid_transition expression_vlsm (existT IVar x)
      (` (composite_s0 expression_components), None)
      (` (composite_s0 expression_components), Some ([PVar x])));
      [by eapply input_valid_transition_out |].Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
x: Var
input_valid_transition expression_vlsm (existT IVar x)
  (`(composite_s0 expression_components), None)
  (`(composite_s0 expression_components),
   Some [PVar x])
    repeat split.Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
x: Var
valid_state_prop expression_vlsm
  (`(composite_s0 expression_components))
Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
x: Var
option_valid_message_prop expression_vlsm None
Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
x: Var
transition (existT IVar x)
  (`(composite_s0 expression_components), None) =
(`(composite_s0 expression_components), Some [PVar x])
    +Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
x: Var
valid_state_prop expression_vlsm
  (`(composite_s0 expression_components)) by apply initial_state_is_valid; destruct composite_s0.
    +Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
x: Var
option_valid_message_prop expression_vlsm None by apply option_valid_message_None.
    +Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
x: Var
transition (existT IVar x)
  (`(composite_s0 expression_components), None) =
(`(composite_s0 expression_components), Some [PVar x]) by cbn; rewrite state_update_id.
  -Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
f: Formula
IHf: well_formed_expression (flatten_formula f)
well_formed_expression (Neg :: flatten_formula f) cut (input_valid_transition expression_vlsm (existT INeg ())
      (` (composite_s0 expression_components), Some (flatten_formula f))
      (` (composite_s0 expression_components), Some (Neg :: flatten_formula f)));
      [by eapply input_valid_transition_out |].Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
f: Formula
IHf: well_formed_expression (flatten_formula f)
input_valid_transition expression_vlsm
  (existT INeg ())
  (`(composite_s0 expression_components),
   Some (flatten_formula f))
  (`(composite_s0 expression_components),
   Some (Neg :: flatten_formula f))
    repeat split.Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
f: Formula
IHf: well_formed_expression (flatten_formula f)
valid_state_prop expression_vlsm
  (`(composite_s0 expression_components))
Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
f: Formula
IHf: well_formed_expression (flatten_formula f)
option_valid_message_prop expression_vlsm
  (Some (flatten_formula f))
Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
f: Formula
IHf: well_formed_expression (flatten_formula f)
valid (existT INeg ())
  (`(composite_s0 expression_components),
   Some (flatten_formula f))
Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
f: Formula
IHf: well_formed_expression (flatten_formula f)
transition (existT INeg ())
  (`(composite_s0 expression_components),
   Some (flatten_formula f)) =
(`(composite_s0 expression_components),
 Some (Neg :: flatten_formula f))
    +Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
f: Formula
IHf: well_formed_expression (flatten_formula f)
valid_state_prop expression_vlsm
  (`(composite_s0 expression_components)) by apply initial_state_is_valid; destruct composite_s0.
    +Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
f: Formula
IHf: well_formed_expression (flatten_formula f)
option_valid_message_prop expression_vlsm
  (Some (flatten_formula f)) done.
    +Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
f: Formula
IHf: well_formed_expression (flatten_formula f)
valid (existT INeg ())
  (`(composite_s0 expression_components),
   Some (flatten_formula f)) by eexists.
    +Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
f: Formula
IHf: well_formed_expression (flatten_formula f)
transition (existT INeg ())
  (`(composite_s0 expression_components),
   Some (flatten_formula f)) =
(`(composite_s0 expression_components),
 Some (Neg :: flatten_formula f)) by cbn; rewrite state_update_id.
  -Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
f1, f2: Formula
IHf1: well_formed_expression (flatten_formula f1)
IHf2: well_formed_expression (flatten_formula f2)
well_formed_expression
  (Conj :: flatten_formula f1 ++ flatten_formula f2) by apply well_formed_flatten_formula_helper; [constructor | ..].
  -Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
f1, f2: Formula
IHf1: well_formed_expression (flatten_formula f1)
IHf2: well_formed_expression (flatten_formula f2)
well_formed_expression
  (Disj :: flatten_formula f1 ++ flatten_formula f2) by apply well_formed_flatten_formula_helper; [constructor | ..].
  -Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
f1, f2: Formula
IHf1: well_formed_expression (flatten_formula f1)
IHf2: well_formed_expression (flatten_formula f2)
well_formed_expression
  (Impl :: flatten_formula f1 ++ flatten_formula f2) by apply well_formed_flatten_formula_helper; [constructor | ..].
  -Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
f1, f2: Formula
IHf1: well_formed_expression (flatten_formula f1)
IHf2: well_formed_expression (flatten_formula f2)
well_formed_expression
  (Iff :: flatten_formula f1 ++ flatten_formula f2) by apply well_formed_flatten_formula_helper; [constructor | ..].
Qed.

Definition binop_state_proj
  (s : composite_state expression_components) (i : index) : option expression :=
  match i with
  | ITop | IBot | IVar | INeg => None
  | i => s i
  end.

Lemma well_formed_is_flatten_formula_helper
  (binop : symbol)
  (Hbinop : BinOp binop)
  (i := symbol_to_index binop)
  (e : expression)
  (Hind : forall (y : nat),
    y < length e ->
    forall (e : expression), y = length e -> well_formed_expression e ->
    exists (f : Formula), flatten_formula f = e)
  (s0 : composite_state expression_components)
  (si' : option expression)
  (om : option expression)
  (Hom : option_valid_message_prop expression_vlsm om)
  (Hti : transition (VLSMMachine := expression_binop_vlsm_machine binop) ()
    (binop_state_proj s0 i, om) = (si', Some e))
  (Hs0 : valid_state_prop expression_vlsm s0) :
    exists f : Formula, flatten_formula f = e.Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
binop: symbol
Hbinop: BinOp binop
i:= symbol_to_index binop: index
e: expression
Hind: ∀ y : nat,
  y < length e
  → ∀ e : expression,
      y = length e
      → well_formed_expression e
        → ∃ f : Formula, flatten_formula f = e
s0: composite_state expression_components
si', om: option expression
Hom: option_valid_message_prop expression_vlsm om
Hti: transition () (binop_state_proj s0 i, om) =
(si', Some e)
Hs0: valid_state_prop expression_vlsm s0
∃ f : Formula, flatten_formula f = e
Proof.Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
binop: symbol
Hbinop: BinOp binop
i:= symbol_to_index binop: index
e: expression
Hind: ∀ y : nat,
  y < length e
  → ∀ e : expression,
      y = length e
      → well_formed_expression e
        → ∃ f : Formula, flatten_formula f = e
s0: composite_state expression_components
si', om: option expression
Hom: option_valid_message_prop expression_vlsm om
Hti: transition () (binop_state_proj s0 i, om) =
(si', Some e)
Hs0: valid_state_prop expression_vlsm s0
∃ f : Formula, flatten_formula f = e
  destruct (binop_state_proj s0 i) as [e1 |] eqn: Hs0i;
    [| by destruct om; inversion Hti].Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
binop: symbol
Hbinop: BinOp binop
i:= symbol_to_index binop: index
e: expression
Hind: ∀ y : nat,
  y < length e
  → ∀ e : expression,
      y = length e
      → well_formed_expression e
        → ∃ f : Formula, flatten_formula f = e
s0: composite_state expression_components
si', om: option expression
Hom: option_valid_message_prop expression_vlsm om
e1: expression
Hs0i: binop_state_proj s0 i = Some e1
Hti: transition () (Some e1, om) = (si', Some e)
Hs0: valid_state_prop expression_vlsm s0
∃ f : Formula, flatten_formula f = e
  destruct om as [m |]; [| done].Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
binop: symbol
Hbinop: BinOp binop
i:= symbol_to_index binop: index
e: expression
Hind: ∀ y : nat,
  y < length e
  → ∀ e : expression,
      y = length e
      → well_formed_expression e
        → ∃ f : Formula, flatten_formula f = e
s0: composite_state expression_components
si': option expression
m: expression
Hom: option_valid_message_prop expression_vlsm
  (Some m)
e1: expression
Hs0i: binop_state_proj s0 i = Some e1
Hti: transition () (Some e1, Some m) = (si', Some e)
Hs0: valid_state_prop expression_vlsm s0
∃ f : Formula, flatten_formula f = e
  inversion Hti; subst; clear Hti.Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
binop: symbol
Hbinop: BinOp binop
i:= symbol_to_index binop: index
m, e1: expression
Hind: ∀ y : nat,
  y < length (binop :: e1 ++ m)
  → ∀ e : expression,
      y = length e
      → well_formed_expression e
        → ∃ f : Formula, flatten_formula f = e
s0: composite_state expression_components
Hom: option_valid_message_prop expression_vlsm
  (Some m)
Hs0i: binop_state_proj s0 i = Some e1
Hs0: valid_state_prop expression_vlsm s0
∃ f : Formula, flatten_formula f = binop :: e1 ++ m
  apply (free_valid_state_component_initial_or_transition i) in Hs0.Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
binop: symbol
Hbinop: BinOp binop
i:= symbol_to_index binop: index
m, e1: expression
Hind: ∀ y : nat,
  y < length (binop :: e1 ++ m)
  → ∀ e : expression,
      y = length e
      → well_formed_expression e
        → ∃ f : Formula, flatten_formula f = e
s0: composite_state expression_components
Hom: option_valid_message_prop expression_vlsm
  (Some m)
Hs0i: binop_state_proj s0 i = Some e1
Hs0: (initial_state_prop (s0 i)
 ∨ (∃ (l : label (expression_components i)) 
      (si0 : state (expression_components i)) 
      (om om' : option expression),
      input_valid_transition
        (free_composite_vlsm
           expression_components) 
        (existT i l)
        (state_update expression_components s0 i
           si0, om) (
        s0, om')))%type
∃ f : Formula, flatten_formula f = binop :: e1 ++ m
  destruct Hs0 as [Hs0 | (l & si & iom & oom & (_ & Hiom & Hvs0) & Ht)];
    [by inversion Hbinop; subst; cbn in *; congruence |].Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
binop: symbol
Hbinop: BinOp binop
i:= symbol_to_index binop: index
m, e1: expression
Hind: ∀ y : nat,
  y < length (binop :: e1 ++ m)
  → ∀ e : expression,
      y = length e
      → well_formed_expression e
        → ∃ f : Formula, flatten_formula f = e
s0: composite_state expression_components
Hom: option_valid_message_prop expression_vlsm
  (Some m)
Hs0i: binop_state_proj s0 i = Some e1
l: label (expression_components i)
si: state (expression_components i)
iom, oom: option expression
Hiom: option_valid_message_prop
  (free_composite_vlsm expression_components)
  iom
Hvs0: valid (existT i l)
  (state_update expression_components s0 i si,
   iom)
Ht: transition (existT i l)
  (state_update expression_components s0 i si,
   iom) = (s0, oom)
∃ f : Formula, flatten_formula f = binop :: e1 ++ m
  cbn in *; state_update_simpl.Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
binop: symbol
Hbinop: BinOp binop
i:= symbol_to_index binop: index
m, e1: expression
Hind: ∀ y : nat,
  y < S (length (e1 ++ m))
  → ∀ e : expression,
      y = length e
      → well_formed_expression e
        → ∃ f : Formula, flatten_formula f = e
s0: composite_state expression_components
Hom: option_valid_message_prop expression_vlsm
  (Some m)
Hs0i: binop_state_proj s0 i = Some e1
l: label (expression_components i)
si: state (expression_components i)
iom, oom: option expression
Hiom: option_valid_message_prop
  (free_composite_vlsm expression_components)
  iom
Hvs0: valid l (si, iom)
Ht: (let (si', om') := transition l (si, iom) in
 (state_update expression_components
    (state_update expression_components s0 i si)
    i si', om')) = (s0, oom)
∃ f : Formula, flatten_formula f = binop :: e1 ++ m
  eapply Hind in Hom as [f2 Hf2]; cycle 2;
    [done | | by rewrite app_length; lia].Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
binop: symbol
Hbinop: BinOp binop
i:= symbol_to_index binop: index
m, e1: expression
Hind: ∀ y : nat,
  y < S (length (e1 ++ m))
  → ∀ e : expression,
      y = length e
      → well_formed_expression e
        → ∃ f : Formula, flatten_formula f = e
s0: composite_state expression_components
Hs0i: binop_state_proj s0 i = Some e1
l: label (expression_components i)
si: state (expression_components i)
iom, oom: option expression
Hiom: option_valid_message_prop
  (free_composite_vlsm expression_components)
  iom
Hvs0: valid l (si, iom)
Ht: (let (si', om') := transition l (si, iom) in
 (state_update expression_components
    (state_update expression_components s0 i si)
    i si', om')) = (s0, oom)
f2: Formula
Hf2: flatten_formula f2 = m
∃ f : Formula, flatten_formula f = binop :: e1 ++ m
  cut (exists f1 : Formula, flatten_formula f1 = e1).Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
binop: symbol
Hbinop: BinOp binop
i:= symbol_to_index binop: index
m, e1: expression
Hind: ∀ y : nat,
  y < S (length (e1 ++ m))
  → ∀ e : expression,
      y = length e
      → well_formed_expression e
        → ∃ f : Formula, flatten_formula f = e
s0: composite_state expression_components
Hs0i: binop_state_proj s0 i = Some e1
l: label (expression_components i)
si: state (expression_components i)
iom, oom: option expression
Hiom: option_valid_message_prop
  (free_composite_vlsm expression_components)
  iom
Hvs0: valid l (si, iom)
Ht: (let (si', om') := transition l (si, iom) in
 (state_update expression_components
    (state_update expression_components s0 i si)
    i si', om')) = (s0, oom)
f2: Formula
Hf2: flatten_formula f2 = m
((∃ f1 : Formula, flatten_formula f1 = e1)
 → ∃ f : Formula, flatten_formula f = binop :: e1 ++ m)%type
Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
binop: symbol
Hbinop: BinOp binop
i:= symbol_to_index binop: index
m, e1: expression
Hind: ∀ y : nat,
  y < S (length (e1 ++ m))
  → ∀ e : expression,
      y = length e
      → well_formed_expression e
        → ∃ f : Formula, flatten_formula f = e
s0: composite_state expression_components
Hs0i: binop_state_proj s0 i = Some e1
l: label (expression_components i)
si: state (expression_components i)
iom, oom: option expression
Hiom: option_valid_message_prop
  (free_composite_vlsm expression_components)
  iom
Hvs0: valid l (si, iom)
Ht: (let (si', om') := transition l (si, iom) in
 (state_update expression_components
    (state_update expression_components s0 i si)
    i si', om')) = (s0, oom)
f2: Formula
Hf2: flatten_formula f2 = m
∃ f1 : Formula, flatten_formula f1 = e1
  {Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
binop: symbol
Hbinop: BinOp binop
i:= symbol_to_index binop: index
m, e1: expression
Hind: ∀ y : nat,
  y < S (length (e1 ++ m))
  → ∀ e : expression,
      y = length e
      → well_formed_expression e
        → ∃ f : Formula, flatten_formula f = e
s0: composite_state expression_components
Hs0i: binop_state_proj s0 i = Some e1
l: label (expression_components i)
si: state (expression_components i)
iom, oom: option expression
Hiom: option_valid_message_prop
  (free_composite_vlsm expression_components)
  iom
Hvs0: valid l (si, iom)
Ht: (let (si', om') := transition l (si, iom) in
 (state_update expression_components
    (state_update expression_components s0 i si)
    i si', om')) = (s0, oom)
f2: Formula
Hf2: flatten_formula f2 = m
((∃ f1 : Formula, flatten_formula f1 = e1)
 → ∃ f : Formula, flatten_formula f = binop :: e1 ++ m)%type
    subst m; intros [f1 <-]; inversion Hbinop.Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
binop: symbol
Hbinop: BinOp binop
i:= symbol_to_index binop: index
f2, f1: Formula
Hind: ∀ y : nat,
  y <
  S
    (length
       (flatten_formula f1 ++
        flatten_formula f2))
  → ∀ e : expression,
      y = length e
      → well_formed_expression e
        → ∃ f : Formula, flatten_formula f = e
s0: composite_state expression_components
Hs0i: binop_state_proj s0 i =
Some (flatten_formula f1)
l: label (expression_components i)
si: state (expression_components i)
iom, oom: option expression
Hiom: option_valid_message_prop
  (free_composite_vlsm expression_components)
  iom
Hvs0: valid l (si, iom)
Ht: (let (si', om') := transition l (si, iom) in
 (state_update expression_components
    (state_update expression_components s0 i si)
    i si', om')) = (s0, oom)
H0: Conj = binop
∃ f : Formula,
  flatten_formula f =
  Conj :: flatten_formula f1 ++ flatten_formula f2
Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
binop: symbol
Hbinop: BinOp binop
i:= symbol_to_index binop: index
f2, f1: Formula
Hind: ∀ y : nat,
  y <
  S
    (length
       (flatten_formula f1 ++
        flatten_formula f2))
  → ∀ e : expression,
      y = length e
      → well_formed_expression e
        → ∃ f : Formula, flatten_formula f = e
s0: composite_state expression_components
Hs0i: binop_state_proj s0 i =
Some (flatten_formula f1)
l: label (expression_components i)
si: state (expression_components i)
iom, oom: option expression
Hiom: option_valid_message_prop
  (free_composite_vlsm expression_components)
  iom
Hvs0: valid l (si, iom)
Ht: (let (si', om') := transition l (si, iom) in
 (state_update expression_components
    (state_update expression_components s0 i si)
    i si', om')) = (s0, oom)
H0: Disj = binop
∃ f : Formula,
  flatten_formula f =
  Disj :: flatten_formula f1 ++ flatten_formula f2
Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
binop: symbol
Hbinop: BinOp binop
i:= symbol_to_index binop: index
f2, f1: Formula
Hind: ∀ y : nat,
  y <
  S
    (length
       (flatten_formula f1 ++
        flatten_formula f2))
  → ∀ e : expression,
      y = length e
      → well_formed_expression e
        → ∃ f : Formula, flatten_formula f = e
s0: composite_state expression_components
Hs0i: binop_state_proj s0 i =
Some (flatten_formula f1)
l: label (expression_components i)
si: state (expression_components i)
iom, oom: option expression
Hiom: option_valid_message_prop
  (free_composite_vlsm expression_components)
  iom
Hvs0: valid l (si, iom)
Ht: (let (si', om') := transition l (si, iom) in
 (state_update expression_components
    (state_update expression_components s0 i si)
    i si', om')) = (s0, oom)
H0: Impl = binop
∃ f : Formula,
  flatten_formula f =
  Impl :: flatten_formula f1 ++ flatten_formula f2
Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
binop: symbol
Hbinop: BinOp binop
i:= symbol_to_index binop: index
f2, f1: Formula
Hind: ∀ y : nat,
  y <
  S
    (length
       (flatten_formula f1 ++
        flatten_formula f2))
  → ∀ e : expression,
      y = length e
      → well_formed_expression e
        → ∃ f : Formula, flatten_formula f = e
s0: composite_state expression_components
Hs0i: binop_state_proj s0 i =
Some (flatten_formula f1)
l: label (expression_components i)
si: state (expression_components i)
iom, oom: option expression
Hiom: option_valid_message_prop
  (free_composite_vlsm expression_components)
  iom
Hvs0: valid l (si, iom)
Ht: (let (si', om') := transition l (si, iom) in
 (state_update expression_components
    (state_update expression_components s0 i si)
    i si', om')) = (s0, oom)
H0: Iff = binop
∃ f : Formula,
  flatten_formula f =
  Iff :: flatten_formula f1 ++ flatten_formula f2
    -Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
binop: symbol
Hbinop: BinOp binop
i:= symbol_to_index binop: index
f2, f1: Formula
Hind: ∀ y : nat,
  y <
  S
    (length
       (flatten_formula f1 ++
        flatten_formula f2))
  → ∀ e : expression,
      y = length e
      → well_formed_expression e
        → ∃ f : Formula, flatten_formula f = e
s0: composite_state expression_components
Hs0i: binop_state_proj s0 i =
Some (flatten_formula f1)
l: label (expression_components i)
si: state (expression_components i)
iom, oom: option expression
Hiom: option_valid_message_prop
  (free_composite_vlsm expression_components)
  iom
Hvs0: valid l (si, iom)
Ht: (let (si', om') := transition l (si, iom) in
 (state_update expression_components
    (state_update expression_components s0 i si)
    i si', om')) = (s0, oom)
H0: Conj = binop
∃ f : Formula,
  flatten_formula f =
  Conj :: flatten_formula f1 ++ flatten_formula f2 by exists (f1 ∧ f2).
    -Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
binop: symbol
Hbinop: BinOp binop
i:= symbol_to_index binop: index
f2, f1: Formula
Hind: ∀ y : nat,
  y <
  S
    (length
       (flatten_formula f1 ++
        flatten_formula f2))
  → ∀ e : expression,
      y = length e
      → well_formed_expression e
        → ∃ f : Formula, flatten_formula f = e
s0: composite_state expression_components
Hs0i: binop_state_proj s0 i =
Some (flatten_formula f1)
l: label (expression_components i)
si: state (expression_components i)
iom, oom: option expression
Hiom: option_valid_message_prop
  (free_composite_vlsm expression_components)
  iom
Hvs0: valid l (si, iom)
Ht: (let (si', om') := transition l (si, iom) in
 (state_update expression_components
    (state_update expression_components s0 i si)
    i si', om')) = (s0, oom)
H0: Disj = binop
∃ f : Formula,
  flatten_formula f =
  Disj :: flatten_formula f1 ++ flatten_formula f2 by exists (f1 ∨ f2).
    -Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
binop: symbol
Hbinop: BinOp binop
i:= symbol_to_index binop: index
f2, f1: Formula
Hind: ∀ y : nat,
  y <
  S
    (length
       (flatten_formula f1 ++
        flatten_formula f2))
  → ∀ e : expression,
      y = length e
      → well_formed_expression e
        → ∃ f : Formula, flatten_formula f = e
s0: composite_state expression_components
Hs0i: binop_state_proj s0 i =
Some (flatten_formula f1)
l: label (expression_components i)
si: state (expression_components i)
iom, oom: option expression
Hiom: option_valid_message_prop
  (free_composite_vlsm expression_components)
  iom
Hvs0: valid l (si, iom)
Ht: (let (si', om') := transition l (si, iom) in
 (state_update expression_components
    (state_update expression_components s0 i si)
    i si', om')) = (s0, oom)
H0: Impl = binop
∃ f : Formula,
  flatten_formula f =
  Impl :: flatten_formula f1 ++ flatten_formula f2 by exists (f1 → f2).
    -Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
binop: symbol
Hbinop: BinOp binop
i:= symbol_to_index binop: index
f2, f1: Formula
Hind: ∀ y : nat,
  y <
  S
    (length
       (flatten_formula f1 ++
        flatten_formula f2))
  → ∀ e : expression,
      y = length e
      → well_formed_expression e
        → ∃ f : Formula, flatten_formula f = e
s0: composite_state expression_components
Hs0i: binop_state_proj s0 i =
Some (flatten_formula f1)
l: label (expression_components i)
si: state (expression_components i)
iom, oom: option expression
Hiom: option_valid_message_prop
  (free_composite_vlsm expression_components)
  iom
Hvs0: valid l (si, iom)
Ht: (let (si', om') := transition l (si, iom) in
 (state_update expression_components
    (state_update expression_components s0 i si)
    i si', om')) = (s0, oom)
H0: Iff = binop
∃ f : Formula,
  flatten_formula f =
  Iff :: flatten_formula f1 ++ flatten_formula f2 by exists (f1 ↔ f2).
  }Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
binop: symbol
Hbinop: BinOp binop
i:= symbol_to_index binop: index
m, e1: expression
Hind: ∀ y : nat,
  y < S (length (e1 ++ m))
  → ∀ e : expression,
      y = length e
      → well_formed_expression e
        → ∃ f : Formula, flatten_formula f = e
s0: composite_state expression_components
Hs0i: binop_state_proj s0 i = Some e1
l: label (expression_components i)
si: state (expression_components i)
iom, oom: option expression
Hiom: option_valid_message_prop
  (free_composite_vlsm expression_components)
  iom
Hvs0: valid l (si, iom)
Ht: (let (si', om') := transition l (si, iom) in
 (state_update expression_components
    (state_update expression_components s0 i si)
    i si', om')) = (s0, oom)
f2: Formula
Hf2: flatten_formula f2 = m
∃ f1 : Formula, flatten_formula f1 = e1
  eapply Hind; cycle 1; [done | | by rewrite app_length; lia].Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
binop: symbol
Hbinop: BinOp binop
i:= symbol_to_index binop: index
m, e1: expression
Hind: ∀ y : nat,
  y < S (length (e1 ++ m))
  → ∀ e : expression,
      y = length e
      → well_formed_expression e
        → ∃ f : Formula, flatten_formula f = e
s0: composite_state expression_components
Hs0i: binop_state_proj s0 i = Some e1
l: label (expression_components i)
si: state (expression_components i)
iom, oom: option expression
Hiom: option_valid_message_prop
  (free_composite_vlsm expression_components)
  iom
Hvs0: valid l (si, iom)
Ht: (let (si', om') := transition l (si, iom) in
 (state_update expression_components
    (state_update expression_components s0 i si)
    i si', om')) = (s0, oom)
f2: Formula
Hf2: flatten_formula f2 = m
well_formed_expression e1
  destruct (transition l (si, iom)) eqn: Hti; inversion Ht as [Heq]; subst.Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
binop: symbol
Hbinop: BinOp binop
i:= symbol_to_index binop: index
e1: expression
f2: Formula
Hind: ∀ y : nat,
  y < S (length (e1 ++ flatten_formula f2))
  → ∀ e : expression,
      y = length e
      → well_formed_expression e
        → ∃ f : Formula, flatten_formula f = e
s0: composite_state expression_components
Hs0i: binop_state_proj s0 i = Some e1
l: label (expression_components i)
si: state (expression_components i)
iom, oom: option expression
Hiom: option_valid_message_prop
  (free_composite_vlsm expression_components)
  iom
Hvs0: valid l (si, iom)
s: state (expression_components i)
Ht: (state_update expression_components
   (state_update expression_components s0 i si) i
   s, oom) = (s0, oom)
Hti: transition l (si, iom) = (s, oom)
Heq: state_update expression_components
  (state_update expression_components s0 i si) i
  s = s0
well_formed_expression e1
  rewrite <- Heq, state_update_twice in Hs0i.Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
binop: symbol
Hbinop: BinOp binop
i:= symbol_to_index binop: index
e1: expression
f2: Formula
Hind: ∀ y : nat,
  y < S (length (e1 ++ flatten_formula f2))
  → ∀ e : expression,
      y = length e
      → well_formed_expression e
        → ∃ f : Formula, flatten_formula f = e
s0: composite_state expression_components
si, s: state (expression_components i)
Hs0i: binop_state_proj
  (state_update expression_components s0 i s) i =
Some e1
l: label (expression_components i)
iom, oom: option expression
Hiom: option_valid_message_prop
  (free_composite_vlsm expression_components)
  iom
Hvs0: valid l (si, iom)
Ht: (state_update expression_components
   (state_update expression_components s0 i si) i
   s, oom) = (s0, oom)
Hti: transition l (si, iom) = (s, oom)
Heq: state_update expression_components
  (state_update expression_components s0 i si) i
  s = s0
well_formed_expression e1
  by inversion Hbinop; subst binop i; destruct Hvs0 as [im Him]; cbn in *;
    state_update_simpl; subst; (destruct si; [done |]);
    inversion Hti; subst.
Qed.

Any well_formed_expression is the flattening of a Formula.

Theorem well_formed_expression_are_flatten_formulas :
  forall (e : expression), well_formed_expression e ->
    exists (f : Formula), flatten_formula f = e.Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
∀ e : expression,
  well_formed_expression e
  → ∃ f : Formula, flatten_formula f = e
Proof.Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
∀ e : expression,
  well_formed_expression e
  → ∃ f : Formula, flatten_formula f = e
  intros e.Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
e: expression
(well_formed_expression e
 → ∃ f : Formula, flatten_formula f = e)%type
  remember (length e) as n.Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
e: expression
n: nat
Heqn: n = length e
(well_formed_expression e
 → ∃ f : Formula, flatten_formula f = e)%type
  revert e Heqn; induction n as [n Hind] using (well_founded_ind lt_wf).Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
n: nat
Hind: ∀ y : nat,
  y < n
  → ∀ e : expression,
      y = length e
      → well_formed_expression e
        → ∃ f : Formula, flatten_formula f = e
∀ e : expression,
  n = length e
  → well_formed_expression e
    → ∃ f : Formula, flatten_formula f = e
  intros e -> [s He].Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
e: expression
Hind: ∀ y : nat,
  y < length e
  → ∀ e : expression,
      y = length e
      → well_formed_expression e
        → ∃ f : Formula, flatten_formula f = e
s: state expression_vlsm
He: valid_state_message_prop expression_vlsm s
  (Some e)
∃ f : Formula, flatten_formula f = e
  inversion He; subst; [by destruct Hom as ([] & [im Him] & Hom) |].Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
e: expression
Hind: ∀ y : nat,
  y < length e
  → ∀ e : expression,
      y = length e
      → well_formed_expression e
        → ∃ f : Formula, flatten_formula f = e
s: state expression_vlsm
He: valid_state_message_prop expression_vlsm s
  (Some e)
s0: state expression_vlsm
_om: option expression
_s: state expression_vlsm
om: option expression
l: label expression_vlsm
Hps: valid_state_message_prop expression_vlsm s0 _om
Hpm: valid_state_message_prop expression_vlsm _s om
Hv: valid l (s0, om)
Ht: transition l (s0, om) = (s, Some e)
∃ f : Formula, flatten_formula f = e
  destruct l as [i li]; cbn in *.Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
e: expression
Hind: ∀ y : nat,
  y < length e
  → ∀ e : expression,
      y = length e
      → well_formed_expression e
        → ∃ f : Formula, flatten_formula f = e
s: composite_state expression_components
He: valid_state_message_prop expression_vlsm s
  (Some e)
s0: composite_state expression_components
_om: option expression
_s: composite_state expression_components
om: option expression
i: index
li: label (expression_components i)
Hps: valid_state_message_prop expression_vlsm s0 _om
Hpm: valid_state_message_prop expression_vlsm _s om
Hv: valid li (s0 i, om)
Ht: (let (si', om') := transition li (s0 i, om) in
 (state_update expression_components s0 i si',
  om')) = (s, Some e)
∃ f : Formula, flatten_formula f = e
  assert (Hs0 : valid_state_prop expression_vlsm s0) by (eexists; done).Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
e: expression
Hind: ∀ y : nat,
  y < length e
  → ∀ e : expression,
      y = length e
      → well_formed_expression e
        → ∃ f : Formula, flatten_formula f = e
s: composite_state expression_components
He: valid_state_message_prop expression_vlsm s
  (Some e)
s0: composite_state expression_components
_om: option expression
_s: composite_state expression_components
om: option expression
i: index
li: label (expression_components i)
Hps: valid_state_message_prop expression_vlsm s0 _om
Hpm: valid_state_message_prop expression_vlsm _s om
Hv: valid li (s0 i, om)
Ht: (let (si', om') := transition li (s0 i, om) in
 (state_update expression_components s0 i si',
  om')) = (s, Some e)
Hs0: valid_state_prop expression_vlsm s0
∃ f : Formula, flatten_formula f = e
  destruct (transition li (s0 i, om)) as [si' om'] eqn: Hti.Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
e: expression
Hind: ∀ y : nat,
  y < length e
  → ∀ e : expression,
      y = length e
      → well_formed_expression e
        → ∃ f : Formula, flatten_formula f = e
s: composite_state expression_components
He: valid_state_message_prop expression_vlsm s
  (Some e)
s0: composite_state expression_components
_om: option expression
_s: composite_state expression_components
om: option expression
i: index
li: label (expression_components i)
Hps: valid_state_message_prop expression_vlsm s0 _om
Hpm: valid_state_message_prop expression_vlsm _s om
Hv: valid li (s0 i, om)
si': state (expression_components i)
om': option expression
Hti: transition li (s0 i, om) = (si', om')
Ht: (state_update expression_components s0 i si', om') =
(s, Some e)
Hs0: valid_state_prop expression_vlsm s0
∃ f : Formula, flatten_formula f = e
  inversion Ht; subst; clear Ht.Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
e: expression
Hind: ∀ y : nat,
  y < length e
  → ∀ e : expression,
      y = length e
      → well_formed_expression e
        → ∃ f : Formula, flatten_formula f = e
s0: composite_state expression_components
i: index
si': state (expression_components i)
He: valid_state_message_prop expression_vlsm
  (state_update expression_components s0 i si')
  (Some e)
_om: option expression
_s: composite_state expression_components
om: option expression
li: label (expression_components i)
Hps: valid_state_message_prop expression_vlsm s0 _om
Hpm: valid_state_message_prop expression_vlsm _s om
Hv: valid li (s0 i, om)
Hti: transition li (s0 i, om) = (si', Some e)
Hs0: valid_state_prop expression_vlsm s0
∃ f : Formula, flatten_formula f = e
  destruct i.Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
e: expression
Hind: ∀ y : nat,
  y < length e
  → ∀ e : expression,
      y = length e
      → well_formed_expression e
        → ∃ f : Formula, flatten_formula f = e
s0: composite_state expression_components
si': state (expression_components ITop)
He: valid_state_message_prop expression_vlsm
  (state_update expression_components s0 ITop si')
  (Some e)
_om: option expression
_s: composite_state expression_components
om: option expression
li: label (expression_components ITop)
Hps: valid_state_message_prop expression_vlsm s0 _om
Hpm: valid_state_message_prop expression_vlsm _s om
Hv: valid li (s0 ITop, om)
Hti: transition li (s0 ITop, om) = (si', Some e)
Hs0: valid_state_prop expression_vlsm s0
∃ f : Formula, flatten_formula f = e
Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
e: expression
Hind: ∀ y : nat,
  y < length e
  → ∀ e : expression,
      y = length e
      → well_formed_expression e
        → ∃ f : Formula, flatten_formula f = e
s0: composite_state expression_components
si': state (expression_components IBot)
He: valid_state_message_prop expression_vlsm
  (state_update expression_components s0 IBot si')
  (Some e)
_om: option expression
_s: composite_state expression_components
om: option expression
li: label (expression_components IBot)
Hps: valid_state_message_prop expression_vlsm s0 _om
Hpm: valid_state_message_prop expression_vlsm _s om
Hv: valid li (s0 IBot, om)
Hti: transition li (s0 IBot, om) = (si', Some e)
Hs0: valid_state_prop expression_vlsm s0
∃ f : Formula, flatten_formula f = e
Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
e: expression
Hind: ∀ y : nat,
  y < length e
  → ∀ e : expression,
      y = length e
      → well_formed_expression e
        → ∃ f : Formula, flatten_formula f = e
s0: composite_state expression_components
si': state (expression_components IVar)
He: valid_state_message_prop expression_vlsm
  (state_update expression_components s0 IVar si')
  (Some e)
_om: option expression
_s: composite_state expression_components
om: option expression
li: label (expression_components IVar)
Hps: valid_state_message_prop expression_vlsm s0 _om
Hpm: valid_state_message_prop expression_vlsm _s om
Hv: valid li (s0 IVar, om)
Hti: transition li (s0 IVar, om) = (si', Some e)
Hs0: valid_state_prop expression_vlsm s0
∃ f : Formula, flatten_formula f = e
Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
e: expression
Hind: ∀ y : nat,
  y < length e
  → ∀ e : expression,
      y = length e
      → well_formed_expression e
        → ∃ f : Formula, flatten_formula f = e
s0: composite_state expression_components
si': state (expression_components INeg)
He: valid_state_message_prop expression_vlsm
  (state_update expression_components s0 INeg si')
  (Some e)
_om: option expression
_s: composite_state expression_components
om: option expression
li: label (expression_components INeg)
Hps: valid_state_message_prop expression_vlsm s0 _om
Hpm: valid_state_message_prop expression_vlsm _s om
Hv: valid li (s0 INeg, om)
Hti: transition li (s0 INeg, om) = (si', Some e)
Hs0: valid_state_prop expression_vlsm s0
∃ f : Formula, flatten_formula f = e
Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
e: expression
Hind: ∀ y : nat,
  y < length e
  → ∀ e : expression,
      y = length e
      → well_formed_expression e
        → ∃ f : Formula, flatten_formula f = e
s0: composite_state expression_components
si': state (expression_components IConj)
He: valid_state_message_prop expression_vlsm
  (state_update expression_components s0 IConj
     si') (Some e)
_om: option expression
_s: composite_state expression_components
om: option expression
li: label (expression_components IConj)
Hps: valid_state_message_prop expression_vlsm s0 _om
Hpm: valid_state_message_prop expression_vlsm _s om
Hv: valid li (s0 IConj, om)
Hti: transition li (s0 IConj, om) = (si', Some e)
Hs0: valid_state_prop expression_vlsm s0
∃ f : Formula, flatten_formula f = e
Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
e: expression
Hind: ∀ y : nat,
  y < length e
  → ∀ e : expression,
      y = length e
      → well_formed_expression e
        → ∃ f : Formula, flatten_formula f = e
s0: composite_state expression_components
si': state (expression_components IDisj)
He: valid_state_message_prop expression_vlsm
  (state_update expression_components s0 IDisj
     si') (Some e)
_om: option expression
_s: composite_state expression_components
om: option expression
li: label (expression_components IDisj)
Hps: valid_state_message_prop expression_vlsm s0 _om
Hpm: valid_state_message_prop expression_vlsm _s om
Hv: valid li (s0 IDisj, om)
Hti: transition li (s0 IDisj, om) = (si', Some e)
Hs0: valid_state_prop expression_vlsm s0
∃ f : Formula, flatten_formula f = e
Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
e: expression
Hind: ∀ y : nat,
  y < length e
  → ∀ e : expression,
      y = length e
      → well_formed_expression e
        → ∃ f : Formula, flatten_formula f = e
s0: composite_state expression_components
si': state (expression_components IImpl)
He: valid_state_message_prop expression_vlsm
  (state_update expression_components s0 IImpl
     si') (Some e)
_om: option expression
_s: composite_state expression_components
om: option expression
li: label (expression_components IImpl)
Hps: valid_state_message_prop expression_vlsm s0 _om
Hpm: valid_state_message_prop expression_vlsm _s om
Hv: valid li (s0 IImpl, om)
Hti: transition li (s0 IImpl, om) = (si', Some e)
Hs0: valid_state_prop expression_vlsm s0
∃ f : Formula, flatten_formula f = e
Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
e: expression
Hind: ∀ y : nat,
  y < length e
  → ∀ e : expression,
      y = length e
      → well_formed_expression e
        → ∃ f : Formula, flatten_formula f = e
s0: composite_state expression_components
si': state (expression_components IIff)
He: valid_state_message_prop expression_vlsm
  (state_update expression_components s0 IIff si')
  (Some e)
_om: option expression
_s: composite_state expression_components
om: option expression
li: label (expression_components IIff)
Hps: valid_state_message_prop expression_vlsm s0 _om
Hpm: valid_state_message_prop expression_vlsm _s om
Hv: valid li (s0 IIff, om)
Hti: transition li (s0 IIff, om) = (si', Some e)
Hs0: valid_state_prop expression_vlsm s0
∃ f : Formula, flatten_formula f = e
  -Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
e: expression
Hind: ∀ y : nat,
  y < length e
  → ∀ e : expression,
      y = length e
      → well_formed_expression e
        → ∃ f : Formula, flatten_formula f = e
s0: composite_state expression_components
si': state (expression_components ITop)
He: valid_state_message_prop expression_vlsm
  (state_update expression_components s0 ITop si')
  (Some e)
_om: option expression
_s: composite_state expression_components
om: option expression
li: label (expression_components ITop)
Hps: valid_state_message_prop expression_vlsm s0 _om
Hpm: valid_state_message_prop expression_vlsm _s om
Hv: valid li (s0 ITop, om)
Hti: transition li (s0 ITop, om) = (si', Some e)
Hs0: valid_state_prop expression_vlsm s0
∃ f : Formula, flatten_formula f = e by inversion Hti; exists ⊤.
  -Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
e: expression
Hind: ∀ y : nat,
  y < length e
  → ∀ e : expression,
      y = length e
      → well_formed_expression e
        → ∃ f : Formula, flatten_formula f = e
s0: composite_state expression_components
si': state (expression_components IBot)
He: valid_state_message_prop expression_vlsm
  (state_update expression_components s0 IBot si')
  (Some e)
_om: option expression
_s: composite_state expression_components
om: option expression
li: label (expression_components IBot)
Hps: valid_state_message_prop expression_vlsm s0 _om
Hpm: valid_state_message_prop expression_vlsm _s om
Hv: valid li (s0 IBot, om)
Hti: transition li (s0 IBot, om) = (si', Some e)
Hs0: valid_state_prop expression_vlsm s0
∃ f : Formula, flatten_formula f = e by inversion Hti; exists ⊥.
  -Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
e: expression
Hind: ∀ y : nat,
  y < length e
  → ∀ e : expression,
      y = length e
      → well_formed_expression e
        → ∃ f : Formula, flatten_formula f = e
s0: composite_state expression_components
si': state (expression_components IVar)
He: valid_state_message_prop expression_vlsm
  (state_update expression_components s0 IVar si')
  (Some e)
_om: option expression
_s: composite_state expression_components
om: option expression
li: label (expression_components IVar)
Hps: valid_state_message_prop expression_vlsm s0 _om
Hpm: valid_state_message_prop expression_vlsm _s om
Hv: valid li (s0 IVar, om)
Hti: transition li (s0 IVar, om) = (si', Some e)
Hs0: valid_state_prop expression_vlsm s0
∃ f : Formula, flatten_formula f = e by inversion Hti; exists li.
  -Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
e: expression
Hind: ∀ y : nat,
  y < length e
  → ∀ e : expression,
      y = length e
      → well_formed_expression e
        → ∃ f : Formula, flatten_formula f = e
s0: composite_state expression_components
si': state (expression_components INeg)
He: valid_state_message_prop expression_vlsm
  (state_update expression_components s0 INeg si')
  (Some e)
_om: option expression
_s: composite_state expression_components
om: option expression
li: label (expression_components INeg)
Hps: valid_state_message_prop expression_vlsm s0 _om
Hpm: valid_state_message_prop expression_vlsm _s om
Hv: valid li (s0 INeg, om)
Hti: transition li (s0 INeg, om) = (si', Some e)
Hs0: valid_state_prop expression_vlsm s0
∃ f : Formula, flatten_formula f = e destruct om as [m |]; [| done].Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
e: expression
Hind: ∀ y : nat,
  y < length e
  → ∀ e : expression,
      y = length e
      → well_formed_expression e
        → ∃ f : Formula, flatten_formula f = e
s0: composite_state expression_components
si': state (expression_components INeg)
He: valid_state_message_prop expression_vlsm
  (state_update expression_components s0 INeg si')
  (Some e)
_om: option expression
_s: composite_state expression_components
m: expression
li: label (expression_components INeg)
Hps: valid_state_message_prop expression_vlsm s0 _om
Hpm: valid_state_message_prop expression_vlsm _s
  (Some m)
Hv: valid li (s0 INeg, Some m)
Hti: transition li (s0 INeg, Some m) = (si', Some e)
Hs0: valid_state_prop expression_vlsm s0
∃ f : Formula, flatten_formula f = e
    inversion Hti; subst.Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
m: expression
Hind: ∀ y : nat,
  y < length (Neg :: m)
  → ∀ e : expression,
      y = length e
      → well_formed_expression e
        → ∃ f : Formula, flatten_formula f = e
s0: composite_state expression_components
He: valid_state_message_prop expression_vlsm
  (state_update expression_components s0 INeg ())
  (Some (Neg :: m))
_om: option expression
_s: composite_state expression_components
li: label (expression_components INeg)
Hps: valid_state_message_prop expression_vlsm s0 _om
Hpm: valid_state_message_prop expression_vlsm _s
  (Some m)
Hv: valid li (s0 INeg, Some m)
Hti: transition li (s0 INeg, Some m) =
((), Some (Neg :: m))
Hs0: valid_state_prop expression_vlsm s0
∃ f : Formula, flatten_formula f = Neg :: m
    assert (Hm : well_formed_expression m) by (eexists; done).Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
m: expression
Hind: ∀ y : nat,
  y < length (Neg :: m)
  → ∀ e : expression,
      y = length e
      → well_formed_expression e
        → ∃ f : Formula, flatten_formula f = e
s0: composite_state expression_components
He: valid_state_message_prop expression_vlsm
  (state_update expression_components s0 INeg ())
  (Some (Neg :: m))
_om: option expression
_s: composite_state expression_components
li: label (expression_components INeg)
Hps: valid_state_message_prop expression_vlsm s0 _om
Hpm: valid_state_message_prop expression_vlsm _s
  (Some m)
Hv: valid li (s0 INeg, Some m)
Hti: transition li (s0 INeg, Some m) =
((), Some (Neg :: m))
Hs0: valid_state_prop expression_vlsm s0
Hm: well_formed_expression m
∃ f : Formula, flatten_formula f = Neg :: m
    by apply (Hind (length m)) in Hm as [fm <-]; [exists (FNeg fm) | cbn; lia |].
  -Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
e: expression
Hind: ∀ y : nat,
  y < length e
  → ∀ e : expression,
      y = length e
      → well_formed_expression e
        → ∃ f : Formula, flatten_formula f = e
s0: composite_state expression_components
si': state (expression_components IConj)
He: valid_state_message_prop expression_vlsm
  (state_update expression_components s0 IConj
     si') (Some e)
_om: option expression
_s: composite_state expression_components
om: option expression
li: label (expression_components IConj)
Hps: valid_state_message_prop expression_vlsm s0 _om
Hpm: valid_state_message_prop expression_vlsm _s om
Hv: valid li (s0 IConj, om)
Hti: transition li (s0 IConj, om) = (si', Some e)
Hs0: valid_state_prop expression_vlsm s0
∃ f : Formula, flatten_formula f = e by eapply well_formed_is_flatten_formula_helper;
      [constructor | | exists _s | cbn in *; apply Hti | ..].
  -Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
e: expression
Hind: ∀ y : nat,
  y < length e
  → ∀ e : expression,
      y = length e
      → well_formed_expression e
        → ∃ f : Formula, flatten_formula f = e
s0: composite_state expression_components
si': state (expression_components IDisj)
He: valid_state_message_prop expression_vlsm
  (state_update expression_components s0 IDisj
     si') (Some e)
_om: option expression
_s: composite_state expression_components
om: option expression
li: label (expression_components IDisj)
Hps: valid_state_message_prop expression_vlsm s0 _om
Hpm: valid_state_message_prop expression_vlsm _s om
Hv: valid li (s0 IDisj, om)
Hti: transition li (s0 IDisj, om) = (si', Some e)
Hs0: valid_state_prop expression_vlsm s0
∃ f : Formula, flatten_formula f = e by eapply well_formed_is_flatten_formula_helper;
      [constructor | | exists _s | cbn in *; apply Hti | ..].
  -Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
e: expression
Hind: ∀ y : nat,
  y < length e
  → ∀ e : expression,
      y = length e
      → well_formed_expression e
        → ∃ f : Formula, flatten_formula f = e
s0: composite_state expression_components
si': state (expression_components IImpl)
He: valid_state_message_prop expression_vlsm
  (state_update expression_components s0 IImpl
     si') (Some e)
_om: option expression
_s: composite_state expression_components
om: option expression
li: label (expression_components IImpl)
Hps: valid_state_message_prop expression_vlsm s0 _om
Hpm: valid_state_message_prop expression_vlsm _s om
Hv: valid li (s0 IImpl, om)
Hti: transition li (s0 IImpl, om) = (si', Some e)
Hs0: valid_state_prop expression_vlsm s0
∃ f : Formula, flatten_formula f = e by eapply well_formed_is_flatten_formula_helper;
      [constructor | | exists _s | cbn in *; apply Hti | ..].
  -Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
e: expression
Hind: ∀ y : nat,
  y < length e
  → ∀ e : expression,
      y = length e
      → well_formed_expression e
        → ∃ f : Formula, flatten_formula f = e
s0: composite_state expression_components
si': state (expression_components IIff)
He: valid_state_message_prop expression_vlsm
  (state_update expression_components s0 IIff si')
  (Some e)
_om: option expression
_s: composite_state expression_components
om: option expression
li: label (expression_components IIff)
Hps: valid_state_message_prop expression_vlsm s0 _om
Hpm: valid_state_message_prop expression_vlsm _s om
Hv: valid li (s0 IIff, om)
Hti: transition li (s0 IIff, om) = (si', Some e)
Hs0: valid_state_prop expression_vlsm s0
∃ f : Formula, flatten_formula f = e by eapply well_formed_is_flatten_formula_helper;
      [constructor | | exists _s | cbn in *; apply Hti | ..].
Qed.

well_formed_expressions, that is, valid messages of the expression_vlsm coincide with flatten Formulas.

Corollary well_formed_expression_flatten_formula_equiv :
  forall (e : expression), well_formed_expression e <->
  exists (f : Formula), flatten_formula f = e.Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
∀ e : expression,
  well_formed_expression e
  ↔ (∃ f : Formula, flatten_formula f = e)
Proof.Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
∀ e : expression,
  well_formed_expression e
  ↔ (∃ f : Formula, flatten_formula f = e)
  split.Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
e: expression
(well_formed_expression e
 → ∃ f : Formula, flatten_formula f = e)%type
Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
e: expression
((∃ f : Formula, flatten_formula f = e)
 → well_formed_expression e)%type
  -Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
e: expression
(well_formed_expression e
 → ∃ f : Formula, flatten_formula f = e)%type by apply well_formed_expression_are_flatten_formulas.
  -Var: Type
EqDecision0: EqDecision Var
H: base.Infinite Var
e: expression
((∃ f : Formula, flatten_formula f = e)
 → well_formed_expression e)%type by intros [f <-]; apply flatten_formulas_are_well_formed_expressions.
Qed.

End sec_valid_message_char.

Interpretation of formulas

We define a function to interpret formulas as Coq terms in the Prop sort, given that all atoms are mapped to Prop terms.

Section sec_formula_interpretation.

Context
  (formula_var_interp : Var -> Prop).

Fixpoint formula_vars (f : Formula) : listset Var :=
  match f with
  | ⊤ | ⊥ => ∅
  | FVar x => {[x]}
  | ¬ f => formula_vars f
  | f1 ∧ f2 | f1 ∨ f2 | f1 → f2 | f1 ↔ f2 => formula_vars f1 ∪ formula_vars f2
  end.

Fixpoint formula_interp (f : Formula) : Prop :=
  match f with
  | ⊤ => True
  | ⊥ => False
  | FVar x => formula_var_interp x
  | ¬ f => ~ formula_interp f
  | f1 ∧ f2 => formula_interp f1 /\ formula_interp f2
  | f1 ∨ f2 => formula_interp f1 \/ formula_interp f2
  | f1 → f2 => formula_interp f1 -> formula_interp f2
  | f1 ↔ f2 => formula_interp f1 <-> formula_interp f2
  end.

End sec_formula_interpretation.

Definition formula_holds_prop (f : Formula) : Prop :=
  forall (i : Var -> Prop), formula_interp i f.

End sec_formula.

Arguments Formula : clear implicits.

The formula notations we introduced above were local to this module. To allow these notations to be used elsewhere, while also allowing them to be enabled and disabled by need, we declare them as part of a scope.

Declare Scope formula_scope.
Bind Scope formula_scope with Formula.

Notation "⊤" := FTop : formula_scope.
Notation "⊥" := FBot : formula_scope.
Notation "x ∨ y" := (FDisj x y) (at level 85, right associativity) : formula_scope.
Notation "x ∧ y" := (FConj x y) (at level 80, right associativity) : formula_scope.
Notation "x → y" := (FImpl x y) (at level 99, y at level 200, right associativity) : formula_scope.
Notation "x ↔ y" := (FIff x y) (at level 95, no associativity): formula_scope.
Notation "¬ x" := (FNeg x) (at level 75, right associativity) : formula_scope.