建立滿足邊界的有界自然和自然之間的同構？

Question

在伊德里斯，你能建立一個Fin n和(x ** So (x < n))之間的同構嗎？ （我實際上並不知道伊德里斯，所以這些類型可能不是有效的。總體思路是我們有一個數據類型，通過構建保證小於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