# Cannot discriminate 0 = 1

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.

• Have you tried just discriminate? Commented Apr 13, 2022 at 14:13
• intros contra. discriminate. gives the same result Commented Apr 14, 2022 at 0:33
• I don't know anything about UniMath in particular, but I believe discriminate is not designed univalently, so it may not work. I don't know what the authors of those exercises recommended, but the standard way to prove this "by hand" is a simplified version of the encode-decode method. Commented Apr 14, 2022 at 22:22
• Oh, I see now that there are solutions. These solve the entire exercise by exact (λ p, transportf (nat_rect (λ _, UU) unit (λ _ _, empty)) p tt). It will take some time to unpack that, but at least I have a solution now. Commented Apr 15, 2022 at 8:50

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