证明所以（0 < m) ->（N ** M = S n中）

我试图让(j : Nat) -> {auto p : So (j < n)} -> Fin n类型的伊德里斯功能的Nat转换为Fin n。为了让Z情况下工作（和输出FZ）我试图证明0 < n的证明是足以能够使FZ : Fin n。但我不能做出如何做到这一点。证明所以（0 < m) ->（N ** M = S n中）

我打开做一个完全不同的功能，只要它可以将Nat的值转换为Fin n的值（它们存在的地方）。我的目标是有一些其他函数可以将任何Nat转换为Mod n的值，所以th例如，在15 : Nat被映射到3 : Mod 4。我的Mod类型目前有一个构造函数，mkMod : Fin n -> Mod n。

来源

2014-11-15 James Wood

这可能会更好地服务于[CS]（http://cs.stackexchange.com/）？ –

@ LasseV.Karlsen我认为它还是一个编程问题，而不是别的。在SO上有类似的（回答）证明问题（如[this]（http://stackoverflow.com/questions/23519043/i-cant-prove-n-0-n-with-idris?rq=1）），我似乎更有可能在这里得到答复。 –

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

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

。在n = Z情况下案例分裂的n，然后p导致：

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，而这一切都签出。现在

唯一的问题是，伊德里斯似乎无法自动找到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-16 23:01:03

证明所以（0 < m) ->（N ** M = S n中）

回答

相关问题