有没有办法通过重写步骤自动化 Coq 证明？

Posted 2023-03-28

【中文标题】有没有办法通过重写步骤自动化 Coq 证明？

【英文标题】：Is there a way to automate a Coq proof with rewrite steps?

【发布时间】：2016-11-14 19:06:45

【问题描述】：

我正在做一个证明，我的一个子目标看起来有点像这样：

Goal forall
  (a b : bool)
  (p: Prop)
  (H1: p -> a = b)
  (H2: p),
  negb a = negb b.
Proof.
  intros.
  apply H1 in H2. rewrite H2. reflexivity.
Qed.

证明不依赖于任何外部引理，仅包括将上下文中的一个假设应用于另一个假设并使用已知假设重写步骤。

有没有办法让这个自动化？我尝试做intros. auto.，但没有效果。我怀疑这是因为auto 只能执行apply 步骤但不能执行rewrite 步骤，但我不确定。也许我需要一些更强的策略？

我想要自动执行此操作的原因是，在我最初的问题中，我实际上有大量与这个非常相似的子目标，但假设的名称（H1、H2 等）略有不同，假设的数量（有时还有一个或两个额外的归纳假设）和最后的布尔公式。我认为如果我可以使用自动化来解决这个问题，我的整体证明脚本会更加简洁和健壮。

---

编辑：如果其中一个假设有一个 forall 怎么办？

Goal forall
  (a b c : bool)
  (p: bool -> Prop)
  (H1: forall x, p x -> a = b)
  (H2: p c),
  negb a = negb b.
Proof.
  intros.
  apply H1 in H2. subst. reflexivity.
Qed

【参考方案1】：

当您在证明某些引理的过程中看到重复模式时，您通常可以定义自己的策略来自动化证明。

在您的具体情况下，您可以编写以下内容：

Ltac rewrite_all' :=
  match goal with
  | H  : _ |- _ => rewrite H; rewrite_all'
  | _ => idtac
 end.

Ltac apply_in_all :=
  match goal with
  | H  : _, H2 : _ |- _ => apply H in H2; apply_in_all
  | _ => idtac
 end.

Ltac my_tac :=
  intros;
  apply_in_all;
  rewrite_all';
  auto.

Goal forall (a b : bool) (p: Prop) (H1: p -> a = b) (H2: p), negb a = negb b.
Proof.
  my_tac.
Qed.

Goal forall (a b c : bool) (p: bool -> Prop)
  (H1: forall x, p x -> a = b)
  (H2: p c),
  negb a = negb b.
Proof.
  my_tac.
Qed.

如果您想遵循这条写证明的道路，通常推荐（但我还没有阅读）的参考文献是 Adam Chlipala 的 CPDT。

【讨论】：

有趣！顺便说一句，如果你有两个这样的假设：(H1: p -> a = b) (H1swap : a = b -> p)，apply_in_all 将永远循环。

Cpdt 的crush 策略单独可以解决第一个目标，但在使用谓词的情况下会失败。

@AntonTrunov 对。感谢您注意到这一点。它显示了这种编写证明方式的一个限制：它很快就会变得混乱，然后很难调试。

【参考方案2】：

这个特定的目标可以这样解决：

Goal forall (a b : bool) (p: Prop) (H1: p -> a = b) (H2: p),
  negb a = negb b.
Proof.
  now intuition; subst.
Qed.

或者，使用destruct_all 策略（前提是您没有很多布尔变量）：

intros; destruct_all bool; intuition.

以上是在destr_bool 策略之后建模的，在Coq.Bool.Bool 中定义：

Ltac destr_bool :=
  intros; destruct_all bool; simpl in *; trivial; try discriminate.  

你也可以尝试使用类似的东西

destr_bool; intuition.

在简单的destr_bool 之后激发强大的intuition。

---

now在Coq.Init.Tactics中定义如下

Tactic Notation "now" tactic(t) := t; easy.

easy 定义在它的正上方，（顾名思义）可以解决简单的目标。

intuition 可以解决需要应用（直觉）逻辑法则的目标。例如。以下两个来自问题原始版本的假设需要应用自决方式法则。

H1 : p -> false = true
H2 : p

另一方面，auto 默认不这样做，它也不能解决矛盾。

如果你的假设包括一些一阶逻辑语句，firstorder 策略可能是答案（就像在这种情况下）——只需用它替换 intuition。

【讨论】：

now 是战术名称还是关键字？我很难搜索文档，因为有很多误报。你能否解释一下auto和`intuition for this question有什么区别？

我还注意到 intuition 策略无法解决我最初的问题，因为其中一种策略有一个 forall （请参阅我对问题的编辑）。有没有办法解决这个问题？

@hugomg 我已经更新了答案。似乎无法修改第一个版本（带有now），但其余版本似乎可以正常使用提议的修改。

哦，好吧......不幸的是，我原来的例子是使用更复杂的类型而不是 bool，所以 destruct_all 也不理想:(

这种情况偶尔会发生，当人们试图为 SO 简化事情时 :) 也许有人会想出一个更通用的方法。您还可以发布另一个问题以提供更多详细信息，我相信我们将能够以某种方式提供帮助。无论如何，这本身就是一个很好的问题！快乐的黑客攻击！