Currently known limitations and caveats of AAC Tactics

Limitations

Dependent parameters

The type of the rewriting hypothesis must be of the form forall (x_1: T_1) ... (x_n: T_n), R l r where R is a relation over some type T and such that for all variable x_i appearing in the left-hand side (l), we actually have T_i = T. The goal should be of the form S g d, where S is a relation on T. In other words, we cannot instantiate arguments of an exogeneous type.

In Hf, since the parameter n has type nat, it cannot be instantiated automatically

aac_rewrite does not instantiate n automatically

of course, this argument can be given explicitly

For the same reason, we cannot handle higher-order parameters (here, g)

Exogeneous morphisms

We do not handle "exogeneous" morphisms: morphisms that move from type T to some other type T'.

Typically, although N_of_nat is a proper morphism from @eq nat to @eq N, we cannot rewrite under N_of_nat

More generally, this prevents us from rewriting under propositional contexts

a solution is to introduce an evar to replace the part to be rewritten - this tiresome process should be improved in the future; here, it can be done using eapply and the morphism

similarly, we need to bring equations to the toplevel before being able to rewrite

Treatment of variance with inequations

We do not take variance into account when we compute the set of solutions to a matching problem modulo AC. As a consequence, aac_instances may propose solutions for which aac_rewrite will fail, due to the lack of adequate morphisms.

this fails because the first solution is not valid (Z.opp is not increasing)

on the contrary, the second solution is valid:

currently, we cannot filter out such invalid solutions in an easy way; this should be fixed in the future

Caveats

Special treatment for units

S 0 is considered as a unit for multiplication whenever a Nat.mul appears in the goal. The downside is that S x does not match 1, and 1 does not match S (0 + 0) whenever Nat.mul appears in the goal.

OK (no multiplication around), x is instantiated with O

fails since 1 is seen as a unit, not the application of the morphism S to the constant O

OK (no multiplication around), x is instantiated with a

fails: although S (0+0) is understood as the application of the morphism S to the constant O, it is not recognised as the unit S O of multiplication

More generally, similar counter-intuitive behaviours can appear when declaring an applied morphism as a unit

Existential variables

We implemented an algorithm for matching modulo AC, not for unifying modulo AC. As a consequence, existential variables appearing in a goal are considered as constants and will not be instantiated.

this works: x is instantiated with an evar

this does work but there are remaining evars in the end

this fails since we do not instantiate evars

Distinction between aac_rewrite and aacu_rewrite

in some situations, the aac_rewrite tactic allows instantiations of a variable with a unit, when the variable occurs directly under a function symbol:

this behaviour seems desirable in most situations: these solutions with units are less peculiar than the other ones, since the unit comes from the goal; however, this policy is not properly enforced for now (hard to do with the current algorithm):

Rewriting units

aac_rewrite uses the symbols appearing in the goal and the hypothesis to infer the AC and A operations. In the following example, dot appears neither in the left-hand-side of the goal, nor in the right-hand side of the hypothesis. Hence, 1 is not recognised as a unit. To circumvent this problem, we can force aac_rewrite to take into account a given operation, by giving it an extra argument. This extra argument seems useful only in this peculiar case.

Rewriting too many things

aac_rewrite finds a pattern modulo AC that matches a given hypothesis, and then makes a call to setoid_rewrite. This setoid_rewrite can unfortunately make several rewrites (in a non-intuitive way: below, the 1 in the right-hand side is rewritten into S c)

to this end, we provide a companion tactic to aac_rewrite and aacu_rewrite, that makes the transitivity step, but not the setoid_rewrite; this allows the user to select the relevant occurrences in which to rewrite:

Rewriting nullifiable patterns

If the pattern of the rewritten hypothesis does not contain "hard" symbols (like constants, function symbols, AC or A symbols without units), there can be infinitely many subterms such that the pattern matches: it is possible to build "subterms" modulo ACU that make the size of the term increase (by making neutral elements appear in a layered fashion). Hence, we settled with heuristics to propose only "some" of these solutions. In such cases, the tactic displays a (conservative) warning.

in this case, only three solutions are proposed, while there are infinitely many solutions, for example:

• a+b*c*(1+☐)
• a+b*c*(1+0*(1+ ☐))
• ...

If the pattern is a unit or can be instantiated to be equal to a unit

The heuristic is to make the unit appear at each possible position in the term, e.g. transforming a into 1*a and a*1, but this process is not recursive (we will not transform 1*a) into (1+0*1)*a.

1 solution, we miss solutions like (a+b+c*(1+0*(1+[]))) and so on

7 solutions, we miss solutions like (a+b+c+0*(1+0*[]))

Another example of the former case

In the following, the hypothesis can be instantiated to be equal to 1.

here, only one solution if we use the aac_instance tactic

there are 8 solutions using aacu_instances (but, here, there are infinitely many different solutions); we miss, e.g., a*a +b*a + (x*x + y*x)*c, which seems to be more peculiar

the 7 last solutions are the same as if we were matching 1

The behavior of the tactic is not satisfying in this case. It is still unclear how to handle properly this kind of situation; we plan to investigate this in the future.