CODEWITHSUNDEEP
coqcoq-tactic
Carl Patenaude Poulin
Carl Patenaude Poulin

Reputation: 6589

Split conjunction goal into subgoals

Consider the following toy exercise:

Theorem swap_id: forall (m n : nat), m = n -> (m, n) = (n, m).
Proof.
  intros m n H.

At this point I have the following:

1 subgoal
m, n : nat
H : m = n
______________________________________(1/1)
(m, n) = (n, m)

I would like to split the goal into two subgoals, m = n and n = m. Is there a tactic which does that?

Upvotes: 1

Views: 554

Answers (1)

Carl Patenaude Poulin
Carl Patenaude Poulin

Reputation: 6589

Solve using the f_equal tactic:

Theorem test: forall (m n : nat), m = n -> (m, n) = (n, m).
Proof.
  intros m n H. f_equal.

With state:

2 subgoals
m, n : nat
H : m = n
______________________________________(1/2)
m = n
______________________________________(2/2)
n = m

Upvotes: 4

Related Questions