Unicity of non-equality proofs

Question

If equality is decidable, all proofs of equality are "the same". I.e. for nat:

Require Logic.

Goal forall (n m:nat)  (H1 H2: n = m), H1 = H2.
  intros n m H1 H2.
  subst n.
  now rewrite Logic.Eqdep_dec.UIP_refl_nat.
Qed.

Can I prove a similar statement for non-equality?

Goal forall (n m:nat)  (H1 H2: n <> m), H1 = H2.

EDIT: the reason I asked was because I wanted define positive numbers as nats different from 0, and prove that they are equal if their arguments nat arguments are equal.

Inductive Pos : Set := pos: forall n, n <> 0 -> Pos.

Since they also contain a proof term n <> 0, one must also show that the proof terms are equal. But that is apparently impossible (without the addition of an additional axiom) because the proof term is a function. @Arthur's suggestion to use a boolean predicate is perfect here.

Inductive Pos : Set := pos: forall n, n =? 0 = false -> Pos.

It is perfect because now the proof term is an equality constraint (an inductive type) and not a function that cannot be proven equal. So below both H1 and H2 are equal to eq_refl.

Definition p2n (p:Pos) := let (n, H) := p in n.

Goal forall p1 p2, p2n p1 = p2n p2 -> p1 = p2.

  destruct p1 as [[|n1] H1], p2 as [[|n2] H2];
    simpl in *; try congruence.
  rewrite (Logic.Eqdep_dec.UIP_refl_bool _ H1).
  rewrite (Logic.Eqdep_dec.UIP_refl_bool _ H2).
  now inversion 1.
Qed.

Anton Trunov Anton Trunov · Accepted Answer · 2018-07-10T12:52:28

Since H1 and H2 are functions, you need the functional extensionality axiom to prove that two such functions are equal.

From Coq Require Import FunctionalExtensionality.

Goal forall (n m:nat) (H1 H2: n <> m), H1 = H2.
Proof.
  unfold not; intros n m H1 H2.
  apply functional_extensionality; intros H.
  contradiction (H1 H).
Qed.

Interestingly enough, one does not need UIP_refl_nat in this case.

You might want to check out this related question which shows that one should be careful when choosing representations.

Unicity of non-equality proofs

1 Answers