在Coq中，将目标从“ S x = S y”更改为“ x = y”的策略 [英] In Coq, which tactic to change the goal from `S x = S y` to `x = y`

问题描述

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

I want to change the goal from S x = S y to x = y. It's like inversion, but for the goal instead of a hypothesis.

这种策略似乎合法，因为当我们有 x = y ，我们可以简单地使用 rewrite 和 reflexivity 证明目标。

Such a tactic seems legit, because when we have x = y, we can simply use rewrite and reflexivity to prove the goal.

目前，我总是使用 assert（x = y）来介绍自己的新目标subgoal，但是当 x 和 y 是复杂表达式时写起来很麻烦。

Currently I always find myself using assert (x = y) to introduce a new subgoal, but it's tedious to write when x and y are complex expression.

推荐答案

策略 应用f_equal。 将为任何构造函数提供所需的功能

The tactic apply f_equal. will do what you want, for any constructor or function.

lema f_equal 显示对于任何函数 f ，您总是有 x = y-> f x = f y 。这使您可以将目标从 fx = fy 降低到 x = y ：

The lema f_equal shows that for any function f, you always have x = y -> f x = f y. This allows you to reduce the goal from f x = f y to x = y:

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

（注入策略实现了相反的含义—对于某些函数，特别是对于构造函数， fx = fy-> x = y 。）

(The injection tactic implements the converse implication — that for some functions, and in particular for constructors, f x = f y -> x = y.)

这篇关于在Coq中，将目标从“ S x = S y”更改为“ x = y”的策略的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！