Require Export some_neg_form propositional_rules.

Section Propositional_models.

  Variable V : Type.
  Variable L : modal_operators.

  Definition prop_model : Type := set V.

  Fixpoint is_prop_model(m : prop_model)(f : lambda_formula V L)
                              (prop_f : propositional f) : Prop :=
    match f return propositional f → Prop with
      | lf_prop v ⇒ fun _ ⇒ m v
      | lf_neg f1 ⇒ fun(H : propositional (lf_neg f1)) ⇒
          not (is_prop_model m f1 (propositional_neg f1 H))
      | lf_and f1 f2 ⇒ fun(H : propositional (lf_and f1 f2)) ⇒
          is_prop_model m f1 (propositional_and_left f1 f2 H) ∧
          is_prop_model m f2 (propositional_and_right f1 f2 H)
      | lf_modal op args ⇒ fun(H : propositional (lf_modal op args)) ⇒
          propositional_tcc_modal op args H
    end prop_f.

  Lemma is_prop_model_tcc_irr :
    ∀(m : prop_model)(f : lambda_formula V L)(p1 p2 : propositional f),
      is_prop_model m f p1 → is_prop_model m f p2.

  Lemma is_prop_model_false :
    ∀(m : prop_model)(nonempty_v : V)
          (prop_false : propositional (lambda_false nonempty_v)),
      is_prop_model m (lambda_false nonempty_v) prop_false → False.

  Definition prop_valid(f : lambda_formula V L)
                       (prop_f : propositional f) : Prop :=
    ∀(m : prop_model), is_prop_model m f prop_f.

  Definition prop_valid_sequent(nonempty_v : V)(s : sequent V L)
                               (prop_s : propositional_sequent s) : Prop :=
    prop_valid (or_formula_of_sequent s nonempty_v)
               (propositional_or_formula nonempty_v s prop_s).

  Definition prop_sequent_interpretation(m : prop_model)(s : sequent V L)
                                 (prop_seq : propositional_sequent s) : Prop :=
    some_neg_dep propositional (is_prop_model m) s prop_seq.

  Lemma prop_sequent_interpretation_tcc_irr :
    ∀(m : prop_model)(s : sequent V L)(ps1 ps2 : propositional_sequent s),
      prop_sequent_interpretation m s ps1 →
        prop_sequent_interpretation m s ps2.

  Lemma prop_sequent_interpretation_empty :
    ∀(m : prop_model)(prop : propositional_sequent []),
      prop_sequent_interpretation m [] prop → False.

  Lemma prop_sequent_interpretation_singleton :
    ∀(m : prop_model)(f : lambda_formula V L)
          (prop_s : propositional_sequent [f]),
      prop_sequent_interpretation m [f] prop_s ↔
        is_prop_model m f (prop_s 0 (lt_0_Sn 0)).

  Lemma prop_sequent_interpretation_nth_intro :
    ∀(m : prop_model)(s : sequent V L)(n : nat)(n_less : n < length s)
          (prop_s : propositional_sequent s),
      is_prop_model m (nth s n n_less) (prop_s n n_less) →
        prop_sequent_interpretation m s prop_s.

  Lemma prop_sequent_interpretation_cons_case_elim :
    ∀(m : prop_model)(f : lambda_formula V L)(s : sequent V L)
          (prop_fs : propositional_sequent (f :: s)),
      prop_sequent_interpretation m (f :: s) prop_fs →
        ((s = [] ∧ is_prop_model m f
                            (propositional_sequent_head _ _ prop_fs)) ∨
         (s ≠ [] ∧
            ~(~is_prop_model m f
                            (propositional_sequent_head _ _ prop_fs) ∧
              ¬prop_sequent_interpretation m s
                            (propositional_sequent_tail _ _ prop_fs)))).

  Lemma prop_sequent_interpretation_cons_cons_elim :
    ∀(m : prop_model)(f1 f2 : lambda_formula V L)(s : sequent V L)
          (prop_s : propositional_sequent (f1 :: f2 :: s)),
      prop_sequent_interpretation m (f1 :: f2 :: s) prop_s →
        ~(~is_prop_model m f1 (propositional_sequent_head _ _ prop_s) ∧
          ¬prop_sequent_interpretation m (f2 :: s)
                                    (propositional_sequent_tail _ _ prop_s)).

  Lemma prop_sequent_interpretation_length_case_intro :
    ∀(m : prop_model)(s : sequent V L)(prop_s : propositional_sequent s),
      (length s = 1 → prop_sequent_interpretation m s prop_s) →
      (length s ≠ 1 → ~~prop_sequent_interpretation m s prop_s) →
         prop_sequent_interpretation m s prop_s.

  Lemma prop_sequent_interpretation_cons_case_intro :
    ∀(m : prop_model)(f : lambda_formula V L)(s : sequent V L)
          (prop_fs : propositional_sequent (f :: s)),
      (s = [] → is_prop_model m f (propositional_sequent_head _ _ prop_fs))
        →
      (s ≠ [] → ~~prop_sequent_interpretation m (f :: s) prop_fs) →
        prop_sequent_interpretation m (f :: s) prop_fs.

  Lemma prop_sequent_interpretation_cons_cons_intro :
    ∀(m : prop_model)(f1 f2 : lambda_formula V L)(s : sequent V L)
          (prop_fs : propositional_sequent (f1 :: f2 :: s)),
      ~~prop_sequent_interpretation m (f1 :: f2 :: s) prop_fs →
        prop_sequent_interpretation m (f1 :: f2 :: s) prop_fs.

  Lemma prop_sequent_interpretation_append :
    ∀(m : prop_model)(sl sr : sequent V L)
          (prop_sl : propositional_sequent sl)
          (prop_sr : propositional_sequent sr),
      (prop_sequent_interpretation m sl prop_sl ∨
         prop_sequent_interpretation m sr prop_sr) →
      prop_sequent_interpretation m (sl ++ sr)
        (propositional_sequent_append sl sr prop_sl prop_sr).

  Lemma prop_sequent_interpretation_append_split :
    ∀(m : prop_model)(sl sr : sequent V L)
          (prop_sl_sr : propositional_sequent (sl ++ sr)),
      prop_sequent_interpretation m (sl ++ sr) prop_sl_sr →
        ~(~ (∀ (prop_sl : propositional_sequent sl),
               prop_sequent_interpretation m sl prop_sl) ∧
          ¬ (∀ (prop_sr : propositional_sequent sr),
               prop_sequent_interpretation m sr prop_sr)).

  Lemma prop_sequent_interpretation_add_context :
    ∀(m : prop_model)(sl s sr : sequent V L)
          (prop_sl : propositional_sequent sl)
          (prop_s : propositional_sequent s)
          (prop_sr : propositional_sequent sr),
      (prop_sequent_interpretation m sl prop_sl ∨
         prop_sequent_interpretation m s prop_s ∨
         prop_sequent_interpretation m sr prop_sr) →
      prop_sequent_interpretation m (add_context sl sr s)
        (propositional_add_context sl sr s prop_sl prop_sr prop_s).

  Lemma prop_sequent_interpretation_add_context_split :
    ∀(m : prop_model)(sl s sr : sequent V L)
          (prop_sl_s_sr : propositional_sequent (add_context sl sr s)),
      prop_sequent_interpretation m (add_context sl sr s) prop_sl_s_sr
      →
        ~(~(∀(prop_sl : propositional_sequent sl),
              prop_sequent_interpretation m sl prop_sl) ∧
          ~(∀(prop_s : propositional_sequent s),
              prop_sequent_interpretation m s prop_s) ∧
          ~(∀(prop_sr : propositional_sequent sr),
              prop_sequent_interpretation m sr prop_sr)).

  Lemma is_prop_model_or :
   ∀(m : prop_model)(f1 f2 : lambda_formula V L)
         (prop_f1 : propositional f1)(prop_f2 : propositional f2),
     is_prop_model m (lambda_or f1 f2)
                     (propositional_lambda_or _ _ prop_f1 prop_f2)
        ↔
     ~(~is_prop_model m f1 prop_f1 ∧ ¬is_prop_model m f2 prop_f2).

  Lemma prop_model_sequent_interpretation :
    ∀(nonempty_v : V)(m : prop_model)(s : sequent V L)
          (prop_seq : propositional_sequent s),
      prop_sequent_interpretation m s prop_seq
        ↔
      is_prop_model m (or_formula_of_sequent s nonempty_v)
              (propositional_or_formula nonempty_v _ prop_seq).

End Propositional_models.

Implicit Arguments is_prop_model [V L].
Implicit Arguments is_prop_model_tcc_irr [V L].
Implicit Arguments is_prop_model_false [V L].
Implicit Arguments prop_valid [V L].
Implicit Arguments prop_valid_sequent [V L].
Implicit Arguments prop_sequent_interpretation [V L].
Implicit Arguments prop_sequent_interpretation_tcc_irr [V L].
Implicit Arguments prop_sequent_interpretation_singleton [V L].
Implicit Arguments prop_sequent_interpretation_nth_intro [V L].
Implicit Arguments prop_model_sequent_interpretation [V L].
Implicit Arguments prop_sequent_interpretation_append [V L].
Implicit Arguments prop_sequent_interpretation_append_split [V L].
Implicit Arguments prop_sequent_interpretation_add_context [V L].
Implicit Arguments prop_sequent_interpretation_add_context_split [V L].