如何“翻转”Coq中的平等命题？(How to “flip” an equality proposition in Coq?)

如何“翻转”Coq中的平等命题？(How to “flip” an equality proposition in Coq?)

如果我在Coq，并且发现自己处于这样的目标状态：

================== x = y -> y = x

有没有一种策略可以一举处理？ 事实上，我正在写作

intros H. rewrite -> H. reflexivity.

但它有点笨重。

If I'm in Coq and I find myself in a situation with a goal like so:

================== x = y -> y = x

Is there a tactic that can can take care of this in one swoop? As it is, I'm writing

intros H. rewrite -> H. reflexivity.

But it's a bit clunky.

最满意答案

为了“翻转”平等H: x = y ，可以symmetry in H使用symmetry in H 。 如果你想翻转目标，只需使用symmetry 。

To "flip" an equality H: x = y you can use symmetry in H. If you want to flip the goal, simply use symmetry.