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