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.