Completeness and semantic cut elimination, Section 4
Non-decomposable formulas
Require Export dsets build_prop_proof.
Section Prop_mod.
Variable V : Type.
Variable L : modal_operators.
Need a decidable equality on propositional constants for
the properties on the proof built oracle.
Definition dneg_form_maybe(F : dset (lambda_formula V L))
: dset (lambda_formula V L) :=
fun(f : lambda_formula V L) ⇒
match f with
| lf_neg f ⇒ F f
| _ ⇒ F f
end.
Definition dprop_or_mod_formula : dset (lambda_formula V L) :=
dunion (dneg_form_maybe is_prop) (dneg_form_maybe is_modal).
Definition dprop_or_mod_sequent : dset (sequent V L) :=
forallb dprop_or_mod_formula.
: dset (lambda_formula V L) :=
fun(f : lambda_formula V L) ⇒
match f with
| lf_neg f ⇒ F f
| _ ⇒ F f
end.
Definition dprop_or_mod_formula : dset (lambda_formula V L) :=
dunion (dneg_form_maybe is_prop) (dneg_form_maybe is_modal).
Definition dprop_or_mod_sequent : dset (sequent V L) :=
forallb dprop_or_mod_formula.
Definition prop_or_mod_formula : set (lambda_formula V L) :=
union (neg_form_maybe prop_form) (@top_modal_form V L).
Lemma simple_prop_from_prop : ∀(f : lambda_formula V L),
neg_form_maybe prop_form f ↔ dneg_form_maybe is_prop f = true.
Lemma simple_modal_from_prop : ∀(f : lambda_formula V L),
top_modal_form f ↔ dneg_form_maybe is_modal f = true.
Lemma prop_or_mod_formula_prop : ∀(f : lambda_formula V L),
prop_or_mod_formula f ↔ dprop_or_mod_formula f = true.
Definition prop_or_mod_sequent : set (sequent V L) :=
every_nth prop_or_mod_formula.
Lemma prop_or_mod_sequent_empty : prop_or_mod_sequent [].
Lemma prop_or_mod_sequent_cons :
∀(f : lambda_formula V L)(s : sequent V L),
prop_or_mod_sequent (f :: s) ↔
prop_or_mod_formula f ∧ prop_or_mod_sequent s.
Lemma prop_or_mod_sequent_list_reorder : ∀(s1 s2 : sequent V L),
list_reorder s1 s2 →
prop_or_mod_sequent s1 →
prop_or_mod_sequent s2.
Lemma prop_or_mod_sequent_append_left : ∀(s1 s2 : sequent V L),
prop_or_mod_sequent (s1 ++ s2) → prop_or_mod_sequent s1.
Lemma prop_or_mod_sequent_append_right : ∀(s1 s2 : sequent V L),
prop_or_mod_sequent (s1 ++ s2) → prop_or_mod_sequent s2.
Lemma prop_or_mod_sequent_prop : ∀(s : sequent V L),
prop_or_mod_sequent s ↔ dprop_or_mod_sequent s = true.
Lemma non_decomposable_is_prop_mod : ∀(s : sequent V L),
prop_G_oracle v_eq s = None → prop_or_mod_sequent s.
Lemma prop_or_mod_partition : ∀(s : sequent V L),
prop_or_mod_sequent s →
∃(prop_s mod_s : sequent V L),
prop_sequent prop_s ∧
top_modal_sequent mod_s ∧
list_reorder s (mod_s ++ prop_s).
End Prop_mod.
Implicit Arguments dprop_or_mod_sequent [V L].
Implicit Arguments prop_or_mod_sequent_prop [V L].
Implicit Arguments prop_or_mod_partition [V L].