Factorize two substitutions
subst_sequent sigma1 s1 = subst_sequent (subst_compose sigma_i sigma_r1) s1
subst_sequent sigma2 s2 = subst_sequent (subst_compose sigma_i sigma_r2) s2
Require Export factor_subst.
Section Factor_two_subst.
Variable V : Type.
Variable L : modal_operators.
Need decidable equalitities for the factoring
Functions definitions
Fixpoint next_unused_var(f : nat → V)(used : list V)(n bound : nat) :
V × nat :=
match bound with
| 0 ⇒ (f n, S n)
| S bound ⇒
if member v_eq (f n) used
then next_unused_var f used (S n) bound
else (f n, S n)
end.
V × nat :=
match bound with
| 0 ⇒ (f n, S n)
| S bound ⇒
if member v_eq (f n) used
then next_unused_var f used (S n) bound
else (f n, S n)
end.
This function constructs the mapping for a renaming of the
variables in the intersection of pv1 and pv2. The renaming
maps those duplicates in pv2 to fresh variables that do
neither occur in pv1 nor in pv2_orig. Initially pv2 and
pv2_orig are identically. But then pv2 is reduced in the
recursion, while pv2_orig keeps the original pv2 value.
Fixpoint rename_disjoint(f : nat → V)(n : nat)(pv1 pv2_orig pv2 : list V) :
list (V × V) :=
match pv2 with
| [] ⇒ []
| v :: pv2 ⇒
if member v_eq v pv1
then
let (v', n') := next_unused_var f (pv1 ++ pv2_orig) n
(length (pv1 ++ pv2_orig)) in
(v, v') :: (rename_disjoint f n' pv1 pv2_orig pv2)
else rename_disjoint f n pv1 pv2_orig pv2
end.
list (V × V) :=
match pv2 with
| [] ⇒ []
| v :: pv2 ⇒
if member v_eq v pv1
then
let (v', n') := next_unused_var f (pv1 ++ pv2_orig) n
(length (pv1 ++ pv2_orig)) in
(v, v') :: (rename_disjoint f n' pv1 pv2_orig pv2)
else rename_disjoint f n pv1 pv2_orig pv2
end.
This function joins the two injective mappings smap1 and
smap2 into one injective mapping and a renaming. This function
works only correct if the domains of smap1 and smap2 are
disjoint. Elements (v,f) of smap2 where f is not in
smap1 are simply added to smap1. Otherwiese, v is added to
the renaming that is returned as second result.
Fixpoint join_subst_maps(smap1 smap2 : list (V × lambda_formula V L)) :
list (V × lambda_formula V L) × list (V × V) :=
match smap2 with
| [] ⇒ (smap1, [])
| (v, f) :: smap2 ⇒
let (join_tl, r_tl) := join_subst_maps smap1 smap2
in
match rassoc (lambda_formula_eq op_eq v_eq) join_tl f with
| Some v' ⇒ (join_tl, (v, v') :: r_tl)
| None ⇒ ((v, f) :: join_tl, r_tl)
end
end.
list (V × lambda_formula V L) × list (V × V) :=
match smap2 with
| [] ⇒ (smap1, [])
| (v, f) :: smap2 ⇒
let (join_tl, r_tl) := join_subst_maps smap1 smap2
in
match rassoc (lambda_formula_eq op_eq v_eq) join_tl f with
| Some v' ⇒ (join_tl, (v, v') :: r_tl)
| None ⇒ ((v, f) :: join_tl, r_tl)
end
end.
This is the main function for factorizing two substitutions. It
first constructs the mapping ru_for of a renaming to make the
variables of s1 and s2 disjoint. (ru_for stands for
rename-unique-forward). This renaming can easily be inverted by
swapping the pairs in the mapping. Next, both substitutions are
split using the functions from module
factor_subst .
Next, the
two injective substitution mappings obtained this way are
joined. Finally, the renaming for s2 must be assembled from
various pieces and the variable-chain end points in the joined
mapping must be fixed.
Definition factor_two_subst(f : nat → V)(subst1 subst2 : lambda_subst V L)
(s1 s2 : sequent V L) :
(lambda_subst V L) × (lambda_subst V L) × (lambda_subst V L) :=
let rumap :=
rename_disjoint f 0 (prop_var_sequent s1)
(list_support v_eq (prop_var_sequent s2))
(list_support v_eq (prop_var_sequent s2)) in
let ru_for := rename_of_map v_eq rumap in
let s2_ru := subst_sequent ru_for s2 in
let subst2_ru :=
subst_compose subst2 (rename_of_map v_eq (swap_pairs rumap)) in
let (smap1, rmap1) :=
divide_subst op_eq v_eq subst1 (prop_var_sequent s1) in
let (smap2, rmap2) :=
divide_subst op_eq v_eq subst2_ru (prop_var_sequent s2_ru) in
let (sjoin, rjoin) := join_subst_maps smap1 smap2
in (rename_of_map v_eq rmap1,
subst_compose
(subst_compose (rename_of_map v_eq rjoin) (rename_of_map v_eq rmap2))
ru_for,
subst_of_map v_eq (fix_var_chain_ends v_eq sjoin)).
(s1 s2 : sequent V L) :
(lambda_subst V L) × (lambda_subst V L) × (lambda_subst V L) :=
let rumap :=
rename_disjoint f 0 (prop_var_sequent s1)
(list_support v_eq (prop_var_sequent s2))
(list_support v_eq (prop_var_sequent s2)) in
let ru_for := rename_of_map v_eq rumap in
let s2_ru := subst_sequent ru_for s2 in
let subst2_ru :=
subst_compose subst2 (rename_of_map v_eq (swap_pairs rumap)) in
let (smap1, rmap1) :=
divide_subst op_eq v_eq subst1 (prop_var_sequent s1) in
let (smap2, rmap2) :=
divide_subst op_eq v_eq subst2_ru (prop_var_sequent s2_ru) in
let (sjoin, rjoin) := join_subst_maps smap1 smap2
in (rename_of_map v_eq rmap1,
subst_compose
(subst_compose (rename_of_map v_eq rjoin) (rename_of_map v_eq rmap2))
ru_for,
subst_of_map v_eq (fix_var_chain_ends v_eq sjoin)).
Lemma prop_var_formula_subst_rename_of_map :
∀(rmap : list (V × V))(f : lambda_formula V L),
prop_var_formula (subst_form (rename_of_map v_eq rmap) f) =
apply_assoc_map v_eq rmap (prop_var_formula f).
Lemma prop_var_sequent_subst_rename_of_map :
∀(rmap : list (V × V))(s : sequent V L),
prop_var_sequent (subst_sequent (rename_of_map v_eq rmap) s) =
apply_assoc_map v_eq rmap (prop_var_sequent s).
Lemma subst_eq_on_vars_compose_rename_change :
∀(subst1 subst2 : lambda_subst V L)
(rmap : list (V × V))(pv : list V),
subst_eq_on_vars subst1 subst2 (apply_assoc_map v_eq rmap pv) →
subst_eq_on_vars
(subst_compose subst1 (rename_of_map v_eq rmap))
(subst_compose subst2 (rename_of_map v_eq rmap))
pv.
Lemma unused_next_unused_var_ind :
∀(f : nat → V)(bound n n' : nat)(used unmet : list V)(v : V),
injective f →
length unmet ≤ bound →
next_unused_var f used n bound = (v, n') →
(∀(v : V)(m : nat), In v used → f m = v → n ≤ m → In v unmet) →
¬ In v used.
Lemma unused_next_unused_var :
∀(f : nat → V)(used : list V)(n n' : nat)(v : V),
injective f →
next_unused_var f used n (length used) = (v, n') →
¬ In v used.
Lemma unused_next_unused_var_left :
∀(f : nat → V)(pv1 pv2 : list V)(n n' : nat)(v : V),
injective f →
next_unused_var f (pv1 ++ pv2) n (length (pv1 ++ pv2)) = (v, n') →
¬ In v pv1.
Lemma next_unused_var_fresh :
∀(f : nat → V)(pv : list V)(bound n n' : nat)(v : V),
next_unused_var f pv n bound = (v, n') →
n < n' ∧ v = f (pred n').
Lemma rename_disjoint_disjoint_ind :
∀(f : nat → V)(pv1 pv2 pv3 : list V)(n : nat)(rmap : list (V × V)),
injective f →
incl pv3 pv2 →
(∀(v1 v2 : V), assoc v_eq rmap v1 = Some v2 → ¬ In v2 pv1) →
lists_disjoint
pv1
(apply_assoc_map v_eq (rmap ++ rename_disjoint f n pv1 pv2 pv3) pv3)
∧
(∀(v1 v2 : V),
assoc v_eq (rename_disjoint f n pv1 pv2 pv3) v1 = Some v2 →
¬ In v2 pv1 ∧ ¬ In v2 pv2).
Lemma rename_disjoint_disjoint :
∀(f : nat → V)(pv1 pv2 : list V)(n : nat),
injective f →
lists_disjoint
pv1
(apply_assoc_map v_eq (rename_disjoint f n pv1 pv2 pv2) pv2).
Lemma rename_disjoint_values_not_in_source :
∀(f : nat → V)(pv1 pv2 : list V)(v1 v2 : V),
injective f →
assoc v_eq (rename_disjoint f 0 pv1 pv2 pv2) v1 = Some v2 →
¬ In v2 pv2.
Lemma assoc_mapping_rename_disjoint_ind :
∀(f : nat → V)(pv1 pv2 pv3 : list V)(n : nat),
let rumap := rename_disjoint f n pv1 pv2 pv3
in
NoDup pv3 →
assoc_mapping v_eq rumap ∧
(∀(v1 v2 : V), assoc v_eq rumap v1 = Some v2 →
In v1 pv3).
Lemma assoc_mapping_rename_disjoint :
∀(f : nat → V)(pv1 pv2 : list V),
NoDup pv2 →
assoc_mapping v_eq (rename_disjoint f 0 pv1 pv2 pv2).
Lemma injective_assoc_rename_disjoint_ind :
∀(f : nat → V)(pv1 pv2 pv3 : list V)(n : nat),
let rumap := rename_disjoint f n pv1 pv2 pv3
in
injective f →
injective_assoc v_eq rumap ∧
(∀(v : V)(m : nat), assoc v_eq rumap v = Some (f m) →
n ≤ m).
Lemma injective_assoc_rename_disjoint :
∀(f : nat → V)(pv1 pv2 : list V),
injective f →
injective_assoc v_eq (rename_disjoint f 0 pv1 pv2 pv2).
Lemma rename_disjoint_compose_identity :
∀(f : nat → V)(pv1 pv2 : list V),
let rumap := rename_disjoint f 0 pv1 pv2 pv2
in
injective f →
NoDup pv2 →
subst_eq_on_vars
(subst_compose (rename_of_map v_eq (swap_pairs rumap))
(rename_of_map v_eq rumap))
(@id_subst V L)
pv2.
Lemma map_subst_correct_disjoint_keys_half :
∀(subst1 subst2 : lambda_subst V L)
(smap1 smap2 : list (V × lambda_formula V L))
(rmap1 rmap2 : list (V × V))(pv1 pv2 : list V)(v : V),
map_subst_correct v_eq subst1 smap1 rmap1 pv1 →
map_subst_correct v_eq subst2 smap2 rmap2 pv2 →
lists_disjoint pv1 pv2 →
is_some (assoc v_eq smap1 v) →
is_none (assoc v_eq smap2 v).
Lemma map_subst_correct_disjoint_keys :
∀(subst1 subst2 : lambda_subst V L)
(smap1 smap2 : list (V × lambda_formula V L))
(rmap1 rmap2 : list (V × V))(pv1 pv2 : list V),
map_subst_correct v_eq subst1 smap1 rmap1 pv1 →
map_subst_correct v_eq subst2 smap2 rmap2 pv2 →
lists_disjoint pv1 pv2 →
assoc_disjoint_keys v_eq smap1 smap2.
Lemma injective_assoc_join_subst_maps :
∀(smap1 smap2 sjoin : list (V × lambda_formula V L))
(rmap1 rmap2 rjoin : list (V × V)),
join_subst_maps smap1 smap2 = (sjoin, rjoin) →
injective_assoc v_eq smap1 →
injective_assoc v_eq smap2 →
assoc_mapping v_eq smap2 →
injective_assoc v_eq sjoin.
Lemma assoc_mapping_join_subst_maps :
∀(smap1 smap2 sjoin : list (V × lambda_formula V L))
(rjoin : list (V × V)),
join_subst_maps smap1 smap2 = (sjoin, rjoin) →
assoc_mapping v_eq smap1 →
assoc_mapping v_eq smap2 →
assoc_disjoint_keys v_eq smap1 smap2 →
assoc_mapping v_eq sjoin ∧
(∀(v : V), is_some (assoc v_eq sjoin v) →
is_some (assoc v_eq smap1 v) ∨ is_some (assoc v_eq smap2 v)).
Lemma join_subst_maps_subst_char :
∀(smap1 smap2 sjoin : list (V × lambda_formula V L))
(rjoin : list (V × V)),
join_subst_maps smap1 smap2 = (sjoin, rjoin) →
assoc_mapping v_eq sjoin →
∃(smap2_part : list (V × lambda_formula V L)),
sjoin = smap2_part ++ smap1 ∧
incl smap2_part smap2 ∧
assoc_mapping v_eq smap2_part.
Lemma rank_join_subst_maps :
∀(smap1 smap2 sjoin : list (V × lambda_formula V L))
(n : nat)(rjoin : list (V × V)),
join_subst_maps smap1 smap2 = (sjoin, rjoin) →
assoc_mapping v_eq smap2 →
assoc_mapping v_eq sjoin →
map_rank v_eq n smap1 →
map_rank v_eq n smap2 →
map_rank v_eq n sjoin.
Lemma join_subst_maps_contains_first_vars :
∀(subst1 : lambda_subst V L)(pv1 : list V)
(smap1 smap2 sjoin : list (V × lambda_formula V L))
(rmap1 rjoin : list (V × V))(v1 v2 : V),
join_subst_maps smap1 smap2 = (sjoin, rjoin) →
assoc_mapping v_eq sjoin →
map_subst_correct v_eq subst1 smap1 rmap1 pv1 →
In v1 pv1 →
rename_of_map v_eq rmap1 v1 = lf_prop (L:=L) v2 →
is_some (assoc v_eq sjoin v2).
Lemma join_subst_maps_equal_first_map :
∀(subst1 : lambda_subst V L)(pv1 : list V)
(smap1 smap2 sjoin : list (V × lambda_formula V L))
(rmap1 rjoin : list (V × V)),
join_subst_maps smap1 smap2 = (sjoin, rjoin) →
assoc_disjoint_keys v_eq smap1 smap2 →
assoc_mapping v_eq smap2 →
assoc_mapping v_eq sjoin →
map_subst_correct v_eq subst1 smap1 rmap1 pv1 →
subst_eq_on_vars (subst_of_map v_eq smap1) (subst_of_map v_eq sjoin)
(apply_assoc_map v_eq rmap1 pv1).
Lemma join_subst_maps_correct_second_map :
∀(smap1 smap2 sjoin : list (V × lambda_formula V L))
(rjoin : list (V × V)),
join_subst_maps smap1 smap2 = (sjoin, rjoin) →
assoc_mapping v_eq smap2 →
assoc_mapping v_eq sjoin →
(∀(v1 v2 : V),
assoc v_eq rjoin v1 = Some v2 →
∃(f : lambda_formula V L),
assoc v_eq smap2 v1 = Some f ∧ assoc v_eq sjoin v2 = Some f
) ∧
(∀(v1 : V)(f : lambda_formula V L),
assoc v_eq rjoin v1 = None →
assoc v_eq smap2 v1 = Some f →
assoc v_eq sjoin v1 = Some f).
Lemma join_subst_maps_contains_second_vars :
∀(subst2 : lambda_subst V L)(pv2 : list V)
(smap1 smap2 sjoin : list (V × lambda_formula V L))
(rmap2 rjoin : list (V × V))(v1 v2 : V),
join_subst_maps smap1 smap2 = (sjoin, rjoin) →
map_subst_correct v_eq subst2 smap2 rmap2 pv2 →
assoc_mapping v_eq smap2 →
assoc_mapping v_eq sjoin →
In v1 pv2 →
subst_compose (rename_of_map v_eq rjoin)
(rename_of_map v_eq rmap2) v1 = lf_prop (L:=L) v2 →
is_some (assoc v_eq sjoin v2).
Lemma join_subst_maps_equal_second_map :
∀(subst2 : lambda_subst V L)(pv2 : list V)
(smap1 smap2 sjoin : list (V × lambda_formula V L))
(rmap2 rjoin : list (V × V)),
join_subst_maps smap1 smap2 = (sjoin, rjoin) →
map_subst_correct v_eq subst2 smap2 rmap2 pv2 →
assoc_mapping v_eq smap2 →
assoc_mapping v_eq sjoin →
subst_eq_on_vars
(subst_compose (subst_of_map v_eq sjoin) (rename_of_map v_eq rjoin))
(subst_of_map v_eq smap2)
(apply_assoc_map v_eq rmap2 pv2).
Lemma factor_two_subst_equal_2 :
∀(f : nat → V)(subst2 : lambda_subst V L)
(smap1 smap2 sjoin : list (V × lambda_formula V L))
(rmap2 rjoin : list (V × V))
(pv1 : list V)(s2 : sequent V L),
let rumap := rename_disjoint f 0 pv1
(list_support v_eq (prop_var_sequent s2))
(list_support v_eq (prop_var_sequent s2)) in
let ru_for := rename_of_map v_eq rumap in
let s2_ru := subst_sequent ru_for s2 in
let subst2_ru := subst_compose subst2
(rename_of_map v_eq (swap_pairs rumap))
in
injective f →
join_subst_maps smap1 smap2 = (sjoin, rjoin) →
map_subst_correct v_eq subst2_ru smap2 rmap2
(prop_var_sequent s2_ru) →
assoc_mapping v_eq smap2 →
assoc_mapping v_eq sjoin →
subst_eq_on_vars subst2
(subst_compose (subst_of_map v_eq (fix_var_chain_ends v_eq sjoin))
(subst_compose
(subst_compose (rename_of_map v_eq rjoin)
(rename_of_map v_eq rmap2)) ru_for))
(prop_var_sequent s2).
Lemma factor_two_subst_property :
∀(subst1 subst2 : lambda_subst V L)(s1 s2 : sequent V L)(n : nat),
countably_infinite V →
rank_subst (S n) subst1 →
rank_subst (S n) subst2 →
∃(rsubst1 rsubst2 inj_subst : lambda_subst V L),
renaming rsubst1 ∧
renaming rsubst2 ∧
injective inj_subst ∧
rank_subst (S n) inj_subst ∧
subst_eq_on_vars subst1 (subst_compose inj_subst rsubst1)
(prop_var_sequent s1) ∧
subst_eq_on_vars subst2 (subst_compose inj_subst rsubst2)
(prop_var_sequent s2).
End Factor_two_subst.
Implicit Arguments factor_two_subst_property [V L].