coq - 将联合目标拆分为子目标

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