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

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.


  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'

    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

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

  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

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

  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'

  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

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


  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.


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

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