Library CoLoR.Term.Varyadic.VTrs

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
  • Frederic Blanqui, 2005-02-17
rewriting

Set Implicit Arguments.


definition

Section def.

  Variable Sig : Signature.

  Notation term := (term Sig).

  Record rule : Type := mkRule { lhs : term; rhs : term }.

  Definition rules := list rule.

  Definition red R t1 t2 := exists l, exists r, exists c, exists s,
    In (mkRule l r) R /\ t1 = fill c (sub s l) /\ t2 = fill c (sub s r).

  Definition hd_red R t1 t2 := exists l, exists r, exists s,
    In (mkRule l r) R /\ t1 = sub s l /\ t2 = sub s r.

  Definition int_red R t1 t2 := exists l, exists r, exists c, exists s,
    c <> Hole
    /\ In (mkRule l r) R /\ t1 = fill c (sub s l) /\ t2 = fill c (sub s r).

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

End def.

tactics

Ltac redtac := repeat
  match goal with
    | H : red ?R ?t ?u |- _ =>
      let l := fresh "l" in let r := fresh "r" in let c := fresh "c" in
      let s := fresh "s" in let h1 := fresh in
      (unfold red in H; destruct H as [l]; destruct H as [r]; destruct H as [c];
      destruct H as [s]; destruct H as [H h1]; destruct h1)
    | H : transp (red _) _ _ |- _ => unfold transp in H; redtac
    | H : hd_red ?R ?t ?u |- _ =>
      let l := fresh "l" in let r := fresh "r" in
      let s := fresh "s" in let h1 := fresh in
      (unfold hd_red in H; destruct H as [l]; destruct H as [r];
      destruct H as [s]; destruct H as [H h1]; destruct h1)
    | H : transp (hd_red _) _ _ |- _ => unfold transp in H; redtac
    | H : int_red ?R ?t ?u |- _ =>
      let l := fresh "l" in let r := fresh "r" in let c := fresh "c" in
      let s := fresh "s" in let h1 := fresh in let h2 := fresh in
      (unfold int_red in H; destruct H as [l]; destruct H as [r];
      destruct H as [c]; destruct H as [s]; destruct H as [H h1];
      destruct h1 as [h1 h2]; destruct h2)
    | H : transp (int_red _) _ _ |- _ =>
      unfold transp in H; redtac
  end.

properties

Section S.

  Variable Sig : Signature.

  Notation rule := (rule Sig).

  Variable R : list rule.

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

  Lemma red_rule_top : forall l r s,
    In (mkRule l r) R -> red R (sub s l) (sub s r).

  Lemma red_fill : forall c t u, red R t u -> red R (fill c t) (fill c u).

End S.