coq插件-如何使用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.

生成错误:

错误:tactical failure: Not an equal modulo 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.