rewriting: additional rewriting support

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.

User-end rewriting tactics