Library Combi.Basic.congr: Rewriting rule and congruencies of words

Equivalence and congruence closure of a rewriting rule on words

If what follows a relation on T is a term of type rel T and a rewriting rule on T is a term of type T -> seq T.
Recall that a word congruence is an equivalence relation compatible with the concatenation product. This is the following definitions
  • congruence_rel r == the relation r on seq T is a congruence
  • congruence_rule == the rule rule on seq T is a congruence rule
Given a rewriting rule, the goal of this file is to compute its word congruence closure as well as its congruence classes. We therefore suppose that equivalence classes are finite. This also ensure that the generated equivalence relation is decidable by bounding the length of the rewriting paths. Concretely, this is done by requiring that rule is included in a reflexive relation invar which is invariant by rewriting rule, that is:
Hypothesis Hinvar : forall x0 x, invar x0 x -> all (invar x0) (rule x).
We show that this is true for homogeneous rules (ie: that preserve size) for words over a finite alphabet as well as multi-homogeneous rules (ie: that permutes words). Precisely, under the hypothesis
Hypothesis Hsym : forall x y, x \in rule y -> y \in rule x.
1- for homogeneous rules (ie: that preserve size) for words over a finite alphabet:
Hypothesis Hhom : forall u : word, all (szinvar u) (rule u).
We define
  • gencongr_hom == the word congrugence generated by a rule
  • genclass_hom == the class for gencongr_multhom
2- for multi-homogeneous rules (ie: that permutes words):
Hypothesis Hmulthom : forall u : word, all (perm_eq u) (rule u).
We define
  • gencongr_multhom == the word congrugence generated by a rule
  • genclass_multhom == the class for gencongr_multhom
Assuming the two latter hypothesis, we define a relation gencongr which is the congruence transitive closure of rule. The main results here are
  • gencongrP : gencongr is the smallest transitive congruence relation contaning rule.
  • gencongr_unique : gencongr is uniquely characterized by the property above
  • gencongr_ind : induction principle on classes for gencongr, any property preserved along the rewriting rule holds for classes.
From HB Require Import structures.
From mathcomp Require Import all_ssreflect.
Require Import Recdef.
Require Import permcomp permuted multinomial vectNK.

Set Implicit Arguments.

Transitive closure of a rule with finite classes

Since we only need to contruct it and not to compute with it, we use a simple but extremely inefficient algorithm
Section Transitive.

Variable T : eqType.
Variable rule : T -> seq T.
Variable invar : pred T.
Hypothesis Hinvar : forall x, invar x -> all invar (rule x).

Section FullKnown.

Variable full : seq T.
Hypothesis Hfull : forall x, invar x -> x \in full.

Theorem full_bound :
  forall s : seq T, all invar s -> uniq s -> size s <= size full.

End FullKnown.

Variable bound : nat.
Hypothesis Hbound: forall s : seq T, all invar s -> uniq s -> size s <= bound.

Lemma invar_undupE s : all invar (undup s) = all invar s.

Definition step s := undup (s ++ flatten (map rule s)).

Lemma step_mem s x y : y \in rule x -> x \in s -> y \in step s.

Lemma uniq_step s : uniq (step s).

Lemma undup_step s : undup (step s) = step s.

Lemma invar_step s : all invar s -> all invar (step s).

Lemma subset_step s : {subset s <= step s}.

Lemma subset_undup_step s : {subset undup s <= step s}.

This is a very unefficient transitive closure algorithm
Function trans
         (s : seq T) {measure (fun s => bound - size (undup s))} : seq T :=
  let us := undup s in
  if all invar us then
    let news := step s in
    if size news > size us then trans news
    else us
  else us.

Lemma subset_s_trans_s s : {subset s <= trans s}.

Variant rewrite_path x y : Prop :=
  Rew : forall l, path (fun t => [mem (rule t)]) x l ->
                  y = last x l -> rewrite_path x y.

Arguments Rew {x y} (l).

Lemma invar_rewrite_path x y : invar x -> rewrite_path x y -> invar y.

Lemma step_closed x s y :
  undup s =i step s -> x \in s -> rewrite_path x y -> y \in s.

Lemma transP y l :
  all invar l ->
  reflect (exists x, x \in l /\ rewrite_path x y) (y \in trans l).

Lemma rewrite_path_trans x y z :
  rewrite_path x y -> rewrite_path y z -> rewrite_path x z.

