Coq：证明如果 (A, B) = (C, D) 那么 A = C /\ B = D

Question

如标题所示，我找不到足够的工具来解决这个琐碎的事情：

p : (A, B) = (C, D)
------------
A = C /\ B = D

如何证明？

Answer 1

刚收到。这是 pair_equal_spec:

Proof.
  intros.
  apply pair_equal_spec.
  assumption.
Qed.

Answer 2

更原始的证明方法是injection p。

看看pair_equal_spec本身在标准库中是如何证明的也很有意思，用假设(a1, b1) = (a2, b2)重写了fst (a1, b1)和snd (a1, b1).

Lemma pair_equal_spec :
  forall (A B : Type) (a1 a2 : A) (b1 b2 : B),
    (a1, b1) = (a2, b2) <-> a1 = a2 /\ b1 = b2.
Proof with auto.
  split; intros.
  - split.
    + replace a1 with (fst (a1, b1)); replace a2 with (fst (a2, b2))...
      rewrite H...
    + replace b1 with (snd (a1, b1)); replace b2 with (snd (a2, b2))...
      rewrite H...
  - destruct H; subst...
Qed.

Coq：证明如果 (A, B) = (C, D) 那么 A = C /\ B = D

Coq: prove that if (A, B) = (C, D) then A = C /\ B = D

theorem-proving

coq