Rewriting with AC (not modulo AC), using a small scale command.

[CohenCyril]

Replaces opA, opC, opAC, opCA, ... and any combinations of them

Usage :
rewrite [pattern](AC patternshape reordering)
rewrite [pattern](ACl reordering)
rewrite [pattern](ACof reordering reordering)
rewrite [pattern]op.[AC patternshape reordering]
rewrite [pattern]op.[ACl reordering]
rewrite [pattern]op.[ACof reordering reordering]

• if op is specified, the rule is specialized to op
  otherwise, the head symbol is a generic comm_law
  and the rewrite might be less efficient
  NOTE because of a bug in Coq's notations notations/syndefs with parameters applied to holes result in tac-in-term not being executed coq/coq#8190
  op must not contain any hole.
  *%R.[AC p s] currently does not work because of that
  (@GRing.mul R).[AC p s] must be used instead

• pattern is optional, as usual, but must be used to select the appropriate operator in case of ambiguity such an operator must have a canonical Monoid.com_law structure (additions, multiplications, conjuction and disjunction do)

• patternshape is expressed using the syntax
  p := n | p * p'
  where * is formal and n (assuming n > 0) is number of left associated symbols
  examples of pattern shapes:

  • 4 represents (n * m * p * q)
  • (1*2) represents (n * (m * p))

• reordering is expressed using the syntax
  s := n | s * s'
  where * is formal and n (assuming n > 0) is the position in the LHS
  positions start at 1 !

If the ACl variant is used, the patternshape defaults to the pattern fully associated to the left i.e. n i.e (x * y * ...)

Examples of reorderings:

• ACl ((1*2)*3) is the identity (and will fail with error message)
• opAC <-> op.[ACl (1*3)*2] <-> op.[AC 3 ((1*3)*2)]
• opCA <->op.[AC (2*1) (1*2*3)]
• opACA <-> op.[AC (2*2) ((1*3)*(2*4))]
• rewrite opAC -opA is rewrite op.[ACl 1*(3*2)]

TODO:

• ChangeLog entry
• Use cases in the library.

[CohenCyril]

Hi @pi8027! I have had this small dev pending for a while, and after listening to your talk I revived it.
The difference with you work is the fact that the shapes of the terms have to be provided by hand, and the comparison function is not using a merge sort but some kind of spaghetti sort instead.
There would be some ltac plumbery to do to compute the shapes from LHS and RHS in ltac and apply: (AC shape_lhs shape_rhs).

[pi8027]

@CohenCyril I discovered many clever techniques in your code! I am especially surprised that your "spaghetti sort" can be done in O(n log n). Thanks for sharing your work.

