在Coq中，將目標從'S x = S y'更改爲'x = y'的策略

我想要將目標從S x = S y更改爲x = y。這就像inversion，但爲了目標而不是假設。在Coq中，將目標從'S x = S y'更改爲'x = y'的策略

這種戰術似乎合法的，因爲當我們有x = y，我們可以簡單地使用rewrite和reflexivity證明的目標。

目前我總是發現自己使用assert (x = y)來引入一個新的子目標，但是當編寫x和y是一個複雜的表達時，它是很繁瑣的。

2012-12-06 Tianyi Cui

的戰術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。）

2012-12-08 21:56:11 PLL

你也可以使用'f_equal'策略，它可以節省一些打字。 – hugomg

2012-12-06 19:26:52 Virgile

這是不正確的：「注入」實現了形式'fx = fy - > x = y'的含義（並且這不適用於任意函數'f'，僅適用於構造函數的特殊情況）。 OP所描述的僅僅是使用反函數蘊涵'x = y - > f x = f y'，它適用於任何函數。 – PLL

是的，對不起，我誤解了這個問題，並認爲問題是當'S x = S y'出現在假設中時。 – Virgile

回答