idris - 一个可疑的同构证明

Question

所以我创建了两种整数表示形式:

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

和两个转换函数:

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

请注意，PZ Z 代表+1，而不是0。

现在我证明这些表示是同构的:

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

令我惊讶的是， idris 礼貌地点头表示同意。

诚然，这正是我想要的，尽管我现在可以证明 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

这似乎不对。毕竟，NN 0 3 在结构上与 NN 6 9 不同。那么 idris 到底是从哪里确信他们是一样的呢？这是有意为之的行为吗(我可以想象是)，如果是这样，它究竟是如何工作的？

Answer 1

您对 toNatNatToZZId 的证明并不全面，您只涵盖了一些特定情况。如果您将 %default total 放入 Idris 文件中，类型检查器会拒绝该定义。当然，toNatNatToZZId 没有完整的定义，因为正如您观察到的那样，它不是真的。