Library CoLoR.Term.WithArity.ADepRel

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.