2014-11-15 8 views
2

I)가 작동하도록 Z 경우를 얻으려면. 유형 (j : Nat) -> {auto p : So (j < n)} -> Fin n의 이드리스 함수는 Fin nNat을 변환 할 수 있도록 노력 (출력 FZ하고있어, 0 < n을 증명하는 것이 충분하다는 것을 증명하려고 노력하고 있습니다. 그러나 이것을 수행하는 방법을 배울 수는 없습니다.이 증명 그래서 (0 < m) -> (N ** m = S n)도

나는 완전히 다른 기능을 만드는 것에 대해 열려 있습니다. 그것은 Nat 값을 Fin n 값 (존재하는 곳)으로 변환 할 수 있습니다. 제 목표는 NatMod n 값으로 변환 할 수있는 다른 함수를 사용하는 것입니다. 예를 들어, 15 : Nat3 : Mod 4에 매핑됩니다. 내 Mod 유형에는 현재 단일 생성자 mkMod : Fin n -> Mod n이 있습니다.

+0

이것은 [CS] (http://cs.stackexchange.com/)에서 더 잘 제공 될 것입니다. –

+0

@ LasseV.Karlsen 다른 문제와는 달리 프로그래밍 문제라고 생각합니다. SO와 유사한 (답) 증명 질문이 있습니다 (예 : [this] (http://stackoverflow.com/questions/23519043/i-cant-prove-n-0-n-with-idris?rq=1)). 나는 여기에서 응답을 얻는 것 같아 보인다. –

답변

1

LT : Nat -> Nat -> Type에 대해 학습 한 후에 다른 접근 방식을 취했습니다. 나는 선언으로 시작했다 :

natToFin : (j : Nat) -> {auto p : j `LT` n} -> Fin n 
natToFin {n} j {p} = ?natToFin_rhs_1 

. 기본적으로 내가 요구 한 증거이다,

natToFin : (j : Nat) -> {auto p : j `LT` n} -> Fin n 
natToFin {n = (S k)} j {p = p} = ?natToFin_rhs_2 

다음 n = Z 경우 p에 다음 n에 케이스 분할은 결과. 거기에서 j을 대소 문자로 구분하고 0을 채우면 다음을 남깁니다.

natToFin : (j : Nat) -> {auto p : j `LT` n} -> Fin n 
natToFin {n = (S k)} Z = FZ 
natToFin {n = (S k)} (S j) {p = p} = ?natToFin_rhs_3 

. FS (natToFin j)으로 ?natToFin_rhs_3을 채우고 싶었지만 형식 검사기가 나를 보내지 않았습니다. 경우가 p에 분할 후에 그러나, 그것은 괜찮다고 :

natToFin : (j : Nat) -> {auto p : j `LT` n} -> Fin n 
natToFin {n = (S k)} Z = FZ 
natToFin {n = (S k)} (S j) {p = (LTESucc x)} = FS (natToFin j) 

마지막으로, 나는 total을 추가하고, 모든 체크 아웃.


유일한 문제는 지금 이드리스가 자동으로 LT 증거를 찾을 수 없습니다 것입니다. 다음과 같은 현상이 발생합니다.

λΠ> the (Fin 6) (natToFin 2) 
When elaborating argument p to function mod2.natToFin: 
     Can't solve goal 
       LT (fromInteger 2) (fromInteger 6) 

해결할 방법이 있습니까?