proof - 在 Coq 中，将目标从 `S x = S y` 更改为 `x = y` 的策略

Question

我想将目标从更改S x = S y为x = y。就像inversion，但为了目标而不是假设。

这样的策略似乎是合法的，因为当我们有时x = y，我们可以简单地使用rewriteandreflexivity来证明目标。

目前我总是发现自己assert (x = y)用来引入一个新的子目标，但是写 whenx和yare 复杂的表达式很乏味。

score 7 · Accepted Answer

对于任何构造函数或函数，该策略apply f_equal.都会做你想做的事。

引理f_equal表明，对于任何函数f，你总是有x = y -> f x = f y. 这使您可以将目标从减少f x = f y到x = y：

Proposition myprop (x y: nat) (H : x = y) : S x = S y.
Proof.
  apply f_equal.  assumption.
Qed.

（该injection策略实现了相反的含义——对于某些函数，特别是对于构造函数，f x = f y -> x = y.）

score 1 · Accepted Answer

2 回答 2