2

(j : Nat) -> {auto p : So (j < n)} -> Fin na をに変換するタイプの Idris 関数を作成しようとしてNatいFin nます。ケースを機能させるZ(そして を出力する) ために、 の証明が を作成できるのに十分であることFZを証明しようとしています。しかし、私はこれを行う方法を理解できません。0 < nFZ : Fin n

Nat値を値に変換できる限りFin n(値が存在する場合)、まったく異なる関数を作成することにオープンです。Nat私の目標は、 anyを値に変換できる他の関数を用意し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

. で大文字と小文字を分割しn、その後でp大文字と小文字を区別すると、次のようにn = Zなりました。

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唯一の問題は、Idris が証明を自動的に見つけられないように見えることです。これが起こることです：

λΠ> 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 に答える