Как использовать тактику Coq aac, чтобы доказать равенство в цели?

Question

Я предполагаю, что Coq aac_tactics (8.5p1) должен уметь общаться с асс. и коммутативность. Но я не могу понять, как использовать это доказать простые равенства, такие как

2 + y + 5 = 7 + y

Например:

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

генерирует ошибку:

Ошибка: Тактическая ошибка: Не равенство по модулю A/AC.

Изменение последней тактики на aac_normalise тоже не решает.

Как такие цели могут быть доказаны с помощью AAC?

Answer 1

Документация довольно скудная, поэтому я могу только догадываться, что ваш пример требует некоторых явных переписываний (по сути, вам нужно показать 5 + 2 = 7).

Обратите внимание, что следующий пример работает, потому что ему не нужен тот факт, что 5 + 2 = 7:

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

Итак, если бы я сделал оригинальный пример так:

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