CODEWITHSUNDEEP
coq
limp_chimp
limp_chimp

Reputation: 15203

How to "flip" an equality proposition in Coq?

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.

Upvotes: 7

Views: 3218

Answers (2)

Vinz
Vinz

Reputation: 6057

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

Upvotes: 10

Mark Dickinson
Mark Dickinson

Reputation: 30856

If you're looking for a single tactic, then the easy tactic handles this one immediately:

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 take a look at the proof that the easy tactic found, the key part is an application of eq_sym:

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

The heavier-weight auto tactic will also handle this goal in a single step. For a slightly lower-level proof that produces exactly the same proof term, you can use the symmetry tactic (which also automatically does the necessary intro for you):

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)

Upvotes: 4

Related Questions