Factorize substitutions

The syntactic proof of contraction and cut elimination need to factorize a substituion into an injective substitution and a renaming. To stay constructive, I do something weaker. Given a sequent s and a substitutions sigma, I construct an injective sigma_i and a renaming sigma_r, such that
    subst_sequent sigma s = subst_sequent (subst_compose sigma_i sigma_r) s
The main idea for the construction is simple. Starting from the identity substitution and the identity renaming, I consider all propositional variables v in s. If I find sigma v in the codomain of sigma_i, then I add a suitable renaming in sigma_r. Otherwise the mapping v → sigma v is added to sigma_i.
In order to work with finite, searchable data structures, I first collect the mappings for sigma_i and sigma_r in lists. At the end, these lists are converted into functions.
A problem arises if sigma maps v to lf_prop v' for a v' that does not appear in s. Then the resulting substitution sigma_i would map both v and v' to lf_prop v', breaking injectivity.
To fix this problem, I collect all such problematic v', which are called variable-chain end points, var_chain_ends. For each such v' I add a mapping v' → f to sigma_i, for an f that is unique in the codomain of sigma_i. To construct such an f, I include v' in f and the conjuntion of all formulas in s. Thus, f is bigger then all formulas that were originally in the codomain of sigma_i and it is different from all mappings that are added to fix variable-chain ends.
The contraction proof relies directly on the properties proved here. The cut-elimination proof needs something more complicated, see factor_two_subst.

Require Export assoc renaming sequent_support.

Section Factor_subst.

  Variable V : Type.
  Variable L : modal_operators.

Need decidable equalitities for the factoring
  Variable op_eq : eq_type (operator L).
  Variable v_eq : eq_type V.

Functions definitions

subst is the substitution to factorize and pv are the variables occurring in s (see above). The first returned list are the mappings for an injective substitution, the second are the mappings for the renaming.
  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.

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.

(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).

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)).

rename_of_map properties


  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

map_subst_correct expresses that
  • (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).

map_rank

The substitution mapping has some rank.
  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.

var_chain_ends

defining property of the variable-chain end points
  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)).

divide_subst Properties


  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.

var_chain_ends Properties


  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).

unique form Properties


  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).

rename_of_map Properties


  Lemma renaming_rename_of_map : ∀(m : list (V × V)),
    renaming (rename_of_map m).

fix_var_chain Properties


  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)).

Final Properties


  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].