Cannot discriminate `0 = 1`

Question

I am just practicing a bit with coq, doing some UniMath exercises and am trying to prove (0 = 1) -> empty. However, for some reason, I seem unable to reason based on 0 = 1:

Require Import UniMath.Foundations.PartD.

Theorem exercise_1_3 : (0 = 1) → empty.
Proof.
  intros contra.
  exfalso.
  discriminate contra.
Qed.

The discriminate line gives the error No primitive equality found.

Answer 1

UniMath redefines the notation x = y away from Coq's standard eq (without also replacing discriminate), so discriminate doesn't work. You can consider discriminate to be a specialized variant of injection, which you can consider further to be a specialized variant of inversion, which should work here (as UniMath's = is still just an Inductive, and with the same definition as eq at that).

Theorem exercise_1_3 : (0 = 1) → empty.
Proof.
  intros contra.
  exfalso.
  inversion contra.
Qed.

Or you can manually replicate the proof generated by discriminate, which UniMath sort of does here. The idea is this: the most fundamental representation of the fact that O and S O are different is that nat has a matching principle that lets you make a computational decision based on O vs. S O (without requiring that the results of that decision be equal anyway, as a higher inductive might demand). So construct a function P satisfying P O := unit; P (S O) := empty, and then use O = S O to rewrite tt : P O into an P (S O).

Theorem exercise_1_3 : (0 = 1) → empty.
Proof.
  intros contra.
  pose (P n := match n with | O => unit | S _ => empty end).
  change (P 1).
  destruct contra.
  constructor.
Qed.
(* The resulting proof is basically the one you commented *)