functional-programming - 有界な自然界と境界を満たす自然界との間に同形性を確立しますか?

Question

Fin nIdris では、との間の同型を確立できます(x ** So (x < n))か? (私は実際に Idris を知らないので、それらの型は有効でない可能性があります。一般的な考え方は、n構築によってより小さいことが保証されるデータ型とn、テストによってより小さいことが保証される別のデータ型があるということです。)

Answer 1

Idris 0.10.2 での証明は次のとおりです。ご覧のとおりroundtrip2、唯一のトリッキーな証明です。

import Data.Fin
%default total

Bound : Nat -> Type
Bound n = DPair Nat (\x => x `LT` n)

bZ : Bound (S n)
bZ = (0 ** LTESucc LTEZero)

bS : Bound n -> Bound (S n)
bS (x ** bound) = (S x ** LTESucc bound)

fromFin : Fin n -> Bound n
fromFin FZ = bZ
fromFin (FS k) = bS (fromFin k)

toFin : Bound n -> Fin n
toFin (Z ** LTEZero) impossible
toFin {n = S n} (Z ** bound) = FZ
toFin (S x ** LTESucc bound) = FS (toFin (x ** bound))

roundtrip1 : {n : Nat} -> (k : Bound n) -> fromFin (toFin k) = k
roundtrip1 (Z ** LTEZero) impossible
roundtrip1 {n = S n} (Z ** LTESucc LTEZero) = Refl
roundtrip1 (S x ** LTESucc bound) = rewrite (roundtrip1 (x ** bound)) in Refl

roundtrip2 : {n : Nat} -> (k : Fin n) -> toFin (fromFin k) = k
roundtrip2 FZ = Refl
roundtrip2 (FS k) = rewrite (lemma (fromFin k)) in cong {f = FS} (roundtrip2 k)
  where
    lemma : {n : Nat} -> (k : Bound n) -> toFin (bS k) = FS (toFin k)
    lemma (x ** pf) = Refl

あなたが持っているものがSo (x < n)ではなく非命題であるx `LT` n場合、それを証明形式に変換する必要があります。これは私がこのようにすることができました：

import Data.So

%default total

stepBack : So (S x < S y) -> So (x < y)
stepBack {x = x} {y = y} so with (compare x y)
  | LT = so
  | EQ = so
  | GT = so

correct : So (x < y) -> x `LT` y
correct {x = Z}   {y = Z}     Oh impossible
correct {x = S _} {y = Z}     Oh impossible
correct {x = Z}   {y = S _} so = LTESucc LTEZero
correct {x = S x} {y = S y} so = LTESucc $ correct $ stepBack so