4
$\begingroup$

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.

$\endgroup$
4
  • 1
    $\begingroup$ Have you tried just discriminate? $\endgroup$ Apr 13 at 14:13
  • $\begingroup$ intros contra. discriminate. gives the same result $\endgroup$ Apr 14 at 0:33
  • $\begingroup$ 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. $\endgroup$ Apr 14 at 22:22
  • $\begingroup$ 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. $\endgroup$ Apr 15 at 8:50

1 Answer 1

6
$\begingroup$

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 *)
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.