Isomorphismus zwischen begrenzten Naturalen und Naturalen etablieren, die Grenzen erfüllen?

Question

Kann ich in Idris einen Isomorphismus zwischen Fin n und (x ** So (x < n)) feststellen? (Ich weiß nicht, eigentlich Idris, so dass diese Typen nicht gültig sein. Die allgemeine Idee ist, dass wir einen Datentyp haben, der garantiert kleiner als n durch den Bau, und ein anderer, der garantiert kleiner als n von Test .)

Answer 1

ein Beweis in Idris 0.10.2 Hier Wie Sie sehen können, ist roundtrip2 der einzige schwierige Beweis.

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 

Wenn das, was Sie haben eine nicht-propositionalen So (x < n) statt x `LT` n ist, müssen Sie es auf den Beweis Form zu transformieren. Dieser konnte ich wie dies tun:

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