Coq:有没有可能证明，如果两个记录不同，那么其中一个字段就不同

Question

假设您有一个记录：

Record Example := {
fieldA : nat;
fieldB : nat
}.

我们能证明吗：

Lemma record_difference : forall (e1 e2 : Example),
e1 <> e2 ->
(fieldA e1 <> fieldA e2)
/
(fieldB e1 <> fieldB e2).

如果是，如何？

一方面，这看起来是真的，因为Record绝对是由它们的字段定义的。另一方面，在不知道e1与e2的区别的情况下，我们应该如何决定证明析取的哪一边？

---

作为比较，请注意，如果记录中只有一个字段，我们能够证明各自的引理：

Record SmallExample := {
field : nat
}.
Lemma record_dif_small : forall (e1 e2 : SmallExample),
e1 <> e2 -> field e1 <> field e2.
Proof.
unfold not; intros; apply H.
destruct e1; destruct e2; simpl in H0.
f_equal; auto.
Qed.

Answer 1

另一方面，在不知道e1与e2的区别的情况下，我们应该如何决定要证明析取的哪一边？

这正是重点：我们需要弄清楚是什么让这两条记录不同。我们可以通过测试fieldA e1 = fieldA e2。

Require Import Coq.Arith.PeanoNat.
Record Example := {
fieldA : nat;
fieldB : nat
}.
Lemma record_difference : forall (e1 e2 : Example),
e1 <> e2 ->
(fieldA e1 <> fieldA e2)
/
(fieldB e1 <> fieldB e2).
Proof.
intros [n1 m1] [n2 m2] He1e2; simpl.
destruct (Nat.eq_dec n1 n2) as [en|nen]; try now left.
right. intros em. congruence.
Qed.

这里，Nat.eq_dec是标准库中的一个函数，它允许我们检查两个自然数是否相等：

Nat.eq_dec : forall n m, {n = m} + {n <> m}.

{P} + {~ P}表示法表示一种特殊的布尔值，它在被破坏时为P或~ P提供证明，这取决于它位于哪一边。

值得通过这个证明来了解发生了什么。例如，在证明的第三行，执行intros em会导致以下目标。

n1, m1, n2, m2 : nat
He1e2 : {| fieldA := n1; fieldB := m1 |} <> {| fieldA := n2; fieldB := m2 |}
en : n1 = n2
em : m1 = m2
============================
False

如果en和em保持不变，那么这两条记录必须相等，与He1e2相矛盾。congruence策略只是指示Coq尝试自己解决这个问题。

编辑

有趣的是，如果没有决定性的平等，一个人能走多远。以下类似的陈述可以被琐碎地证明：

forall (A B : Type) (p1 p2 : A * B),
p1 = p2 <-> fst p1 = fst p2 / snd p1 = snd p2.

通过对位，我们得到

forall (A B : Type) (p1 p2 : A * B),
p1 <> p2 <-> ~ (fst p1 = fst p2 / snd p1 = snd p2).

正是在这里，我们陷入了没有决定性假设的困境。德摩根定律允许我们将右手边转换为~ P / ~ Q形式的陈述；然而，他们的证明诉诸于可判定性，这在Coq的建设性逻辑中通常是不可用的。