Fin n
在 Idris 中,你能在和之间建立同构(x ** So (x < n))
吗?(我实际上不知道 Idris,所以这些类型可能无效。一般的想法是我们有一个数据类型保证小于n
构造,另一个保证小于n
测试。)
问问题
80 次
1 回答
2
这是 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
于 2016-03-22T02:31:02.503 回答