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].