Require Export propositional_formulas modal_formulas rules.

Section Rule_sets.

  Variable V : Type.
  Variable L : modal_operators.

  Definition G_struct_set(r : sequent_rule V L) : Prop :=
    is_and_rule r ∨ is_neg_and_rule r ∨ is_neg_neg_rule r.

  Definition G_set : set (sequent_rule V L) :=
    union is_ax_rule
     (union is_and_rule
       (union is_neg_and_rule is_neg_neg_rule)).

  Lemma G_set_struct_union :
    set_equal G_set (union is_ax_rule G_struct_set).

  Lemma subst_closed_G_struct_set : subst_closed_rule_set G_struct_set.

  Lemma G_struct_multiset : rule_multiset G_struct_set.

  Lemma G_multiset : rule_multiset G_set.

  Lemma const_rank_G_set :
    ∀(n : nat)(r : sequent_rule V L),
      G_set r →
      rank_sequent n (conclusion r) →
        every_nth (rank_sequent n) (assumptions r).

  Lemma ax_rule_no_simple_modal_conclusion :
    ∀(r : sequent_rule V L),
      is_ax_rule r →
      ¬ simple_modal_sequent (conclusion r).

  Lemma and_rule_no_simple_modal_conclusion :
    ∀(r : sequent_rule V L),
      is_and_rule r →
      ¬ simple_modal_sequent (conclusion r).

  Lemma neg_and_rule_no_simple_modal_conclusion :
    ∀(r : sequent_rule V L),
      is_neg_and_rule r →
      ¬ simple_modal_sequent (conclusion r).

  Lemma neg_neg_rule_no_simple_modal_conclusion :
    ∀(r : sequent_rule V L),
      is_neg_neg_rule r →
      ¬ simple_modal_sequent (conclusion r).

  Lemma G_rules_no_simple_modal_conclusion :
    ∀(r : sequent_rule V L),
      G_set r →
      ¬ simple_modal_sequent (conclusion r).

  Lemma G_set_no_empty_conclusion : ∀(r : sequent_rule V L),
    G_set r → conclusion r ≠ [].

  Definition G_n_set(n : nat) : set (sequent_rule V L) :=
    rank_rules n G_set.

  Lemma G_n_multiset : ∀(n : nat),
    rule_multiset (G_n_set n).

  Lemma provable_depth_G_n_hyp_list_reorder :
    ∀(hyp : set (sequent V L))(n d : nat)(s1 s2 : sequent V L),
      sequent_multiset hyp →
      list_reorder s1 s2 →
      provable_at_depth (G_n_set n) hyp d s1 →
        provable_at_depth (G_n_set n) hyp d s2.

  Lemma provable_G_n_hyp_list_reorder :
    ∀(hyp : set (sequent V L))(n : nat)(s1 s2 : sequent V L),
      sequent_multiset hyp →
      list_reorder s1 s2 →
      provable (G_n_set n) hyp s1 →
        provable (G_n_set n) hyp s2.

  Lemma provable_G_n_list_reorder :
    ∀(n : nat)(s1 s2 : sequent V L),
      list_reorder s1 s2 →
      provable (G_n_set n) (empty_sequent_set V L) s1 →
        provable (G_n_set n) (empty_sequent_set V L) s2.

  Lemma G_n_set_mono : ∀(n1 n2 : nat),
    n1 ≤ n2 → subset (G_n_set n1) (G_n_set n2).

  Lemma ax_n_subset_G_n : ∀(n : nat),
    subset (rank_rules n is_ax_rule) (G_n_set n).

  Lemma and_n_subset_G_n : ∀(n : nat),
    subset (rank_rules n is_and_rule) (G_n_set n).

  Lemma neg_and_n_subset_G_n : ∀(n : nat),
    subset (rank_rules n is_neg_and_rule) (G_n_set n).

  Lemma neg_neg_n_subset_G_n : ∀(n : nat),
    subset (rank_rules n is_neg_neg_rule) (G_n_set n).

  Lemma decompose_G_n_set_coarsly :
    ∀(n : nat)(r : sequent_rule V L),
      G_n_set n r →
        (assumptions r = [] ∧
         simple_tautology (conclusion r) ∧
         rank_sequent n (conclusion r)
        ) ∨
        (∃(rb : sequent_rule V L)(sl sr : sequent V L)
               (concl_rb : lambda_formula V L),
          every_nth (rank_sequent n) (assumptions r) ∧
          rank_sequent n (conclusion r) ∧
          r = rule_add_context sl sr rb ∧
          ((∃(f1 f2 : lambda_formula V L), rb = bare_and_rule f1 f2) ∨
           (∃(f1 f2 : lambda_formula V L), rb = bare_neg_and_rule f1 f2) ∨
           (∃(f : lambda_formula V L), rb = bare_neg_neg_rule f))
          ∧ [concl_rb] = conclusion rb).

  Lemma decompose_G_n_set :
    ∀(n : nat)(r : sequent_rule V L),
      G_n_set n r →
        (assumptions r = [] ∧
         simple_tautology (conclusion r) ∧
         rank_sequent n (conclusion r)
        ) ∨
        (∃(sl sr : sequent V L)(f1 f2 : lambda_formula V L),
          assumptions r = [sl ++ f1 :: sr; sl ++ f2 :: sr] ∧
          conclusion r = sl ++ (lf_and f1 f2) :: sr ∧
          rank_sequent n (sl ++ f1 :: sr) ∧
          rank_sequent n (sl ++ f2 :: sr) ∧
          rank_sequent n (sl ++ (lf_and f1 f2) :: sr)
        ) ∨
        (∃(sl sr : sequent V L)(f1 f2 : lambda_formula V L),
          assumptions r = [sl ++ (lf_neg f1) :: (lf_neg f2) :: sr] ∧
          conclusion r = sl ++ (lf_neg (lf_and f1 f2)) :: sr ∧
          rank_sequent n (sl ++ (lf_neg f1) :: (lf_neg f2) :: sr) ∧
          rank_sequent n (sl ++ (lf_neg (lf_and f1 f2)) :: sr)
        ) ∨
        (∃(sl sr : sequent V L)(f : lambda_formula V L),
          assumptions r = [sl ++ f :: sr] ∧
          conclusion r = sl ++ (lf_neg (lf_neg f)) :: sr ∧
          rank_sequent n (sl ++ f :: sr) ∧
          rank_sequent n (sl ++ (lf_neg (lf_neg f)) :: sr)
        ).

  Lemma provable_with_and :
    ∀(rules : set (sequent_rule V L))(hyp : set (sequent V L))
          (sl sr : sequent V L)(f1 f2 : lambda_formula V L)(n : nat),
      subset (G_n_set n) (rank_rules n rules) →
      rank_sequent n (sl ++ (lf_and f1 f2) :: sr) →
      provable (rank_rules n rules) hyp (sl ++ f1 :: sr) →
      provable (rank_rules n rules) hyp (sl ++ f2 :: sr) →
        provable (rank_rules n rules) hyp (sl ++ (lf_and f1 f2) :: sr).

  Lemma provable_with_neg_and :
    ∀(rules : set (sequent_rule V L))(hyp : set (sequent V L))
          (sl sr : sequent V L)(f1 f2 : lambda_formula V L)(n : nat),
      subset (G_n_set n) (rank_rules n rules) →
      rank_sequent n (sl ++ (lf_neg (lf_and f1 f2)) :: sr) →
      provable (rank_rules n rules) hyp
               (sl ++ (lf_neg f1) :: (lf_neg f2) :: sr) →
        provable (rank_rules n rules) hyp
                 (sl ++ (lf_neg (lf_and f1 f2)) :: sr).

  Lemma provable_with_neg_neg :
    ∀(rules : set (sequent_rule V L))(hyp : set (sequent V L))
          (sl sr : sequent V L)(f : lambda_formula V L)(n : nat),
      subset (G_n_set n) (rank_rules n rules) →
      rank_sequent n (sl ++ (lf_neg (lf_neg f)) :: sr) →
      provable (rank_rules n rules) hyp (sl ++ f :: sr) →
        provable (rank_rules n rules) hyp (sl ++ (lf_neg (lf_neg f)) :: sr).

  Lemma G_n_set_no_simple_modal_conclusion :
    ∀(n : nat)(r : sequent_rule V L),
      G_n_set n r →
      ¬ simple_modal_sequent (conclusion r).

  Lemma sequent_other_context_G_n_set :
    ∀(n : nat)(sl1 sl2 sr1 sr2 : sequent V L)
          (rbase : sequent_rule V L),
      ((∃ f1 f2 : lambda_formula V L, rbase = bare_and_rule f1 f2) ∨
       (∃ f1 f2 : lambda_formula V L, rbase = bare_neg_and_rule f1 f2) ∨
       (∃ f : lambda_formula V L, rbase = bare_neg_neg_rule f)) →
      (rank_sequent n sl1 → rank_sequent n sl2) →
      (rank_sequent n sr1 → rank_sequent n sr2) →
      rank_sequent n (sl1 ++ conclusion rbase ++ sr1) →
        G_n_set n (rule_add_context sl2 sr2 rbase).

  Lemma other_context_G_n_set :
    ∀(n : nat)(f1 f2 : lambda_formula V L)(sl sr : sequent V L)
          (rbase : sequent_rule V L),
      ((∃ f1 f2 : lambda_formula V L, rbase = bare_and_rule f1 f2) ∨
       (∃ f1 f2 : lambda_formula V L, rbase = bare_neg_and_rule f1 f2) ∨
       (∃ f : lambda_formula V L, rbase = bare_neg_neg_rule f)) →
      rank_sequent n ((f1 :: sl) ++ conclusion rbase ++ sr) →
      (rank_formula n f1 → rank_formula n f2) →
        G_n_set n (rule_add_context (f2 :: sl) sr rbase).

  Lemma smaller_context_G_n_set :
    ∀(n : nat)(f : lambda_formula V L)(sl sr : sequent V L)
          (rbase : sequent_rule V L),
      ((∃ f1 f2 : lambda_formula V L, rbase = bare_and_rule f1 f2) ∨
       (∃ f1 f2 : lambda_formula V L, rbase = bare_neg_and_rule f1 f2) ∨
       (∃ f : lambda_formula V L, rbase = bare_neg_neg_rule f)) →
      rank_sequent n ((f :: sl) ++ conclusion rbase ++ sr) →
        G_n_set n (rule_add_context sl sr rbase).

  Definition GC_set : set (sequent_rule V L) :=
    union G_set is_cut_rule.

  Lemma GC_multiset : rule_multiset GC_set.

  Definition GC_n_set(n : nat) : set (sequent_rule V L) :=
    rank_rules n GC_set.

  Lemma GC_n_multiset : ∀(n : nat), rule_multiset (GC_n_set n).

  Lemma G_n_subset_GC_n : ∀(n : nat),
    subset (G_n_set n) (GC_n_set n).

  Lemma C_n_subset_GC_n : ∀(n : nat),
    subset (bounded_cut_rules V L n) (GC_n_set n).

  Lemma GC_n_as_G_C_union : ∀(n : nat),
    set_equal (GC_n_set n) (union (bounded_cut_rules V L n) (G_n_set n)).

  Lemma provable_with_cut :
    ∀(rules : set (sequent_rule V L))(hyp : set (sequent V L))
          (gl gr dl dr : sequent V L)(f : lambda_formula V L)(n : nat),
      subset (GC_n_set n) (rank_rules n rules) →
      rank_formula n f →
      rank_sequent n (gl ++ gr ++ dl ++ dr) →
      provable (rank_rules n rules) hyp (gl ++ f :: gr) →
      provable (rank_rules n rules) hyp (dl ++ (lf_neg f) :: dr) →
        provable (rank_rules n rules) hyp (gl ++ gr ++ dl ++ dr).

  Definition one_step_rule(r : sequent_rule V L) : Prop :=
    every_nth prop_sequent (assumptions r) ∧
    simple_modal_sequent (conclusion r) ∧
    every_nth (fun(s : sequent V L) ⇒
                 incl (prop_var_sequent s) (prop_var_sequent (conclusion r)))
      (assumptions r) ∧
    conclusion r ≠ [].

  Lemma one_step_rule_multiset : rule_multiset one_step_rule.

  Definition one_step_rule_set(rules : set (sequent_rule V L)) : Prop :=
    ∀(r : sequent_rule V L), rules r → one_step_rule r.

  Lemma one_step_rule_propositional_assumption :
    ∀(r : sequent_rule V L),
      one_step_rule r →
        every_nth propositional_sequent (assumptions r).

  Lemma rank_subst_assumptions :
    ∀(r : sequent_rule V L)(sigma : lambda_subst V L)(n : nat),
      one_step_rule r →
      rank_subst n sigma →
      every_nth (rank_sequent n)
        (map (subst_sequent sigma) (assumptions r)).

  Lemma rank_sequent_subst_nth_assumptions :
    ∀(r : sequent_rule V L)(sigma : lambda_subst V L)(n i : nat)
          (i_less : i < length (assumptions r)),
      one_step_rule r →
      rank_subst n sigma →
      rank_sequent n (subst_sequent sigma (nth (assumptions r) i i_less)).

  Lemma rank_subst_conclusion :
    ∀(r : sequent_rule V L)(sigma : lambda_subst V L)(n : nat),
      1 < n →
      one_step_rule r →
      rank_subst (pred n) sigma →
      rank_sequent n (subst_sequent sigma (conclusion r)).

  Lemma one_step_rule_simple_modal_conclusion :
    ∀(r : sequent_rule V L),
      one_step_rule r → simple_modal_sequent (conclusion r).

  Lemma one_step_rule_subst_top_modal_conclusion :
    ∀(r : sequent_rule V L)(sigma : lambda_subst V L),
      one_step_rule r →
        top_modal_sequent (subst_sequent sigma (conclusion r)).

  Lemma one_step_rule_prop_modal_prop_conclusion :
    ∀(r : sequent_rule V L),
      one_step_rule r → prop_modal_prop_sequent (conclusion r).

  Lemma one_step_rule_incl_prop_var_sequent :
    ∀(r : sequent_rule V L),
      one_step_rule r →
        every_nth
          (fun(a : sequent V L) ⇒
                   incl (prop_var_sequent a) (prop_var_sequent (conclusion r)))
          (assumptions r).

  Lemma one_step_rule_nonempty_conclusion :
    ∀(r : sequent_rule V L),
      one_step_rule r → conclusion r ≠ [].

  Definition weaken_subst_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 ∧
        assumptions r_subst = map (subst_sequent sigma) (assumptions r_base) ∧
        list_reorder (conclusion r_subst)
                     ((subst_sequent sigma (conclusion r_base)) ++ delta).

  Lemma weaken_subst_rule_multiset :
    ∀(rules : set (sequent_rule V L)),
      rule_multiset (weaken_subst_rule rules).

  Lemma subst_closed_weaken_subst :
    ∀(rules : set (sequent_rule V L)),
      subst_closed_rule_set (weaken_subst_rule rules).

  Lemma R_set_no_empty_conclusion :
    ∀(rules : set (sequent_rule V L))(r : sequent_rule V L),
      one_step_rule_set rules →
      weaken_subst_rule rules r →
        conclusion r ≠ [].

  Lemma R_set_1_empty :
    ∀(rules : set (sequent_rule V L)),
      one_step_rule_set rules →
        set_equal (rank_rules 1 (weaken_subst_rule rules)) (empty_set _).

  Definition GR_set(rules : set (sequent_rule V L)) : set (sequent_rule V L) :=
    union G_set (weaken_subst_rule rules).

  Lemma GR_multiset : ∀(rules : set (sequent_rule V L)),
    rule_multiset (GR_set rules).

  Definition GR_set_wo_ax(rules : set (sequent_rule V L))
                                                    : set (sequent_rule V L) :=
    union G_struct_set (weaken_subst_rule rules).

  Lemma GR_set_wo_ax_multiset : ∀(rules : set (sequent_rule V L)),
    rule_multiset (GR_set_wo_ax rules).

  Lemma GR_set_struct_union : ∀(rules : set (sequent_rule V L)),
    set_equal (GR_set rules) (union is_ax_rule (GR_set_wo_ax rules)).

  Lemma subst_closed_GR_set_wo_ax :
    ∀(rules : set (sequent_rule V L)),
      subst_closed_rule_set (GR_set_wo_ax rules).

  Lemma GR_set_no_empty_conclusion :
    ∀(rules : set (sequent_rule V L))(r : sequent_rule V L),
      one_step_rule_set rules →
      GR_set rules r →
        conclusion r ≠ [].

  Lemma G_subset_GR : ∀(rules : set (sequent_rule V L)),
    subset G_set (GR_set rules).

  Definition GR_n_set(rules : set (sequent_rule V L))(n : nat)
                                                    : set (sequent_rule V L) :=
    rank_rules n (GR_set rules).

  Lemma GR_n_multiset : ∀(rules : set (sequent_rule V L))(n : nat),
    rule_multiset (GR_n_set rules n).

  Lemma provable_GR_n_hyp_list_reorder :
    ∀(rules : set (sequent_rule V L))(hyp : set (sequent V L))
          (n : nat)(s1 s2 : sequent V L),
      list_reorder s1 s2 →
      sequent_multiset hyp →
      provable (GR_n_set rules n) hyp s1 →
        provable (GR_n_set rules n) hyp s2.

  Lemma provable_GR_n_list_reorder :
    ∀(rules : set (sequent_rule V L))(n : nat)(s1 s2 : sequent V L),
      list_reorder s1 s2 →
      provable (GR_n_set rules n) (empty_sequent_set V L) s1 →
        provable (GR_n_set rules n) (empty_sequent_set V L) s2.

  Lemma GR_n_set_struct_union :
    ∀(rules : set (sequent_rule V L))(n : nat),
      set_equal (GR_n_set rules n)
                (rank_rules n (union is_ax_rule (GR_set_wo_ax rules))).

  Lemma G_n_subset_GR_n :
    ∀(rules : set (sequent_rule V L))(n : nat),
      subset (G_n_set n) (GR_n_set rules n).

  Lemma R_n_subset_GR_n :
    ∀(rules : set (sequent_rule V L))(n : nat),
      subset (rank_rules n (weaken_subst_rule rules)) (GR_n_set rules n).

  Definition GRC_set(rules : set (sequent_rule V L))
                                                    : set (sequent_rule V L) :=
    union (GR_set rules) is_cut_rule.

  Lemma GRC_multiset : ∀(rules : set (sequent_rule V L)),
    rule_multiset (GRC_set rules).

  Definition GRC_set_wo_ax(rules : set (sequent_rule V L))
                                                    : set (sequent_rule V L) :=
    union (GR_set_wo_ax rules) is_cut_rule.

  Lemma GRC_set_wo_ax_multiset : ∀(rules : set (sequent_rule V L)),
    rule_multiset (GRC_set_wo_ax rules).

  Lemma GRC_set_struct_union : ∀(rules : set (sequent_rule V L)),
    set_equal (GRC_set rules) (union is_ax_rule (GRC_set_wo_ax rules)).

  Lemma subst_closed_GRC_set_wo_ax :
    ∀(rules : set (sequent_rule V L)),
      subst_closed_rule_set (GRC_set_wo_ax rules).

  Lemma GR_subset_GRC :
    ∀(rules : set (sequent_rule V L)),
      subset (GR_set rules) (GRC_set rules).

  Definition GRC_n_set(rules : set (sequent_rule V L))(n : nat)
                                                    : set (sequent_rule V L) :=
    rank_rules n (GRC_set rules).

  Lemma GRC_n_multiset : ∀(rules : set (sequent_rule V L))(n : nat),
    rule_multiset (GRC_n_set rules n).

  Lemma provable_GRC_n_list_reorder :
    ∀(rules : set (sequent_rule V L))(n : nat)(s1 s2 : sequent V L),
      list_reorder s1 s2 →
      provable (GRC_n_set rules n) (empty_sequent_set V L) s1 →
        provable (GRC_n_set rules n) (empty_sequent_set V L) s2.

  Definition GRC_n_set_wo_ax(rules : set (sequent_rule V L))(n : nat)
                                                    : set (sequent_rule V L) :=
    rank_rules n (GRC_set_wo_ax rules).

  Lemma GRC_n_set_wo_ax_multiset :
    ∀(rules : set (sequent_rule V L))(n : nat),
      rule_multiset (GRC_n_set_wo_ax rules n).

  Lemma GRC_n_set_struct_union :
    ∀(rules : set (sequent_rule V L))(n : nat),
      set_equal (GRC_n_set rules n)
                (rank_rules n (union is_ax_rule (GRC_set_wo_ax rules))).

  Lemma GRC_n_set_empty :
    ∀(rules : set (sequent_rule V L)),
      one_step_rule_set rules →
      set_equal (GRC_n_set rules 0) (empty_set (sequent_rule V L)).

  Lemma GR_n_subset_GRC_n :
    ∀(rules : set (sequent_rule V L))(n : nat),
      subset (GR_n_set rules n) (GRC_n_set rules n).

  Lemma GC_n_subset_GRC_n :
    ∀(rules : set (sequent_rule V L))(n : nat),
      subset (GC_n_set n) (GRC_n_set rules n).

  Lemma G_n_subset_GRC_n :
    ∀(rules : set (sequent_rule V L))(n : nat),
      subset (G_n_set n) (GRC_n_set rules n).

  Lemma R_n_subset_GRC_n :
    ∀(rules : set (sequent_rule V L))(n : nat),
      subset (rank_rules n (weaken_subst_rule rules)) (GRC_n_set rules n).

  Lemma GRC_n_as_GR_C_union :
    ∀(rules : set (sequent_rule V L))(n : nat),
      set_equal (GRC_n_set rules n)
                (union (bounded_cut_rules V L n) (GR_n_set rules n)).

End Rule_sets.

Implicit Arguments const_rank_G_set [V L].
Implicit Arguments decompose_G_n_set_coarsly [V L].
Implicit Arguments decompose_G_n_set [V L].
Implicit Arguments other_context_G_n_set [V L].
Implicit Arguments sequent_other_context_G_n_set [V L].
Implicit Arguments smaller_context_G_n_set [V L].
Implicit Arguments one_step_rule [V L].
Implicit Arguments one_step_rule_set [V L].
Implicit Arguments one_step_rule_propositional_assumption [V L].
Implicit Arguments one_step_rule_nonempty_conclusion [V L].
Implicit Arguments one_step_rule_prop_modal_prop_conclusion [V L].
Implicit Arguments one_step_rule_incl_prop_var_sequent [V L].
Implicit Arguments weaken_subst_rule [V L].
Implicit Arguments GR_set [V L].
Implicit Arguments GR_n_set [V L].
Implicit Arguments GRC_set [V L].
Implicit Arguments GRC_n_set [V L].
Implicit Arguments GRC_n_set_struct_union [V L].
Implicit Arguments GRC_n_multiset [V L].