Idris에서 재 작성 전술로 고생하다

Question

나는 자연수로부터 근본적인 수학을 구성하는 Terry Tao의 실제 분석 교과서를 살펴볼 것이다. 가능한 한 많은 교정본을 공식화함으로써 Idris와 종속 형 모두에 익숙해지기를 바랍니다.

data GE: Nat -> Nat -> Type where 
    Ge : (n: Nat) -> (m: Nat) -> GE n (n + m) 

하나 자연수 다른 이상인 것을 제안을 표현하기 :

I는 다음 데이터 유형을 정의했다.

나는 현재 서명

geRefl : GE n n 

내 첫 번째 시도는 단순히 geRefl {n} = Ge n Z을 시도하는 것이었다과 증거를 구성, 즉를이 관계의 재귀를 증명하기 위해 사투를 벌인거야,하지만이 Ge n (add n Z)을 입력있다.

geRefl : GE n n                 
geRefl {n} = x                 
    where x : GE n (n + Z)              
      x = rewrite plusZeroRightNeutral n in Ge n Z 

하지만이 유형 체킹이되지 않습니다 원하는 서명으로 통일이를 얻으려면, 우리는 분명히 아마도 보조 정리를

plusZeroRightNeutral : (left : Nat) -> left + fromInteger 0 = left 

내 최고의 시도를 포함, 재 작성의 어떤 종류를 수행해야하면 다음과 같다 .

이 정리에 대한 올바른 증거를 제시하고 그 이유에 대해 설명해 주실 수 있습니까?

Answer 1

첫 번째 문제는 외면입니다. 잘못된 위치에 다시 쓰기를 적용하려고합니다. 당신이 x : GE n (n + Z)있는 경우에, 당신은 당신이 geRefl : GE n n의 정의로 사용하려는 경우 유형을 재 작성해야합니다, 그래서 당신은

geRefl : GE n n 
geRefl {n} = rewrite plusZeroRightNeutral n in x 

를 작성해야 거라고하지만 여전히 작동하지 않습니다. 실제 문제는 GE n n 유형의 일부만 다시 쓰고 싶다는 것입니다. n + 0 = n을 사용하여 다시 작성하는 경우 GE (n + 0) (n + 0)이 표시되고 여전히 Ge n 0 : GE n (n + 0)을 사용하여 증명할 수 없습니다.

a = b 인 경우 x : GE n a은 x' : GE n b으로 바뀔 수 있다는 사실을 사용해야합니다.

replace : (x = y) -> P x -> P y 

, 우리는 쓸 수 P = GE n을 설정하고 Ge n 0 : GE n (n + 0)를 사용하여이 사용 geRefl

geRefl {n} = replace {P = GE n} (plusZeroRightNeutral n) (Ge n 0) 

로 (이드리스 완벽 수 있습니다 : 이것은 표준 라이브러리의 replace 기능을 제공합니다 정확히 무엇인가 함축적 인 매개 변수 P을 추론하기 때문에, 그것 없이는 작동하지만,이 경우에는 어떤 일이 일어나는지 명확하게 알 수 있습니다.)