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

Question

Say you have a record:

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

Can we prove:

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

If so, how?

On the one hand, it looks true, since Records are absolutely defined by their fields. 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?

---

As a comparison, note that if there is only one field in the record, we are able to prove the respective lemma:

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?

That is precisely the point: we need to figure out what makes both records different. We can do this by testing whether 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.

Here, Nat.eq_dec is a function from the standard library that allows us to check whether two natural numbers are equal:

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

The {P} + {~ P} notation denotes a special kind of boolean that gives you a proof of P or ~ P when destructed, depending on which side it lies on.

It is worth stepping through this proof to see what is going on. On the third line of the proof, for instance, executing intros em leads to the following goal.

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

If en and em hold, then the two records must be equal, contradicting He1e2. The congruence tactic simply instructs Coq to try to figure this out by itself.

Edit

It is interesting to see how far one can get without decidable equality. The following similar statement can be proved trivially:

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

By contraposition, we get

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

It is here that we get stuck without a decidability assumption. De Morgan's laws would allow us to convert the right-hand side to a statement of the form ~ P \/ ~ Q; however, their proof appeals to decidability, which is not generally available in Coq's constructive logic.