Different subsets of formulas and sequents
- simple modal formulas/sequents, S(Lambda(V)), possibly negated modal formulas with variables as arguments only
- prop_modal_prop, Prop(Lambda(V)), propositional formulas over modalities with variables as arguments only
- prop_modal formulas/sequents, Prop(Lambda(S)), propositional formulas over modalities with arbitrary arguments
- top_modal formulas/sequents, S(Lambda(S)), possibly negated modalities with arbitrary arguments
Require Export substitution.
Section Modal_formulas.
Variable V : Type.
Variable L : modal_operators.
need a decidable equality on propositional constants for some results
Definition simple_modal_form(f : lambda_formula V L) : Prop :=
match f with
| lf_modal op args ⇒ every_nth prop_form (list_of_counted_list args)
| _ ⇒ False
end.
Definition simple_modal_sequent(s : sequent V L) : Prop :=
every_nth (neg_form_maybe simple_modal_form) s.
Lemma simple_modal_sequent_empty : simple_modal_sequent [].
Lemma simple_modal_sequent_append :
∀(s1 s2 : sequent V L),
simple_modal_sequent s1 →
simple_modal_sequent s2 →
simple_modal_sequent (s1 ++ s2).
Lemma simple_modal_sequent_append_left :
∀(s1 s2 : sequent V L),
simple_modal_sequent (s1 ++ s2) → simple_modal_sequent s1.
Lemma simple_modal_sequent_append_right :
∀(s1 s2 : sequent V L),
simple_modal_sequent (s1 ++ s2) → simple_modal_sequent s2.
Lemma simple_modal_sequent_cons :
∀(f : lambda_formula V L)(s : sequent V L),
neg_form_maybe simple_modal_form f →
simple_modal_sequent s →
simple_modal_sequent (f :: s).
Lemma simple_modal_sequent_head :
∀(f : lambda_formula V L)(s : sequent V L),
simple_modal_sequent (f :: s) → neg_form_maybe simple_modal_form f.
Lemma simple_modal_sequent_tail :
∀(f : lambda_formula V L)(s : sequent V L),
simple_modal_sequent (f :: s) → simple_modal_sequent s.
Lemma simple_modal_sequent_list_reorder : ∀(s1 s2 : sequent V L),
list_reorder s1 s2 →
simple_modal_sequent s1 →
simple_modal_sequent s2.
Lemma simple_modal_sequent_cutout_nth : ∀(s : sequent V L)(n : nat),
simple_modal_sequent s → simple_modal_sequent (cutout_nth s n).
Lemma rank_formula_simple_modal_form :
∀(f : lambda_formula V L),
simple_modal_form f →
rank_formula 2 f.
Lemma rank_simple_modal_sequent : ∀(s : sequent V L),
simple_modal_sequent s → rank_sequent 2 s.
Lemma minimal_rank_simple_modal_sequent :
∀(n : nat)(s : sequent V L),
s ≠ [] →
simple_modal_sequent s →
rank_sequent n s →
1 < n.
Lemma rank_sequent_subst_simple_modal_sequent :
∀(s : sequent V L)(sigma : lambda_subst V L)(n : nat),
simple_modal_sequent s →
1 < n →
rank_subst (pred n) sigma →
rank_sequent n (subst_sequent sigma s).
Lemma rank_subst_limit_simple_modal_form :
∀(n : nat)(v : V)(sigma : lambda_subst V L)(f : lambda_formula V L),
neg_form_maybe simple_modal_form f →
In v (prop_var_formula f) →
rank_formula n (subst_form sigma f) →
rank_formula (pred n) (sigma v).
Lemma rank_subst_limit_subst_rule :
∀(n : nat)(s : sequent V L)(sigma : lambda_subst V L),
s ≠ [] →
simple_modal_sequent s →
rank_sequent n (subst_sequent sigma s) →
rank_subst (pred n) (limit_subst v_eq (prop_var_sequent s) sigma).
Lemma injective_subst_prop_form :
∀(sigma : lambda_subst V L)(f1 f2 : lambda_formula V L),
injective sigma →
prop_form f1 →
prop_form f2 →
subst_form sigma f1 = subst_form sigma f2 →
f1 = f2.
Lemma injective_subst_simple_modal :
∀(sigma : lambda_subst V L)(f1 f2 : lambda_formula V L),
injective sigma →
simple_modal_form f1 →
simple_modal_form f2 →
subst_form sigma f1 = subst_form sigma f2 →
f1 = f2.
Lemma injective_subst_neg_simple_modal :
∀(sigma : lambda_subst V L)(f1 f2 : lambda_formula V L),
injective sigma →
neg_form_maybe simple_modal_form f1 →
neg_form_maybe simple_modal_form f2 →
subst_form sigma f1 = subst_form sigma f2 →
f1 = f2.
Separete negated and unnegated formulas in simple modal sequents
Lemma simple_modal_sequent_partition : ∀(s : sequent V L),
simple_modal_sequent s →
∃(ms ns : sequent V L),
every_nth neg_form ns ∧
every_nth simple_modal_form ms ∧
list_reorder s (ms ++ ns).
Definition prop_modal_prop(f : lambda_formula V L) : Prop :=
neg_and_over simple_modal_form f.
Lemma prop_modal_prop_lambda_or :
∀(f1 f2 : lambda_formula V L),
prop_modal_prop f1 →
prop_modal_prop f2 →
prop_modal_prop (lambda_or f1 f2).
Lemma prop_modal_prop_tcc_prop : ∀{X : Type}(v : V),
prop_modal_prop (lf_prop v) → X.
Lemma prop_modal_prop_tcc_neg : ∀(f : lambda_formula V L),
prop_modal_prop (lf_neg f) → prop_modal_prop f.
Lemma prop_modal_prop_tcc_and_1 : ∀(f1 f2 : lambda_formula V L),
prop_modal_prop (lf_and f1 f2) → prop_modal_prop f1.
Lemma prop_modal_prop_tcc_and_2 : ∀(f1 f2 : lambda_formula V L),
prop_modal_prop (lf_and f1 f2) → prop_modal_prop f2.
Lemma prop_modal_prop_tcc_modal :
∀(op : operator L)
(args : counted_list (lambda_formula V L) (arity L op)),
prop_modal_prop (lf_modal op args) →
every_nth prop_form (list_of_counted_list args).
Lemma rank_formula_prop_modal_prop : ∀(f : lambda_formula V L),
prop_modal_prop f →
rank_formula 2 f.
Lemma simple_modal_form_is_prop_modal_prop :
∀(f : lambda_formula V L),
neg_form_maybe simple_modal_form f → prop_modal_prop f.
Definition prop_modal_prop_sequent(s : sequent V L) : Prop :=
every_nth prop_modal_prop s.
Lemma prop_modal_prop_sequent_append_left :
∀(s1 s2 : sequent V L),
prop_modal_prop_sequent (s1 ++ s2) → prop_modal_prop_sequent s1.
Lemma prop_modal_prop_sequent_append_right :
∀(s1 s2 : sequent V L),
prop_modal_prop_sequent (s1 ++ s2) → prop_modal_prop_sequent s2.
Lemma prop_modal_prop_sequent_cons :
∀(f : lambda_formula V L)(s : sequent V L),
prop_modal_prop f →
prop_modal_prop_sequent s →
prop_modal_prop_sequent (f :: s).
Lemma prop_modal_prop_sequent_head :
∀(f : lambda_formula V L)(s : sequent V L),
prop_modal_prop_sequent (f :: s) → prop_modal_prop f.
Lemma prop_modal_prop_sequent_tail :
∀(f : lambda_formula V L)(s : sequent V L),
prop_modal_prop_sequent (f :: s) → prop_modal_prop_sequent s.
Lemma prop_modal_prop_or_formula_iter :
∀(f : lambda_formula V L)(s : sequent V L),
prop_modal_prop_sequent (f :: s) →
prop_modal_prop (or_formula_of_sequent_iter f s).
Lemma prop_modal_prop_or_formula :
∀(s : sequent V L)(nonempty_s : s ≠ []),
prop_modal_prop_sequent s →
prop_modal_prop (or_formula_of_ne_sequent s nonempty_s).
Lemma simple_modal_sequent_is_prop_modal_prop :
∀(s : sequent V L),
simple_modal_sequent s → prop_modal_prop_sequent s.
Lemma rank_sequent_prop_modal_prop_sequent :
∀(s : sequent V L),
prop_modal_prop_sequent s →
rank_sequent 2 s.
Definition modal_form(f : lambda_formula V L) : Prop :=
match f with
| lf_modal _ _ ⇒ True
| _ ⇒ False
end.
Definition prop_modal(f : lambda_formula V L) : Prop :=
neg_and_over modal_form f.
Definition prop_modal_sequent(s : sequent V L) : Prop :=
every_nth prop_modal s.
Lemma prop_modal_sequent_cons :
∀(f : lambda_formula V L)(s : sequent V L),
prop_modal f →
prop_modal_sequent s →
prop_modal_sequent (f :: s).
Lemma prop_modal_sequent_head :
∀(f : lambda_formula V L)(s : sequent V L),
prop_modal_sequent (f :: s) → prop_modal f.
Lemma prop_modal_sequent_tail :
∀(f : lambda_formula V L)(s : sequent V L),
prop_modal_sequent (f :: s) → prop_modal_sequent s.
Definition top_modal_form(f : lambda_formula V L) : Prop :=
neg_form_maybe modal_form f.
Lemma top_modal_is_prop_modal : ∀(f : lambda_formula V L),
top_modal_form f → prop_modal f.
Lemma top_modal_form_lf_neg : ∀(f : lambda_formula V L),
top_modal_form (lf_neg f) → top_modal_form f.
Lemma top_modal_not_neg_prop : ∀(f : lambda_formula V L),
top_modal_form f → ¬ neg_form_maybe prop_form f.
Lemma top_modal_not_prop : ∀(f : lambda_formula V L),
top_modal_form f → ¬ prop_form f.
Definition top_modal_sequent(s : sequent V L) : Prop :=
every_nth top_modal_form s.
Lemma top_modal_sequent_list_reorder : ∀(s1 s2 : sequent V L),
list_reorder s1 s2 →
top_modal_sequent s2 →
top_modal_sequent s1.
Lemma top_modal_is_prop_modal_sequent : ∀(s : sequent V L),
top_modal_sequent s → prop_modal_sequent s.
Lemma top_modal_sequent_tail :
∀(f : lambda_formula V L)(s : sequent V L),
top_modal_sequent (f :: s) → top_modal_sequent s.
Lemma top_modal_sequent_head :
∀(f : lambda_formula V L)(s : sequent V L),
top_modal_sequent (f :: s) → top_modal_form f.
End Modal_formulas.
Implicit Arguments prop_modal_prop [[V] [L]].
Implicit Arguments prop_modal_prop_lambda_or [V L].
Implicit Arguments prop_modal_prop_tcc_prop [V L X].
Implicit Arguments prop_modal_prop_tcc_neg [V L].
Implicit Arguments prop_modal_prop_tcc_and_1 [V L].
Implicit Arguments prop_modal_prop_tcc_and_2 [V L].
Implicit Arguments prop_modal_prop_tcc_modal [V L].
Implicit Arguments prop_modal_prop_sequent [V L].
Implicit Arguments prop_modal_prop_sequent_append_left [V L].
Implicit Arguments prop_modal_prop_sequent_append_right [V L].
Implicit Arguments prop_modal_prop_sequent_head [V L].
Implicit Arguments prop_modal_prop_sequent_tail [V L].
Implicit Arguments prop_modal_prop_or_formula [V L].
Implicit Arguments simple_modal_sequent_is_prop_modal_prop [V L].
Implicit Arguments modal_form [[V] [L]].
Implicit Arguments prop_modal_sequent [V L].
Implicit Arguments top_modal_form [V L].
Implicit Arguments top_modal_sequent [V L].
Implicit Arguments simple_modal_form [[V] [L]].
Implicit Arguments simple_modal_sequent [V L].
Implicit Arguments simple_modal_sequent_append_left [V L].
Implicit Arguments simple_modal_sequent_append_right [V L].
Implicit Arguments simple_modal_sequent_head [V L].
Implicit Arguments simple_modal_sequent_tail [V L].
Implicit Arguments simple_modal_sequent_list_reorder [V L].
Implicit Arguments injective_subst_neg_simple_modal [V L].