Require Export propositional_formulas plain_prop_mod.

Section Back_subst.

  Variable V : Type.
  Variable L : modal_operators.

  Variable v_eq : eq_type V.

  Definition back_subst_result(form_type : Type) : Type :=
    ( form_type × (lambda_subst V L) × nat )%type.

  Fixpoint mod_arg_back_subst_mod_args(f : nat → V)(next : nat)
               (subst : lambda_subst V L)
               (n : nat)(args : counted_list (lambda_formula V L) n) :
                    back_subst_result (counted_list (lambda_formula V L) n) :=
    match args with
      | counted_nil ⇒ (counted_nil, subst, next)
      | counted_cons n arg args ⇒
        let (res_subst, next) :=
            mod_arg_back_subst_mod_args f next subst n args in
        let (res, subst) := res_subst
        in
          (counted_cons (lf_prop (f next)) res,
           function_update v_eq subst (f next) arg,
           S next)
    end.

  Definition mod_arg_back_subst_modal_form(f : nat → V)(next : nat)
               (subst : lambda_subst V L)
               (form : lambda_formula V L)(mod_form : modal_form form)
                                   : back_subst_result (lambda_formula V L) :=
    match form return modal_form form → back_subst_result (lambda_formula V L)
    with
      | lf_modal op args ⇒ fun _ ⇒
        let (res_subst, next) :=
                mod_arg_back_subst_mod_args f next subst (arity L op) args in
        let (res, subst) := res_subst
        in
          (lf_modal op res, subst, next)
      | _ ⇒ fun(H : False) ⇒ False_rect _ H
    end mod_form.

  Definition mod_arg_back_subst_neg_mod_form(f : nat → V)(next : nat)
               (subst : lambda_subst V L)
               (form : lambda_formula V L)
               (neg_mod_form : top_modal_form form)
                                   : back_subst_result (lambda_formula V L) :=
    match form
        return top_modal_form form
                     → back_subst_result (lambda_formula V L)
    with
      | lf_neg form ⇒ fun(H : modal_form form) ⇒
        let (res_subst, next) :=
            mod_arg_back_subst_modal_form f next subst form H in
        let (res, subst) := res_subst
        in (lf_neg res, subst, next)
      | lf_modal op args ⇒ fun(H : modal_form (lf_modal op args)) ⇒
          mod_arg_back_subst_modal_form f next subst (lf_modal op args) H
      | _ ⇒ fun(H : False) ⇒ False_rect _ H
    end neg_mod_form.

  Fixpoint mod_arg_back_subst_sequent_rec(f : nat → V)(next : nat)
               (subst : lambda_subst V L)
               (s : sequent V L)(top_mod_s : top_modal_sequent s)
                                          : back_subst_result (sequent V L) :=
    match s return top_modal_sequent s → back_subst_result (sequent V L)
    with
      | [] ⇒ fun _ ⇒ ([], subst, next)
      | form :: seq ⇒ fun(H : top_modal_sequent (form :: seq)) ⇒
        let (res_subst, next) :=
              mod_arg_back_subst_sequent_rec f next subst seq
                                                  (every_nth_tail _ _ _ H) in
        let (sres, subst) := res_subst in
        let (res_subst, next) :=
              mod_arg_back_subst_neg_mod_form f next subst form
                                                  (every_nth_head _ _ _ H) in
        let (fres, subst) := res_subst
        in
          (fres :: sres, subst, next)
    end top_mod_s.

  Definition mod_arg_back_subst_sequent(f : nat → V)
                  (s : sequent V L)(top_mod_s : top_modal_sequent s)
                                      : (sequent V L) × (lambda_subst V L) :=
    let (res, _) := mod_arg_back_subst_sequent_rec f 0 id_subst s top_mod_s
    in res.

  Definition subst_equal_below(f : nat → V)(n : nat)
                              (sigma1 sigma2 : lambda_subst V L) : Prop :=
    ∀(i : nat),
      i < n →
      sigma1 (f i) = sigma2 (f i).

  Definition subst_equal_below_refl :
    ∀(f : nat → V)(n : nat)(sigma : lambda_subst V L),
      subst_equal_below f n sigma sigma.

  Definition subst_equal_below_trans :
    ∀(f : nat → V)(n : nat)(sigma1 sigma2 sigma3 : lambda_subst V L),
      subst_equal_below f n sigma1 sigma2 →
      subst_equal_below f n sigma2 sigma3 →
        subst_equal_below f n sigma1 sigma3.

  Definition subst_equal_below_single_update :
    ∀(f : nat → V)(n1 n2 : nat)(sigma : lambda_subst V L)
          (form : lambda_formula V L),
      injective f →
      n1 ≤ n2 →
        subst_equal_below f n1
          (function_update v_eq sigma (f n2) form)
          sigma.

  Definition subst_equal_below_mono :
    ∀(f : nat → V)(n1 n2 : nat)(sigma1 sigma2 : lambda_subst V L),
      subst_equal_below f n1 sigma1 sigma2 →
      n2 ≤ n1 →
        subst_equal_below f n2 sigma1 sigma2.

  Definition prop_var_list_below(f : nat → V)(n : nat)
                                (prop_vars : list V) : Prop :=
    ∀(v : V),
      In v prop_vars →
      ∃(i : nat),
        i < n ∧ f i = v.

  Lemma prop_var_list_below_singleton :
    ∀(f : nat → V)(bound n : nat),
      n < bound →
        prop_var_list_below f bound [f n].

  Lemma prop_var_list_below_empty :
    ∀(f : nat → V)(n : nat),
      prop_var_list_below f n [].

  Lemma prop_var_list_below_append :
    ∀(f : nat → V)(n : nat)(pv1 pv2 : list V),
      prop_var_list_below f n pv1 →
      prop_var_list_below f n pv2 →
        prop_var_list_below f n (pv1 ++ pv2).

  Lemma subst_eq_on_vars_below :
    ∀(f : nat → V)(n : nat)
          (sigma1 sigma2 : lambda_subst V L)(prop_vars : list V),
      subst_equal_below f n sigma1 sigma2 →
      prop_var_list_below f n prop_vars →
        subst_eq_on_vars sigma1 sigma2 prop_vars.

  Lemma mod_arg_back_subst_mod_args_prop_ind :
    ∀(f : nat → V)(arity : nat)
          (args back_args : counted_list (lambda_formula V L) arity)
          (r n n_res : nat)(sigma sigma_res : lambda_subst V L),
      injective f →
      every_nth (rank_formula (S r)) (list_of_counted_list args) →
      rank_subst (S r) sigma →
      mod_arg_back_subst_mod_args f n sigma arity args =
                                (back_args, sigma_res, n_res) →
        (∀(bound : nat),
           n_res ≤ bound →
             prop_var_list_below f bound (prop_var_modal_args arity back_args))
        ∧ n ≤ n_res ∧
        subst_equal_below f n sigma_res sigma ∧
        counted_map (subst_form sigma_res) back_args = args ∧
        every_nth prop_form (list_of_counted_list back_args) ∧
        rank_subst (S r) sigma_res.

  Lemma mod_arg_back_subst_mod_args_prop :
    ∀(arity : nat)(args : counted_list (lambda_formula V L) arity)
          (rank : nat),
      countably_infinite V →
      every_nth (rank_formula (S rank)) (list_of_counted_list args) →
      ∃(simple_args : counted_list (lambda_formula V L) arity)
            (sigma : lambda_subst V L),
        counted_map (subst_form sigma) simple_args = args ∧
        every_nth prop_form (list_of_counted_list simple_args) ∧
        rank_subst (S rank) sigma.

  Lemma mod_arg_back_subst_modal_form_prop :
    ∀(f : nat → V)(form back_form : lambda_formula V L)
          (mod_form : modal_form form)
          (r n n_res : nat)(sigma sigma_res : lambda_subst V L) ,
      injective f →
      rank_formula (2 + r) form →
      rank_subst (S r) sigma →
      mod_arg_back_subst_modal_form f n sigma form mod_form =
                                       (back_form, sigma_res, n_res) →
        (∀(bound : nat),
           n_res ≤ bound →
             prop_var_list_below f bound (prop_var_formula back_form))
        ∧
        n ≤ n_res ∧
        subst_equal_below f n sigma_res sigma ∧
        subst_form sigma_res back_form = form ∧
        simple_modal_form back_form ∧
        rank_subst (S r) sigma_res.

  Lemma mod_arg_back_subst_neg_form_prop :
    ∀(f : nat → V)(form back_form : lambda_formula V L)
          (neg_mod_form : top_modal_form form)
          (r n n_res : nat)(sigma sigma_res: lambda_subst V L),
      injective f →
      rank_formula (2 + r) form →
      rank_subst (S r) sigma →
      mod_arg_back_subst_neg_mod_form f n sigma form neg_mod_form =
                  (back_form, sigma_res, n_res) →
        (∀(bound : nat),
           n_res ≤ bound →
             prop_var_list_below f bound (prop_var_formula back_form))
        ∧
        n ≤ n_res ∧
        subst_equal_below f n sigma_res sigma ∧
        subst_form sigma_res back_form = form ∧
        neg_form_maybe simple_modal_form back_form ∧
        rank_subst (S r) sigma_res.

  Lemma mod_arg_back_subst_sequent_rec_prop :
    ∀(f : nat → V)(s back_s : sequent V L)
          (top_mod_s : top_modal_sequent s)(r n n_res : nat)
          (sigma sigma_res : lambda_subst V L),
      injective f →
      rank_sequent (2 + r) s →
      rank_subst (S r) sigma →
      mod_arg_back_subst_sequent_rec f n sigma s top_mod_s
                             = (back_s, sigma_res, n_res) →
        (∀(bound : nat),
           n_res ≤ bound →
             prop_var_list_below f bound (prop_var_sequent back_s)) ∧
        subst_sequent sigma_res back_s = s ∧
        simple_modal_sequent back_s ∧
        rank_subst (S r) sigma_res.

  Lemma mod_arg_back_subst_sequent_prop :
    ∀(s : sequent V L)(n : nat),
      countably_infinite V →
      top_modal_sequent s →
      rank_sequent (2 + n) s →
      ∃(simple_s : sequent V L)(sigma : lambda_subst V L),
        subst_sequent sigma simple_s = s ∧
        simple_modal_sequent simple_s ∧
        rank_subst (S n) sigma.

  Fixpoint prop_back_subst_form_rec(f : nat → V)(next : nat)
               (subst : lambda_subst V L)(form : lambda_formula V L)
                                   : back_subst_result (lambda_formula V L) :=
    match form
    with
      | lf_prop v ⇒
        (lf_prop (f next),
         function_update v_eq subst (f next) (lf_prop v),
         S next)
      | lf_neg form ⇒
        let (res_subst, next) :=
            prop_back_subst_form_rec f next subst form in
        let (res, subst) := res_subst
        in (lf_neg res, subst, next)
      | lf_and form1 form2 ⇒
        let (res_subst, next) :=
            prop_back_subst_form_rec f next subst form1 in
        let (res_1, subst) := res_subst in
        let (res_subst, next) :=
            prop_back_subst_form_rec f next subst form2 in
        let (res_2, subst) := res_subst
        in (lf_and res_1 res_2, subst, next)
      | lf_modal op args ⇒
        (lf_prop (f next),
         function_update v_eq subst (f next) (lf_modal op args),
         S next)
    end.

  Definition prop_back_subst_form(f : nat → V)(form : lambda_formula V L)
                               : (lambda_formula V L) × (lambda_subst V L) :=
    let (res, _) := prop_back_subst_form_rec f 0 id_subst form
    in res.

  Lemma prop_back_subst_form_prop_ind :
    ∀(f : nat → V)(form back_form : lambda_formula V L)
          (r n n_res : nat)(sigma sigma_res : lambda_subst V L) ,
      injective f →
      rank_formula (S r) form →
      rank_subst (S r) sigma →
      plain_prop_mod_subst sigma →
      prop_back_subst_form_rec f n sigma form = (back_form, sigma_res, n_res) →
        (∀(bound : nat),
           n_res ≤ bound →
             prop_var_list_below f bound (prop_var_formula back_form))
        ∧
        n ≤ n_res ∧
        subst_equal_below f n sigma_res sigma ∧
        subst_form sigma_res back_form = form ∧
        propositional back_form ∧
        rank_subst (S r) sigma_res ∧
        plain_prop_mod_subst sigma_res.

  Lemma prop_back_subst_form_prop :
    ∀(form : lambda_formula V L)(n : nat),
      countably_infinite V →
      rank_formula (S n) form →
      ∃(simple_f : lambda_formula V L)(sigma : lambda_subst V L),
        subst_form sigma simple_f = form ∧
        propositional simple_f ∧
        rank_subst (S n) sigma ∧
        plain_prop_mod_subst sigma.

End Back_subst.

Implicit Arguments mod_arg_back_subst_mod_args_prop [V L].
Implicit Arguments mod_arg_back_subst_sequent_prop [V L].
Implicit Arguments prop_back_subst_form_prop [V L].