将联合目标拆分为子目标

Question

考虑以下玩具练习：

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

此时我有以下内容：

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

我想将目标分成两个子目标，m = n 和 n = m。有这样的策略吗？

Answer 1

使用f_equal策略解决：

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

状态：

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

Split conjunction goal into subgoals