Logic library

Sequent support

This module defines a decidable equality on formulas and the support of a sequent.

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.

Equality over formulas, needed for the support in 5.3

  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
        ) (arity L op1) (arity L op2) args1 args2)
      | _false

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

Sequent support

  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 LProp)(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).

Results for substitutions

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