One-step conditions, 4.1 - 4.3

This module defines one-step soundness and completeness (4.1) and proves the simplification for cut-free one-step completeness (4.3.)

Require Export rule_sets semantics renaming list_multiset.

Section One_step_conditions.

  Variable V : Type.
  Variable L : modal_operators.
  Variable T : functor.

Need a decidable equality for limit_subst, which is needed in 4.3
  Variable v_eq : eq_type V.

One-step Soundness, Def 4.1, page 16


  Definition one_step_sound(nonempty_v : V)(LS : lambda_structure L T)
                           (rules : set (sequent_rule V L))
                           (osr : one_step_rule_set rules) : Prop :=
    (X : Type)(r : sequent_rule V L)(rules_r : rules r)
          (coval : Xset V),
      ((n : nat)(n_less : n < length (assumptions r)),
         prop_seq_val_valid nonempty_v coval
           (nth (assumptions r) n n_less)
           (one_step_rule_propositional_assumption r
               (osr r rules_r) n n_less))
        →
          mod_seq_val_valid LS coval (conclusion r)
            (one_step_rule_nonempty_conclusion r (osr r rules_r))
            (one_step_rule_prop_modal_prop_conclusion r (osr r rules_r)).

Towards one-step Completeness, Def 4.1

Define first the rule set appearing in the hypothesis. This is very similar to rank_weaken_subst_rule in module weakening.
  Definition simple_mod_weaken_rule(rules : set (sequent_rule V L))
                                                   : set (sequent_rule V L) :=
    fun(r_subst : sequent_rule V L) ⇒
      (r_base : sequent_rule V L)
            (sigma : lambda_subst V L)
            (delta : sequent V L),
        rules r_base
        rank_subst 1 sigma
        simple_modal_sequent delta
        assumptions r_subst = map (subst_sequent sigma) (assumptions r_base)
        list_reorder (conclusion r_subst)
                     ((subst_sequent sigma (conclusion r_base)) ++ delta).

  Lemma simple_mod_weaken_rule_assumptions :
    (rules : set (sequent_rule V L))(r : sequent_rule V L),
      one_step_rule_set rules
      simple_mod_weaken_rule rules r
        every_nth propositional_sequent (assumptions r).

The set of assumptions
  Definition valid_subst_n_conclusions
                     {X : Type}(nonempty_v : V)
                     (rules : set (sequent_rule V L))
                     (osr : one_step_rule_set rules)
                     (coval : Xset V) : set (sequent V L) :=
    fun(s : sequent V L) ⇒
      (r : sequent_rule V L),
        swr # simple_mod_weaken_rule rules r /#\
        s = conclusion r
        (i : nat)(i_less : i < length (assumptions r)),
          prop_seq_val_valid nonempty_v coval
            (nth (assumptions r) i i_less)
            (simple_mod_weaken_rule_assumptions _ _ osr swr _ _).

  Lemma multiset_valid_subst_n_conclusions :
    (X : Type)(nonempty_v : V)(rules : set (sequent_rule V L))
          (osr : one_step_rule_set rules)(coval : Xset V),
      sequent_multiset
        (valid_subst_n_conclusions nonempty_v rules osr coval).

  Lemma rank_sequent_set_valid_subst_n_conclusions :
    (X : Type)(nonempty_v : V)
          (rules : set (sequent_rule V L))(osr : one_step_rule_set rules)
          (coval : Xset V),
      rank_sequent_set 2
        (valid_subst_n_conclusions nonempty_v rules osr coval).

Generic one-step completeness
  Definition one_step_generic_complete
             (nonempty_v : V)(LS : lambda_structure L T)
             (prop_rules : set (sequent_rule V L))
             (rules : set (sequent_rule V L))
             (osr : one_step_rule_set rules) : Prop :=
    (X : Type)(coval : Xset V)
          (gamma : sequent V L)(gamma_nonempty : gamma [])
          (gamma_simple : simple_modal_sequent gamma),
      mod_seq_val_valid LS coval gamma gamma_nonempty
             (simple_modal_sequent_is_prop_modal_prop gamma gamma_simple) →
        provable prop_rules
          (valid_subst_n_conclusions nonempty_v rules osr coval)
          gamma.

One-step completeness, Def 4.1

  Definition one_step_complete(nonempty_v : V)(LS : lambda_structure L T)
             (rules : set (sequent_rule V L))
             (osr : one_step_rule_set rules) : Prop :=
    one_step_generic_complete nonempty_v LS (GC_n_set V L 2) rules osr.

One-step cut-free completeness, Def 4.1

  Definition one_step_cut_free_complete
             (nonempty_v : V)
             (LS : lambda_structure L T)
             (rules : set (sequent_rule V L))
             (osr : one_step_rule_set rules) : Prop :=
    one_step_generic_complete nonempty_v LS (G_n_set V L 2) rules osr.

Simple characterization of one-step cut-free completeness

Lemma 4.3, page 17

  Lemma propositional_renamed_one_step_assumptions :
    (rules : set (sequent_rule V L))(r : sequent_rule V L)
          (sigma : lambda_subst V L)
          (i : nat)(i_less : i < length (assumptions r)),
      one_step_rule_set rules
      rules r
      renaming sigma
        propositional_sequent
           (subst_sequent sigma (nth (assumptions r) i i_less)).

Lemma 4.3

  Lemma simple_one_step_cut_free_complete :
    (nonempty_v : V)(LS : lambda_structure L T)
          (rules : set (sequent_rule V L))(osr : one_step_rule_set rules),
      one_step_cut_free_complete nonempty_v LS rules osr
      (X : Type)(coval : Xset V)
            (gamma : sequent V L)(gamma_nonempty : gamma [])
            (gamma_simple : simple_modal_sequent gamma),
        mod_seq_val_valid LS coval gamma gamma_nonempty
               (simple_modal_sequent_is_prop_modal_prop gamma gamma_simple) →
          (r : sequent_rule V L)(sigma : lambda_subst V L),
            rules_r # rules r /#\
            renaming_sigma # renaming sigma /#\
            multi_subset (subst_sequent sigma (conclusion r)) gamma
            (i : nat)(i_less : i < length (assumptions r)),
              prop_seq_val_valid nonempty_v coval
                (subst_sequent sigma (nth (assumptions r) i i_less))
                (propositional_renamed_one_step_assumptions rules r sigma
                   i i_less osr rules_r renaming_sigma).

End One_step_conditions.

Implicit Arguments one_step_sound [V L T].
Implicit Arguments valid_subst_n_conclusions [V L X].
Implicit Arguments simple_mod_weaken_rule_assumptions [V L].
Implicit Arguments one_step_complete [V L T].
Implicit Arguments one_step_cut_free_complete [V L T].
Implicit Arguments simple_one_step_cut_free_complete [V L T].