CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
• Sidi Ould-Biha & Frederic Blanqui, 2010-05-04
Dependency relation on defined symbols implied by rules:
f is bigger than g if g occurs in the RHS of a defining rule of f

Set Implicit Arguments.

Section S.

Variable Sig : Signature.

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

defined symbols occuring in a term

Definition def_symbs R (t : term) := filter (fun f => defined f R) (symbs t).

Lemma def_symbs_incl : forall R a t, def_symbs R t [= def_symbs (a :: R) t.

function testing if the root of a term is equal to some given symbol

Definition root_eq (f : Sig) (t : term) : bool :=
match t with | Fun g _ => beq_symb f g | _ => false end.

dependency relation on defined symbols implied by rules

Definition symb_ord R : relation Sig := fun f g =>
exists a, In a R /\ root_eq f (lhs a) = true /\ In g (def_symbs R (rhs a)).

Lemma symb_ord_cons : forall a R f g, symb_ord R f g -> symb_ord (a :: R) f g.

Lemma symb_ord_cons_var : forall R f g n r,
symb_ord (mkRule (Var n) r :: R) f g -> symb_ord R f g.

Fixpoint symb_ord_img_rec R Rc f : list Sig :=
match Rc with
| nil => nil
| a :: Rc' =>
if root_eq f (lhs a) && Inb (@eq_rule_dec Sig) a R then
def_symbs R (rhs a) ++ symb_ord_img_rec R Rc' f
else symb_ord_img_rec R Rc' f
end.

Lemma symb_ord_img_rec_cons1 : forall Rc a R f,
symb_ord_img_rec R Rc f [= symb_ord_img_rec (a :: R) Rc f.

Lemma symb_ord_img_rec_cons2 : forall Rc a R f,
symb_ord_img_rec R Rc f [= symb_ord_img_rec R (a :: Rc) f.

Lemma symb_ord_img_recP1 : forall Rc R f g,
In g (symb_ord_img_rec R Rc f) -> symb_ord R f g.

Lemma symb_ord_img_recP2 : forall Rc R f g a,
In g (def_symbs R (rhs a)) -> In a R -> In a Rc ->
root_eq f (lhs a) = true -> In g (symb_ord_img_rec R Rc f).

Lemma symb_ord_img_rec_incl : forall Rc1 Rc2 R f,
Rc1 [= Rc2 -> symb_ord_img_rec R Rc1 f [= symb_ord_img_rec R Rc2 f.

Lemma symb_ord_img_incl : forall Rc R f g,
R [= Rc -> symb_ord R f g -> In g (symb_ord_img_rec R Rc f).

Definition symb_ord_img R f := symb_ord_img_rec R R f.

Lemma symb_ord_imgP : forall R f g,
In g (symb_ord_img R f) <-> symb_ord R f g.

Lemma symb_ord_dec : forall R, rel_dec (symb_ord R).

LHS root symbols of a list of rules

Fixpoint root_lhs_rules (R : rules) : list Sig :=
match R with
| nil => nil
| a :: R' =>
match lhs a with
| Fun f _ => f :: root_lhs_rules R'
| _ => root_lhs_rules R'
end
end.

Lemma root_lhsP : forall R f,
In f (root_lhs_rules R) <-> exists a, In a R /\ root_eq f (lhs a) = true.

End S.