限界を満たしている有界自然界と自然界の同型性を確立するか？

Question

Idrisでは、Fin nと(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 

何を持っていることの代わりにx `LT` nの非命題So (x < n)ある場合は、証明フォームに変換する必要があります。私はこのように行うことができました。この1：

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