Completeness for propositional logic

This module proves Proposition 3.2.1, which is also needed as base case for the completeness of coalgebric logics.
I prove prove completeness here by using proof construction. If the proof construction fails, build_proof returns a non-tautological sequent for which I can build a counter model in order to derive a contradiction.
The use of the generic build_proof function has the problem that the returned proof trees have the wrong type. They are proof trees over rule set G of arbitrary rank, instead of over the propositional subset of G. One way to fix this problem is to use a dependent proof search, which moves a well-formedness predicate (here being a propositional sequent) up during the search. However, this seemed to complicated.
I therefore change the rule set of the proof afterwards.

Require Export classic propositional_sound build_prop_proof.

Section Propositional_Completeness.

  Variable V : Type.
  Variable L : modal_operators.

need a decidable equality on propositional constants for the proof construction
  Variable v_eq : eq_type V.

Simple tautologies


  Lemma simple_tautology_cons_append :
    (v : V)(f g : lambda_formula V L)(s1 s2 : sequent V L),
      (f = lf_prop v g = lf_neg (lf_prop v))
      (f = lf_neg (lf_prop v) g = lf_prop v)
        simple_tautology (f :: s1 ++ g :: s2).

build_proof for propositional sequents


  Definition prop_hyp_oracle :
                         hypotheses_oracle_type V L (empty_sequent_set V L) :=
    fun _None.

  Definition prop_build_proof(s : sequent V L) :
         (proof (G_set V L) (empty_sequent_set V L) s) + (sequent V L) :=
    build_proof (S (sequent_measure s))
      prop_hyp_oracle (prop_G_oracle v_eq) s.

  Definition prop_build_proof_prop_type(s : sequent V L) : Type :=
    propositional_sequent sprop_proof_type s.

  Fixpoint apply_propositional_subproofs(sl : list (sequent V L))
        (cond_subproofs : dep_list (sequent V L) prop_build_proof_prop_type sl)
        (prop_subproofs : every_nth propositional_sequent sl)
                                : dep_list (sequent V L) prop_proof_type sl :=
    match cond_subproofs
      in dep_list _ _ sl
      return every_nth propositional_sequent sl
                 dep_list (sequent V L) prop_proof_type sl
    with
      | dep_nilfun _dep_nil
      | dep_cons s rsl prop_fun_s r_prop_funs
        fun(prop_s_rsl : every_nth propositional_sequent (s :: rsl)) ⇒
          dep_cons s rsl (prop_fun_s (every_nth_head _ _ _ prop_s_rsl))
            (apply_propositional_subproofs rsl r_prop_funs
               (every_nth_tail _ _ _ prop_s_rsl))
    end prop_subproofs.

  Definition prop_build_proof_prop(s : sequent V L)
                      (p : proof (G_set V L) (empty_sequent_set V L) s) :
                                                prop_build_proof_prop_type s :=
    proof_rect V L (G_set V L) (empty_sequent_set V L)
      prop_build_proof_prop_type
      (fun(gamma : sequent V L)(in_hyp : empty_sequent_set V L gamma) _
         assume (prop_G_set V L) (empty_sequent_set V L) gamma in_hyp)
      (fun(r : sequent_rule V L)(in_G : G_set V L r)
          (subproofs : dep_list (sequent V L)
                                prop_build_proof_prop_type
                                (assumptions r))
          (prop_concl : propositional_sequent (conclusion r))
          ⇒
        rule (prop_G_set V L) (empty_sequent_set V L) r
             (G_set_prop_set r in_G prop_concl)
             (apply_propositional_subproofs (assumptions r) subproofs
                (const_rank_G_set 1 r in_G prop_concl)))
      s p.

Counter models


  Definition all_true_model : prop_model V := fun _True.

  Definition formula_counter_model(f : lambda_formula V L)
                                  (m : prop_model V) : prop_model V :=
    match f with
      | lf_prop vfunction_update v_eq m v False
      | lf_neg (lf_prop v) ⇒ function_update v_eq m v True
      | _m
    end.

  Fixpoint build_counter_model(l : sequent V L)(m : prop_model V)
                                                               : prop_model V :=
    match l with
      | []m
      | f :: rbuild_counter_model r (formula_counter_model f m)
    end.

  Lemma build_counter_model_const_v_ind :
    (s1 s2 : sequent V L)(f : lambda_formula V L)
          (m : prop_model V)(v : V),
      (f = lf_prop v f = lf_neg (lf_prop v)) →
      not (simple_tautology (f :: (s1 ++ s2))) →
      (formula_counter_model f m v = m v) →
        ((build_counter_model s2 m v) = (m v)).

  Lemma build_counter_model_const_v :
    (s : sequent V L)(f : lambda_formula V L)(m : prop_model V)(v : V),
      (f = lf_prop v f = lf_neg (lf_prop v)) →
      not (simple_tautology (f :: s)) →
      (formula_counter_model f m v = m v) →
        ((build_counter_model s m v) = (m v)).

  Lemma formula_counter_model_correct :
    (m : prop_model V)(f : lambda_formula V L)
          (prop_f : propositional f)(s : sequent V L),
      neg_form_maybe prop_form f
      ¬ simple_tautology (f :: s) →
        ¬ is_prop_model (build_counter_model s (formula_counter_model f m))
                        f prop_f.

  Lemma build_counter_model_correct :
    (s : sequent V L)(prop_s : propositional_sequent s)(m : prop_model V),
      prop_sequent s
      (not (simple_tautology s)) →
        not (prop_sequent_interpretation (build_counter_model s m) s prop_s).

