Library CoLoR.Term.WithArity.AShift

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
  • Frederic Blanqui, 2007-01-22
term variables shifting

Set Implicit Arguments.

Section S.

  Variable Sig : Signature.

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

  Notation rule := (rule Sig). Notation rules := (list rule).
  Notation lhs := (@lhs Sig).

shift variable indices in terms

  Section shift.

    Variable p : nat.

    Definition shift_var x := x+p.

    Definition shift_sub x := @Var Sig (x+p).
    Definition shift := sub shift_sub.

    Definition shift_rule (rho : rule) :=
      let (l,r) := rho in mkRule (shift l) (shift r).

properties of shifting

    Lemma in_vars_shift_min x t : In x (vars (shift t)) -> p <= x.

    Lemma in_vars_shift_max x t : In x (vars (shift t)) -> x <= maxvar t + p.

    Lemma vars_shift : forall t, vars (shift t) = map shift_var (vars t).

    Lemma notin_vars_shift x l :
      ~In x (vars (shift l)) -> p <= x -> ~In (x-p) (vars l).

inverse shifting wrt a term

    Section inverse.

      Variable l : term.

      Definition shift_inv_var x :=
        match le_lt_dec p x with
        | left _ =>
          if Inb eq_nat_dec (x-p) (vars l) then x-p else x
        | right _ => x

      Definition shift_inv_sub x := @Var Sig (shift_inv_var x).
      Definition shift_inv := sub shift_inv_sub.

      Lemma sub_shift s : sub s l = sub (sub_comp s shift_inv_sub) (shift l).

      Lemma sub_shift_incl s r : vars r [= vars l ->
        sub s r = sub (sub_comp s shift_inv_sub) (shift r).

    End inverse.

  End shift.

declaration of implicit arguments

red included in shifted red

  Section red_incl_shift_red.

    Variables (R R' : rules) (hyp0 : rules_preserve_vars R)
              (hyp : forall a, In a R -> exists p, In (shift_rule p a) R').

    Lemma red_incl_shift_red : red R << red R'.

  End red_incl_shift_red.

shifted red included in red

  Section shift_red_incl_red.

    Variables (R R' : rules)
      (hyp : forall a', In a' R' -> exists p a, In a R /\ a' = shift_rule p a).

    Lemma shift_red_incl_red : red R' << red R.

  End shift_red_incl_red.

terms with disjoint vars

  Definition disjoint_vars t u :=
    forall x, In x (vars t) -> In x (vars u) -> t = u.

  Lemma disjoint_vars_refl t : disjoint_vars t t.

  Lemma disjoint_vars_com t u : disjoint_vars t u -> disjoint_vars u t.

  Definition pw_disjoint_vars l :=
    forall t u, In t l -> In u l -> disjoint_vars t u.

  Lemma pw_disjoint_vars_cons : forall t l, pw_disjoint_vars l ->
    (forall u, In u l -> disjoint_vars t u) -> pw_disjoint_vars (t :: l).

shift terms

  Fixpoint shift_terms (p : nat) (l : list term) : list term :=
    match l with
    | nil => nil
    | cons t l' => shift p t :: shift_terms (maxvar t + p + 1) l'

  Lemma in_vars_shift_terms : forall t l p, In t (shift_terms p l) ->
    exists u, exists q, In u l /\ t = shift q u /\ p <= q.

  Lemma in_vars_shift_terms_min : forall p t l x,
      In t (shift_terms p l) -> In x (vars t) -> p <= x.

  Lemma shift_terms_correct : forall l p, pw_disjoint_vars (shift_terms p l).

shift rules

  Fixpoint shift_rules (p : nat) (R : rules) : rules :=
    match R with
    | nil => nil
    | cons a R' => shift_rule p a :: shift_rules (maxvar(lhs a)+p+1) R'

  Lemma shift_rules_lhs : forall R p,
      map lhs (shift_rules p R) = shift_terms p (map lhs R).

End S.