Library CoLoR.Term.Lambda.LSubs

CoLoR, a Coq library on rewriting and termination.
See the COPYRIGHTS and LICENSE files.
  • Frederic Blanqui, 2012-04-05

Higher-order simultaneous substitutions

This formalization is inspired by the definition of a substitution of one variable given by Haskell Curry and Robert Feys in Combinatory Logic, volume 1, 1958, page 94 (written CF in the following). In order to be able to use this in the context of higher-order rewriting, which is more general than pure lambda-calculus, we instead define the simultaneous substitution of any number of variables.

Set Implicit Arguments.


Definition of substitution.


Module Export Def.

Parameters.

  Section subs.

We assume given decidable sets F and X for function symbols and variables respectively.

    Variables (F X : Type)
      (eq_fun_dec : forall f g : F, {f=g}+{~f=g})
      (eq_var_dec : forall x y : X, {x=y}+{~x=y}).

    Notation Te := (@Te F X).
    Notation Var := (@Var F X).
    Notation eq_term_dec := (@eq_term_dec F X eq_fun_dec eq_var_dec).
    Notation beq_term := (bool_of_rel eq_term_dec).

We assume given a structure for finite sets on X.

    Variable ens_X : Ens X.

    Notation empty := (Ens_empty ens_X).
    Notation mem := (Ens_mem ens_X).
    Notation add := (Ens_add ens_X).
    Notation union := (Ens_union ens_X).
    Notation remove := (Ens_remove ens_X).
    Notation fold := (Ens_fold ens_X).
    Notation In := (Ens_In ens_X).

    Notation fv := (@fv F X ens_X).

We assume that X is infinite.

    Variable var_notin : Ens_type ens_X -> X.

Type for substitutions:

a substitution is given by a total function from X to Te.
Identity substitution.

    Definition id := fun y => Var y.

update x t s is the substitution mapping x to t and any other variable y to s y.

    Definition update x (t : Te) s := fun y =>
      match eq_var_dec y x with
        | left _ => t
        | _ => s y
      end.

single x t is the substitution mapping x to t and leaving any other variable unchanged.

    Definition single x t := update x t id.

restrict xs s is the substitution mapping any variable z of xs to s z and leaving any other variable unchanged.

    Definition restrict xs s z := if mem z xs then s z else Var z.

"Domain" of a substitution: given a substitution s and a finite set xs, domain s xs is the set of variables x in xs such that s x <> Var x. It is defined by iteration of the function domain_fun on xs.

    Definition domain_fun s x xs :=
      if beq_term (s x) (Var x) then xs else add x xs.

    Definition domain xs s := fold (domain_fun s) xs empty.

Free variables of the "codomain" of a substitution: given a substitution s and a finite set xs, fvcod s xs is the union of the free variables of s x for every x in xs. It is defined by iteration of the function fvcod_fun on xs.

    Definition fvcod_fun s (x : X) xs := union (fv (s x)) xs.

    Definition fvcod xs s := fold (fvcod_fun s) xs empty.

Let fvcodom be the composition of fvcod and domain.

    Definition fvcodom xs s := fvcod (domain xs s) s.

Substitution with variable capture.

    Fixpoint subs1 s (t : Te) :=
      match t with
        | Def.Var x => s x
        | Def.Fun f => t
        | Def.App u v => App (subs1 s u) (subs1 s v)
        | Def.Lam x u => Lam x (subs1 (update x (Var x) s) u)
      end.

    Definition rename1 y z := subs1 (single y (Var z)).

    Definition comp1 s2 s1 (x:X) := subs1 s2 (s1 x).

Generation of a fresh variable.

    Definition var x u s :=
      let xs := fvcodom (remove x (fv u)) s in
        if mem x xs then var_notin (union (fv u) xs) else x.

subs: Effect of a substitution on a term. When applying s on Lam x u, if x belongs to the set xs of the free variables of the codomain of s w.r.t. the free variables of Lam x u, then x is renamed into a variable var s x u not belonging to fv u nor xs.
In Curry-Feys, subs is only defined for substitutions s of the form single y v and subs (Lam x u) is defined as Lam x' (subs s (rename x x' u)) where:
  • rename x x' = subs (single x (Var x')),
