K example, semantics, 4.6
Require Export some_nth k_syntax semantics.
Section K_sementics.
Hypothesis pred_ext : ∀(A : Type)(P Q : A → Prop),
(∀(a : A), P a ↔ Q a) → P = Q.
Definition k_functor : functor.
Lemma non_trivial_k_functor : non_trivial_functor k_functor.
Definition k_lifting : lambda_structure_type KL k_functor :=
fun(op : k_operator)(X : Type)(arg : counted_list (set X) 1)
(P : set X) ⇒
subset P (counted_head arg).
Definition k_lambda : lambda_structure KL k_functor.
Lemma non_trivial_k_functor : non_trivial_functor k_functor.
Definition k_lifting : lambda_structure_type KL k_functor :=
fun(op : k_operator)(X : Type)(arg : counted_list (set X) 1)
(P : set X) ⇒
subset P (counted_head arg).
Definition k_lambda : lambda_structure KL k_functor.
Prove the semantics of box, as test for the semantics
Lemma box_semantics :
∀(f : lambda_formula KV KL)(m : model KV k_functor)(x : state m),
form_semantics k_lambda m (box f) x ↔
(∀(x' : state m), coalg m x x' →
form_semantics k_lambda m f x').
∀(f : lambda_formula KV KL)(m : model KV k_functor)(x : state m),
form_semantics k_lambda m (box f) x ↔
(∀(x' : state m), coalg m x x' →
form_semantics k_lambda m f x').
Lemma simple_prop_seq_val_k_assumption_head :
∀(X : Type)(coval : X → set KV)(x : X)(n : nat),
coval x 0 →
simple_prop_seq_val coval (k_assumption n)
(propositional_sequent_k_assumption n) x.
Lemma prop_seq_valid_k_assumption_0 :
∀(X : Type)(coval : X → set KV),
prop_seq_val_valid 0 coval (k_assumption 0)
(propositional_sequent_k_assumption 0)
↔
∀(x : X), coval x 0.
Lemma prop_seq_valid_renamed_k_assumption_0 :
∀(X : Type)(coval : X → set KV)(f : KV → KV)
(prop_subst_ass : propositional_sequent
(subst_sequent (rename_of_fun f) (k_assumption 0))),
prop_seq_val_valid 0 coval
(subst_sequent (rename_of_fun f) (k_assumption 0))
prop_subst_ass
↔
∀(x : X), coval x (f 0).
Lemma subst_sequent_renamed_k_assumption :
∀(f : KV → KV)(n : nat),
subst_sequent (rename_of_fun f) (k_assumption n) =
(lf_prop (f 0)) :: map neg_v (map f (seq 1 n)).
Lemma neg_v_sequent_double_neg_semantics :
∀(X : Type)(coval : X → set KV)(vl : list KV)(x : X)
(prop_subst_ass : propositional_sequent (map neg_v vl)),
¬every_nth (coval x) vl →
~~simple_prop_seq_val coval (map neg_v vl) prop_subst_ass x.
Lemma prop_seq_valid_renamed_k_assumption_Sn :
∀(X : Type)(coval : X → set KV)(f : KV → KV)(n : nat)
(prop_subst_ass : propositional_sequent
(subst_sequent (rename_of_fun f) (k_assumption (S n)))),
prop_seq_val_valid 0 coval
(subst_sequent (rename_of_fun f) (k_assumption (S n)))
prop_subst_ass
↔
∀(x : X),
~~(every_nth (coval x) (map f (seq 1 (S n))) → coval x (f 0)).
Lemma prop_seq_valid_k_assumption_Sn :
∀(X : Type)(coval : X → set KV)(n : nat),
prop_seq_val_valid 0 coval (k_assumption (S n))
(propositional_sequent_k_assumption (S n))
↔
∀(x : X),
~~(every_nth (coval x) (seq 1 (S n)) → coval x 0).
Lemma neg_box_v_sequent_semantics_char :
∀(X : Type)(coval : X → set KV)(P : set X)(vl : list KV)
(vl_prop : prop_modal_prop_sequent (map neg_box_v vl)),
¬every_nth (fun v ⇒ subset P (fun x ⇒ coval x v)) vl →
~~simple_mod_seq_val k_lambda coval (map neg_box_v vl) vl_prop P.
Lemma box_v_sequent_semantics_char :
∀(X : Type)(coval : X → set KV)(P : set X)(vl : list KV)
(vl_prop : prop_modal_prop_sequent (map box_v vl)),
some_nth (fun v ⇒ subset P (fun x ⇒ coval x v)) vl →
simple_mod_seq_val k_lambda coval (map box_v vl) vl_prop P.
Lemma short_mod_seq_valid_char :
∀(X : Type)(coval : X → set KV)(mods negs : sequent KV KL)
(mv nv : list KV)(mod_neg_nonempty : mods ++ negs ≠ [])
(mod_neg_prop : prop_modal_prop_sequent (mods ++ negs)),
length (mods ++ negs) = 1 →
mods = map box_v mv →
negs = map neg_box_v nv →
(mod_seq_val_valid k_lambda coval (mods ++ negs)
mod_neg_nonempty mod_neg_prop
↔
nv = [] ∧
∃(v : KV), mv = [v] ∧
∀(P : set X), subset P (fun x ⇒ coval x v)).
Lemma mod_seq_valid_k_conclusion_0 :
∀(X : Type)(coval : X → set KV),
mod_seq_val_valid k_lambda coval (k_conclusion 0)
(k_conclusion_nonempty 0)
(prop_modal_prop_sequent_k_conclusion 0)
↔
∀(P : set X), subset P (fun x ⇒ coval x 0).
Lemma long_mod_seq_valid_char :
∀(X : Type)(coval : X → set KV)(mods negs : sequent KV KL)
(mv nv : list KV)(mod_neg_nonempty : mods ++ negs ≠ [])
(mod_neg_prop : prop_modal_prop_sequent (mods ++ negs)),
length (mods ++ negs) ≠ 1 →
mods = map box_v mv →
negs = map neg_box_v nv →
(mod_seq_val_valid k_lambda coval (mods ++ negs)
mod_neg_nonempty mod_neg_prop
↔
∀(P : set X),
~~(every_nth (fun v ⇒ subset P (fun x ⇒ coval x v)) nv
→ some_nth (fun v ⇒ subset P (fun x ⇒ coval x v)) mv)).
Lemma mod_seq_valid_k_conclusion_Sn :
∀(X : Type)(coval : X → set KV)(n : nat),
mod_seq_val_valid k_lambda coval (k_conclusion (S n))
(k_conclusion_nonempty (S n))
(prop_modal_prop_sequent_k_conclusion (S n))
↔
∀(P : set X),
~~(every_nth (fun v ⇒ subset P (fun x ⇒ coval x v))
(seq 1 (S n))
→ subset P (fun x ⇒ coval x 0)).
End K_sementics.