如何自动利用 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

一个相当通用的构造是 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 中的某些章节（可能）。

Answer 2

我相信您正在寻找的结构是

Hint Rewrite false_eqb_string using solve [ trivial ].

the reference manual 中对此进行了记录。与 rewrite ... by ... 不同，Hint Rewrite ... using ... 不会在策略未完全解决附加条件时撤消重写，因此您必须将其包装在 solve [ ... ] 中才能获得该效果。

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

How to automatically leverage hypotheses of the form x <> y?

coq

coq-tactic