Here I point out an issue I found (but I don't know how can we solve it...):

• https://github.com/CohenCyril/math-comp/blob/aab7a3be907430c131f51c844686c56de24c8bcf/mathcomp/ssrtest/test_ssrAC.v#L5,
  https://github.com/CohenCyril/math-comp/blob/aab7a3be907430c131f51c844686c56de24c8bcf/mathcomp/ssrtest/test_ssrAC.v#L9
  Some orb_comoids and addn_comoids are left in the goal after rewriting.

[pi8027]

• https://github.com/CohenCyril/math-comp/blob/aab7a3be907430c131f51c844686c56de24c8bcf/mathcomp/ssreflect/ssrAC.v#L210
  have: pat' = ord by reflexivity can be replaced with unify pat' ord or unify pat ord. It would be a smarter way to invoke the convertibility test.
• https://github.com/CohenCyril/math-comp/blob/aab7a3be907430c131f51c844686c56de24c8bcf/mathcomp/ssreflect/ssrAC.v#L213
  In this context, vm_compute; reflexivity seems to be equivalent to reflexivity. (I don't know which one is efficient.)

[CohenCyril]

@pi8027 Thank you for your positive feedback! I am glad you found it interesting.

I am especially surprised that your "spaghetti sort" can be done in O(n log n). Thanks for sharing your work.

I did not take the time to check (did you?) but I believe it is indeed O(n log n) in time and a call stack of size O(log n).

Some orb_comoids and addn_comoids are left in the goal after rewriting.

This is unavoidable when the rule is quantified over a monoid law, (indeed lemmas Monoid.mulm1 ... leave similar overhead). The goal can be simplified using /=, and if you really do not want this, you may use the op.[AC p s] rule instead.

have: pat' = ord by reflexivity can be replaced with unify pat' ord or unify pat ord. It would be a smarter way to invoke the convertibility test.

AFAIK, unify x y invokes unification, which in this case is not necessary because the terms must be ground, and it might be less efficient (wouldn't it?)

In this context, vm_compute; reflexivity seems to be equivalent to reflexivity. (I don't know which one is efficient.)

vm_compute; reflexivity inserts a vm cast to make the computation using the VM instead of the abstract machine, so should be more efficient. I guess this whole ltac: () notation could be replaced by (isT <: _), but it would prevent me from producing a nice error message.

[CohenCyril]

@maximedenes this is how I encountered the issue coq/coq#8190

[pi8027]

@CohenCyril

I did not take the time to check (did you?) but I believe it is indeed O(n log n) in time and a call stack of size O(log n).

Proof. Let us suppose that a reordering s: syntax consists of m leaves and the largest leaf in s is n. It is easy to check that the height of acc: env N is always less than or equal to (log_2 n + 1) during the execution of content s. Each set_pos 0%num Nsucc acc n does only two things: [part 1: O(log n)] reconstructs a path in acc from the root to the node of position n and [part 2: O(log m)] increments the node value of position n. The whole sorting process content s repeats set_pos ... m times and can be done in O(m log(nm)). In this usage, well-formed reordering syntax holds the equation n = m (right?). So the sorting can be done in O(n log n) time complexity. ■

However, content may consume the call stack linearly. I think that it can't be solved.

This is unavoidable when the rule is quantified over a monoid law, (indeed lemmas Monoid.mulm1 ... leave similar overhead). The goal can be simplified using /=, and if you really do not want this, you may use the op.[AC p s] rule instead.

I understood it. Thank you.

vm_compute; reflexivity inserts a vm cast to make the computation using the VM instead of the abstract machine, so should be more efficient. I guess this whole ltac: () notation could be replaced by (isT <: _), but it would prevent me from producing a nice error message.

I compared reflexivity and vm_compute; reflexivity in some examples. You were right!

AFAIK, unify x y invokes unification, which in this case is not necessary because the terms must be ground, and it might be less efficient (wouldn't it?)

I compared two normalized ground terms by unify and reflexivity. The following example seems to indicate that the unify tactic is slightly better on efficiency.

Require Import ssreflect Arith ZArith.

Goal False.
Proof.
let x := constr: ((1000 ^ 2000)%Z) in
let y := constr: ((1000000 ^ 1000)%Z) in
let x' := eval vm_compute in x in
let y' := eval vm_compute in y in
(time unify x' y');
(time let _ := constr: (eq_refl _ : x' = y') in idtac);
(time have _: x' = y' by reflexivity).
(*
Tactic call ran for 0.007 secs (0.007u,0.s) (success)
Tactic call ran for 0.02 secs (0.019u,0.s) (success)
Tactic call ran for 0.179 secs (0.18u,0.s) (success)
*)
Abort.

[CohenCyril]

@pi8027

Proof [...] ■

Yeah I'm convinced by your proof.

However, content may consume the call stack linearly. I think that it can't be solved.

I'd say both content and set_pos occupy O(log n) of the stack each, because there is one non tail recursive call in each.
I replaced set_pos by a tail recursive alternative set_pos_trec (using Huet's zipper), so that only the non tail recursive calls of content consume the stack, and I think that is the best I can do.

I compared two normalized ground terms by unify and reflexivity. The following example seems to indicate that the unify tactic is slightly better on efficiency.

I am surprised...

[CohenCyril]

I'd say both content and set_pos occupy O(log n) of the stack each, because there is one non tail recursive call in each.

oh, but each continuation contains a tree of half of the size of the argument...

[pi8027]

@CohenCyril

I am surprised...

It is easy to check that reflexivity may instantiate existential variables like as unify. So I guess that have _: x = y by reflexivity and unify x y have the same behavior for any x and y. However, the former one does some additional tasks: trying to instantiate the goal and type checking of erefl: x = y (that includes convertibility test x =? y). Your neighbors would know whether my understanding is correct or not, and more details. :)

[gares]

The only comment I have right now is that, as for under, there is quite some ltac code.

I think it is good to make a prototype and let people play with it, but at some point things should be rewritten in ML, so that one can just call whd_all rather than going trough notations and tactics-in-terms to perform some reduction on the given term.

[amahboubi]

Hi, I think that it is great to have this code available, but I also think that it is not ready (yet) for merge. The roadmap is probably something to be discussed in the next dev working group. By the way, could you document the (names of the) constants that are the user's environment after a Require Import ssr_AC?

[CohenCyril]

Hi @amahboubi right now the following notations are exported:

• AC_check_pattern, AC_strategy, opACof law p s, opAC op p s, opACl op s which are internal (but outside of the module AC for technical reason (namely too agressive name substitution in ltac in notation (not sure this is a bug though...)))
• op .[ 'ACof' p s ], op .[ 'AC' p s ], op .[ 'ACl' s ], ACof p s, AC p s and ACl s which are documented in the header (I realize now a scope is missing for non simple notations, this must be fixed).
• 1 and x * y in scope AC_scope (shortened with %AC which is bound to the right arguments of the previous notations, so no explicit %AC is required). Also documented in the header (except for the scope).

And all the exported constants are prefixed with module AC.

Do you want me to add this to the header?

[CohenCyril]

This PR needs an assignee...

[affeldt-aist]

From the release managers for 1.11: does this PR really need propagation? Could it be merged as is and an issue be opened to propagate?

[CohenCyril]

I would be happy that this merged, but it has not been reviewed and it had no assignee... and I guess it is difficult to assess. It should at least be rebased, let me do that first...

[CohenCyril]

I rewrote some proof scripts using ssrAC, just for the example. Two are significantly shorter but were badly written in the first place.
It is very likely that this tool will essentially help during proof development, but that final refactoring of proofs will hopefully get rid of it... but I guess it is a useful tool for that purpose.

As such, I will remove the "needs: propagation" label. If we change our minds we can reestablish it. I am also in favor of having this part of the beta, and withdraw it in the final release if necessary (as I said in my previous post)

[gares]

Some versions of Coq fail with message The term "2" has type "nat" while it is expected to have type "GRing.Ring.sort ?R1".

I personally don't care about 8.7..8.9 much, but if this PR is the only reason to drop compatibility with them, then I'm not in favor of merging it "as it is".

[CohenCyril]

Some versions of Coq fail with message The term "2" has type "nat" while it is expected to have type "GRing.Ring.sort ?R1".

I personally don't care about 8.7..8.9 much, but if this PR is the only reason to drop compatibility with them, then I'm not in favor of merging it "as it is".

You are right, we should not lose compatibility and the tests and the main file used to passe.
I tried to rewrite some parts of the libraries but it seems I messed with scopes somehow, I will look into it by tomorrow noon.

[CohenCyril]

@gares @affeldt-aist @ybertot should we integrate it?

[ybertot]

ping @gares