Semantics

Standard Semantics

This module defines lambda structures, models and then three semantics for formulas and sequents. First the normative coalgebraic semantics. The other semantic definitions are only utility constructions. Second, the semantics X,tau |= f for propositional formulas f, and, third, the semantics TX,tau |= f for modal formulas f.
Each semantics comes with a simplified sequent semantics (based on some_neg) and the necessary utility lemmas.

Require Export image functor propositional_formulas modal_formulas
               some_neg_form.

Section Semantics.

  Variable V : Type.
  Variable L : modal_operators.
  Variable T : functor.

Coalgebraic models

LAMBDA structures, page 5
  Definition lambda_structure_type : Type :=
    (op : operator L){X : Type},
      counted_list (set X) (arity L op) → set (obj T X).

  Record lambda_structure : Type := {
    modal_semantics : lambda_structure_type;
    set_equal_modal_semantics :
      (X : Type)(op : operator L)
            (preds_x_1 preds_x_2 : counted_list (set X) (arity L op)),
        ((i : nat)(i_less : i < arity L op),
           set_equal
             (nth (list_of_counted_list preds_x_1) i
                  (less_length_counted_list _ _ preds_x_1 i_less))
             (nth (list_of_counted_list preds_x_2) i
                  (less_length_counted_list _ _ preds_x_2 i_less)))
          →
            set_equal (modal_semantics op X preds_x_1)
                       (modal_semantics op X preds_x_2);
    fibred_semantics :
      (op : operator L)(X Y : Type)(f : XY)
            (preds_y : counted_list (set Y) (arity L op)),
        set_equal
          (modal_semantics op X (counted_map (inv_img f) preds_y))
          (inv_img (fmap T f) (modal_semantics op Y preds_y))
    }.

  Implicit Arguments modal_semantics [X].

T/P(V) coalgebras as models, page 4, 5
  Record model : Type := {
    state : Type;
    coalg : stateobj T state;
    coval : stateset V
  }.

Normative semantics


  Definition form_semantics(LS : lambda_structure)(m : model)
                           (f : lambda_formula V L) : set (state m) :=
    lambda_formula_rec
      (fun(v : V)(c : state m) ⇒ coval m c v)
      set_inverse
      intersection
      (fun(op : operator L)
          (sem_args : counted_list (set (state m)) (arity L op)) ⇒
         inv_img (coalg m) (modal_semantics LS op sem_args))
      f.

  Lemma form_semantics_char :
    (LS : lambda_structure)(m : model)(f : lambda_formula V L),
      form_semantics LS m f = match f with
        | lf_prop vfun(c : state m) ⇒ coval m c v
        | lf_neg fset_inverse (form_semantics LS m f)
        | lf_and f1 f2
            intersection (form_semantics LS m f1) (form_semantics LS m f2)
        | lf_modal op args
            inv_img (coalg m)
                    (modal_semantics LS op
                       (counted_map (form_semantics LS m) args))
    end.

  Lemma form_semantics_false :
    (nonempty_v : V)(LS : lambda_structure)(m : model)(x : state m),
      not (form_semantics LS m (lambda_false nonempty_v) x).

Changing the model for substitutions


  Definition subst_coval(LS : lambda_structure)(m : model)
                           (sigma : lambda_subst V L) : (state m) → set V :=
    fun(x : state m)(v : V) ⇒
      form_semantics LS m (sigma v) x.

  Definition modal_subst_coval(LS : lambda_structure)(m : model)
                                         (sigma : lambda_subst V L) : model :=
    {| state := state m;
       coalg := coalg m;
       coval := subst_coval LS m sigma
    |}.

  Lemma set_equal_form_semantics_subst_change_coval :
    (LS : lambda_structure)(m : model)
          (sigma : lambda_subst V L)(f : lambda_formula V L),
      set_equal
        (form_semantics LS m (subst_form sigma f))
        (form_semantics LS (modal_subst_coval LS m sigma) f).

  Lemma form_semantics_subst_change_coval :
    (LS : lambda_structure)(m : model)(x : state m)
          (sigma : lambda_subst V L)(f : lambda_formula V L),
      form_semantics LS m (subst_form sigma f) x
        form_semantics LS (modal_subst_coval LS m sigma) f x.

