3

所以我创建了两种整数表示：

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. 那么伊德里斯到底是从哪里确信他们是一样的呢？这是一种预期的行为（我可以想象它是），如果是这样，它究竟是如何工作的？

4

1 回答 1

3

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

于 2019-07-27T13:15:18.270 回答