Require Export propositional_rules generic_cut inversion.

Section Propositional_properties.

  Variable V : Type.
  Variable L : modal_operators.


  Lemma G_non_atomic_axiom_head :
    ∀(hyp : set (sequent V L))(f : lambda_formula V L)(s : sequent V L),
      sequent_multiset hyp →
      propositional f →
      propositional_sequent s →
        provable (prop_G_set V L) hyp (f :: lf_neg f :: s).

  Definition head_contraction_closed(ss : set (sequent V L)) : Prop :=
    ∀(f : lambda_formula V L)(s : sequent V L),
      ss (f :: f :: s) → ss (f :: s).

  Lemma head_contraction_closed_empty :
    head_contraction_closed (empty_sequent_set V L).

  Lemma G_n_contraction_head_ax :
    ∀(hyp : set (sequent V L))
          (n d : nat)(f : lambda_formula V L)(s : sequent V L),
      simple_tautology (f :: f :: s) →
      rank_sequent n (f :: f :: s) →
        provable_at_depth (G_n_set V L n) hyp (S d) (f :: s).

  Lemma G_n_contraction_and_assumptions_head :
    ∀(hyp : set (sequent V L))(n d : nat)(f g1 g2 : lambda_formula V L)
          (s : sequent V L)(br : sequent_rule V L)
          (subproofs : dep_list (sequent V L) (proof (G_n_set V L n) hyp)
                                (map (add_context [f] s) (assumptions br))),
      conj_head_inversion_closed hyp →
      (∀(s : sequent V L),
         provable_at_depth (G_n_set V L n) hyp d s →
         ∀(s_tl : sequent V L)(f : lambda_formula V L),
           s = f :: f :: s_tl →
             provable_at_depth (G_n_set V L n) hyp d (f :: s_tl)) →
      br = bare_and_rule g1 g2 →
      [f] = conclusion br →
      every_dep_nth
             (fun(s : sequent V L)(p : proof (G_n_set V L n) hyp s) ⇒
                 proof_depth p ≤ d)
             (map (add_context [f] s) (assumptions br))
             subproofs →
        every_nth (provable_at_depth (G_n_set V L n) hyp d)
                  (map (add_context [] s) (assumptions br)).

  Lemma G_n_contraction_neg_and_assumptions_head :
    ∀(hyp : set (sequent V L))(n d : nat)(f g1 g2 : lambda_formula V L)
          (s : sequent V L)(br : sequent_rule V L)
          (subproofs : dep_list (sequent V L) (proof (G_n_set V L n) hyp)
                                (map (add_context [f] s) (assumptions br))),
      sequent_multiset hyp →
      disj_head_inversion_closed hyp →
      (∀(s : sequent V L),
         provable_at_depth (G_n_set V L n) hyp d s →
         ∀(s_tl : sequent V L)(f : lambda_formula V L),
           s = f :: f :: s_tl →
             provable_at_depth (G_n_set V L n) hyp d (f :: s_tl)) →
      br = bare_neg_and_rule g1 g2 →
      [f] = conclusion br →
      every_dep_nth
            (fun(s : sequent V L)(p : proof (G_n_set V L n) hyp s) ⇒
                proof_depth p ≤ d)
            (map (add_context [f] s) (assumptions br)) subproofs →
        every_nth (provable_at_depth (G_n_set V L n) hyp d)
          (map (add_context [] s) (assumptions br)).

  Lemma G_n_contraction_neg_neg_assumptions_head :
    ∀(hyp : set (sequent V L))(n d : nat)(f g : lambda_formula V L)
          (s : sequent V L)(br : sequent_rule V L)
          (subproofs : dep_list (sequent V L) (proof (G_n_set V L n) hyp)
                                (map (add_context [f] s) (assumptions br))),
      neg_head_inversion_closed hyp →
      (∀(s : sequent V L),
         provable_at_depth (G_n_set V L n) hyp d s →
         ∀(s_tl : sequent V L)(f : lambda_formula V L),
           s = f :: f :: s_tl →
             provable_at_depth (G_n_set V L n) hyp d (f :: s_tl)) →
      br = bare_neg_neg_rule g →
      [f] = conclusion br →
      every_dep_nth
           (fun(s : sequent V L)(p : proof (G_n_set V L n) hyp s) ⇒
               proof_depth p ≤ d)
           (map (add_context [f] s) (assumptions br)) subproofs →
        every_nth (provable_at_depth (G_n_set V L n) hyp d)
          (map (add_context [] s) (assumptions br)).

  Lemma G_n_contraction_head :
    ∀(hyp : set (sequent V L))(n : nat)
          (f : lambda_formula V L)(s : sequent V L),
      sequent_multiset hyp →
      head_inversion_closed hyp →
      head_contraction_closed hyp →
      provable (G_n_set V L n) hyp (f :: f :: s) →
        provable (G_n_set V L n) hyp (f :: s).

  Lemma prop_contraction_head :
    ∀(f : lambda_formula V L)(s : sequent V L),
      provable (prop_G_set V L) (empty_sequent_set V L) (f :: f :: s) →
        provable (prop_G_set V L) (empty_sequent_set V L) (f :: s).

  Lemma G_n_hyp_list_contraction_left :
    ∀(n : nat)(hyp : set (sequent V L))(r s : sequent V L),
      sequent_multiset hyp →
      head_inversion_closed hyp →
      head_contraction_closed hyp →
      provable (G_n_set V L n) hyp (r ++ r ++ s) →
        provable (G_n_set V L n) hyp (r ++ s).

  Lemma G_n_cut_elim_head_ax :
    ∀(n : nat)(hyp : set (sequent V L))
          (f : lambda_formula V L)(q r : sequent V L),
      rank_sequent_set n hyp →
      sequent_multiset hyp →
      bounded_weakening_closed n hyp →
      neg_head_inversion_closed hyp →
      rank_sequent n q →
      simple_tautology (f :: q) →
      provable (G_n_set V L n) hyp ((lf_neg f) :: r) →
        provable (G_n_set V L n) hyp (q ++ r).

  Lemma G_n_cut_elim_head_and_inside :
    ∀(n m d : nat)(hyp : set (sequent V L))
          (f g1 g2 : lambda_formula V L)(r q : sequent V L)
          (brule : sequent_rule V L),
      sequent_multiset hyp →
      head_inversion_closed hyp →
      head_contraction_closed hyp →
      (∀(f : lambda_formula V L)(q r : sequent V L),
         formula_measure f < m →
         provable (G_n_set V L n) hyp (f :: q) →
         provable (G_n_set V L n) hyp (lf_neg f :: r) →
           provable (G_n_set V L n) hyp (q ++ r)) →
      formula_measure f < S m →
      provable (G_n_set V L n) hyp (lf_neg f :: r) →
      every_nth (provable (G_n_set V L n) hyp)
                (map (add_context [] q) (assumptions brule)) →
      brule = bare_and_rule g1 g2 →
      [f] = conclusion brule →
        provable (G_n_set V L n) hyp (q ++ r).

  Lemma G_n_cut_elim_head_neg_and_inside :
    ∀(n m : nat)(hyp : set (sequent V L))
          (f g1 g2 : lambda_formula V L)(r q : sequent V L)
          (brule : sequent_rule V L),
      sequent_multiset hyp →
      head_inversion_closed hyp →
      (∀(f : lambda_formula V L)(q r : sequent V L),
         formula_measure f < m →
         provable (G_n_set V L n) hyp (f :: q) →
         provable (G_n_set V L n) hyp (lf_neg f :: r) →
           provable (G_n_set V L n) hyp (q ++ r)) →
      formula_measure f < S m →
      provable (G_n_set V L n) hyp (f :: q) →
      provable (G_n_set V L n) hyp (lf_neg f :: r) →
      brule = bare_neg_and_rule g1 g2 →
      [f] = conclusion brule →
        provable (G_n_set V L n) hyp (q ++ r).

  Lemma G_n_cut_elim_head_neg_neg_inside :
    ∀(n m : nat)(hyp : set (sequent V L))
          (f : lambda_formula V L)(r q : sequent V L),
      sequent_multiset hyp →
      head_inversion_closed hyp →
      (∀(f : lambda_formula V L)(q r : sequent V L),
        formula_measure f < m →
        provable (G_n_set V L n) hyp (f :: q) →
        provable (G_n_set V L n) hyp (lf_neg f :: r) →
          provable (G_n_set V L n) hyp (q ++ r)) →
      formula_measure (lf_neg f) < S m →
      provable (G_n_set V L n) hyp (lf_neg f :: q) →
      provable (G_n_set V L n) hyp (lf_neg (lf_neg f) :: r) →
        provable (G_n_set V L n) hyp (q ++ r).

  Lemma G_n_cut_elim_head_and_outside :
    ∀(n d : nat)(hyp : set (sequent V L))
          (f1 f2 g1 g2 : lambda_formula V L)(sl sr r : sequent V L)
          (brule : sequent_rule V L),
      (∀(q : sequent V L),
         provable_at_depth (G_n_set V L n) hyp d (f1 :: q) →
           provable (G_n_set V L n) hyp (q ++ r)) →
      provable (G_n_set V L n) hyp (f2 :: r) →
      every_nth (provable_at_depth (G_n_set V L n) hyp d)
                (map (add_context (f1 :: sl) sr) (assumptions brule)) →
      brule = bare_and_rule g1 g2 →
        every_nth (provable (G_n_set V L n) hyp)
                  (map (add_context sl (sr ++ r)) (assumptions brule)).

  Lemma G_n_cut_elim_head_neg_and_outside :
    ∀(n d : nat)(hyp : set (sequent V L))
          (f1 f2 g1 g2 : lambda_formula V L)(sl sr r : sequent V L)
          (brule : sequent_rule V L),
      (∀(q : sequent V L),
         provable_at_depth (G_n_set V L n) hyp d (f1 :: q) →
           provable (G_n_set V L n) hyp (q ++ r)) →
      provable (G_n_set V L n) hyp (f2 :: r) →
      every_nth (provable_at_depth (G_n_set V L n) hyp d)
                (map (add_context (f1 :: sl) sr) (assumptions brule)) →
      brule = bare_neg_and_rule g1 g2 →
        every_nth (provable (G_n_set V L n) hyp)
                  (map (add_context sl (sr ++ r)) (assumptions brule)).

  Lemma G_n_cut_elim_head_neg_neg_outside :
    ∀(n d : nat)(hyp : set (sequent V L))
          (f1 f2 g : lambda_formula V L)(sl sr r : sequent V L)
          (brule : sequent_rule V L),
      (∀(q : sequent V L),
         provable_at_depth (G_n_set V L n) hyp d (f1 :: q) →
           provable (G_n_set V L n) hyp (q ++ r)) →
      provable (G_n_set V L n) hyp (f2 :: r) →
      every_nth (provable_at_depth (G_n_set V L n) hyp d)
                (map (add_context (f1 :: sl) sr) (assumptions brule)) →
      brule = bare_neg_neg_rule g →
        every_nth (provable (G_n_set V L n) hyp)
                  (map (add_context sl (sr ++ r)) (assumptions brule)).

  Lemma prop_G_cut_elim_head_ind :
    ∀(n : nat)(f : lambda_formula V L)(q r : sequent V L),
      formula_measure f < n →
      provable (prop_G_set V L) (empty_sequent_set V L) (f :: q) →
      provable (prop_G_set V L) (empty_sequent_set V L) ((lf_neg f) :: r) →
        provable (prop_G_set V L) (empty_sequent_set V L) (q ++ r).

  Lemma prop_G_cut_elim_head :
    ∀(f : lambda_formula V L)(q r : sequent V L),
      provable (prop_G_set V L) (empty_sequent_set V L) (f :: q) →
      provable (prop_G_set V L) (empty_sequent_set V L) ((lf_neg f) :: r) →
        provable (prop_G_set V L) (empty_sequent_set V L) (q ++ r).

  Lemma admissible_bounded_cut_prop_G :
    admissible_rule_set (prop_G_set V L) (empty_sequent_set V L)
                        (bounded_cut_rules V L 1).

  Lemma provable_GC_1_G_1 : ∀(s : sequent V L),
    provable (GC_n_set V L 1) (empty_sequent_set V L) s →
      provable (G_n_set V L 1) (empty_sequent_set V L) s.

  Lemma provable_GRC_1_GR_1 :
    ∀(rules : set (sequent_rule V L))(s : sequent V L),
      one_step_rule_set rules →
      provable (GRC_n_set rules 1) (empty_sequent_set V L) s →
        provable (GR_n_set rules 1) (empty_sequent_set V L) s.

  Lemma propositional_cut_contraction_weakening :
    ∀(hyp : set (sequent V L))(os cs : sequent V L),
      sequent_multiset hyp →
      rank_sequent_set 1 hyp →
      incl os cs →
      os ≠ [] →
      propositional_sequent cs →
      provable (prop_GC_set V L) hyp os →
        provable (prop_GC_set V L) hyp cs.

End Propositional_properties.

Implicit Arguments head_contraction_closed [V L].