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).

如果是，怎么做？

一方面，它看起来是真的，因为 Records 是由它们的字段绝对定义的。另一方面，如果一开始就不知道是什么让 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

On the other, without knowing what made e1 different from e2 in the first place, how are we supposed to decide which side of the disjunction to prove?

这正是关键所在：我们需要弄清楚是什么让这两个记录不同。我们可以通过测试是否 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 的构造逻辑中通常不可用。

Coq：是否可以证明，如果两条记录不同，那么它们的其中一个字段是不同的？

Coq: Is it possible to prove that, if two records are different, then one of their fields is different?

record

coq

编辑