一个可疑的同构证明

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

令我惊讶的是，伊德里斯礼貌地点头表示同意。

所以诚然，这正是我想要的，尽管我现在可以证明这一事实让我感到有点不安 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 不同。那么伊德里斯到底是从哪里确信他们是一样的呢？这是有意为之的行为吗（我可以想象是），如果是这样，它究竟是如何工作的？

Answer 1

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

一个可疑的同构证明

A suspicious Isomorphism proof

theorem-proving

isomorphism

idris