Require Export formulas list_set functions.

Section Substitutions.

  Variable V : Type.
  Variable L : modal_operators.

need a decidable equality on propositional constants for limit_subst
  Variable v_eq : eq_type V.

Substitutions on formulas

  Definition lambda_subst : Type := Vlambda_formula V L.

  Definition subst_form(sigma : lambda_subst)(f : lambda_formula V L) :
                                                        lambda_formula V L :=
    lambda_formula_rec sigma lf_neg lf_and lf_modal f.

  Lemma subst_form_char :
    (sigma : lambda_subst)(f : lambda_formula V L),
      subst_form sigma f =
        match f with
          | lf_prop vsigma v
          | lf_neg flf_neg (subst_form sigma f)
          | lf_and f1 f2lf_and (subst_form sigma f1) (subst_form sigma f2)
          | lf_modal op args
            lf_modal op (counted_map (subst_form sigma) args)

  Lemma subst_form_or :
    (f1 f2 : lambda_formula V L)(sigma : lambda_subst),
      subst_form sigma (lambda_or f1 f2) =
        lambda_or (subst_form sigma f1) (subst_form sigma f2).

  Lemma subst_form_rank_increase :
    (f : lambda_formula V L)(sigma : lambda_subst),
      modal_rank f modal_rank (subst_form sigma f).

  Definition id_subst(v : V) : lambda_formula V L := lf_prop v.

  Lemma subst_form_id : (f : lambda_formula V L),
    subst_form id_subst f = f.

Composition of substitutions

  Definition subst_compose(sigma_1 sigma_2 : lambda_subst) : lambda_subst :=
    fun(v : V) ⇒ subst_form sigma_1 (sigma_2 v).

  Lemma subst_form_compose :
    (f : lambda_formula V L)(sigma_1 sigma_2 : lambda_subst),
      subst_form (subst_compose sigma_1 sigma_2) f =
        subst_form sigma_1 (subst_form sigma_2 f).

  Lemma subst_compose_id_right :
    (sigma : lambda_subst),
      subst_compose sigma id_subst sigma.

  Lemma subst_compose_assoc :
    (sigma1 sigma2 sigma3 : lambda_subst),
      subst_compose (subst_compose sigma1 sigma2) sigma3
        subst_compose sigma1 (subst_compose sigma2 sigma3).

Substitutions on sequents

  Definition subst_sequent(sigma : lambda_subst)(s : sequent V L) :
                                                                sequent V L :=
    map (subst_form sigma) s.

  Lemma length_subst_sequent : (sigma : lambda_subst)(s : sequent V L),
    length (subst_sequent sigma s) = length s.

  Lemma subst_sequent_id :
    (s : sequent V L), subst_sequent id_subst s = s.

  Lemma subst_sequent_append :
    (sigma : lambda_subst)(s1 s2 : sequent V L),
      subst_sequent sigma (s1 ++ s2) =
        (subst_sequent sigma s1) ++ (subst_sequent sigma s2).

  Lemma neg_sequent_subst_sequent :
    (sigma : lambda_subst)(s : sequent V L),
      every_nth neg_form severy_nth neg_form (subst_sequent sigma s).

  Lemma nth_subst_sequent :
    (sigma : lambda_subst)(s : sequent V L)
          (n : nat)(n_less_subst : n < length (subst_sequent sigma s))
          (n_less_s : n < length s),
      nth (subst_sequent sigma s) n n_less_subst =
        subst_form sigma (nth s n n_less_s).

  Lemma list_reorder_subst_sequent :
    (sigma : lambda_subst)(s1 s2 : sequent V L),
      list_reorder s1 s2
        list_reorder (subst_sequent sigma s1) (subst_sequent sigma s2).

  Lemma or_formula_subst_sequent_tcc :
    (s : sequent V L)(sigma : lambda_subst),
      s []subst_sequent sigma s [].

  Lemma or_formula_subst_sequent :
    (s : sequent V L)(sigma : lambda_subst)(nonempty_s : s []),
      or_formula_of_ne_sequent (subst_sequent sigma s)
               (or_formula_subst_sequent_tcc s sigma nonempty_s) =
        subst_form sigma (or_formula_of_ne_sequent s nonempty_s).

  Lemma subst_sequent_rank_increase :
    (n : nat)(s : sequent V L)(sigma : lambda_subst),
      rank_sequent n (subst_sequent sigma s) → rank_sequent n s.

  Lemma subst_sequent_compose :
    (s : sequent V L)(sigma_1 sigma_2 : lambda_subst),
      subst_sequent (subst_compose sigma_1 sigma_2) s =
        subst_sequent sigma_1 (subst_sequent sigma_2 s).

