Library RelationAlgebra.rewriting


rewriting: additional rewriting support


Require Import monoid.

rewriting modulo associativity of dot

We notice that to rewrite modulo A, it suffices to normalise associativity, and to use an extended lemma: for instance, if one wants to rewrite using a closed hypothesis
H: a_1*...*a_n == c
in a goal including a subterm like d×e×a_1*...*a_n×f, then one can simply rewrite using
(ext_weq_n H): x, x×a_1*...*a_n == x×c
where ext_weq_n is the appropriate lemma (see rewriting.v).
Such a lemma could be generated by hand, but it's a bit heavy, so that we simply hardwire it for n=2,3,4
This trick generalises to "open" equations, like
H: x y, P x y z, y*(x+z)*y == y
where one wants to rewrite using (fun x y Hxy z ext_weq_3 (H x y Hxy z))
The ML plugin mrewrite generates such abstractions in the appropriate way, taking care efficiently of the order in which one wants to rewrite, and whether we have an equation or an inequation. (Doing so in Ltac is both painful and inefficient.)
Of course the method is incomplete (e.g., if y has to be instantiated by a product), but it seems enough for most common situations. The advantage over using the AAC_tactics library is that it's much faster since reification is "syntactic", and that it works for typed structures and heterogeneous terms, which are not supported in AAC_tactics.

Lemma ext_leq_2 `{laws} {n m p} (x: X n m) (y: X m p) v: x×y <== v
   o (u: X o n), u×x×y <== u×v.
Proof. intros E ? ?. now rewrite <-E, !dotA. Qed.

Lemma ext_leq_3 `{laws} {n m p q} (x: X n m) (y: X m p) (z: X p q) v: x×y×z <== v
   o (u: X o n), u×x×y×z <== u×v.
Proof. intros E ? ?. now rewrite <-E, !dotA. Qed.

Lemma ext_leq_4 `{laws} {n m p q r} (x: X n m) (y: X m p) (z: X p q) (t: X q r) v: x×y×z×t <== v
   o (u: X o n), u×x×y×z×t <== u×v.
Proof. intros E ? ?. now rewrite <-E, !dotA. Qed.

Lemma ext_weq_2 `{laws} {n m p} (x: X n m) (y: X m p) v: x×y == v
   o (u: X o n), u×x×y == u×v.
Proof. intros E ? ?. now rewrite <-E, !dotA. Qed.

Lemma ext_weq_3 `{laws} {n m p q} (x: X n m) (y: X m p) (z: X p q) v: x×y×z == v
   o (u: X o n), u×x×y×z == u×v.
Proof. intros E ? ?. now rewrite <-E, !dotA. Qed.

Lemma ext_weq_4 `{laws} {n m p q r} (x: X n m) (y: X m p) (z: X p q) (t: X q r) v: x×y×z×t == v
   o (u: X o n), u×x×y×z×t == u×v.
Proof. intros E ? ?. now rewrite <-E, !dotA. Qed.

Lemma ext_leq_2' `{laws} {n m p} (x: X n m) (y: X m p) v: v <== x×y
   o (u: X o n), u×v <== u×x×y.
Proof. intros E ? ?. now rewrite E, !dotA. Qed.

Lemma ext_leq_3' `{laws} {n m p q} (x: X n m) (y: X m p) (z: X p q) v: v <== x×y×z
   o (u: X o n), u×v <== u×x×y×z.
Proof. intros E ? ?. now rewrite E, !dotA. Qed.

Lemma ext_leq_4' `{laws} {n m p q r} (x: X n m) (y: X m p) (z: X p q) (t: X q r) v: v <== x×y×z×t
   o (u: X o n), u×v <== u×x×y×z×t.
Proof. intros E ? ?. now rewrite E, !dotA. Qed.

Lemma ext_weq_2' `{laws} {n m p} (x: X n m) (y: X m p) v: v == x×y
   o (u: X o n), u×v == u×x×y.
Proof. intros E ? ?. now rewrite E, !dotA. Qed.

Lemma ext_weq_3' `{laws} {n m p q} (x: X n m) (y: X m p) (z: X p q) v: v == x×y×z
   o (u: X o n), u×v == u×x×y×z.
Proof. intros E ? ?. now rewrite E, !dotA. Qed.

Lemma ext_weq_4' `{laws} {n m p q r} (x: X n m) (y: X m p) (z: X p q) (t: X q r) v: v == x×y×z×t
   o (u: X o n), u×v == u×x×y×z×t.
Proof. intros E ? ?. now rewrite E, !dotA. Qed.

Declare ML Module "mrewrite".

User-end rewriting tactics

Tactic Notation "mrewrite" constr(H) :=
  rewrite ?dotA; (rewrite H || ra_extend (fun Hrewrite H) →H); [rewrite ?dotA|..].
Tactic Notation "mrewrite" "<-" constr(H) :=
  rewrite ?dotA; (rewrite <-H || ra_extend (fun Hrewrite <-H) <-H); [rewrite ?dotA|..].
Tactic Notation "mrewrite" constr(H) "in" hyp(H') :=
  rewrite ?dotA in H'; (rewrite H in H' || ra_extend (fun Hrewrite H in H') →H); rewrite ?dotA in H'.
Tactic Notation "mrewrite" "<-" constr(H) "in" hyp(H') :=
  rewrite ?dotA in H'; (rewrite <-H in H' || ra_extend (fun Hrewrite <-H in H') <-H); rewrite ?dotA in H'.

Bridge with AAC_tactics

(to be activated manually, by uncommenting the lines below.)