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_l → rules rb_r →
      rank_subst (S n) sigma_l → rank_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_l → rules rb_r →
      renaming rsigma_l → renaming rsigma_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 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_l → rules rb_r →
      rank_subst (S n) sigma_l → rank_subst (S n) sigma_r →
      rank_sequent (2 + n) delta_l → rank_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.