Library CoLoR.Term.WithArity.ARelation

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
  • Sebastien Hinderer, 2004-02-09
general definitions and results about relations on terms

Set Implicit Arguments.


Section S.

  Variable Sig : Signature.

  Notation term := (term Sig).

basic definitions

  Section basic.

    Variable R : relation term.

    Definition preserve_vars := forall t u, R t u -> incl (vars u) (vars t).

    Definition substitution_closed :=
      forall t1 t2 s, R t1 t2 -> R (sub s t1) (sub s t2).

    Definition context_closed :=
      forall t1 t2 c, R t1 t2 -> R (fill c t1) (fill c t2).

    Definition rewrite_ordering := substitution_closed /\ context_closed.

    Definition reduction_ordering := WF R /\ rewrite_ordering.

  End basic.

  Record Rewrite_ordering : Type := mkRewrite_ordering {
    rew_ord_rel :> relation term;
    rew_ord_subs : substitution_closed rew_ord_rel;
    rew_ord_cont : context_closed rew_ord_rel
  }.

closure by substitution
closure by context

  Lemma context_closed_rtc : forall R, context_closed R -> context_closed (R #).

  Lemma context_closed_tc : forall R, context_closed R -> context_closed (R !).

  Lemma context_closed_comp : forall R S,
    context_closed R -> context_closed S -> context_closed (R @ S).

  Lemma context_closed_fun : forall R, context_closed R ->
    forall f i v1 t u j v2 (e : i+S j=arity f),
      R t u -> R (Fun f (Vcast (Vapp v1 (Vcons t v2)) e))
                 (Fun f (Vcast (Vapp v1 (Vcons u v2)) e)).

  Lemma Vmonotone_context_closed : forall R,
    (forall f : Sig, Vmonotone (Fun f) R R) <-> context_closed R.

reduction pair
weak reduction pair

  Section weak_reduction_pair.

    Variables R E : relation term.

    Definition weak_context_closed :=
      forall t1 t2 c, R t1 t2 -> E (fill c t1) (fill c t2).

    Definition weak_rewrite_ordering :=
      substitution_closed R /\ weak_context_closed.

    Definition weak_reduction_ordering := WF R /\ weak_rewrite_ordering.

    Definition weak_reduction_pair :=
      weak_reduction_ordering /\ absorbs_left R E /\ rewrite_ordering E.

  End weak_reduction_pair.

  Record Weak_reduction_pair : Type := mkWeak_reduction_pair {
    wp_succ : relation term;
    wp_succ_eq : relation term;
    wp_subs : substitution_closed wp_succ;
    wp_subs_eq : substitution_closed wp_succ_eq;
    wp_cont_eq : context_closed wp_succ_eq;
    wp_absorb : absorbs_left wp_succ wp_succ_eq;
    wp_succ_wf : WF wp_succ
  }.

reflexive closure

  Section clos_refl.

    Variable R : relation term.

    Notation E := (R %).

    Lemma rc_context_closed :
      weak_context_closed R E -> context_closed E.

    Lemma rc_substitution_closed :
      substitution_closed R -> substitution_closed E.

    Lemma rc_rewrite_ordering :
      weak_rewrite_ordering R E -> rewrite_ordering E.

  End clos_refl.

when R is the strict part of E

  Section strict.

    Variables (E : relation term) (E_trans : transitive E).

    Notation R := (strict_part E).

    Lemma absorb_strict : absorbs_left R E.

  End strict.

subterm relation