coq - 如何使用 Coq aac 战术来证明目标相等？

Question

我猜 Coq aac_tactics(8.5p1) 应该能够处理 assoc。和交换性。但我不知道如何使用它来证明简单的等式，例如

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

文档非常稀缺，所以我只能猜测您的示例需要一些明确的重写（本质上，您需要 show 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.