Library CoLoR.Term.WithArity.ATrs

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
  • Frederic Blanqui, 2005-02-17
  • Adam Koprowski and Hans Zantema, 2007-03-20
rewriting

Set Implicit Arguments.


Section basic_definitions.

  Variable Sig : Signature.

  Notation term := (term Sig). Notation terms := (vector term).

rules

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

  Lemma rule_eq : forall a b : rule, (lhs a = lhs b /\ rhs a = rhs b) <-> a = b.

  Definition beq_rule (a b : rule) : bool :=
    beq_term (lhs a) (lhs b) && beq_term (rhs a) (rhs b).

  Lemma beq_rule_ok : forall a b, beq_rule a b = true <-> a = b.

  Definition eq_rule_dec := dec_beq beq_rule_ok.

  Definition rules := list rule.

  Definition brule (f : term -> term -> bool) a := f (lhs a) (rhs a).

basic definitions and properties on rules

  Definition is_notvar_lhs a :=
    match lhs a with
      | Var _ => false
      | _ => true
    end.

  Lemma is_notvar_lhs_elim : forall R, forallb is_notvar_lhs R = true ->
    forall l r, In (mkRule l r) R -> exists f ts, l = Fun f ts.

  Lemma is_notvar_lhs_false : forall R, forallb is_notvar_lhs R = true ->
    forall x r, In (mkRule (Var x) r) R -> False.

  Definition is_notvar_rhs a :=
    match rhs a with
      | Var _ => false
      | _ => true
    end.

  Lemma is_notvar_rhs_elim : forall R, forallb is_notvar_rhs R = true ->
    forall l r, In (mkRule l r) R -> exists f ts, r = Fun f ts.

  Lemma is_notvar_rhs_false : forall R, forallb is_notvar_rhs R = true ->
    forall x l, In (mkRule l (Var x)) R -> False.

standard rewriting

  Section rewriting.

    Variable R : rules.

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

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

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

    Definition NF u := forall v, ~red u v.

innermost rewriting

    Definition innermost u := forall f us, u = Fun f us -> Vforall NF us.

    Definition inner_red u v := exists l r c s,
      In (mkRule l r) R /\ u = fill c (sub s l) /\ v = fill c (sub s r)
      /\ innermost (sub s l).

    Definition inner_hd_red u v := exists l r s,
      In (mkRule l r) R /\ u = sub s l /\ v = sub s r /\ innermost u.

    Definition inner_int_red u v := exists l r c s, c <> Hole
      /\ In (mkRule l r) R /\ u = fill c (sub s l) /\ v = fill c (sub s r)
      /\ innermost (sub s l).

  End rewriting.

rewrite modulo steps

  Section rewriting_modulo.

    Variables (S : relation term) (E R : rules).

    Definition red_mod := red E # @ red R.

    Definition hd_red_Mod := S @ hd_red R.

    Definition hd_red_mod := red E # @ hd_red R.

  End rewriting_modulo.

End basic_definitions.


basic tactic for eliminating rewriting hypotheses

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 : int_red _ _ _ |- _ =>
      let l := fresh "l" in let r := fresh "r" in
      let c := fresh "c" in let cne := fresh "cne" 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 [cne [lr [xl yr]]]]]]]
