`replace`를 통해 이러한 commutativity의 증명을 완성하는 방법은 무엇입니까?

Question

this 설명서에는 증명을 완료하는 데 replace을 사용할 수있는 방법이 나와 있지만 rewrite으로 끝나며 이는 replace이라고 쓰는 구문 설탕처럼 보입니다. 나는 그것을 명시 적으로 사용하는 방법을 이해하는데 관심이있다.

정확하게 이해하면 S k = S (plus k 0)을 S (plus k 0) = S (plus k 0)으로 다시 쓸 수 있으며 k = plus k 0이라는 증명이 주어지면 반사도를 통해 증명할 수 있습니다. 그러나 replace {P = \x => S x = S (plus k 0)} {x = k} {y = plus k 0} rec으로 인스턴스화하면 S k = S (plus k 0)이라는 증명이 필요합니다. 이는 우리가 처음부터 입증하고자했던 것입니다. 간단히 말해서, 정확히 P이 무엇인지 잘 모르겠습니다.

Answer 1

아, 되돌아 보면 분명합니다. 우리가 할 수있는 경우 :

P = \x => S x = S (plus k 0) 

을 그리고, 우리는 (재귀에 의해) x = (plus k 0) 그것을 증명할 수 있습니다. 이제 y = k을 replace을 사용하면 S k = S (plus k 0)이라는 증명을 얻습니다. 이것이 우리가 필요로하는 것입니다. 즉,

plusCommZ : (m : Nat) -> m = plus m 0 
plusCommZ Z = Refl 
plusCommZ (S k) = replace 
    {P = \x => S x = S (plus k 0)} 
    {x = plus k 0} 
    {y = k} 
    (sym (plusCommZ k)) 
    Refl 

증명을 완성합니다. 우리는 P = \x => S x = S k으로 다른 방향으로 할 수 있습니다.