Sequent semantics and validity


  Definition seq_semantics(nonempty_v : V)(LS : lambda_structure)
                          (m : model)(s : sequent V L) : set (state m) :=
    form_semantics LS m (or_formula_of_sequent s nonempty_v).

M |= A, page 7
  Definition valid_all_states(nonempty_v : V)(LS : lambda_structure)
                             (m : model)(s : sequent V L) : Prop :=
    is_full_set (seq_semantics nonempty_v LS m s).

  Lemma valid_all_states_subst_change_coval :
    (nonempty_v : V)(LS : lambda_structure)(m : model)
          (sigma : lambda_subst V L)(s : sequent V L),
      (valid_all_states nonempty_v LS m (subst_sequent sigma s)
        valid_all_states nonempty_v LS (modal_subst_coval LS m sigma) s).

  Definition valid_all_models(nonempty_v : V)(LS : lambda_structure)
                             (s : sequent V L) : Prop :=
    (m : model), valid_all_states nonempty_v LS m s.

Simplified sequence semantics


  Definition state_seq_semantics(LS : lambda_structure)
                                (m : model)(x : state m)
                                (s : sequent V L) : Prop :=
    some_neg (fun fform_semantics LS m f x) s.

  Lemma state_seq_semantics_singleton :
    (LS : lambda_structure)(m : model)(x : state m)
          (f : lambda_formula V L),
      state_seq_semantics LS m x [f] form_semantics LS m f x.

  Lemma state_seq_semantics_nth_intro :
    (LS : lambda_structure)(m : model)(x : state m)
          (s : sequent V L)(n : nat)(n_less : n < length s),
      form_semantics LS m (nth s n n_less) x
        state_seq_semantics LS m x s.

  Lemma state_seq_semantics_cons_case_elim :
    (LS : lambda_structure)(m : model)(x : state m)
          (f : lambda_formula V L)(s : sequent V L),
      state_seq_semantics LS m x (f :: s) →
        (s = [] form_semantics LS m f x)
        (s [] ~(~form_semantics LS m f x
                      ¬state_seq_semantics LS m x s)).

  Lemma state_seq_semantics_length_case_intro :
    (LS : lambda_structure)(m : model)(x : state m)(s : sequent V L),
      ((s_len : length s = 1),
         form_semantics LS m (nth s 0 (nth_head_tcc s s_len)) x) →
      (length s 1 → ~~state_seq_semantics LS m x s) →
        state_seq_semantics LS m x s.

  Lemma state_seq_semantics_append :
    (LS : lambda_structure)(m : model)(x : state m)
          (s1 s2 : sequent V L),
      state_seq_semantics LS m x (s1 ++ s2) →
        ¬ ( ¬ (state_seq_semantics LS m x s1)
            ¬ (state_seq_semantics LS m x s2)).

  Lemma state_seq_semantics_append_right :
    (LS : lambda_structure)(m : model)(x : state m)
          (s1 s2 : sequent V L),
      state_seq_semantics LS m x s1
        state_seq_semantics LS m x (s1 ++ s2).

  Lemma state_seq_semantics_append_left :
    (LS : lambda_structure)(m : model)(x : state m)
          (s1 s2 : sequent V L),
      state_seq_semantics LS m x s2
        state_seq_semantics LS m x (s1 ++ s2).

  Lemma state_seq_semantics_reorder :
    (LS : lambda_structure)(m : model)(x : state m)
          (s1 s2 : sequent V L),
      list_reorder s1 s2
      state_seq_semantics LS m x s1
        state_seq_semantics LS m x s2.

Equivalence for simplified semantics


  Lemma state_seq_semantics_correct :
    (nonempty_v : V)(LS : lambda_structure)(m : model)(x : state m)
          (s : sequent V L),
      state_seq_semantics LS m x s seq_semantics nonempty_v LS m s x.

  Lemma state_seq_semantics_valid :
    (nonempty_v : V)(LS : lambda_structure)(m : model)(s : sequent V L),
      valid_all_states nonempty_v LS m s
        ((x : state m), state_seq_semantics LS m x s).

