Propositional rules and rule sets

This module proves some utility results for propositional rules and defines the propositional rule sets G and GC.

Require Export rule_sets.

Section Propositional_rules.

  Variable V : Type.
  Variable L : modal_operators.

Results for propositional rules

  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 rpropositional_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 LProp) : Prop :=
    (s : sequent V L), ss spropositional_sequent s.

  Lemma propositional_empty_sequent_set :
    propositional_sequent_set (empty_sequent_set V L).

  Definition propositional_rule_set(rules : sequent_rule V LProp) : Prop :=
    (r : sequent_rule V L), rules rpropositional_rule r.

Propositional G rule set

  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.

Subset lemmas for G

  Lemma prop_G_subset_Gn : (n : nat),
    1 nsubset 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 rpropositional_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).

Propositional GC rule set

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