Factorize substitutions
subst_sequent sigma s = subst_sequent (subst_compose sigma_i sigma_r) s
Require Export assoc renaming sequent_support.
Section Factor_subst.
Variable V : Type.
Variable L : modal_operators.
Need decidable equalitities for the factoring
Functions definitions
Fixpoint divide_subst(subst : lambda_subst V L)
(pv : list V)
: list (V × lambda_formula V L) × list (V × V) :=
match pv with
| [] ⇒ ([], [])
| v :: pv ⇒
let (smap, rmap) := divide_subst subst pv
in
match rassoc (lambda_formula_eq op_eq v_eq) smap (subst v) with
| Some v' ⇒ (smap, (v, v') :: rmap)
| None ⇒ ((v, subst v) :: smap, rmap)
end
end.
(pv : list V)
: list (V × lambda_formula V L) × list (V × V) :=
match pv with
| [] ⇒ ([], [])
| v :: pv ⇒
let (smap, rmap) := divide_subst subst pv
in
match rassoc (lambda_formula_eq op_eq v_eq) smap (subst v) with
| Some v' ⇒ (smap, (v, v') :: rmap)
| None ⇒ ((v, subst v) :: smap, rmap)
end
end.
Collect the variable-chain end points in the substitution
mapping
Fixpoint collect_var_chain_ends(map orig : list (V × lambda_formula V L))
: list V :=
match map with
| [] ⇒ []
| (v, f) :: map ⇒ match f with
| lf_prop v' ⇒ match assoc v_eq orig v' with
| Some _ ⇒ collect_var_chain_ends map orig
| None ⇒ v' :: (collect_var_chain_ends map orig)
end
| _ ⇒ collect_var_chain_ends map orig
end
end.
: list V :=
match map with
| [] ⇒ []
| (v, f) :: map ⇒ match f with
| lf_prop v' ⇒ match assoc v_eq orig v' with
| Some _ ⇒ collect_var_chain_ends map orig
| None ⇒ v' :: (collect_var_chain_ends map orig)
end
| _ ⇒ collect_var_chain_ends map orig
end
end.
(v, f) :: l are the mappings for the injective substitution.
They are here split into head and tail, because this function
works only for non-empty lists of mappings.
Fixpoint make_unique_form(v : V)(f : lambda_formula V L)
(l : list (V × lambda_formula V L))
: lambda_formula V L :=
match l with
| [] ⇒ lf_and (lf_prop v) f
| (v', f') :: l ⇒ lf_and f (make_unique_form v' f' l)
end.
Definition subst_of_map(map : list (V × lambda_formula V L))
: lambda_subst V L :=
fun(v : V) ⇒ match assoc v_eq map v with
| None ⇒ lf_prop v
| Some f ⇒ f
end.
Definition rename_of_map(rmap : list (V × V)) : lambda_subst V L :=
subst_of_map (map (fun vv ⇒ (fst vv, lf_prop (snd vv))) rmap).
(l : list (V × lambda_formula V L))
: lambda_formula V L :=
match l with
| [] ⇒ lf_and (lf_prop v) f
| (v', f') :: l ⇒ lf_and f (make_unique_form v' f' l)
end.
Definition subst_of_map(map : list (V × lambda_formula V L))
: lambda_subst V L :=
fun(v : V) ⇒ match assoc v_eq map v with
| None ⇒ lf_prop v
| Some f ⇒ f
end.
Definition rename_of_map(rmap : list (V × V)) : lambda_subst V L :=
subst_of_map (map (fun vv ⇒ (fst vv, lf_prop (snd vv))) rmap).
Fix the mappings in smap such that the result is an injective
assoc list.
Definition fix_var_chain_ends(smap : list (V × lambda_formula V L))
: list (V × lambda_formula V L) :=
match smap with
| [] ⇒ []
| (v1, f1) :: mtl ⇒
(map (fun v ⇒ (v, lf_and (lf_prop v) (make_unique_form v1 f1 mtl)))
(collect_var_chain_ends smap smap))
++ smap
end.
Definition factor_subst(subst : lambda_subst V L)(s : sequent V L) :
(lambda_subst V L) × (lambda_subst V L) :=
let (smap, rmap) := divide_subst subst (prop_var_sequent s)
in (rename_of_map rmap, subst_of_map (fix_var_chain_ends smap)).
: list (V × lambda_formula V L) :=
match smap with
| [] ⇒ []
| (v1, f1) :: mtl ⇒
(map (fun v ⇒ (v, lf_and (lf_prop v) (make_unique_form v1 f1 mtl)))
(collect_var_chain_ends smap smap))
++ smap
end.
Definition factor_subst(subst : lambda_subst V L)(s : sequent V L) :
(lambda_subst V L) × (lambda_subst V L) :=
let (smap, rmap) := divide_subst subst (prop_var_sequent s)
in (rename_of_map rmap, subst_of_map (fix_var_chain_ends smap)).
Lemma rename_of_map_cons_split :
∀(P : lambda_formula V L → Prop)(rmap : list (V × V))(v1 v2 v3 : V),
(v1 = v3 → P (lf_prop v2)) →
(v1 ≠ v3 → P (rename_of_map rmap v3)) →
P (rename_of_map ((v1, v2) :: rmap) v3).
Lemma rename_of_map_prop :
∀(rmap : list (V × V))(v : V),
(∃(v' : V), assoc v_eq rmap v = Some v' ∧
rename_of_map rmap v = lf_prop v') ∨
(assoc v_eq rmap v = None ∧ rename_of_map rmap v = lf_prop v).
Utility predicates
map_subst_correct
- (smap, rmap) agree with original subst
- (smap, rmap) are defined for just the right variables
- codomain values in rmap are mapped in smap
Definition map_subst_correct(subst : lambda_subst V L)
(smap : list (V × lambda_formula V L))
(rmap : list (V × V))
(pv : list V) : Prop :=
subst_eq_on_vars
subst
(subst_compose (subst_of_map smap) (rename_of_map rmap))
pv ∧
(∀(v : V),
In v pv
↔
(is_some (assoc v_eq smap v) ∨ is_some (assoc v_eq rmap v)))
∧
(∀(v1 v2 : V),
assoc v_eq rmap v1 = Some v2 → is_some (assoc v_eq smap v2)).
Lemma map_subst_correct_empty :
∀(subst : lambda_subst V L),
map_subst_correct subst [] [] [].
Lemma map_subst_correct_cons_rmap :
∀(subst : lambda_subst V L)(smap : list (V × lambda_formula V L))
(rmap : list (V × V))(pv : list V)(v1 v2 : V),
map_subst_correct subst smap rmap pv →
assoc v_eq smap v2 = Some (subst v1) →
map_subst_correct subst smap ((v1, v2) :: rmap) (v1 :: pv).
Lemma map_subst_correct_cons_smap :
∀(subst : lambda_subst V L)(smap : list (V × lambda_formula V L))
(rmap : list (V × V))(pv : list V)(v : V),
rassoc (lambda_formula_eq op_eq v_eq) smap (subst v) = None →
map_subst_correct subst smap rmap pv →
map_subst_correct subst ((v, subst v) :: smap) rmap (v :: pv).
(smap : list (V × lambda_formula V L))
(rmap : list (V × V))
(pv : list V) : Prop :=
subst_eq_on_vars
subst
(subst_compose (subst_of_map smap) (rename_of_map rmap))
pv ∧
(∀(v : V),
In v pv
↔
(is_some (assoc v_eq smap v) ∨ is_some (assoc v_eq rmap v)))
∧
(∀(v1 v2 : V),
assoc v_eq rmap v1 = Some v2 → is_some (assoc v_eq smap v2)).
Lemma map_subst_correct_empty :
∀(subst : lambda_subst V L),
map_subst_correct subst [] [] [].
Lemma map_subst_correct_cons_rmap :
∀(subst : lambda_subst V L)(smap : list (V × lambda_formula V L))
(rmap : list (V × V))(pv : list V)(v1 v2 : V),
map_subst_correct subst smap rmap pv →
assoc v_eq smap v2 = Some (subst v1) →
map_subst_correct subst smap ((v1, v2) :: rmap) (v1 :: pv).
Lemma map_subst_correct_cons_smap :
∀(subst : lambda_subst V L)(smap : list (V × lambda_formula V L))
(rmap : list (V × V))(pv : list V)(v : V),
rassoc (lambda_formula_eq op_eq v_eq) smap (subst v) = None →
map_subst_correct subst smap rmap pv →
map_subst_correct subst ((v, subst v) :: smap) rmap (v :: pv).
Definition map_rank(n : nat)(map : list (V × lambda_formula V L)) : Prop :=
∀(v : V),
match assoc v_eq map v with
| None ⇒ True
| Some f ⇒ rank_formula (S n) f
end.
Lemma map_rank_empty : ∀(n : nat), map_rank n [].
Lemma map_rank_cons :
∀(n : nat)(map : list (V × lambda_formula V L))
(v : V)(f : lambda_formula V L),
rank_formula (S n) f →
map_rank n map →
map_rank n ((v, f) :: map).
Lemma map_rank_head :
∀(n : nat)(v : V)(f : lambda_formula V L)
(map : list (V × lambda_formula V L)),
map_rank n ((v, f) :: map) →
rank_formula (S n) f.
Lemma map_rank_tail :
∀(n : nat)(v : V)(f : lambda_formula V L)
(map : list (V × lambda_formula V L)),
assoc_mapping v_eq ((v, f) :: map) →
map_rank n ((v, f) :: map) →
map_rank n map.
Lemma map_rank_In :
∀(n : nat)(v : V)(f : lambda_formula V L)
(map : list (V × lambda_formula V L)),
In (v, f) map →
map_rank n map →
assoc_mapping v_eq map →
rank_formula (S n) f.
Lemma map_rank_append :
∀(n : nat)(map1 map2 : list (V × lambda_formula V L)),
map_rank n map1 →
map_rank n map2 →
assoc_mapping v_eq map1 →
map_rank n (map1 ++ map2).
Lemma map_rank_incl :
∀(n : nat)(map1 map2 : list (V × lambda_formula V L)),
incl map1 map2 →
map_rank n map2 →
assoc_mapping v_eq map2 →
map_rank n map1.
∀(v : V),
match assoc v_eq map v with
| None ⇒ True
| Some f ⇒ rank_formula (S n) f
end.
Lemma map_rank_empty : ∀(n : nat), map_rank n [].
Lemma map_rank_cons :
∀(n : nat)(map : list (V × lambda_formula V L))
(v : V)(f : lambda_formula V L),
rank_formula (S n) f →
map_rank n map →
map_rank n ((v, f) :: map).
Lemma map_rank_head :
∀(n : nat)(v : V)(f : lambda_formula V L)
(map : list (V × lambda_formula V L)),
map_rank n ((v, f) :: map) →
rank_formula (S n) f.
Lemma map_rank_tail :
∀(n : nat)(v : V)(f : lambda_formula V L)
(map : list (V × lambda_formula V L)),
assoc_mapping v_eq ((v, f) :: map) →
map_rank n ((v, f) :: map) →
map_rank n map.
Lemma map_rank_In :
∀(n : nat)(v : V)(f : lambda_formula V L)
(map : list (V × lambda_formula V L)),
In (v, f) map →
map_rank n map →
assoc_mapping v_eq map →
rank_formula (S n) f.
Lemma map_rank_append :
∀(n : nat)(map1 map2 : list (V × lambda_formula V L)),
map_rank n map1 →
map_rank n map2 →
assoc_mapping v_eq map1 →
map_rank n (map1 ++ map2).
Lemma map_rank_incl :
∀(n : nat)(map1 map2 : list (V × lambda_formula V L)),
incl map1 map2 →
map_rank n map2 →
assoc_mapping v_eq map2 →
map_rank n map1.
Definition var_chain_ends(map : list (V × lambda_formula V L))
(l : list V) : Prop :=
∀(v : V),
In v l ↔
(is_some (rassoc (lambda_formula_eq op_eq v_eq) map (lf_prop v)) ∧
is_none (assoc v_eq map v)).
(l : list V) : Prop :=
∀(v : V),
In v l ↔
(is_some (rassoc (lambda_formula_eq op_eq v_eq) map (lf_prop v)) ∧
is_none (assoc v_eq map v)).
Lemma divide_subst_prop :
∀(subst : lambda_subst V L)(n : nat)(pv : list V)
(smap : list (V × lambda_formula V L))
(rmap : list (V × V)),
divide_subst subst pv = (smap, rmap) →
rank_subst (S n) subst →
injective_assoc v_eq smap ∧
map_subst_correct subst smap rmap pv ∧
assoc_mapping v_eq smap ∧
map_rank n smap.
Lemma collect_var_chain_ends_correct_ind :
∀(map orig : list (V × lambda_formula V L))(v : V),
In v (collect_var_chain_ends map orig)
↔
(is_some (rassoc (lambda_formula_eq op_eq v_eq) map (lf_prop v)) ∧
is_none (assoc v_eq orig v)).
Lemma collect_var_chain_ends_correct :
∀(map : list (V × lambda_formula V L)),
var_chain_ends map (collect_var_chain_ends map map).
Lemma unique_form_greater :
∀(map : list (V × lambda_formula V L))
(v1 v2 : V)(f1 f2 : lambda_formula V L),
assoc v_eq ((v1, f1) :: map) v2 = Some f2 →
formula_measure f2 < formula_measure (make_unique_form v1 f1 map).
Lemma rank_unique_form :
∀(n : nat)(map : list (V × lambda_formula V L))
(v : V)(f : lambda_formula V L),
assoc_mapping v_eq ((v, f) :: map) →
map_rank n ((v, f) :: map) →
rank_formula (S n) (make_unique_form v f map).
Lemma injective_assoc_fix_var_chain_ends :
∀(m : list (V × lambda_formula V L)),
injective_assoc v_eq m →
injective_assoc v_eq (fix_var_chain_ends m).
Lemma fix_var_chain_ends_no_ends :
∀(m : list (V × lambda_formula V L))(v1 v2 : V),
assoc v_eq (fix_var_chain_ends m) v1 = Some (lf_prop v2) →
assoc v_eq (fix_var_chain_ends m) v2 = None →
False.
Lemma injective_subst_of_fixed_map :
∀(map : list (V × lambda_formula V L)),
injective_assoc v_eq map →
injective (subst_of_map (fix_var_chain_ends map)).
Lemma subst_subst_of_fixed_map :
∀(subst : lambda_subst V L)(smap : list (V × lambda_formula V L))
(v1 v2 : V),
subst v1 = subst_of_map smap v2 →
is_some (assoc v_eq smap v2) →
subst v1 = subst_of_map (fix_var_chain_ends smap) v2.
Lemma weak_map_subst_correct_fix_var_chain_ends :
∀(subst rsubst : lambda_subst V L)
(smap : list (V × lambda_formula V L))(pv : list V),
subst_eq_on_vars subst (subst_compose (subst_of_map smap) rsubst) pv →
renaming rsubst →
(∀(v1 v2 : V),
In v1 pv →
rsubst v1 = lf_prop v2 →
is_some (assoc v_eq smap v2)) →
subst_eq_on_vars
subst
(subst_compose (subst_of_map (fix_var_chain_ends smap)) rsubst)
pv.
Lemma map_subst_correct_fix_var_chain_ends :
∀(subst : lambda_subst V L)(smap : list (V × lambda_formula V L))
(rmap : list (V × V))(pv : list V),
map_subst_correct subst smap rmap pv →
subst_eq_on_vars
subst
(subst_compose (subst_of_map (fix_var_chain_ends smap))
(rename_of_map rmap))
pv.
Lemma rank_subst_subst_of_fixed_map :
∀(n : nat)(m : list (V × lambda_formula V L)),
assoc_mapping v_eq m →
map_rank n m →
rank_subst (S n) (subst_of_map (fix_var_chain_ends m)).
Lemma factor_subst_property :
∀(subst : lambda_subst V L)(s : sequent V L)(n : nat),
rank_subst (S n) subst →
∃(rsubst inj_subst : lambda_subst V L),
renaming rsubst ∧
injective inj_subst ∧
rank_subst (S n) inj_subst ∧
subst_eq_on_vars subst (subst_compose inj_subst rsubst)
(prop_var_sequent s).
End Factor_subst.
Implicit Arguments divide_subst [V L].
Implicit Arguments subst_of_map [V L].
Implicit Arguments rename_of_map [V L].
Implicit Arguments fix_var_chain_ends [V L].
Implicit Arguments map_subst_correct [V L].
Implicit Arguments map_rank [V L].
Implicit Arguments divide_subst_prop [V L].
Implicit Arguments factor_subst_property [V L].