Standard semantic lemma (derived via simplified semantics)


  Lemma valid_all_states_append_right :
    (nonempty_v : V)(LS : lambda_structure)(m : model)
          (s1 s2 : sequent V L),
      valid_all_states nonempty_v LS m s1
        valid_all_states nonempty_v LS m (s1 ++ s2).

  Lemma valid_all_states_reorder :
    (nonempty_v : V)(LS : lambda_structure)(m : model)
          (s1 s2 : sequent V L),
      list_reorder s1 s2
      valid_all_states nonempty_v LS m s1
        valid_all_states nonempty_v LS m s2.

Semantics X,tau |= f for propositional f


  Fixpoint propositional_valuation{X : Type}(coval : Xset V)
                 (f : lambda_formula V L)(prop_f : propositional f) : set X :=
    match f return propositional fset X with
      | lf_prop vfun _ (c : X) ⇒ coval c v
      | lf_neg ffun(H : propositional (lf_neg f)) ⇒
          set_inverse (propositional_valuation coval f (propositional_neg _ H))
      | lf_and f1 f2fun(H : propositional (lf_and f1 f2)) ⇒
          intersection
            (propositional_valuation coval f1 (propositional_and_left _ _ H))
            (propositional_valuation coval f2 (propositional_and_right _ _ H))
      | lf_modal op args
          fun(H : propositional (lf_modal op args)) ⇒
            propositional_tcc_modal op args H
    end prop_f.

  Lemma propositional_valuation_tcc_irr :
    (X : Type)(coval : Xset V)(f : lambda_formula V L)
          (prop_f_1 prop_f_2 : propositional f),
      propositional_valuation coval f prop_f_1 =
        propositional_valuation coval f prop_f_2.

  Lemma propositional_valuation_false :
    (X : Type)(coval : Xset V)(v : V)
          (prop_false : propositional (lambda_false v))(x : X),
      not (propositional_valuation coval (lambda_false v) prop_false x).

  Definition prop_seq_val{X : Type}(nonempty_v : V)(coval : Xset V)
                (s : sequent V L)(prop_s : propositional_sequent s) : set X :=
    propositional_valuation coval
      (or_formula_of_sequent s nonempty_v)
      (propositional_or_formula nonempty_v s prop_s).

  Lemma prop_seq_val_tcc_irr :
    (X : Type)(nonempty_v : V)(coval : Xset V)(s : sequent V L)
          (prop_s_1 prop_s_2 : propositional_sequent s),
      prop_seq_val nonempty_v coval s prop_s_1 =
        prop_seq_val nonempty_v coval s prop_s_2.

  Definition prop_seq_val_valid{X : Type}(nonempty_v : V)(coval : Xset V)
                  (s : sequent V L)(prop_s : propositional_sequent s) : Prop :=
    is_full_set (prop_seq_val nonempty_v coval s prop_s).

  Lemma prop_seq_val_valid_tcc_irr :
    (X : Type)(nonempty_v : V)(coval : Xset V)(s : sequent V L)
          (prop_s_1 prop_s_2 : propositional_sequent s),
      prop_seq_val_valid nonempty_v coval s prop_s_1
        prop_seq_val_valid nonempty_v coval s prop_s_2.

Equivalence of standard semantics with X,tau |= f


  Lemma prop_val_semantics :
    (LS : lambda_structure)(m : model)
          (f : lambda_formula V L)(prop_f : propositional f),
      set_equal (form_semantics LS m f)
                (propositional_valuation (coval m) f prop_f).

  Lemma prop_val_semantics_valid :
    (nonempty_v : V)(LS : lambda_structure)(m : model)(s : sequent V L)
          (prop_s : propositional_sequent s),
      valid_all_states nonempty_v LS m s
        prop_seq_val_valid nonempty_v (coval m) s prop_s.

