Library CoLoR.Term.WithArity.AReduct

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
  • Frederic Blanqui, 2009-05-06
list of reducts of a term and proof that rewriting is finitely branching

Set Implicit Arguments.


Section S.

  Variable Sig : Signature.

  Notation term := (term Sig). Notation terms := (vector term).
  Notation rule := (rule Sig). Notation rules := (list rule).

top reducts

  Definition top_reduct (t : term) lr :=
    match matches (lhs lr) t with
      | Some s => Some (sub s (rhs lr))
      | None => None
    end.

  Lemma top_reduct_correct : forall R lr t u,
    In lr R -> top_reduct t lr = Some u -> hd_red R t u.

  Definition top_reducts R t := filter_opt (top_reduct t) R.

  Lemma top_reducts_correct : forall t u R,
    In u (top_reducts R t) -> hd_red R t u.


  Lemma top_reducts_correct_red : forall t u R,
    In u (top_reducts R t) -> red R t u.

  Lemma top_reducts_complete : forall t u R,
    rules_preserve_vars R -> hd_red R t u -> In u (top_reducts R t).

list of reducts of a term

  Variable R : rules.

  Lemma reducts_aux1 : forall k n, S k <= n -> k <= n.

  Lemma reducts_aux2 : forall k n, S k <= n -> n - S k < n.

  Fixpoint reducts t :=
    match t with
      | Var _ => top_reducts R t
      | Fun f ts =>
        let fix reducts_vec k (us : terms k) : k <= arity f -> list term :=
          match us in vector _ k return k <= arity f -> list term with
            | Vnil => fun _ => nil
            | Vcons u1 us' => fun h =>
              map (fun x => Fun f (Vreplace ts (reducts_aux2 h) x)) (reducts u1)
              ++ reducts_vec _ us' (reducts_aux1 h)
          end
          in top_reducts R t ++ reducts_vec (arity f) ts (le_refl (arity f))
    end.

  Fixpoint reducts_vec f ts k (us : terms k) : k <= arity f -> list term :=
    match us in vector _ k return k <= arity f -> list term with
      | Vnil => fun _ => nil
      | Vcons u1 us' => fun h =>
        map (fun x => Fun f (Vreplace ts (reducts_aux2 h) x)) (reducts u1)
        ++ reducts_vec f ts us' (reducts_aux1 h)
    end.

  Lemma fix_reducts_vec : forall f ts k us h,
    (fix reducts_vec (k : nat) (us : terms k) : k <= arity f -> list term :=
      match us in (vector _ k0) return (k0 <= arity f -> list term) with
        | Vnil => fun _ => nil
        | Vcons u1 us' => fun h =>
          map (fun x => Fun f (Vreplace ts (reducts_aux2 h) x)) (reducts u1)
          ++ reducts_vec _ us' (reducts_aux1 h)
      end) k us h = reducts_vec f ts us h.

  Lemma reducts_fun : forall f ts, reducts (Fun f ts)
    = top_reducts R (Fun f ts) ++ reducts_vec f ts ts (le_refl (arity f)).

properties

  Lemma reducts_vec_pi : forall f ts k (us : terms k) h h',
    reducts_vec f ts us h = reducts_vec f ts us h'.

  Lemma reducts_vec_cast : forall f ts k (us : terms k) h k' (e : k = k') h',
    reducts_vec f ts (Vcast us e) h' = reducts_vec f ts us h.


  Lemma In_reducts_vec_elim_aux : forall v' f ts k (us : terms k),
    (forall i (p : i < k), exists r : arity f - k + i < arity f,
      Vnth us p = Vnth ts r) -> forall h, In v' (reducts_vec f ts us h) ->
    exists i, exists p : i < arity f, exists u',
      In u' (reducts (Vnth ts p)) /\ v' = Fun f (Vreplace ts p u').


  Lemma In_reducts_vec_elim : forall v' f ts,
    In v' (reducts_vec f ts ts (le_refl (arity f))) ->
    exists i, exists p : i < arity f, exists u',
      In u' (reducts (Vnth ts p)) /\ v' = Fun f (Vreplace ts p u').


  Lemma In_reducts_vec_intro_aux : forall f ts k (us : terms k)
    (h : k <= arity f) t i (p : i < k) (q : arity f - k + i < arity f),
    In t (reducts (Vnth us p)) ->
    In (Fun f (Vreplace ts q t)) (reducts_vec f ts us h).


  Lemma In_reducts_vec_intro : forall f ts t i (p : i < arity f),
    In t (reducts (Vnth ts p)) ->
    In (Fun f (Vreplace ts p t)) (reducts_vec f ts ts (le_refl (arity f))).

alternative definition (Pierre-Yves Strub)

  Fixpoint reducts2 t :=
    match t with
      | Var _ => top_reducts R t
      | Fun f ts =>
        let fix reducts2_vec k (us : terms k) : list (terms k) :=
          match us with
            | Vnil => nil
            | Vcons u1 us' => map (fun x => Vcons x us') (reducts2 u1)
              ++ map (fun x => Vcons u1 x) (reducts2_vec _ us')
          end
          in top_reducts R t ++ map (Fun f) (reducts2_vec (arity f) ts)
    end.

  Fixpoint reducts2_vec k (us : terms k) : list (terms k) :=
    match us with
      | Vnil => nil
      | Vcons u1 us' => map (fun x => Vcons x us') (reducts2 u1)
        ++ map (fun x => Vcons u1 x) (reducts2_vec us')
    end.

  Lemma reducts2_fun : forall f ts, reducts2 (Fun f ts)
    = top_reducts R (Fun f ts) ++ map (Fun f) (reducts2_vec ts).

  Lemma In_reducts2_vec_elim : forall n (vs ts : terms n),
    In vs (reducts2_vec ts) -> exists i, exists p : i < n, exists u,
      In u (reducts2 (Vnth ts p)) /\ vs = Vreplace ts p u.


  Lemma In_reducts2_vec_intro : forall n (ts : terms n) t i (p : i < n),
    In t (reducts2 (Vnth ts p)) -> In (Vreplace ts p t) (reducts2_vec ts).

correctness

  Lemma reducts_correct : forall t u, In u (reducts t) -> red R t u.

completeness

  Lemma reducts_complete : rules_preserve_vars R ->
    forall t u, red R t u -> In u (reducts t).

rewriting is finitely branching