Logic library
Sequent support
Require Export list_support modal_formulas.
Section Sequent_support.
Variable V : Type.
Variable L : modal_operators.
Variable op_eq : eq_type (operator L).
Variable v_eq : eq_type V.
Fixpoint lambda_formula_bool(f1 f2 : lambda_formula V L) : bool :=
match (f1, f2) with
| (lf_prop v1, lf_prop v2) ⇒ if v_eq v1 v2 then true else false
| (lf_neg f1, lf_neg f2) ⇒ lambda_formula_bool f1 f2
| (lf_and f1 f2, lf_and f3 f4) ⇒
lambda_formula_bool f1 f3 &&
lambda_formula_bool f2 f4
| (lf_modal op1 args1, lf_modal op2 args2) ⇒
(if op_eq op1 op2 then true else false) &&
((fix eq_args(l1 l2 : nat)
(args1 : counted_list (lambda_formula V L) l1)
(args2 : counted_list (lambda_formula V L) l2) : bool :=
match (args1, args2) with
| (counted_nil, counted_nil) ⇒ true
| (counted_cons n1 f1 args1, counted_cons n2 f2 args2) ⇒
lambda_formula_bool f1 f2 &&
eq_args n1 n2 args1 args2
| _ ⇒ false
end
) (arity L op1) (arity L op2) args1 args2)
| _ ⇒ false
end.
Lemma lambda_formula_bool_char :
∀ (f1 f2 : lambda_formula V L),
f1 = f2 ↔ lambda_formula_bool f1 f2 = true.
Definition lambda_formula_eq(f1 f2 : lambda_formula V L)
: {f1 = f2}+{f1 ≠ f2}.
Definition sequent_support(s : sequent V L) : sequent V L :=
list_support lambda_formula_eq s.
Lemma sequent_support_correct_no_dup : ∀(s : sequent V L),
NoDup (sequent_support s).
Lemma sequent_support_correct_content :
∀(s : sequent V L),
incl s (sequent_support s).
Lemma sequent_support_correct_subset : ∀(s : sequent V L),
multi_subset (sequent_support s) s.
Lemma sequent_support_incl :
∀(s : sequent V L), incl (sequent_support s) s.
Lemma sequent_support_head_contract :
∀(f : lambda_formula V L)(s : sequent V L),
sequent_support (f :: f :: s) =
sequent_support (f :: s).
Lemma sequent_support_reorder : ∀(s1 s2 : sequent V L),
list_reorder s1 s2 →
list_reorder (sequent_support s1)
(sequent_support s2).
Lemma sequent_support_destruct :
∀(s1 : sequent V L),
∃(s2 : sequent V L),
list_reorder s1 (s2 ++ sequent_support s1) ∧
incl s2 (sequent_support s1).
Lemma multi_subset_right_sequent_support :
∀(s1 s2 : sequent V L),
NoDup s1 →
incl s1 s2 →
multi_subset s1 (sequent_support s2).
Lemma every_nth_sequent_support :
∀(P : lambda_formula V L → Prop)(s : sequent V L),
every_nth P s →
every_nth P (sequent_support s).
Lemma rank_sequent_sequent_support :
∀(s : sequent V L)(n : nat),
rank_sequent n s →
rank_sequent n (sequent_support s).
Lemma subst_eq_on_vars_support :
∀(sigma1 sigma2 : lambda_subst V L)(pv : list V),
subst_eq_on_vars sigma1 sigma2 (list_support v_eq pv) →
subst_eq_on_vars sigma1 sigma2 pv.
Lemma sequent_support_subst_sequent :
∀(sigma : lambda_subst V L)(s : sequent V L),
injective sigma →
simple_modal_sequent s →
sequent_support (subst_sequent sigma s) =
subst_sequent sigma (sequent_support s).
End Sequent_support.
Implicit Arguments lambda_formula_eq [V L].
Implicit Arguments sequent_support [V L].
Implicit Arguments sequent_support_correct_subset [V L].
Implicit Arguments sequent_support_reorder [V L].
Implicit Arguments sequent_support_destruct [V L].