Require Export rule_sets.

Section Propositional_rules.

  Variable V : Type.
  Variable L : modal_operators.

  Lemma propositional_add_context :
    ∀(sl sr s : sequent V L),
      propositional_sequent sl →
      propositional_sequent sr →
      propositional_sequent s →
        propositional_sequent (add_context sl sr s).

  Lemma propositional_add_context_propositional :
    ∀(sl sr s : sequent V L),
      propositional_sequent (add_context sl sr s) →
        propositional_sequent s.

  Lemma propositional_add_context_left :
    ∀(sl sr s : sequent V L),
      propositional_sequent (add_context sl sr s) →
        propositional_sequent sl.

  Lemma propositional_add_context_right :
    ∀(sl sr s : sequent V L),
      propositional_sequent (add_context sl sr s) →
        propositional_sequent sr.

  Definition propositional_rule(r : sequent_rule V L) : Prop :=
    rule_has_rank 1 r.

  Lemma prop_sequent_rule_ass_tcc :
    ∀(r : sequent_rule V L)(n : nat)(n_len : n < length (assumptions r)),
      propositional_rule r →
        propositional_sequent (nth (assumptions r) n n_len).

  Lemma prop_sequent_rule_concl_tcc : ∀(r : sequent_rule V L),
    propositional_rule r → propositional_sequent (conclusion r).

  Lemma propositional_rule_add_context_bare_rule :
    ∀(r : sequent_rule V L)(sl sr : sequent V L),
      propositional_rule (rule_add_context sl sr r) →
        propositional_rule r.

  Definition propositional_sequent_set(ss : sequent V L → Prop) : Prop :=
    ∀(s : sequent V L), ss s → propositional_sequent s.

  Lemma propositional_empty_sequent_set :
    propositional_sequent_set (empty_sequent_set V L).

  Definition propositional_rule_set(rules : sequent_rule V L → Prop) : Prop :=
    ∀(r : sequent_rule V L), rules r → propositional_rule r.

  Definition prop_G_set(r : sequent_rule V L) : Prop :=
    G_n_set V L 1 r.

  Lemma provable_depth_prop_list_reorder :
    ∀(d : nat)(s1 s2 : sequent V L),
      list_reorder s1 s2 →
      provable_at_depth prop_G_set (empty_sequent_set V L) d s1 →
        provable_at_depth prop_G_set (empty_sequent_set V L) d s2.

  Lemma provable_prop_G_hyp_list_reorder :
    ∀(hyp : set (sequent V L))(s1 s2 : sequent V L),
      sequent_multiset hyp →
      list_reorder s1 s2 →
      provable prop_G_set hyp s1 →
        provable prop_G_set hyp s2.

  Lemma prop_G_subset_Gn : ∀(n : nat),
    1 ≤ n → subset prop_G_set (G_n_set V L n).

  Lemma prop_G_subset_GR :
    ∀(rules : set (sequent_rule V L))(n : nat),
      1 ≤ n →
        subset prop_G_set (GR_n_set rules n).

  Lemma prop_G_subset_GRC :
    ∀(rules : set (sequent_rule V L))(n : nat),
      1 ≤ n →
        subset prop_G_set (GRC_n_set rules n).

  Lemma propositional_prop_G_set : propositional_rule_set prop_G_set.

  Lemma G_set_prop_set : ∀(r : sequent_rule V L),
    G_set V L r → propositional_sequent (conclusion r) →
      prop_G_set r.

  Lemma GR_1_is_G_prop :
    ∀(rules : set (sequent_rule V L)),
      one_step_rule_set rules →
        set_equal (GR_n_set rules 1) prop_G_set.

  Lemma GRC_1_is_GC_1 :
    ∀(rules : set (sequent_rule V L)),
      one_step_rule_set rules →
        set_equal (GRC_n_set rules 1) (GC_n_set V L 1).

  Definition prop_GC_set(r : sequent_rule V L) : Prop :=
    GC_n_set V L 1 r.

  Lemma prop_G_subset_prop_GC : subset prop_G_set prop_GC_set.

End Propositional_rules.

Implicit Arguments propositional_add_context [V L].
Implicit Arguments propositional_rule [V L].
Implicit Arguments prop_sequent_rule_ass_tcc [V L].
Implicit Arguments prop_sequent_rule_concl_tcc [V L].
Implicit Arguments propositional_rule_set [V L].
Implicit Arguments propositional_sequent_set [V L].
Implicit Arguments propositional_rule_add_context_bare_rule [V L].
Implicit Arguments propositional_add_context_left [V L].
Implicit Arguments propositional_add_context_right [V L].
Implicit Arguments propositional_prop_G_set [[V] [L]].
Implicit Arguments G_set_prop_set [V L].
Implicit Arguments propositional_empty_sequent_set [[V] [L]].
Implicit Arguments propositional_add_context_propositional [V L].