Simplified X,tau |= f sequent semantics


  Definition prop_val_pred{X : Type}(coval : Xset V)(x : X)
                  (f : lambda_formula V L)(prop_f : propositional f) : Prop :=
    propositional_valuation coval f prop_f x.

  Lemma prop_val_pred_tcc_irr :
    (X : Type)(coval : Xset V)(x : X)(f : lambda_formula V L)
          (prop_f_1 prop_f_2 : propositional f),
      prop_val_pred coval x f prop_f_1
        prop_val_pred coval x f prop_f_2.

  Definition simple_prop_seq_val{X : Type}(coval : Xset V)
          (s : sequent V L)(prop_s : propositional_sequent s)(x : X) : Prop :=
    some_neg_dep propositional (prop_val_pred coval x) s prop_s.

  Lemma simple_prop_seq_val_tcc_irr :
    (X : Type)(coval : Xset V)(x : X)
          (s : sequent V L)(prop_s_1 prop_s_2 : propositional_sequent s),
      simple_prop_seq_val coval s prop_s_1 x
        simple_prop_seq_val coval s prop_s_2 x.

  Lemma simple_prop_seq_val_head :
    (X : Type)(coval : Xset V)(x : X)
          (f : lambda_formula V L)(s : sequent V L)
          (prop_fs : propositional_sequent (f :: s)),
      propositional_valuation coval f
           (propositional_sequent_head _ _ prop_fs) x
        simple_prop_seq_val coval (f :: s) prop_fs x.

  Lemma simple_prop_seq_val_tail :
    (X : Type)(coval : Xset V)(x : X)
          (f : lambda_formula V L)(s : sequent V L)
          (prop_fs : propositional_sequent (f :: s)),
      simple_prop_seq_val coval s (propositional_sequent_tail _ _ prop_fs) x
        simple_prop_seq_val coval (f :: s) prop_fs x.

  Lemma simple_prop_seq_val_length_case_intro :
    (X : Type)(coval : Xset V)(x : X)(s : sequent V L)
          (prop_s : propositional_sequent s),
      length s 1 →
      ~~simple_prop_seq_val coval s prop_s x
        simple_prop_seq_val coval s prop_s x.

  Definition simple_prop_seq_val_valid{X : Type}(coval : Xset V)
          (s : sequent V L)(prop_s : propositional_sequent s) : Prop :=
    is_full_set (simple_prop_seq_val coval s prop_s).

Equivalence for simplified X,tau |= f sequent semantics


  Lemma prop_val_pred_or :
   (X : Type)(coval : Xset V)(x : X)(f1 f2 : lambda_formula V L)
         (prop_f1 : propositional f1)(prop_f2 : propositional f2),
     prop_val_pred coval x (lambda_or f1 f2)
                     (propositional_lambda_or _ _ prop_f1 prop_f2)
        
     ~(~prop_val_pred coval x f1 prop_f1 ¬prop_val_pred coval x f2 prop_f2).

  Lemma simple_prop_seq_val_valid_correct :
    (nonempty_v : V)(X : Type)(coval : Xset V)(s : sequent V L)
          (prop_s : propositional_sequent s),
      prop_seq_val_valid nonempty_v coval s prop_s
         simple_prop_seq_val_valid coval s prop_s.

  Lemma prop_seq_val_valid_reorder :
    (nonempty_v : V)(X : Type)(coval : Xset V)(s1 s2 : sequent V L)
          (prop_s1 : propositional_sequent s1)
          (prop_s2 : propositional_sequent s2),
      list_reorder s1 s2
      prop_seq_val_valid nonempty_v coval s1 prop_s1
        prop_seq_val_valid nonempty_v coval s2 prop_s2.

