이드리스 재 작성은 발생하지 않습니다

Question

import Data.Vect 
import Data.Vect.Quantifiers 

sameKeys : Vect n (lbl, Type) -> Vect n (lbl, Type) -> Type 
sameKeys xs ys = All (uncurry (=)) (zip (map fst xs) (map fst ys)) 

g : {xs,ys : Vect n (lbl, Type)} -> sameKeys xs ys -> map (\b => fst b) xs = map (\b => fst b) ys 
g {xs = []} {ys = []} [] = Refl 
g {xs = x::xs} {ys = y::ys} (p::ps) = rewrite g ps in ?q 

이 오류가 내가 볼 수 있습니다 :

*main> :load main.idr 
Type checking ./main.idr 
main.idr:57:3:When checking right hand side of g with expected type 
     map (\b => fst b) (x :: xs) = map (\b6 => fst b6) (y :: ys) 

rewriting 
    Data.Vect.Vect n implementation of Prelude.Functor.Functor, method map (\b => fst b) xs 
to 
    Data.Vect.Vect n implementation of Prelude.Functor.Functor, method map (\b6 => fst b6) ys 
did not change type 
    fst x :: Data.Vect.Vect n implementation of Prelude.Functor.Functor, method map (\b => fst b) xs = fst y :: Data.Vect.Vect n implementation of Prelude.Functor.Functor, method map (\b6 => fst b6) ys 
Holes: Main.g 

왜 그것을 다시 작성하지 않는 이유는 무엇입니까?

Answer 1

Idris가 올바른 암시 적 인수를 g으로 유추하지 못하고 문맥에서 새로운 벡터를 도입하기 때문에 이러한 현상이 발생합니다.

해결 방법은 다음과 같이 증명할 수 있습니다. 첫째, 우리는 2 개의 인수를 함수에 대한 적합성의 보조 정리해야합니다 :

total 
cong2 : {f : a -> b -> c} -> (a1 = a2) -> (b1 = b2) -> f a1 b1 = f a2 b2 
cong2 Refl Refl = Refl 

은 이제 원래의 보조 정리의 증명은 간단하다 :

total 
g : sameKeys xs ys -> map (\b => fst b) xs = map (\b => fst b) ys 
g {xs = []} {ys = []} x = Refl 
g {xs = x :: xs} {ys = y :: ys} (p :: ps) = cong2 p $ g ps