Semantics
Standard Semantics
Require Export image functor propositional_formulas modal_formulas
some_neg_form.
Section Semantics.
Variable V : Type.
Variable L : modal_operators.
Variable T : functor.
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 : X → Y)
(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].
∀(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 : X → Y)
(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
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 v ⇒ fun(c : state m) ⇒ coval m c v
| lf_neg f ⇒ set_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).
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.
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.
(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.
Definition state_seq_semantics(LS : lambda_structure)
(m : model)(x : state m)
(s : sequent V L) : Prop :=
some_neg (fun f ⇒ form_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.
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).
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.
Fixpoint propositional_valuation{X : Type}(coval : X → set V)
(f : lambda_formula V L)(prop_f : propositional f) : set X :=
match f return propositional f → set X with
| lf_prop v ⇒ fun _ (c : X) ⇒ coval c v
| lf_neg f ⇒ fun(H : propositional (lf_neg f)) ⇒
set_inverse (propositional_valuation coval f (propositional_neg _ H))
| lf_and f1 f2 ⇒ fun(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 : X → set 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 : X → set 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 : X → set 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 : X → set 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 : X → set 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 : X → set 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.
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.
Definition prop_val_pred{X : Type}(coval : X → set 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 : X → set 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 : X → set 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 : X → set 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 : X → set 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 : X → set 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 : X → set 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 : X → set V)
(s : sequent V L)(prop_s : propositional_sequent s) : Prop :=
is_full_set (simple_prop_seq_val coval s prop_s).
Lemma prop_val_pred_or :
∀(X : Type)(coval : X → set 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 : X → set 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 : X → set 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.
Fixpoint counted_prop_list_valuation{X : Type}(coval : X → set 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_nil ⇒ fun _ ⇒ 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 : X → set 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 : X → set 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 : X → set 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))).
Fixpoint prop_modal_prop_valuation{X : Type}(LS : lambda_structure)
(coval : X → set V)
(f : lambda_formula V L)(propm_f : prop_modal_prop f)
: set (obj T X) :=
match f return prop_modal_prop f → set (obj T X) with
| lf_prop v ⇒ fun(H : prop_modal_prop (lf_prop v)) ⇒
prop_modal_prop_tcc_prop v H
| lf_neg f ⇒ fun(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 f2 ⇒ fun(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 : X → set 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 : X → set 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 : X → set 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 : X → set 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 : X → set 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.
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.
Definition mod_val_pred{X : Type}(LS : lambda_structure)
(coval : X → set 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 : X → set 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 : X → set 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 : X → set 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 : X → set 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 : X → set 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 : X → set 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 : X → set 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 : X → set 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 : X → set 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 : X → set 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).
Lemma mod_val_pred_or :
∀(X : Type)(LS : lambda_structure)(coval : X → set 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 : X → set 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 : X → set 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].