Library CoLoR.Term.WithArity.ACompat

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
  • Frederic Blanqui, 2007-01-25
  • 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).
Notation rule := (rule Sig). Notation rules := (list rule).


Section compat.

Variable succ : relation term.

Definition compat R := forall l r : term, In (mkRule l r) R -> succ l r.

Lemma compat_empty : compat nil.

Lemma compat_red : forall R,
  rewrite_ordering succ -> compat R -> red R << succ.

Lemma compat_hd_red : forall R,
  substitution_closed succ -> compat R -> hd_red R << succ.

Lemma incl_compat : forall R S, incl R S -> compat S -> compat R.

Lemma compat_red_mod_tc : forall R E,
  rewrite_ordering succ -> compat E -> compat R -> red_mod E R << succ!.

Lemma compat_cons : forall l r R,
  succ l r -> compat R -> compat (mkRule l r :: R).

Lemma compat_cons_elim : forall l r R,
  compat (mkRule l r :: R) -> succ l r /\ compat R.

Lemma compat_app : forall R R',
  compat R -> compat R' -> compat (R ++ R').

Definition compat_rule a := match a with mkRule l r => succ l r end.

Lemma compat_lforall : forall R, lforall compat_rule R -> compat R.


Variable succ_dec : rel_dec succ.

Function is_compat (R : rules) : bool :=
  match R with
    | nil => true
    | cons a R' =>
      match a with mkRule l r =>
        match succ_dec l r with
          | left _ => is_compat R'
          | right _ => false

Lemma is_compat_correct : forall R,
  is_compat R = true -> compat R /\ is_compat R = false -> ~compat R.

Lemma is_compat_complete : forall R,
  compat R -> is_compat R = true /\ ~compat R -> is_compat R = false.

End compat.

Lemma compat_incl : forall succ succ' R,
  succ << succ' -> compat succ R -> compat succ' R.

reduction pair
weak reduction pair
partitioning rewrite rules according to some decidable relation

Lemma red_partition : forall (R R1 R2 : rules),
  (forall r, In r R -> In r R1 \/ In r R2) -> red R << red R1 U red R2.

Section rule_partition.

  Variable R : rules.

  Definition rule_partition succ (succ_dec : rel_dec succ) (r : rule) :=
    partition_by_rel succ_dec (lhs r, rhs r).

  Lemma rule_partition_left : forall succ (succ_dec : rel_dec succ) l r rs,
    In (mkRule l r) (fst (partition (rule_partition succ_dec) rs)) ->
    partition_by_rel succ_dec (l, r) = true.

  Lemma rule_partition_compat : forall succ (succ_dec : rel_dec succ),
    snd (partition (rule_partition succ_dec) R) = nil ->
    compat succ R.

  Lemma rule_partition_complete : forall pf (R : rules),
    let part := partition pf R in
      red R << red (fst part) U red (snd part).

  Lemma hd_rule_partition_complete : forall pf (R : rules),
    let part := partition pf R in
      hd_red R << hd_red (fst part) U hd_red (snd part).

End rule_partition.

End S.