y = x ...">
Geek Answers Handbook

How to "flip" an equality sentence in Coq?

If I'm in Coq, and I find myself in a situation with this goal:

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

Is there a tactic that can take care of this in one fell swoop? Be that as it may, I write

intros H. rewrite -> H. reflexivity.

But this is a little awkward.

+4
source share
2 answers

To “flip” equality H: x = y, you can use symmetry in H. If you want to flip a target, just use symmetry.

+6
source

If you are looking for one tactic, then the easytactic immediately processes this:

Coq < Parameter x y : nat.
x is assumed
y is assumed

Coq < Lemma sym : x = y -> y = x.
1 subgoal

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

sym < easy.
No more subgoals.

If you look at the proof that the tactics found, the easykey part is the application eq_sym:

sym < Show Proof.
(fun H : x = y => eq_sym H)

auto . , , symmetry ( intro):

sym < Restart.
1 subgoal

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

sym < symmetry.
1 subgoal

  H : x = y
  ============================
   x = y

sym < assumption.
No more subgoals.

sym < Show Proof.
(fun H : x = y => eq_sym H)
+3

More articles:


All Articles