Semantics TX,tau |= f for counted modal arguments


  Fixpoint counted_prop_list_valuation{X : Type}(coval : Xset V)(n : nat)
                   (fl : counted_list (lambda_formula V L) n)
                   (fl_prop : every_nth prop_form
                                        (list_of_counted_list fl))
                    : counted_list (set X) n :=
    match fl in counted_list _ n
      return every_nth prop_form (list_of_counted_list fl) →
                                                       counted_list (set X) n
    with
      | counted_nilfun _counted_nil
      | counted_cons n f fl
          fun(H : every_nth prop_form (f :: list_of_counted_list fl)) ⇒
            counted_cons
              (fun(x : X) ⇒ coval x (prop_form_acc f (every_nth_head _ _ _ H)))
              (counted_prop_list_valuation coval n fl (every_nth_tail _ _ _ H))
    end fl_prop.

  Lemma counted_prop_list_valuation_tcc_irr :
    (X : Type)(coval : Xset V)(n : nat)
          (fl : counted_list (lambda_formula V L) n)
          (fl_prop_1 fl_prop_2 : every_nth prop_form (list_of_counted_list fl)),
      counted_prop_list_valuation coval n fl fl_prop_1 =
        counted_prop_list_valuation coval n fl fl_prop_2.

  Lemma counted_prop_list_valuation_semantics :
    (LS : lambda_structure)(m : model)(n : nat)
          (fl : counted_list (lambda_formula V L) n)
          (fl_prop : every_nth prop_form (list_of_counted_list fl)),
      counted_map (form_semantics LS m) fl =
        counted_prop_list_valuation (coval m) n fl fl_prop.

  Lemma nth_counted_prop_list_valuation_tcc :
    (X : Type)(coval : Xset V)(n : nat)
          (fl : counted_list (lambda_formula V L) n)
          (fl_prop : every_nth prop_form (list_of_counted_list fl))
          (i : nat),
      i < length (list_of_counted_list
                    (counted_prop_list_valuation coval n fl fl_prop))
      → i < length (list_of_counted_list fl).

  Lemma nth_counted_prop_list_valuation :
    (X : Type)(coval : Xset V)(n : nat)
          (fl : counted_list (lambda_formula V L) n)
          (fl_prop : every_nth prop_form (list_of_counted_list fl))
          (i : nat)
          (i_less : i < length (list_of_counted_list
                    (counted_prop_list_valuation coval n fl fl_prop)))
          (x : X),
      nth (list_of_counted_list
               (counted_prop_list_valuation coval n fl fl_prop))
        i i_less x
      = coval x
          (prop_form_acc
            (nth (list_of_counted_list fl) i
               (nth_counted_prop_list_valuation_tcc _ _ _ _ _ _ i_less))
            (fl_prop i
               (nth_counted_prop_list_valuation_tcc _ _ _ _ _ _ i_less))).

Semantics TX,tau |= f for modal formulas f


  Fixpoint prop_modal_prop_valuation{X : Type}(LS : lambda_structure)
           (coval : Xset V)
           (f : lambda_formula V L)(propm_f : prop_modal_prop f)
                                                           : set (obj T X) :=
    match f return prop_modal_prop fset (obj T X) with
      | lf_prop vfun(H : prop_modal_prop (lf_prop v)) ⇒
          prop_modal_prop_tcc_prop v H
      | lf_neg ffun(H : prop_modal_prop (lf_neg f)) ⇒
          set_inverse (prop_modal_prop_valuation LS coval f
                                             (prop_modal_prop_tcc_neg f H))
      | lf_and f1 f2fun(H : prop_modal_prop (lf_and f1 f2)) ⇒
          intersection
            (prop_modal_prop_valuation LS coval f1
                  (prop_modal_prop_tcc_and_1 f1 f2 H))
            (prop_modal_prop_valuation LS coval f2
                  (prop_modal_prop_tcc_and_2 f1 f2 H))
      | lf_modal op args
          fun(H : prop_modal_prop (lf_modal op args)) ⇒
            modal_semantics LS op
              (counted_prop_list_valuation coval (arity L op) args
                 (prop_modal_prop_tcc_modal op args H))
    end propm_f.

  Lemma prop_modal_prop_valuation_tcc_irr :
    (X : Type)(LS : lambda_structure)(coval : Xset V)
          (f : lambda_formula V L)(propm_f_1 propm_f_2 : prop_modal_prop f),
      prop_modal_prop_valuation LS coval f propm_f_1 =
        prop_modal_prop_valuation LS coval f propm_f_2.

  Definition mod_seq_val{X : Type}(LS : lambda_structure)(coval : Xset V)
                        (s : sequent V L)(nonempty_s : s [])
                      (propm_s : prop_modal_prop_sequent s) : set (obj T X) :=
    prop_modal_prop_valuation LS coval
      (or_formula_of_ne_sequent s nonempty_s)
      (prop_modal_prop_or_formula s nonempty_s propm_s).

  Lemma mod_seq_val_tcc_irr :
    (X : Type)(LS : lambda_structure)(coval : Xset V)
          (s : sequent V L)(nonempty_s_1 nonempty_s_2 : s [])
          (propm_s_1 propm_s_2 : prop_modal_prop_sequent s),
      mod_seq_val LS coval s nonempty_s_1 propm_s_1 =
        mod_seq_val LS coval s nonempty_s_2 propm_s_2.

  Definition mod_seq_val_valid{X : Type}(LS : lambda_structure)
                              (coval : Xset V)
                              (s : sequent V L)(nonempty_s : s [])
                              (propm_s : prop_modal_prop_sequent s) : Prop :=
    is_full_set (mod_seq_val LS coval s nonempty_s propm_s).

  Lemma mod_seq_val_valid_tcc_irr :
    (X : Type)(LS : lambda_structure)(coval : Xset V)
          (s : sequent V L)(nonempty_s_1 nonempty_s_2 : s [])
          (propm_s_1 propm_s_2 : prop_modal_prop_sequent s),
      mod_seq_val_valid LS coval s nonempty_s_1 propm_s_1
        mod_seq_val_valid LS coval s nonempty_s_2 propm_s_2.

