Require Export substitution.

Section Rules.

  Variable V : Type.
  Variable L : modal_operators.

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