如何自动利用x <> y形式的假设？

Question

Goal forall (w x y z: string), w <> x -> (if (eqb_string w x) then y else z) = z.
Proof.
  intros.
  rewrite false_eqb_string by trivial.
  reflexivity.
Qed.

false_eqb_string是一个相当简单的证明原则。我想通过autorewrite或类似方式隐式使用它。不幸的是，如果我添加Hint Rewrite false_eqb_string，那么形式eqb_string _ _的任何子项都会被重写，并且假设_ <> _会添加到目标中，即使这不是一件明智的事情。

如何让rewrite false_eqb_string by trivial自动发生，而不提名呢？

Answer 1

我相信你正在寻找的建筑是

Hint Rewrite false_eqb_string using solve [ trivial ].

这在the reference manual中有记载。与rewrite ... by ...不同，如果策略不能完全解决边条件，Hint Rewrite ... using ...将不会撤消重写，所以你必须将其包裹在solve [ ... ]中以获得该效果。

Answer 2

一个相当一般的结构是match goal with，允许你模式匹配，以及你的目标。因此，您可以在目标中使用相应的布尔比较（或者如果您需要其他假设）来查找假设中的不等式（context _ [ _ ]是一种特殊模式，允许您将任何子项与括号中的模式进行匹配），并使用右引理重写。然后你可以给这个match战术命名，所以你不需要记住引理实际上是如何调用的。正如您所料，match还支持许多子句（需要注意奇怪的回溯行为），因此您可以将此策略扩展到您自己的穷人的重写数据库中。

From Coq Require Import Arith.

Ltac rewrite_eqb :=
  match goal with
  | [ H : ?u <> ?v |- context E [ ?u =? ?v ] ] =>
    rewrite (proj2 (Nat.eqb_neq u v) H)
  end.

Goal forall (w x y z: nat), w <> x -> (if (Nat.eqb w x) then y else z) = z.
Proof.
  intros.
  rewrite_eqb.
  reflexivity.
Qed.

也可以看看：

• The Tactic language: matching on goals参考手册;
• CPDT的一些章节（可能）。