Upward correctness


  Definition prop_correct(m : prop_model V)(s : sequent V L) : Prop :=
    prop_s # propositional_sequent s /#\ prop_sequent_interpretation m s prop_s.

  Lemma prop_correct_propositional :
    (m : prop_model V)(s : sequent V L),
      prop_correct m spropositional_sequent s.

  Definition upward_correct_rule(r : sequent_rule V L) : Prop :=
    (m : prop_model V),
      prop_correct m (conclusion r) →
        every_nth (prop_correct m) (assumptions r).

  Lemma upward_correct_context :
    (r : sequent_rule V L)(sl sr : sequent V L),
      every_nth propositional_sequent (assumptions r) →
      every_nth (fun aa []) (assumptions r) →
      upward_correct_rule r
        upward_correct_rule (rule_add_context sl sr r).

Ax


  Lemma upward_correct_ax : (r : sequent_rule V L),
      is_ax_rule rupward_correct_rule r.

And


  Lemma upward_propositional_bare_and_left :
    (f1 f2 : lambda_formula V L),
      propositional_sequent [lf_and f1 f2]propositional_sequent [f1].

  Lemma upward_propositional_bare_and_right :
    (f1 f2 : lambda_formula V L),
      propositional_sequent [lf_and f1 f2]propositional_sequent [f2].

  Lemma upward_propositional_bare_and :
    (f1 f2 : lambda_formula V L),
      propositional_sequent (conclusion (bare_and_rule f1 f2)) →
        every_nth propositional_sequent
                  (assumptions (bare_and_rule f1 f2)).

  Lemma upward_correct_and : (r : sequent_rule V L),
    is_and_rule rupward_correct_rule r.

Neg And


  Lemma upward_propositional_bare_neg_and_sequent :
    (f1 f2 : lambda_formula V L),
      propositional_sequent [lf_neg (lf_and f1 f2)]
        propositional_sequent [lf_neg f1; lf_neg f2].

  Lemma upward_propositional_bare_neg_and :
    (f1 f2 : lambda_formula V L),
      propositional_sequent (conclusion (bare_neg_and_rule f1 f2)) →
        every_nth propositional_sequent
                  (assumptions (bare_neg_and_rule f1 f2)).

  Lemma upward_correct_neg_and : (r : sequent_rule V L),
    is_neg_and_rule r
      upward_correct_rule r.

Neg Neg


  Lemma upward_propositional_bare_neg_neg_sequent :
    (f : lambda_formula V L),
      propositional_sequent [lf_neg (lf_neg f)]
        propositional_sequent [f].

  Lemma upward_propositional_bare_neg_neg :
    (f : lambda_formula V L),
      propositional_sequent (conclusion (bare_neg_neg_rule f)) →
        every_nth propositional_sequent
                  (assumptions (bare_neg_neg_rule f)).

  Lemma upward_correct_neg_neg : (r : sequent_rule V L),
    classical_logic
    is_neg_neg_rule r
      upward_correct_rule r.

Whole G


  Lemma correct_rule_inductive_G : (m : prop_model V),
    classical_logic
      rule_inductive (G_set V L) (prop_correct m).

Completeness


  Lemma propositional_complete_G :
    (nonempty_v : V)(s : sequent V L)
          (prop_s : propositional_sequent s),
      classical_logic
      prop_valid_sequent nonempty_v s prop_s
        provable (prop_G_set V L) (empty_sequent_set V L) s.

  Theorem prop_3_2_1 :
    (nonempty_v : V)(s : sequent V L)(prop_s : propositional_sequent s),
      classical_logic
        (prop_valid_sequent nonempty_v s prop_s
           
         provable (prop_G_set V L) (empty_sequent_set V L) s).

End Propositional_Completeness.

Implicit Arguments build_counter_model_correct [V L].