Substitution construction
Backward substitution for arguments of modalities
Substitute unique variables for formulas, needed in 4.13
Need a decidable equality on propositional constants for
function update in substitutions.
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].