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)
해결할 방법이 있습니까?
이것은 [CS] (http://cs.stackexchange.com/)에서 더 잘 제공 될 것입니다. –
@ LasseV.Karlsen 다른 문제와는 달리 프로그래밍 문제라고 생각합니다. SO와 유사한 (답) 증명 질문이 있습니다 (예 : [this] (http://stackoverflow.com/questions/23519043/i-cant-prove-n-0-n-with-idris?rq=1)). 나는 여기에서 응답을 얻는 것 같아 보인다. –