2

我正在尝试制作一个 Idris 类型的函数(j : Nat) -> {auto p : So (j < n)} -> Fin n来将 a 转换Nat为 a Fin n。为了使Z案例起作用（和输出FZ），我试图证明证明0 < n足以使FZ : Fin n. 但我无法弄清楚如何做到这一点。

我愿意制作一个完全不同的函数，只要它可以将Nat值转换为Fin n值（它们存在的地方）。我的目标是拥有一些可以将任何Nat转换为Mod n​​值的其他函数，例如，15 : Nat映射到3 : Mod 4. 我的Mod类型目前有一个构造函数，mkMod : Fin n -> Mod n.

4

1 回答 1

1

了解后LT : Nat -> Nat -> Type，我采取了不同的方法。我从声明开始：

natToFin : (j : Nat) -> {auto p : j `LT` n} -> Fin n
natToFin {n} j {p} = ?natToFin_rhs_1

. 将 case拆分n，然后p在n = Zcase 中拆分导致：

natToFin : (j : Nat) -> {auto p : j `LT` n} -> Fin n
natToFin {n = (S k)} j {p = p} = ?natToFin_rhs_2

，这基本上就是我要的证明。从那里，我拆分j并填充零大小写，留下：

natToFin : (j : Nat) -> {auto p : j `LT` n} -> Fin n
natToFin {n = (S k)} Z = FZ
natToFin {n = (S k)} (S j) {p = p} = ?natToFin_rhs_3

. 我想填写?natToFin_rhs_3，FS (natToFin j)但类型检查器不允许我填写。但是，在案例拆分后p，它很好：

natToFin : (j : Nat) -> {auto p : j `LT` n} -> Fin n
natToFin {n = (S k)} Z = FZ
natToFin {n = (S k)} (S j) {p = (LTESucc x)} = FS (natToFin j)

最后，我添加了total，一切都检查出来了。

现在唯一的问题是 Idris 似乎无法LT自动找到证据。这就是发生的事情：

λΠ> the (Fin 6) (natToFin 2)
When elaborating argument p to function mod2.natToFin:
        Can't solve goal 
                LT (fromInteger 2) (fromInteger 6)

有没有办法解决这个问题？

于 2014-11-16T23:01:03.443 回答