substitution rank

  Definition rank_subst(n : nat)(sigma : lambda_subst) : Prop :=
    (v : V), rank_formula n (sigma v).

  Lemma nonempty_rank_subst : (v : V)(n : nat)(sigma : lambda_subst),
    rank_subst n sigma → 0 < n.

  Lemma rank_subst_ge :
    (n1 n2 : nat),
      n1 n2
        subset (rank_subst n1) (rank_subst n2).

  Lemma rank_subst_update :
   (sigma : lambda_subst)(n : nat)(v : V)(f : lambda_formula V L),
     rank_formula n f
     rank_subst n sigma
       rank_subst n (function_update v_eq sigma v f).

  Lemma rank_formula_subst_formula_add :
    (f : lambda_formula V L)(sigma : lambda_subst)(n k : nat),
      1 k
      rank_formula n f
      rank_subst k sigma
        rank_formula (n + k - 1) (subst_form sigma f).

  Lemma rank_sequent_subst_add :
    (s : sequent V L)(sigma : lambda_subst)(n k npk : nat),
      rank_sequent n s
      rank_subst k sigma
      1 k
      n + k - 1 = npk
        rank_sequent npk (subst_sequent sigma s).

  Lemma rank_sequent_subst_prop_sequent :
    (s : sequent V L)(sigma : lambda_subst)(n : nat),
      prop_sequent s
      rank_subst n sigma
        rank_sequent n (subst_sequent sigma s).

  Lemma rank_subst_subst_compose :
    (n k npk : nat)(sigma_1 sigma_2 : lambda_subst),
      rank_subst (S n) sigma_1
      rank_subst (S k) sigma_2
      S (n + k) = npk
        rank_subst npk (subst_compose sigma_1 sigma_2).

Substitution on sequent sets

  Definition subst_sequent_set(sigma : lambda_subst)(ss : set (sequent V L))
                                                        : set (sequent V L) :=
    fun(s : sequent V L) ⇒
      (o : sequent V L),
        ss o s = subst_sequent sigma o.

  Lemma subst_sequent_set_empty :
    (sigma : lambda_subst),
      set_equal (subst_sequent_set sigma (empty_sequent_set V L))
                (empty_sequent_set V L).