Lemma rewrite_path_sym x y :
  (forall x y, x \in rule y -> y \in rule x) ->
  rewrite_path x y -> rewrite_path y x.

End Transitive.

Dealing with the dependance of invar on x

Section Depend.

Variable T : eqType.
Variable rule : T -> seq T.

Record invariant_context :=
  InvariantContext {
      invar : T -> pred T;
      Hinvar_refl : forall x, invar x x;
      Hinvar_all : forall x0 x, invar x0 x -> all (invar x0) (rule x);
      bound : T -> nat;
      Hbound: forall x s, all (invar x) s -> uniq s -> size s <= bound x
    }.
Variable inv : invariant_context.
Hypothesis Hsym : forall x y, x \in rule y -> y \in rule x.

Definition rclass x := trans (@Hinvar_all inv x) (@Hbound inv x) [:: x].
Definition rtrans : rel T := fun x y => y \in rclass x.

Lemma rtransP x y : reflect (rewrite_path rule y x) (rtrans y x).

Theorem equiv_rtrans : equivalence_rel rtrans.

Lemma rtrans_ind (P : T -> Prop) x :
  P x -> (forall y z, P y -> z \in rule y -> P z) ->
  forall t, rtrans x t -> P t.

Lemma rule_rtrans x y : y \in rule x -> rtrans x y.

Lemma rewrite_path_min (r : rel T) :
  equivalence_rel r -> (forall x y, y \in rule x -> r x y) ->
  forall x y, rewrite_path rule x y -> r x y.

Lemma rtrans_min (r : rel T) :
  equivalence_rel r -> (forall x y, y \in rule x -> r x y) ->
  forall x y, rtrans x y -> r x y.

End Depend.

Definition congruence_rel (T : eqType) (r : rel (seq T)) :=
  forall a b1 c b2, r b1 b2 -> r (a ++ b1 ++ c) (a ++ b2 ++ c).

Definition congruence_rule (T : eqType) (rule : seq T -> seq (seq T)) :=
  congruence_rel (fun a b => a \in rule b).

Basic facts on congruences:

equivalence of various definitions and immediate consequences
Section CongruenceFacts.

Variable Alph : eqType.
Notation word := (seq Alph).

Variable r : rel word.
Hypothesis Hcongr : congruence_rel r.
Hypothesis Hequiv : equivalence_rel r.

Lemma congr_cons w1 w2 a : r w1 w2 -> r (a :: w1) (a :: w2).

Lemma congr_rcons w1 w2 a : r w1 w2 -> r (rcons w1 a) (rcons w2 a).

Lemma congr_catl u1 u2 v : r u1 u2 -> r (u1 ++ v) (u2 ++ v).

Lemma congr_catr u v1 v2 : r v1 v2 -> r (u ++ v1) (u ++ v2).

Lemma congr_cat u1 u2 v1 v2 : r u1 u2 -> r v1 v2 -> r (u1 ++ v1) (u2 ++ v2).

End CongruenceFacts.

Congruence closure of a bounded rule

Section CongruenceClosure.

Variable Alph : eqType.
Notation word := (seq Alph).
Implicit Types (a b c u v w : word).

Variable rule : word -> seq word.

Hypothesis Hsym : forall u v : word, v \in rule u -> u \in rule v.
Variable inv : invariant_context rule.

Definition congrrule s :=
  flatten [seq
             [seq (triple.1.1) ++ b1 ++ (triple.2) | b1 <- rule triple.1.2]
          | triple <- cut3 s ].

Lemma congrruleP u1 u2 :
  reflect (exists a v1 b v2,
              [/\ u1 = a ++ v1 ++ b, u2 = a ++ v2 ++ b & v1 \in rule v2])
          (u1 \in congrrule u2).

Lemma rule_congrrule u v : v \in rule u -> v \in congrrule u.

Lemma congrrule_is_congr : congruence_rule congrrule.

Hypothesis Hinvar_congr :
  forall u a b1 b2 c,
    invar inv b1 b2 -> invar inv u (a ++ b1 ++ c) -> invar inv u (a ++ b2 ++ c).

Lemma congrrule_invar u v :
 invar inv u v -> all (invar inv u) (congrrule v).

Lemma congrrule_sym u v : v \in congrrule u -> u \in congrrule v.

Definition invcont_congr :=
  InvariantContext (Hinvar_refl inv) congrrule_invar (@Hbound _ _ inv).

