Idris에서 정확히 다시 쓰기가 어떻게 작동합니까?

Question

나는 이드리스에서 다음과 같은 제안을 쓴 다음 Prelude.Nat 소스 코드에서 영감을 사용

total 
plusOneCommutes : (n : Nat) -> (m : Nat) -> (n + S m = S n + m) 
plusOneCommutes Z  k  = Refl 
plusOneCommutes (S k) j  = 
let inductiveHypothesis = plusOneCommutes k j in 
    rewrite inductiveHypothesis in Refl 

, 그것을 증명하기 위해 유도 가설로 (두 번째 경우에) 재귀 호출을 사용하는 의미가 왜 이해 경우. 그러나 구멍을 다시 긋는 작업의 세부 사항을 거치면서, 나는 실제로 일어나고있는 일과 왜 이것이 작동하는지에 대해 정말 몰두하지 않습니다.

내가 작성하는 경우 : 나는 컴파일러에서 다음을 얻을

plusOneCommutes (S k) j  = ?hole 

:

정말하지 않습니다

- + HolyGrail.hole [P] 
`--    k : Nat 
        j : Nat 
    ------------------------------------------------------ 
     HolyGrail.hole : S (plus k (S j)) = S (S (plus k j)) 

잘 보인다. plusOneCommutes의 서명에 따라이 구멍의 유형은 (plus (S k) (S j)) = (plus (S (S k)) j)이어야합니다.

가

plusOneCommutes (S k) j  = 
let inductiveHypothesis = plusOneCommutes k j in 
    ?hole 

다음 hole 타입이된다 :

- + HolyGrail.hole [P] 
    `--     k : Nat 
         j : Nat 
     inductiveHypothesis : k + S j = S k + j 
     ------------------------------------------------------------------------- 
     HolyGrail.hole : S (plus k (S j)) = S (S (plus k j)) 

다음 inductiveHypothesis

- + HolyGrail.hole [P] 
    `--     k : Nat 
         j : Nat 
     inductiveHypothesis : k + S j = S k + j 
      _rewrite_rule : k + S j = S k + j 
     ------------------------------------------------------------------------- 
     HolyGrail.hole : (\replaced => S replaced = S (S (plus k j))) (S k + j) 

주어진 재기록 룰을 이용하여 I 쓰는 경우

한 단계 더 나아가 유도 가설 도입

S (plus (S k) j) = S (S (plus k j)) whi ch는 예상 유형이며, Idris는 ?hole을 Refl으로 자동 대체하는 증거를 완료 할 수 있습니다.

내가 당황한 것은 내가 서명에서 추론 한 것과 컴파일러가 구멍에서 유추하는 것 사이에 예상치 못한 차이가 있다는 것입니다. 내가 자발적으로 오류가 소개하는 경우 :

을 나는 다음과 같은 메시지가 :

- + Errors (1) 
    `-- HolyGrail.idr line 121 col 16: 
     When checking right hand side of plusOneCommutes with expected type 
       S k + S j = S (S k) + j 

     Type mismatch between 
       S (S (plus k j)) = S (S (plus k j)) (Type of Refl) 
     and 
       S (plus k (S j)) = S (S (plus k j)) (Expected type) 

     Specifically: 
       Type mismatch between 
         S (plus k j) 
       and 
         plus k (S j) 

Type mismatch... 부분은 위의 단계가 아니라 내가 기대하는 유형을 제공하는 When checking ... 부분과 일치한다.

- + HolyGrail.hole [P] 
`--    k : Nat 
        j : Nat 
    ------------------------------------------------------ 
     HolyGrail.hole : S (plus k (S j)) = S (S (plus k j)) 

당신이 n + S m이 유형 =의 왼쪽에서 :

Answer 1

컴파일러에서 다음과 같은 사실 의미합니다. n의 패턴 매칭 후 (S k)이고 plus (S k) (S j) 인 유형은 S k + S j이어야합니다. this question에서 나는 하나의 중요한 점을 설명했다 : 실제로 plus 함수가 작성되었고 컴파일러가 을에서 (S k) 및 (S j)에 적용하는 유형에서 패턴 일치를 수행 할 수 있다는 사실부터 설명했다. S n + m과 비슷한 상황.

지금은 rewrite입니다. Agda 프로그래밍 언어 rewrite은 Refl에서 패턴 일치를위한 구문 설탕 일뿐입니다.그리고 때로 rewrite을 Idris의 패턴 매칭으로 대체 할 수 있지만이 경우에는 불가능합니다.

우리는 비슷한 것을 시도 할 수 있습니다. 다음 고려 :

total 
plusOneCommutes : (n : Nat) -> (m : Nat) -> (n + S m = S n + m) 
plusOneCommutes Z  k  = Refl 
plusOneCommutes (S k) j  = case plusOneCommutes k j of 
    prf => ?hole 

컴파일러는 다음 매우 합리적인 것을 말한다 :

- + HolyGrail.hole [P] 
`--    k : Nat 
        j : Nat 
       prf : k + S j = S k + j 
    ------------------------------------------------------ 
     HolyGrail.hole : S (plus k (S j)) = S (S (plus k j)) 

prf하는 것은 의미가 k + S j = S k + j을 증명하는 무언가이다. 그리고 rewrite 사용 후 :

plusOneCommutes (S k) j  = case plusOneCommutes k j of 
    prf => rewrite prf in ?hole 

우리는 가지고 :

- + HolyGrail.hole [P] 
`--    k : Nat 
        j : Nat 
       prf : k + S j = S k + j 
     _rewrite_rule : k + S j = S k + j 
    ------------------------------------------------------------------------- 
     HolyGrail.hole : (\replaced => S replaced = S (S (plus k j))) (S k + j) 

rewrite 이드리스입력 Refl의 목적은, in 후 식 =의 왼쪽을 검색 소요 오른쪽으로 대체 주어진 Refl의 =이다. 그러므로 rewrite 전에 결과 유형으로 S (plus k (S j)) = S (S (plus k j))을 가졌습니다. inductiveHypothesis의 유형은 k + S j = S k + j이며 우리가 원하는 유형으로 k + S j을 얻었습니다. 이 부분은 그 람다에 replaced으로 볼 수 있습니다. k + S j 대신 S k + j을 대입하면 올바른 것으로 인식 된 것처럼 S (plus (S k) j) = S (S (plus k j))이됩니다. 그러나 Idris은 패턴 일치를 수행 할 수 있음을 기억하십시오. 그리고 S (plus (S k) j)은 자연히 S (S (plus k j))이됩니다. QED.