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 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').

  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.