Library CoLoR.Term.WithArity.APosition

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
• Frederic Blanqui & Wang Qian & Zhang Lianyi, 2009-05-06
positions in a term and related functions and relations: subterm at some position, replacement of a subterm at some position, context corresponding to a position, position of the Hole of a context, definition of rewriting based on positions

Set Implicit Arguments.

positions are lists of natural numbers

Notation position := (list nat).

Section S.

Variable Sig : Signature.

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

context corresponding to a position

Fixpoint context_pos (t : term) (ps : position) : option context :=
match t, ps with
| _, nil => Some Hole
| Var x, _ :: _ => None
| Fun f ts, p :: ps =>
match lt_ge_dec p (arity f) with
| left h =>
match context_pos (Vnth ts h) ps with
| None => None
| Some x =>
Some (Cont f (Veq_app_cons_aux3 h)
(Vsub ts (Veq_app_cons_aux1 h))
x (Vsub ts (Veq_app_cons_aux2 h)))
end
| right _ => None
end
end.

subterm at some position

Fixpoint subterm_pos (t : term) (ps : position) {struct ps} : option term :=
match t, ps with
| _ , nil => Some t
| Var x , _ :: _ => None
| Fun f ts, p :: ps' =>
match lt_ge_dec p (arity f) with
| left h => subterm_pos (Vnth ts h) ps'
| right _ => None
end
end.

Lemma subterm_pos_elim : forall p t u, subterm_pos t p = Some u ->
{C | context_pos t p = Some C /\ t = fill C u}.

Lemma subterm_pos_sub : forall s u p t,
subterm_pos t p = Some u -> subterm_pos (sub s t) p = Some (sub s u).

replace subterm at some position

Fixpoint replace_pos (t : term) (ps : position) (u : term)
: option term :=
match t, ps with
| _, nil => Some u
| Var x, _ :: _ => None
| Fun f ts, p :: ps' =>
match lt_ge_dec p (arity f) with
| left h =>
match replace_pos (Vnth ts h) ps' u with
| None => None
| Some v => Some (Fun f (Vreplace ts h v))
end
| right _ => None
end
end.

Lemma subterm_pos_replace_eq_Some : forall p u v t,
subterm_pos t p = Some u -> {w | replace_pos t p v = Some w}.

Lemma subterm_pos_replace_neq_None : forall p u v t,
subterm_pos t p = Some u -> replace_pos t p v <> None.

Lemma replace_pos_elim : forall p t u t', replace_pos t p u = Some t' ->
{C | context_pos t p = Some C /\ t' = fill C u}.

position of the Hole in a context

Fixpoint pos_context (C : context) : position :=
match C with
| Hole => nil
| @Cont _ _ i _ _ _ C _ => i :: pos_context C
end.

Lemma subterm_fill_pos_context : forall c u,
subterm_pos (fill c u) (pos_context c) = Some u.

Lemma replace_fill_pos_context : forall c u v,
replace_pos (fill c u) (pos_context c) v = Some (fill c v).

definition of rewriting based on positions

Definition red_pos R u v := exists p, exists l, exists r, exists s,
In (mkRule l r) R
/\ subterm_pos u p = Some (sub s l)
/\ replace_pos u p (sub s r) = Some v.

Lemma red_pos_ok : forall R t u, red R t u <-> red_pos R t u.

position of a variables

Lemma in_vars_subterm : forall x t, In x (vars t) ->
exists ps, subterm_pos t ps = Some (Var x).

End S.