# Library CoLoR.Term.WithArity.ASubstitution

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
• Frederic Blanqui, 2005-01-27
• Sebastien Hinderer, 2004-02-10
• Pierre-Yves Strub, 2009-04-13
substitutions

Set Implicit Arguments.

Section S.

Variable Sig : Signature.

Notation term := (term Sig). Notation terms := (vector term).

definition of substitutions as interpretations in terms

Definition I0 := mkInterpretation (Var 0) (@Fun Sig).

Definition substitution := valuation I0.

Definition id : substitution := fun x => Var x.

Definition single x t : substitution :=
fun y => if beq_nat x y then t else Var y.

application of a substitution

Definition sub : substitution -> term -> term := @term_int Sig I0.

Lemma sub_fun s f v : sub s (Fun f v) = Fun f (Vmap (sub s) v).

Lemma sub_id : forall t, sub id t = t.

Lemma fun_eq_sub f ts s u : Fun f ts = sub s u ->
{exists us, u = Fun f us} + {exists x, u = Var x}.

Lemma vars_eq_sub n s u : Var n = sub s u -> exists m, u = Var m.

Lemma sub_eq s1 s2 t :
(forall x, In x (vars t) -> s1 x = s2 x) -> sub s1 t = sub s2 t.

Lemma sub_eq_id s t :
(forall x, In x (vars t) -> s x = Var x) -> sub s t = t.

Lemma Vmap_sub_eq s1 s2 n (ts : terms n) :
(forall x, In x (vars_vec ts) -> s1 x = s2 x) ->
Vmap (sub s1) ts = Vmap (sub s2) ts.

Lemma subeq_inversion :
forall u θ θ', sub θ u = sub θ' u -> forall x, In x (vars u) -> θ x = θ' x.

Lemma sub_single_not_var x u t : ~In x (vars t) -> sub (single x u) t = t.

composition

Definition sub_comp (s1 s2 : substitution) : substitution :=
fun x => sub s1 (s2 x).

Lemma sub_sub s1 s2 t : sub s1 (sub s2 t) = sub (sub_comp s1 s2) t.

Lemma sub_comp_assoc s1 s2 s3 x :
sub_comp (sub_comp s1 s2) s3 x = sub_comp s1 (sub_comp s2 s3) x.

extension of a substitution

Definition extend (s : substitution) x v : substitution :=
fun y => if beq_nat y x then v else s y.

Lemma sub_extend_notin s x v u :
~In x (vars u) -> sub (extend s x v) u = sub s u.

Lemma sub_comp_single_extend s x v (t : term) :
sub (sub_comp s (single x v)) t = sub (extend s x (sub s v)) t.

Lemma sub_comp_single s x (u : term) : s x = sub s u ->
forall t, sub (sub_comp s (single x u)) t = sub s t.

substitution lemma for interpretations

Section substitution_lemma.

Variable I : interpretation Sig.

Definition beta (xint : valuation I) (s : substitution) x :=
term_int xint (s x).

Lemma substitution_lemma xint s t :
term_int xint (sub s t) = term_int (beta xint s) t.

End substitution_lemma.

variables of a substitution

Section vars.

Variable s : substitution.

Fixpoint svars (l : variables) : variables :=
match l with
| nil => nil
| x :: l' => vars (s x) ++ svars l'
end.

Lemma in_svars_intro x y :
forall l, In x (vars (s y)) -> In y l -> In x (svars l).

Lemma in_svars_elim x :
forall l, In x (svars l) -> exists y, In y l /\ In x (vars (s y)).

Lemma svars_app l2 : forall l1, svars (l1 ++ l2) = svars l1 ++ svars l2.

Lemma incl_svars l1 l2 : incl l1 l2 -> incl (svars l1) (svars l2).

Lemma vars_sub : forall t, vars (sub s t) = svars (vars t).

Lemma incl_vars_sub l r :
incl (vars r) (vars l) -> incl (vars (sub s r)) (vars (sub s l)).

End vars.