Definition gencongr := rtrans invcont_congr.
Definition genclass := rclass invcont_congr.

Lemma genclassE u v : (u \in genclass v) = (u \in gencongr v).

Lemma gencongr_equiv : equivalence_rel gencongr.

Lemma gencongr_is_congr : congruence_rel gencongr.

Lemma rule_gencongr u v : v \in rule u -> v \in gencongr u.

Lemma gencongr_min (r : rel word) :
  equivalence_rel r -> congruence_rel r ->
  (forall x y, y \in rule x -> r x y) ->
  forall x y, gencongr x y -> r x y.

Theorem gencongr_ind (P : word -> Prop) x :
  P x ->
  (forall a b1 c b2, P (a ++ b1 ++ c) -> b2 \in rule b1 -> P (a ++ b2 ++ c)) ->
  forall y, gencongr x y -> P y.

Lemma gencongr_invar u v : gencongr u v-> invar inv u v.

Variant Generated_EquivCongruence (grel : rel word) :=
  GenCongr : equivalence_rel grel ->
             congruence_rel grel ->
             ( forall u v, v \in rule u -> grel u v ) ->
             ( forall r : rel word,
                      equivalence_rel r -> congruence_rel r ->
                      (forall x y, y \in rule x -> r x y) ->
                      forall x y, grel x y -> r x y
             ) -> Generated_EquivCongruence grel.

Theorem gencongrP : Generated_EquivCongruence gencongr.

Lemma gencongr_imply r1 r2 :
  Generated_EquivCongruence r1 -> Generated_EquivCongruence r2 ->
  forall x y, r1 x y -> r2 x y.

Theorem gencongr_unique grel :
  Generated_EquivCongruence grel -> grel =2 gencongr.

Theorem gencongr_generic_ind grel (P : word -> Prop) x :
  Generated_EquivCongruence grel ->
  P x ->
  (forall a b1 c b2, P (a ++ b1 ++ c) -> b2 \in rule b1 -> P (a ++ b2 ++ c)) ->
  forall y, grel x y -> P y.

End CongruenceClosure.

Multi-homogeneous congruence rules

Section InvarContMultHom.

Variable Alph : eqType.
Notation word := (seq Alph).

Variable rule : word -> seq word.
Hypothesis Hmulthom : forall u : word, all (perm_eq u) (rule u).

Lemma perm_bound (x : word) (s : seq word) :
  all (perm_eq x) s -> uniq s -> size s <= (size x)`!.

Lemma perm_invar (x0 x : word) : perm_eq x0 x -> all (perm_eq x0) (rule x).

Definition invcont_perm :=
  InvariantContext (@perm_refl _) perm_invar perm_bound.

Hypothesis Hsym : forall u v : word, v \in rule u -> u \in rule v.
Hypothesis Hcongr : congruence_rule rule.

Lemma perm_invar_congr u (a b1 b2 c : word) :
  invar invcont_perm b1 b2 ->
  invar invcont_perm u (a ++ b1 ++ c) -> invar invcont_perm u (a ++ b2 ++ c).

Definition gencongr_multhom := gencongr perm_invar_congr.
Definition genclass_multhom := genclass perm_invar_congr.

End InvarContMultHom.

Homogeneous congruence rules on a finite type

Section InvarContHom.

Variable Alph : finType.
Notation word := (seq Alph).

Variable rule : word -> seq word.
Let szinvar (u : word) := [pred v : word | size v == size u].
Hypothesis Hhom : forall u : word, all (szinvar u) (rule u).

Lemma size_bound (x : word) (s : seq word) :
  all (szinvar x) s -> uniq s -> size s <= #|Alph|^(size x).

Lemma size_invar (x0 x : word) : szinvar x0 x -> all (szinvar x0) (rule x).

Lemma size_invar_refl (x : word) : szinvar x x.

Definition invcont_size :=
  InvariantContext size_invar_refl size_invar size_bound.

Hypothesis Hcongr : congruence_rule rule.

Lemma size_invar_congr u (a b1 b2 c : word) :
  invar invcont_size b1 b2 ->
  invar invcont_size u (a ++ b1 ++ c) -> invar invcont_size u (a ++ b2 ++ c).

Definition gencongr_hom := gencongr size_invar_congr.
Definition genclass_hom := genclass size_invar_congr.

End InvarContHom.