在Coq中，将目标从“ S x = S y”更改为“ x = y”的策略

Question

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

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

目前，我总是发现自己经常使用assert (x = y)新的子目标，但是编写何时x且y复杂的表达式是很繁琐的。

Answer 1

该策略apply f_equal.将对任何构造函数或函数执行您想要的操作。

lema 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。）