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

Question

我正在研究证据,我的一个子目标看起来有点像这样:

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等)的差异很小,假设(有时会有一个额外的归纳假设或两个)和最后的布尔公式.我认为,如果我可以使用自动化来解决这个问题,我的整体校对脚本会更加简洁和强大.

---

编辑:如果其中一个假设存在问题怎么办？

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

Answer 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 。