domain of a substitution

Definition dom_incl (s : substitution) (l : variables) :=
forall x, ~In x l -> s x = Var x.

Definition sub_eq_dom (s1 s2 : substitution) (l : variables) :=
forall x, In x l -> s1 x = s2 x.

Lemma sub_eq_dom_incl s1 s2 l1 l2 :
sub_eq_dom s1 s2 l2 -> incl l1 l2 -> sub_eq_dom s1 s2 l1.

Lemma sub_eq_dom_incl_sub s1 s2 l : sub_eq_dom s1 s2 l ->
forall t, incl (vars t) l -> sub s1 t = sub s2 t.

Lemma sub_eq_vars_sub s1 s2 t :
sub_eq_dom s1 s2 (vars t) -> sub s1 t = sub s2 t.

union of 2 substitutions ordered by the domain of the first: union s1 s2 x = s1 x if s1 x <> x, and s2 x otherwise

Section union.

Variables s1 s2 : substitution.

Definition union : substitution := fun x =>
match eq_term_dec (s1 x) (Var x) with
| left _ => s2 x
| right _ => s1 x
end.

Variables l1 l2 : variables.

Definition compat := forall x : variable, In x l1 -> In x l2 -> s1 x = s2 x.

Variables (hyp1 : dom_incl s1 l1) (hyp2 : dom_incl s2 l2) (hyp : compat).

Lemma union_correct1 : sub_eq_dom union s1 l1.

Lemma union_correct2 : sub_eq_dom union s2 l2.

Lemma sub_union1 t : incl (vars t) l1 -> sub union t = sub s1 t.

Lemma sub_union2 t : incl (vars t) l2 -> sub union t = sub s2 t.

End union.

union of 2 substitutions ordered by some index n: maxvar_union n s1 s2 x = s1 x if x < n, and s2 x otherwise

Section maxvar_union.

Variables (n : nat) (s1 s2 : substitution).

Definition maxvar_union : substitution := fun x =>
match lt_ge_dec x n with
| left _ => s1 x
| _ => s2 x
end.

End maxvar_union.

restriction of a substitution

Notation Inb := (Inb eq_nat_dec).

Definition restrict (s : substitution) (l : variables) : substitution :=
fun x => if Inb x l then s x else Var x.

Lemma restrict_var s l x : In x l -> restrict s l x = s x.

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

Lemma sub_eq_restrict s : forall l, sub_eq_dom (restrict s l) s l.

Lemma sub_restrict s t : sub s t = sub (restrict s (vars t)) t.

Lemma sub_restrict_incl s (l r : term) :
incl (vars r) (vars l) -> sub s r = sub (restrict s (vars l)) r.

substitution on contexts

Notation context := (context Sig).

Fixpoint subc (s : substitution) (c : context) : context :=
match c with
| Hole => Hole
| Cont f H v1 c' v2 =>
Cont f H (Vmap (sub s) v1) (subc s c') (Vmap (sub s) v2)
end.

Lemma sub_fill s u : forall C, sub s (fill C u) = fill (subc s C) (sub s u).

relation wrt subterm

Lemma subterm_eq_sub u t s :
subterm_eq u t -> subterm_eq (sub s u) (sub s t).

Lemma subterm_sub u t s : subterm u t -> subterm (sub s u) (sub s t).

Lemma subterm_eq_sub_elim : forall u t s, subterm_eq t (sub s u) ->
exists v, subterm_eq v u
/\ match v with
| Var x => subterm_eq t (s x)
| Fun f ts => t = sub s v
end.

function generating the sequence of terms Var 0, .., Var (n-1)

Definition fresh_vars n := @vec_of_val _ I0 (@Var Sig) n.

Lemma Vnth_fresh_vars n i (h : i<n) : Vnth (fresh_vars n) h = Var i.

Definition sub_vars n (ts : terms n) : substitution := val_of_vec I0 ts.

Lemma sub_fresh_vars n (ts : terms n) :
ts = Vmap (sub (sub_vars ts)) (fresh_vars n).

function generating the sequence of terms Var x0, .., Var (x0+n-1)

Fixpoint fresh (x0 n : nat) : terms n :=
match n as n return terms n with
| 0 => Vnil
| S n' => Vcons (Var x0) (fresh (S x0) n')
end.