Substituted rules

  Definition subst_sequent_rule(sigma : lambda_subst)(r : sequent_rule V L)
                                                         : sequent_rule V L :=
    {| assumptions := map (subst_sequent sigma) (assumptions r);
       conclusion := subst_sequent sigma (conclusion r)

  Lemma rule_has_rank_subst_rule :
    (sigma : lambda_subst)(r : sequent_rule V L)(n k : nat),
      rule_has_rank n r
      rank_subst (S k) sigma
        rule_has_rank (n + k) (subst_sequent_rule sigma r).

  Definition subst_closed_rule_set(rules : set (sequent_rule V L)) : Prop :=
    (sigma : lambda_subst)(r : sequent_rule V L),
      rules rrules (subst_sequent_rule sigma r).

Limit substitutions

  Lemma rank_formula_id_subst : (n : nat)(v : V),
    0 < nrank_formula n (id_subst v).

  Lemma rank_subst_id_subst : (n : nat),
    0 < nrank_subst n id_subst.

  Definition limit_subst(pv : list V)(sigma : lambda_subst) : lambda_subst :=
    fun(v : V) ⇒
      if member v_eq v pv
      then sigma v
      else id_subst v.

  Lemma rank_subst_limit_lf_modal :
    (n : nat)(v : V)(sigma : lambda_subst)
          (op : operator L)
          (args : counted_list (lambda_formula V L) (arity L op)),
      every_nth prop_form (list_of_counted_list args) →
      In v (prop_var_formula (lf_modal op args)) →
      rank_formula n (subst_form sigma (lf_modal op args)) →
        rank_formula (pred n) (sigma v).

Substitution equality

  Definition subst_eq_on_vars(sigma1 sigma2 : lambda_subst)(pv : list V)
                                                                     : Prop :=
    (v : V), In v pvsigma1 v = sigma2 v.

  Lemma subst_eq_on_vars_empty :
    (sigma1 sigma2 : lambda_subst),
      subst_eq_on_vars sigma1 sigma2 [].

  Lemma subst_eq_on_vars_symm :
    (sigma1 sigma2 : lambda_subst)(pv : list V),
      subst_eq_on_vars sigma1 sigma2 pv
        subst_eq_on_vars sigma2 sigma1 pv.

  Lemma subst_eq_on_vars_trans :
    (sigma1 sigma2 sigma3: lambda_subst)(pv : list V),
      subst_eq_on_vars sigma1 sigma2 pv
      subst_eq_on_vars sigma2 sigma3 pv
        subst_eq_on_vars sigma1 sigma3 pv.

  Lemma subst_eq_on_vars_trans_rev :
    (sigma1 sigma2 sigma3: lambda_subst)(pv : list V),
      subst_eq_on_vars sigma3 sigma2 pv
      subst_eq_on_vars sigma1 sigma2 pv
        subst_eq_on_vars sigma1 sigma3 pv.

  Lemma subst_eq_on_vars_seq :
    (sigma1 sigma2 : lambda_subst)(pv : list V),
      sigma1 sigma2

  Lemma subst_eq_on_vars_compose_right_change :
    (subst1 subst2 subst3 : lambda_subst)(pv : list V),
      subst_eq_on_vars subst2 subst3 pv
          (subst_compose subst1 subst2)
          (subst_compose subst1 subst3) pv.

  Lemma subst_eq_on_vars_append :
    (pv1 pv2 : list V)(sigma1 sigma2 : lambda_subst),
      subst_eq_on_vars sigma1 sigma2 pv1
      subst_eq_on_vars sigma1 sigma2 pv2
        subst_eq_on_vars sigma1 sigma2 (pv1 ++ pv2).

  Lemma subst_formula_eq :
    (sigma1 sigma2 : lambda_subst)
          (f : lambda_formula V L)(prop_vars : list V),
      incl (prop_var_formula f) prop_vars
      subst_eq_on_vars sigma1 sigma2 prop_vars
        subst_form sigma1 f = subst_form sigma2 f.

Proof the case for modal arguments again, because it is needed separately.
  Lemma subst_modal_args_eq :
    (sigma1 sigma2 : lambda_subst)
          (n : nat)(args : counted_list (lambda_formula V L) n)
          (prop_vars : list V),
      incl (prop_var_modal_args n args) prop_vars
      subst_eq_on_vars sigma1 sigma2 prop_vars
        counted_map (subst_form sigma1) args =
        counted_map (subst_form sigma2) args.

  Lemma subst_sequent_eq :
    (sigma1 sigma2 : lambda_subst)(s : sequent V L)(prop_vars : list V),
      incl (prop_var_sequent s) prop_vars
      subst_eq_on_vars sigma1 sigma2 prop_vars
        subst_sequent sigma1 s = subst_sequent sigma2 s.

Equality for limited substitutions

  Lemma subst_eq_on_vars_limit :
    (sigma : lambda_subst)(pv : list V),
      subst_eq_on_vars (limit_subst pv sigma) sigma pv.

  Lemma subst_sequent_limit_eq :
    (s : sequent V L)(sigma : lambda_subst)(prop_vars : list V),
      incl (prop_var_sequent s) prop_vars
        subst_sequent (limit_subst prop_vars sigma) s = subst_sequent sigma s.

  Lemma map_subst_sequent_limit_eq :
    (ss : list (sequent V L))(sigma : lambda_subst)(prop_vars : list V),
      incl (flatten (map prop_var_sequent ss)) prop_vars
        map (subst_sequent (limit_subst prop_vars sigma)) ss =
        map (subst_sequent sigma) ss.

End Substitutions.

Implicit Arguments subst_form [V L].
Implicit Arguments subst_form_char [V L].
Implicit Arguments subst_compose [V L].
Implicit Arguments subst_sequent [V L].
Implicit Arguments rank_subst [V L].
Implicit Arguments rank_formula_subst_formula_add [V L].
Implicit Arguments or_formula_subst_sequent_tcc [V L].
Implicit Arguments nonempty_rank_subst [V L].
Implicit Arguments rank_subst_ge [V L].
Implicit Arguments rank_sequent_subst_add [V L].
Implicit Arguments subst_sequent_set [V L].
Implicit Arguments subst_sequent_rule [V L].
Implicit Arguments subst_closed_rule_set [V L].
Implicit Arguments id_subst [[V] [L]].
Implicit Arguments subst_eq_on_vars [V L].
Implicit Arguments limit_subst [V L].