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

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

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

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

End S.