Equivalence of standard semantics with TX,tau |= f


  Lemma prop_modal_prop_semantics :
    (LS : lambda_structure)(m : model)
          (f : lambda_formula V L)(propm_f : prop_modal_prop f),
      set_equal (form_semantics LS m f)
                 (inv_img (coalg m)
                           (prop_modal_prop_valuation LS (coval m) f propm_f)).

  Lemma mod_val_semantics_valid :
    (nonempty_v : V)(LS : lambda_structure)(m : model)(s : sequent V L)
          (nonempty_s : s [])(propm_s : prop_modal_prop_sequent s),
      mod_seq_val_valid LS (coval m) s nonempty_s propm_s
        valid_all_states nonempty_v LS m s.

Simplified TX,tau |= f sequent semantics


  Definition mod_val_pred{X : Type}(LS : lambda_structure)
             (coval : Xset V)(x : obj T X)
             (f : lambda_formula V L)(propm_f : prop_modal_prop f) : Prop :=
    prop_modal_prop_valuation LS coval f propm_f x.

  Lemma mod_val_pred_tcc_irr :
    (X : Type)(LS : lambda_structure)(coval : Xset V)
          (x : obj T X)(f : lambda_formula V L)
          (propm_f_1 propm_f_2 : prop_modal_prop f),
      mod_val_pred LS coval x f propm_f_1
        mod_val_pred LS coval x f propm_f_2.

  Definition simple_mod_seq_val{X : Type}(LS : lambda_structure)
             (coval : Xset V)(s : sequent V L)
             (propm_s : prop_modal_prop_sequent s)(x : obj T X) : Prop :=
    some_neg_dep prop_modal_prop (mod_val_pred LS coval x) s propm_s.

  Lemma simple_mod_seq_val_tcc_irr :
    (X : Type)(LS : lambda_structure)(coval : Xset V)(x : obj T X)
          (s : sequent V L)(propm_s_1 propm_s_2 : prop_modal_prop_sequent s),
      simple_mod_seq_val LS coval s propm_s_1 x
        simple_mod_seq_val LS coval s propm_s_2 x.

  Lemma simple_mod_seq_val_nth_intro :
    (X : Type)(LS : lambda_structure)(coval : Xset V)(x : obj T X)
          (s : sequent V L)(propm_s : prop_modal_prop_sequent s)
          (n : nat)(n_less : n < length s),
      prop_modal_prop_valuation LS coval
                                (nth s n n_less) (propm_s n n_less) x
        simple_mod_seq_val LS coval s propm_s x.

  Lemma simple_mod_seq_val_head :
    (X : Type)(LS : lambda_structure)(coval : Xset V)(x : obj T X)
          (f : lambda_formula V L)(s : sequent V L)
          (propm_fs : prop_modal_prop_sequent (f :: s)),
      prop_modal_prop_valuation LS coval f
           (prop_modal_prop_sequent_head _ _ propm_fs) x
        simple_mod_seq_val LS coval (f :: s) propm_fs x.

  Lemma simple_mod_seq_val_tail :
    (X : Type)(LS : lambda_structure)(coval : Xset V)(x : obj T X)
          (f : lambda_formula V L)(s : sequent V L)
          (propm_fs : prop_modal_prop_sequent (f :: s)),
      simple_mod_seq_val LS coval s
                 (prop_modal_prop_sequent_tail _ _ propm_fs) x
        simple_mod_seq_val LS coval (f :: s) propm_fs x.

  Lemma simple_mod_seq_val_append_left :
    (X : Type)(LS : lambda_structure)(coval : Xset V)(x : obj T X)
          (s1 s2 : sequent V L)
          (prop_s12 : prop_modal_prop_sequent (s1 ++ s2)),
      simple_mod_seq_val LS coval s2
                 (prop_modal_prop_sequent_append_right _ _ prop_s12) x
        simple_mod_seq_val LS coval (s1 ++ s2) prop_s12 x.

  Lemma simple_mod_seq_val_append_right :
    (X : Type)(LS : lambda_structure)(coval : Xset V)(x : obj T X)
          (s1 s2 : sequent V L)
          (prop_s12 : prop_modal_prop_sequent (s1 ++ s2)),
      simple_mod_seq_val LS coval s1
                 (prop_modal_prop_sequent_append_left _ _ prop_s12) x
        simple_mod_seq_val LS coval (s1 ++ s2) prop_s12 x.

  Lemma simple_mod_seq_val_length_case_intro :
    (X : Type)(LS : lambda_structure)(coval : Xset V)
          (x : obj T X)(s : sequent V L)(propm_s : prop_modal_prop_sequent s),
      length s 1 →
      ~~simple_mod_seq_val LS coval s propm_s x
        simple_mod_seq_val LS coval s propm_s x.

  Definition simple_mod_seq_val_valid{X : Type}(LS : lambda_structure)
             (coval : Xset V)(s : sequent V L)
             (propm_s : prop_modal_prop_sequent s) : Prop :=
    is_full_set (simple_mod_seq_val LS coval s propm_s).

