Library CoLoR.Term.WithArity.ARules

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
  • Frederic Blanqui, 2009-06-24
infinite sets of rules

Set Implicit Arguments.


Section defs.

  Variable Sig : Signature.

  Notation term := (term Sig). Notation rule := (rule Sig).
  Notation rules := (set rule).

rewriting

  Definition red (R : rules) : relation term :=
    fun u v => exists l, exists r, exists c, exists s,
      R (mkRule l r) /\ u = fill c (sub s l) /\ v = fill c (sub s r).

  Definition hd_red (R : rules) : relation term :=
    fun u v => exists l, exists r, exists s,
      R (mkRule l r) /\ u = sub s l /\ v = sub s r.

  Definition red_mod E R := red E # @ red R.

  Definition hd_red_mod E R := red E # @ hd_red R.

End defs.

Ltac redtac := repeat
  match goal with
    | H : red _ _ _ |- _ =>
      let l := fresh "l" in let r := fresh "r" in
      let c := fresh "c" in let s := fresh "s" in
      let lr := fresh "lr" in let xl := fresh "xl" in
      let yr := fresh "yr" in
        destruct H as [l [r [c [s [lr [xl yr]]]]]]
| H : transp (red _) _ _ |- _ => unfold transp in H; redtac
    | H : hd_red _ _ _ |- _ =>
      let l := fresh "l" in let r := fresh "r" in
      let s := fresh "s" in let lr := fresh "lr" in
      let xl := fresh "xl" in let yr := fresh "yr" in
        destruct H as [l [r [s [lr [xl yr]]]]]
| H : transp (hd_red _) _ _ |- _ => unfold transp in H; redtac
    | H : red_mod _ _ _ _ |- _ =>
      let t := fresh "t" in let h := fresh in
        destruct H as [t h]; destruct h; redtac
    | H : hd_red_mod _ _ _ _ |- _ =>
      let t := fresh "t" in let h := fresh in
        destruct H as [t h]; destruct h; redtac
  end.

monotony properties
properties of rewriting

Section props.

  Variable Sig : Signature.

  Notation rule := (rule Sig). Notation rules := (set rule).

  Lemma red_rule (R : rules) l r c s :
    R (mkRule l r) -> red R (fill c (sub s l)) (fill c (sub s r)).

  Lemma hd_red_rule (R : rules) l r s :
    R (mkRule l r) -> hd_red R (sub s l) (sub s r).

  Lemma context_closed_red (R : rules) : context_closed (red R).

  Lemma red_Rules (R : list rule) : red (of_list R) == ATrs.red R.

  Lemma hd_red_Rules (R : list rule) : hd_red (of_list R) == ATrs.hd_red R.

  Lemma rt_red_empty : red (@empty rule) # == eq.

properties of rewriting modulo

  Lemma context_closed_red_mod (E R : rules) : context_closed (red_mod E R).

  Lemma red_mod_union (E R : rules) : red_mod E R << red (union E R) #.

  Lemma rt_red_mod_union (E R : rules) : red_mod E R # << red (union E R) #.

  Lemma red_mod_Rules (E R : list rule) :
    red_mod (of_list E) (of_list R) == ATrs.red_mod E R.

  Lemma hd_red_mod_Rules (E R : list rule) :
    hd_red_mod (of_list E) (of_list R) == ATrs.hd_red_mod E R.

  Lemma red_mod_empty (R : rules) : red_mod empty R == red R.

End props.