Various rules
Definition add_context(sl sr s : sequent V L) : sequent V L := sl ++ s ++ sr.
Definition rule_add_context(sl sr : sequent V L)
(r : sequent_rule V L) : sequent_rule V L :=
{| assumptions := map (add_context sl sr) r.(assumptions);
conclusion := add_context sl sr r.(conclusion)
|}.
Lemma rank_rule_add_context_rev :
∀(sl sr : sequent V L)(r : sequent_rule V L)(n : nat),
rule_has_rank n (rule_add_context sl sr r) →
rule_has_rank n r.
Lemma reorder_rule_add_context :
∀(r : sequent_rule V L)(s : sequent V L)(sl0 sr0 : sequent V L),
list_reorder (add_context sl0 sr0 (conclusion r)) s →
length (conclusion r) = 1 →
∃(sl1 sr1 : sequent V L),
reordered_rule (rule_add_context sl0 sr0 r) s
(rule_add_context sl1 sr1 r).
Lemma const_rank_add_context :
∀(n : nat)(sl sr : sequent V L)(r rc : sequent_rule V L),
rc = rule_add_context sl sr r →
(rank_sequent n (conclusion r) →
every_nth (rank_sequent n) (assumptions r)) →
rank_sequent n (conclusion rc) →
every_nth (rank_sequent n) (assumptions rc).
Definition simple_tautology_witness(l : sequent V L)
(n1 n2 : nat)(v : V) : Prop :=
n1_less # n1 < length l /#\
n2_less # n2 < length l /#\
nth l n1 n1_less = lf_prop v ∧
nth l n2 n2_less = lf_neg (lf_prop v).
Definition simple_tautology(l : sequent V L) : Prop :=
∃ n1 : nat, ∃ n2 : nat, ∃ v : V,
simple_tautology_witness l n1 n2 v.
Lemma simple_tautology_cons :
∀(s : sequent V L)(f : lambda_formula V L),
simple_tautology s → simple_tautology (f :: s).
Lemma simple_tautology_append_left :
∀(s1 s2 : sequent V L),
simple_tautology s2 → simple_tautology (s1 ++ s2).
Lemma simple_tautology_tail :
∀(s : sequent V L)(f : lambda_formula V L),
simple_tautology (f :: s) →
(not (neg_form_maybe prop_form f)) →
simple_tautology s.
Lemma simple_tautology_reorder : ∀(s1 s2 : sequent V L),
simple_tautology s1 → list_reorder s1 s2 → simple_tautology s2.
Lemma simple_tautology_append_right :
∀(s1 s2 : sequent V L),
simple_tautology s1 → simple_tautology (s1 ++ s2).
Lemma simple_tautology_cons_destruct :
∀(f : lambda_formula V L)(s : sequent V L),
simple_tautology (f :: s) →
simple_tautology s ∨
(∃(sr : sequent V L),
list_reorder s ((lf_neg f) :: sr) ∧ prop_form f) ∨
(∃(g : lambda_formula V L)(sr : sequent V L),
f = lf_neg g ∧
list_reorder s (g :: sr) ∧
prop_form g).
Lemma simple_tautology_contract_head :
∀(f : lambda_formula V L)(s : sequent V L),
simple_tautology (f :: f :: s) → simple_tautology (f :: s).
Definition is_ax_rule(r : sequent_rule V L) : Prop :=
assumptions r = [] ∧ simple_tautology (conclusion r).
Lemma ax_rule_no_empty_conclusion : ∀(r : sequent_rule V L),
is_ax_rule r → conclusion r ≠ [].
Definition is_and_rule(r : sequent_rule V L) : Prop :=
∃(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.
Definition bare_and_rule(f1 f2 : lambda_formula V L) : sequent_rule V L :=
{| assumptions := [[f1]; [f2]];
conclusion := [lf_and f1 f2]
|}.
Lemma and_rule_context :
∀(r : sequent_rule V L),
is_and_rule r →
∃(sl sr : sequent V L)(f1 f2 : lambda_formula V L),
r = rule_add_context sl sr (bare_and_rule f1 f2).
Lemma context_and_rule :
∀(sl sr : sequent V L)(f1 f2 : lambda_formula V L),
is_and_rule (rule_add_context sl sr (bare_and_rule f1 f2)).
Lemma const_rank_and_rule :
∀(n : nat)(f1 f2 : lambda_formula V L),
rank_sequent n [lf_and f1 f2] →
every_nth (rank_sequent n) [[f1]; [f2]].
Lemma const_rank_and_rule_left_context :
∀(n : nat)(sl sr : sequent V L)(f1 f2 : lambda_formula V L),
rank_sequent n (sl ++ (lf_and f1 f2) :: sr) →
rank_sequent n (sl ++ f1 :: sr).
Lemma const_rank_and_rule_right_context :
∀(n : nat)(sl sr : sequent V L)(f1 f2 : lambda_formula V L),
rank_sequent n (sl ++ (lf_and f1 f2) :: sr) →
rank_sequent n (sl ++ f2 :: sr).
Lemma subst_closed_and : subst_closed_rule_set is_and_rule.
Lemma and_rule_no_empty_conclusion : ∀(r : sequent_rule V L),
is_and_rule r → conclusion r ≠ [].
Definition is_neg_and_rule(r : sequent_rule V L) : Prop :=
∃(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.
Definition bare_neg_and_rule(f1 f2 : lambda_formula V L) : sequent_rule V L :=
{| assumptions := [[lf_neg f1; lf_neg f2]];
conclusion := [lf_neg (lf_and f1 f2)]
|}.
Lemma neg_and_rule_context :
∀(r : sequent_rule V L),
is_neg_and_rule r →
∃(sl sr : sequent V L)(f1 f2 : lambda_formula V L),
r = rule_add_context sl sr (bare_neg_and_rule f1 f2).
Lemma context_neg_and_rule :
∀(sl sr : sequent V L)(f1 f2 : lambda_formula V L),
is_neg_and_rule (rule_add_context sl sr (bare_neg_and_rule f1 f2)).
Lemma const_rank_neg_and_rule :
∀(n : nat)(f1 f2 : lambda_formula V L),
rank_sequent n [lf_neg (lf_and f1 f2)] →
every_nth (rank_sequent n) [[lf_neg f1; lf_neg f2]].
Lemma const_rank_neg_and_rule_context :
∀(n : nat)(sl sr : sequent V L)(f1 f2 : lambda_formula V L),
rank_sequent n (sl ++ (lf_neg (lf_and f1 f2)) :: sr) →
rank_sequent n (sl ++ (lf_neg f1) :: (lf_neg f2) :: sr).
Lemma subst_closed_neg_and : subst_closed_rule_set is_neg_and_rule.
Lemma neg_and_rule_no_empty_conclusion : ∀(r : sequent_rule V L),
is_neg_and_rule r → conclusion r ≠ [].
Definition is_neg_neg_rule(r : sequent_rule V L) : Prop :=
∃(sl sr : sequent V L)(f : lambda_formula V L),
assumptions r = [sl ++ f :: sr] ∧
conclusion r = sl ++ (lf_neg (lf_neg f)) :: sr.
Definition bare_neg_neg_rule(f : lambda_formula V L) : sequent_rule V L :=
{| assumptions := [[f]];
conclusion := [lf_neg (lf_neg f)]
|}.
Lemma neg_neg_rule_context :
∀(r : sequent_rule V L),
is_neg_neg_rule r →
∃(sl sr : sequent V L)(f : lambda_formula V L),
r = rule_add_context sl sr (bare_neg_neg_rule f).
Lemma context_neg_neg_rule :
∀(sl sr : sequent V L)(f : lambda_formula V L),
is_neg_neg_rule (rule_add_context sl sr (bare_neg_neg_rule f)).
Lemma const_rank_neg_neg_rule :
∀(n : nat)(f : lambda_formula V L),
rank_sequent n [lf_neg (lf_neg f)] →
every_nth (rank_sequent n) [[f]].
Lemma const_rank_neg_neg_rule_context :
∀(n : nat)(sl sr : sequent V L)(f : lambda_formula V L),
rank_sequent n (sl ++ (lf_neg (lf_neg f)) :: sr) →
rank_sequent n (sl ++ f :: sr).
Lemma subst_closed_neg_neg : subst_closed_rule_set is_neg_neg_rule.
Lemma neg_neg_rule_no_empty_conclusion : ∀(r : sequent_rule V L),
is_neg_neg_rule r → conclusion r ≠ [].
Definition tautology_witness(s : sequent V L)(n1 n2 : nat) : Prop :=
n1_less # n1 < length s /#\
n2_less # n2 < length s /#\
nth s n1 n1_less = lf_neg (nth s n2 n2_less).
Definition subst_Ax_set(sigma : lambda_subst V L)(s : sequent V L) : Prop :=
∃(v : V), s = [sigma v; lf_neg (sigma v)].
Lemma rank_sequent_subst_Ax_set :
∀(k : nat)(sigma : lambda_subst V L)(s : sequent V L),
rank_subst k sigma →
subst_Ax_set sigma s →
rank_sequent k s.
Definition subst_Ax_n_set(sigma : lambda_subst V L)(n : nat)
(s : sequent V L) : Prop :=
∃(ax delta : sequent V L),
subst_Ax_set sigma ax ∧
list_reorder (ax ++ delta) s ∧
rank_sequent n delta.
Lemma ax_rule_subst :
∀(r : sequent_rule V L)(sigma : lambda_subst V L)(n k : nat),
rank_subst (S k) sigma →
rank_rules n is_ax_rule r →
subst_Ax_n_set sigma (n + k) (subst_sequent sigma (conclusion r)).
Definition is_cut_rule(r : sequent_rule V L) : Prop :=
∃(gamma_l gamma_r delta_l delta_r : sequent V L)
(f : lambda_formula V L),
assumptions r = [gamma_l ++ f :: gamma_r;
delta_l ++ (lf_neg f) :: delta_r] ∧
list_reorder (conclusion r) (gamma_l ++ gamma_r ++ delta_l ++ delta_r).
Lemma cut_rule_multiset : rule_multiset is_cut_rule.
Lemma const_rank_cut_rule_left :
∀(n : nat)(gl gr dl dr : sequent V L)(f : lambda_formula V L),
rank_formula n f →
rank_sequent n (gl ++ gr ++ dl ++ dr) →
rank_sequent n (gl ++ f :: gr).
Lemma const_rank_cut_rule_right :
∀(n : nat)(gl gr dl dr : sequent V L)(f : lambda_formula V L),
rank_formula n f →
rank_sequent n (gl ++ gr ++ dl ++ dr) →
rank_sequent n (dl ++ (lf_neg f) :: dr).
Lemma subst_cut_rule : subst_closed_rule_set is_cut_rule.
Definition bounded_cut_rules(n : nat) : set (sequent_rule V L) :=
rank_rules n is_cut_rule.
Definition bounded_weakening_rules(n : nat)(r : sequent_rule V L) : Prop :=
∃(s : sequent V L)(f : lambda_formula V L),
rank_formula n f ∧
rank_sequent n s ∧
assumptions r = [s] ∧
list_reorder (conclusion r) (f :: s).
Lemma rank_conclusion_bounded_weakening_rule :
∀(n : nat)(r : sequent_rule V L),
bounded_weakening_rules n r →
rank_sequent n (conclusion r).
Lemma rank_assumptions_bounded_weakening_rule :
∀(n : nat)(r : sequent_rule V L),
bounded_weakening_rules n r →
every_nth (rank_sequent n) (assumptions r).
Lemma bounded_weakening_rules_multiset : ∀(n : nat),
rule_multiset (bounded_weakening_rules n).
Definition bounded_weakening_closed(n : nat)(ss : set (sequent V L))
: Prop :=
∀(s r : sequent V L)(f : lambda_formula V L),
ss s → rank_formula n f → list_reorder r (f :: s) → ss r.
Lemma bounded_weakening_closed_empty : ∀(n : nat),
bounded_weakening_closed n (empty_sequent_set V L).
Definition full_weakening_rules(r : sequent_rule V L) : Prop :=
∃(s : sequent V L)(f : lambda_formula V L),
assumptions r = [s] ∧
list_reorder (conclusion r) (f :: s).
Lemma full_weakening_rules_multiset : rule_multiset full_weakening_rules.
Definition full_weakening_closed(ss : set (sequent V L)) : Prop :=
∀(s r : sequent V L)(f : lambda_formula V L),
ss s → list_reorder r (f :: s) → ss r.
Lemma bounded_full_weakening :
∀(r : sequent_rule V L),
full_weakening_rules r →
bounded_weakening_rules (minimal_rule_rank r) r.
Lemma full_weakening_rules_nonempty_conclusion :
∀(r : sequent_rule V L),
full_weakening_rules r →
conclusion r ≠ [].
Definition inverted_and_left_rule(r : sequent_rule V L) : Prop :=
∃(sl sr : sequent V L)(f1 f2 : lambda_formula V L),
assumptions r = [sl ++ (lf_and f1 f2) :: sr] ∧
conclusion r = sl ++ f1 :: sr.
Definition bare_inverted_and_left_rule(f1 f2 : lambda_formula V L)
: sequent_rule V L :=
{| assumptions := [[lf_and f1 f2]];
conclusion := [f1]
|}.
Lemma inverted_and_left_rule_context :
∀(r : sequent_rule V L),
inverted_and_left_rule r →
∃(sl sr : sequent V L)(f1 f2 : lambda_formula V L),
r = rule_add_context sl sr (bare_inverted_and_left_rule f1 f2).
Lemma context_inverted_and_left_rule :
∀(sl sr : sequent V L)(f1 f2 : lambda_formula V L),
inverted_and_left_rule
(rule_add_context sl sr (bare_inverted_and_left_rule f1 f2)).
Definition inverted_and_right_rule(r : sequent_rule V L) : Prop :=
∃(sl sr : sequent V L)(f1 f2 : lambda_formula V L),
assumptions r = [sl ++ (lf_and f1 f2) :: sr] ∧
conclusion r = sl ++ f2 :: sr.
Definition bare_inverted_and_right_rule(f1 f2 : lambda_formula V L)
: sequent_rule V L :=
{| assumptions := [[lf_and f1 f2]];
conclusion := [f2]
|}.
Lemma inverted_and_right_rule_context :
∀(r : sequent_rule V L),
inverted_and_right_rule r →
∃(sl sr : sequent V L)(f1 f2 : lambda_formula V L),
r = rule_add_context sl sr (bare_inverted_and_right_rule f1 f2).
Lemma context_inverted_and_right_rule :
∀(sl sr : sequent V L)(f1 f2 : lambda_formula V L),
inverted_and_right_rule
(rule_add_context sl sr (bare_inverted_and_right_rule f1 f2)).
Definition inverted_or_rule(r : sequent_rule V L) : Prop :=
∃(sl sm sr : sequent V L)(f1 f2 : lambda_formula V L),
assumptions r = [sl ++ (lf_neg (lf_and f1 f2)) :: sm ++ sr] ∧
(conclusion r = sl ++ (lf_neg f1) :: sm ++ (lf_neg f2) :: sr ∨
conclusion r = sl ++ (lf_neg f2) :: sm ++ (lf_neg f1) :: sr).
Lemma inverted_or_left_reordered_rule :
∀(or : sequent_rule V L)(rc sl sm sr : sequent V L)
(f1 f2 : lambda_formula V L),
list_reorder (conclusion or) rc →
assumptions or = [sl ++ (lf_neg (lf_and f1 f2)) :: sm ++ sr] →
conclusion or = sl ++ (lf_neg f1) :: sm ++ (lf_neg f2) :: sr →
∃(rr : sequent_rule V L),
reordered_rule or rc rr ∧ inverted_or_rule rr.
Definition inverted_or_rule_multiset : rule_multiset inverted_or_rule.
Definition inverted_neg_rule(r : sequent_rule V L) : Prop :=
∃(sl sr : sequent V L)(f : lambda_formula V L),
assumptions r = [sl ++ (lf_neg (lf_neg f)) :: sr] ∧
conclusion r = sl ++ f :: sr.
Definition bare_inverted_neg_rule(f : lambda_formula V L)
: sequent_rule V L :=
{| assumptions := [[lf_neg (lf_neg f)]];
conclusion := [f]
|}.
Lemma inverted_neg_rule_context :
∀(r : sequent_rule V L),
inverted_neg_rule r →
∃(sl sr : sequent V L)(f : lambda_formula V L),
r = rule_add_context sl sr (bare_inverted_neg_rule f).
Lemma context_inverted_neg_rule :
∀(sl sr : sequent V L)(f : lambda_formula V L),
inverted_neg_rule
(rule_add_context sl sr (bare_inverted_neg_rule f)).
Definition inversion_rules(r : sequent_rule V L) : Prop :=
inverted_and_left_rule r ∨ inverted_and_right_rule r ∨
inverted_or_rule r ∨ inverted_neg_rule r.
Lemma inversion_rules_multiset : rule_multiset inversion_rules.
Lemma inversion_rules_nonempty_conclusion : ∀(r : sequent_rule V L),
inversion_rules r →
conclusion r ≠ [].
Definition is_contraction_rule(r : sequent_rule V L) : Prop :=
∃(n : nat),
n_less # n < length (conclusion r) /#\
assumptions r = [(nth (conclusion r) n n_less) :: (conclusion r)].
Lemma contraction_rule_multiset : rule_multiset is_contraction_rule.
End Rules.
Implicit Arguments simple_tautology_witness [V L].
Implicit Arguments simple_tautology [[V] [L]].
Implicit Arguments simple_tautology_cons [V L].
Implicit Arguments add_context [V L].
Implicit Arguments rule_add_context [V L].
Implicit Arguments rank_rule_add_context_rev [V L].
Implicit Arguments reorder_rule_add_context [V L].
Implicit Arguments rank_sequent_subst_Ax_set [V L].
Implicit Arguments is_ax_rule [[V] [L]].
Implicit Arguments is_and_rule [[V] [L]].
Implicit Arguments bare_and_rule [V L].
Implicit Arguments and_rule_context [V L].
Implicit Arguments is_neg_and_rule [[V] [L]].
Implicit Arguments bare_neg_and_rule [V L].
Implicit Arguments neg_and_rule_context [V L].
Implicit Arguments is_neg_neg_rule [[V] [L]].
Implicit Arguments bare_neg_neg_rule [V L].
Implicit Arguments neg_neg_rule_context [V L].
Implicit Arguments tautology_witness [V L].
Implicit Arguments subst_Ax_set [V L].
Implicit Arguments subst_Ax_n_set [V L].
Implicit Arguments is_cut_rule [[V] [L]].
Implicit Arguments bounded_weakening_closed [V L].
Implicit Arguments full_weakening_closed [V L].
Implicit Arguments inverted_and_left_rule [V L].
Implicit Arguments inverted_and_right_rule [V L].
Implicit Arguments inverted_or_rule [V L].
Implicit Arguments inverted_neg_rule [V L].
Implicit Arguments is_contraction_rule [[V] [L]].