Equivalence for simplified TX,tau |= f sequent semantics


  Lemma mod_val_pred_or :
   (X : Type)(LS : lambda_structure)(coval : Xset V)
         (x : obj T X)(f1 f2 : lambda_formula V L)
         (propm_f1 : prop_modal_prop f1)(propm_f2 : prop_modal_prop f2),
     mod_val_pred LS coval x (lambda_or f1 f2)
                     (prop_modal_prop_lambda_or _ _ propm_f1 propm_f2)
        
     ~(~mod_val_pred LS coval x f1 propm_f1
       ¬mod_val_pred LS coval x f2 propm_f2).

  Lemma simple_mod_seq_val_valid_correct :
    (X : Type)(LS : lambda_structure)
          (coval : Xset V)(s : sequent V L)(nonempty_s : s [])
          (propm_s : prop_modal_prop_sequent s),
      mod_seq_val_valid LS coval s nonempty_s propm_s
         simple_mod_seq_val_valid LS coval s propm_s.

  Lemma mod_seq_val_valid_reorder :
    (X : Type)(LS : lambda_structure)(coval : Xset V)
          (s1 s2 : sequent V L)
          (nonempty_s1 : s1 [])(nonempty_s2 : s2 [])
          (propm_s1 : prop_modal_prop_sequent s1)
          (propm_s2 : prop_modal_prop_sequent s2),
      list_reorder s1 s2
      mod_seq_val_valid LS coval s1 nonempty_s1 propm_s1
        mod_seq_val_valid LS coval s2 nonempty_s2 propm_s2.

End Semantics.

Implicit Arguments modal_semantics [L T X].
Implicit Arguments set_equal_modal_semantics [L T].
Implicit Arguments fibred_semantics [L T].
Implicit Arguments state [V T].
Implicit Arguments coalg [V T].
Implicit Arguments coval [V T].
Implicit Arguments form_semantics [V L T].
Implicit Arguments valid_all_states [V L T].
Implicit Arguments valid_all_models [V L T].
Implicit Arguments state_seq_semantics [V L T].
Implicit Arguments state_seq_semantics_append [V L T].
Implicit Arguments propositional_valuation [V L X].
Implicit Arguments prop_seq_val_valid [V L X].
Implicit Arguments simple_prop_seq_val [V L X].
Implicit Arguments simple_prop_seq_val_tail [V L X].
Implicit Arguments prop_modal_prop_valuation [V L T X].
Implicit Arguments prop_modal_prop_semantics [V L T].
Implicit Arguments mod_seq_val_valid [V L T X].
Implicit Arguments simple_mod_seq_val [V L T X].
Implicit Arguments simple_mod_seq_val_valid [V L T X].
Implicit Arguments simple_mod_seq_val_append_left [V L T X].
Implicit Arguments simple_mod_seq_val_append_right [V L T X].