Require Export propositional_models.

Section Propositional_soundness.

  Variable V : Type.
  Variable L : modal_operators.

  Definition prop_proof_type : sequent V L → Type :=
    proof (prop_G_set V L) (empty_sequent_set V L).

  Definition prop_downward_correct_rule(r : sequent_rule V L)
                                     (prop_r : propositional_rule r) : Prop :=
    ∀(m : prop_model V),
      (∀(n : nat)(n_len : n < length (assumptions r)),
         prop_sequent_interpretation m (nth (assumptions r) n n_len)
           (prop_sequent_rule_ass_tcc r n n_len prop_r)) →
      prop_sequent_interpretation m (conclusion r)
          (prop_sequent_rule_concl_tcc r prop_r).

  Lemma prop_downward_correct_rule_tcc_irr :
    ∀(r : sequent_rule V L)(prop_r1 prop_r2 : propositional_rule r),
      prop_downward_correct_rule r prop_r1 →
        prop_downward_correct_rule r prop_r2.

  Definition prop_downward_correct_rule_set(rules : sequent_rule V L → Prop)
                          (prop_rules : propositional_rule_set rules) : Prop :=
    ∀(r : sequent_rule V L)(r_rule : rules r),
      prop_downward_correct_rule r (prop_rules r r_rule).

  Lemma propositional_correct_derivation :
    ∀(m : prop_model V)
          (rules : sequent_rule V L → Prop)
          (prop_rules : propositional_rule_set rules)
          (hypotheses : sequent V L → Prop)
          (prop_hyp : propositional_sequent_set hypotheses)
          (l : sequent V L)(prop_l : propositional_sequent l),
      prop_downward_correct_rule_set rules prop_rules →
      (∀(h : sequent V L)(in_hyp : hypotheses h),
                  prop_sequent_interpretation m h (prop_hyp h in_hyp)) →
      proof rules hypotheses l →
        prop_sequent_interpretation m l prop_l.

  Lemma assumption_add_context_interpretation :
    ∀(m : prop_model V)(sl sr : sequent V L)
          (prop_sl : propositional_sequent sl)
          (prop_sr : propositional_sequent sr)
          (sml : list (sequent V L))
          (prop_sml : every_nth propositional_sequent sml)
          (prop_sml_context :
             every_nth propositional_sequent (map (add_context sl sr) sml)),
   sml ≠ [] →
   (∀(n : nat)(n_len : n < length (map (add_context sl sr) sml)),
      prop_sequent_interpretation m
        (nth (map (add_context sl sr) sml) n n_len)
        (prop_sml_context n n_len))
     →
       ~(~(prop_sequent_interpretation m sl prop_sl) ∧
         ~(prop_sequent_interpretation m sr prop_sr) ∧
         ~(∀(n : nat)(n_less : n < length sml),
            prop_sequent_interpretation m
              (nth sml n n_less) (prop_sml n n_less))).

  Lemma prop_downward_correct_context :
    ∀(r : sequent_rule V L)(sl sr : sequent V L)
          (prop_sl_r_sr : propositional_rule (rule_add_context sl sr r)),
      conclusion r ≠ [] →
      prop_downward_correct_rule r
        (propositional_rule_add_context_bare_rule r sl sr prop_sl_r_sr)
      →
        prop_downward_correct_rule (rule_add_context sl sr r) prop_sl_r_sr.

  Lemma prop_downward_correct_ax :
    ∀(r : sequent_rule V L)(prop_r : propositional_rule r),
      is_ax_rule r →
        prop_downward_correct_rule r prop_r.

  Lemma prop_downward_correct_and :
    ∀(r : sequent_rule V L)(prop_r : propositional_rule r),
      is_and_rule r → prop_downward_correct_rule r prop_r.

  Lemma prop_downward_correct_neg_and :
    ∀(r : sequent_rule V L)(prop_r : propositional_rule r),
      is_neg_and_rule r → prop_downward_correct_rule r prop_r.

  Lemma prop_downward_correct_neg_neg :
    ∀(r : sequent_rule V L)(prop_r : propositional_rule r),
      is_neg_neg_rule r → prop_downward_correct_rule r prop_r.

  Lemma prop_downward_correct_prop_G :
    prop_downward_correct_rule_set (prop_G_set V L) propositional_prop_G_set.

  Lemma propositional_correct_G_derivation :
    ∀(m : prop_model V)
          (l : sequent V L)(prop_l : propositional_sequent l),
      prop_proof_type l →
        prop_sequent_interpretation m l prop_l.

  Lemma propositional_sound_G :
    ∀(nonempty_v : V)(s : sequent V L)(prop_s : propositional_sequent s),
      provable (prop_G_set V L) (empty_sequent_set V L) s →
        prop_valid_sequent nonempty_v s prop_s.

End Propositional_soundness.

Implicit Arguments prop_proof_type [[V] [L]].
Implicit Arguments propositional_sound_G [V L].