How to use Coq aac tactics to prove equalities in the goal?

Question

I am guessing that Coq aac_tactics (8.5p1) should be able to deal with assoc. and commutativity. But I can't figure out how to use it prove simple equalities such as

2 + y + 5 = 7 + y

For example:

Require Import AAC_tactics.AAC.
Require Import AAC_tactics.Instances.
Goal forall y: nat, 2 + y + 5 = 7 + y.
intros ?.  
aac_reflexivity.

generates an error:

Error: Tactic failure: Not an equality modulo A/AC.

Changing the last tactic to aac_normalise doesn't solve it either.

How can such goals be proven using AAC?

Answer 1

The documentation is pretty scarce, so I can only guess that your example requires some explicit rewritings (essentially, you need to show 5 + 2 = 7).

Notice that the next example works because it doesn't need the fact that 5 + 2 = 7:

Goal forall y : nat, 2 + y + 5 = 5 + y + 2.
  intros ?.
  aac_reflexivity.
Qed.

So, if I'd do the original example like this:

Goal forall y : nat, 2 + y + 5 = 7 + y.
  intros ?.
  assert (5 + 2 = 7) as H. reflexivity.
  aac_rewrite H.
  aac_reflexivity.
Qed.