Cut elimination case a, part of 5.6.3

This module contains the proof for case a) for the induction step of cut eliminations in 5.6. Case a) is the case of a cut between two one-step rules.
For case a) 1, i.e., the cut formula is in the weakening context of one of the one-step rules, see generic_cut.v

Require Export contraction factor_two_subst.

Section OSR_cut.

  Variable V : Type.
  Variable L : modal_operators.

  Variable op_eq : eq_type (operator L).
  Variable v_eq : eq_type V.

Case a 2: both cut formulas are in the one-step rule


  Lemma syntactic_GR_n_get_cut_rule :
    (rules : set (sequent_rule V L))(n : nat)
          (fsub : lambda_formula V L)
          (rb_l rb_r : sequent_rule V L)(sigma_l sigma_r : lambda_subst V L)
          (concl_l_subst concl_r_subst : sequent V L),
      countably_infinite V
      one_step_rule_set rules
      absorbs_cut op_eq v_eq rules
      rules rb_lrules rb_r
      rank_subst (S n) sigma_lrank_subst (S n) sigma_r
      list_reorder (fsub :: concl_l_subst)
                   (subst_sequent sigma_l (conclusion rb_l)) →
      list_reorder ((lf_neg fsub) :: concl_r_subst)
                   (subst_sequent sigma_r (conclusion rb_r))
      →
        (rsigma_l rsigma_r inj_sigma cut_sigma : lambda_subst V L)
              (cut_r : sequent_rule V L)(concl_l concl_r : sequent V L),
          renaming rsigma_l renaming rsigma_r
          renaming cut_sigma rank_subst (S n) inj_sigma
          injective inj_sigma
          rules cut_r
          rank_sequent 2 concl_l rank_sequent 2 concl_r
          concl_l_subst = subst_sequent inj_sigma concl_l
          concl_r_subst = subst_sequent inj_sigma concl_r
          map (subst_sequent sigma_l) (assumptions rb_l) =
            map (subst_sequent (subst_compose inj_sigma rsigma_l))
                (assumptions rb_l)
          map (subst_sequent sigma_r) (assumptions rb_r) =
            map (subst_sequent (subst_compose inj_sigma rsigma_r))
                (assumptions rb_r)
          multi_subset
            (sequent_support op_eq v_eq
                     (subst_sequent cut_sigma (conclusion cut_r)))
            (concl_l ++ concl_r)
          every_nth
            (fun ass
               provable (GC_n_set V L 1)
                        (reordered_sequent_list_set
                           ((map (subst_sequent rsigma_l) (assumptions rb_l)) ++
                            (map (subst_sequent rsigma_r) (assumptions rb_r))))
                 (subst_sequent cut_sigma ass))
            (assumptions cut_r).

  Lemma syntactic_GR_n_prove_cut_absorb_assumptions :
    (rules : set (sequent_rule V L))(n : nat)
          (rb_l rb_r cut_r : sequent_rule V L)
          (rsigma_l rsigma_r inj_sigma cut_sigma : lambda_subst V L),
      countably_infinite V
      one_step_rule_set rules
      absorbs_congruence rules
      rules rb_lrules rb_r
      renaming rsigma_lrenaming rsigma_rrenaming cut_sigma
      rank_subst (S n) inj_sigma
      every_nth (provable (GR_n_set rules (S n)) (empty_sequent_set V L))
        (map (subst_sequent (subst_compose inj_sigma rsigma_l))
             (assumptions rb_l)) →
      every_nth (provable (GR_n_set rules (S n)) (empty_sequent_set V L))
        (map (subst_sequent (subst_compose inj_sigma rsigma_r))
             (assumptions rb_r)) →
      every_nth
        (fun(ass : sequent V L) ⇒
           provable (GC_n_set V L 1)
             (reordered_sequent_list_set
                (map (subst_sequent rsigma_l) (assumptions rb_l) ++
                 map (subst_sequent rsigma_r) (assumptions rb_r)))
             (subst_sequent cut_sigma ass))
        (assumptions cut_r)
      →
        every_nth
          (provable (GRC_n_set rules (S n)) (empty_sequent_set V L))
          (map (subst_sequent (subst_compose inj_sigma cut_sigma))
               (assumptions cut_r)).

  Lemma syntactic_GR_n_prove_cut_absorb_conclusion :
    (rules : set (sequent_rule V L))(n : nat)
          (cut_r : sequent_rule V L)
          (inj_sigma cut_sigma : lambda_subst V L),
      one_step_rule_set rules
      rules cut_r
      renaming cut_sigma
      rank_subst (S n) inj_sigma
      every_nth (provable (GR_n_set rules (S n)) (empty_sequent_set V L))
        (map (subst_sequent (subst_compose inj_sigma cut_sigma))
           (assumptions cut_r))
      →
         provable (GR_n_set rules (2 + n)) (empty_sequent_set V L)
           (subst_sequent (subst_compose inj_sigma cut_sigma)
                          (conclusion cut_r)).

  Lemma syntactic_GR_n_cut_eli_two_osr_concl :
    (rules : set (sequent_rule V L))(n : nat)(ssn_pos : 0 < 2 + n)
          (f : lambda_formula V L)(q r : sequent V L)
          (rb_l rb_r : sequent_rule V L)(sigma_l sigma_r : lambda_subst V L)
          (delta_l delta_r concl_l_tl concl_r_tl : sequent V L),
      countably_infinite V
      one_step_rule_set rules
      absorbs_congruence rules
      absorbs_cut op_eq v_eq rules
      ((s : sequent V L)(f : lambda_formula V L),
         provable (GR_n_set rules (2 + n)) (empty_sequent_set V L)
                  (f :: f :: s) →
           provable (GR_n_set rules (2 + n)) (empty_sequent_set V L) (f :: s))
      →
      ((s : sequent V L),
         provable (GRC_n_set rules (S n)) (empty_sequent_set V L) s
           provable (GR_n_set rules (S n)) (empty_sequent_set V L) s) →
      rules rb_lrules rb_r
      rank_subst (S n) sigma_lrank_subst (S n) sigma_r
      rank_sequent (2 + n) delta_lrank_sequent (2 + n) delta_r
      list_reorder (f :: q)
                   (subst_sequent sigma_l (conclusion rb_l) ++ delta_l) →
      list_reorder (f :: concl_l_tl)
                   (subst_sequent sigma_l (conclusion rb_l)) →
      list_reorder ((lf_neg f) :: r)
                   (subst_sequent sigma_r (conclusion rb_r) ++ delta_r) →
      list_reorder ((lf_neg f) :: concl_r_tl)
                   (subst_sequent sigma_r (conclusion rb_r)) →
      every_nth
           (provable (GR_n_set rules (S n)) (empty_sequent_set V L))
           (map (subst_sequent sigma_l) (assumptions rb_l)) →
      every_nth
           (provable (GR_n_set rules (S n)) (empty_sequent_set V L))
           (map (subst_sequent sigma_r) (assumptions rb_r)) →
        provable (G_n_set V L (2 + n))
                 (provable_subst_n_conclusions rules (2 + n) ssn_pos)
          (q ++ r).

Combine proofs for case a)


  Lemma syntactic_GR_n_cut_eli_two_osr :
    (rules : set (sequent_rule V L))(n : nat)(ssn_pos : 0 < 2 + n)
          (f : lambda_formula V L)(r q : sequent V L),
      countably_infinite V
      one_step_rule_set rules
      absorbs_cut op_eq v_eq rules
      absorbs_congruence rules
      ((s : sequent V L)(f : lambda_formula V L),
         provable (GR_n_set rules (2 + n)) (empty_sequent_set V L)
                  (f :: f :: s) →
           provable (GR_n_set rules (2 + n)) (empty_sequent_set V L) (f :: s))
      →
      ((s : sequent V L),
         provable (GRC_n_set rules (S n)) (empty_sequent_set V L) s
           provable (GR_n_set rules (S n)) (empty_sequent_set V L) s) →
      provable_subst_n_conclusions rules (2 + n) ssn_pos (f :: q) →
      provable_subst_n_conclusions rules (2 + n) ssn_pos (lf_neg f :: r) →
        provable (G_n_set V L (2 + n))
                 (provable_subst_n_conclusions rules (2 + n) ssn_pos)
          (q ++ r).

End OSR_cut.