| H : transp (int_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
    | H : hd_red_Mod _ _ _ _ |- _ =>
      let t := fresh "t" in let h := fresh in
        destruct H as [t h]; destruct h; redtac
  end.

monotony properties
basic properties

Section S.

  Variable Sig : Signature.

  Notation term := (term Sig). Notation terms := (vector term).
  Notation rule := (rule Sig). Notation rules := (list rule).

  Section rewriting.

    Variable R R' : rules.

    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_empty : forall t u : term, red nil # t u -> t = u.

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

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

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

    Lemma context_closed_red : context_closed (red R).

    Lemma red_sub : forall t u s, red R t u -> red R (sub s t) (sub s u).

    Lemma red_subterm : forall u u' t, red R u u' -> subterm_eq u t
      -> exists t', red R t t' /\ subterm_eq u' t'.

    Lemma int_red_fun : forall f ts v, int_red R (Fun f ts) v
      -> exists i (vi : terms i) t j (vj : terms j) h t',
        ts = Vcast (Vapp vi (Vcons t vj)) h
        /\ v = Fun f (Vcast (Vapp vi (Vcons t' vj)) h) /\ red R t t'.

    Lemma red_swap : red (R ++ R') << red (R' ++ R).

    Lemma hd_red_swap : hd_red (R ++ R') << hd_red (R' ++ R).

    Lemma int_red_incl_red : int_red R << red R.

    Lemma hd_red_incl_red : hd_red R << red R.

    Lemma WF_red_empty : WF (red (@nil rule)).

    Lemma hd_red_mod_incl_red_mod : forall E, hd_red_mod E R << red_mod E R.

    Lemma int_red_preserve_hd : forall u v, int_red R u v ->
      exists f us vs, u = Fun f us /\ v = Fun f vs.

    Lemma int_red_rtc_preserve_hd : forall u v, int_red R # u v ->
      u=v \/ exists f us vs, u = Fun f us /\ v = Fun f vs.

    Lemma red_case : forall t u, red R t u -> hd_red R t u
      \/ exists f ts i (p : i < arity f) u',
        t = Fun f ts /\ red R (Vnth ts p) u' /\ u = Fun f (Vreplace ts p u').

    Lemma red_split : forall t u, red R t u -> hd_red R t u \/ int_red R t u.

  End rewriting.

preservation of variables under reduction


  Definition rules_preserve_vars (R : rules) :=
    forall l r, In (mkRule l r) R -> vars r [= vars l.

  Definition brules_preserve_vars (R : rules) :=
    forallb (fun x => incl beq_nat (vars (rhs x)) (vars (lhs x))) R.

  Lemma brules_preserve_vars_ok :
    forall R, brules_preserve_vars R = true <-> rules_preserve_vars R.

  Lemma rules_preserve_vars_cons : forall a R, rules_preserve_vars (a :: R)
    <-> vars (rhs a) [= vars (lhs a) /\ rules_preserve_vars R.

  Section vars.

    Variables (R : rules) (hyp : rules_preserve_vars R).

    Lemma red_preserve_vars : preserve_vars (red R).

    Lemma tred_preserve_vars : preserve_vars (red R !).

    Lemma rtred_preserve_vars : preserve_vars (red R #).


    Lemma red_maxvar : forall t u, red R t u -> maxvar u <= maxvar t.

    Lemma red_maxvar0 : forall t u, maxvar t = 0 -> red R t u -> maxvar u = 0.

    Lemma rtc_red_maxvar : forall t u, red R # t u -> maxvar u <= maxvar t.

    Lemma rtc_red_maxvar0 : forall t u,
      maxvar t = 0 -> red R # t u -> maxvar u = 0.

  End vars.

  Section red_mod.

    Variables (E R : rules)
      (hE : rules_preserve_vars E) (hR : rules_preserve_vars R).

    Lemma red_mod_maxvar : forall t u, red_mod E R t u -> maxvar u <= maxvar t.

    Lemma red_mod_maxvar0 : forall t u,
      maxvar t = 0 -> red_mod E R t u -> maxvar u = 0.

  End red_mod.

  Lemma rules_preserve_vars_incl : forall R S : rules,
    R [= S -> rules_preserve_vars S -> rules_preserve_vars R.

biggest variable in a list of rules


  Definition maxvar_rule (a : rule) :=
    let (l,r) := a in max (maxvar l) (maxvar r).

  Definition fold_max m a := max m (maxvar_rule a).

  Definition maxvar_rules R := fold_left fold_max R 0.

  Lemma maxvar_rules_init : forall R x, fold_left fold_max R x >= x.

  Lemma maxvar_rules_init_mon : forall R x y,
    x >= y -> fold_left fold_max R x >= fold_left fold_max R y.

  Notation rule_dec := (dec_beq (@beq_rule_ok Sig)).
  Notation remove := (remove rule_dec).

  Lemma maxvar_rules_remove : forall a R x y,
    x >= y -> fold_left fold_max R x >= fold_left fold_max (remove a R) y.

  Lemma maxvar_rules_elim : forall a R n,
    In a R -> n > maxvar_rules R -> n > maxvar_rule a.

rewriting vectors of terms

  Section vector.


    Variable R : rules.

    Lemma Vgt_prod_fun : forall f ts ts',
      Vrel1 (red R) ts ts' -> int_red R (Fun f ts) (Fun f ts').

  End vector.

union of rewrite rules

  Section union.

    Variables R R' : rules.

    Lemma red_union : red (R ++ R') << red R U red R'.

    Lemma red_union_inv : red R U red R' << red (R ++ R').

    Lemma hd_red_union : hd_red (R ++ R') << hd_red R U hd_red R'.

    Lemma hd_red_union_inv : hd_red R U hd_red R' << hd_red (R ++ R').

  End union.

properties of rewriting modulo

  Section rewriting_modulo_results.

    Variables (S S' : relation term) (E E' R R' : rules).

    Lemma hd_red_mod_of_hd_red_Mod_int :
      hd_red_Mod (int_red E #) R << hd_red_mod E R.

    Lemma hd_red_mod_of_hd_red_Mod : hd_red_Mod (red E #) R << hd_red_mod E R.

    Lemma hd_red_Mod_remdup :
      hd_red_Mod S R << hd_red_Mod S (remdup (@eq_rule_dec Sig) R).

    Lemma hd_red_mod_remdup :
      hd_red_mod E R << hd_red_mod E (remdup (@eq_rule_dec Sig) R).

    Lemma red_mod_empty_incl_red : red_mod nil R << red R.

    Lemma red_mod_empty : red_mod nil R == red R.

    Lemma hd_red_mod_empty_incl_hd_red : hd_red_mod nil R << hd_red R.

    Lemma WF_red_mod_empty : WF (red_mod E nil).

    Lemma WF_hd_red_mod_empty : WF (hd_red_mod E nil).

    Lemma WF_hd_red_Mod_empty : WF (hd_red_Mod S nil).

    Lemma red_mod_fill : forall t u c,
      red_mod E R t u -> red_mod E R (fill c t) (fill c u).

    Lemma context_closed_red_mod : context_closed (red_mod E R).

    Lemma red_mod_sub : forall t u s,
      red_mod E R t u -> red_mod E R (sub s t) (sub s u).

  End rewriting_modulo_results.

termination as special case of relative termination

  Section termination_as_relative_term.

    Variable R R' : rules.

    Lemma red_incl_red_mod : red R << red_mod nil R.

    Lemma hd_red_incl_hd_red_mod : hd_red R << hd_red_mod nil R.

  End termination_as_relative_term.

union of rewrite rules modulo

  Section union_modulo.

    Variables (S : relation term) (E R R' : rules).

    Lemma red_mod_union : red_mod E (R ++ R') << red_mod E R U red_mod E R'.

    Lemma hd_red_Mod_union :
      hd_red_Mod S (R ++ R') << hd_red_Mod S R U hd_red_Mod S R'.

    Lemma hd_red_mod_union :
      hd_red_mod E (R ++ R') << hd_red_mod E R U hd_red_mod E R'.

  End union_modulo.

rewriting is invariant under rule renamings

  Definition sub_rule s (a : rule) := mkRule (sub s (lhs a)) (sub s (rhs a)).

  Definition sub_rules s := map (sub_rule s).

  Section rule_renaming.

    Variable s1 s2 : @substitution Sig.
    Variable hyp : forall x, sub s1 (sub s2 (Var x)) = Var x.

    Lemma sub_rule_inv : forall x, sub_rule s1 (sub_rule s2 x) = x.

    Lemma sub_rules_inv : forall x, sub_rules s1 (sub_rules s2 x) = x.

    Lemma red_ren : forall R, red R << red (map (sub_rule s2) R).

  End rule_renaming.

internal reduction in some specific subterm

  Definition int_red_pos_at (R : rules) i t u :=
    exists f (h : i < arity f) ts, t = Fun f ts
      /\ exists v, red R (Vnth ts h) v /\ u = Fun f (Vreplace ts h v).

  Definition int_red_pos R t u := exists i, int_red_pos_at R i t u.

  Lemma int_red_pos_eq : forall R, int_red_pos R == int_red R.

minimal (wrt subterm ordering) non-terminating terms

  Definition min R t := forall u : term, subterm u t -> ~NT R u.

  Definition NT_min R t := NT R t /\ min R t.

  Lemma min_eq : forall R t, min (red R) t <->
    (forall f ts, t = Fun f ts -> Vforall (fun u => ~NT (red R) u) ts).

  Lemma int_red_min : forall R t u,
    int_red R t u -> min (red R) t -> min (red R) u.

  Lemma int_red_rtc_min : forall R t u,
    int_red R # t u -> min (red R) t -> min (red R) u.

minimal infinite rewrite sequences modulo: two functions f and g describing an infinite sequence of head D-steps modulo arbitrary internal R-steps is minimal if:
  • every rule of D is applied infinitely often
  • the strict subterms of this rewrite sequence terminate wrt R

  Definition Min R (f : nat -> term) :=
    forall i x, subterm x (f i) -> forall g, g 0 = x -> ~IS R g.

  Definition InfRuleApp (D : rules) f g :=
    forall d, In d D -> exists h : nat -> nat,
      forall j, h j < h (S j) /\ hd_red (d :: nil) (g (h j)) (f (S (h j))).

  Definition ISModMin (R D : rules) f g :=
    ISMod (int_red R #) (hd_red D) f g
    /\ InfRuleApp D f g /\ Min (red R) f /\ Min (red R) g.

End S.


tactics

Ltac is_var_lhs := cut False;
  [tauto | eapply is_notvar_lhs_false; ehyp].

Ltac is_var_rhs := cut False;
  [tauto | eapply is_notvar_rhs_false; ehyp].

Ltac incl_rule Sig := incl (@beq_rule_ok Sig).

Ltac set_Sig_to x :=
  match goal with
  | |- WF (@hd_red_Mod ?S _ _) => set (x := S)
  | |- WF (@hd_red_mod ?S _ _) => set (x := S)
  end.

Ltac set_rules_to x :=
  match goal with
  | |- WF (hd_red_Mod _ ?R) => set (x := R)
  | |- WF (hd_red_mod _ ?R) => set (x := R)
  | |- WF (red_mod _ ?R) => set (x := R)
  | |- WF (red ?R) => set (x := R)
  end.

Ltac set_mod_rules_to x :=
  match goal with
  | |- WF (hd_red_mod ?E _) => set (x := E)
  end.

Ltac set_Mod_to x :=
  match goal with
  | |- WF (hd_red_Mod ?S _) => set (x := S)
  | |- WF (hd_red_mod ?E _) => set (x := red E #)
  end.

Ltac hd_red_mod :=
  match goal with
  | |- WF (hd_red_Mod _ _) =>
    eapply WF_incl;
    [(apply hd_red_mod_of_hd_red_Mod || apply hd_red_mod_of_hd_red_Mod_int)
      | idtac]
  | |- WF (hd_red_mod _ _) => idtac
  end.

Ltac termination_trivial :=
  let R := fresh in set_rules_to R; norm R;
  (apply WF_hd_red_mod_empty || apply WF_red_mod_empty || apply WF_red_empty).

Ltac remove_relative_rules E := norm E; rewrite red_mod_empty
  || fail "this certificate cannot be applied on a relative system".

Ltac no_relative_rules :=
  match goal with
    | |- WF (red_mod ?E _) => remove_relative_rules E
    | |- EIS (red_mod ?E _) => remove_relative_rules E
    | |- _ => idtac
  end.

Ltac norm_rules := match goal with |- forallb _ ?R = _ => norm R end.

Ltac get_rule :=
  match goal with |- forallb ?f ?l = _ =>
    match l with context C [ @mkRule ?S ?l ?r] =>
      let x := fresh "r" in set (x := @mkRule S l r);
        let y := fresh "b" in set (y := f x); norm_in y (f x) end end.

Ltac init := set(r:=0); set(r0:=0); set(b:=0); set(b0:=0).

Ltac get_rules := norm_rules; repeat get_rule.