Factorize two substitutions

The syntactic cut elimination proof (5.6 (3) case a 2) needs to factorize two substitutions into one injetive substitution and two renamings. To stay constructive, I do something weaker. Given two pairs of sequents and substitutions s1, sigma1 and s2, sigma2, I construct an injective sigma_i and a two renamings sigma_r1 and sigma_r2, such that
  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
The basic idea is to split the substitutions sigma1 and sigma2 separately with the machinery of module factor_subst and combine the two resulting substitutions. There are, however, two slight complications.
The first complication is that the join of the two substitutions works only if the two mappings to be joined have disjoint domains. Therefore, I rename all clashing variables in s2 before splitting sigma2. Of course, this renaming has to be taken into account at various places.
The second complication is that the two injective substitutions that I get from the factorization may map different variables to the same formula. In order to deliver an injective substitution in the end, the join collects these duplications into a separate renaming. This renaming must be inserted into the substitution chain of s2 at a suitable place.

Require Export factor_subst.

Section Factor_two_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

This function uses the enumeration f to find a fresh variable that does not occur in used. For the initial call bound must be greater or equal then the length of used. We check bound + 1 variables from f, always incrementing the f-argument. At least one of those cannot occur in used. The argument n is the starting index for f. The next index to be used with f is returned as second result.
  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.

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.

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.

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

rename_of_map substitution Properties


  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.

next_unused_var Properties


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

rename_disjoint Properties


  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.

join_subst_maps Properties


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

Final Properties


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