It is not possible to have a similar definition in Coq because the inner recursive call is not recognized by Coq as preserving the size of its argument. Considering simultaneous substitutions and update avoid this problem.
  • x' = if negb (eqb x y) && mem y (fv u) && mem x (fv v) then var_notin (union (fv u) (add y (fv v))) else x.
With our definition, after Lemma var_single proved below, for x', we get if negb (eqb x y) && mem y (fv u) && mem x (fv v) && negb (beq_term v (Var y)) then var_notin (union (fv u) (fv v)) else x. Hence, we do a renaming only if v <> Var y (i.e. if s is not the identity), and x can be renamed into y. In Curry-Feys definition, renaming x into y would not be correct. For instance, with s = single y (Var x) and u = Var x, we would have subs (single y (Var x)) (Lam x (Var x)) = Lam y (subs (single y (Var x)) (rename x y (Var x))) = Lam y (Var x) instead of a term alpha-equivalent to Lam x (Var x). With our definition, this is correct since we use simultaneous substitutions instead of the composition of two substitutions. In the example, we have subs (single y (Var x)) (Lam x (Var x)) = Lam y (subs (update x (Var y) (single y (Var x))) (Var x)) = Lam y (Var y).
In "Substitution Revisited", Theoretical Computer Science 59:317-325, 1988, Allen Stoughton defines higher-order simultaneous substitutions too, but by always renaming bound variables, i.e. var x u s = choice (new x u s) where new x u s is the complement of fvcodom (remove x (fv u)) s and choice:XSet.t -> X is a choice function (In (choice A) A if A is not empty).

    Fixpoint subs s (t : Te) :=
      match t with
        | Def.Var x => s x
        | Fun f => t
        | App u v => App (subs s u) (subs s v)
        | Lam x u =>
          let x' := var x u s in Lam x' (subs (update x (Var x') s) u)
      end.

    Definition rename y z := subs (single y (Var z)).

    Definition subs_single x u := subs (single x u).

Composition of two substitutions.

    Definition comp s2 s1 (x : X) := subs s2 (s1 x).

Closure by substitution of a relation on terms.
Note that clos_subs R is a priori NOT stable by substitution since substitution composition is correct modulo alpha-equivalence only (Lemma subs_comp in LAlpha).

    Inductive clos_subs R : rel Te :=
    | subs_step : forall x y s, R x y -> clos_subs R (subs s x) (subs s y).

Point-wise extension of a relation to substitutions.

    Definition subs_rel (R : rel Te) xs s s' :=
      forall x : X, In x xs -> R (s x) (s' x).

  End subs.


End Def.

Properties of substitution.


Module Make (Export L : L_Struct).

Notations for substitutions and related definitions.

  Notation id := (@id F X).
  Notation update := (@update F X XOrd.eq_dec).
  Notation single := (@single F X XOrd.eq_dec).
  Notation restrict := (@restrict F X ens_X).
  Notation domain_fun := (@domain_fun F X FOrd.eq_dec XOrd.eq_dec ens_X).
  Notation domain := (@domain F X FOrd.eq_dec XOrd.eq_dec ens_X).
  Notation fvcod_fun := (@fvcod_fun F X ens_X).
  Notation fvcod := (@fvcod F X ens_X).
  Notation fvcodom := (@fvcodom F X FOrd.eq_dec XOrd.eq_dec ens_X).
  Notation var := (@var F X FOrd.eq_dec XOrd.eq_dec ens_X var_notin).
  Notation subs1 := (@subs1 F X XOrd.eq_dec).
  Notation rename1 := (@rename1 F X XOrd.eq_dec).
  Notation comp1 := (@comp1 F X XOrd.eq_dec).
  Notation subs := (@subs F X FOrd.eq_dec XOrd.eq_dec ens_X var_notin).
  Notation subs_single :=
    (@subs_single F X FOrd.eq_dec XOrd.eq_dec ens_X var_notin).
  Notation comp := (@comp F X FOrd.eq_dec XOrd.eq_dec ens_X var_notin).
  Notation rename := (@rename F X FOrd.eq_dec XOrd.eq_dec ens_X var_notin).
  Notation clos_subs :=
    (@clos_subs F X FOrd.eq_dec XOrd.eq_dec ens_X var_notin).
  Notation subs_rel := (@subs_rel F X ens_X).

  Module Export T := LTerm.Make L.

Basic properties.

  Instance rename_proper_eq A B : Proper (Logic.eq ==> A ==> B) subs ->
    Proper (Logic.eq ==> Logic.eq ==> A ==> B) rename.


  Lemma update_eq x u s : update x u s x = u.

  Lemma update_neq x u s y : x <> y -> update x u s y = s y.

  Lemma single_eq y v : single y v y = v.

  Lemma single_neq y v z : y <> z -> single y v z = Var z.

Predicate saying that the domain of a substitution is included in some finite set.

  Definition dom_incl xs s := forall x, ~In x xs -> s x = Var x.

  Instance dom_incl_e : Proper (Equal ==> Logic.eq ==> iff) dom_incl.


  Instance dom_incl_s : Proper (Subset ==> Logic.eq ==> impl) dom_incl.


  Lemma dom_incl_restrict s xs : dom_incl xs (restrict xs s).

Properties of subs_rel.


  Lemma subs_rel_update (R : rel Te) xs x u u' s s' :
    R u u' -> subs_rel R (remove x xs) s s'
    -> subs_rel R xs (update x u s) (update x u' s').

Preserved properties.

  Instance subs_rel_refl R xs : Reflexive R -> Reflexive (subs_rel R xs).


  Instance subs_rel_sym R xs : Symmetric R -> Symmetric (subs_rel R xs).


  Instance subs_rel_trans R xs : Transitive R -> Transitive (subs_rel R xs).


subs_rel R is compatible with set inclusion and equality.

Syntactic equality of two substitutions

on some finite set of variables

  Notation seq := (subs_rel Logic.eq).

  Lemma seq_restrict xs ys s : xs [<=] ys -> seq xs s (restrict ys s).

Properties of domain.

domain_fun is compatible with set inclusion and equality and commutes with add.
domain is compatible with set equality.
Set equalities on domain.

  Lemma domain_empty s : domain empty s [=] empty.

  Lemma domain_add s x xs : ~In x xs ->
    domain (add x xs) s [=] domain_fun s x (domain xs s).

Correctness proof of the definition of domain.

  Lemma In_domain x s : forall xs,
    In x (domain xs s) <-> In x xs /\ s x <> Var x.

  Lemma mem_domain x s xs :
    mem x (domain xs s) = mem x xs && negb (beq_term (s x) (Var x)).

  Lemma notin_domain s xs x :
    domain xs s [=] empty -> In x xs -> s x = Var x.

domain is compatible with set inclusion.

  Instance domain_s : Proper (Subset ==> Logic.eq ==> Subset) domain.


  Lemma domain_subset s xs : domain xs s [<=] xs.

More set equalities on domain.

  Lemma domain_singleton s x : domain (singleton x) s
    [=] if beq_term (s x) (Var x) then empty else singleton x.

  Lemma domain_union s p q :
    domain (union p q) s [=] union (domain p s) (domain q s).

  Lemma domain_single y v : forall xs, domain xs (single y v)
    [=] if mem y xs && negb (beq_term v (Var y)) then singleton y else empty.

  Lemma domain_rename y z xs : domain xs (single y (Var z))
    [=] if mem y xs && negb (eqb z y) then singleton y else empty.

  Lemma domain_single_empty y v xs :
    domain xs (single y v) [=] empty <-> ~In y xs \/ v = Var y.

  Lemma domain_id : forall xs, domain xs id [=] empty.

  Lemma domain_update_id x s xs :
    domain xs (update x (Var x) s) [=] domain (remove x xs) s.

domain is compatible with subs_rel.

  Instance domain_subs_rel_Subset (R : rel Te) : VarInvL R ->
    forall xs, Proper (subs_rel R xs --> Subset) (domain xs).


  Instance domain_subs_rel_Equal (R : rel Te) : VarInvL R -> VarInvR R ->
    forall xs, Proper (subs_rel R xs ==> Equal) (domain xs).


Properties of fvcod.

fvcod_fun is compatible with set equality and commutes with add.
fvcod is compatible with set equality.
Set equalities on fvcod.

  Lemma fvcod_empty s : fvcod empty s [=] empty.

  Lemma fvcod_add s x xs : ~In x xs ->
    fvcod (add x xs) s [=] fvcod_fun s x (fvcod xs s).

Correctness proof of fvcod.

  Lemma In_fvcod y s : forall xs,
    In y (fvcod xs s) <-> exists x, In x xs /\ In y (fv (s x)).

fvcod is compatible with inclusion.
More equalities on fvcod.

  Lemma fvcod_singleton s x : fvcod (singleton x) s [=] fv (s x).

  Lemma fvcod_union s p q :
    fvcod (union p q) s [=] union (fvcod p s) (fvcod q s).

  Lemma fvcod_single y v : forall xs, fvcod xs (single y v)
    [=] if mem y xs then union (fv v) (remove y xs) else xs.

  Lemma fvcod_rename y z xs : fvcod xs (single y (Var z))
    [=] if mem y xs then add z (remove y xs) else xs.

  Lemma fvcod_id : forall xs, fvcod xs id [=] xs.

fvcod is compatible with subs_rel.

  Instance fvcod_subs_rel_Subset R : Proper (R --> Subset) fv ->
    forall xs, Proper (subs_rel R xs --> Subset) (fvcod xs).


  Instance fvcod_subs_rel_Equal R : Proper (R ==> Equal) fv ->
    forall xs, Proper (subs_rel R xs ==> Equal) (fvcod xs).


Properties of fvcodom.

fvcodom is compatible with set inclusion and equality.
Correctness of fvcodom.

  Lemma In_fvcodom s xs y : In y (fvcodom xs s)
    <-> (exists x, In x xs /\ s x <> Var x /\ In y (fv (s x))).


  Lemma fvcodom_singleton s x : fvcodom (singleton x) s
    [=] if beq_term (s x) (Var x) then empty else fv (s x).

  Lemma fvcodom_union s p q :
    fvcodom (union p q) s [=] union (fvcodom p s) (fvcodom q s).

  Lemma fvcodom_id xs : fvcodom xs id [=] empty.

  Lemma fvcodom_single y v xs : fvcodom xs (single y v)
    [=] if mem y xs && negb (beq_term v (Var y)) then fv v else empty.

  Lemma fvcodom_rename y z xs : fvcodom xs (single y (Var z))
    [=] if mem y xs && negb (eqb z y) then singleton z else empty.

  Lemma fvcodom_update_id x s xs :
    fvcodom xs (update x (Var x) s) [=] fvcodom (remove x xs) s.

fvcodom is compatible with subs_rel.

  Instance fvcodom_subs_rel_Subset R :
    Proper (R --> Subset) fv -> VarInvL R ->
    forall xs, Proper (subs_rel R xs --> Subset) (fvcodom xs).


  Instance fvcodom_subs_rel_Equal R :
    Proper (R ==> Equal) fv -> VarInvL R -> VarInvR R ->
    forall xs, Proper (subs_rel R xs ==> Equal) (fvcodom xs).


Properties of var.


  Lemma var_subs_rel R :
    Proper (R ==> Equal) fv -> VarInvL R -> VarInvR R ->
    forall x u, Proper (subs_rel R (remove x (fv u)) ==> Logic.eq) (var x u).


  Instance var_seq x u : Proper (seq (remove x (fv u)) ==> Logic.eq) (var x u).



  Lemma var_notin_fvcodom x u s :
    ~In (var x u s) (fvcodom (remove x (fv u)) s).

  Lemma var_notin_fv_subs x u s y :
    In y (fv u) -> y <> x -> ~In (var x u s) (fv (s y)).


  Lemma var_notin_fvcod x u s : ~In (var x u s) (fvcod (remove x (fv u)) s).

Properties of subs.


  Lemma fold_subs_single x u : subs (single x u) = subs_single x u.

  Lemma subs_lam_no_alpha s x u :
    ~In x (fvcodom (remove x (fv u)) s) ->
    subs s (Lam x u) = Lam x (subs (update x (Var x) s) u).

  Lemma subs_apps s : forall n (us : Tes n) t,
    subs s (apps t us) = apps (subs s t) (Vmap (subs s) us).

Given u, fun s => subs s u is compatible with subs_rel R (fv u).

  Lemma subs_rel_mon_preorder R : PreOrder R -> Monotone R ->
    Proper (R ==> Equal) fv -> VarInvL R -> VarInvR R ->
    forall u s s', subs_rel R (fv u) s s' -> R (subs s u) (subs s' u).

  Lemma subs_seq u s s' : seq (fv u) s s' -> subs s u = subs s' u.


  Lemma subs_seq_restrict u s : subs s u = subs (restrict (fv u) s) u.

Applying the identity substitution does not change the term (extension of CF, Theorem 1a, page 95, proof given on page 97).

  Lemma subs_id : forall u, subs id u = u.

Applying on a term u a substitution which domain w.r.t. fv u is empty does not change the term (CF, Theorem 1b, page 95, proof given on page 98).

  Lemma subs_notin_fv u s : domain (fv u) s [=] empty -> subs s u = u.

Free variables of a substituted term.

  Lemma fv_subs : forall u s, fv (subs s u)
    [=] let xs := domain (fv u) s in union (diff (fv u) xs) (fvcod xs s).

  Lemma fvcod_subset_fv_subs s u : fvcod (fv u) s [<=] fv (subs s u).

Stability by substitution.


  Section stable.

    Definition stable R := Proper (Logic.eq ==> R ==> R) subs.

    Instance stable_same : Proper (same ==> impl) stable.


    Instance stable_same_iff : Proper (same ==> iff) stable.


    Lemma stable_union R S : stable R -> stable S -> stable (R U S).

  End stable.

clos_subs preserves free variables.


  Instance fv_clos_subs R :
    Proper (R --> Subset) fv -> Proper (clos_subs R --> Subset) fv.


Some equalities on update.


  Lemma update2_eq x u v w s :
    subs (update x v (update x w s)) u = subs (update x v s) u.

  Lemma update2_neq_com s x u y v w : x <> y ->
    subs (update x u (update y v s)) w = subs (update y v (update x u s)) w.

  Lemma update_single_eq y v w u :
    subs (update y w (single y v)) u = subs (single y w) u.

  Lemma update2_single_eq y w x v v' u :
    subs (update y w (update x v' (single x v))) u
    = subs (update y w (single x v')) u.

  Lemma update_id x s u :
    s x = Var x -> subs (update x (Var x) s) u = subs s u.

  Lemma update_id_single y v x u : x<>y \/ v=Var x ->
    subs (update x (Var x) (single y v)) u = subs (single y v) u.

Some equalities on single.

CF, Theorem 1a, page 95, proof page 97.

  Lemma single_id y u : subs (single y (Var y)) u = u.

CF, Theorem 1b, page 95, proof page 98.

  Lemma single_notin_fv y u v : ~In y (fv v) -> subs (single y u) v = v.

Other equalities on single.

  Lemma single_var x u s v z : In z (fv u) -> x <> z ->
    subs (single (var x u s) v) (s z) = s z.

  Lemma var_single y v x u : var x u (single y v) =
    if mem y (fv u) && negb (eqb x y) && negb (beq_term v (Var y))
      && mem x (fv v) then var_notin (union (fv u) (fv v)) else x.

  Lemma single_lam_no_alpha y v x u :
    ~In y (fv u) \/ x=y \/ v=Var y \/ ~In x (fv v) ->
    subs (single y v) (Lam x u)
    = Lam x (subs (update x (Var x) (single y v)) u).

  Lemma fv_single y v u : fv (subs (single y v) u) [=]
    if mem y (fv u) then union (remove y (fv u)) (fv v) else fv u.

  Lemma single_update x y u v s :
    ~In y (remove x (fv u)) -> ~In y (fvcodom (remove x (fv u)) s) ->
    subs (comp (single y v) (update x (Var y) s)) u = subs (update x v s) u.

  Lemma single_update_var x u v s :
    subs (comp (single (var x u s) v) (update x (Var (var x u s)) s)) u
    = subs (update x v s) u.

Some equalities on single renamings.


  Lemma rename_id x u : rename x x u = u.

  Lemma rename_notin_fv x y u : ~In x (fv u) -> rename x y u = u.

  Lemma rename_var y z x : rename y z (Var x) = Var (if eqb x y then z else x).

  Lemma rename_fun x y f : rename x y (Fun f) = Fun f.

  Lemma rename_app y z u v :
    rename y z (App u v) = App (rename y z u) (rename y z v).

  Lemma var_rename y z x u : var x u (single y (Var z))
    = if mem y (fv u) && negb (eqb x y) && eqb z x
      then var_notin (add z (fv u)) else x.

  Lemma fv_rename y z u : fv (rename y z u) [=] replace y z (fv u).

  Lemma rename_lam_no_alpha y z x u :
    ~In y (fv u) \/ x=y \/ x<>z -> rename y z (Lam x u)
    = Lam x (subs (update x (Var x) (single y (Var z))) u).

  Lemma remove_fv_rename x y u : ~In y (fv u) ->
    remove y (fv (rename x y u)) [=] remove x (fv u).

Renamings: substitutions mapping variables to variables.


  Definition renaming s := exists m, forall x : X, s x = Var (m x).

Applying a renaming preserves the size.

  Lemma size_renaming1 : forall u s, renaming s -> size (subs1 s u) = size u.

  Lemma size_renaming : forall u s, renaming s -> size (subs s u) = size u.

rename is a renaming.

  Lemma renaming_update s y z : renaming s -> renaming (update y (Var z) s).

  Lemma renaming_single y z : renaming (single y (Var z)).

  Lemma size_rename1 x y u : size (rename1 x y u) = size u.

  Lemma size_rename x y u : size (rename x y u) = size u.

Preservation of bound variables by some renaming.


  Lemma bv_rename x y : forall u, ~In y (bv u) -> bv (rename x y u) [=] bv u.

Bound variables of the "codomain" of a substitution:

given a substitution s and a finite set xs, bvcod s xs is the union of the bound variables of s x for every x in xs. It is defined by iteration of the function bvcod_fun on xs.

  Definition bvcod_fun s (x : X) xs := union (bv (s x)) xs.

bvcod_fun is compatible with set equality and commutes with add.

  Instance bvcod_fun_e :
    Proper (Logic.eq ==> Logic.eq ==> Equal ==> Equal) bvcod_fun.


  Lemma bvcod_fun_transp s : transpose Equal (bvcod_fun s).

  Definition bvcod xs s := fold (bvcod_fun s) xs empty.

bvcod is compatible with set equality.
Set equalities on bvcod.

  Lemma bvcod_empty s : bvcod empty s [=] empty.

  Lemma bvcod_add s x xs : ~In x xs ->
    bvcod (add x xs) s [=] bvcod_fun s x (bvcod xs s).

Correctness proof of bvcod.

  Lemma In_bvcod y s : forall xs,
    In y (bvcod xs s) <-> exists x, In x xs /\ In y (bv (s x)).

bvcod is compatible with inclusion.
More equalities on bvcod.

  Lemma bvcod_singleton s x : bvcod (singleton x) s [=] bv (s x).

  Lemma bvcod_union s p q :
    bvcod (union p q) s [=] union (bvcod p s) (bvcod q s).

  Lemma bvcod_single y v : forall xs,
    bvcod xs (single y v) [=] if mem y xs then bv v else empty.

  Lemma bvcod_rename y z xs : bvcod xs (single y (Var z)) [=] empty.

  Lemma bvcod_id : forall xs, bvcod xs id [=] empty.

  Lemma bvcod_update x u s xs :
    bvcod xs (update x u s) [=]
    union (if mem x xs then bv u else empty) (bvcod (remove x xs) s).

bvcod is compatible with substitution equality.

  Lemma bvcod_seq xs xs' : xs [=] xs' ->
    forall s s', seq xs s s' -> bvcod xs s [=] bvcod xs' s'.

  Instance bvcod_seq' xs : Proper (seq xs ==> Equal) (bvcod xs).


Commutation properties

when free variables are distinct from bound variables.
In fact, these properties won't be used later. Instead, we will use similar properties but with another renaming-free substitution function subs1 defined hereafter, which is equivalent when bound variables are distinct from free variables(Lemma subs1_no_alpha) but easier to work with, and whose properties are easier to established.
CF, Theorem 1c, page 95, proof page 98.

  Lemma single_com x y v w : x<>y -> forall u,
    ~In x (fv w) \/ ~In y (fv u) ->
    inter (bv u) (union (fv v) (fv w)) [=] empty ->
    subs (single y w) (subs (single x v) u)
    = subs (single x (subs (single y w) v)) (subs (single y w) u).

  Lemma update_single_split : forall u x y v w, x<>y -> ~In y (fv v) ->
    inter (bv u) (union (fv v) (fv w)) [=] empty ->
    subs (update y w (single x v)) u = subs (single y w) (subs (single x v) u).

  Lemma update_single_split_swap : forall u x y v w, x<>y -> ~In x (fv w) ->
    inter (bv u) (union (fv v) (fv w)) [=] empty ->
    subs (update y w (single x v)) u = subs (single x v) (subs (single y w) u).

  Lemma subs_lam s x u :
    subs s (Lam x u) = subs (update x (Var x) s) (Lam x u).

  Lemma rename_lam x y z u : rename x y (Lam z u) =
    if mem x (fv u) && negb (eqb y x) && eqb y z then
      let z' := var_notin (add y (fv u)) in
        Lam z' (subs (update z (Var z') (single x (Var y))) u)
    else if eqb z x then Lam z u else Lam z (rename x y u).

  Lemma rename_subs_com x y :
    forall u s, s x = Var x -> s y = Var y -> ~In x (fvcodom (fv u) s) ->
      inter (bv u) (add y (fvcodom (fv u) s)) [=] empty ->
      rename x y (subs s u) = subs s (rename x y u).

Properties of subs1.

Given u, fun s => subs s u is compatible with subs_rel R (fv u).

  Lemma subs1_rel_mon_preorder R : PreOrder R -> Monotone R ->
    forall u s s', subs_rel R (fv u) s s' -> R (subs1 s u) (subs1 s' u).

Bound variables of a term of the form subs1 s u (CF, Lemma 3, page 99).

  Lemma bv_subs1 : forall u s,
    bv (subs1 s u) [<=] union (bv u) (bvcod (fv u) s).

subs1 s u equals u if no free variable of u is in the domain of s.

  Lemma subs1_notin_fv : forall u s,
    domain (fv u) s [=] empty -> subs1 s u = u.

subs s u is equivalent to subs1 s u if no bound variable of u occurs in fvcodom (fv u) s.

  Lemma subs1_no_alpha : forall u s,
    inter (bv u) (fvcodom (fv u) s) [=] empty -> subs s u = subs1 s u.

  Lemma rename1_no_alpha u x y :
    x=y \/ ~In x (fv u) \/ ~In y (bv u) -> rename x y u = rename1 x y u.

subs1 s1 u equals subs1 s2 u if s1 and s2 are equal on the free variables of u.

  Lemma subs1_seq : forall u s1 s2, (forall x, In x (fv u) -> s1 x = s2 x) ->
    subs1 s1 u = subs1 s2 u.

Other properties of subs1.

  Lemma subs1_update2_eq x u v w s :
    subs1 (update x v (update x w s)) u = subs1 (update x v s) u.

  Lemma subs1_update2_neq_com s x u y v w : x <> y ->
    subs1 (update x u (update y v s)) w = subs1 (update y v (update x u s)) w.

  Lemma subs1_update_single_eq y v w u :
    subs1 (update y w (single y v)) u = subs1 (single y w) u.

  Lemma subs1_update2_single_eq y w x v v' u :
    subs1 (update y w (update x v' (single x v))) u
    = subs1 (update y w (single x v')) u.

  Lemma subs1_update_id x s u : s x = Var x ->
    subs1 (update x (Var x) s) u = subs1 s u.

  Lemma subs1_id : forall u, subs1 id u = u.

  Lemma subs1_single_id y u : subs1 (single y (Var y)) u = u.

  Lemma subs1_update_id_single y v x u : x<>y \/ v=Var x ->
    subs1 (update x (Var x) (single y v)) u = subs1 (single y v) u.

  Lemma subs1_update_single_id y v x u :
    subs1 (update y v (single x (Var x))) u = subs1 (single y v) u.

Composition properties of subs1.

  Lemma subs1_update_single x y y' : forall u s, ~In y (bv u) ->
    subs1 (update y (Var y') s) (subs1 (single x (Var y)) u)
    = subs1 (update x (Var y') (update y (Var y') s)) u.

  Lemma subs1_single_subs1 y v : forall u s, s y = Var y ->
    ~In y (fvcodom (fv u) s) ->
    subs1 (single y v) (subs1 s u) = subs1 (update y v s) u.

  Lemma subs1_single_update x x' y' : forall u s, ~In x' (fv u) ->
    ~In x' (fvcodom (remove x (fv u)) s) -> ~In x' (bv u) -> ~In x (bv u) ->
    subs1 (single x' (Var y')) (subs1 (update x (Var x') s) u)
    = subs1 (update x' (Var y') (update x (Var y') s)) u.

  Lemma subs1_comp : forall u s1 s2,
    inter (bv u) (fvcodom (fv u) s1) [=] empty ->
    subs1 s2 (subs1 s1 u) = subs1 (comp1 s2 s1) u.

End Make.