# 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.