# 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