Lemma fresh_plus :
forall n1 n2 x0, fresh x0 (n1+n2) = Vapp (fresh x0 n1) (fresh (x0+n1) n2).

Lemma fresh_tail x0 : forall n, fresh (S x0) n = Vtail (fresh x0 (S n)).

Lemma Vnth_fresh :
forall n i (h : i < n) x0, Vnth (fresh x0 n) h = Var (x0+i).

Lemma Vbreak_fresh p :
forall n k, Vbreak (fresh k (n+p)) = (fresh k n, fresh (k+n) p).

generates a list of variables

Fixpoint freshl (x0 n : nat) : list variable :=
match n with
| 0 => nil
| S n' => x0 :: freshl (S x0) n'
end.

Lemma in_freshl x :
forall n x0, ~In x (freshl x0 n) -> x < x0 \/ x >= x0 + n.

given a variable x0 and a vector v of n terms, fsub x0 n v is the substitution {x0+1 -> v1, .., x0+n -> vn}

Definition fsub x0 n (ts : terms n) x :=
match le_lt_dec x x0 with
| left _ => Var x
| right h1 =>
match le_lt_dec x (x0+n) with
| left h2 => Vnth ts (lt_pm h1 h2)
| _ => Var x
end
end.

Lemma fsub_inf x0 n (ts : terms n) x : x <= x0 -> fsub x0 ts x = Var x.

Lemma fsub_sup x0 n (ts : terms n) x : x > x0+n -> fsub x0 ts x = Var x.

Lemma fsub_nth x0 n (ts : terms n) x (h1 : x0 < x) (h2 : x <= x0+n) :
fsub x0 ts x = Vnth ts (lt_pm h1 h2).

Lemma fsub_cons x0 t n (ts : terms n) x :
x = x0+1 -> fsub x0 (Vcons t ts) x = t.

Lemma fsub_cons_rec x0 t n (ts : terms n) x k :
x = x0+2+k -> fsub x0 (Vcons t ts) x = fsub (x0+1) ts x.

Lemma fsub_cons_rec0 x0 t n (ts : terms n) x :
x = x0+2 -> fsub x0 (Vcons t ts) x = fsub (x0+1) ts x.

Lemma fsub_nil x0 x : fsub x0 Vnil x = Var x.

Lemma sub_fsub_inf n (ts : terms n) m :
forall t, maxvar t <= m -> sub (fsub m ts) t = t.

Lemma Vmap_fsub_fresh x0 n (ts : terms n) :
Vmap (sub (fsub x0 ts)) (fresh (S x0) n) = ts.

Lemma fsub_dom x0 n :
forall ts : terms n, dom_incl (fsub x0 ts) (freshl (x0+1) n).

Lemma fill_sub n f i vi j vj e s l : n >= maxvar l ->
fill (Cont f e vi Hole vj) (sub s l)
= sub (maxvar_union (S n) s (fsub n (Vapp vi vj)))
(fill (Cont f e (fresh (S n) i) Hole (fresh (S n+i) j)) l).

renamings

Section sub_inv.

Variables (s1 s2 : substitution)
(hyp : forall x, sub s1 (sub s2 (Var x)) = Var x).

Lemma sub_inv : forall t, sub s1 (sub s2 t) = t.

End sub_inv.

Section swap.

Definition swap x y := single x (Var y).

Lemma swap_intro s x y t : ~In y (vars t) ->
sub s t = sub (sub_comp s (swap y x)) (sub (swap x y) t).

Lemma swap_id x t : sub (swap x x) t = t.

End swap.

End S.

tactics

Ltac single := simpl; unfold single; rewrite <- beq_nat_refl; refl.

Ltac exists_single x t := exists (single x t); single.