A suspicious Isomorphism proof

Question

So I have created two representations of integers:

data ZZ : Type where
    PZ : Nat -> ZZ
    Zero : ZZ
    NZ : Nat -> ZZ

-- Represent an integer as a difference of two Nats.
data NatNat = NN Nat Nat

and two conversion functions:

toNatNat : ZZ -> NatNat
toNatNat (PZ k) = NN (S k) Z
toNatNat Zero = NN Z Z
toNatNat (NZ k) = NN Z (S k)

toZZ : NatNat -> ZZ
toZZ (NN pos neg) with (cmp pos neg)
    toZZ (NN (n + S d) n)    | CmpGT d = PZ d
    toZZ (NN z z)            | CmpEQ = Zero
    toZZ (NN p (p + S d))    | CmpLT d = NZ d

Please note, that PZ Z represents +1, and not 0.

Now I prove that these representations are isomorphic:

import Control.Isomorphism

toNatNatToZZId : (z : NatNat) -> toNatNat (toZZ z) = z
toNatNatToZZId (NN k j) with (cmp k j)
    toNatNatToZZId (NN (S d) Z)     | CmpGT d = Refl
    toNatNatToZZId (NN Z Z)         | CmpEQ = Refl
    toNatNatToZZId (NN Z (S d))     | CmpLT d = Refl

toZZToNatNatId : (z : ZZ) -> toZZ (toNatNat z) = z
toZZToNatNatId (PZ k) = Refl
toZZToNatNatId Zero = Refl
toZZToNatNatId (NZ k) = Refl

zzIsoNatNat : Iso ZZ NatNat
zzIsoNatNat = MkIso toNatNat toZZ toNatNatToZZId toZZToNatNatId

and to my astonishment Idris politely nods in agreement.

So admittedly this is exactly what I wanted, although I feel a bit uneasy with the fact that I can now prove NN 0 3 = NN 6 9:

*Data/Verified/Z> the (NN 0 3 = NN 6 9) $ toNatNatToZZId (NN 6 9)
with block in Data.Verified.Z.toNatNatToZZId 6 9 (CmpGT 2) : NN 0 3 = NN 6 9

This doesn't seem right. After all, NN 0 3 is not structurally identical to NN 6 9. So where exactly Idris got convinced that they're the same? Is this an intended behaviour (I can imagine it is) and if so, how exactly does this work?

Answer 1

Your proof for toNatNatToZZId is not total, you only covered some specific cases. If you put %default total in the Idris file, the typechecker rejects the definition. Of course, there is no total definition for toNatNatToZZId, because as you observed it is not true.