Cubical Agda: how do I prove two things not equal

Question

How can I prove two things are not equal in Cubical Agda? (v2.6.1, Cubical repo version acabbd9)

Concretely, here are the integers as a higher inductive type:

{-# OPTIONS --safe --warning=error --cubical --without-K #-}

open import Cubical.Core.Everything
open import Cubical.Foundations.Prelude

module Integers where

data False : Set where

data ℕ : Set where
  zero : ℕ
  succ : ℕ → ℕ

{-# BUILTIN NATURAL ℕ #-}

data ℤ : Set where
  pos : ℕ → ℤ
  neg : ℕ → ℤ
  congZero : pos 0 ≡ neg 0

It's easy to show some rather odd equalities, because "equality" here actually means something which isn't quite what we're used to in the non-cubical world:

oddThing2 : pos 0 ≡ congZero i1
oddThing2 = congZero

I found a rather nasty-looking proof that successors are nonzero at https://github.com/Saizan/cubical-demo/blob/b112c292ded61b02fa32a1b65cac77314a1e9698/examples/Cubical/Examples/CTT/Data/Nat.agda :

succNonzero : {a : ℕ} → succ a ≡ 0 → False
succNonzero {a} s = subst t s 0
  where
    t : ℕ → Set
    t zero = False
    t (succ i) = ℕ

Is there a nicer proof? I can't pattern-match on the proof of succ a ≡ 0 any more; in non-cubical Agda the proof would simply be oneNotZero (), identifying the impossible pattern.

Then how can I prove the following (is it even true?)

posInjective : {a b : ℤ} → pos a ≡ pos b → a ≡ b

It's probably clear that I'm a complete novice with Cubical; but I've used Agda a nontrivial amount in the past.

Answer 1

For posInjective you can actually do a much simpler proof,

fromPos : ℤ → ℕ
fromPos (pos n) = n
fromPos (neg _) = 0
fromPos (congZero i) = refl

then posInjective = cong fromPos.

More generally one should do a so-called encode/decode proof (also called a NoConfusion proof), where one explicitly defines a relation on the datatype by recursion, and then proves it equivalent to path equality.

e.g. there's one such proof here about List

https://github.com/agda/cubical/blob/master/Cubical/Data/List/Properties.agda#L37

Injectivity and distinctness follow easily from the definition of Cover.

The possibility of this kind of proofs are actually the justification for the soundness of Agda's powerful pattern matching on inductive families. However HITs constructors in general are neither distinct nor injective, so Agda is conservative and doesn't use those properties for HITs at all.

Answer 2

Well, I have a very odd answer which I don't understand at all.

decr : ℤ → ℤ
decr (pos zero) = neg 1
decr (pos (succ x)) = pos x
decr (neg x) = neg (succ x)
decr (congZero i) = neg 1

-- "Given a proof that `pos (succ a) = pos (succ b)`, transport it back along `decr`."
posDecr : {a b : ℕ} → pos (succ a) ≡ pos (succ b) → pos a ≡ pos b
posDecr {a} {b} pr = cong decr pr

posInjective : {a b : ℕ} → pos a ≡ pos b → a ≡ b
posInjective {zero} {zero} x = refl
posInjective {zero} {succ b} x = subst t x (succ b)
  where
    t : ℤ → Set
    t (pos zero) = ℕ
    t (pos (succ x)) = zero ≡ succ b
    t (neg x) = ℕ
    t (congZero i) = ℕ
posInjective {succ a} {zero} x = subst t x (succ a)
  where
    t : ℤ → Set
    t (pos zero) = succ a ≡ zero
    t (pos (succ x)) = ℕ
    t (neg x) = succ a ≡ zero
    t (congZero i) = succ a ≡ zero
posInjective {succ a} {succ b} x = cong succ (posInjective (posDecr x))